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