Statically Checked Invariants
Invariants the compiler refuses to let you violate: Dafny invariant
clauses, Frama-C annotations, JML specs, type-level witnesses like
NonEmptyList. Where database invariants are
checked by a live system against live data, these are proved once, at build
time, for all possible executions.
Sensor properties
| Property | Value |
|---|---|
| Oracle strength | High — a discharged proof obligation is definitive for its claim |
| Independence | High — the prover is outside the code |
| Scope | Module |
| Feedback latency | Milliseconds to minutes |
| Actionability | Blocking — the build fails |
| Type | Predictive |
What it cannot detect
Invariants that were never written down, and invariants whose statement is wrong. The gap between “the invariant holds” and “the invariant is the one the business needs” is exactly what business invariants measure from the other direction.