Descripció del projecte
Formal Vindications SL (FV for short) is a start-up that dedicates itself to the development of formally verified software using proof assistants and applied proof theory. Currently the main activities of FV revolve around the development of legal software, specifically related to European and other traffic regulations involving tachographs. As a society, we are increasingly dependent on software based data interpretations that may lead to wrong legal decisions due to unexpected software behavior. FV strives to provide provably correct software in order to address this issue. Furthermore, the company is one of the few companies deidicated to the beginnings of serious software homologation.
A central tool in obtaining mathematically proven correct software is the Coq proof assistant, Although proof assistants are well-understood tools to perform these activities, there are many techniques and standards still to be developed in the process. As such the project involves various aspects of pure and applied proof theory. Non-proprietary findings are published by FV and shared with the scientific community. Certain modules of the developed software are made available as open source.
FV operates in a formal consortium with Guretruck SL and the Fundació Bosch i Gimpera of the University of Barcelona and counts with a group of around 7 scientists and all the necessary logistic support.
