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.

Enums

CheckResult 🔒

Verification status for one required property on one path.

UnknownReason 🔒

Why a CheckResult::Unknown could not be discharged.