UTC time, formally verified
summary
A verified UTC conversion library implemented in Coq with MathComp that implements leap seconds (27 added since 1972) and proves bidirectional correctness between human dates/times and epoch timestamps. The project produces a three-stage extraction pipeline: abstract spec, efficient uint-refined implementation (with a uint↔nat refinement library), and a nondependent “clean” executable C extraction; it also supplies tactics that brute-force decidable finite ranges and structured error reporting. All artifacts build, extract, and run; supplementary code and data are available.
AI-written summary · about
chapters (10)
- 0:00Formal UTC time verification
- 3:03UTC time conversion challenges
- 7:25Naive implementation approach
- 11:14Correctness theorems and extraction
- 13:00Refining data types
- 16:38Extracted code problems
- 17:42Clean implementation
- 20:30Error control for practical use
- 21:36Verified UTC library summary
- 22:19Q&A
related talks
29mTime is an illusion
01h 05mWelcome To The Time Zone
58mC++20’s ＜chrono＞ Calendars and Time Zones in MSVC
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
31mA Crash Course in Calendars, Dates, Time, and Time Zones
27mI have a Date
01h 04mCoq's vibrant ecosystem for verification engineering
01h 01mA ＜chrono＞ Tutorial