Pith. sign in

REVIEW 4 major objections 6 minor 89 references

Foundational Refinement Proofs for Deployed Bytecode, at the Price of Tokens

T0 review · 4 major / 6 minor · reviewed 2026-08-01 · deepseek-v4-flash

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

Pith's one-line read LLM agents produce machine-checked refinement proofs for deployed Ethereum bytecode.

desk verdict A genuinely new post-hoc foundational refinement framework for arbitrary EVM bytecode whose headline claim overruns the shipped evidence: the external-call rule makes the refinement certificate substantially weaker than 'proved correct', and the reported counts don't match the tables. read the letter →

arxiv 2607.26306 v1 pith:KTYWHZL7 submitted 2026-07-28 cs.PL

Lefteris Lazaropoulos , Zoe Paraskevopoulou This is my paper · ORCID
classification cs.PL
keywords refinementEVMLeanLLMtranslationvalidationproof-carryingcodesmartcontractsSol−
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper claims that foundational, machine-checked proofs relating deployed EVM bytecode to a high-level specification are no longer beyond reach: large language model agents can generate them at the price of tokens. The authors build EquiVM, a Lean framework with an executable EVM semantics and the Sol− specification language, and define a refinement relation covering every message call a contract can receive. They report that twenty-three real-world contracts, most of the MakerDAO stablecoin system among them, were proved end to end with minimal human guidance. If correct, each proof is a replayable certificate checked by the Lean kernel, independent of any compiler, and the trusted base shrinks to the semantics, the refinement statement, and a small set of per-contract facts.

What carries the argument

The argument rides on a refinement judgment between the EVM's code-execution function Ξ and a big-step judgment over Sol−, a small imperative specification language whose semantics is parametric in storage layout. Sol− deliberately gives meaning to external calls by invoking the EVM's own message-call function Θ on the live account map, so interaction with unknown bytecode is handled by the semantics rather than by a linking theorem. The proof side is a compositional library built around a reach invariant: a cursor exposing pc, stack, memory, return data, and world, with combinators for forward symbolic execution of the bytecode, so whole-contract proofs reduce to chaining per-opcode lemmas.

What would settle it

Recover the original Sol− specification for a contract whose agent was authorized to change it after a mismatch report (e.g., Flipper or Cure), and check whether the deployed bytecode refines that original; if it does not, the theorem only holds for the revised spec. Alternatively, re-run the official EVM conformance suite against the modified semantics and compare the pass rate to the 99.99% reported for the base model.

Watch

Extended reading notes

Core claim

The central claim is the runtime refinement theorem: for any protocol-conforming EVM state, calldata, gas, and substate, executing the deployed bytecode via Ξ either matches a run of the Sol− specification with the same created accounts, account maps up to representation, and return bytes; or reverts when the specification does not dispatch; or exhausts gas. The authors further claim this theorem was discharged by frontier LLM agents for twenty-three deployed contracts at up to a hundred million tokens and a hundred hours per contract, including most of MakerDAO, and conclude that foundational mechanized proofs can now be bought at the price of tokens.

Load-bearing premise

The proof only certifies what the Sol− specification says, so the load-bearing premise is that the specification was written before, not retrofitted after, the bytecode behavior was observed; a second fragile premise is that the modified EVM semantics still faithfully models the Cancun EVM.

Editorial extensions

If this is right

  • A verified contract comes with a replayable, independently checkable Lean certificate that does not name or rely on the compiler that produced the bytecode.
  • Auditors and analyzers can work from the Sol− specification rather than decompiled bytecode, for bytecode of any provenance.
  • Interoperation with arbitrary deployed code is part of the semantics, so compositional reasoning across contract boundaries does not require a linking theorem.
  • Verification frameworks can be architected around an untrusted LLM proof agent plus a trusted kernel, shifting cost from human labor to tokens.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The technique inherits the risk that a specification may be edited to match observed bytecode behavior; the paper's own appendix records such authorizations, so the durable guarantee is for the adjusted description, not necessarily the original intent.
  • Because Sol− models no gas, the refinement theorem allows vacuous equivalence on runs that exhaust gas; a natural extension is to add explicit gas bounds or upper-bound gas proofs.
  • The same per-artifact certification could transfer to other bytecode platforms with a formal semantics and a high-level spec language, not just the EVM.
  • A cheap test of the framework's validity is to re-run the official EVM conformance suite against the modified semantics; without that, a silent mismatch between the model and the Cancun EVM would invalidate all certificates.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

4 major / 6 minor

Summary. The paper introduces EquiVM, a Lean framework for proving that deployed EVM bytecode refines a high-level specification written in Sol−, a Solidity-like language with big-step semantics. The refinement theorem (Fig. 9) is stated against an executable EVM model extending Nethermind's EVMYulLean; the specification language handles external calls by invoking the same EVM message-call function Θ, and a proof library provides reach-invariant combinators for forward symbolic execution. An LLM agent is used to construct proofs, and the paper reports telemetry for exploratory examples and deployed MakerDAO, WETH9, and Nouns contracts. The claimed contribution is the first combination of foundational, replayable, per-artifact refinement proofs for arbitrary bytecode, including interaction with unknown code, at a cost dominated by LLM tokens.

Significance. If the claims are borne out, the paper would demonstrate a genuine shift: per-contract, compiler-independent, machine-checked equivalence certificates for deployed EVM bytecode, with the LLM agent untrusted because the Lean kernel checks the proof. The design of Sol−, especially the external-call boundary that reuses the EVM's own Θ, is elegant and avoids a linking theorem for unknown callees. The paper is unusually honest about costs, failures, and trusted components (native_decide axioms, opaque Keccak, underspecified gas). However, the headline strength is not supported by the current theorem: the existential gas in external-call rules makes the specification over-approximate to the point that always-revert bytecode refines any external-calling spec, and no artifact is provided to verify the empirical claims. The core idea is promising and the formal development appears substantial, but the main theorem as stated does not deliver the advertised correctness guarantee.

major comments (4)
  1. [§4.2, Fig. 7 (Θ-Call); §5, Fig. 9 (R-Exec)] The existential quantification over call gas g in Θ-Call gives every external-calling transition a spurious revert derivation: for any callee, choosing g below the intrinsic call cost makes Θ return z=false, so ExtCallFail allows the specification to revert on any input. Since R-Exec only requires the bytecode result to equal some Sol− derivation, a bytecode that reverts unconditionally on such a transition is refined by a specification that was written to succeed. Thus the end-to-end theorem for contracts with external calls does not establish that those transitions can ever complete their intended effects. Section 5.2's disclosure of underspecified gas is also weaker than this: the problem is not just absence of gas bounds, but that the spec itself contains unconditional failure paths. Please either make gas a tracked component of the Sol− state and force the two sides to use the same
  2. [§6, Tables 1-2; no artifact section] The paper claims replayable machine-checked certificates but provides no artifact: no repository, commit hash, build instructions, or list of Lean files. Tables 1 and 2 report proof line counts and check times, but without the development the reader cannot verify that the proofs exist, that they contain no `sorry`/axioms beyond those disclosed, or that the native_decide-generated axioms are benign. This is a hard requirement for a foundational-verification paper. Please make the full development available and pin the exact versions (Lean, mathlib, EVMYulLean, solc, bytecode hashes).
  3. [§1 Abstract and §8 Conclusion vs §6 Evaluation] The abstract and conclusion state that twenty-three real-world contracts were proved end to end, and the conclusion says twenty-seven contracts total. Section 6, however, says 'Nineteen contracts are proved complete at the time of writing, and two more are in progress with partial proofs,' and Table 2 shows Clipper (26/29) and Auction (18/20) incomplete, with 21 deployed contracts listed. The numbers must be reconciled; the current text is self-contradictory and overstates the shipped results.
  4. [§3, 'The EVM, Formally'] The paper states that the semantics were modified from EVMYulLean — changing gas arithmetic, reducing FFI reliance, adding dependent types — but does not report a re-run of the conformance suite. The original model was validated against 99.99% of the Cancun tests; the modified model may no longer conform. Since the refinement theorem is only as good as the EVM model, please report the conformance result for the exact semantics used in the proofs, or list and justify any failing tests.
minor comments (6)
  1. [§2.2] Typo: 'A refinement relations s fixes' should be 'A refinement relation fixes'.
  2. [§4.2] 'it let's us' should be 'it lets us'.
  3. [§5.2] Typo: 'the the refinement relation' -> 'the refinement relation'.
  4. [Throughout] Inconsistent spelling: the abstract uses 'EquiVM' while the body uses 'EqiVM'. Please standardize.
  5. [Table 2] The Auction row reports Check as '?' (timeout); make this explicit in the caption or as a footnote so it is not confused with a complete check.
  6. [§6] The specification-editing incidents (Flipper, Cure, Auction, Clipper) should be highlighted in the main text as a limitation: the certificate only proves that bytecode matches the final edited spec, not that the spec matches original human intent. This is partially disclosed in Appendix C but deserves prominence in Section 6.

Circularity Check

2 steps flagged · score 6.0 of 10

Existential call gas and post-hoc specification edits make the 'end-to-end proof' claims partially reduce to the definitions and to fitted specs.

  1. self definitional [Section 4.2 (Fig. 7, Θ-Call) and Section 5 (Fig. 9, R-Exec / r≈R)]
    "Because Sol− tracks neither gas nor the accrued substate, the call’s gas allowance and input substate are existentially quantified in the premise: the call “behaves as Θ would, for some gas and substate.” ... R-Exec ... Ξ(cA, σ_evm, σ0, g, A, I) = r; χ; ctr ⊢ (σ_solm, g, A, I) ⇓tx R; r ≈ R ... revert g' o ≈ rev"

    With ∃g A_in in Θ-Call, every typed external call has a spec-level rev derivation: choose g small enough that the callee fails, and ExtCallFail fires. Since R-Exec only requires the bytecode result to equal some Sol− judgment R, and revert g' o ≈ rev, any bytecode that reverts on an external-calling transition is trivially refined by a specification written to succeed. The theorem therefore cannot certify the transition's intended storage/return effect on the success path; the 'end-to-end proof' conclusion is forced, on the failure side, by the over-approximate definition of the external-call rule rather than by the bytecode's actual intended behavior.

  2. fitted input called prediction [Section 6 (Autonomy, Semantic blockers) and Appendix C (Flipper, Auction)]
    "Flipper’s agent reported a specification mismatch and was authorized to correct the specification. ... In order to overcome this semantic mismatch, we added a well-formed storage hypothesis in the refinement relation, requiring that the size in bytes of the array does not exceed the UInt256 range. ... Auction ... 'can you add it and update the spec and keep working on the proof?'"

    The specification and refinement relation are modified after observing bytecode behavior, and the same pipeline then proves that the bytecode refines the edited specification. The certificate is therefore a check of consistency between the bytecode and a retrofitted description, not of the original intended behavior. The evaluation's 'twenty-three contracts proved end to end' claim is fitted to the data: the proof target was adjusted based on the mismatches it reported, so the successful proofs are partially forced by construction.

full rationale

The kernel-checked refinement theorem itself is not circular in the sense of an unproved equality: R-Exec is a genuine Lean statement and using the same Θ on both sides of external calls is a sound congruence, not a tautology. No load-bearing self-citation or imported uniqueness theorem appears; the citation to the authors' prior ICFP work is contextual only. However, two steps reduce the advertised strength of the results. First, the existential gas/substate in Sol−'s external-call rule gives every external-calling transition a spurious revert derivation, so the existential matching in R-Exec makes always-revert bytecode refine a succeeding specification; the theorem no longer establishes intended effects. Second, the paper explicitly discloses that the same agent was authorized to correct specifications after reporting mismatches and that a well-formedness hypothesis was inserted after a semantic mismatch; this makes the 'proved end to end' evaluation a fitted-input result rather than an independent prediction. These are disclosed limitations, but they are load-bearing for the headline claim, hence a partial-circularity score of 6.

Assumptions & free parameters 4 free parameters · 9 assumptions · 2 invented entities

The central claim rests on trust in the EVM formalization, the Lean kernel, the Keccak extern, native_decide axioms, per-contract selector facts, and crucially on the fidelity of the Sol− specification. The storage layout and ABI configuration are hand-set per contract to match the bytecode; these are legitimate verification parameters, but they are fitted to the artifact being verified. The paper introduces no empirical physical entities, only formal artifacts whose adequacy is established by the paper's own semantics and proofs.

free parameters (4)
  • per-contract storage layout L = Solidity layout: declaration-order slots, keccak-derived mapping slots, packed bytes/string layouts
    The Sol− semantics is parametric in a storage layout that maps symbolic references to concrete slots. The layout is supplied per contract to match the bytecode's storage behavior; if it is wrong, the refinement theorem compares against a mis-modeled specification.
  • external ABI encode/decode functions encode_χ/decode_χ = ABI standard encoders/decoders, instantiated per callee interface
    Configuration data that fixes how typed external calls and returns are serialized. It is chosen to match the selectors and encodings the bytecode actually uses.
  • constructor payload assembly and immutable splice offsets = Template runtime code and published offsets for contracts with immutables
    The constructor judgment is parameterized over a function assembling the creation payload and over the offsets where immutable values are patched into the runtime code template.
  • well-formed storage array bound = Array byte-size must not exceed UInt256 range
    Added post hoc in Section 6 after a semantic mismatch between bytecode dynamic-array copying and Sol− semantics; this narrows the refinement theorem for large arrays.
assumptions (9)
  • domain assumption The extended EVM formalization faithfully models the Cancun EVM after modifications to gas arithmetic and FFI use.
    Section 3: builds on EVMYulLean validated against 99.99% of the conformance suite, but the paper does not report re-validation of the modified semantics.
  • standard math The Lean kernel and imported standard axioms are sound.
    Section 5.2: the trusted computing base explicitly includes the Lean kernel and standard axioms.
  • domain assumption The opaque Lean constant for Keccak-256 is correctly implemented externally.
    Sections 3 and 5.2: Keccak is used by the KECCAK256 opcode, address derivation, and Sol− selectors; closed facts about selectors cannot be derived by kernel reduction.
  • ad hoc to paper native_decide-generated axioms from Lean's compiled evaluator are sound.
    Section 5.2: native_decide is used for large computations; it expands the trusted base, and the authors argue it could be replaced by untrusted decide with more resources.
  • domain assumption Per-contract selector facts are trusted: the first four bytes of a signature's Keccak hash match the bytes hard-coded in the dispatcher.
    Section 5.2: explicitly listed as trusted per verified contract because opaque Keccak prevents kernel reduction of selector facts.
  • domain assumption The official EVM conformance test suite is correct and sufficiently covers the intended EVM semantics.
    Section 5.2: the trust in the EVM model is based on conformance with the official test suite.
  • domain assumption The Sol− specification, including authorized edits, faithfully captures the intended contract behavior.
    Sections 4 and 6: a certificate is only as meaningful as the specification; in several runs the proving agent was authorized to modify the specification after reporting mismatches.
  • ad hoc to paper For dynamic-array returns, the stored array byte-size is within UInt256, so bytecode copy and Sol− semantics agree.
    Section 6, 'Semantic blockers': added as a well-formed storage hypothesis to reconcile bytecode wrap-around behavior with Sol− semantics.
  • domain assumption Protocol preconditions such as calldata length below 2^256, write permission, and call depth bounds hold for top-level calls.
    Fig. 9: the runtime judgment is restricted to protocol-conforming top-level calls.
invented entities (2)
  • Sol− specification language
    purpose: Provides the high-level, Solidity-like behavioral specification that the bytecode refinement theorem is stated against.
    A new formal artifact introduced by the paper; it has a Lean semantics but no external behavioral validation, and its fidelity to the source contract's intent is assumed and in places edited by the LLM agent.
  • Reach-invariant proof combinator algebra (RD)
    purpose: Compositional forward-symbolic-execution device used to reduce whole-run Ξ statements to per-opcode lemmas.
    A proof-engineering device; its adequacy is internal to the Lean development and not independently validated outside the paper.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Foundational Refinement Proofs for Deployed Bytecode, at the Price of Tokens." pith.science (2026). https://pith.science/paper/KTYWHZL7

@misc{pith2026260726306,
  author       = {Pith},
  title        = {Pith review of: Foundational Refinement Proofs for Deployed Bytecode, at the Price of Tokens},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/KTYWHZL7}},
  note         = {Machine review of arXiv:2607.26306}
}
read the original abstract

Relating low-level executable code to a high-level account of its behavior has been a central concern of programming-language research for decades. From formally verified compilers to translation validators, certifying compilers, and proof-carrying code, each approach chooses between laborious but foundational mechanized proofs and automation that costs completeness, generality, and an increased trusted base. Recently, large language models (LLMs) have begun to change the economics of formal verification. Agentic proof development is now capable of producing machine-checked proofs at a scale and speed that were previously out of reach. In this paper, we evaluate the capabilities of LLMs to produce foundational, machine-checked proofs of refinement between executable code and its high-level specification, as post hoc, per-artifact certificates. We study this in the context of the Ethereum Virtual Machine (EVM), a low-level virtual machine that executes smart contracts on the Ethereum blockchain. We build EquiVM, a foundational framework in Lean comprising an executable EVM semantics and a specification language that characterizes the intended behavior of smart contracts, but commits to no source language or compilation toolchain. In EquiVM, refinement is stated for deployed bytecode of arbitrary provenance, interaction with unknown code is part of the semantics, and each proof is a replayable, machine-checked certificate. No previous technique achieves this combination. Using frontier commercial LLMs, twenty-three real-world contracts are proved end to end with minimal human guidance, among them most of the MakerDAO stablecoin system, at up to a hundred million tokens and a hundred hours of proof time per contract. We conclude that foundational mechanized proofs can now be bought at the price of tokens, and that this shift can reshape how verification frameworks are architected.

Figures

Figures reproduced from arXiv: 2607.26306 by the authors.

Figure 1
Figure 1. The running example: an ERC20 token contract, and the calldata of one call to it. [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. The EVM state Σ, with the Yellow Paper’s glyphs [88]. All components are purely functional data (finite maps as balanced search trees, memory as a byte array). Storage is a word-to-word map, and an account carries its deployed code as bytes, where real clients store a hash into a global database. then constructs the proof, using a proof library built for this purpose (section 5.1), and the Lean kernel checks it, and… view at source ↗
Figure 3
Figure 3. The semantic functions of the EVM model (total Lean functions). The mutual nest step/X/Ξ/Θ/Λ terminates by a lexicographic measure: the remaining call depth, bounded by 1024, decreases at every nested call, and within one call frame the fuel of X decreases at every instruction. Execution as Total Functions. Execution is organized, as in the Yellow Paper, into a hierarchy of semantic functions (fig. 3). The transacti… view at source ↗
Figures from the paper (10 more)
Figure 4
Figure 4. Figure 4: Syntax of Sol− . Superscript ? marks optional elements. target’s code in the caller’s storage and context and takes no value argument (DELEGATECALL opcode preserves msg.value). The try/catch form (try 𝑒.𝑓 {value: 𝑒}(𝑒) returns (𝑥) {𝑠} catch (𝑦) {𝑠}) is a typed external…
Figure 5
Figure 5. Figure 5: Runtime values and frames of Sol− . Here 𝑛 is an unbounded integer, 𝑏 a boolean, 𝑎 a 160-bit address, bs𝑛 a fixed-size (bytes𝑛) and bs a dynamic byte string; unit is the void result. A storage-reference value ref ( ˆℓ : 𝑇 ) tags an evaluated reference with its Sol− typ…
Figure 6
Figure 6. Figure 6: Selected statement rules of Sol− (of 65 in the full relation). All judgments are implicitly indexed by the configuration 𝜒. 𝐹 [𝑥 ↦→ 𝑣] updates a local binding; 𝐹 ⟨𝑥 ↦→ 𝑣⟩ is a fresh frame for the same contract whose locals bind exactly the callee’s parameters; 𝑣 ′ ↓ co…
Figure 7
Figure 7. Figure 7: The external-call boundary (excerpt; argument-evaluation failure rules omitted). [PITH_FULL_IMAGE:figures/full_fig_p013_7.png]
Figure 8
Figure 8. Figure 8: Message-level execution of a Sol− contract (constructor execution is analogous). The judgment’s interface mirrors the EVM code-execution function Ξ: an account map 𝜎 (and transaction snapshot 𝜎0), gas 𝑔, substate 𝐴, and execution environment 𝐼. selector matches the fir…
Figure 9
Figure 9. Figure 9: The top-level runtime judgment, the refinement relation it requires, and the result-, return-, and state [PITH_FULL_IMAGE:figures/full_fig_p016_9.png]
Figure 10
Figure 10. Figure 10: Cursors, the reach invariant (RD in the development), and its terminal forms, over an ambient environment 𝐼, gas budget 𝑔, and start state 𝑠0. Push1 𝑠0 ⇝𝑘,𝐶 ⟨pc | 𝑤 | 𝑚, aw | 𝑟 | 𝑊 ⟩ decode(𝐼𝑏, pc) = PUSH1 𝑣 |𝑤| + 1 ≤ 1024 𝑠0 ⇝𝑘+1,𝐶+3 ⟨pc + 2 | 𝑣 · 𝑤 | 𝑚, aw | 𝑟 | 𝑊 ⟩…
Figure 11
Figure 11. Figure 11: Selected combinators of the reach algebra ( [PITH_FULL_IMAGE:figures/full_fig_p018_11.png]
Figure 12
Figure 12. Figure 12: The same straight-line reasoning before the [PITH_FULL_IMAGE:figures/full_fig_p031_12.png]
Figure 13
Figure 13. Figure 13: A segment lemma from the ERC20 proof (lightly reformatted). [PITH_FULL_IMAGE:figures/full_fig_p032_13.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

89 extracted references · 13 canonical work pages

  1. [1]

    Hayden Adams, Noah Zinsmeister, and Dan Robinson. 2020. Uniswap v2 Core. Whitepaper, https://app.uniswap.org/ whitepaper.pdf

    2020

  2. [2]

    Amal Ahmed. 2015. Verified Compilers for a Multi-Language World. In1st Summit on Advances in Programming Languages (SNAPL 2015) (LIPIcs, Vol. 32). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 15–31. https://doi.org/ 10.4230/LIPIcs.SNAPL.2015.15

    work page doi:10.4230/lipics.snapl.2015.15 2015

  3. [3]

    Sidney Amani, Myriam Bégel, Maksym Bortin, and Mark Staples. 2018. Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL. InProceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP). ACM, 66–77. https://doi.org/10.1145/3167084

    doi:10.1145/3167084 2018

  4. [4]

    Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, and Bas Spitters. 2021. Extracting Smart Contracts Tested and Verified in Coq. InProceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP). ACM, 105–121. https://doi.org/10.1145/3437992.3439934

    arXiv 2021

  5. [5]

    Andrew W. Appel. 2001. Foundational Proof-Carrying Code. InProceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society, 247–256. https://doi.org/10.1109/LICS.2001.932501

    arXiv 2001

  6. [6]

    Gilles Barthe, Benjamin Grégoire, César Kunz, and Tamara Rezk. 2006. Certificate Translation for Optimizing Compilers. InStatic Analysis, 13th International Symposium (SAS) (Lecture Notes in Computer Science, Vol. 4134). Springer, 301–317

    2006

  7. [7]

    Gilles Barthe, Benjamin Grégoire, César Kunz, and Tamara Rezk. 2009. Certificate Translation for Optimizing Compilers. ACM Transactions on Programming Languages and Systems (TOPLAS)31, 5, Article 18 (2009), 18:1–18:45 pages

    2009

  8. [8]

    Sandrine Blazy, Zaynah Dargaye, and Xavier Leroy. 2006. Formal Verification of a C Compiler Front-End. InFM 2006: Int. Symp. on Formal Methods (Lecture Notes in Computer Science, Vol. 4085). Springer, 460–475. http://xavierleroy.org/ publi/cfront.pdf

    2006

Show all 89 references
  1. [9]

    Jan Olaf Blech and Benjamin Grégoire. 2008. Certifying Code Generation with Coq. InProceedings of the Workshop on Compiler Optimization Meets Compiler Verification (COCV 2008) (Electronic Notes in Theoretical Computer Science). Elsevier

    2008

  2. [10]

    Jan Olaf Blech and Arnd Poetzsch-Heffter. 2007. A Certifying Code Generation Phase.Electronic Notes in Theoretical Computer Science190, 4 (2007), 65–82

    2007

  3. [11]

    Sergiu Bursuc, Theodore Ehrenborg, Shaowei Lin, Lacramioara Astefanoaei, Ionel Emilian Chiosa, Jure Kukovec, Alok Singh, Oliver Butterley, Adem Bizid, Quinn Dougherty, Miranda Zhao, Max Tan, and Max Tegmark. 2025. A Benchmark for Vericoding: Formally Verified Program Synthesis...

    2025

  4. [12]

    Ghale, David J

    Franck Cassez, Joanne Fuller, Milad K. Ghale, David J. Pearce, and Horacio Mijail Anton Quiles. 2023. Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny. InFormal Methods (FM 2023) (Lecture Notes in Computer Science, Vol. 14000). Springer, 571–583. https:...

    2023 doi

  5. [13]

    Certora. 2025. The Certora Prover. https://github.com/Certora/CertoraProver. Open-sourced February 2025. Accessed July 2026

    2025

  6. [14]

    Dapphub. [n.d.]. WETH9: Wrapped Ether. Deployed contract https://etherscan.io/address/ 0xC02aaA39b223FE8D0A0e5C4F27eAD9083C756Cc2. Accessed July 2026

    2026

  7. [15]

    dxo, Mate Soos, Zoe Paraskevopoulou, Martin Lundfall, and Mikael Brockman. 2024. Hevm, a Fast Symbolic Execution Framework for EVM Bytecode. InComputer Aided Verification (CA V 2024) (Lecture Notes in Computer Science). Springer, 453–465. https://doi.org/10.1007/978-3-031-65627-9_22

    2024 doi

  8. [16]

    Yueyang Feng, Dipesh Kafle, Vladimir Gladshtein, Vitaly Kurin, George Pîrlea, Qiyuan Zhao, Peter Müller, and Ilya Sergey. 2026. Certified Program Synthesis with a Multi-Modal Verifier. arXiv:2604.16584 [cs.SE]

    2026 arXiv

  9. [17]

    Rabe, Talia Ringer, and Yuriy Brun

    Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. 2023. Baldur: Whole-Proof Generation and Repair with Large Language Models. InProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering(San Fran...

    2023

  10. [18]

    Benjamin Goldberg, Lenore Zuck, and Clark Barrett. 2005. Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers. InProceedings of the Workshop on Compiler Optimization Meets Compiler Verification (COCV

    2005

  11. [19]

    Neville Grech, Lexi Brent, Bernhard Scholz, and Yannis Smaragdakis. 2019. Gigahorse: Thorough, Declarative Decompilation of Smart Contracts. InProceedings of the 41st International Conference on Software Engineering (ICSE). IEEE, 1176–1186. https://doi.org/10.1109/ICSE.2019.00120

    2019

  12. [20]

    Neville Grech, Sifis Lagouvardos, Ilias Tsatiris, and Yannis Smaragdakis. 2022. Elipmoc: Advanced Decompilation of Ethereum Smart Contracts.Proceedings of the ACM on Programming Languages6, OOPSLA1 (2022), 77:1–77:27. https://doi.org/10.1145/3527321

    2022 doi

  13. [21]

    Ilya Grishchenko, Matteo Maffei, and Clara Schneidewind. 2018. A Semantic Framework for the Security Analysis of Ethereum Smart Contracts. InPrinciples of Security and Trust (POST 2018) (Lecture Notes in Computer Science, Vol. 10804). Springer, 243–269. https://doi.org/10.1007...

    2018 doi

  14. [22]

    Shelly Grossman, John Toman, Alexander Bakst, Sameer Arora, Mooly Sagiv, and Chandrakana Nandi. 2024. Practical Verification of Smart Contracts using Memory Splitting.Proceedings of the ACM on Programming Languages8, OOPSLA2 (2024), 2402–2433. https://doi.org/10.1145/3689796

    2024 doi

  15. [24]

    Pollard, Nadesh Ramanathan, and John Wickerson

    Yann Herklotz, James D. Pollard, Nadesh Ramanathan, and John Wickerson. 2021. Formal Verification of High-Level Synthesis.Proceedings of the ACM on Programming Languages5, OOPSLA, Article 117 (2021), 117:1–117:30 pages. https://doi.org/10.1145/3485494

    2021 doi

  16. [25]

    Moore, Daejun Park, Yi Zhang, Andrei Stefanescu, and Grigore Rosu

    Everett Hildenbrandt, Manasvi Saxena, Nishant Rodrigues, Xiaoran Zhu, Philip Daian, Dwight Guth, Brandon M. Moore, Daejun Park, Yi Zhang, Andrei Stefanescu, and Grigore Rosu. 2018. KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine. In31st IEEE Computer Security...

    2018

  17. [26]

    Yoichi Hirai. 2017. Defining the Ethereum Virtual Machine for Interactive Theorem Provers. InFinancial Cryptography and Data Security – FC 2017 International Workshops (WTSC) (Lecture Notes in Computer Science, Vol. 10323). Springer, 520–535. https://doi.org/10.1007/978-3-319-...

    2017 doi

  18. [27]

    Childers, and Mary Lou Soffa

    Yuqiang Huang, Bruce R. Childers, and Mary Lou Soffa. 2006. Catching and Identifying Bugs in Register Allocation. In Static Analysis, 13th International Symposium (SAS) (Lecture Notes in Computer Science, Vol. 4134). Springer, 281–300

    2006

  19. [28]

    Eleftherios Ioannidis, Nikhil Swamy, Gabriel Ebner, Matthai Philipose, and Tahina Ramananandro. 2026. Proofs Promptly: An Experience Report on Proof-Oriented Programming with AI Agents.Proceedings of the ACM on Programming Languages10, ICFP (2026). To appear

    2026

  20. [29]

    Jacques-Henri Jourdan, François Pottier, and Xavier Leroy. 2012. Validating LR(1) Parsers. InESOP 2012 - Programming Languages and Systems - 21st European Symposium on Programming (Lecture Notes in Computer Science, Vol. 7211). Springer, Tallinn, Estonia, 397–416. https://doi....

    2012 doi

  21. [30]

    Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, and Viktor Vafeiadis. 2016. Lightweight Verification of Separate Compilation.SIGPLAN Not.51, 1 (Jan. 2016), 178–190. https://doi.org/10.1145/2914770.2837642

    2016

  22. [31]

    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. InProceedings of the A...

    2009

  23. [32]

    Jérémie Koenig and Zhong Shao. 2021. CompCertO: Compiling Certified Open C Components. InProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI). ACM, 1095–1109. https://doi.org/10.1145/3453483.3454097

    2021

  24. [33]

    Jacco O. G. Krijnen, Manuel M. T. Chakravarty, Gabriele Keller, and Wouter Swierstra. 2024. Translation Certification for Smart Contracts.Science of Computer Programming233 (2024), 103051

    2024

  25. [34]

    Myreen, Michael Norrish, and Scott Owens

    Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. 2014. CakeML: A Verified Implementation of ML.SIGPLAN Not.49, 1 (Jan. 2014), 179–191. https://doi.org/10.1145/2578855.2535841

    2014

  26. [35]

    Peter Lammich. 2019. Generating Verified LLVM from Isabelle/HOL. In10th International Conference on Interactive Theorem Proving (ITP 2019) (LIPIcs, Vol. 141). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 22:1–22:19. https: //doi.org/10.4230/LIPIcs.ITP.2019.22

    2019 doi

  27. [36]

    Xavier Leroy. 2009. Formal verification of a realistic compiler.Commun. ACM52, 7 (2009), 107–115. http://xavierleroy. org/publi/compcert-CACM.pdf

    2009

  28. [37]

    Guodong Li, Scott Owens, and Konrad Slind. 2007. Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic. InEuropean Symposium on Programming (ESOP) (Lecture Notes in Computer Science, Vol. 4421). Springer, 205–219

    2007

  29. [38]

    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 Transla- tion Validation for LLVM. InProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, 65–79

    2021

  30. [39]

    Minghai Lu, Benjamin Delaware, and Tianyi Zhang. 2024. Proof Automation with Large Language Models. In Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering(Sacramento, CA, USA) (ASE ’24). Association for Computing Machinery, New York, NY,...

    2024 doi

  31. [40]

    Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor. 2016. Making Smart Contracts Smarter. InProceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (CCS). ACM, 254–269. https://doi.org/10.1145/2976749.2978309 1:28 Lazaropoulo...

    2016

  32. [41]

    Haoyang Ma, Wuqi Zhang, Qingchao Shen, Yongqiang Tian, Junjie Chen, and Shing-Chi Cheung. 2024. Towards Understanding the Bugs in Solidity Compiler. InProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA). ACM, 1312–1324. https://...

    2024

  33. [42]

    MakerDAO. [n.d.]. DSS: The Dai Stablecoin System. https://github.com/makerdao/dss. Accessed July 2026

    2026

  34. [43]

    Thomas Marchand. 2026. Verity: A Verified Compiler for a Core Fragment of EVM Smart Contracts in Lean 4. LFG Labs report, https://lfglabs.dev/papers/verity.pdf; code at https://github.com/lfglabs-dev/verity. Accessed July 2026

    2026

  35. [44]

    Jacob Matthews and Robert Bruce Findler. 2007. Operational Semantics for Multi-Language Programs. InProceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(Nice, France)(POPL ’07). Association for Computing Machinery, New York, NY, US...

    2007

  36. [45]

    John Mccarthy and James Painter. 1967. Correctness of a compiler for arithmetic expressions. InProceedings of a Symposium in Applied Mathematics, Vol. 19(Providence, R.I.), J.T. Schwartz (Ed.). American Mathematical Society, 33–41

    1967

  37. [46]

    Weyhrauch

    Robin Milner and R.W. Weyhrauch. 1972. Proving compiler correctness in a mechanised logic.Machine Intelligence7 (1972), 51–73

    1972

  38. [47]

    Myreen, Michael J

    Magnus O. Myreen, Michael J. C. Gordon, and Konrad Slind. 2012. Decompilation into Logic — Improved. InFormal Methods in Computer-Aided Design (FMCAD). IEEE, 78–81

    2012

  39. [48]

    Myreen, Konrad Slind, and Michael J

    Magnus O. Myreen, Konrad Slind, and Michael J. C. Gordon. 2008. Machine-Code Verification for Multiple Architectures — An Application of Decompilation into Logic. InFormal Methods in Computer-Aided Design (FMCAD). IEEE

    2008

  40. [49]

    Myreen, Konrad Slind, and Michael J

    Magnus O. Myreen, Konrad Slind, and Michael J. C. Gordon. 2009. Extensible Proof-Producing Compilation. In Compiler Construction, 18th International Conference (CC) (Lecture Notes in Computer Science, Vol. 5501). Springer, 2–16

    2009

  41. [50]

    George C. Necula. 1997. Proof-Carrying Code. InProceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 106–119

    1997

  42. [51]

    George C. Necula. 2000. Translation Validation for an Optimizing Compiler. InProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, 83–94

    2000

  43. [52]

    Necula and Peter Lee

    George C. Necula and Peter Lee. 1996. Safe Kernel Extensions Without Run-Time Checking. InProceedings of the Second USENIX Symposium on Operating Systems Design and Implementation (OSDI). ACM/USENIX, 229–243. https://doi.org/10.1145/238721.238781

    1996

  44. [53]

    Necula and Peter Lee

    George C. Necula and Peter Lee. 1998. The Design and Implementation of a Certifying Compiler. InProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, 333–344

    1998

  45. [54]

    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. InProceedings of the 20th ACM SIGPLAN International Conference on Functional Programmi...

    2015

  46. [55]

    Nethermind Formal Verification Team. 2025. EVMYulLean: Executable Formal Model of the EVM and Yul in Lean 4. https://github.com/NethermindEth/EVMYulLean. Validated against 99.99% of the Ethereum Cancun conformance tests. Accessed July 2026

    2025

  47. [56]

    Nouns DAO. [n.d.]. Nouns Auction House. https://github.com/nounsDAO/nouns-monorepo. Accessed July 2026

    2026

  48. [57]

    OpenZeppelin. [n.d.]. OpenZeppelin Contracts: A Library for Secure Smart Contract Development. https://github. com/OpenZeppelin/openzeppelin-contracts. Accessed July 2026

    2026

  49. [58]

    Zoe Paraskevopoulou. 2026. Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report). Proceedings of the ACM on Programming Languages10, ICFP (2026). To appear

    2026

  50. [59]

    Li, and Andrew W

    Zoe Paraskevopoulou, John M. Li, and Andrew W. Appel. 2021. Compositional Optimizations for CertiCoq.Proc. ACM Program. Lang.5, ICFP, Article 86 (July 2021), 30 pages. https://doi.org/10.1145/3473591

    2021 doi

  51. [60]

    Daejun Park, Yi Zhang, and Grigore Roşu. 2020. End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract. InComputer Aided Verification (CA V 2020), Part I (Lecture Notes in Computer Science, Vol. 12224). Springer, 151–164. https://doi.org/10.1007/978-3-030-53288-8_8

    2020 doi

  52. [61]

    Daejun Park, Yi Zhang, Manasvi Saxena, Philip Daian, and Grigore Rosu. 2018. A Formal Verification Tool for Ethereum VM Bytecode. InProceedings of the 2018 ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (E...

    2018

  53. [62]

    Daniel Patterson and Amal Ahmed. 2019. The next 700 Compiler Correctness Theorems (Functional Pearl).Proc. ACM Program. Lang.3, ICFP, Article 85 (July 2019), 29 pages. https://doi.org/10.1145/3341689

    2019 doi

  54. [63]

    Daniel Patterson, Noble Mushtak, Andrew Wagner, and Amal Ahmed. 2022. Semantic Soundness for Language Interoperability. InProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI). ACM, 609–624. https://doi.org/10.114...

    2022

  55. [64]

    Daniel Patterson, Jamie Perconti, Christos Dimoulas, and Amal Ahmed. 2017. FunTAL: Reasonably Mixing a Functional Language with Assembly. InProceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, 495–509. https://doi.org/10...

    2017

  56. [65]

    Perconti and Amal Ahmed

    James T. Perconti and Amal Ahmed. 2014. Verifying an Open Compiler Using Multi-Language Semantics. InProceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 8410. Springer-Verlag, Berlin, Heidelberg, 128–148. https://doi.org/10.1007/978-3-642-54833-8_8

    2014 doi

  57. [66]

    Amir Pnueli, Michael Siegel, and Eli Singerman. 1998. Translation Validation. InTools and Algorithms for the Construction and Analysis of Systems (TACAS) (Lecture Notes in Computer Science, Vol. 1384). Springer, 151–166

    1998

  58. [67]

    Nadia Polikarpova and Ilya Sergey. 2019. Structuring the Synthesis of Heap-Manipulating Programs.Proceedings of the ACM on Programming Languages3, POPL, Article 72 (2019), 72:1–72:30 pages. https://doi.org/10.1145/3290385

    2019 doi

  59. [68]

    Jianxing Qin, Alexander Du, Danfeng Zhang, Matthew Lentz, and Danyang Zhuo. 2025. Can Large Language Models Verify System Software? A Case Study Using FSCQ as a Benchmark. InProceedings of the 2025 Workshop on Hot Topics in Operating Systems(Banff, AB, Canada)(HotOS ’25). Asso...

    2025

  60. [69]

    Tahina Ramananandro, Zhong Shao, Shu-Chun Weng, Jérémie Koenig, and Yuchen Fu. 2015. A Compositional Semantics for Verified Separate Compilation and Linking. InProceedings of the 2015 Conference on Certified Programs and Proofs(Mumbai, India)(CPP ’15). Association for Computin...

    2015

  61. [70]

    Martin Rinard. 2026. Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude Code. https://doi.org/10.48550/arXiv.2605.01660 arXiv:2605.01660 [cs.PL]

    2026 doi arXiv

  62. [71]

    Xavier Rival. 2004. Symbolic Transfer Function-based Approaches to Certified Compilation. InProceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM Press, 1–13

    2004

  63. [72]

    Clara Schneidewind, Ilya Grishchenko, Markus Scherer, and Matteo Maffei. 2020. eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts. InProceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security (CCS). ACM, 621–640. https://...

    2020

  64. [73]

    Ilya Sergey, Vaivaswatha Nagaraj, Jacob Johannsen, Amrit Kumar, Anton Trunov, and Ken Chan Guan Hao. 2019. Safer Smart Contract Programming with Scilla.Proceedings of the ACM on Programming Languages3, OOPSLA (2019), 185:1–185:30. https://doi.org/10.1145/3360611

    2019 doi

  65. [74]

    Myreen, and Gerwin Klein

    Thomas Arthur Leck Sewell, Magnus O. Myreen, and Gerwin Klein. 2013. Translation Validation for a Verified OS Kernel. InProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, 471–482. https://doi.org/10.1145/2491956.2462183

    2013

  66. [75]

    Schett, Xinyuan Sun, Qinshi Wang, Sean Noble Anderson, Steve Reeves, and Zhong Shao

    Vilhelm Sjöberg, Kinnari Dave, Daniel Britten, Maria A. Schett, Xinyuan Sun, Qinshi Wang, Sean Noble Anderson, Steve Reeves, and Zhong Shao. 2024. Foundational Verification of Smart Contracts through Verified Compilation. https://doi.org/10.48550/arXiv.2405.08348 arXiv:2405.08...

    2024 doi arXiv

  67. [76]

    Vilhelm Sjöberg, Yuyang Sang, Shu-Chun Weng, and Zhong Shao. 2019. DeepSEA: A Language for Certified System Software.Proceedings of the ACM on Programming Languages3, OOPSLA (2019), 136:1–136:27. https://doi.org/10. 1145/3360562

    2019

  68. [77]

    Solidity Team. [n.d.]. List of Known Bugs — Solidity Documentation. https://docs.soliditylang.org/en/latest/bugs.html. Machine-readable list at https://github.com/ethereum/solidity/blob/develop/docs/bugs.json. Accessed July 2026

    2026

  69. [78]

    Solidity Team. [n.d.]. Solidity Documentation. https://docs.soliditylang.org. Accessed July 2026

    2026

  70. [79]

    Youngju Song, Minki Cho, Dongjoo Kim, Yonghyun Kim, Jeehoon Kang, and Chung-Kil Hur. 2019. CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification.Proc. ACM Program. Lang.4, POPL, Article 23 (Dec. 2019), 31 pages. https://doi.org/10.1145/3371091

    2019 doi

  71. [80]

    Gordon Stewart, Lennart Beringer, Santiago Cuellar, and Andrew W. Appel. 2015. Compositional CompCert. In Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(Mumbai, India)(POPL ’15). ACM, New York, NY, USA, 275–287. https://doi.o...

    2015

  72. [81]

    Ferreira, Sorin Lerner, and Emily First

    Kyle Thompson, Nuno Saavedra, Pedro Carrott, Kevin Fisher, Alex Sanchez-Stern, Yuriy Brun, João F. Ferreira, Sorin Lerner, and Emily First. 2025. Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification. InProceedings of the IEEE/ACM 47th International C...

    2025

  73. [82]

    Jean-Baptiste Tristan and Xavier Leroy. 2008. Formal Verification of Translation Validators: A Case Study on Instruction Scheduling Optimizations. InProceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 17–27

    2008

  74. [83]

    Jean-Baptiste Tristan and Xavier Leroy. 2009. Verified Validation of Lazy Code Motion. InProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, 316–326

    2009

  75. [84]

    Petar Tsankov, Andrei Dan, Dana Drachsler-Cohen, Arthur Gervais, Florian Bünzli, and Martin Vechev. 2018. Securify: Practical Security Analysis of Smart Contracts. InProceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security (CCS). ACM, 67–82. https:...

    2018

  76. [85]

    Vyper Team. [n.d.]. Vyper Documentation. https://docs.vyperlang.org. Accessed July 2026. 1:30 Lazaropoulos and Paraskevopoulou

    2026

  77. [86]

    Yuting Wang, Pierre Wilke, and Zhong Shao. 2019. An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code.Proc. ACM Program. Lang.3, POPL, Article 62 (Jan. 2019), 30 pages. https://doi.org/10. 1145/3290375

    2019

  78. [87]

    Yasunari Watanabe, Kiran Gopinathan, George Pîrlea, Nadia Polikarpova, and Ilya Sergey. 2021. Certifying the Synthesis of Heap-Manipulating Programs.Proceedings of the ACM on Programming Languages5, ICFP, Article 84 (2021), 84:1–84:29 pages. https://doi.org/10.1145/3473589

    2021 doi

  79. [88]

    Gavin Wood. 2014. Ethereum: A Secure Decentralised Generalised Transaction Ledger. Ethereum project yellow paper, https://ethereum.github.io/yellowpaper/paper.pdf. Continuously revised; page and equation references follow the Shanghai–Cancun revisions

    2014

  80. [89]

    why did you stop? The goal was to finish the whole proof

    Jingyi Emma Zhong, Kevin Cheang, Shaz Qadeer, Wolfgang Grieskamp, Sam Blackshear, Junkil Park, Yoni Zohar, Clark W. Barrett, and David L. Dill. 2020. The Move Prover. InComputer Aided Verification (CA V 2020) (Lecture Notes in Computer Science, Vol. 12225). Springer, 137–150. ...

    2020 doi

  81. [2004]

    (Electronic Notes in Theoretical Computer Science, Vol. 132). Elsevier, 53–71

Pith tools

Reviewed August 1, 2026 · model on record in the stance chip above.