Concurrency and Unsafe Code
Verus provides a framework based on “tokenized state machines” for verifing programs that require a nontrivial ownership discipline. This includes multi-threaded concurrent code as well as code that needs unsafe features (e.g., raw pointers and unsafe cells).
The topic is sufficiently complex that we cover it in a separate tutorial and reference book.