Proof Technologies Ltd

Proof Technologies Ltd

Proof Technologies specialise in cutting-edge mathematical proof software for use in mathematics and the formal verification of computer hardware/software. We also provide consultancy in safety-critical software development and functional programming.

HOL Zero

We produce the open source HOL Zero theorem prover. This has a $100 bounty reward for soundness flaws!


We produce the open source Tactician, a utility for refactoring HOL Light tactic proof scripts.

Common HOL

We promote a standard for basic HOL system functionality called Common HOL.

HOL Glossary

We have written an extensive Glossary of HOL-Related Terminology. This covers the basic concepts required to understand the HOL logic and its implementation in theorem provers.

Contact us

Please e-mail with any general queries.