# Concurrency

Verus provides the _VerusSync framework_
for verifying 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](https://verus-lang.github.io/verus/state_machines/intro.html).