Verified software for legal applications


Our society depends on software
Software is present in all areas of our lives, and the expansion and complexity of these applications continues to advance exponentially, as well as our dependence of them.
Safety and security
Achieving the infallibility of the most critical systems for society is an increasingly necessary milestone, especially in a context where machines and their processes are starting to be automated and autonomous. Legislation to guarantee the safety of all critical systems has started.
Threat to our legal system
Is software used as legal evidence in judiciary cases reliable? If it is not formally verified, the answer is no. To depend on a fallible source of information while having the possibility of developing an infallible solution leads to a direct threat to the rule of law.

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.

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.

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:

  • Mathematical 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


Research

We are deeply involved in generating knowledge for the benefit of all. We dive between academia and the private sector, researching the ethical and logical implications of the application of verified software to quantitative laws. An example of a recent publication.


Our team

Collaboration with academic institutions

As a high scientific value start-up company, we work in close collaboration with Universitat de Barcelona. We offer apprenticeships to the best students of Logic, promoting their learning process while offering an early chance to apply their knowledge into the private sector. In our 2017 and 2018 editions, we have offered courses teaching lambda-calculus, type theory, intuitionistic logic, formal verification in Coq, and functional programming in OCaml. The most promising students have developed themselves, and have later chosen to work with us.

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.

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.

Time Management web service

Example of the use of the web-services

Technical specifications of Ocaml library.

Register

Create your account to get free access to the webservice.


Contact


Formal Vindications S.L, Barcelona.

info@formalvindications.com
Project funded by the "Ministry of Science, Innovation and Universities ", the "State Agency for Research " and the "European Regional Development Fund " (ERDF)