Module report 

Diagnostics and summaries for the staged verifier pipeline.

The driver and later checking stages report their per-path property results through the types in this module. Keeping these types here leaves the driver focused on orchestration.

Structs

PropertyCheckResult

Result for one required property along one path to a checkpoint.

VerificationReport

Verification report for one function target.

VisitDiagnostics

Human-readable diagnostics emitted for one path/property check.

Enums

CheckResult

Verification status for one required property on one path.