Pith. sign in

REVIEW 4 major objections 6 minor 89 references

LLM agents produce machine-checked refinement proofs for deployed Ethereum bytecode.

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-01 00:13 UTC pith:KTYWHZL7

load-bearing objection 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. the 4 major comments →

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

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

Lefteris Lazaropoulos , Zoe Paraskevopoulou This is my paper
classification cs.PL
keywords refinementEVMLeanLLMtranslation validationproof-carrying codesmart contractsSol−
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 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.

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.

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.

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.

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 this falsifier — get emailed when new claim-graph text bears on it.

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.

Where Pith is reading between the lines

These are 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.

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

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

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

specific steps
  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.

Axiom & Free-Parameter Ledger

4 free parameters · 9 axioms · 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.
axioms (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 no independent evidence
    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) no independent evidence
    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.

pith-pipeline@v1.3.0-alltime-deepseek · 35929 in / 21632 out tokens · 207136 ms · 2026-08-01T00:13:10.857720+00:00 · methodology

0 comments
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 Lefteris Lazaropoulos, Zoe Paraskevopoulou.

Figure 1
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. 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 chec… view at source ↗
Figure 3
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… view at source ↗
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 call whose revert is caught. On success it runs the success block with the decoded return bound to 𝑥; on any callee revert it runs the catc… view at source ↗
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− type; an evaluated reference is a root variable 𝑥 followed by concrete steps—field, tuple-component, index (a mapping key or array index 𝑘), or… view at source ↗
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; 𝑣 ′ ↓ collapses a returned value list ([ ] ↦→ unit, singleton ↦→ the value, otherwise a tuple); W is the set of EVM words. Gas is deliberately nonde… view at source ↗
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] view at source ↗
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 first four calldata bytes against the Keccak-256 selectors of the contract’s transitions; decodecd 𝜒 ABI-decodes calldata into the transition’s… view at source ↗
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] view at source ↗
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 | 𝑟 | 𝑊 ⟩ JumpiT 𝑠0 ⇝𝑘,𝐶 ⟨pc | 𝑎 · 𝑏 · 𝑤 | 𝑚, aw | 𝑟 | 𝑊 ⟩ decode(𝐼𝑏, pc) = JUMPI 𝑏 ≠ 0 𝑎 ∈ 𝐷𝐽 (𝐼𝑏 ) 𝑠0 ⇝𝑘+1,𝐶+10 ⟨𝑎 | 𝑤 | 𝑚, aw | 𝑟 | 𝑊 ⟩ Sstore 𝑠0 … view at source ↗
Figure 11
Figure 11. Figure 11: Selected combinators of the reach algebra ( [PITH_FULL_IMAGE:figures/full_fig_p018_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: The same straight-line reasoning before the [PITH_FULL_IMAGE:figures/full_fig_p031_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: A segment lemma from the ERC20 proof (lightly reformatted). [PITH_FULL_IMAGE:figures/full_fig_p032_13.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

89 extracted references · 13 canonical work pages · 1 internal anchor

  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

  9. [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

  10. [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

  11. [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. arXiv:2509.22908 [cs.AI]

    arXiv 2025

  12. [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://doi.org/10.1007/978-3-031-27481-7_32

    work page doi:10.1007/978-3-031-27481-7_32 2023

  13. [13]

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

    2025

  14. [14]

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

    2026

  15. [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

    work page doi:10.1007/978-3-031-65627-9_22 2024

  16. [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]

    Pith/arXiv arXiv 2026

  17. [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 Francisco, CA, USA)(ESEC/FSE 2023). Association for Computing Machinery, New York, N...

    arXiv 2023

  18. [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

  19. [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

    arXiv 2019

  20. [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

    work page doi:10.1145/3527321 2022

  21. [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/978-3-319-89722-6_10 Foundational Refinement Proofs for Deployed Bytecode, at t...

    work page doi:10.1007/978-3-319-89722-6_10 2018

  22. [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

    work page doi:10.1145/3689796 2024

  23. [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

    doi:10.1145/3485494 2021

  24. [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 Foundations Symposium (CSF). IEEE, 204–217. https://doi.org/10.1109/CSF.2018.00022

    arXiv 2018

  25. [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-70278-0_33

    doi:10.1007/978-3-319-70278-0_33 2017

  26. [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

  27. [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

  28. [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.org/10.1007/978-3-642-28869-2_20

    doi:10.1007/978-3-642-28869-2_20 2012

  29. [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

    arXiv 2016

  30. [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 ACM SIGOPS 22nd Symposium on Operating Systems Principles (SOSP). ACM, 207–220. h...

    arXiv 2009

  31. [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

    arXiv 2021

  32. [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

  33. [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

    arXiv 2014

  34. [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

    work page doi:10.4230/lipics.itp.2019.22 2019

  35. [36]

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

    2009

  36. [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

  37. [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

  38. [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, USA, 1509–1520. https://doi.org/10.1145/3691620. 3695521

    doi:10.1145/3691620 2024

  39. [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 Lazaropoulos and Paraskevopoulou

    arXiv 2016

  40. [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://doi.org/10.1145/3650212.3680362

    arXiv 2024

  41. [42]

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

    2026

  42. [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

  43. [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, USA, 3–10. https://doi.org/10.1145/1190216.1190220

    arXiv 2007

  44. [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

  45. [46]

    Weyhrauch

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

    1972

  46. [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

  47. [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

  48. [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

  49. [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

  50. [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

  51. [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

    arXiv 1996

  52. [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

  53. [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 Programming(Vancouver, BC, Canada)(ICFP 2015). Association for Computing Machinery, New Y...

    arXiv 2015

  54. [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

  55. [56]

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

    2026

  56. [57]

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

    2026

  57. [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

  58. [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

    doi:10.1145/3473591 2021

  59. [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

    work page doi:10.1007/978-3-030-53288-8_8 2020

  60. [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 (ESEC/FSE). ACM, 912–915. https://doi.org/10.1145/3236024.3264591

    arXiv 2018

  61. [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

    work page doi:10.1145/3341689 2019

  62. [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.1145/3519939.3523703

    arXiv 2022

  63. [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.1145/3062341.3062347 Foundational Refinement Proofs for Deployed Bytecode, at t...

    arXiv 2017

  64. [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

    work page doi:10.1007/978-3-642-54833-8_8 2014

  65. [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

  66. [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

    doi:10.1145/3290385 2019

  67. [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). Association for Computing Machinery, New York, NY, USA, 34–41. https://doi.org/10.11...

    arXiv 2025

  68. [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 Computing Machinery, New York, NY, USA, 3–14. https: //doi.org/10.1145/2676724.2693167

    arXiv 2015

  69. [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]

    Pith/arXiv arXiv doi:10.48550/arxiv.2605.01660 2026

  70. [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

  71. [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://doi.org/10.1145/3372297.3417250

    arXiv 2020

  72. [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

    work page doi:10.1145/3360611 2019

  73. [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

    arXiv 2013

  74. [75]

    Foundational Verification of Smart Contracts through Verified Compilation

    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.08348 [cs.PL]

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2405.08348 2024

  75. [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

  76. [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

  77. [78]

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

    2026

  78. [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

    doi:10.1145/3371091 2019

  79. [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.org/10.1145/2676726.2676985

    arXiv 2015

  80. [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 Conference on Software Engineering (ICSE ’25). ACM. https: //doi.org/10.1109/ICSE...

    arXiv 2025

Showing first 80 references.