public Certification of a Specification and
its Software (PCSS)
We guarantee the mathematical correctness of your specification and its exact transmission to the
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
Our philosophy
If we want to create perfect software, we would not write a single line of code , just focus on technical and formal specifications. The code is obtained by the formally verified extraction mechanism
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.