Machines change.The work is unchanged.
Software built around models, proofs and verifiers.
The code orbits.
The model holds.
Rewrite it every week, by any hand. What it must satisfy stays at the centre, and every checker measures against it.
01Method
Three steps. Every era.
The tools have changed every decade since the first program was written. The steps that make software correct have not.
- 01
Understand
Write down what must always be true, in words a person can read and argue with, before any code exists.
- 02
Write
By hand or by agent. Writing is the one step machines changed, and it was always the smallest of the three.
- 03
Verify
Point different kinds of checker at the same claim. Trust none until it has been shown it can fail.
\* What must always be true, written before the code.\* A committed transaction is never lost. Inv == \A t \in Txns : Committed(t) => Durable(t) THEOREM Spec => []Inv
VARIABLES tools, understand, write, verify Next == /\ tools' = "punch cards" /\ UNCHANGED <<understand, write, verify>> \* 1951 punch cards · 1957 compilers · 1972 C · 1991 IDEs · 2026 agents
model Inv holds over every reachable state okproperty round-trip, idempotence, 25,600 cases oksimulation 4,096 seeds under crashes and partitions okhistory no lost writes, no G2 anomalies oksabotage every planted defect convicted ok \* a checker that has never failed is untested
02Inspection
Code grew 100×. Review didn’t.
- 01
Code arrives faster than review.
The agent’s hopper never empties. Put a single check on the line, even a proof, and anything it does not measure ships.
- 02
Each check measures one thing.
Add stations that measure different properties, and the defect the first one passed is rejected by the next.
- 03
Checks that keep pace.
Every part, every station, at the speed the code arrives. No defect waits for a reviewer, and none reaches the bin.
03The claim
Proved is not the same as right.
A checker confirms the sentence you wrote, not the one you meant. Whether a proof is worth having depends on a claim a person has read and argued with.
struct S { char buf[20]; unsigned char op; }; for (i = 0; i < n && i <= 20; ++i) // meant: i < 20 dst[i] = in[i]; handlers[x->op](); // op is the 21st byte
- Proved
- Never raises a sanitizer error, on any input.
- Holds
- Meant
- Never writes outside
buf. - Fails
- Result
- The 21st input byte rewrites
opand selects the admin handler. Every check stays green.
The oracle is partial.
The sanitizer was never told where
bufends.Agreement is not correctness.
Two builds can be wrong the same way.
The harness is the horizon.
What no harness runs, no proof covers.
Rewarded provers take shortcuts.
The weakest claim that passes gets proved.
After “What does verified memory safe even mean?”, FOCS Lab, NUS, November 2026.
04Drift
A model drifts. A proof can agree with anything.
- 01
Zeroed on the model.
Three gauges, three verifiers, all calibrated on the master block: the model the code was meant to match.
- 02
The code drifts.
The workpiece rises. Every gauge that touches it reads the drift, and the finding is plain: the code no longer matches the model.
- 03
One gauge agrees with anything.
Re-zero a gauge on the code itself, as a proof checked only against the code it came from is, and it reads zero whatever happens. Only the disagreement gives it away.
05Verifiers
A verifier for every way to be wrong.
A replicated log, a parser and a cipher fail differently. Each domain gets the checkers that see its failures, named with what they cannot see.
Catches split brain, lost acknowledged writes, stale reads under partition.
Blind to faults the nemesis never schedules.
Catches linearizability violations and isolation anomalies: G0, G1c, G2, lost updates.
Blind to operations no client ever issued.
Catches rare orderings of time, network and disk, replayed exactly from a seed.
Blind to anything outside the simulated world.
Catches data lost, or resurrected, after a crash at any point.
Blind to devices that break the disk model.
Catches races, deadlocks and weak-memory reorderings.
Blind to protocols too large to enumerate.
Catches crashes and broken contracts: round-trips, idempotence, equivalence to a reference.
Blind to deep states, and bugs the reference shares.
Catches out-of-bounds access, use-after-free, undefined behaviour.
Blind to object bounds the tool was never told.
Catches optimizer logic bugs and floating-point error: wrong answers that never crash.
Blind to relations the metamorphic rule does not state.
Catches protocol attacks, known-bad edge cases, timing leaks.
Blind to the gap between the protocol model and the code.
Catches a suite that passes because it cannot fail.
Blind to defect classes nobody thought to plant.
06Software
Open source, built unchanged.
Each product ships with its claims, the models it was designed against and the checkers that convict its bugs. Waraq, a B+tree database, comes first; three more follow.
-
001
Waraq
ورقA fast B+tree ACID database, built to be the fastest in Rust. In-memory speed while the working set fits in RAM, near device rate when it spills to NVMe, and correct or refusing, never a plausible wrong answer.
In development
- 002
Faris
فارسComing
- 003
Tahqiq
تحقيقA black-box tester for key-value stores: drives a target over its own protocol, injects process, disk, network and clock faults, and checks the history against its contract.
Designing
- 004
Sila
صلةAn embedded-first data system with optional object storage: storage, a query engine, and multi-node and edge.
Designed
The tools will keep changing.
The method stays unchanged.
Models and proofs at the centre, the code held to them, and every checker named for what it cannot see.