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"

Why do our clients want to contact us?

We are a start-up consulting team on error free software specialized in legal issues:

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?

Verified Software for Legal Applications

More specifically…

The advantage of the process we offer is that we provide law-makers a method of checking consistency, applicability and precision of their laws. How?

We offer a combination of mathematically designed laws with corresponding software which is formally verified, called a formally verified pair. In essence, a formally verified pair is incorruptible proof 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 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

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
Technical specifications of the Ocaml library.

Try the time manager online

Try it now

Contact Us

Our headquarters are located at the center of Barcelona:

Contact us via email in the form below:

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