[Tock Verification] Re: Progress verifying the Tock timer using Verus

Eric, Thanks for posting that report, and I'm pleased to meet you. I haven't used Verus except for simple examples, so it was enlightening to see how the limitations of the system posed problems for real code. David Dill