Pith. sign in

REVIEW 3 major objections 5 minor 53 references

The paper argues that answers which carry a witness are self-certifying by source replay, so trust shrinks to a single interpreter, while 'no' answers must buy assurance from graded hops, independent routes, and certificates.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-02 07:33 UTC pith:IKMHDRDX

load-bearing objection A genuinely novel and unusually honest paper on composing translation trust, with a machine-checked calculus core; its main soft spot is the empirically discharged interpreter-adequacy assumption that Theorem 3.17 reduces everything to. the 3 major comments →

arxiv 2607.14137 v2 pith:IKMHDRDX submitted 2026-07-10 cs.PL cs.AIcs.LOcs.SE

Untrusted Authors, Trusted Answers: A Calculus of Fidelity-Graded Translations

Christoph Kirsch This is my paper
classification cs.PL cs.AIcs.LOcs.SE
keywords fidelity-graded translationstranslation validationwitness replaycommuting squaretrusted computing baseweakest-link contractLLM-generated codereachability analysis
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper proposes treating every program translation — a compiler, a lowering into a solver's logic — as an untrusted component, and provides a calculus for composing what each translation actually guarantees. Its organizing claim is an asymmetry: when a query returns a witness-carrying answer (a counterexample, a model, a trace), carrying that witness back through the reverse translations and replaying it in the source interpreter makes the answer self-certifying, leaving only the interpreter itself in the trusted base. 'No' answers — unreachable, unsatisfiable — get no such shortcut; they must earn their way through graded fidelity classes, agreement between independently derived routes, and re-checked certificates. The paper proves that a route's guarantee is the weakest of its hops on every axis at once, that per-run square checks can temporarily re-establish a hop's fidelity, and that the whole compositional core is machine-checked in a proof assistant. It then measures a working platform of 13 languages and 15 registered pairs whose translators were written by LLM agents, with the architecture's checks as the only semantic gate — catching, among other things, defects in its own instruments.

Core claim

The paper's discovery: translation trust can be manufactured by architecture, not by trusting authors. Each translation is a 'pair' — translator, shared interpreters, and a target-to-source carry-back re-expressing target behaviors in source vocabulary — closing a directional square decidable per program on declared observables, with failures localizing to a hop, a step, and a named field. The central theorem: an existential answer is self-certifying, since replaying the carried-back witness at the source turns every translator and solver into a discovery device that can lose the witness but never fake it, while a universal answer needs every hop faithful, branch corroboration, and certified

What carries the argument

The central object is the 'pair': a translator between two languages plus a target-to-source interpreter (carry-back) that re-expresses target behaviors in source vocabulary, closing a directional commuting square checked per program on declared observables. Two theorems carry the argument — existential answers are self-certifying by source replay (trust collapses to interpreter adequacy); universal answers need faithful hops, corroboration across independent branches, and certified verdicts. Trust composes as the componentwise meet of contracts — assurance class, direction, kept observables, cost — so a route is as faithful as its weakest hop, with per-run re-establishment and branch agreem

Load-bearing premise

Everything rests on interpreter adequacy — that each language's interpreter really computes the language's reference semantics — which is discharged by differential testing at modest volume and, for Python, is circular because the pinned runtime is both the semantics and the interpreter; if it fails on any covered program, even a perfectly replayed witness can be wrong.

What would settle it

Run the reachability route on a covered RISC-V program, replay the carried-back witness in the source interpreter, and compare the exhibited behavior against an independently derived ISA reference simulator on the same inputs: a divergence would show interpreter adequacy fails and self-certification collapses for that fragment. Symmetrically, an 'unreachable' verdict that a formally verified certificate checker has re-validated, but which a later, different engine shows reachable, would falsify the universal half.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • Witness-carrying answers (counterexamples, models, traces) can be made nearly free of trust: replay at the source interpreter reduces the user's trusted base to interpreter adequacy, so no translator, hub, or solver needs to be believed for the verdict to stand.
  • Universal answers (unreachable, unsatisfiable) are exactly where assurance budgets belong: the route's guarantee is its weakest hop on every axis at once, so one unverified hop caps the whole chain no matter how strong the rest.
  • Per-run square checks can temporarily re-establish a weak hop's fidelity: a reproducible or ungraded translator that passes the per-program oracle contributes, for that run, exactly what a checked hop contributes.
  • Agreement between independently derived routes leaves only common-mode failure as the residual risk, and corroboration saturates at the finite supply of independent semantic anchors.
  • The ratchet guarantees that growing the translation graph never silently invalidates prior verdicts: additive extensions preserve all earlier evidence, so coverage and trust only accumulate.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • My reading, beyond the paper: the existential/universal asymmetry is a general engineering rule — whenever a toolchain can emit a checkable artifact, push final verification to the consumer's endpoint and treat every intermediate stage as a discovery device; reserve weakest-link graded guarantees for conclusions that cannot carry artifacts.
  • The weakest-link contract algebra transfers to the broader question of trusting LLM-generated code: generative pipelines should expose per-hop fidelity declarations, and replayable evidence rather than generator reputation should carry conviction.
  • A testable extension the authors leave implicit: carry certificate replay to the source level for universal verdicts, so that 'unreachable' claims undergo the same endpoint re-check that reachability enjoys — a source-level certificate checker would shrink the universal trusted base as dramatically as replay shrinks the existential one.
  • The platform's own history — a checker adapter that accepted every outcome until a negative control ran — suggests every automated check in such a pipeline needs its own positive and negative controls; auditing the instruments may matter as much as the instruments.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper proposes a calculus for composing program-translation steps of heterogeneous trustworthiness. A pair consists of a translator, shared interpreters, a projection, a declared direction, and a carry-back interpreter; faithfulness is a per-program decidable commuting-square check. Squares paste under a support condition, and a route's contract is the componentwise meet of its hops' contracts (assurance class, direction, kept observables, cost). Two end-to-end theorems organize the trust story: existential answers are self-certifying by source-level replay (Theorem 3.17), while universal answers require route fidelity, certificates, and specialization hypotheses (Theorem 3.18). The system hurdy-gurdy implements the calculus with LLM-built pairs, demand-driven graph growth, a ratchet, and a substantial evaluation snapshot, including machine-checked Lean 4 proofs of the compositional core.

Significance. If the advertised claims hold, this is a valuable contribution: it turns translation validation into a compositional graph calculus with decidable per-run checks, explicit loss/assurance bookkeeping, and a principled account of when independent routes corroborate one another. The Lean 4 mechanization with a clean axiom audit, the reproducible evaluation scripts, the negative controls, the mutation-based escape-rate experiments, and the unusually candid incident catalog are all genuine strengths. The central logical core — pasting, localization, the contract meet, per-run re-establishment, and the replay-based existential theorem — is sound given its stated hypotheses. The main weakness is that the most important trust-reduction claim rests on an empirical adequacy assumption that the paper itself shows can fail in practice, and the paper's headline language is stronger than what the evidence establishes.

major comments (3)
  1. [§3.7 / §3.1 / §6.6] Theorem 3.17 reduces the trusted base of existential verdicts to Assumption 1 (interpreter adequacy) plus a small replay harness. The paper is explicit that Assumption 1 is not proved and is discharged empirically 'at modest volume' (§4.2). Section 6.6 then documents a concrete failure of that very assumption: the RISC-V interpreter and the riscv-btor2 translator both mis-decoded MUL as ADD, so every square, branch agreement, and the derived benchmark agreed on the wrong semantics, and only manual audit found the defect. This is not a blemish in the proof but a puncture in the trust-reduction claim: a replayed witness for such a program can produce a false 'reachable' verdict, and the architecture's gates are structurally blind to the failure. The Python case (§4.2) is even weaker: the pinned runtime is both the semantics and the interpreter, making adequacy vacuous. The central asymmetr
  2. [§3.8 / Table 2 / Theorem 3.18] The universal half of the asymmetry is mechanized only in conditional form: clauses (iii) and (iv) of Theorem 3.18 enter the Lean statement as hypotheses, and the paper's tested surrogates are sampled commutation checks and per-verdict re-execution. The text correctly says 'sampling corroborates, it does not entail.' That epistemic language should be carried into the paper's summary claims about universal answers. The abstract's statement that universal answers are 'where grades, independent branches, and re-checked certificates earn their cost' is a design principle, not a theorem; the theorem itself is a conditional. I recommend making this conditional status prominent wherever Section 6 reports unreachable verdicts, and adding a per-row pointer to which hypotheses (i)–(iv) were actually discharged for each reported universal verdict. Currently Tables 4 and 5 report unreachable verdict
  3. [§4.2 / §6.3 / Assumption 1] The empirical discharge of Assumption 1 is too thin for the load it carries. The main differential evidence is 300 seeded RV64IMC programs against the Sail simulator, a 10-seed Csmith run, and 463 reference cases (§6.6), while the largest derived benchmark is 78 questions over 10 programs (§6.3). The 78-question benchmark's ground truth is produced by the very interpreter whose adequacy is at issue; the external Sail differential is separate, but it runs at modest volume and the paper's own history shows it missed the MUL/ADD fault until a human audit. I am not asking for SV-COMP scale, but for a quantitative adequacy campaign with construct-level coverage targets, mixed-sign and non-zero operands, and mutation-survival thresholds, so that the reader can see what 'adequacy' is being claimed. Without this, Theorem 3.17's trusted base remains an article of faith rather than a measured engi
minor comments (5)
  1. [§3.2, Definition 3.4] The phrase 'pure (as in Theorem 3.2)' should refer to Definition 3.2; purity is defined there, not as a theorem.
  2. [§2 and §5.2] The ratchet is introduced as 'Theorem 5.2' in §2 but is stated as Proposition 5.2 in §5.2. Please normalize the numbering.
  3. [Figure 7] The figure's gate-stack labels are confusing: 51 killed, 0 killed, 4 killed, followed by '4 survive' and then 'escaped: 0'. The final survivor count should read 0 after the derived-benchmark gate; the current label seems to show the intermediate survivor count twice.
  4. [Table 3] The 'per-run' entries for predicted-grade hops are not conjoined coverage in the same sense as the other rows. Consider splitting the table or using a separate marker so the reader is not misled into comparing '96/96' with 'per-run' as if they were the same measurement.
  5. [§6.3] The compliance slice is a derived benchmark rather than upstream binaries taken verbatim; the paper says this plainly in the honesty notes, but the first sentence of §6.3 could state 'derived from riscv-tests under a re-created grading convention' even more prominently to avoid any impression that the upstream binaries were run unchanged.

Circularity Check

2 steps flagged

Core calculus is non-circular; two admitted by-construction cases (Python interpreter adequacy, LLM-player grading) keep the score at 3.

specific steps
  1. self definitional [§4.2 'Languages and reasoning hubs' (and §3.1, Assumption 1)]
    "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"

    For Python, the reference semantics ⟦·⟧_A is defined as the behavior of the pinned CPython runtime, and the interpreter I_A is the same runtime under an AST allow-list. Assumption 1 (I_A(p)=⟦p⟧_A on dom(I_A)) therefore holds by definition, not by empirical discharge. Since Theorem 3.17 reduces the trusted base for existential answers to exactly Assumption 1, the 'self-certifying' replay for Python reduces to the interpreter agreeing with itself: no independent check can fail. The paper explicitly calls this a circularity; it is a boundary case of the platform rather than of the calculus theorems, which take adequacy as an explicit hypothesis.

  2. other [§6.8 'The other direction: an LLM plays the platform' (limitations paragraph)]
    "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"

    The player experiment's headline result (both arms 12/12, and v2 arm B 8/8) is an evaluation claim, and its correctness criterion is ground truth established by the same platform through which arm B must answer. Success in arm B is therefore partly guaranteed by construction: the experiment measures whether the LLM can operate the platform's tools, not whether the platform's verdicts are independently correct. The paper discloses this limitation, and it affects the empirical player-ability claim rather than the formal derivation chain.

full rationale

The paper's load-bearing derivation — the directional square, pasting with the support condition, composition by componentwise meet, the existential/universal asymmetry (Theorems 3.7, 3.13, 3.14, 3.17, 3.18) — is not circular. Each theorem is stated with explicit hypotheses and mechanically checked in Lean; Theorem 3.17's proof is literally a three-token consequence of interpreter adequacy and the observed replay, so its trusted base is transparently Assumption 1. Assumption 1 is an assumption, not a derived result, and its empirical discharge against external oracles (Sail, riscv-tests, CBMC) is independent support; the MUL/ADD blind spot is a limitation of that empirical discharge, not a circular derivation. The two genuine by-construction cases are the ones the paper itself names: Python interpreter adequacy ('the pinned runtime is both the semantics and the interpreter') and the LLM-player grading ('ground truth is platform-established and arm B answers via the platform'). Both are openly disclosed, both affect specific platform/evaluation claims rather than the central calculus, and neither is disguised as an independent result. Accordingly the score is 3: not a clean 0-2, because the paper contains admitted self-definitional instances, but far from 6+, because the central trust-collapse theorem and its composition machinery do not reduce to those instances.

Axiom & Free-Parameter Ledger

3 free parameters · 5 axioms · 3 invented entities

The formal calculus rests on explicit assumptions (interpreter adequacy, diversity, deterministic finite semantics, and specialization/solver-artifact correspondence) that the paper discloses rather than hides. The empirical measurements depend on hand-chosen bounds, construct inventories, and sampling sizes. The invented entities are architectural/formal constructs with the Lean mechanization and the artifact as independent evidence; none are physical postulates.

free parameters (3)
  • unrolling bound k (per question, chosen) = e.g., k=25, k=505, k=60, k=30
    Universal (unreachable) verdicts are bounded claims within k; the paper declares these per question (§3.7, §6.3, §6.9).
  • per-language construct inventories = RV64IMC 96; A64 slice 33; Wasm 75; EVM 144; eBPF 126; Python subset 27; CRN 10; SMILES 17; BTOR2 56
    Coverage denominators are chosen 'from its specification' but the slice boundaries (e.g., the A64 slice, Python subset) are hand-declared, and coverage scores are relative to them (§5.2, Table 3).
  • sampling size for specialization-commutation checks = undisclosed in the paper
    Theorem 3.18(iv) is discharged by 'sampled commutation tests per reasoning pair with free inputs'; the number of samples is not stated, so the surrogate's strength is unquantified (§3.8).
axioms (5)
  • domain assumption Assumption 1: I_A(p) = ⟦p⟧_A for all p in dom(I_A)
    Interpreter adequacy is the irreducible trusted-base residue; the replay of Theorem 3.17 reduces trust to it. Empirically discharged by differential testing; Python is admitted circular (§3.1, §4.2, §6.3).
  • domain assumption Assumption 2: corroborating routes share no translator or carry-back on the diverse prefix, derived from independent semantic artifacts
    Branch-agreement evidence (Lemma 3.16) only means something under this assumption; the paper marks it declared/protected but states residual common-mode failures are not excluded (§3.6, §6.6 MUL/ADD incident).
  • domain assumption Reference semantics are deterministic, finite-behavior functions; nondeterminism, divergence, and reactive I/O are outside scope
    Definition 3.1 restricts behaviors to finite sequences and the reference semantics to a function, which excludes many real languages (§3.1).
  • ad hoc to paper Theorem 3.18(iv): translation commutes with input specialization; and (iii): solver artifacts relate to target semantics
    Both enter the Lean statement as hypotheses; only sampled commutation tests and per-verdict interpreter replay are provided as surrogates (§3.8, §6.2-6.5).
  • domain assumption Declared grade/projection/direction are trusted inputs
    The paper notes grade declarations are themselves trusted inputs; only checked is mechanically enforced, and a predicted edge can be universally wrong (§3.5).
invented entities (3)
  • fidelity-graded translation pair (translator + interpreters + carry-back Λ + witness embedding W) independent evidence
    purpose: Unit of trust in the graph; turns every translation into a per-program checkable square.
    Formal construct, machine-checked in Lean and implemented in hurdy-gurdy; observable through the square oracle's failure reports (§3.2-3.4).
  • assurance classes A: none<replay<perrun<universal and grade set G independent evidence
    purpose: Basis for contract meet and weakest-link composition.
    Mechanized (Contract.comp_glb) and used by the route report; grades are declared, only checked is enforced (§3.5).
  • trusted-base ledger TCB(v) independent evidence
    purpose: Itemizes residual trust after each cross-check layer; makes the existential/universal asymmetry concrete.
    Implemented and instantiated in the certified tier, with the cake_lpr anchor; entries are checkable (§3.6, §6.5).

pith-pipeline@v1.3.0-alltime-deepseek · 41458 in / 16604 out tokens · 175734 ms · 2026-08-02T07:33:34.974616+00:00 · methodology

0 comments
read the original abstract

To answer a question about a program, move the program to where the question is decidable. Every such move is a translation, and every translation is a place to be wrong. We study translation as a graph -- many languages, a few reasoning targets, independently built routes of honestly different trustworthiness -- and give it a calculus: pairs of languages close commuting squares that are directional (exactness is the identity-embedding special case of over-approximation), checkable per program, and composable, a route's contract being the componentwise meet of its hops' contracts -- assurance class, direction, kept observables, measured cost. One asymmetry organizes trust: witness-carrying answers are self-certifying by replay at the source; universal answers are where grades, independent branches, and re-checked certificates earn their cost. The compositional core, lax telescope included, is mechanized in Lean 4. hurdy-gurdy implements the calculus as two planes meeting in one registry. The use plane reads declarations and produces evidence-carrying answers; its builders and its intended player are both LLMs, untrusted by construction. The evolution plane grows the graph: unmet questions are recorded as demand, pairs are recommended by evidence and registered by humans, and a ratchet keeps every prior verdict standing. Answers never write; growth never answers. Run indefinitely, the loop converges on every reducibly decidable question, at fidelity that only rises. We measure the July 2026 snapshot -- per-construct conjoined coverage, dual-route branch agreement for two ISAs, source-level witness replay, certified unreachability re-validated by a formally verified checker, escape rates for the gate itself -- and report the defects the architecture caught in its own authors' work.

Figures

Figures reproduced from arXiv: 2607.14137 by Christoph Kirsch.

Figure 1
Figure 1. Figure 1: The two planes, meeting in one data structure. The use plane reads the registry’s declarations and pro￾duces evidence-carrying answers; the evolution plane turns recorded demand into new declarations, gated and ratcheted, with registration a human act. Answers never write; growth never answers. or to validate each of its runs [19, 26, 30]. Both are statements about a single edge.1 This paper is about the g… view at source ↗
Figure 2
Figure 2. Figure 2: One run down the spine. The question travels C→RISC-V→BTOR2→SMT-LIB (RISC-V reaching BTOR2 twice, the manual-derived and Sail-derived branches whose agreement corroborates both); a sat model is carried back hop by hop and replayed in the source-side interpreter — the answer’s evidence, not the solver’s say-so (Theorem 3.17). universal transfer across over-approximation (Theo￾rem 3.11). • The contract algeb… view at source ↗
Figure 3
Figure 3. Figure 3: The registry: 13 languages (nodes; the two rea￾soning hubs shaded) and 15 registered pairs (edges), each carrying its declared grade. The two loops on the BTOR2 hub are the abstraction endo-pairs of the direction axis (§3.4): btor2-havoc, built, and — gray — btor2-interval, regis￾tered as a brief. The evaluation of Section 6 covers the thir￾teen pairs built at its snapshot. RISC-V and AArch64 each reach BT… view at source ↗
Figure 4
Figure 4. Figure 4: What the bottom block of [PITH_FULL_IMAGE:figures/full_fig_p015_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: The round trip every case study in [PITH_FULL_IMAGE:figures/full_fig_p016_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: The pipeline [PITH_FULL_IMAGE:figures/full_fig_p017_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: The escape-rate experiment ( [PITH_FULL_IMAGE:figures/full_fig_p019_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: The two-arm player protocol of [PITH_FULL_IMAGE:figures/full_fig_p020_8.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

53 extracted references · 1 linked inside Pith

  1. [1]

    Bruno Andreotti, Hanna Lachnitt, and Haniel Barbosa. 2023. Carcara: An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format. InTACAS

    2023

  2. [2]

    Gray, Robert M

    Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Was- sell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Kr- ishnaswami, and Peter Sewell. 2019. ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS.Proceedings of the ACM on Programming Languages3, POPL (2019), 71:1–71:31

    2019

  3. [3]

    Algirdas Avižienis. 1985. The N-Version Approach to Fault-Tolerant Software.IEEE Transactions on Software EngineeringSE-11, 12 (1985), 1491–1501

    1985

  4. [4]

    Dirk Beyer, Matthias Dangl, Daniel Dietsch, Matthias Heizmann, and Andreas Stahlbauer. 2015. Witness Validation and Stepwise Testifica- tion across Software Verifiers. InESEC/FSE

    2015

  5. [5]

    Paul- son

    Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paul- son. 2013. Extending Sledgehammer with SMT Solvers.Journal of Automated Reasoning51, 1 (2013), 109–128

    2013

  6. [6]

    Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith

    Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2000. Counterexample-Guided Abstraction Refinement. InCA V (LNCS, Vol. 1855). 154–169

    2000

  7. [7]

    Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. InPOPL. 238–252

    1977

  8. [8]

    Jean-Christophe Filliâtre and Andrei Paskevich. 2013. Why3 — Where Programs Meet Provers. InESOP

    2013

  9. [9]

    Ronghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, and Yu Guo. 2015. Deep Specifications and Certified Abstraction Layers. In POPL

    2015

  10. [10]

    Everett Hildenbrandt, Manasvi Saxena, Nishant Rodrigues, Xiaoran Zhu, Philip Daian, Dwight Guth, Brandon Moore, Daejun Park, Yi Zhang, Andrei Stefanescu, and Grigore Roşu. 2018. KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine. InCSF

    2018

  11. [11]

    Shoaib Kamil, Alvin Cheung, Shachar Itzhaky, and Armando Solar- Lezama. 2016. Verified Lifting of Stencil Computations. InPLDI

    2016

  12. [12]

    Christoph M. Kirsch. 2017. Selfie and the Basics. InOnward!

    2017

  13. [13]

    Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009. seL4: Formal Verification of an OS Kernel. In SOSP

    2009

  14. [14]

    Knight and Nancy G

    John C. Knight and Nancy G. Leveson. 1986. An Experimental Evalua- tion of the Assumption of Independence in Multiversion Programming. IEEE Transactions on Software EngineeringSE-12, 1 (1986), 96–109

    1986

  15. [15]

    Jérémie Koenig and Zhong Shao. 2021. CompCertO: Compiling Certi- fied Open C Components. InPLDI

    2021

  16. [16]

    Myreen, Michael Norrish, and Scott Owens

    Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens

  17. [17]

    Robert P. Kurshan. 1994.Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press

    1994

  18. [18]

    Xavier Leroy. 2009. Formal Verification of a Realistic Compiler.Com- mun. ACM52, 7 (2009), 107–115

    2009

  19. [19]

    Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, and John Regehr

    Nuno P. Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, and John Regehr. 2021. Alive2: Bounded Translation Validation for LLVM. InPLDI

    2021

  20. [20]

    Jacob Matthews and Robert Bruce Findler. 2007. Operational Semantics for Multi-language Programs. InPOPL

    2007

  21. [21]

    McConnell, Kurt Mehlhorn, Stefan Näher, and Pascal Schweitzer

    Ross M. McConnell, Kurt Mehlhorn, Stefan Näher, and Pascal Schweitzer. 2011. Certifying Algorithms.Computer Science Review5, 2 (2011), 119–161

    2011

  22. [22]

    McKeeman

    William M. McKeeman. 1998. Differential Testing for Software.Digital Technical Journal10, 1 (1998), 100–107

    1998

  23. [23]

    Myreen, Michael J

    Magnus O. Myreen, Michael J. C. Gordon, and Konrad Slind. 2008. Machine-Code Verification for Multiple Architectures: An Application of Decompilation into Logic. InFMCAD

    2008

  24. [24]

    Namjoshi

    Kedar S. Namjoshi. 2001. Certifying Model Checkers. InCA V

    2001

  25. [25]

    George C. Necula. 1997. Proof-Carrying Code. InPOPL

    1997

  26. [26]

    George C. Necula. 2000. Translation Validation for an Optimizing Compiler. InPLDI. 27 Christoph Kirsch

    2000

  27. [27]

    Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, and Viktor Vafeiadis. 2015. Pilsner: A Compositionally Verified Compiler for a Higher-Order Imperative Language. InICFP

    2015

  28. [28]

    Aina Niemetz, Mathias Preiner, Clifford Wolf, and Armin Biere. 2018. Btor2, BtorMC and Boolector 3.0. InCA V

    2018

  29. [29]

    Perconti and Amal Ahmed

    James T. Perconti and Amal Ahmed. 2014. Verifying an Open Compiler Using Multi-language Semantics. InESOP

    2014

  30. [30]

    Amir Pnueli, Michael Siegel, and Eli Singerman. 1998. Translation Validation. InTACAS

    1998

  31. [31]

    Brian Randell. 1975. System Structure for Software Fault Tolerance. IEEE Transactions on Software EngineeringSE-1, 2 (1975), 220–232

    1975

  32. [32]

    1999.Credible Compilation

    Martin Rinard and Darko Marinov. 1999.Credible Compilation. Tech- nical Report MIT-LCS-TR-776. MIT Laboratory for Computer Science

    1999

  33. [33]

    Grigore Roşu and Traian Florin Şerbănuţă. 2010. An Overview of the K Semantic Framework.Journal of Logic and Algebraic Programming 79, 6 (2010), 397–434

    2010

  34. [34]

    John Rushby. 2005. An Evidential Tool Bus. InICFEM

    2005

  35. [35]

    Saltzer, David P

    Jerome H. Saltzer, David P. Reed, and David D. Clark. 1984. End-to-End Arguments in System Design.ACM Transactions on Computer Systems 2, 4 (1984), 277–288

    1984

  36. [36]

    Michael Sammler, Simon Spies, Youngju Song, Emanuele D’Osualdo, Robbert Krebbers, Deepak Garg, and Derek Dreyer. 2023. DimSum: A Decentralized Approach to Multi-language Semantics and Verification. Proceedings of the ACM on Programming Languages7, POPL (2023)

    2023

  37. [37]

    Schlichting and Fred B

    Richard D. Schlichting and Fred B. Schneider. 1983. Fail-Stop Proces- sors: An Approach to Designing Fault-Tolerant Computing Systems. ACM Transactions on Computer Systems1, 3 (1983), 222–238

    1983

  38. [38]

    Myreen, and Gerwin Klein

    Thomas Arthur Leck Sewell, Magnus O. Myreen, and Gerwin Klein

  39. [39]

    Gordon Stewart, Lennart Beringer, Santiago Cuellar, and Andrew W. Appel. 2015. Compositional CompCert. InPOPL

    2015

  40. [40]

    Chuyue Sun, Ying Sheng, Oded Padon, and Clark Barrett. 2024. Clover: Closed-Loop Verifiable Code Generation.arXiv preprint arXiv:2310.17807(2024)

    Pith/arXiv arXiv 2024

  41. [41]

    Yong Kiam Tan, Marijn J. H. Heule, and Magnus O. Myreen. 2021. cake_lpr: Verified Propagation Redundancy Checking in CakeML. In TACAS

    2021

  42. [42]

    Jean-Baptiste Tristan and Xavier Leroy. 2008. Formal Verification of Translation Validators: A Case Study on Instruction Scheduling Optimizations. InPOPL

    2008

  43. [43]

    Tjark Weber, Sylvain Conchon, David Déharbe, Matthias Heizmann, Aina Niemetz, and Giles Reger. 2019. The SMT Competition 2015– 2018.Journal on Satisfiability, Boolean Modeling and Computation11, 1 (2019), 221–259

    2019

  44. [44]

    Nathan Wetzler, Marijn J. H. Heule, and Warren A. Hunt Jr. 2014. DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs. InSAT

    2014

  45. [45]

    Claire Wolf. 2019. riscv-formal: A Framework for RISC-V Formal Verification.https://github.com/YosysHQ/riscv-formal

    2019

  46. [46]

    Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. 2011. Finding and Understanding Bugs in C Compilers. InPLDI

    2011

  47. [47]

    Emily Yu, Armin Biere, and Keijo Heljanko. 2021. Progress in Certify- ing Hardware Model Checking Results. InCA V. A Proofs A.1 Pasting (Theorem 3.7) We spell out the chain, including the domain side conditions elided in the paper’s proof sketch. Let 𝑝∈dom(𝑃 2◦𝑃 1), i.e.𝑝∈dom(𝐼 𝐴)∩dom(𝑇 1),𝑞 :=𝑇 1(𝑝) ∈dom(𝑇 2),𝑟 := 𝑇2(𝑞),𝐼𝐶(𝑟) defined, Λ2(𝐼𝐶(𝑟))∈dom(Λ 1),...

    2021

  48. [50]

    By faithfulness of 𝑃1 at𝑝 and 𝜋⊆𝜋 1, 𝜋(𝐼𝐴(𝑝))= 𝜋(Λ 1(𝐼𝐵(𝑞)))

  49. [51]

    By faithfulness of𝑃 2 at𝑞:𝜋 2(𝐼𝐵(𝑞))=𝜋 2(Λ2(𝐼𝐶(𝑟)))

  50. [52]

    By (𝜋2⇒𝜋) -support applied to step (2):𝜋(Λ 1(𝐼𝐵(𝑞)))= 𝜋(Λ 1(Λ2(𝐼𝐶(𝑟))))

    Both𝐼𝐵(𝑞) and Λ2(𝐼𝐶(𝑟)) lie in dom(Λ 1) (the first by 𝑝∈dom(𝑃 1), the second by 𝑝∈dom(𝑃 2◦𝑃 1)). By (𝜋2⇒𝜋) -support applied to step (2):𝜋(Λ 1(𝐼𝐵(𝑞)))= 𝜋(Λ 1(Λ2(𝐼𝐶(𝑟))))

  51. [53]

    This form is machine-checked (lax_pasting; telescoped, DRoute

    Chaining (1) and (3): 𝜋(𝐼𝐴(𝑝))=𝜋(Λ 1(Λ2(𝐼𝐶(𝑟)))) , which is faithfulness of𝑃 2◦𝑃 1 at𝑝w.r.t.𝜋.□ Directional pairs.For pairs with a non-identity witness embedding (Theorem 3.4), the same four steps run per closing valuation, the three legs closed at 𝑥,𝑊1(𝑝,𝑥) , and 𝑊2(𝑇1(𝑝),𝑊 1(𝑝,𝑥)) ; the composite’s square is then faithful- ness along𝑊2◦𝑊 1, with directi...

  52. [2013]

    Translation Validation for a Verified OS Kernel. InPLDI

  53. [2014]

    CakeML: A Verified Implementation of ML. InPOPL