The FV Time Manager

The team has developed a Coq verified library for time conversions between UTC and Unix, including leap seconds [to be published]. More precisely, the Coq Time Library is a verification project consisting of a library for managing conversions between formats of time (UTC and timestamp), as well as some commonly used functions like sums, computation of a duration between two times, etc.

There are of course many libraries to perform conversions between time formats. However, our library incorporates two crucial aspects:

  1. It includes leap seconds. Leap seconds are part of the UTC standard, but they are not usually counted in this kind of general-purpose libraries, because the error is small and irrelevant for many purposes. However, it can be relevant for some, like computations that are meant to enforce a law or regulation, or for critical systems.

  2. It is formally verified, which means that we provide computer-checked mathematical proof that the algorithms to perform time conversions behave exactly according to a simple, human-readable specification.

The FV Time Manager is the extraction of these verified algorithms to a computer-efficient language like OCaml, so that it can be used as time manager in industrial projects. Our team can also provide wrappers to other programming languages to facilitate the integration of the manager in developments.