Public Certification of Software and its necessity in Computable Law

Our work in the transportation law field has given us perspective on the kind of problems that need to be solved to develop 100-reliable software for Law applications. Formal verification is the main technical methodology, yet it is not enough by itself in this field, since the behavior of the software must be not just properly specified, but also accessible and understandable for enforcement agencies and citizens.

In this presentation we present what formal verification can (and cannot) achieve, and address the issue of accessibility via our own defined protocol, Public Certification of Software, going beyond mere formal verification. We also present a small-scale project which has gone through Public Certification - FV Time, a library for managing conversions between time formats (UTC and timestamps), as well as commonly used functions for time arithmetic.

These are the two versions of the presentation (the slides and an extended document) we gave in Barcelona, at the Conference on Algorithmic Law Design and Implementation.

Extended slides