Module verify 

IR verification pass.

Validates structural and logical properties of the IR:

• All variable references in expressions are bound (params or quantifier bindings) (uppercase identifiers are treated as union variant labels and skipped)
• old() only appears in postconditions or temporal invariants
• Postconditions reference at least one parameter (otherwise they’re trivially unverifiable)
• Quantifiers reference known types (structs or functions) in this module
• Functions with postconditions have at least one parameter (nothing to ensure about)

Also performs coherence analysis:

• Extracts verification obligations (invariant-action relationships)
• Tracks which entity fields each action modifies (via old() in postconditions)
• Matches modified fields against invariant constraints

Structs

Obligation

A verification obligation — something that needs to be proven for the module to be correct.

VerifyError

A verification diagnostic.

Enums

ObligationKind

VerifyErrorKind

Functions

analyze_obligations

Analyze a verified IR module for verification obligations.

verify_module

Run verification checks on an IR module.