Towards Public Certification of a Specification and its Software

We live in the era of software. From DNA sequencing to the auto-pilot of a plane or a car, from facial recognition to the controller of a space shuttle, software is pervasive in the functioning of our world.

However… How do we know that software does what it's supposed to do? How do we know that DNA sequencing software actually “sequences DNA”, that facial recognition software actually does “facial recognition”… How can we make correspond code lines with “sequences DNA” and with “recognizes faces”?
How can we prove that some code is satisfying a “specification”? Is it possible? If it is, who can understand the “specification”?
These questions are on the edge of the highest level of knowledge in mathematics, philosophy and computer science. If these questions cannot be answered, no certification of software is possible, which condemns humanity to live by the law of the jungle. Even the meaning of certification of software is not defined yet.

Our team is working towards this end, and is convinced to have gathered enough knowledge to surpass the current limitations of computer science and reach such a goal. There's light at the end of the tunnel.

We are able not only to provide formally verified software according to a formal specification, but also to certify that existing verified software is according to a formal specification, including a jump from formal specification to natural language, to make it feasible to understand for non- experts, and of course including proofs that the specification follows the required mathematical properties (consistency, completeness, correctness…).

Our targeted clients are those who need to prove that their software follows a specification which, at the same time, should be feasible to understand and follow all mathematical rules to avoid bugs and crashes.

We develop software that doesn't need to be tested – let's repeat that calmly, software that doesn’t need to be tested, because it's proved “perfect”.

“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)

The future of the Formal Verification

The formal specification follows physical and computational limits (it is a representation of some part of the physical world and can be computed)

This is the key point in our definition of Public Certification of a Specification and its Software. In cases like the Ariane 5 rocket explosion (1996), the Mars Climate Orbiter crash (1999), Schiaparelli (2017), US and Canadian definition of driving time for ELD, etc., the issue was the incorrect understanding of physical consequences of mathematically formally verified software.


Once we know how to prove that our formal specification is mathematically consistent and unambiguous, once we know how to prove that the code does exactly what the formal specification says it should do, once we have public certification to understand the formal specification… then, and only then, we will finally have the tools to work in the greatest question: what should the code do? Can we advance what are all physical consequences?


This is the main issue in modern formal verification. To get a perfect code isn’t such a big issue in some cases. To understand exactly the consequences of what the code does is the first key question. Once we are able to understand that,then second questions can be posed: what should the code do?


There won’t be a final answer for that question, each business will find its way and will be in a continuous evolution. But we can give the right tools to transmit any answer to this question from the technical specification to the final code.



A perfect example of this issue is the autonomous car. There is no one in the world qualified to say what the autonomous car should do: there are open philosophical, ethical and legal questions. But without getting into that, there’s a previous concern:can anyone prove what the autonomous car actually do? Our aim is to provide the tools to answer this kind of questions.