Before the theorem prover verification is older than the alphabet

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 you check the number and shape of the sealed tokens. A stronger claim you will sometimes read — that the surface marks were a full semantic mirror of the contents, an exact "golden reference" — does not survive scrutiny; the quote usually cited for it actually describes the solid tablets that replaced envelopes around 3200 BC. That subtlety was caught, on re-reading the source in context — one paragraph further down than the quote usually stops. The difference between the two claims is the difference between a checksum and a full specification.

And the reading is not one enthusiast's theory. Robert Englund, the leading skeptic of the grand token-to-writing narrative, granted exactly this much: tokens gathered and sealed into clay balls in the period before proto-cuneiform emerged around 3300 BC, with exterior impressions that "conform exactly" to the numerical signs on the earliest clay tablets.

What happened next is the part I find genuinely moving. When the envelopes flattened into tablets — when writing proper arrived — the verification structure came along and grew stronger. Proto-cuneiform accounts of Uruk (c. 3300–3000 BC) routinely carry subtotals and grand totals inscribed on the reverse face, summing the entries on the front. The document checks itself: anyone can re-add it. Modern Assyriologists do exactly that — recomputing the totals is how the decipherment is tested.

From almost the beginning, these archives distinguish what Assyriologists call theoretical amounts — expected values — the theoretical credits an account was supposed to show — from actual deliveries. That is a specification, in the engineer's sense: the number reality must be checked against.

By the Ur III period (2112–2004 BC) this had hardened into one of the most rigorous verification institutions of the ancient world: the balanced account, ni₃-kas₇-aka. A fixed two-part format — a debit section of capital and theoretical credits, a credit section of actual performance — closing with an explicitly computed deficit (la₂-ia₃) or surplus (diri), carried forward into the next period. You can stand in front of one of these — the Metropolitan Museum's tablet 11.217.3, the balanced account of a man named Dugga, from Drehem, dated to the year, month, and day: about 2039 BC.

And the scribes verified computations, not just inventories. Old Babylonian mathematics (c. 1800–1600 BC) includes a procedure now called "the Technique" for computing reciprocals in sexagesimal arithmetic — and its texts check the result by inverting it to recover the original number. A British Museum tablet, BM 46550, shows the same compute-then-verify routine still being executed — twice in succession, on one tablet — in the Achaemenid era, over a thousand years later.

One boundary case belongs here, because it is so often miscast. Hammurabi's laws (~1754 BC, Louvre stele Sb 8) famously prescribe death for a builder whose house collapses and kills the owner (§229), require him to rebuild a buckling wall at his own cost (§233), and even set a one-year warranty on boat caulking (§235). This is real, and it is on the stone. But it is a verification incentive, not a verification procedure: no Mesopotamian text prescribes an inspection or acceptance test for buildings, and scholars dispute whether the Code was enforced at all. Liability makes builders check their own work; it is not itself a check.

The Harappan civilization (urban floruit ~2600–1900 BC) left the opposite fragment of the puzzle: a specification with no surviving procedure. Cubical stone weights appear at more than forty sites across the Indus world, and when you run the corpus through cosine quantogram analysis — the statistician's tool for asking "is there one underlying unit here?" — the answer is an exceptionally clear yes: a single standard, a "Harappan shekel" of about 13.4–13.6 grams. Rahmstorf, the leading specialist, judges it cleaner than the multiple concurrent standards documented across Bronze Age Mesopotamia and Syria; a peer-reviewed 2021 PNAS reanalysis found it statistically inconsistent with having drifted out of those western systems. Weight metrology appears during the transition into the urban phase, around 2800–2600 BC, and holds for centuries.

Somebody enforced that. Statistical conformance that tight, across a subcontinent, for that long, does not happen without checking. But no inspection office, no master weight, no procedural text survives — the script is undeciphered and terse. So the Indus thread earns exactly one of the four grades (specification), and stands as the essay's standing reminder: sometimes verification is archaeologically invisible, and all you can see is its effect — the conformance it produced.

The Egyptian document I keep returning to is not mathematical at all. Papyrus Abbott (British Museum EA 10221) is the official record of a state audit — of tombs. In Year 16 of Ramesses IX, about 1110 BC, reports of royal-tomb robbery in the Theban necropolis triggered a formal commission: necropolis inspectors, the vizier's scribe, the treasury's scribe. Over four days they walked a defined list of monuments — ten royal tombs, four tombs of the Chantresses, then the Valley of the Queens — and recorded, tomb by tomb, a standardized verdict: examined this day; found intact / found to have been violated by the thieves. Each entry identifies the tomb by location and landmark, one by the depth of its shaft. The itemized list closes with a summary tally — nine intact, one violated, of ten royal tombs — that arithmetically cross-checks the entries. I redid that addition; it closes.

The report was deposited in the vizier's archives; integrity in the Queens' Valley was checked against the tomb seals, a tamper-evident reference. Checklist, formulaic verdicts, identifying specifications, arithmetic self-check, archival record. The protocol is thirty-one centuries old and an auditor today would recognise every line of it.

And then the twist that makes it modern in the uncomfortable way too. T. E. Peet, whose 1930 edition remains canonical, read the day-19 seal inspection as "a carefully staged scene": the audit sat inside a political feud between two officials — Paser, who alleged the robberies, and Paweraa, on whose watch they had happened — the commission was not disinterested, and a queen's tomb the commission passed as intact was proven robbed within a year. The procedure was sound; the verifier was compromised. Every security engineer knows this failure mode: the auditee controls the auditor. It is why SOC 2 has independence requirements, and why a compiler cannot certify itself. The Egyptians invented the audit and the audit-capture scandal in the same document.

The Rhind Mathematical Papyrus (British Museum EA 10057/10058, copied by the scribe Ahmose around 1550 BC from a Middle Kingdom original of about 1850 BC) does not just present answers — it checks them. Peet's edition notes that many problems end in an explicit "proof" showing the computed result "actually satisfies the conditions of the problem," by substituting the found answer back through the prescribed operations and closing with a QED-like formula, mitt pw — "that is it". In Problem 25, a computed quantity of 10⅔ plus its half, 5⅓, is shown to equal the required 16. The false-position problems (guess a trial number, compute forward, scale to fit: Problems 24–27, 30, 32–38) are all verified this way; Problem 31, tellingly, is left unproved. Red auxiliary numbers keep the checking separate from the working. This is the same inverse-operation idiom as the Babylonian reciprocals — The papyrus is roughly 3,500 years old.

Egypt is also where I have to kill a beloved story. You will read, in metrology textbooks and standards lore, that Egyptian working cubits were recalibrated against a royal master cubit "at each full moon, on pain of death" — often cited as the first calibration regime in history. The physical standard is real: surviving royal cubit rods (Kha's folding rule and Amenhotep II's gold-leaf rod, both in Turin's Museo Egizio) measure about 52.4 cm, and the Great Pyramid's dimensional precision is genuine indirect evidence of a consistently held unit.

But the full-moon recalibration story has no primary Egyptian source. Its earliest traceable appearance is a modern metrologists' commentary — popularized by an instruments company — that cites nothing and seems to derive from a 2005 opinion piece. The most-cited fact about the world's first measurement standard is an uncited twenty-first-century embellishment. I verified the cubit; I could not verify the ritual. (And when I pushed the "pyramid proves an enforced standard" claim, the fact-check killed it outright: exquisite construction proves careful work, not necessarily a calibration bureaucracy.)

India contributes two threads at opposite ends of the abstraction ladder. The first is a redundancy scheme for oral transmission that has no real parallel anywhere: the Vedic pāṭhas. The same text was memorized and chanted in multiple interleaved orderings — beyond the natural word order (saṁhitā), reciters learned the pada (word-by-word), the krama (each word paired with the next: AB, BC, CD…), and elaborate permutation modes (jaṭā, ghana) that weave the words forward and backward in fixed patterns. Because each mode re-encodes the same words under a different rule, a slip in one ordering fails to reconcile with the others — a purely oral error-detecting code, credited within the tradition to named grammarians. The claim commonly attached to it — that this preserved the Rigveda's word order and phonetics across nearly three millennia — is extraordinary, and I flag it as such.

The second is Pāṇini's Aṣṭādhyāyī (~350 BCE), a grammar of Sanskrit written as roughly 4,000 ordered rules with a genuine formal apparatus: a regimented metalanguage, compression devices, metarules, and — the part that matters here — an explicit conflict-resolution metarule (1.4.2, "in conflict, the later rule prevails"), intended to drive a derivation toward a single well-defined result that can be checked step by step — though how completely the architecture achieves that is exactly what modern Pāṇinian scholarship, Kiparsky included, still argues about. That checking was actually practiced: within two centuries, the commentarial tradition (Kātyāyana, Patañjali) was testing the rules against attested usage. I keep this brief, and precise: it verifies language derivations, not artifacts or computations.

The Mohist canon supplies the doctrine. The Mozi (5th c. BCE) says the hundred artisans make squares with the set-square, circles with the compass, straight lines with the string, verticals with the plumb-line, flats with the level — judging work against explicit physical standards (fa). What makes it strikingly modern is that a fa functions as what we would now call an operator-independent decision procedure — as Chris Fraser glosses the Mohist position, fa are "objective, reliable, and easy to use, so that with minimal training anyone can employ them to perform a task or check the results" — and judgment proceeds by citing a fa, comparing the object to it, and ruling that what matches the fa is "this" (correct) and what does not is "not." That is a binary, rule-governed conformance verdict, stated as a principle — the clearest ancient articulation of the idea of checking against a specification.

The device is the tiger tally (hufu 虎符): a bronze token cast in two interlocking halves, the ruler keeping the right, the field commander the left. A mobilization order was authenticated by physically matching the two halves — a forged half will not fit the cast mate. The Du tiger tally in the Shaanxi History Museum carries an inscription conditioning troop movements on the match above a threshold of fifty men, with an explicit exemption for beacon-fire emergencies — a scoped authentication requirement with an availability bypass, cast in bronze. It is, precisely, a split-key, dual-control authentication device from the Warring States / Qin era: two halves of one casting are a single factor — possession — held under divided authority.

The bureaucracy is documented in the Shuihudi Qin bamboo slips (a tomb sealed around 217 BC, some 1,155 slips — mostly Qin statutes and legal-administrative texts, alongside a personal chronicle and divination almanacs). Among them is the Xiàolǜ (效律), literally "statutes concerning checking": an audit code that penalizes discrepancies in official accounts, with fines triggered only when errors exceed set numerical thresholds — a rule-governed audit with explicit tolerances. Another statute requires every government weapon to be branded with its issuing office; on return, the physical brand is checked against the register, and a mismatch means confiscation: an artifact checked against a golden recorded reference. There is a graduated schedule of fines cascading down the supervisory hierarchy when manufactured goods fail inspection. This is the legal machinery behind the famous Qin practice of "inscribe the maker's name" (物勒工名) on products for accountability. Specification, procedure, soundness, institution: the Qin checking statutes are the essay's second four-for-four — the only artifact besides the Ur III balanced account to earn all four grades. And the incentive thread from Babylon recurs here on schedule: another Shuihudi statute makes supervising officials liable if a city wall collapses within a year of completion — Hammurabi's boat-caulking warranty, fifteen centuries on and a continent away.

A caution the specialists insist on, and so will I: the bronze crossbow triggers of the Terracotta Army, often invoked as proof of Qin "interchangeable parts" and assembly-line mass production, do not support that reading. Metrical analysis shows batch (cellular) production by small workshops, with parts still individually filed to fit and match-marked so co-fabricated pieces stayed together. The defensible analogy is accountability-marking and check-against-register, not proto-Fordism.

If you want a single ancient artifact that a verification engineer would recognize as a colleague's work, it is a marble stele dug out of a drain in the Athenian Agora in 1970. It carries the law of Nikophon, 375/4 BC, on silver coinage. The specification: Attic silver currency must be accepted when it is determined to be silver and bears the public stamp — the dēmosios charaktēr. Two conditions, conjoined, written down. The verifier: a standing public official — the dokimastēs, a state-owned slave, expert and permanent where magistrates rotated — required to sit among the bankers' tables and test coins every day, under penalty of fifty lashes if he fails to appear; the law creates a second post in Piraeus, scaling the service to the port. The verdict-to-action mapping: a good foreign imitation is returned to the presenter; a coin with a bronze or lead core, or otherwise debased, is cut through on the spot, consecrated to the Mother of the Gods, and deposited with the Council — the failed artifact physically invalidated and removed from circulation, in full view of the market. The meta-rules: sellers must accept what the dokimastēs approves, and the law orders its own publication on stone, among the bankers' tables and in Piraeus. The specification of the verification system is itself a public, checkable artifact.

The scholarly hedges are minor and worth carrying: one clause's verb is restored; the "test-cut and return" detail for passing imitations follows a 2017 restoration; and Athens likely had a dokimastēs decades before Nikophon, so the law codified and regulated an existing office rather than inventing it. Codifying an existing practice into published, sanction-backed rules is, of course, exactly what writing a specification is.

Greece also gives us the written build-spec and the acceptance test. The Arsenal of Philon inscription (IG II² 1668, 347/6 BC) is a marble stele carrying a complete building specification — the syngraphai — for the Piraeus naval arsenal: dimensions, materials, and construction detail prescribed in advance. The companion machinery — inspection of delivered materials, acceptance of finished work, penalties for nonconformance, all run by oath-bound overseers — is spelled out in temple-building contracts such as the one from Lebadeia. Together — a written spec from 347/6 BC, the acceptance machinery in a sibling contract from roughly a century later — they show contract-based design with acceptance testing, on stone.

And there is a tunnel. On Samos, around 550 BC, the engineer Eupalinos drove a kilometre-long aqueduct tunnel from both ends of the mountain at once, to meet in the middle — a feat Herodotus thought worth recording (Histories 3.60). What makes it a verification story rather than a lucky guess is the physical evidence Hermann Kienast documented on the walls: a system of red-painted, alphabetically-lettered measuring marks laid down as a reference grid, and geometric evidence that the diggers detected a drift in one heading and corrected it. The two headings met with a horizontal offset of about 60 cm over a kilometre — and a vertical error of a few centimetres.

Here the evidence is thinner than the story wants: the wall marks are the reference grid, and the course-correction is inferred from the tunnel's geometry, not read directly off the marks; and whether the famous zig-zag near the junction was a planned catching manoeuvre or a corrected mistake is genuinely disputed. Either way, it is measurement against a planned line — verification of a work-in-progress against a geometric specification.

Rome's contribution is the verification certificate as a physical object. A tessera nummularia is a small bone or ivory tag that a professional coin-tester — a nummularius — attached to a sealed bag of coins he had checked. It carries his name, his master's name, the verb spectavit ("has inspected"), and a date. One in the Kunsthistorisches Museum in Vienna reads Hilario Caecili sp(ectavit) — Hilario, slave of Caecilius, inspected — followed by the day and consular year: 30 October, 26 BC. Over a thousand survive; more than 160 carry consular dates. Of these survive, all datable between 96 BC and AD 88. It is a signed, timestamped attestation that a specific artifact passed a specific check by a specific, named verifier — a build attestation in bone, two thousand years old. (The one thing the tags do not preserve is the exact test the nummularius ran; that is scholarly reconstruction.)

And in AD 97 the emperor Nerva handed Sextus Julius Frontinus the curatorship of Rome's water supply, and Frontinus did something that would look startlingly modern to any auditor today: he refused to trust the books. His De aquaeductu records the audit. The official records credited the system with 12,755 quinariae of water; downstream, the same records accounted for 14,018 being delivered — a discrepancy of 1,263 he flags and investigates. Rather than reconcile paper against paper, he sent gaugers to measure each aqueduct as close to its source as the works allowed, and found reality exceeding the ledger substantially (De aq. 64–73). Per aqueduct he ran a three-point cross-check — recorded versus gauged versus delivered — and then classified the failures: arithmetic blunders in the original records; water-men fraudulently using a smaller gauge at the reservoir than at the intake; landowners tapping the conduits illegally. Every legal water grant, moreover, ran through a stamped bronze nozzle — the calix — of certified bore, and he physically found oversized ones installed.

Ledger versus measurement, quantified discrepancy, classified root causes, hardware checked against its certificate. The one thing hydraulic historians flag is that the quinaria measured cross-sectional area, not flow, so his unit is not hydrodynamically sound. Frontinus ran the audit right; he just measured in the wrong unit. There is a lesson in that pairing too.

The subtlest ancient verification is the one that guards a text against its own copyists. The scribes who transmitted the Hebrew Bible were called soferim — literally "counters" — and the Talmud (Kiddushin 30a) explains why: they counted the letters, words, and verses of the Torah, and marked its exact midpoints (the middle letter is fixed as the vav of gaḥon in Leviticus 11:42). Those counts became a marginal apparatus, the Masorah, carried in the great codices (the Aleppo Codex, ~925 AD; the Leningrad Codex, 1008 AD) — a running redundancy over the consonantal text. To check a new scroll you recounted it against the reference totals; a dropped or added letter shifts a count and betrays itself. It is a checksum maintained for a millennium. The caveat matters: the Talmud's own midpoint values no longer match the received text, and it concedes that the expertise to run the check had been lost — an ancient verification system recording that its own procedure had become unrunnable.

Which brings the arc, fittingly, to a check that is provably unsound. Casting out nines — verify an arithmetic result by comparing digit-sums modulo nine — is the conceptual ancestor of the checksum every network packet carries. Its earliest attestation as a verification method is surprisingly late (an Indian text of about 950 AD; the Persian polymath Ibn Sina gave full details around 1020, calling it "the Hindu method"), even though the underlying digit-sum was known to Greco-Roman writers centuries earlier without being used to check anything. And it is unsound: because it only sees the residue mod nine, it silently accepts any error that is a multiple of nine — it would pass 44, 53, or 26 as the product of 5 and 7 (53 being the one a tired scribe actually produces: 35 with its digits transposed). Unsound as a verifier, though perfectly sound as a refuter: when the check fails the answer is definitely wrong; when it passes, nothing follows. The ancients had not only checks but checks we can now show to be unsound, though nothing in the record suggests Aryabhata or Ibn Sina ever flagged the mod-nine blind spot. The Masoretes are the stronger case: they watched their own check become unrunnable, and said so.