What TA1.2 promised, and what was built
The campaign’s thesis was “TA1.2, finished,” so the rubric is TA1.2’s own stated objectives — an external rubric, not a curve this site drew. The table below assesses each objective against the landed state of the public repositories and served artefacts as of 4 August 2026.
TA1.2’s overarching objectives, from the programme’s solicitation materials: a “professional-grade computational implementation of the mathematical modelling language, according to the requirements developed in TA1.1 (incl. version controlling, type checking, proof checking, security-by-design, accommodating human-AI collaborations)”, and “an interface with AI agents to verify probabilistic claims about specific checkpoints of domain-specific neural network controllers and produce counterexamples or informative error messages.” The programme thesis adds the backend charter — a “distributed version control system for knowledge”, counterexamples on failed verification — and a stretch goal: verified compilation.
The objective map
| TA1.2 objective | Discharged by | Status on 4 August 2026 |
|---|---|---|
| A1 — implementation of the modelling language | geolog: theories, instances, and the chase; the homoiconic meta-schema (GeologMeta); ground formats; tensors | shipped the engine is public (geolog-alpha): chase fixpoint, meta-schema self-hosting — theories and certificates ride as ordinary rows — the exact-rational ground floor, and signed golden theories minted in-tree by a public ceremony; the QTSL theory pair itself ships in the public qtsl repository |
| A2 — version controlling; “distributed version control system for knowledge” | content-addressed, signed commit blocklace; durable store; geolog-sync | shipped the signed content-addressed store and the merge-free sync engine are in the public engine repository, and the toolkit’s own certificate theories ride them in earnest: sealed containers pinned by revision identifiers, carried and re-verified byte-identically across the toolkit’s repositories |
| A3 — type checking | GeologMeta validity judgments; elaboration; certificate-bound dispatch for extensible ground types | shipped rides the A1 surface in the public engine: per-commit validity judgments, the geometric-form linter, and the ground-vocabulary binder — unbound atoms refuse at compile |
| A4 — proof checking | Bernstein Logic — QTSL’s polynomial-certificate core — with certificates as rows in a signed geolog commit; the Lean rule-lemma development; the HOL4 checker theorem | shipped the Lean soundness development closes sorry-free at standard axioms, and the HOL4 side now carries a composed checker-soundness theorem binding an ACCEPT on the sealed commit bytes to the semantic validity judgment for the Bernstein-Logic fragment; real certificates checked end-to-end, at benchmark scale |
| A5 — security-by-design | signed envelopes; trust-basis semantics; the capability algebra (Keyhive-shaped) | in flight envelopes, trust semantics, and a first working capability tier are in the public engine; the full capability algebra remains design-stage, shown as such with its adversarial review record |
| A6 — accommodating human-AI collaborations | the agent session daemon; the proof-production cookbook; this site’s own agent legibility (/llms.txt) | partial the cookbook ships in the public modelling-toolkit repository, and the session daemon ships beside it — a stateful obligation workspace whose strategy layer may be any agent, with typed moves, verdicts from exact arithmetic only, and an append-only replayable event log; the site’s markdown mirror is live. Partial because these are first tiers — the fuller collaboration surface the objective names is human–AI dialogue working the same System workspace and the same Spec workspace, before synthesis and certification even begin, and that surface is still building |
| B1 — verify probabilistic claims about NN-controller checkpoints | QTSL → verification-condition towers → Bernstein Logic; neural supermartingale certificates; the certificate families of the reproduction spine | shipped the four campaign certificates stand (cartpole decrease & rate, double-pendulum small-gain & syzygy), plus a published 17-row neural-supermartingale benchmark swept in full — 28,569 certificates, re-verified under two checker generations with zero refusals. Certificate families now span circuits, Petri nets, stochastic PDEs, recorded control policies, and discrete probabilistic programs — the last compared like-for-like against the two published guaranteed-bounds tools (GuBPI, PLDI 2022; Diabolo, POPL 2025) on their shared benchmark programs, with per-case rows and receipts public and cases where a baseline wins an axis reported as rows; the newest certificate species there is staged for its theory-revision event, and its rows say so |
| B2 — counterexamples or informative error messages | counterexample-bearing elaboration errors; refusal semantics that track true boundaries; kernel-checked countermodels | shipped a staged rule was refuted by a kernel-checked countermodel; checker refusals are localized — naming the cell, the coefficient, and the exact value that failed — and the cartpole producer’s refusals locate the controller’s real decrease boundary |
| S1 (stretch) — verified compilation | machine-code checker routes: the HOL4/CakeML development with a machine-code soundness theorem, re-proven at each emission; CompCert route for the Lean-emitted core | partial the checker’s machine-code chain — HOL4 through the CakeML verified compiler down to Arm semantics — is green and kernel-checked, and the certified lane reads the data plane’s own commit bytes with its composed soundness theorem covering the Bernstein-Logic fragment. Partial because the full System-satisfies-Spec binding is not yet composed: it arrives with the wire’s system and spec tags — demonstrated route, assembling now |
In this table, “shipped” means the artefact exists in a public repository or served artefact and its stated check has run; “partial” means real artefacts ship and their stated checks run, but the objective’s full scope is not yet discharged — the remainder is named in the row; “in flight” names designed work still building, stated as design. Statuses re-assessed 4 August 2026 against the landed state; the dated build record, day by day, is the campaign ledger. The book is the authoritative deep account.
The TA1.1 scoreboard · status on 4 August 2026
TA1.2 builds “according to the requirements developed in TA1.1”, and TA1.1’s headline requirement is a list: Appendix A.1 of the programme thesis names the modelling frames the mathematical modelling language is meant to unify — differential equations in five flavours, Markov processes, hybrid systems, Petri nets, and the probabilistic-model family. The scoreboard below grades the toolkit’s language against that list, frame by frame. The vocabulary the grades cite is the book’s model-type catalogue, whose organizing rule is that a model type is a profile, not a tag: nothing in the theory stores “this is an SDE” — the type is which field families are populated, which is what lets one composite mix frames freely.
A frame is subsumed when four legs are witnessed, each by landed, checkable artefacts:
- representation — the frame’s models are declarable as data of the language, in a form a native reader of that frame recognizes as their model, preserving the frame’s own compositional grain;
- semantics — the frame’s standard semantics is recovered exactly, or at a named rung with the bridging analysis staged as named obligations, never silent assumptions;
- certification — at least one of the frame’s own bread-and-butter verification questions (reachability for chains, dissipation for PDEs, coverability for nets, posterior bounds for Bayesian networks, …) compiles to certificates checked by the unmodified kernel, with a landed exact-rational example;
- compositional closure — the frame’s systems compose with systems of other frames through each of the three wiring modes (variable-sharing, parameter-setting, mode-switching) and nesting, each mode witnessed by a checked heterogeneous composite carrying a transported certificate.
Partial means at least one leg is landed as artefact and the missing legs are named; absent means no landed leg (adjacent design noted where it exists). Design prose, however deep, never lifts a frame out of absent — that line is what keeps the grades checkable.
| Frame (thesis Appendix A.1) | Grade | Standing |
|---|---|---|
| ODEs | subsumed | controller certificates (cartpole; the ACAS-Xu benchmark ladder) and a validated-enclosure certificate family; mechanism rows load end-to-end through the engine; all three wiring modes and nesting witnessed by heterogeneous composites |
| PDEs (deterministic) | partial | exact-rational dissipation certificates at the sharp rate (Burgers, Fisher–KPP, Kuramoto–Sivashinsky), with the solution-concept bridges substantially discharged in Lean; the jet-level mechanism rows and PDE participation in composition remain |
| SDEs | subsumed | generator certificates from the 1-D Ornstein–Uhlenbeck pair through full-rank correlated-noise encounter models, state-dependent noise and jump rates included; the extended-generator rung in Lean; closure complete |
| SPDEs | partial | five exact-rational stochastic certificates (stochastic Burgers, stochastic heat, stochastic Kuramoto–Sivashinsky absorbing balls) and the stochastic solution-rung classes in Lean; noise spectra ride as rows at mode level — the jet-level grain and composition remain |
| random ODEs (RODEs) | subsumed | a parameter-boxed barrier certificate uniform over the box, the parameter carried as a region axis of every checked cell; per-parameter semantics machine-checked; closure complete; the random-PDE extension rides the PDE lane |
| jump-diffusion | subsumed | all three field families — drift, diffusion, multi-leg jump kernels — certified in one generator, each jump leg shown necessary by exact refusal witnesses; the jump-kernel rung in Lean; closure complete |
| discrete-time Markov chains (DTMCs) | subsumed | a published 17-row neural-supermartingale benchmark reproduced or refuted row by row in exact arithmetic; the discrete Dynkin inequality proven outright in Lean, no staged obligations left open; closure complete |
| continuous-time Markov chains (CTMCs) | subsumed | rate matrices as rows — pure tables beyond any mass-action law included — with certified time-bounded reachability; the generator rung in Lean; closure complete |
| Markov decision processes (MDPs) | subsumed | certificates uniform over every adapted randomized policy, the quantifier’s price stated exactly; the one-step rung in Lean, no staged obligations left open; closure complete |
| Markov automata | subsumed | closure under a declared scheduler proven in Lean — the closed object is an ordinary CTMC citizen — with bounds uniform over the adapted scheduler class; closure complete |
| open games | absent | a research road, named |
| mean-field games | absent | structurally hard; the road runs through the PDE row |
| GSHS (generalized stochastic hybrid systems) | subsumed | guards, resets, diffusion, and jumps certified together; the guard-kind seam proven as theorems; parallel products of guarded systems proven at the profile level; closure complete |
| SDCPN (stochastically and dynamically coloured Petri nets — an earlier candidate unifying language, graded here as a frame in its own right) | partial | a narrowing shelf: the population (bag) former, the whole uncoloured adequacy square, and the coloured core — coloured formation with cascade adequacy, the demonic scheduler module, the composed corollary, and its directed transfer faces — are landed and machine-checked, with mutant batteries, at the Dirac-reset grain; the delay faces are now certified at the general-reset grain as well — firing kernels in place of point resets, sub-stochastic over markings in the uncoloured case and mass-one over produced colours in the coloured case, with the Dirac case recovered as a degenerate corner by theorem and the earlier delay squares re-derived from the kernel ones; the cascade and immediate faces now join them — produced-colour firing kernels, marking-aware by mechanized necessity (a jamming argument shows a marking-independent kernel cannot express any genuinely mixing certified net), with the earlier Dirac-grain cascade square re-derived through structural ties alone; the net-to-hybrid equivalence obligations remain enumerated as design |
| Petri nets | subsumed | the token game runs natively as chase derivation; first checker-verified quantitative bounds for stochastic nets, in decay and avoidance forms; closure complete |
| Bayesian networks | partial | exact posterior certificates in the finite corner; the semantics leg is machine-checked — the network’s judgment in the mechanized semantic universe is proven, and recovered from the dependency-graph scoring face at every structure weight in the regime (positive conditional tables); closure complete; the continuous, score-carrying case remains |
| structural causal models | subsumed | counterfactual certificates in both truth directions; twin-network substitution proven outright in Lean, no staged obligations left open; counterfactual-given-evidence certified beyond enumeration; closure complete |
| Markov random fields | partial | exact partition-function brackets (trial-restriction lower, tree-reweighted upper) with checker and mutant battery; the Gibbs semantics is now machine-checked — the exact-rational Gibbs law of a field of positive potentials pinned in the mechanized semantic universe, with the log-partition identity proven; native rows and the continuous case remain |
| probabilistic dependency graphs (added row, like SDCPN: the published scoring-semantics frame through which the toolkit renders this family — networks and random fields arise as its corners) | partial | exact-rational two-sided inconsistency brackets with an independent checker and mutant battery; the scoring semantics machine-checked in Lean — the Donsker–Varadhan and free-energy inequalities the brackets rest on, the Gibbs-corner identity, and uniqueness in the convex regime — and the adequacy square ties the scoring face to the mechanized semantic universe, with the network judgment recovered at every structure weight in the regime and the exact-rational Gibbs law pinned at the random-field corner; native rows, a transported certificate in the frame’s own right, and the continuous case remain |
| probabilistic programs | partial | certified posterior brackets at infinite horizon for score-carrying programs, compared like-for-like against the two published guaranteed-bounds tools; continuous latents remain; the thesis’s autoregressive-LLM clause is a programme-scale question, out of scope here by design |
| probabilistic logic programs | absent | the semiring-chase machinery sits adjacent; the wiring remains |
| score-based generative models (diffusion models) | absent | a composite of the SDE row and the piecewise-polynomial route, sequenced behind it |
Headline: 11 subsumed · 7 partial · 4 absent across the 22 graded rows (the thesis’s stochastic item splits into SDE and SPDE rows, its probabilistic-graphical-model item into the three named classes, and the SDCPN and probabilistic-dependency-graph rows are added). Grades are conservative by rule — each subsumed grade cites specific landed artefacts for all four legs — and the expected reading is a campaign map, not a victory lap: the absent rows are stated as absent.
The adequacy-square roster
One rung below the frame grades, the book’s semantics-first spine tracks, for every System-former, an adequacy square: the machine-checked theorem tying the former’s own textbook semantics to the mechanized semantic universe — the model-type analogue of a soundness lemma. The roster, as of 4 August 2026, against the toolkit’s Lean development (documented in the book; the development ships in the qtsl repository). “Proven” means the square, or its stated floor, is machine-checked; “partial” means a rung or one face is machine-checked and the rest is named; “owed” means the statement stands as design, stated as such.
| System-former | Adequacy square |
|---|---|
| ODE | proven |
| PDE | proven at former level, over the jet-grain mechanism — with the honesty point stated in the book: no canonical weak form exists at former generality, so solution-concept rungs ride as data |
| delay equations (DDE) | proven, two-sided |
| SDE | proven at the martingale-problem floor — the literature’s own definition for the compiled polynomial class |
| SPDE | partial the stochastic solution-rung classes are proven; the square’s left edge — the literature’s own solution concept — remains |
| random ODE | proven |
| jump-diffusion | proven at the martingale-problem floor, at full generality (multi-leg kernels, killing, sub-stochastic resets) |
| GSHS | proven at the martingale-problem floor |
| DTMC | proven |
| CTMC | proven, via the jump-chain square |
| MDP | proven, both faces — fixed-policy and demonic |
| Markov automata | proven, both faces — fixed-scheduler and demonic |
| bag (population former) | proven — transport core and judgment wiring |
| stochastic Petri / SDCPN | partial the uncoloured square is whole and the coloured square is proven at the Dirac-reset grain (delay and cascade faces, demonic scheduler, composed corollary, directed transfer faces); the delay faces are proven at the general-reset grain — firing kernels in place of point resets, both colourings, the Dirac case a degenerate corner by theorem — and the cascade and immediate faces now proven at that grain too, produced-colour kernels marking-aware by a mechanized jamming argument, the Dirac square recovered through structural ties; the net-to-hybrid comparisons remain |
| Petri nets | partial the witness battery exists; the square statement tying chase saturation to the standard token game remains |
| probabilistic graphical models | proven — the Bayesian-network face; the Markov-random-field face, with the exact-rational Gibbs law of a field of positive potentials pinned and the log-partition identity proven; and the dependency-graph scoring square, which recovers the network judgment (positive conditional tables) from the scoring face at every structure weight in the regime |
| SCM | partial the twin-network rung is proven outright, no staged obligations left open; the full counterfactual square remains |
| probabilistic programs | owed the probabilistic-kernel semantics is proven one tier down (Kleisli functoriality of the noise-port construction); the former-level square remains |
| probabilistic logic programs | owed deliberately sequenced last |
| clocked boolean circuits | owed exact replay is the semantics (the checker is the model); whether that identity deserves a separate theorem is an open adjudication, stated as open |
Roster count: 13 proven · 4 partial · 3 owed across the twenty formers rostered.
The components · inventory, 4 August 2026
Artefact availability is badged honestly: public a public link exists · paper a PDF is served on this site · described the artefact and its check are stated precisely, and the page upgrades in place when a repository or paper becomes available.
Bernstein Logic checked paper
The polynomial-certificate core of QTSL — its workhorse fragment: all polynomial reasoning in one rule (exact-rational Bernstein coefficient sweeps against conic predicates — no SDP, no floats), a literate rule catalogue with per-rule soundness status, a Lean soundness development that closes sorry-free at standard axioms, and a composed HOL4 theorem binding checker acceptance to the semantic judgment for this fragment.
QTSL public paper
A quantitative temporal specification logic compiling to Streett/tower verification conditions — the layer where probabilistic and temporal claims live before they compile away into exact arithmetic — public in the qtsl repository.
The book & technical reports paper
The book is the self-contained account of the whole stack, rebuilt from committed sources and republished continuously, with its complete LaTeX source embedded in the PDF and served beside it. Two technical reports are served: certifying stochastically and dynamically coloured Petri nets without a non-Zeno axiom, and a design-delta survey of geolog-alpha and Coln. Author lines and model credits are stated plainly on the colophon.
geolog public
A relational logical framework — not an expressive logic: a framework adequate to host a theory of proof trees of an expressive logic. Theories ride as delta rows against one fixed, homoiconic meta-schema (GeologMeta); the wire format’s whole job is signed deltas over that schema.
The modelling toolkit public
The producer side, untrusted by construction (mtk): a float proposing tier and an exact certifying tier, every accelerated kernel emitting witnesses, never bare verdicts — being wrong costs a rejected certificate, never a false verdict. Beside the producer tiers: the EventLoop component engine, and the agent session daemon — a stateful obligation workspace in which any strategy, a person or a language model, can only ever select among the moves the workspace offers, and verdicts come exclusively from exact arithmetic.
Capability algebra first tier public
Authorization as judgments computed by deterministic replay of signed operations riding ordinary revisions — the Keyhive move adopted at the operation-shape level: proof-carrying attenuable delegations, and revocation semantics held to theorem standard rather than policy — adversarial review sharpened the claim to per-revocation shielding: each effective revocation spares the additions in its signed past (path C, stop 3). A first working capability tier ships in the public engine; the full algebra remains design-stage, shown as such with its adversarial review record — including findings confirmed as bugs in upstream pinned code.
Sync & replication public
Ground-truth replication is merge-free by construction (grow-only commit set; merge = union) over per-device single-writer logs; the CRDT question survives only on a short enumerable list of mutable surfaces. The sync engine — implemented sans-io with its wire codec, hardened through two adversarial review rounds — ships in the public engine repository.
Assurance edifice checked
The machinery that makes “take our word for it” unnecessary: kernel replay plus a decorrelated second kernel, a three-path comparator, signed verification receipts over content-addressed stores with a trust-roots file, and machine-code checker routes (HOL4/CakeML with a machine-code soundness theorem, re-proven at each emission; CompCert for the Lean-emitted core). Decode totality is a theorem over arbitrary byte strings, and the composed HOL4 theorem binds acceptance on the data plane’s own commit bytes to the semantic judgment for the Bernstein-Logic fragment — demonstrated route, assembling now.
Proof-production cookbook public
An agent-facing corpus of proof-production meta-insight — Polya for minds that read .tex and .md natively — harvested from the campaign’s own proof work and genericized for reuse. Ships in the public modelling-toolkit repository.
Worked examples public
Benchmark certificates that teach the toolkit by existing, in the public reproduction spine: the one-dimensional ReLU worked example at full fidelity; the cartpole and double-pendulum controller certificates; and certificate families across circuits, Petri nets, stochastic PDEs, recorded control policies, and discrete probabilistic programs. Each is real bytes, checked by the real checker, with its refusals as informative as its acceptances — one make target per book section, mutant batteries beside positive controls.
Producer-side science notes
Research notes from the certificate-producing side, published with measured nulls intact — including the decomposition-beats-spectral-heroics verdict, established three independent ways. They model the receipts culture the rest of the site practices; the numbers land in the book’s experiments chapter and re-derive from the reproduction spine.
Boundary, stated once: this site is the toolkit itself. Applications of the toolkit to verifying specific external systems, and the coalition’s broader story, live elsewhere.