# 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!

## Tactician

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
info@proof-technologies.com with any general queries.