The logical framework and data plane

For the category-theory reader, most likely arriving from Coln. Eight stops. maitria is independent work by the maitria coalition; the kinship described below is intellectual, and nothing here carries an ARIA endorsement.

1.Lineage, stated plainly

geolog-zeta is the public ancestor, a prototype of roughly 36,000 lines (github.com/davidad/geolog-zeta), now dormant. Its postmortem was inverted into the engineering covenants of what came after. The engine of record today is geolog-alpha, which keeps zeta’s lessons and replaces its semantic core; the historical toolkit snapshot knows it by its campaign-era working name, geolog-beta. (The letters are working names, not version order; arrival ran zeta, then beta, now alpha.) That repository is public.

Now the kinship. Coln is the Categorical Core implementation of ARIA’s Safeguarded AI programme, led by Martin Kleppmann and Owen Lynch, and it is a sibling of this line rather than a competitor to it. geolog-alpha is built to complement Coln and to converge with it at the wire format. On several axes the two arrived independently at the same answer, including content-addressed canonical identity and commit-DAG truth with tables as replayed views, which is worth more as evidence than either project’s say-so. The detail is written down and served: a design-delta survey of geolog-alpha and Coln, 13 pages, deltas in both directions at pinned revisions on both sides, with each divergence steelmanned before it is judged. Six of Coln’s choices come out as replicate-candidates; seven of geolog-alpha’s are held as advantages. Read it before deciding which of us is wrong about anything.

2.Theories, instances, and the chase

Doctrine first. geolog is a logical framework, not an expressive logic. It is a relational substrate adequate to host a theory of the proof trees of an expressive logic, with the model theory of geometric theories underneath. (geolog names the framework; geolog-alpha is the engine that implements it.)

The cycle has three steps. Declare a theory, giving sorts, functions, relations, and geometric axioms. Populate an instance with facts. Run the chase, which completes the instance to its free model, witnessing existentials, congruence-closing equalities, and materializing derived facts to fixpoint. Tables are not authored; they are entailed.

A small example fixes the picture. Take sorts V and E with source and target functions from E to V, and one axiom saying that whenever the target of one edge equals the source of another there exists an edge from the first’s source to the second’s target. Assert three vertices and two composable edges. The chase produces the composite as a derived row, with the equalities its existence forces already closed, and merging that instance with another replica is set union on commits followed by re-derivation. Nothing structural can conflict.

Elaboration errors carry counterexamples rather than line numbers, and reference semantics in the Datalog and egglog family give the engine something independent to be differentially tested against. The Geolog part of the book is the working account: Quick Start, Tutorial, and Reference Manual are full drafts in the served PDF.

3.GeologMeta, the homoiconic meta-schema

One schema is fixed by the system. GeologMeta is the theory of theories, and it is itself a geolog theory. Everything else, the certificate vocabulary included, is delta rows against GeologMeta carried on signed, content-addressed revisions, so a schema migration is data like anything else.

Two consequences matter. Every declared object gets a canonical content-addressed identity, the declaring revision’s hash together with a counter. And type checking becomes a validity judgment over meta-rows, uniform across user theories, with no privileged path for the system’s own schema.

Before the first production byte, the design went through repeated external adversarial review and an encodability audit over an entire pre-existing schema corpus. Gaps became typed extensions rather than exceptions (campaign ledger, day 3).

4.Ground formats

Two tiers, for a reason worth stating. Some carriers should never change, and some must.

The primordial tier is fixed forever: exact rationals, integers, naturals, booleans, together with strings over Unicode. It also includes the Lawvere rationals, the nonnegative rationals with a point at infinity, the carrier for enrichment over the interval from zero to infinity, whose quantale operations appear as ordinary ground functions rather than as a special case in the engine.

The extensible tier exists because new numeric formats keep arriving; the first extension covers IEEE floats beside FP8 and NVFP4-class block formats. A new ground type enters as declared rows, and any dispatching code must hold a certificate relationship to the declaration that added it. Implementations pin to a definitional wasm reference, and an accelerated path is admissible only when cotested against that reference, same inputs through both, outputs compared, with a signed witness. Floats are finite only: NaN and the infinities are rejected at ingress and negative zero is normalized there.

5.Tensors, two primitives and no more

A tensor over a finite family of finite index sets is a finite function from their product into a semiring. Tensor product is a lazy index-arithmetic view that allocates nothing. Contraction is taken along a map of finite index sets, summing over the indices the map does not hit. Einsum and broadcasting are corollaries rather than primitives.

The load-bearing side condition is that every un-hit index must be an output. That makes the one value-relevant free choice, a silent cardinality scaling, unrepresentable rather than merely discouraged.

The condition is younger than the definition it repairs, and the emendation history is preserved (ledger, day 3). Adversarial review caught an ill-typed index family in the definition’s 2025Q4 ancestor. An interim repair over-restricted the form. A probe asking which choices can affect values selected the version now in use.

Compilation follows the same discipline. Einsum lowers to contraction rows, with the index map and the output set carried as data, and never to eager sum-of-products expansion. The tensor former is primordial, which is where the block-sparse codec binds, and per-block precision is typed rather than smuggled.

6.The certificate vocabulary as hosted theories

The calculus of path A lives inside the framework rather than beside it. The vocabulary is two geolog theories: the Bernstein-Logic core, and the full QTSL vocabulary above it. Proof trees, sequents, and cell complexes are declared objects in those theories, and certificates are carried on the same signed revisions, the same store, and the same sync as everything else. Fixtures, goldens, and a mutant battery sit beside the theories, in the public qtsl repository. Certificate fixtures for the published experiments are already public and byte-committed in qtsl-experiments.

One property of that arrangement is pleasant enough to point at. The Bernstein-Logic theory’s file boundary is the certified checker’s fragment boundary, so the scope of the machine-checked soundness theorem is something you can see by looking at where a file ends rather than by reading a paragraph about it. The certified checker’s landed theorem covers that fragment today; certified arms for the System-and-Spec rule family are the assembly that remains.

The geometric-form normalizer, with a linter that has teeth, went green at three hash-stability strengths and was differentially tested against an independent reference (ledger, day 4).

7.The Semantic Universe

For this audience, the chapter to read first is The Semantic Universe. The compositional semantics is assembled by a double Grothendieck construction over a wiring base. Open hypernets include into it as a single machine-checked lax double functor, with strictness on the identity-carrying locus proved as a theorem rather than assumed at the outset. Say lax, and mean it; the strictness that holds is local and earned.

Above that sit machine-checked adequacy statements connecting the model-type catalogue’s formers to the Semantic Universe’s own semantics. The catalogue covers ordinary, partial, delay, stochastic, and random differential equations, jump-diffusions, Markov chains in both time styles, Markov decision processes, Markov automata, and bags of interchangeable units. Several of the stochastic formers are connected to a martingale-problem floor, with the remaining gap named in the module instead of papered over. The companion chapters are Hypernets: Primitive Functions, Hypernets: Markov Kernels, Systems: Mathematical Models, and Systems: Composition Patterns, all in the served book.

The systems vocabulary here is built on public work by others, gratefully and by name: the double operadic theory of systems of David Jaz Myers, and of Sophie Libkind and David Jaz Myers; and compositional Lyapunov certificates via assume-guarantee reasoning, from Matteo Capucci and David Jaz Myers.

8.S-complexes, and the frontier

S-complexes have moved from stated direction to shipped substance. Diagrams as Data: S-Complexes is a chapter of the book’s Geolog part, and the genus lives in the geolog standard library as an ordinary theory. There is no subtraction in a geometric theory, so boundary-of-boundary-is-zero is carried subtraction-free, as contraction rows.

Above the relational core, three directions have design notes and no shipped code, and they are named as invitations rather than promises. e-complexes, meaning higher-dimensional quantitative Datalog with a GPU-friendly evaluation story. Directed higher inductive types with computation by rewriting. Higher Petri nets and event structures for processes and provenance.

One road not yet taken deserves naming for this audience: proofs as cell complexes, with certificates as 2-complexes whose boundaries are the circuits being equated, replacing proof trees at the base layer. Genuinely attractive, genuinely unbuilt, and awaiting a champion.

Continue to: the certificate calculus · replication & authority · programme orientation.