Declaring Invariants
An invariant is a property that must hold at the actor boundaries the verifier cares about: after initialization, at public/exported method boundaries, and before/after suspending await points. Actor invariants express global facts that every public operation must preserve.
Invariant Preservation
Every public/exported method must maintain actor invariants. The verifier checks this by injecting invariant conditions into method contracts automatically, and by checking the invariant around suspending await points.
Invariant Patterns
Common invariant shapes that appear in real actor-based systems. Use these patterns as building blocks for expressing the global correctness properties every public method must preserve.