Correctness is not one thing.

A type error. A malformed payload accepted at an API boundary. A state machine that can reach a state its designer swore was impossible. A function whose central property nobody ever proved. A test suite that passes because it never generates the input that breaks. A language model that answers fluently and wrongly.

Every one of these is "incorrect." No two of them are caught by the same tool. That is the whole problem with the word: it flattens six different failure classes into one, and teams inherit the flattening. A shop that lives in its type checker believes typed code is correct code. A shop that lives in its test suite believes green is done. Both are measuring one tier and reporting it as the total.

Tiers, in cost order

We treat correctness as a ladder of tiers, run cheapest first, so the fast checks fail before the slow ones spend your patience:

1. Static. Strict types and lint. Catches the errors that never needed a runtime. Seconds.
2. Contracts. Schema validation at every I/O boundary, because the outside world does not read your type definitions. Zod-class tooling.
3. Spec. Model checking for protocols and state machines. Tools like quint or TLA+ ask the question tests cannot: is the bad state reachable at all.
4. Property. Generated inputs against declared invariants, in the Hypothesis and Antithesis tradition. The suite you did not think to write.
5. Proof. Machine-checked properties for the functions that carry the system, in the Dafny and Lean tradition. Expensive, rare, and the only tier whose answer is "cannot," not "did not."
6. Generation. Evaluation for model output, with metrics and thresholds, because "the demo looked good" is not a gate.

One gate

The tiers report into a single gate with a single contract: non-zero exit means not correct enough to ship. Two rules keep the gate honest. A finding above the configured threshold fails, and a tool crash fails, because a checker that crashed checked nothing. But a tier whose tooling simply is not installed reports unavailable and does not fail: a provisioning gap is not a correctness failure, and punishing it teaches teams to turn checks off. Strict mode flips that for CI, where a missing prover should be loud.

That one design choice is what makes the ladder adoptable. A project starts with two tiers it gets for free, and each additional tier is a decision about the work, not a rearchitecture. The categories stay open: swap the model checker, swap the prover, the gate does not care.

Why a small practice bothers

We are a small practice that builds for people holding data they can't afford to leak. At that size discipline has to be mechanical, because there is no review board to catch what the tooling missed. The gate is how we keep the promise on our about page: where it matters, prove properties instead of asserting them. Not everything gets a proof. Everything gets a tier, and the gate knows which one.