Correctness was never
a property of the tools.

01 · The name

A specification must say what a step leaves alone.

In TLA+, every action describes how the state changes, and UNCHANGED names what it does not touch. The keyword exists because silence is ambiguous. A step that says nothing about a variable has not promised to leave it alone. The author has to account for every part of the state, including the parts that stay the same.

The name is borrowed for that discipline. Building software well means saying, explicitly, what must never change while everything around it does.

02 · What has not changed

Every generation moved further from the machine. None moved away from the question.

Punch cards gave way to compilers, compilers to Unix and C, C to IDEs and package managers, and those, now, to agents that write code from a paragraph of English. Each step let programmers think less about the machine and more about the problem.

None of them answered whether the program is right. That question has always been settled the same way. Understand the problem well enough to state what must hold. Write the code. Then check, by every means available, that it holds. The tools changed how fast the middle step goes. They did not touch the first or the last.

This is the claim unchanged is named for, and the reason its work starts with the first step rather than the second.

03 · A proof proves a sentence

A machine-checked proof is exactly as good as the claim it checks.

Proofs are becoming cheap. Models now write proofs that run to hundreds of thousands of lines, and a proof checker confirms each one without anyone reading it. That is real progress. It also moves all the risk to one place: the statement being proved.

A checker confirms the theorem as written. If the theorem says “this program never raises a sanitizer error” and the intent was “this program never touches memory it does not own”, the checker will accept the first and say nothing about the second. A recent audit by FOCS Lab at NUS shows exactly this in published proofs about widely used open-source libraries. It found a lifetime rule absent from a pool's contract, invariants that admit a write one byte before a buffer, and test harnesses that never exercise the client sequences where the documented hazards live. The proofs were valid. The claims were narrower than they looked.

Inferring what code does is not the same as deciding what it should do. The second is a human judgement. It needs someone who understands the problem to write the claim, and someone else to read it and try to break it. A specification nobody reads guarantees nothing anyone wanted.

04 · Why many verifiers

Every checker has an oracle and a horizon.

A sanitizer knows the bounds of the allocations it was told about. A fuzzer knows the inputs it happened to try. A model checker knows the states inside its bound, a simulator the schedules it drew, a history checker the operations its clients issued. Each one is precise within its oracle and silent beyond its horizon, and silence is easy to mistake for safety.

So no single tool is trusted with a claim. The same property is checked by verifiers that do not share an oracle: a model of the design, property tests and fuzzing on the code, deterministic simulation under faults, history checkers on real client traces, and, where it pays, a proof. Each one is first shown that it can fail, against defects planted on purpose. A checker that has never failed has not been tested.

• Model checkingthe design, within a bound
• Property tests and fuzzingthe code, on generated inputs
• Deterministic simulationthe system, under faults
• History checkerswhat clients actually observed
• Planted defectsthe checkers themselves

05 · What is published

The software in full. The claims in full. The reasoning, redacted.

Every product is open source. With it, each claim the product makes is published in full: in prose, and in the formal statement that is checked. So are the verifiers that test each claim and their results. Anyone can read what is promised, run the software, and try to show the promise false.

The models and proofs that establish those claims are published redacted. The statements are visible and the discharge is not.

\* A read returns the last committed value, or refuses. Never anything else.THEOREM CorrectOrRefuse == Spec => [](Served => Correct \/ Refused)PROOF  <1>1.   <1>2.   <1>3.   <1> QED BY 

06 · Why the line falls there

When code can be regenerated, the durable asset is knowing it is right.

An idea can be described in a paragraph, and an agent can turn the paragraph into a working implementation in an afternoon. Neither the idea nor the code is scarce any more, and publishing both costs little.

What remains expensive is the assurance: models that describe the design faithfully, proofs tied to the code that ships, simulation harnesses that reach the failures that matter, and defect corpora that show the checkers can fire. That work takes years and does not regenerate from a prompt. Publishing the claims keeps them open to challenge. Withholding the discharge keeps the work that earns them.

• The ideapublic
• The codeopen source
• The claims and their resultspublished in full
• Models, proofs, harnesses, defect corporaredacted

07 · Complete access

For teams that need to own the assurance.

Some organisations need more than the software: they need to extend it, certify it, or stake their own systems on it. For them the complete set is available. That means unredacted models and proofs, simulation harnesses, planted-defect suites and the full record of findings, each tied to the revision it covers.

Available by licence or acquisition, arranged case by case. arriqaaq321@gmail.com

08 · Who builds it

Farhan Ali Khan

An engineer working on storage and distributed systems, based in Bengaluru. He led the storage team at SurrealDB, where he built SurrealKV, an LSM-tree key-value store in Rust. Before that he worked on immudb at Codenotary, and holds a patent on deleting data from a database designed to prove nothing changed. Earlier work spans infrastructure and data systems at VMware, Cisco and GreedyGame.

The method here is the one he works by: read the paper, build it small, start from what must always be true, and point different kinds of checker at the same claim.

farhan.arriqaaq.com · GitHub · LinkedIn