Proof Technologies Ltd
Home | Software | Publications | Various | Contact Us


We produce both open source and proprietary software, for theorem proving and formal methods:

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.