1 Introduction↩︎

To answer a question about a program, move the program to where the question is decidable. A C program’s reachability question becomes a bit-vector model-checking problem; a Python function’s assertion becomes a linear-arithmetic query; a chemical reaction network’s coverability question becomes an SMT unrolling. Every such move is a translation, and every translation is a place to be wrong. The classical responses are to prove the translator once and for all [1], [2], or to validate each of its runs [3]–[5]. Both are statements about a single edge.

This paper is about the graph. In practice the representations worth reasoning in form a web: several source languages, a few solver-facing targets, more than one way to get from here to there — and, crucially, edges of honestly different trustworthiness. A translator generated rule-for-rule from a logic-to-logic mapping is foreseeable from its specification. An optimizing C compiler is not foreseeable and not proved, only pinned. A translator written from an ISA manual and one derived from the same ISA’s formal model are neither proved — but they were produced independently, and that independence is itself a resource. A theory of the graph must let each edge say what it actually guarantees, compose those statements honestly, and show how several weak edges can corroborate one another into a strong route. Its stance is the one distributed systems take toward processes: a translator is a component that fails, and the failure is to be contained — by declared loss, decidable checks, and independent routes — rather than prevented by universal proof.

1.0.0.1 An experiment in LLM-generated correctness, in both directions

This work is, deliberately, as much an experiment about who can build and use such a system as about the system itself. hurdy-gurdy— the platform this paper defines, builds, and measures — exists to show two things at once. First, that LLMs can be utilized to produce correct code: every pair — translator, carry-back, tests — was implemented by an independent LLM agent from a one-page brief, largely unsupervised, with the architecture’s cross-checks as the only semantic gate; the platform is the experiment’s artifact, and §6.6 reports what the gate caught. Second, that LLMs can be supported in producing correct conclusions: the platform’s intended player is an LLM, which chooses questions and routes but can take no unchecked step — routes of pairs hand the untrusted reasoner deterministic moves whose trust is graded, cross-checked, and, for witness-carrying answers, self-certifying at the source. This paper evaluates the first direction throughout, and reports a first, deliberately small controlled experiment on the second (§6.8): LLM players answering ground-truthed questions through the platform, every verdict carrying a machine-checked evidence artifact where the unaided baseline offers its say-so. Building the instrument and playing it are the same thesis at two scales: trust comes from the architecture, not from the author.

1.0.0.2 Provenance disclaimer

All of hurdy-gurdy— framework, shared interpreters, pairs, solver plumbing, the evaluation harness, and the Lean mechanization — is LLM-generated code (Claude Opus and Claude Fable agents), produced largely unsupervised under the discipline this paper describes; no human reviewed the code for semantic correctness. Most of this paper’s text was likewise LLM-generated. The human contribution is the architecture: the calculus, the contracts the agents were held to, and the decisions about what to build and what to claim. Every quantitative claim in 6 is regenerated from the artifact by one script, and the mechanization’s axiom audit is re-checked at every build — by design, the reader need not trust the writers, human or otherwise, any further than the paper’s own thesis requires.

1.0.0.3 This paper

We give the graph that theory, and measure an implementation of it. The unit is the pair (3): two formally defined languages, a pure translator, pure interpreters for both languages (owned by the languages and shared across all pairs touching them), and a pure target-to-source interpreter — the component, usually an afterthought, that carries a target-side behavior back to a source-side behavior. The four functions close a commuting square, and the square commuting at a given program is decidable: run both sides, compare under the pair’s declared projection. A failure localizes to a step and a named observable.

Squares compose. The pasting of commuting squares is folklore, and the hypothesis it needs when each square commutes only up to a projection — the earlier hop’s carry-back must not read target observables the later hop discards ([def:support,thm:pasting]) — is, as mathematics, a congruence condition whose cousins appear wherever simulations compose vertically across differing observations (7). What we claim for it is its role as an explicit design rule — declare your loss — with a syntactic keep/loss computation: a source observable survives a route iff no hop discards what it depends on.

On this base we build the fidelity story (4). Each edge declares a grade — \(\mathtt{predicted}\), \(\mathtt{reproducible}\), \(\mathtt{checked}\), \(\mathtt{proved}\), \(\mathtt{trusted}\) — naming its guarantee and evidence. Grades compose by weakest link, but on an assurance-class chain (universal / per-run / replay / none) that separates the logic of a guarantee from the kind of evidence behind it. Two further mechanisms move assurance where weakest-link says it cannot go: re-establishment (2) — inline square-checking lifts any single run over an opaque hop to per-run faithfulness, which is how a pinned-but-unproved compiler can head a verification route — and branch corroboration (2) — independently derived routes to the same target that agree on the same input corroborate each other beyond either’s declared grade, with disagreement localizing to one hop of one route (1). A trusted-base ledger (§4.4) itemizes exactly what each layer of checking removes from the set of components one must still believe.

The capstone (§4.6) is an asymmetry we believe deserves to be a design principle. Answers that carry witnesses — reachable, sat — are self-certifying at the source: carry the witness back through the route’s target-to-source interpreters and replay it in the source interpreter; soundness then rests on interpreter adequacy alone, with every translator and solver demoted to a discovery heuristic (3). Universal answers — unreachable, unsat — admit no witness, and are precisely where fidelity grades, branch agreement, and independently checked certificates are the only currencies (4). A translation architecture should therefore make witness carry-back a first-class component of every edge — cashing in the free half of trust — and spend its proof effort exclusively on the other half.

1.0.0.4 Coverage, and honesty about partiality

Fidelity is gameable by triviality (a one-instruction pair is vacuously \(\mathtt{proved}\)); coverage is gameable by unsoundness. We require their per-construct conjunction against spec-enumerated inventories (8), with all rejection typed and enumerable, and we prove the widening discipline sound: additive extensions preserve all prior verdicts ([prop:ratchet]), so coverage ratchets monotonically over a project’s history.

1.0.0.5 The instantiation

The calculus is implemented as hurdy-gurdy, a platform of 13 registered languages and 13 pairs (5): C, RISC-V, AArch64, Wasm, eBPF, EVM, Python, Sail, chemical reaction networks, SMILES molecular graphs with their molecular-formula target, and two reasoning hubs — BTOR2 (bit-level) and SMT-LIB (theory-level) — plus dual, independently derived routes RISC-V\(\to\)BTOR2 and AArch64\(\to\)BTOR2 (manual-derived vs.Sail-model-derived), each pair agent-built as framed above with the square oracle, external differentials (a Sail-generated ISA simulator, a pinned CPython), solver corroboration, and branch cross-checks as the only police. 6 reports the resulting capability snapshot — per-pair conjoined coverage, composed route coverage, branch-agreement runs down to SMT-LIB, end-to-end case studies with source-level witness replay, certified unreachability, performance, and the defects the architecture caught along the way, each localized as 1 promises.

1.0.0.6 Contributions

• A calculus of pairs: commuting squares with declared projections, decidable per-program checking with step/observable localization, and a pasting theorem whose projection-compatibility hypothesis makes cumulative loss compositional (3).

• A fidelity algebra: grades vs.assurance classes, weakest-link composition, per-run re-establishment, branch corroboration under an explicit diversity assumption, and a trusted-base ledger (4) — with the compositional core of both sections mechanized in Lean 4 (§4.7).

• The existential/universal asymmetry as an architectural principle, with the end-to-end soundness theorems that express it (§4.6).

• A measured, LLM-built instantiation: 13 agent-built pairs over 13 languages and two solver hubs, evaluated for conjoined coverage, branch agreement — including decision stacks fully disjoint after the head — a compliance-derived benchmark with machine-derived ground truth, end-to-end witness replay, certified unreachability re-validated by a formally verified checker at up-to-megabyte certificate scale, measured escape rates for the gate stack — single-leg and common-mode, the latter finding and then closing a full-stack escape — a first controlled LLM-player experiment, and the defects caught ([sec:instantiation,sec:evaluation]).

This document is a dated capability snapshot (July 2026) of a system whose coverage ratchets monotonically by construction; every number in

6 is regenerable from the accompanying artifact at this snapshot. The appendix — the detailed proofs of [sec:calculus,sec:fidelity] and the construct-inventory catalog — follows the bibliography.

2 Overview: one question, two routes↩︎

Consider a small C program: a loop over an array with an index computation, and a question — can x == 42 hold at the failure label? We narrate the route this question takes through the platform; 3 then makes the definitions precise.

2.0.0.1 The spine

The program first moves from C to RISC-V. The translator on this edge is a pinned C compiler: a digest-locked gcc with recorded flags. We can replay it bit-for-bit, but nobody can foresee or prove its output — its honest grade is \(\mathtt{reproducible}\), determinism without meaning. The RISC-V program then moves to BTOR2, a bit-vector transition-system logic that model checkers consume, and from there across a rule-for-rule bridge to SMT-LIB, where bit-vector solvers decide the reachability query.

Each of these moves is a pair: translator, source interpreter, target interpreter, and a target-to-source interpreter that carries behaviors backwards. When the RISC-V-to-BTOR2 translator runs, the platform can immediately check it on this very program: interpret the RISC-V program directly (the left edge of a square), interpret the BTOR2 translation and carry the resulting trace back to RISC-V observables (the other three edges), and compare, step by step, on the declared observables — program counter, registers, halt flag. That check passing is what the edge’s \(\mathtt{checked}\) grade means. Note carefully what it covers: every hop from the compiled binary onward. The C hop itself has no square — there is no C interpreter and no ISA-to-C carry-back — so the verified portion of the route begins at the binary; the pinned compiler contributes reproducibility, re-checked separately by a corpus-level differential against an independent C verifier (5).

2.0.0.2 The branch

RISC-V reaches BTOR2 twice. One translator was written against the prose ISA specification; a second route factors through Sail, deriving its semantics from the official RISC-V Sail model. On the segment where they diverge — from RISC-V to BTOR2 — the two routes share no translator and no carry-back; below the reconvergence they share the hub bridge, so it is the diverse prefix that agreement corroborates (§4.3). The platform runs the question down both, and the answers must agree. If they do, two independently derived encodings of RISC-V semantics corroborate each other — evidence strictly stronger than either route’s own grade (2). If they disagree, at least one route has a defect, and the per-hop squares localize it: which hop, which step, which observable ([lem:disagree,cor:localization]). The same dual-route structure exists for AArch64 (Arm manual vs.Arm Sail model).

2.0.0.3 The answer comes home

Suppose the SMT solver answers sat: the label is reachable, with a model. The model is not the answer the user asked for — it is a valuation of SMT variables. The route’s carry-backs now run in reverse: the SMT model becomes a BTOR2 witness, the witness a RISC-V trace, the trace an initial memory and register state — concretely, the inputs of the original C program. The platform then replays those inputs in the route’s source-side interpreter — for this spine, the shared RISC-V interpreter on the compiled binary, the question’s observable read at the ISA level (§4.2) — and watches the failure state actually happen. At that moment the user’s trust obligations collapse: even if every translator, both routes, and the solver were wrong, the replayed run exhibits the behavior (3). Witness-carrying answers are self-certifying; only the interpreter that replays them — itself differentially tested against an independently generated ISA simulator — remains to be believed.

Had the solver answered unsat, no replay could vouch for it. That is where the grades, the branch agreement, the multi-engine corroboration, and the independently checked certificates carry the weight (4) — and where the platform spends its assurance budget.

2.0.0.4 Beyond one spine

Nothing above is specific to C or RISC-V (1 draws the full registry graph). The same square contract admits eBPF, Wasm, and EVM programs into the BTOR2 hub; Python functions and chemical reaction networks reach the SMT-LIB hub directly; a SMILES molecular graph reaches a molecular-formula target with no solver at all (a compile pair — the calculus does not care that the languages are far from computation, only that both have defined meaning). Each pair declares what it preserves (its projection), what it rejects (typed, enumerable \(\mathtt{unsupported}\)), and its grade; the registry composes routes and reports each route’s composed coverage, grade, and loss. The rest of the paper makes each of these words precise, then measures the system.

3 A calculus of pairs↩︎

This section makes the informal contract of 2 precise: languages, behaviors, and projections (§3.1); pairs and their commuting squares (§3.2); and the pasting theorem that lets squares compose into routes, together with the projection-compatibility condition that pasting actually requires (§3.3). Fidelity, coverage, and the end-to-end guarantee build on this base in 4.

3.1 Languages, behaviors, projections↩︎

The only admission criterion for a language is that \(\llbracket \cdot \rrbracket_{A}\) is definable — an ISA manual, a logic’s model theory, a reaction-network semantics, and a molecular-graph notation all qualify. Nothing in this section assumes languages are executable or even computational.

The definition also fixes the calculus’s scope, and we state the restrictions plainly: behaviors are finite and the reference semantics is a function, so nondeterminism, divergence, reactive I/O, and refinement-style behavior inclusion are outside this calculus — faithfulness is projected trace equality. That is the right notion for the near-structure-preserving translations the platform builds and checks, and the wrong one for optimizing compilation, whose home is simulation; accordingly, the one genuinely optimizing hop in the instantiation carries no square at all and is handled differently (§4.2, 5). Languages whose official semantics is not a function (C, with its unspecified orders and undefined behavior) enter through a determinized fragment, with the gap policed differentially (5).

A program here is a closed configuration: free inputs, when present, are part of \(p\) (a program together with an input valuation). Open programs — programs quantified over their inputs — reappear in §4.6, where a solver decides over all inputs and a witness closes one.

Adequacy is an assumption, not a theorem, and we keep it visible: it is the irreducible residue in every trusted-computing-base computation of §4.4. It is discharged empirically, by differential testing against an independently produced oracle for the same semantics (the Sail-generated RISC-V simulator; 5 — which also notes the one honest exception, Python, whose pinned runtime is both semantics and interpreter, leaving adequacy there with no independent reference), and its failure modes are cross-checked by the same machinery that checks translators.

3.2 Pairs and the commuting square↩︎

Three remarks. First, everything in 5 is computable: faithfulness at a given \(p\) is a decidable, executable check — run both sides, compare under \(\pi_P\). We call this check the square oracle; in fault-tolerance terms it is an acceptance test in the sense of recovery blocks [6], turning a silently wrong — in effect Byzantine — translator into a fail-stop component [7]. Second, when the check fails it fails at a first position: a least step index \(i\) and a field \(f \in \pi_P\) on which the two sides differ. The oracle reports \((i, f)\) — a translator (or interpreter, or carry-back) defect, localized to a step and a named observable. Third, the projection is part of the contract, not a tuning knob: \(\pi_P\) states what “preserves meaning” promises for this pair, and \(F_A \setminus \pi_P\) — the pair’s loss — states what it does not.

The carry-back \(\Lambda\) is what makes a target-side result mean something at the source: a solver counterexample or a target trace is re-expressed as a source behavior. It is pair-specific because the correspondence it encodes is pair-specific; it is also why the square’s oracle is as expressive as the translator it checks.

3.3 Pasting: when squares compose↩︎

Two pairs compose when the middle language is shared: \(P_1 = (A, B, T_1, \Lambda_1, \pi_1)\) and \(P_2 = (B, C, T_2, \Lambda_2, \pi_2)\) yield the candidate composite \[P_2 \circ P_1 \;=\; (A,\, C,\; T_2 \circ T_1,\; \Lambda_1 \circ \Lambda_2,\; \pi)\] for a projection \(\pi\subseteq \pi_1\) to be determined, with \(\mathsf{dom}(P_2 \circ P_1)\) the evident composite domain. Folklore says the squares paste. They do not paste for free: \(P_2\) guarantees agreement of the two \(B\)-behaviors only up to \(\pi_2\), and \(\Lambda_1\) consumes whole \(B\)-behaviors. If \(\Lambda_1\) reads a \(B\)-field that \(P_2\) discards, the outer rectangle can fail while both inner squares hold. The missing condition is that \(\Lambda_1\) must not look outside what \(P_2\) preserves:

The support condition is not decorative. Take \(F_B = \{g, h\}\) with \(\pi_2 = \{g\}\), and let \(\Lambda_1\) copy field \(h\) into a \(\pi_1\)-kept source field: \(P_2\) can be faithful — it preserves \(g\) — while \(\Lambda_2(I_C(r))\) differs from \(I_B(q)\) on \(h\), which \(\pi_2\) permits. The outer rectangle then fails on the copied field although both inner squares commute.

3.3.0.1 Composed keep and loss

In the implementable special case — \(\Lambda_1\) fieldwise and step-aligned, each source field \(f\) computed from a dependency set \(\mathit{deps}(f) \subseteq F_B\) of target fields — the support condition has a syntactic reading, and the largest \(\pi\) satisfying 1 is \[\mathsf{keep}(P_2 \circ P_1) \;=\; \{\, f \in \pi_1 \mid \mathit{deps}(f) \subseteq \pi_2 \,\},\] a source field survives the route iff \(P_1\) keeps it and it is computed only from target fields \(P_2\) keeps. Dually \(\mathsf{lost}(P_2 \circ P_1) = F_A \setminus \mathsf{keep}(P_2 \circ P_1)\): route loss is the union of per-hop losses, each pulled back along the carry-backs. This is the formal content of the platform rule that a route must declare its cumulative loss: the observables a destination can still speak about are exactly those no hop discarded. (When \(\Lambda_1\) changes step granularity — one source step spanning several target steps, as in C-to-ISA — the same statement holds with \(\mathit{deps}\) taken over the spanned window; appendix A.2.)

1 is the debugging story of the whole platform: a divergence anywhere along a route is never a mystery about the route; it is an indictment of one hop, one step, one observable. It is also what disagreement between routes will lean on in §4.3.

3.3.0.2 Routes

The registry of languages and pairs forms a directed multigraph; a route \(R : A \to Z\) is a path through it, with composed translator \(T_R\), composed carry-back \(\Lambda_R\), composed projection \(\mathsf{keep}(R)\), and faithfulness given by iterating 1. Purity composes too, and gives caching:

4 Fidelity, coverage, and the end-to-end guarantee↩︎

3 says what it means for one translation, or one route, to be faithful. This section grades how well we know it is faithful (§4.1), shows how the grades compose — weakest link, per-run re-establishment, and branch corroboration (§4.2–§4.3) — accounts for what each layer of cross-checking removes from the trusted base (§4.4), pairs fidelity with its anti-triviality companion, coverage (§4.5), and assembles everything into the end-to-end guarantee a user actually receives (§4.6).

4.1 Fidelity grades and assurance classes↩︎

A pair declares a fidelity grade from the set \(G = \{\) \(\mathtt{trusted}\), \(\mathtt{reproducible}\), \(\mathtt{checked}\), \(\mathtt{predicted}\), \(\mathtt{proved}\) \(\}\), each grade naming both a guarantee and the kind of evidence that establishes it: \(\mathtt{predicted}\) — the translator’s output is derivable byte-for-byte from a written specification (evidence: an audit that re-derives the bytes); \(\mathtt{proved}\) — a machine-checked certificate that the square commutes, re-checked by an independent checker (evidence: the certificate and the checker’s pedigree); \(\mathtt{checked}\) — the square oracle runs and passes on every translation actually performed (evidence: this run’s oracle verdict); \(\mathtt{reproducible}\) — determinism only, via a digest-pinned toolchain (evidence: replayability, no meaning guarantee); \(\mathtt{trusted}\) — nothing.

The grades order by evidence strength, but \(\mathtt{predicted}\) and \(\mathtt{proved}\) are incomparable in kind — one is foreseeable, the other re-checkable — and nothing below is gained by forcing them into a line. What composition actually needs is the logical form of the guarantee, and that is totally ordered:

Separating \(G\) from \(\mathbb{A}\) resolves a wrinkle the informal five-tier story leaves open (what is the “meet” of \(\mathtt{predicted}\) and \(\mathtt{proved}\)?): grades differ in evidence, classes in logic, and only classes compose. A route with one \(\mathtt{predicted}\) hop and one \(\mathtt{proved}\) hop is \(\mathsf{universal}\) end to end, as it should be.

Two honesty notes on the mapping. First, grade declarations are themselves trusted inputs: only \(\mathtt{checked}\) is mechanically enforced by the framework (the oracle runs); \(\mathit{class}(\mathtt{predicted}) = \mathsf{universal}\) additionally presumes that the audited specification maps rules to semantics — a translator faithful to a wrong rule table is \(\mathtt{predicted}\) and universally unfaithful, and our own evaluation exhibits a \(\mathtt{predicted}\) edge that was wrong on covered inputs until a coverage probe caught it (§6.6). Declarations therefore sit in the trusted-base ledger like any other component. Second, \(\mathtt{proved}\) as instantiated in §6.5 certifies a per-question verdict — universal over that question’s inputs, per-run over questions — not the pair’s square for all programs.

4.2 Composition: weakest link, and per-run re-establishment↩︎

The proof is immediate from 7 and 1: universal statements conjoin into universal statements over the composite fragment; a per-run statement at hop \(i\) caps the conjunction at the programs the oracle actually saw; a \(\mathsf{replay}\) hop caps it at purity. Optimality is by the evident counterexamples. Statically, then, a route is as faithful as its weakest hop — but the static story is not the whole story, because every pair carries its own oracle:

2 applies exactly to hops whose squares run. That bounds what it can say about an opaque, pinned C compiler at the head of a route: the C hop has no square (no C interpreter, no ISA-to-C carry-back), so what the inline oracles lift, per run, is the route from the compiled binary onward. The compiler itself contributes \(\mathtt{reproducible}\) — honest: nobody can foresee or prove its output — plus a separate, corpus-level differential against an independent C verifier (5); questions on the spine are accordingly stated over ISA observables. The declared route grade remains the weakest-link meet — re-establishment is per-run evidence, never a static promotion, and never coverage for a hop with no oracle.

4.3 Branch corroboration↩︎

The registry graph is not a line: one source may reach one destination by several routes. Let \(R_1, R_2 : A \to Z\) with composed keep-sets \(K_1, K_2\) and \(K = K_1 \cap K_2\), sharing the endpoint interpreters (language-owned) but no translator or carry-back.

Both are immediate: two faithful routes each equal \(K(I_A(p))\), hence each other. What 2 buys depends on an assumption we state rather than hide:

The scoping matters, and independence must be argued, not assumed. Below the reconvergence, routes may share hops — in the platform both RISC-V\(\to\)SMT-LIB routes share the BTOR2\(\to\)SMT-LIB bridge — and shared emission libraries are shared failure surface, so agreement corroborates the diverse prefix and nothing beneath it. The evaluation therefore also runs a disjoint-decision variant of every branch question (§6.2, 2): the direct route’s BTOR2 system decided natively by btormc, against the Sail-derived route through the bridge and Z3, so the diverse segment extends through the decision procedure and the shared bridge drops out of the corroborating pair entirely; what remains shared is the emission library (the site of the cross-route incident below) and the language-owned endpoints. Correlated failures between nominally independent implementations are, moreover, the empirical norm [8]; our own history exhibits both a cross-route common-mode failure through a shared emitter and a shared-misreading blind spot (§6.6), and translators written by LLM agents plausibly share model-family failure modes.

Under 2, the residual failure mode of an agreeing branch is a common-mode failure: independently produced encodings of the same semantics, wrong in the same observable way on the same program. We do not assign this a probability; we account for it structurally, in the trusted base ledger below. This is how the platform manufactures assurance out of hops that are individually only \(\mathtt{checked}\) — dual modular redundancy whose comparator, unlike a voter, localizes: agreement of independently derived routes is evidence that neither route’s grade alone provides.

4.4 The trusted-base ledger↩︎

Define the trusted computing base \(\mathsf{TCB}(v)\) of a verdict \(v\) as the set of components whose correctness \(v\)’s soundness still assumes after all checks that ran. Each cross-check layer strictly shrinks it (1); the last two rows are not interchangeable, and the difference is the central asymmetry of the whole design.

4.5 Coverage, and the ratchet↩︎

Fidelity alone is gameable by triviality: a pair handling one instruction is vacuously \(\mathtt{proved}\). Its companion axis is measured against a yardstick the implementer does not choose:

Coverage is gamed by unsoundness (accept everything, translate it wrongly) exactly as fidelity is gamed by triviality (translate one thing, prove it); the conjunction closes both routes to a vacuous “pass.” Everything a pair rejects must be a typed \(\mathtt{unsupported}\), so the uncovered set is itself enumerable and auditable — partiality is fail-fast, never silent.

Coverage then grows by a discipline with a soundness theorem:

The implementable extension check is byte-identity of all old outputs across the update — the same twice-and-diff mechanism as [prop:cache], run across versions. This is precisely the repo’s widening protocol (additive interpreter bumps, versioned events, dependent-pair re-validation), which 6 measures over the project’s own history.

4.6 The end-to-end guarantee↩︎

Finally, what does a user hold at the end? Let \(R : A \to Z\) be a route into a reasoning language \(Z\) (one a solver consumes: a transition-system logic, an SMT theory). The user asks a question about an open source program \(p(x)\) — free inputs \(x\) — and a condition \(\varphi\) over \(\mathsf{keep}(R)\)-observables: is \(\varphi\) reachable? The solver decides at \(Z\); its answer comes back in one of two logical shapes, and they differ fundamentally in what must be trusted.

One caution on hypothesis (i): per-run oracle evidence combined with branch agreement (2, 2) raises confidence in it but does not entail it — oracle passes cover the finitely many closures actually run, and agreement bounds the residual failure to common-mode rather than excluding it. Universal verdicts are precisely where the \(\mathsf{universal}\) tiers earn their keep; evidence below that tier is corroboration, not entailment.

The asymmetry between [thm:existential,thm:universal] is, we argue, the right lens on the entire design: for questions whose answers carry witnesses, trust is nearly free — carry the witness back and replay it at the source; the platform’s graded tiers, branches, and certificates exist for the other half, the universal answers where no witness can vouch for the verdict. This is the end-to-end argument [9] transplanted to translation: the check that settles a witness-carrying answer belongs at the endpoint — the source interpreter — and what the intermediate hops provide is, for that half, an optimization; only for universal answers, where no endpoint check can exist, does hop fidelity become the guarantee itself. A system that makes the carry-back \(\Lambda\) a first-class, per-pair component is a system in which the cheap half of trust is always cashed in; a system that grades and stacks cross-checks is one in which the expensive half is bought consciously, in labeled increments, with the bill itemized in the ledger of §4.4.

4.7 Mechanization↩︎

The compositional core of [sec:calculus,sec:fidelity] is mechanized in Lean 4 (core library only, no mathlib; \(\sim\)​820 lines, in the artifact): the pasting theorem with the support condition, localization, the assurance-class chain and weakest link (sound half), per-run re-establishment, both branch lemmas, the ratchet (verdict preservation and coverage monotonicity under extensions), both end-to-end theorems, the specialization obligation of 4(iv) — with the theorem that it discharges the per-instance-translation hypothesis from the single open translation the platform performs — and the route telescope — routes of arbitrary length as a dependently-typed chain of pairs over interpreter-bundled languages, with the paper’s “pairwise support conditions” as a recursive coherence predicate, and the \(n\)-ary pasting and localization theorems proved by induction through the binary ones (the canonical head-projection choice at each junction is shown lossless by a reprojection lemma). Three modeling choices mirror the paper exactly. Components are Lean functions, so purity is by construction and [prop:cache] is definitional; partiality is Option, with \(\mathtt{unsupported}\) as none; and projections are generalized from field subsets to arbitrary observable-compression maps, with “\(\pi\subseteq \pi_1\)” becoming factoring. Because every theorem takes each component-output witness as an explicit hypothesis, a statement’s trusted base is literally its hypothesis list — 3 in Lean assumes source-interpreter adequacy and nothing else, and its proof term is three tokens:

[basicstyle=\ttfamily\footnotesize,
  literate={∀}{{$\forall$}}1 {→}{{$\to$}}1 {₀}{{$_0$}}1
           {φ}{{$\varphi$}}1 {π}{{$\pi$}}1 {∃}{{$\exists$}}1
           {∧}{{$\land$}}1 {⟨}{{$\langle$}}1 {⟩}{{$\rangle$}}1]
theorem existential_self_certifying
  (adequacy : ∀ p b, IA p = some b → sem p = some b)
  (hreplay : IA p₀ = some b) (hφ : φ (projB π b)) :
  ∃ b', sem p₀ = some b' ∧ φ (projB π b') :=
  ⟨b, adequacy _ _ hreplay, hφ⟩

2 maps the paper’s results to their Lean theorems with each proof’s exact axiom footprint, re-checked at every build; the one classical proof is 1 (an unfaithful route names no witness by itself). The table also shows where mechanization stops, and we state it plainly: 4’s clauses (iii) and (iv) enter the Lean statement as hypotheses. Both now carry tested surrogates rather than by-construction assertions. The specialization obligation is discharged by sampled commutation checks per reasoning pair with free inputs (in the suite): the open program is translated once, and for sampled valuations the emitted artifact is byte-identical while the specialized instance’s square passes — the shape universal_from_open_artifact consumes. The solver-artifact-to-target-semantics correspondence behind (iii) is corroborated per verdict: every bounded-unreachable route verdict in the branch, benchmark, and certified experiments is additionally replayed through the strict target interpreter for the full bound — sampled inputs where the system has any — and no bad may fire (§6.2–§6.5). Sampling corroborates, it does not entail — which is the grade discipline applied to the calculus’s own hypotheses.

Deliberately not mechanized: the fieldwise loss computation and retiming case of appendix A.2(syntactic side conditions over a concrete carry-back representation), the optimality halves of [prop:weakestlink] (meta-statements over models), and the grade set \(G\) itself — evidence provenance is not a mathematical object, which is the point of separating \(G\) from \(\mathbb{A}\). The telescope theorems’ audit adds only Quot.sound (from structural-recursion equations); localization remains the sole classical proof.

5 Instantiation: the platform↩︎

The calculus is implemented as hurdy-gurdy, a Python platform whose structure mirrors 3 exactly: a framework that holds no pair semantics, per-language shared interpreters, and per-pair translators and carry-backs. 1 draws the registry graph at the snapshot; this section describes what exists, and 6 measures it.

5.1 Framework↩︎

The framework provides the registry (the language/pair graph with deliverable status); the content-addressed cache of [prop:cache]; the generic square oracle — align \(I_s(p)\) against \(\Lambda(I_t(T(p)))\) under \(\pi\), with step/observable localization —; the route enumerator and route runner (routes are enumerated and reported with composed grade, coverage, and loss — never chosen; choosing is the caller’s job); the coverage harness (construct-inventory extraction, typed-\(\mathtt{unsupported}\) histograms); the route grader (composed determinism, composed coverage, and branch-agreement measurements, run on merge); and the solver/checker plumbing. Everything except the solver call is byte-deterministic, and a twice-and-diff harness enforces [prop:cache] repo-wide.

5.2 Languages and reasoning hubs↩︎

Thirteen languages are registered, each with a specification-anchored formal semantics and (for all but C, at the snapshot) a built shared interpreter: the ISAs RISC-V (RV64IMC), AArch64 (a growing A64 slice), eBPF, Wasm, and EVM; C (whose “interpreter” role is played differentially, see below); Python (a pinned CPython restricted by an AST allow-list to an integer subset — the loader rejects, CPython runs); Sail (an executable slice of the Sail-derived RISC-V and Arm semantics); chemical reaction networks (a discrete Petri-net stepper); SMILES molecular graphs and molecular formulas; and the two reasoning hubs: BTOR2, a bit-vector/array transition-system logic consumed by hardware model checkers, and SMT-LIB (\(\mathrm{QF\_ABV}\) and \(\mathrm{QF\_LIA}\) fragments).

Reasoning languages own, beyond an interpreter, a solver inventory (BtorMC and Pono for BTOR2; Z3, Bitwuzla, Boolector, cvc5, Yices2 for SMT-LIB) and a witness-checker inventory: interpreter replay of BTOR2 .wit witnesses, model evaluation by the deterministic SMT-LIB evaluator, multi-engine corroboration, and a bit-blasted certificate pipeline for \(\mathtt{proved}\)-tier unreachability with two checker rungs: the DRAT proof checked by drat-trim (independent, unverified), and — preferred when present — elaborated to LRAT (drat-trim as an untrusted elaborator) and re-validated by cake_lpr, the formally verified CakeML checker, built natively from its compiler-generated ARMv8 assembly (§6.5).

Interpreter adequacy (1) is discharged differentially: the RISC-V interpreter against the Sail-generated reference simulator (sail_riscv_sim) and the official riscv-tests / riscv-arch-test suites; the Python subset against pinned CPython by construction — a circularity we note plainly: for this one language the pinned runtime is both the semantics and the interpreter, so adequacy has no independent reference; C against CBMC on the same source (with a classification step separating C-undefined-but-ISA-defined behavior from genuine faults).

5.3 Pairs and routes↩︎

Thirteen pairs are built to varying, measured extents (3). The spine is C \(\to\) RISC-V \(\to\) BTOR2 \(\to\) SMT-LIB, with the C head a digest-pinned gcc at grade \(\mathtt{reproducible}\): the square-verified portion of the spine begins at the compiled binary (§4.2), and the C hop is re-checked separately by the CBMC differential above. The direct RISC-V\(\to\)BTOR2 lowering draws on the rotor bounded model checker [10]. RISC-V and AArch64 each reach BTOR2 by two independently derived routes (manual-derived direct translator vs. Sail-model-mediated), instantiating 2; the BTOR2 hub funnels five ISAs into one solver interface, and the \(\mathrm{BTOR2}\to\mathrm{SMT}\)-LIB bridge (a rule-for-rule operator mapping at grade \(\mathtt{predicted}\)) connects the hubs, so every BTOR2 question can also be decided natively-vs-bridged — solve-step corroboration. CRN and Python reach SMT-LIB directly (\(\mathrm{QF\_LIA}\)), and SMILES\(\to\)formula exercises the calculus away from computation entirely.

5.4 How the pairs were built↩︎

Each pair (and each shared interpreter) was implemented by an independent LLM agent from a one-page registration brief, against the calculus as a written contract, under three standing rules: agents never modify the framework or another deliverable’s code; interpreter changes are versioned events that re-validate every dependent pair ([prop:ratchet]); and all growth is by additive widening — extend the covered fragment, re-run all prior evidence byte-for-byte, ratchet the coverage number. The platform’s checks — the square oracle, the differentials, solver corroboration, branch agreement, twice-and-diff — were the only semantic quality gate; no human reviewed agent code for semantic correctness, though an autonomy protocol did escalate one class of change — edits to shared emission code — for human sign-off (“largely unsupervised” means exactly this: the human gated whether such a change could land, never whether it was right). The defects those checks caught, and where they localized, are part of the evaluation (§6.6): the implementation process itself is an experiment in the paper’s thesis that translation trust can be manufactured by architecture rather than by trusting the translator’s author — whether that author is a compiler vendor or a language model. The same discipline is the platform’s intended growth model: hurdy-gurdyis designed to scale in language support through open contribution — new pairs developed by anyone, with LLMs, with agents, or by hand, and added to the repository through ordinary pull requests, admitted by the checks above rather than by trust in their author. Concretely, a contributed pair arrives as the calculus’s tuple with its evidence surface attached: a pure translator and carry-back, the declared projection and grade, typed \(\mathtt{unsupported}\) partiality, probe programs for every construct of the language-owned inventory it claims, and a square the harness can run. The merge gate re-runs the conjoined coverage measurement, the dependent routes’ branch agreements, and twice-and-diff determinism — the same machinery 6 measures, applied as an admission test — and [prop:ratchet] guarantees an additive contribution can only extend, never silently invalidate, the verdicts already earned.

6 Evaluation↩︎

We evaluate the snapshot along the axes the calculus makes measurable: per-pair coverage (§6.1), composed route coverage and branch agreement — including a disjoint-decision block — (§6.2), a compliance-derived reachability benchmark decided along both RISC-V routes (§6.3), end-to-end case studies exercising 3 (§6.4), certified-unreachability runs inhabiting the \(\mathtt{proved}\)tier (§6.5), the defects the architecture caught (§6.6), a measured escape-rate estimate for the gate (§6.7), a first controlled experiment with LLM players (§6.8), and performance, determinism, and scale (§6.9). Every number in this section’s tables is regenerated by one script from the live registry and real runs at the snapshot commit, with a few curated exceptions marked at source — the defect catalog behind 7 is hand-mined from history, and 10 formats the recorded outputs of a manual two-arm protocol; the escape experiment’s earlier-round numbers (§6.7) likewise come from its incident record. (Host: macOS/arm64, CPython 3.12, Z3 4.13, btormc 3.2, cadical; drat-trim pinned at source commit 2e3b2dc and cake_lpr at a4323b2, the engine inventory recorded in the regenerated env.json; the platform’s own suite runs 1215 tests there, all green, with 3 host-dependent skips.) The evaluation remains deliberately fully specified rather than large: every question — authored or derived — is checked end to end with its ground truth stated, and the largest sweep (the 78-question compliance-derived benchmark of §6.3) is still small next to an SV-COMP-scale campaign, which remains future work.

6.1 Capability snapshot↩︎

3 reports per-construct coverage measured at harvest time — not transcribed from documentation — in both of 8’s readings: accepted (the probe translates without a typed \(\mathtt{unsupported}\) abort) and conjoined (accepted and the pair’s square oracle passes on the probe — the definition’s actual conjunction, run probe by probe). For every pair with a decidable square the two columns now coincide; they did not when the conjunction was first measured, and what it surfaced on its first run is instructive enough to report (§6.6, incidents I20–I22): the Sail-route front dropped the program’s initial memory, so every load-family probe diverged at step 0 (accepted, silently wrong — precisely the failure mode acceptance counting cannot see), and three of the BTOR2 lowerings modeled a program counter that leaves the code as stuck where every reference interpreter halts, so every taken-jump probe whose target exits the image diverged on halted (the worked example of §3.2 shows this square, and its oracle output, verbatim). It also audited its own instrument: one probe (SD) stored over its own ECALL terminator, so the reference interpreter could not run it and no square had ever executed on that construct — acceptance counted it covered anyway. Measuring the definition’s conjunction found all three in its first run; the fixes are ordinary versioned translator bumps and one probe repair. Pairs without a decidable square — the predicted-grade hops into the SMT-LIB hub — discharge the faithfulness conjunct per run at question time instead (§4.2) — what their grade leaves to per-run checking; the table marks them per-run (the fourth predicted pair, SMILES\(\to\)formula, has executable ends and conjoins directly). Denominators are language-owned inventories (8’s yardstick): both RISC-V-headed pairs measure against the same 96-construct RV64IMC inventory, the two AArch64 pairs against one declared A64 slice whose out-of-scope constructs count in the denominator, and the Wasm and EVM rows against their in-scope \(\cup\) enumerated-out-of-scope unions (54/75, 86/144) — a gap shows as a typed \(\mathtt{unsupported}\) entry, never by shrinking the total. Depth remains uneven by design and visibly so: the spine is deep (all 96 RV64IMC constructs conjoined; eBPF complete at 126; the BTOR2\(\to\)SMT-LIB bridge total on its 56-item operator/sort/directive inventory), Python stands at 11 of 27 subset constructs, and every gap is a typed \(\mathtt{unsupported}\) the harness can enumerate (the “gaps” column). The declared A64 slice is still narrow against the full base ISA — the honest reading of 27/33 is “the in-scope family conjoins, and the slice is small.” The C head carries no construct inventory: its translator is the pinned compiler, graded \(\mathtt{reproducible}\) (§4.2).

6.2 Composed coverage and branch agreement↩︎

¿tbl:tab:branch? (top) composes conjoined coverage along whole routes: a construct counts iff its probe survives every hop and every hop with a decidable square passes it on that hop’s input. Nothing a head accepts is eaten at the hubs: every accepted probe of every route survives composed to its route’s target, squares included. The denominators are the source language’s inventory, so the two RISC-V routes are measured on the same 96-construct yardstick and both compose 96/96 — the spine composes losslessly, and the earlier version of this table, whose two RISC-V rows quoted different pair-chosen denominators (96 vs.), is exactly the yardstick-shopping 8 forbids and this measurement now closes. The AArch64 rows also carry a ratchet anecdote the machinery makes precise: one revision earlier the Sail-mediated route composed to \(0/33\), because the Sail\(\to\)BTOR2 translator lowered only the RV64IMC arm — and the harness localized every miss to the sail-btor2 hop by name. Widening that one hop (an additive translator bump, RISC-V arm byte-identical per [prop:ratchet]) closed the gap without re-earning any other evidence. A gap the system reports and localizes is the designed behavior; a gap papered over would be the defect.

The bottom of ¿tbl:tab:branch? is the fidelity payoff of 2: the same reachability questions decided along independently derived routes. Twelve solver-level questions — constant dataflow, summation and countdown loops under unrolling, store/load through memory, two questions about a gcc-compiled C program (can a0 be 47 at halt? can it be 99?), and four AArch64 questions decided along the Arm-manual-derived and the Arm-Sail-model-derived route — were each decided along both routes of their branch; all twelve pairs of verdicts agree, including the universal (unreachable) halves where agreement carries real information. The C rows exercise the full re-establishment story: an opaque \(\mathtt{reproducible}\) compiler heads both routes, and its output is validated downstream twice, independently. The AArch64 trace-level rows cross-check the same branch below the solver, directly comparing the two carried-back behaviors under \(\pi\). The table’s bottom block addresses 2’s scoping head-on: the twelve solver-level rows share the BTOR2\(\to\)SMT-LIB bridge below the reconvergence, so every one of the twelve is re-decided with fully disjoint decision stacks after the head (2) — the direct route’s BTOR2 system decided natively by btormc (no bridge, no SMT-LIB, no Z3) against the Sail-model route through the bridge and Z3. All twelve agree. Every unreachable verdict among them is additionally corroborated below the solvers: the strict BTOR2 interpreter replays the direct route’s system for the full bound and no bad fires — the tested surrogate for 4’s artifact-to-semantics hypothesis (recorded per question, as is the same replay for every bounded-unreachable verdict of 4). The diverse segment now spans the lowering derivation (ISA-prose vs.formal-model) and the decision procedure (different solver, different input format); the residual shared surface, stated rather than hidden, is the BTOR2 emission library — the site of incident I3, the platform’s one recorded cross-route common-mode failure through shared code (shared misreadings are the other kind, §6.6) — and the language-owned endpoint interpreters.

6.3 The compliance slice as a question set↩︎

The questions above were authored; 4 scales the same discipline over a derived question set nobody hand-picked. The platform’s RISC-V compliance slice — self-checking programs in the upstream riscv-tests HTIF tohost convention, built with the pinned cross-toolchain at the upstream link base 0x8000_0000 — doubles as a reachability benchmark: each program is reference-run to completion, and for each data register the harness derives one question whose target value the register demonstrably held (ground truth reachable) and one whose target no register held at any step (ground truth unreachable within the bound), with the unrolling bound covering the whole run. Every question is then decided independently along both RISC-V routes. Three honesty notes. First, the slice is curated in the upstream convention rather than taken binary-for-binary from upstream: the stock -p- binaries open with machine-mode CSR and trap setup that is outside the declared user-ISA scope, so the slice re-creates the grading convention over the user subset (the gap is typed, not hidden). Second, the ground truth comes from the shared reference interpreter — but that interpreter is exactly the component the adequacy campaign validates step-for-step against the Sail-generated gold simulator on these same programs, so the benchmark’s ground truth is anchored outside the platform. Third, the benchmark’s discriminating power is scoped: ground truth and both routes share the reference interpreter, so it measures translator- and route-level defects — a shared-misreading defect of the MUL/ADD class (§6.6) would pass it undetected, and the external Sail differential, not this benchmark, is what polices that class. The result: 78 questions over 10 programs (constant dataflow, logic, shifts, 32-bit word ops, taken and untaken branches, computed jumps, the store/load family, multiplication, division with its RISC-V-defined edge cases, and compressed forms), both routes agreeing on all 78 and all 78 matching ground truth, in under a minute end to end — with every one of the 39 bounded-unreachable verdicts additionally corroborated by a full-bound replay of the direct route’s system through the strict BTOR2 interpreter (§6.2’s surrogate, recorded per question). Preparing this benchmark also forced one more fidelity repair the base-0 probes could not see: the Sail-route front rebased images to address 0, which silently breaks every pc-relative absolute-address computation (AUIPC/LA) on images linked at the upstream base — found while squaring the translator against the slice’s link discipline, and fixed by carrying absolute addresses through the Sail object (a versioned bump, with the squares and this benchmark as regression).

6.4 End-to-end case studies↩︎

5 instantiates 3 once per hub and front-end family, completing the round trip of 3 at the source each time. (1) The C spine: both routes answer reachable for a0\({=}47\), and the source-level replay runs the compiled program in the shared RISC-V interpreter to the halt in _start() with a0\({=}47\) observed — the verdict survives even if every translator and the solver were wrong. (2) Python: “is the trailing assert violable?” for a function with a bounded loop and a branch; Z3 finds the witness \(x{=}4\), the shared QF_LIA evaluator independently re-checks the model (smt_model_ok), and the input is replayed through the pinned CPython down the taken branches, firing the assert. (3) EVM: \(6\times7{=}42\) on the operand stack, decided natively (btormc on the BTOR2 system, witness replayed by the strict BTOR2 interpreter) and bridged (through the SMT-LIB hub with Z3) — solve-step corroboration across two engine families, agreeing. (4) CRN: a two-firing reachability question in a reaction network, witness schedule replayed by the Petri-net interpreter. In all four, the final trust rests on the source interpreter (plus the small fixed replay harness 3 names), per the last row of the ledger in §4.4.

6.5 The certified tier↩︎

6 inhabits the ledger’s certified row (§4.4), twice — via the pipeline of 4 — once at each end of the difficulty scale. Both questions are pair-derived and input-driven: eBPF programs whose CALL models helper returns as free inputs. The first squares one input and asks whether \(x^2 = 3\); no square exists modulo \(2^{64}\), so the claim is universal over all inputs — and its refutation is essentially unit propagation on the low bits (the elaborated LRAT is 18 bytes). The second masks and offsets two inputs into \([2, 2^{16}{+}1]\), multiplies them, and asks whether the product can be \(2^{31}-1\): the Mersenne prime admits no factorization with both factors in range, and refuting a \(16{\times}16\)-bit multiplication is certificate checking at scale — a 2.8 MB DRAT elaborating to an 11.8 MB LRAT, re-validated in seconds. In both, three engines corroborate unsat, bitwuzla bit-blasts the query to CNF, cadical emits a DRAT refutation, drat-trim elaborates it to LRAT — an untrusted step: a wrong elaboration can only fail the re-check, never fake a pass — and cake_lpr, the formally verified CakeML LRAT checker (soundness machine-proved down to the binary; here built natively from its compiler-generated ARMv8 assembly), re-validates the proof against the CNF from scratch. The verdicts’ \(\mathsf{TCB}\)is exactly the ledger’s certified row: the bit-blaster’s BV\(\to\)CNF step and a verified checker, with all three deciding engines and the elaborator demoted to discovery devices — the solve step’s residue; the route hops that produced the artifact remain accounted per the ledger. Both certified systems are also corroborated below the whole certificate pipeline: fifty seeded random helper streams replayed through the strict BTOR2 interpreter fire no bad (recorded in the run data). The reachable siblings (\(x^2 = 4\); \(x{\cdot}y = 46341^2\)) correctly decline to certify.

Wiring this exhibit produced one more architecture-caught defect, live: the checker adapter matched the substring VERIFIED in the checker’s output — and drat-trim reports failure as s NOT VERIFIED, which contains it. Every check, sound or bogus, reported success. The bug could not surface on hosts without the checker (the call raised before parsing) nor on real certificates (which do verify); it fell to the negative control — a bogus refutation of a satisfiable CNF that must fail and did not. The fix parses the exact status line, and the control is now a permanent test. This is the paper’s own instrument audited by the discipline it describes (cf.§6.6), and a caution we commend to anyone wiring a proof checker: a checker adapter without a negative control is itself unchecked. The verified checker’s adapter was written under that rule from the start — wisely, since cake_lpr exits 0 even when checking fails; only the exact s VERIFIED UNSAT line signals success, and both checkers’ negative controls are permanent tests. One honest subtlety the exercise surfaced: for this instance the refutation is propagation-dominated, so mutating single proof lines is not a valid negative control (the checker legitimately completes the derivation); the satisfiable-formula control is the sound one, since no valid refutation of a satisfiable formula exists.

6.6 Defects the architecture caught↩︎

The pairs were written by independent LLM agents with no human semantic review (§5.4); the architecture’s checks were the only gate. Mining the full history (675 commits across all refs at the 2026-07-03 mining pass; \(\sim\)​21 runtime-code fix commits) plus the three defects the conjoined-coverage measurement caught on its first run (§6.1), the probe-operand deficiency the fault-injection experiment exposed, and the compare-vector gap only the common-mode round could expose (§6.7) yields 24 recorded defect incidents: 15 caught by the architecture’s cross-checks rather than by ordinary unit tests, and 7 more — including the checker-adapter defect of §6.5, a probe that could never have exercised its own square, probes whose operands underdetermined their constructs, and benchmark compare vectors on which signedness is invisible — by the audits and controls the architecture imposes on its own instruments. Read this as case-study evidence, not a hit rate: the catalog is mined from our own history, it has no denominator (the blind-spot incident below proves the escape rate is nonzero), and no baseline says what a conventional test regime would have caught. 7 lists ten representative architecture-caught defects, each localized — component, step, observable — as 1 promises.

Three second-order observations are worth as much as the table. First, the checks caught their own instruments — seven of the 24 incidents are check-of-the-check repairs; three representatives: the Sail ISA differential was once passing vacuously (comparing empty traces), the in-image suite caught a witness generator emitting empty witnesses, and the DRAT checker adapter accepted every outcome until a negative control ran (§6.5) — all found because the harnesses carry positive and negative controls, and all three are why 1 is stated as an assumption with empirical discharge rather than as a fact. Second, the history contains a genuine blind spot of the square, exactly of the class 2 predicts: the RISC-V interpreter and the RISC-V\(\to\)BTOR2 translator both silently mis-decoded MUL (funct7 \(0x01\)) as ADD — both legs agreed, the square was blind, and the defect was found by manual audit. The platform’s structural answer is diversity: the decoder is now anchored against 610 Sail-emitted words, and unknown funct7 hard-aborts on both sides. Third, in one incident three existing unit tests had been written against the buggy behavior (an evaluator masking every array store to 8 bits): tests written by a component’s author codify the author’s misreading; cross-checks against independently derived semantics do not. The architecture also disconfirmed one reported bug (a claimed slice-width defect shown to be a stale-cache artifact), and its differential campaigns — 300 seeded RV64IMC programs vs.the Sail simulator, a 10-seed Csmith campaign vs.native gcc, 463 reference cases — completed with zero divergences against harnesses whose positive controls confirm they can fail.

6.6.0.1 Two incidents in full

The catalog’s two most argument-bearing entries deserve their narratives. First, the blind spot: the RISC-V interpreter and the riscv-btor2 translator mis-decoded MUL (funct7\({}=\)0x01) as ADD — identically. Both legs of every square agreed, so the square was structurally blind, and the defect was found by manual audit during widening, not by the architecture. This is the residual failure mode the calculus itself predicts — 2’s “both unfaithful with identical projected error” — landing not between two translators but between a translator and the component 3 crowns as the sole residual \(\mathsf{TCB}\). Both sides now hard-abort on unknown funct7, and the structural answer is external anchoring: the decoder is validated against 610 Sail-emitted instruction words and against an independently written RV64C decompressor, construct by construct — and the common-mode round of §6.7 now measures this incident’s whole class directly. Second, the common mode: the shared BTOR2 emission library declared states before their constant init values, so every emitted init line was malformed — in every BTOR2-emitting pair at once, both branches of every RISC-V question included — and the one solver then wired (Z3, through the bridge) tolerated the malformation. Adding the second and third engines turned it into hard rejections: solve-step corroboration, not the squares, caught it (incident I3). Between them the two incidents mark the exact boundary of 2: shared code and shared misreadings are what agreement cannot see, which is why the ledger keeps the emission library and the endpoint interpreters inside every branch verdict’s \(\mathsf{TCB}\)— and why the disjoint stacks of 2 and the external differentials exist.

6.7 An escape-rate estimate for the gate↩︎

The catalog above is mined from history and has no denominator; the MUL/ADD blind spot proves the gate’s escape rate is nonzero. 8 measures it (5 draws the gate stack): seeded semantic mutations of the riscv-btor2 translator’s emissions — uniform rules modeling systematic mis-lowerings (every sext emitted as uext, incident I2’s family) and site rules modeling single-site defects (incident I1’s family); operand swaps only on non-commutative operators, so no trivially-equivalent mutants; rules that change no probe artifact excluded from the denominator — each run through the architecture’s gates in the order the platform applies them. The experiment earned its keep before its final numbers did: in its first round, both srl\(\to\)sra mutants escaped all three gates (36 of 51 caught at the square layer), because every ALU probe ran its construct on degenerate all-zero operands, on which logical and arithmetic shifts agree — the “96/96 conjoined” verdict was faithfulness on the probes, and the probes underdetermined the constructs. Hardening the probes with mixed-sign operands moved 50 of 53 catches to the square layer but let ult\(\to\)ulte escape — strictness is observable only at equal operands — so the probes now run an equal-operand and a mixed-sign instance per construct (incident I23; the ratchet kept every previously covered construct covered throughout). In the final round, 51 of 55 applicable mutants die at the square suite, the remaining 4 at the compliance-derived benchmark, and none escape. Three honest notes: zero escapes means this mutation family is now covered, not that the escape rate is zero; the authored branch questions caught nothing in any round (the derived benchmark subsumes them as a differentiator, a finding in itself); and the denominator is one translator’s emission space, not the platform.

6.7.0.1 The common-mode round

3pt

Single-leg mutation cannot model the MUL/ADD class where both legs of the square are wrong identically — so a second experiment injects exactly that (9): six shared misreadings, each applied as the same uniqueness-checked source patch to both the reference interpreter and the riscv-btor2 translator (in-memory shadows; the repository is untouched). The structural predictions hold, measured: the square suite is blind on all six (both legs agree on every probe), and so is expected-based grading in the poisoned world, where the benchmark’s ground truth is derived by the mutated interpreter itself. What catches the mutants are the gates outside the shared misreading — 5’s stack read as ordered by independence, each gate derived farther from the shared code than the last: four die at cross-route disagreement with the Sail-derived branch, and two survive even that — their misreadings never surface in the per-register values the derived questions sample — falling only to the external Sail-simulator differential, which (run as a parallel column) catches all six. The round also caught its own instrument, live: in its first run, slt-as-sltu escaped every gate — the slice’s compare vectors were all same-sign, on which signed and unsigned comparison agree, so neither the derived questions nor the differential’s executed streams could see the difference (incident I24, the slice-level instance of I23’s probe lesson, and the platform’s first measured full-stack escape). The ratchet’s answer was upstream-faithful — rv64ui-slt’s mixed-sign and equal-operand vectors added to the slice — after which the round completes with zero escapes. The honest reading mirrors 2’s scope exactly: against shared misreadings every gate built from the shared reading is blind by construction, corroboration is only as strong as the most independently derived anchor, and that anchor’s vectors are themselves an instrument the discipline must audit.

6.8 The other direction: an LLM plays the platform↩︎

The introduction’s two-directional experiment has, until here, reported only its build half. This subsection is a first, deliberately small evaluation of the player half: 12 reachability questions with platform-established ground truth (6 reachable / 6 unreachable, spanning RISC-V signedness and load-width traps, eBPF square-residue and bounded-factorization questions, and Python assert-violability), posed to fresh, context-free frontier-LLM agents under two protocols (6). Arm A (unaided) received only the question text, instructed to answer by reasoning with no tools. Arm B (player) received the same question plus the repository and the head-construction snippet, instructed to decide via the platform and report the verdict with its evidence basis. One agent per question per arm, no retries; 10 lists the questions and both arms’ verdicts with each arm-B answer’s evidence artifact; prompts, ground truths, per-run outputs, and grading are in the artifact (results/llm_player/).

Both arms scored 12/12. That is the honest headline, and it reframes what the platform buys at this question scale: not raw accuracy — the unaided frontier model simulated the loops, caught both signedness traps, and factored 2147766287 by Fermat’s method in its head — but the evidence class of the answer. Every arm-A verdict rests on the model’s say-so (all were reported at high confidence, so confidence would not have flagged a wrong one); every arm-B verdict carries a machine-checked artifact: two-route agreement on the RISC-V questions, hedged explicitly as bounded-\(k\) verdicts resting on route fidelity; witness replays through the strict interpreters on the reachable eBPF/Python questions; and tier-raises to \(\mathtt{proved}\)on the unreachable eBPF questions. The sharpest contrast is the bounded-factorization question: arm A answered correctly by recalling that 1073741789 is the largest prime below \(2^{30}\) — opaque memory, exactly the evidence the calculus cannot grade — while arm B produced a 17 MB LRAT certificate re-validated by the formally verified checker, with the trusted base named. One player even devised its own positive control unprompted (flipping the load question’s target to the sign-extended value and confirming reachable on both routes). Four limitations, stated plainly: the protocol scripted which platform entry points to use (the players executed and interpreted; they did not discover the platform cold); the subject model is from the same family that built the platform; the grading is partly circular — ground truth is platform-established and arm B answers via the platform, so arm B can fail essentially only by mis-operating or misreading the tools; and 12 questions at this size cannot separate the arms on correctness — questions hard enough that unaided reasoning actually fails are the obvious next step.

6.9 Performance, determinism, and scale↩︎

Translation is not the cost center: whole-route translation of the loop question (\(k{=}25\) unrolling, \(\sim\)​200 kB of SMT-LIB) is \(\sim\)​5 ms cold and a sub-millisecond content-addressed cache hit warm ([prop:cache] cashed in), against a Z3 decide in the tens of milliseconds on either route; the twice-and-diff determinism check passes on both routes. The numbers say the honest overhead of the whole discipline — checking every hop, re-running for determinism, replaying witnesses — is small against the solver call it wraps. ¿tbl:tab:scale? probes where the pipeline stands as questions grow, on two axes: unrolling the summation loop to \(N{=}100\) (\(k{=}505\), a 4 MB artifact) keeps whole-route translation under 0.1 s and the decide under 1 s, growing roughly linearly; and the certified tier survives the bounded-factorization family from propagation-size to search-size — certificates growing from 25 kB to an 11.8 MB LRAT, each re-validated by the verified checker in seconds. Neither axis reaches industrial scale, but both cross the region where “toy” criticisms live: the pipeline’s costs grow smoothly, with no cliff through the measured range.

7 Related work↩︎

7.0.0.1 Certified compilation and translation validation

CompCert [1] and CakeML [2] prove one translator correct once; translation validation [3], [4] and its modern descendants [5], [11] validate each run of one translator, and validators can themselves be verified [12]. Credible compilation [13] — per-run validation of a compiler’s own result — is a direct ancestor of re-establishment (2). In our vocabulary these are grades of a single edge; our contribution is the graph of edges of heterogeneous grade — how faithfulness, loss, and assurance compose along routes, how per-run validation re-establishes hops that carry squares, and how independent routes corroborate.

7.0.0.2 Compositional compiler correctness

Composing simulations across passes and languages is a rich line: Compositional CompCert [14], parametric inter-language simulations [15], CompCertO’s simulation conventions [16], certified abstraction layers [17], multi-language semantics [18], [19], and DimSum’s decentralized multi-language graph with wrappers [20]. These works confront vertical composition of simulations up to differing observations — the habitat of our support condition, which in their terms is the congruence/well-definedness requirement on the mediating map; CompCert sidesteps it by fixing one global event type, CompCertO negotiates it through simulation conventions, DimSum through wrappers. We claim no mathematical novelty for the condition (6 is a one-line congruence); what this paper adds relative to that line is a different regime and different bookkeeping: edges that are not uniformly proved, trace-equality squares that are decidable per run rather than proved once, an explicit syntactic keep/loss computation for routes, and the grade/class algebra for composing heterogeneous evidence — with the trade-off stated plainly, since equality-up-to-projection is the right notion only for near-structure-preserving translations, not optimizing compilation (§3.1).

7.0.0.3 Semantics-first frameworks

The K framework derives interpreters, symbolic executors, and provers from one semantics [21], with KEVM [22] and KWasm as flagship instances; Sail does the same for ISAs [23], and ISA-conformance frameworks such as riscv-formal [24] prefigure the spec-enumerated per-construct yardsticks of 8. These are our closest philosophical relatives, and our platform consumes their artifacts (the Sail RISC-V and Arm models anchor one of each ISA’s two routes). The difference is what carries trust: a semantics-first framework is a monoculture — every derived tool inherits the one semantics and the one derivation pipeline — whereas our unit of trust is agreement between independently derived translations (2), with the framework structured so routes diverge over independent semantic artifacts. N-version programming [25] and differential testing [26], [27] exploit the same independence resource — and Knight and Leveson’s experiment [8] is the standing caution that independence must be argued, not assumed, which is why 2 is explicit, scoped to the diverse prefix, and confronted with our own common-mode incidents (§6.6). We give the possibilistic account of what agreement does and does not establish (2) and wire it into a compositional calculus rather than a test harness.

7.0.0.4 Certificates, witnesses, and certifying algorithms

Proof-carrying code [28], certifying algorithms [29], certified model-checking [30]–[32], and checked solver proofs (DRAT [33], verified checkers [34], Alethe/Carcara [35]) all instantiate the producer/checker split our \(\mathtt{proved}\) grade requires; SV-COMP’s violation/correctness-witness ecosystem [36] is the deployed, cross-tool form of the existential/universal asymmetry our end-to-end theorems state; Sledgehammer’s checked reconstruction [37] is the same untrusted-discovery/trusted-replay split inside a proof assistant; and SMT-COMP’s model-validation tracks [38] institutionalize witness re-checking at the solver level. What we add is the composition through a translation graph: an existential answer’s certificate is its source-level replay after carry-back (3), while universal answers compose certificate checking with route fidelity (4). The carry-back itself has verified precedent — decompilation into logic [39] makes the lifter a proved component — and our contribution is making it a mandatory, per-pair component of every edge rather than a per-tool artifact.

7.0.0.5 Moving programs to answerable representations

Verified lifting [40] and the broad practice of encoding programs into solver logics (BMC, symbolic execution) motivate the platform’s existence; Why3 [41] is the closest deployed relative of the hub pattern — one verification-condition language translated to many provers of heterogeneous trust — though its edges carry no per-run squares and no declared loss; refinement stacks such as seL4’s [11], [42] show multi-layer semantic preservation with uniform, proof-backed layers. Our setting differs in admitting layers that are not uniformly proved — pinned compilers, agent-written translators, third-party models — and making their heterogeneous trust first-class rather than a threat to the statement. Combining heterogeneous verification evidence with recorded provenance is itself prefigured by the Evidential Tool Bus [43]; the grade/class algebra and the ledger are a formalized cousin.

7.0.0.6 Fault tolerance, end to end

The paper’s vocabulary is deliberately that of fault-tolerant systems, because the concepts coincide: the square oracle is an acceptance test in the recovery-block sense [6], making a silently wrong — in effect Byzantine — translator fail-stop [7]; a branch is dual modular redundancy whose comparator localizes rather than votes; and the existential/universal asymmetry is the end-to-end argument [9] for translation graphs. What the transplant adds is the compositional bookkeeping — graded evidence with weakest-link meets, per-run re-establishment, and the trusted-base ledger.

7.0.0.7 LLMs and formal tools

Recent systems couple LLM generation with solver-checked validation [44]. Our platform is built for that player — an LLM chooses questions and routes but every step it takes is deterministic, graded, and checked — and §5.4 reports the build half of the two-directional experiment of 1: the translators themselves were LLM-written, and correctness was carried by the architecture, not by author trust. §6.8 reports a first controlled experiment on the player half.

8 Limitations and conclusion↩︎

8.0.0.1 Limitations

This is a dated snapshot of a system designed to ratchet, and its numbers say so: coverage is deepest on the spine (all 96 RV64IMC constructs conjoined and composing losslessly to SMT-LIB on both routes; the in-scope eBPF set complete) and deliberately partial elsewhere (EVM at 86 of 144 opcodes; Wasm at 54 of its 75-item declared inventory, without loop/br; Python an integer subset with bounded unrolling). Coverage is now measured as 8’s actual conjunction over language-owned inventories wherever a pair has a decidable square (§6.1); the predicted-grade hops still discharge faithfulness per run rather than per construct, and the A64 inventory, while language-owned, is a declared slice of a much larger ISA. Universal answers are bounded claims wherever BMC-style unrolling caps apply, and rest on \(\mathsf{universal}\)-tier hypotheses that per-run evidence and §4.7’s tested surrogates corroborate but do not entail (4). The verified portion of the C spine begins at the compiled binary: the compiler hop has no square and contributes reproducibility plus a differential, not faithfulness (§4.2). The \(\mathtt{proved}\)tier’s certified row is inhabited with a formally verified checker at the anchor (cake_lpr, §6.5), on one trivial and one certificate-scale instance (an 11.8 MB LRAT); the residual \(\mathsf{TCB}\)is the bit-blaster’s BV\(\to\)CNF step, and a certified claim is per-question and bounded, never a proof of a pair. Interpreter adequacy remains an assumption discharged empirically at modest volume, and the diversity assumption behind branch corroboration is structural, not probabilistic — scoped to the diverse prefix, a boundary the common-mode round (§6.7) now measures directly: shared misreadings blind, by construction, every gate built from the shared reading; only an independently derived external anchor catches them. The compositional core of the calculus — including the \(n\)-ary route telescope and the specialization obligation of 4 — is mechanized in Lean 4 with a clean axiom audit (§4.7); the fieldwise loss computation and the retiming case remain paper-stated.

8.0.0.2 Future work

The gaps above are the roadmap: scale the compliance-derived benchmark of §6.3 to an upstream suite taken binary-for-binary (which needs the machine-mode slice) and to SV-COMP-style C tasks; extend the escape-rate experiments of §6.7 beyond one translator’s emission space; widen the A64 slice toward the base ISA; and scale the player experiment of §6.8 to questions hard enough that unaided reasoning measurably fails, with subject models outside the builders’ family. Past these measured gaps lies the intended trajectory: hurdy-gurdyis meant to evolve into an open platform that scales in language support, where anyone — working with LLMs, with agents, or by hand — develops a new pair against the calculus’s written contract and lands it in the repository through an ordinary pull request. The admission bar is the architecture, not the author: a pair arrives with its declared projection and grade, its typed partiality, and a square the harness runs on merge, and the ratchet ([prop:ratchet]) keeps every prior verdict standing as the graph grows.

8.0.0.3 Conclusion

We proposed treating translations the way distributed systems treat processes: as components that fail, whose failures are contained by architecture — declared projections, decidable squares, graded evidence, independent routes, carried-back witnesses — rather than prevented by universal proof. The calculus makes the composition of partial trust exact; the platform shows the discipline is buildable, by agents, at measured (if modest) coverage; and the asymmetry theorems say where proof effort actually buys assurance. The snapshot is the baseline; the ratchet is the roadmap.

9 Proofs↩︎

9.1 Pasting (Theorem 3.7)↩︎

We spell out the chain, including the domain side conditions elided in the paper’s proof sketch. Let \(p \in \mathsf{dom}(P_2 \circ P_1)\), i.e. \(p \in \mathsf{dom}(I_A) \cap \mathsf{dom}(T_1)\), \(q := T_1(p) \in \mathsf{dom}(T_2)\), \(r := T_2(q)\), \(I_C(r)\) defined, \(\Lambda_2(I_C(r)) \in \mathsf{dom}(\Lambda_1)\), and (from \(p \in \mathsf{dom}(P_1)\), \(q \in \mathsf{dom}(P_2)\)) \(I_B(q)\) defined with \(I_B(q) \in \mathsf{dom}(\Lambda_1)\) and \(I_C(r) \in \mathsf{dom}(\Lambda_2)\).

1. By faithfulness of \(P_1\) at \(p\) and \(\pi\subseteq \pi_1\), \(\pi(I_A(p)) = \pi(\Lambda_1(I_B(q)))\).

2. By faithfulness of \(P_2\) at \(q\): \(\pi_2(I_B(q)) = \pi_2(\Lambda_2(I_C(r)))\).

3. Both \(I_B(q)\) and \(\Lambda_2(I_C(r))\) lie in \(\mathsf{dom}(\Lambda_1)\) (the first by \(p \in \mathsf{dom}(P_1)\), the second by \(p \in \mathsf{dom}(P_2 \circ P_1)\)). By \((\pi_2 \Rightarrow \pi)\)-support applied to step (2): \(\pi(\Lambda_1(I_B(q))) = \pi(\Lambda_1(\Lambda_2(I_C(r))))\).

4. Chaining (1) and (3): \(\pi(I_A(p)) = \pi(\Lambda_1(\Lambda_2(I_C(r))))\), which is faithfulness of \(P_2 \circ P_1\) at \(p\) w.r.t.\(\pi\). 0◻

Necessity of support. Without the support condition (Definition 3.6) the theorem is false: let \(F_B = \{g, h\}\), \(\pi_2 = \{g\}\), and let \(\Lambda_1\) copy field \(h\) into a \(\pi_1\)-kept source field. Take \(P_2\) faithful (it preserves \(g\)) but with \(\Lambda_2(I_C(r))\) differing from \(I_B(q)\) on \(h\) — permitted, since \(h \notin \pi_2\). The outer rectangle then disagrees on the copied field although both inner squares commute.

9.2 Composed keep-set, and step granularity↩︎

For fieldwise, step-aligned \(\Lambda_1\) (each kept source field \(f\) computed per step as \(f = \phi_f(\{\,b.g \mid g \in \mathit{deps}(f)\,\})\)), \((\pi_2 \Rightarrow \pi)\)-support holds iff \(\mathit{deps}(f) \subseteq \pi_2\) for every \(f \in \pi\); hence the largest admissible \(\pi\) is \(\mathsf{keep}= \{ f \in \pi_1 \mid \mathit{deps}(f) \subseteq \pi_2 \}\) and support for it is checkable syntactically from the dependency sets.

When \(\Lambda_1\) retimes — one source step corresponds to a window of target steps, as in C statements over ISA instructions — model \(\Lambda_1\) as a monotone window map \(w\) from source step indices to intervals of target step indices plus a fieldwise read within each window. Support then requires \(\mathit{deps}(f) \subseteq \pi_2\) for reads anywhere in the window, and additionally that the window map itself be determined by \(\pi_2\)-observables (e.g.by a kept program counter), since window boundaries influence the projected output. Both conditions are again syntactic given \(w\) and the dependency sets.

9.3 Localization (Corollary 3.8)↩︎

Contrapositive of the pasting theorem (Theorem 3.7) for two hops. For \(n\) hops, induct on the route: if the outer rectangle over hops \(1..n\) fails at \(p\) but hop \(1\)’s square passes at \(p\), then by the two-hop case applied to (hop 1, rectangle over hops \(2..n\)) the rectangle over \(2..n\) fails at \(T_1(p)\); recurse. Termination yields a least failing hop \(i\); within it, the square oracle’s comparison yields the least failing step and a witnessing field. 0◻

9.4 Weakest link (Proposition 4.2)↩︎

Soundness: if every hop is \(\mathsf{universal}\) on its fragment, iterate the pasting theorem (Theorem 3.7) over all \(p\) in the composite fragment. If some hop is \(\mathsf{perrun}\), the same iteration is available exactly at programs whose per-hop images passed the oracle — the per-run set of the route. If some hop is only \(\mathsf{replay}\), purity composes (Proposition 3.9) but no faithfulness statement is available for the route beyond it. Optimality: a route with a \(\mathsf{perrun}\) hop entails no universal statement (take a defect outside the checked set); a route with a \(\mathsf{replay}\) hop entails no faithfulness at all (take a pure but wrong translator). 0◻

9.5 Ratchet (Proposition 4.7)↩︎

Let \(I' \sqsupseteq I\) and let \(p \in \mathsf{dom}(I)\). Every quantity in the faithfulness square (Definition 3.5) evaluated at \(p\) reads only \(I\)-values on \(\mathsf{dom}(I)\)-points, which \(I'\) preserves; hence the verdict at \(p\) is unchanged. Coverage monotonicity: \(\mathsf{cov}\)’s per-construct conjunction can only gain (new constructs enter \(\mathsf{dom}\)) and never lose (old verdicts preserved). Composition of extensions is an extension. For the failure half: a non-extension update changes some \(I(p)\), which can flip the verdict at \(p\) for any pair whose square consumed it — justifying the versioned-event rule. 0◻

10 Construct inventories and probe corpora↩︎

Per-language construct inventories (the yardsticks of the paper’s Definition 4.6) and the probe corpora behind every coverage figure in the paper’s §6 are enumerated in the artifact — the per-language inventory modules (gurdy/languages/*/inventory.py), the per-pair inventories (gurdy/pairs/*/inventory.py), and the measured coverage data (paper/results/data/); they are spec-derived: the RISC-V RV64IMC opcode inventory, the full 144-opcode EVM inventory, the 126-construct eBPF inventory slice (drawn from the 256-opcode space), the Wasm numeric/parametric/control inventory, the OpenSMILES construct list, the Python-subset AST allow-list, and the two hubs’ operator inventories.

References↩︎