Concurrency

Verus provides the VerusSync framework for verifing programs that require a nontrivial ownership discipline. This includes multi-threaded concurrent code, and frequently it is also needed for nontrivial applications of unsafe features (such as pointers or unsafe cells).

The topic is sufficiently complex that we cover it in a separate tutorial and reference book.