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.
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.
Formal Vindications S.L, Barcelona.firstname.lastname@example.org