The campaign ledger

On 16 July 2026 the goal was stated plainly: finish Bernstein Logic, with an implementation checked against ARM semantics, by July 21 — ideally consuming geolog’s wire format, with the proofs of the cartpole and double-pendulum controllers stored in geolog. This ledger tells the week day by day, completely: what shipped, what refused, what remains.

Reading the ledger. Three statuses, no spin: shipped an artefact exists and its stated check has been run · in flight a named piece of work open on the day of writing · frontier a known-open problem, stated as an invitation. Entries never retro-edit; corrections append. Refusals and nulls are entries too — on this page a checker saying no for a true reason counts as a result, because it is one. Built by a coalition of ephemeral Claude Fable 5 and GPT-5.6 Sol instances in a shared high-context workspace, directed by David “davidad” Dalrymple, whose word is what an entry marked “decided” records — see how this was built.

Day 1 · Thursday 16 July complete

The goal, then immediately the requirements. Within hours of the goal statement, a written requirements spec existed: 23 requirements in three tiers, nine work packages with acceptance criteria, and the wire contract named as the first frozen interface — so the proof-calculus side and the data-plane side could run in parallel from day one instead of serializing.
The frame correction, same day. A mid-day design correction re-scoped that spec before it calcified: geolog is a logical framework — adequate to host a theory of Bernstein Logic proof trees — not an expressive logic to encode into; and its wire format’s whole job is delta rows against one fixed, homoiconic meta-schema. The requirements were rewritten the same afternoon, and a citable “what geolog is (and is not)” primer now travels with the spec so no future work package re-imports the wrong frame.
Coordinate projection entered the term grammar — with its future stated: the decision admitted the indexing constructor as the degenerate case of a two-primitive tensor calculus (lazy tensor product; contraction along a map of finite index sets), so that einsum arrives later as an extension, not a rework.
An honest mathematical surprise. The plan said “zero new mathematics” for multivariate certificates; that was wrong at exactly one joint. Above dimension one, the region machinery hands the kernel real barycentric weights while the kernel theorem eats rational ones — classical LP folklore (a rational system with a nonnegative real solution has a nonnegative rational one) that had to be proven in-tree, ~300 lines. With that bridge, the full-catalogue soundness theorem closed sorry-free at standard axioms, and the first Bernstein-cone verdict above dimension one was checked end to end.
Machine-code route, demonstrated on an existing artefact. To prove the route before building along it: an existing verified SAT-certificate checker (cake_lpr) built out of the box and checked fresh certificates; its in-logic compilation at pinned sources reproduced the shipped AArch64 assembly byte-for-byte; and by evening its full machine-code soundness theorem had been replayed from source at the pins (4h15m on a rented 32-core box, 49.2 GiB peak) — closing, for that artefact, the provenance gap between “a verified checker exists” and “these bytes are that checker.” This demonstrated the toolchain and the replay discipline; the campaign’s own checker did not yet exist.
Trusted-core diet. The checker core was split from its proof development: the emitted-C closure shrank from 3.58M lines to 34,311 (104×), zero external packages — and that core became the first Lean-emitted C through the CompCert verified compiler (9/9 translation units after a mechanical C11 normalization), with the resulting binary’s output byte-identical to the production build’s.
The first real certificate. The cartpole controller’s decrease certificate, end to end: exact-rational weight LPs per cell, a 197-node proof term, 19 KB of certificate bytes, reference-checker ACCEPT, parsed independently by the Rust reader. And a refusal worth as much as the acceptance: on the widened domain the cell-splitter refuses two sectors, and a direct scan confirms the controller’s decrease property genuinely fails there — the refusal tracks the true boundary of the law, not a weakness of the method.
Composition rules drafted (interface-promise, syzygy, small-gain) with their Lean soundness satellite — small-gain reduced to a verified two-line identity, so the checker never sees a fixpoint argument.
The tech report, day one. A 25-page self-contained draft of the whole stack, written and put through an adversarial review round the same day.

Day 2 · Friday 17 July complete

Critical path complete in ~30 hours. Overnight into morning, the data-plane work packages went green end to end: four real certificates — cartpole decrease and rate, double-pendulum small-gain and syzygy — through reader → compiler → signed commit → content-addressed cold store → replay → projection, with the projected bytes byte-identical to the producer’s originals, twice. A cross-language mutant battery (six mutation kinds minted on the Rust side) was rejected across the boundary, every one.
The stretch bar, met early: with the double-pendulum composites checked and stored, both target controllers’ certificates existed in the data plane by breakfast on day 2 — four days ahead of the deadline the bar was set against.
Tech report complete at 35 pages, two appendices (effective sparse Handelman; the defect bound), dual-engine compile clean.
The meta-schema review day. A live line-by-line design review produced a dozen decisions now carried as design record: low-precision float ground sorts (FP8, NVFP4-class) admitted; opcodes renamed asm-like; ground types made extensible with certificate-bound dispatch — “new numeric formats will keep on coming” — while Q/Z/N/B stay fixed as Platonic; GPU implementations admissible only when cotested against a wasm golden (the same inputs run through both implementations, outputs compared) with a signed cotesting witness; a tensor former; Lawvere rationals ([0,∞] with its quantale operations at extension tier); and a uniform multi-precision story across the numerics.
Storage and sync became real code. A durable blocklace store landed; the sync engine was implemented sans-io with its wire codec and hardened through two adversarial rounds the same afternoon. The first production bytes are deliberately held for a write ceremony — the campaign’s one true commitment point.
A first verified checker became a program. A HOL4/CakeML port of an early, partial checker — covering a fragment of the calculus, not the full catalogue — landed as a real binary: certificate bytes on stdin, verdict on stdout, kernel-checked, with that prototype’s machine-code soundness chain green. The full-catalogue certified checker this prefigures is the one still assembling.
An honest no. Asked directly whether that verified binary could check a real ACAS-Xu-scale certificate today, the answer was no — not yet, and the blocker is performance, not vocabulary. The response was a design steer adopted the same hour: checker inner loops as relational joins over flat column stores, never materialized pointer structures — and the performance seating began that evening.
Security-by-design moved. The capability algebra proposal was drafted (authorization as deterministic replay of signed, attenuable delegations riding ordinary revisions — built to converge with Keyhive), and blake3-subtree authenticated range proofs were dispatched as a successor capability.
The programme corpus was indexed — thirteen programme decks and the thesis, concordance-style, deck claims mapped to built artefacts with divergences marked. That index is the spine of this site’s programme path.

Day 3 · Saturday 18 July complete

The ported prototype’s debts were paid. All four named proof cheats in the HOL4 port were discharged — 17/17 receipts green — so the prototype’s machine-code chain rests on no IOUs. (Scope honestly stated: this is the partial checker of day 2; the full-catalogue machine-code story remains the arc in flight.)
Floats: finite-only, decided and enacted. NaNs and infinities rejected at the boundary, negative zero normalized — “bit-exact” semantics with the degenerate cases legislated away rather than special-cased forever.
Theories and instances became first-class in the meta-schema, with the authorization consequences decided the same night: assertion capabilities are per-instance (a non-totally-ordered capability structure), admin exists at both theory and instance grain, and delegation defaults are conservative.
A slide-era bug, found and upgraded. Adversarial review of the aggregation-node brief caught an ill-typed index family in the 2025Q4 tensor-contraction definition; an interim repair over-restricted it (surjectivity the slide never asserted); the reopening probe — which choices can affect values? — selected the final side condition: every un-hit index must be an output, making the one value-relevant free choice unrepresentable rather than discouraged. The emendation history is preserved in the definition’s own record.
The catalogue grew admissible rules with proofs. Exact-constant-matrix reasoning generalized (PConstExact, subsuming rational factorization), a bound-bridging rule (PBound), and PSD certificate entries in three variants — each landing with kernel-clean soundness lemmas, twice-verified.
The pre-first-byte gate ran. Before any production bytes, an encodability audit checked an entire existing schema corpus — every walked column and type — for expressibility in the meta-schema, and a dataflow audit classified nineteen existing computations against the framework. Gaps found became typed extensions, not exceptions.
Zero-copy serialization decided for the envelope and store surfaces (rkyv-class, archived-access), with the signature domain separated and byte-costs checked before ratification.
An overnight fuzz campaign launched — three targets, twelve hours, four forks each, on a rented high-memory box — against the store’s open/crash/state-machine surfaces.
Sound-for-first-byte. By midnight the staged genesis reached the bar its name states: the blocking finding set was empty, the final adversarial round’s findings all folded with zero staged bytes moving afterward, and the genesis re-pinned, golden byte-verified.
A nomenclature knot dissolved. The recurring “where exactly does QTSL sit relative to Bernstein Logic” confusion was traced to a turnstile collision — ⊢ vs ⊨, now separate kinds of judgment within one enormous logic (renamed to QTSL).

Day 4 · Sunday 19 July complete

Geometric normalization landed. The normalizer that puts Bernstein Logic’s theory into geolog’s geometric form — with a linter with teeth — went green at three hash-stability strengths, differentially tested against an independent reference implementation.
The overnight fuzz campaign returns this morning; findings fold into the store the way everything else has: as fixtures.
This site went up on staging — the programme path, the toolkit map, this ledger, and the certificate-calculus path (stops 1–5) — as the campaign’s public face, buildable from the record with zero repository flips.
Appended at close — the fuzz campaign came back clean. All three targets ran to full term against the store’s open, crash, and state-machine surfaces — 424.7 million, 58.1 million, and 20.7 million executions respectively — with zero crashes, zero hangs, and zero out-of-memory events; 405 new coverage-expanding corpus entries were banked as fixtures. An honest null, recorded as one.
Closed 21 July, with the fuzz return appended above. Corrections to earlier days, if any, append rather than editing history.

Day 5 · Monday 20 July complete

Producer scale-up and the checker-ingestion gap: full-certificate ingestion on the verified-checker lane (the one named gap between “the reference checker accepts real bytes” and “the verified binary accepts the same bytes at scale”).
Assembly rehearsal for the end-to-end demonstration: certificate bytes out of the data plane, verdict out of the verified checker.
The two items above were the plan, written in advance; the entries below record the day itself, appended at its close. The ingestion arc they name continued into day 6.
The storage decision — certificates are born as rows. Decided: a certificate’s only durable form is ordinary rows in a signed, content-addressed geolog commit — no separate proof-file format, nothing to version — and the campaign-era binary bridge format was retired across the whole project the same day. The trichotomy now on the front page — one set of sealed commit bytes, three independent checking routes — was written down the same day as the architecture of record.
Re-verification at scale. The campaign’s accumulated certificate corpus — 28,569 certificates from the producer-side science sweeps — was re-verified end to end under both the sweep-era and current checkers: zero refusals, and no certified bound moved.

Day 6 · Tuesday 21 July complete

The programme catch-up — the campaign’s real external coupling — with the end-to-end demonstration as the thing on the table, and this site as the guided record of how it was built.
The certified lane now parses the data plane’s own bytes — at the logic level, inside its proof boundary: the sealed geolog commit-body format entered the verified reader by morning, with decode totality re-proven over the widened grammar, canonical encoding upgraded to a kernel theorem (the accept path executes a re-encode fixed-point gate), and a 21-case differential green against the independent Rust oracles — expected-accept rows byte-exact, eighteen hostile mutants refused in class. The machine-code tier of that arm is the assembling step.
The checkers’ read path completed its cutover to rows: certificate content is consumed from geolog row bodies; no code path reads or writes the retired bridge format.
Closed complete; this closure appended 2 August 2026, with nothing above it edited. The ingestion arc these entries carried ran on into day 7, and the machine-code tier named above as the assembling step is assembling still.

Day 7 · Wednesday 22 July complete

Finish-by target. The ledger closes as an artefact of record; the frontier list below stays the site’s forward edge.
The finish-by target was met in the sense in which it was stated. The ledger closed on 22 July 2026 as an artefact of record, with the toolkit’s core existing end to end, from producer through sealed geolog rows to checker verdict.
The frontier list below stayed the forward edge rather than becoming a list of regrets; the afterword records which of its items have since moved. Appended 2 August 2026.

The frontier

Known-open problems, stated as invitations — they are what keeps this site warm after the ledger closes:

frontier ACAS-Xu-scale checking on the verified binary: the relational-join checker core, taken from design steer to measured throughput.
frontier The assurance edifice as a freestanding distribution: extracting the checker gate, receipts, and comparator into a package with no references to its home infrastructure.
frontier Proofs as cell complexes: the 2-complex alternative to proof trees at the base layer — the road not (yet) taken, awaiting a champion.
frontier The completeness boundary: a meta-theorem for the certificate fragment’s expressive boundary, to make today’s truth-tracking refusals into tomorrow’s characterized ones.

Afterword — 2 August 2026

The ledger above closed on 22 July 2026 and is preserved unedited; corrections to it append, as they always did. Work has continued daily since, in the same open-record style, and the record now accumulates in the book and in the repositories rather than on this page. The book has grown into a preview scaffold of roughly a thousand pages, served at /book.pdf and rebuilt from committed sources at every build, and a mechanized descent now connects the chapters’ patterns to the Semantic Universe’s own semantics: open hypernets include as a single machine-checked lax double functor, the model-type catalogue’s formers carry machine-checked adequacy statements, the Specification Language is presented as deduction rules over a formation judgment, and eighteen rewrite rules are mechanized statement for statement in Lean and in HOL4, with the four wrong-polarity siblings refuted by machine-checked countermodels. The certificate vocabulary itself is now baked as two geolog theories, the Bernstein-Logic core and the full QTSL vocabulary above it, with fixtures, goldens, and a mutant battery beside them. Two technical reports are served on this site, one on certifying stochastically and dynamically coloured Petri nets without a non-Zeno axiom and one on the design deltas between geolog-alpha and Coln. The semiconductor ladder is underway with its first rung certified, carrying linear-Lyapunov drain certificates for the Mini-Fab fluid model under named static-priority dispatch, residual scheduling freedom resolved adversarially, at release rates up to 95.9 of its 96 lots/week fluid capacity, with the probe at 96 correctly failing. Three of the six repositories are public (kernels, mtk, qtsl-experiments), and the rest are arriving. Two items on the frontier list moved: machine-scale checking on the certified binary went from a design steer to a measured replay of the stored corpus, 4,105 verification conditions accepted with no divergence from the fast-path twin at a pooled median of 30 ms per file on one Arm core, and the completeness boundary gained a first characterized fragment, written up in the book’s Partial Completeness chapter. This page stays as history; the current account is the book, and the current receipts are in the repositories.

Correction, appended 4 August 2026: the repository count above has moved — five of the six repositories are now public, with geolog-alpha and qtsl joining kernels, mtk, and qtsl-experiments; the sixth is this site’s own repository. The paragraph above stays as written on 2 August.