Proof Technologies Ltd specialise in cutting-edge mathematical proof software for use in formal methods and mathematics formalisation. We also provide professional consultancy services in high-assurance software development and functional programming.
We believe that formal proof can transform the worlds of software and mathematics, and we want to help make this happen. As well as our proprietary software for industrial formal methods, we produce open source tools for HOL theorem proving, and are actively involved in the research community.
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.