# 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.