Formal Verification · All levels
Formal Verification Glossary
Shared vocabulary for properties, assumptions, convergence, and signoff evidence.
Terms to use precisely
Vacuity: property passes because trigger or meaningful path never occurs.
Reachability: legal scenario can be exercised under current assumptions.
Bounded proof: no counterexample up to depth N, not full-time guarantee.
SEC: equivalence allowing latency/state movement under correspondence rules.
First divergence: earliest semantic mismatch point in proof trace.
Residual risk: unresolved uncertainty after current closure evidence.