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 employ reverse programming, where we prove there are algorithms meeting their specifications. The proof is developed in constructive logic, therefore, the proof allows for automatic code extraction, coming with a certificate.

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.

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)