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.
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:
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.
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.
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.
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:
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?
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.
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.
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.
Create your account to get free access to the webservice.
Formal Vindications S.L, Barcelona.email@example.com