[Tock Verification] Progress verifying the Tock timer using Verus

14 Jan 2025

      Hi all,

I wanted to share an update on my progress verifying the Tock timer using
Verus, with a report attached to this email. TL;DR: While the process has
been challenging due to the effort required to adapt Tock code for the
Verus verifier, there’s promising progress, and I’m optimistic about the
outcome, although I lack time to work on it.

Best,

Eric Mugnier
Ph.D. @ UCSD