As a first step, Dr. Joost J. Joosten and his team present the FV Time Manager, a software that converts and manipulates different time stamps and arithmetical operations on them. This time manager is novel and revolutionary in two aspects: firstly, it is generated from a formally verified source and as such, this source code is guaranteed via a mathematical proof to be error-free; secondly, it incorporates so-called leap seconds, small time variations which most pre-existing time managers have so far ignored, but nonetheless should be accounted for according to the law. The latter has a real impact on road transportation, as shall be shown in the presentation.