Public Certification of Specification and
its Software
We guarantee the mathematical correctness of your specification and its exact transmission to the
final code.
Quote
It is not possible to establish a proven equivalence among formal specification and natural language, nor even to any intermediate abstraction level of mathematical language. Those worlds are disconnected. We also have the issue that a sentence in natural language can be interpreted in different ways: natural language is ambiguous. Knowing that, there are chances to find solutions.
~ Guillermo Errezil
(Director)
Quote
Our philosophy
We believe that critical systems for the security and safety of citizens must follow the highest software standards. We develop formally verified software for public administrations, currently in the area of law-enforcement, while also working to reach a standard protocol for the public certification and homologation of software that claims to be formally verified.
Methodology and tools
We develop our work using the Coq Proof Assistant, a software that allows for writing both code and mathematical definitions and proofs. In front of other tools, Coq is the one that provides the capacity and flexibility to verify practically all the software produced. To this end, the MathComp library and the SSReflect proof language are immensely valuable in our industrial applications.
In accordance with this choice, we are committed members of the Coq Community and we contribute new features to both Coq and MathComp.
We have a method to create the most secure software ever invented.