We produce both open source and proprietary software, for theorem proving and formal methods:
HOL Zero is an open source basic theorem prover for the HOL logic. It is very carefully written to maximise trustworthiness, and has a $100 bounty reward for finding 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 formal proof project, 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, search, dependency analysis, and translation between dialects. This is currently under development.
We write our software to be reliable, simple-to-use 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.