Public Certification of Specification
and
its Software
its Software
We guarantee the mathematical correctness of your
specification and its exact transmission to the
final code.
final code.
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)
(Director)
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.