[Tock Verification] Re: Was: [Core WG] Re: Formal verification in Tock

At this point, we (David Dill and Livia Sun) are looking for examples of real things to verify with Verus instead of standard benchmarks. In my past work as a formal verification researcher, I've found that this is a good way to find interesting new problems as well as guiding my research in a practical direction. Someone suggested Tock, so we talked to Phil to learn more. If we continue pursuing this, we'll talk to Ranjit's group and Eric directly. If anyone knows of more work we should know about, or has more thoughts, please let us know. I may not be monitoring this forum, so feel free to send email to "David.L.Dill@gmail.com" Thanks a lot, Dave