Exhaustiveness Checking
Sector9 ensures that switch expressions cover all possible values of a type, then gives the verifier a complete case split to reason about.
Variant Contracts
Postconditions can specify different guarantees for each variant case, letting you express precise relationships between inputs and outputs based on which constructor is matched.
Option Unwrapping
Sector9 provides two verification-friendly mechanisms for extracting values from option types: the ! operator inside do ? { } blocks and pattern matching with switch. Pattern matching handles both cases explicitly; ! is only legal in the null-propagating do ? context.