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 a specification and its 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.