Invariants and Await
Actor invariants must hold at every suspending boundary, modeling the possibility that other messages executed while the actor was suspended.
Interference Model
The verifier models await interference by asking which public methods could have executed while your actor was suspended, then havocing the actor fields those methods may write.
Local vs Shared State
The verifier's escape analysis classifies variables into local (preserved) and shared (invalidated) categories at await boundaries.
Await Frames
Frame conditions that guarantee unchanged fields are weaker at suspending await boundaries, but Sector9 keeps them precise for fields no public method can write.