Before the theorem prover: verification is older than the alphabet
◐ theme
TL;DR — if you read nothing else
Verification is older than writing. By ~3300 BC, sealed clay envelopes carried a redundant copy<br>of their own contents —<br>and on one influential (contested) reading, writing itself grew out of this checking technology.
The full modern toolkit existed by antiquity: checksums, expected-vs-actual<br>audits, inverse-operation result<br>checks, conformance standards,<br>acceptance tests, split-key authentication, signed + timestamped verification<br>certificates.
The fullest system, 375/4 BC: Athens carved a complete verification system into marble — written<br>acceptance spec, standing daily verifier (a public slave, tested every day), per-defect verdict→action table, sanctions on the checker<br>himself.
The ancients even knew their checks' limits: casting-out-nines is provably blind to ±9k<br>errors; the Talmud openly concedes its letter-count expertise<br>had decayed.
The 20th century added exactly two things: specifications became theorems<br>(all inputs, not this coin), and the checker became an artifact that can itself be checked.
The theorem prover is new. The job is five thousand years old. Seven well-travelled claims did not survive the fact-check and are not in the essay — six refuted on the evidence, and one that had no evidence to refute. They are in the graveyard.
Contents<br>The mapWhat counts as formal?1 Mesopotamia<br>2 Indus3 Egypt4 India5 China<br>6 Greece7 Rome8 Text checksums<br>9 The verdictScoreboardGraveyardReferencesMethod
MAPFive thousand years of verification, on one line
Click any dot to jump to its chapter · click a legend chip to filter
View as table<br>PracticeModalityDate
The taxonomy was complete before Rome fell. Each dot is a museum object, an inscription,<br>or an edited text.
§0What counts as “formal”?
"Verification" alone is everywhere in history — every witness oath and<br>market inspection qualifies. To keep the word formal honest, every artifact here is graded on four<br>ingredients. Almost nothing ancient scores four for four. What is remarkable is how much scores three — and how early.
Specification<br>an explicit reference,<br>distinct from the artifact
Procedure<br>an algorithm, not an<br>expert opinion
Soundness<br>a reason the check catches<br>what it claims to
Institution<br>mandated & repeatable —<br>law, office, ritual
The rubric. Each chapter carries its scorecard; the full scoreboard<br>is at the end. Jump ahead if you want the comparative view first.
§1Mesopotamia: verification before writing
Where Susa · Uruk · DrehemWhen ~3500 BC → 4th c. BC<br>Hold in hand Louvre Sb 1932 · Met 11.217.3 · BM 46550<br>Sources 1234567
Ur III accounts<br>SPΣI<br>four for four, four thousand years ago
The token envelopes are the earliest physical verification artifacts we have — redundant-count<br>checking, attested even by the leading skeptic of the<br>tokens-to-writing theory. When the envelopes flattened into tablets,<br>the checking structure came along and got stronger: totals on the reverse that anyone can<br>re-add, "theoretical amounts" as<br>specifications, and by 2039 BC the balanced account —<br>expected minus actual, closed to the fraction of a shekel, on a tablet you can visit at the<br>Met.
The balanced account · Met 11.217.3 (Ur III, silver, in shekels)
DEBIT — EXPECTED
201.42<br>CREDIT — DELIVERED
140.19<br>la₂-ia₃ (deficit) = 61.23<br>carried into next year's debits
Debits − credits close exactly. The arithmetic of this tablet balances to the last<br>fraction: state-mandated, periodic, rule-governed, arithmetically<br>sound.<br>Cuneiform tablet: balanced account of Dugga · Drehem · ca. 2039 BC · The Metropolitan Museum of Art 11.217.3
The oldest soundness argument · "the Technique," Old Babylonian → BM 46550
compute
1/n
invert
n′
compare
n′ = n ?<br>✓ RECOVERED
Compute, invert, confirm — a verification idiom with a millennium of service life:<br>attested Old Babylonian (~1800 BC), still executed twice-in-succession on Achaemenid-era<br>BM 46550. Any programmer who has round-tripped a serializer<br>knows the move. mitt pw ∎
Insight<br>Incentives are not procedures. Hammurabi §229 makes the builder bear the cost of failure —<br>outsourcing verification to fear. A procedure makes the check bear it. Modern equivalents of both<br>exist; only one of them is verification.
Read the full chapter · envelopes → tablets → balanced accounts → Hammurabi<br>The token envelopes (~3500–3300 BC) are the earliest physical verification artifacts we have. What is attested is redundant-count verification: the external marks let<br>you check the number and shape of the sealed tokens. A stronger claim<br>you will sometimes read — that the surface marks were a full semantic mirror of the contents, an exact "golden<br>reference" — does not survive scrutiny; the quote usually cited for it actually describes the solid tablets that<br>replaced envelopes around 3200 BC. That subtlety was caught,<br>on re-reading the source in context — one paragraph further down than the quote usually stops. The difference...