Proof Technologies Ltd specialise in cutting-edge mathematical proof software for the software industry and academia. We also provide professional consultancy services in safety-critical software development and functional programming.
We believe that formal proof can transform the worlds of software and mathematics, and want to help make this happen. As well as our proprietary formal methods tools for high-integrity software development, we produce open source tools for theorem proving in the HOL logic, and are actively involved in the computer science and mathematics research communities.
We have provided consultancy in safety-critical DO178/B software development, industrial formal methods using SPARK Ada and the Z specification notation, and functional programming in SML and OCaml. Our customers have included QinetiQ, Rolls Royce and Altran Praxis.