They have separate machinery for concurrent code: https://verus-lang.github.io/verus/state_machines/intro.html