It is a project funded by the "Ministry of Science, Innovation and Universities", the "State Agency for Research" and the "European Regional Development Fund" (ERDF).

Time Manager

What is a Time manager

Time manager definition:
Set of algorithms which define the time and arithmetic among dates (add time; difference, etc.). In fact, any programming framework or operating system have their on time manager).
Example of study: different driving times of the same vehicle depending of the time manager used.

We present our FV Time Manager, a formally verified software for managing UTC time, which provides public formal specifications, public software, and public mathematical proofs.

The only fully UTC consistent, time format and timestamp.

2020-01-01-00:00:00 UTC

UTC Timespan 1577836827

Formal calendar definition (different from Gregorian UTC calendar) for time interval measurement as general solution for the problem of grouping seconds in UTC calendars.

Atomic Clock FOCS-1 (Switzerland).
The primary frequency standard device, FOCS-1, one of the
most accurate devices for measuring time in the world.
It stands in a laboratory of the Swiss Federal Office of
Metrology METAS in Bern.

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.

Try the time manager online

Try it now


How-To: Use of the OCaml verified library through the command line (Windows/Linux)
Download Documentaion in English
Documentation for direct integration in OCaml
Download Documentaion in English