Formal Vindications

Formally verified software for public systems

Our work Learn more

Funding

Grant RTC-2017-6740-7 funded by MCIN/AEI/ 10.13039/501100011033 and, as appropriate, by "ERDF A way of making Europe"

Towards certified 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)

More specifically…

Our current work lies in the field of Law, in particular of those laws that are checked or enforced by software.

We offer a combination of mathematically designed laws with corresponding software which is formally verified. We provide computer-checked proofs that:

  • Mathematically speaking, the software is a formal and exact implementation with zero errors of the technical specifications provided in the law.

  • The law is logically consistent, unambiguous, and algorithmic. All these properties are mathematically proven.

  • The law is within computably feasible limits.

  • The physics parameters verifiably match up to the physical reality.

In this way governments can have complete control and peace of mind that both the law and the enforcement software are irrefutable, which in turn improves the quality of law enforcement and reduces enforcement implementation time and effort.

Our goal includes that the certification of the software is public, in the sense that, in principle, everyone can (be trained to) understand what is verified and why. This accessibility feature is crucial to guarantee the quality of democracy.

Why do our clients want to contact us?

Formal Vindications is a start-up consulting team on error-free software specialized in legal issues:

We teach client tailored crash-courses on formal verification of software and zero-error programming. Any campany or university that wishes education in formal verification of software should contact us

We advise governments and public sector bodies who are responsible for drawing up and implementing legislation. Over time our clients have come to realise that anything written in natural language cannot be unproblematically converted to consistent algorithms, that is why they now seek “computable” laws.

We develop Computable Laws, which are laws drafted as technical or formal specifications in order to control automated processes based on digital inputs.

We develop reliable software for legal proofs, since regular software can fail to output real proofs, it ought not to be trusted to manage data in the judiciary part of our system.

Our key sectors include road-transport legal software, as well as the vehicle, aviation and financial industries.

How do we develop our products?

We use the Coq Proof Assistant to implement our algorithms, as well as the mathematical specifications for them. We prove inside Coq that the code meets the specifications. After that, we extract this verified implementation to a computer-efficient programming language, OCaml. We provide wrappers to other programming languages to use our tools from different developments.

Why do our clients want to contact us?

Our social 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.

Analysis document

The tachograph example

In «Industrial software homologation. Theory and case study; Analysis of the European tachograph technology with EU transport Regulations 3821/85, 799/2006 and 561/06 and their consequences for European Citizens» you will find a detailed analysis of potential problems linked to non-verified software. It features:

  • Technological roots and causes of the problem.

  • In-depth and comprehensive case studies.

  • Real examples from EU tachograph technology.

The scientific paper “Industrial software homologation. Theory and case study; Analysis of the European tachograph technology with EU transport Regulations 3821/85, 799/2006 and 561/06 and their consequences for European Citizens” deals with potential problems associated with non-verified software in tachographs and also presents the first workable solution to the issue using the formal verification of software. Some of the highlights include-in depth analysis of the following:

leap seconds are a key part of the UTC time standard, yet Microsoft’s DateTime library does not incorporate them. Alarmingly, Microsoft’s DateTime library is used by all enforcement agency tachograph analysis software to convert TimeReal numbers recorded by the tachograph into UTC time. (Chapter 15 - UNIX-UTC problem) Contradiction in UTC - Unix Time: Tachograph data is measured and calculated according to the Unix standards however disturbingly the legislative framework provides for UTC standards. Analysis of data and the ruinous financial outcomes. (Chapter 15 - UNIX-UTC problem) Errors in the application of the minute rule – that the longest continuous activity in a minute will be logged as that activity - along with dialogue of the devastating financial penalties. (Chapter 14 The definition of driving time: specific software analysis through different versions) Tachographs also have black holes! Discussion on the random registering of driver activities, (including driving time!) depending on how time is calculated. We do not know if time registered as DRIVING in Unix format by the tachograph, should actually be REST or DRIVING in the equivalent calendar minutes in UTC format. (Chapter 15 - UNIX-UTC problem) Expert technical and legal digest on impossible and erroneous recording values from EU tachographs. More than 20 European case studies with resulting fines. Commentary on the unjust and inappropriate outcomes suffered by European citizens, drivers and companies. What is DRIVING TIME duration in an interval? Close investigation of the legal texts reveals that there is no definition of driving time duration in an interval in 3821/85 or in 799/2016. How can that be possible? Driving time is the central notion of the tachograph business. How has the tachograph calculated the daily driving time without a proper definition? (Chapter 3)

In publishing online «Industrial software homologation. Theory and case study», we are proud to introduce the first workable proposal for a solution using formal verification of software.

This scientific document has been developed by Formal Vindications S.L. in collaboration with the University of Barcelona.

pdf
English
pdf
Spanish
pdf
French
pdf
German
pdf
Italian
pdf
Polish

A similar analysis is under development for the USA and Canada ELDs:

pdf
USA/Canada

Time manager

  1. Time manager definition: Set of algorithms which define the time and arithmetic among dates (add time; difference, etc.). In fact, any programming framework or operating system have their on time manager). Example of study: different driving times of the same vehicle depending of the time manager used.

  2. We present our FV Time Manager, a formally verified software for managing UTC time, which provides public formal specifications, public software, and public mathematical proofs.

  3. The only fully UTC consistent, time format and timestamp.

    2020-01-01-00:00:00 UTC

    UTC Timespan 1577836827

  4. Formal calendar definition (different from Gregorian UTC calendar) for time interval measurement as general solution for the problem of grouping seconds in UTC calendars.

Atomic Clock FOCS-1 (Switzerland). The primary frequency standard device, FOCS-1, one of the most accurate devices for measuring time in the world. It stands in a laboratory of the Swiss Federal Office of Metrology METAS in Bern.
Atomic Clock FOCS-1 (Switzerland). The primary frequency standard device, FOCS-1, one of the most accurate devices for measuring time in the world. It stands in a laboratory of the Swiss Federal Office of Metrology METAS in Bern.

pdf
How-To: Use of the OCaml verified library through the command line (Windows/Linux).

Try the time manager online

Try it now

Contact Us

Our headquarters are located at the center of Barcelona:

“Machines should serve our intended purposes, and we should not suffer the consequences of their unexpected behaviour.”

This website does not use any cookies. The handling of any information introduced by the user, personal or otherwise, complies with the latest GDRP regulation.