Tutorial by example

In this section, we will walk through a series of increasingly complex examples to illustrate how to use Verus’s tokenized_state_machine! framework to verify concurrent programs.