Sensor family 04
Invariants
“What must always be true?”
What belongs here
This family is defined by the shape of the claim, not by where it is enforced: a property stated once that must hold for every state or every execution. The same invariant may be checked by a type, a database constraint, an assertion in production, or a gate before promotion.
Contested placements
Because enforcement is spread across the lifecycle, entries here deliberately overlap Structural (Statically Checked Invariants) and Runtime (Runtime Invariants). The interesting fact about an invariant is that somebody stated it, not which mechanism happens to check it.
Where its signals arrive
- Static analysis / types — Build stage. Is it internally coherent and structurally valid?
- Production behavior — Production stage. What is it actually doing in the real world?
The atlas places every family on the same lifecycle grid; the framework defines the six dimensions each entry below is characterized along.
Entries (5)
Business Invariants
A successful payment implies an order eventually becomes paid. order.total == subtotal + tax + shipping - discounts.
Database Invariants
Every foreign key refers to an existing object. Every request has exactly one request_id. created_at <= updated_at.
Pre-Promotion Invariant Gates
Invariants checked at the moment of promotion, before a change can reach users: migrations must be backward-compatible, no PII column may be added without an encryption flag, the new schema must…
Runtime Invariants
You don’t need to know how the payment service works. You can observe: “5,213 payments occurred; 17 have no corresponding order transition.” That’s a sensor of correctness without understanding the…
Statically Checked Invariants
Invariants the compiler refuses to let you violate: Dafny invariant clauses, Frama-C annotations, JML specs, type-level witnesses like NonEmptyList.
Adjacent families
- Previous: Test Effectiveness — Do our tests actually detect failures?
- Next: Adversarial — Can we make our evidence of correctness fail?
- All of them: the complete catalog (this family is also anchored there at /catalog/#invariants).