We produce both open source and proprietary software, for theorem proving and formal methods:
HOL Zero is a basic open source theorem prover for the HOL logic. It is very carefully written to maximise trustworthiness, and has a $100 bounty reward for soundness flaws.
Tactician is an open source utility that enables HOL Light tactic proof scripts to be stepped through interactively. It can also be used to help tidy up a large proof, by identifying unused and duplicate theorems and slow proof steps.
Common HOL is our standard for portability of proofs and source code across HOL systems. We supply various software components to support this, most of which are open source.
Zanadu is a proprietary tool for formal specification in Z. It can parse various Z dialects, and supports type checking, animation, identification of unused and duplicate definitions, and translation between dialects. This is currently under development.
We write our software to be reliable, simple and efficient. OCaml is our main coding language, and user interaction is via the powerful OCaml command line. Part of our aim is to demystify formal proof, and our open source code has sufficient clarity and explanation to make it understandable to non-experts.