Pith. sign in

REVIEW 4 major objections 6 minor 65 references

Reviewed by Pith at T0; open to challenge.

T0 means a machine referee read the full paper against a public rubric. The mark states how deep the mechanical check went, never who wrote it. the ladder, T0–T4 →

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

T0 review · glm-5.2

LLM Code Agent Proves Every Lemma in Iris Verification Library

2026-07-08 09:10 UTC pith:V2TEBAGC

load-bearing objection 100% proof coverage on Iris using a general code agent plus a verification harness — real result, but memorization concern is not fully discharged the 4 major comments →

arxiv 2607.06341 v1 pith:V2TEBAGC submitted 2026-07-07 cs.FL cs.AIcs.SE

Harnessing Code Agents for Automatic Software Verification

Shuangxiang Kan , Shuanglong Kan , Sebastian Ertel This is my paper
classification cs.FL cs.AIcs.SE
keywords formal verificationautomated theorem provinginteractive theorem provingCoqLeanIris separation logiclarge language modelsLLM code agents
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 argues that the elaborate proof strategies prior automated theorem provers use—premise selectors, tactic-by-tactic search, divide-and-conquer decomposition—are not just unnecessary but actively limiting. The authors show that handing an entire unproved lemma to a general-purpose LLM code agent (Claude Code running Claude Opus 4.7), wrapped in a verification harness that checks each attempt against the Coq kernel and feeds back precise errors, achieves full coverage on benchmarks where prior systems proved only a fraction. The system, called Aria, proves all 4,257 lemmas of the Iris separation logic core, 217 RustBelt lemmas verifying Rust's standard libraries, all 318 lemmas of the reglang library (where prior provers managed roughly one in eight), and 72 not-yet-ported lemmas in a Lean 4 port of Iris—with zero failures and no human expert intervention. The central mechanism is the feedback loop: the agent proposes a proof, the harness checks it step-by-step against the Coq kernel, and on failure returns the exact line, error message, and pending proof goal, which the agent uses to revise. The harness also enforces completeness (no target lemma silently dropped or weakened) and termination (a 300-second per-tactic timeout catches divergent tactics). The authors express the harness policy in a declarative language called HHL, making it auditable and portable across agent runtimes and proof assistants.

Core claim

The discovery is that a deliberately coarse loop—general code agent plus sound verifier with structured error feedback—outperforms systems built around hand-engineered proof strategies. The agent makes every strategic decision itself: which lemma to apply, how to decompose a goal, when to backtrack, which definitions to look up. The harness contributes only the ground-truth check (the Coq or Lean kernel accepts or rejects) and the feedback that turns rejection into a revision signal. This suffices for 100% coverage on the hardest separation-logic proofs the authors could find, including the full Iris core and its downstream Rust safety applications, suggesting that the bottleneck in automatm

What carries the argument

The verification harness: a wrapper around the Coq (or Lean) kernel that checks each candidate proof step-by-step, returns the failing line, error message, and pending goal on rejection, enforces a ban on Admitted/Axiom, checks that the target lemma is still present and unweakened, and caps each tactic at 300 seconds to catch divergence. The harness is expressed in HHL, a declarative language compiled to Python hooks on the Claude Code SDK.

Load-bearing premise

The paper's most fragile premise is that the 100% success rate reflects genuine proof synthesis rather than recall of proofs the model may have seen during training. Iris is a widely-cited, publicly available Coq development, and Claude Opus 4.7's training data is not publicly known. The authors argue the generated proofs differ from upstream Iris proofs, but this does not fully exclude the possibility that the model learned proof patterns or individual tactics from the Iris源

What would settle it

Run Aria on a substantial body of lemmas from a Coq or Lean development created entirely after Claude Opus 4.7's training data cutoff, with no public analog in any form. If the success rate drops sharply, memorization is implicated; if it holds, the approach generalizes.

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

If this is right

  • If the result generalizes, the manual proof bottleneck that keeps verified software from scaling could ease substantially: any Coq or Lean development with a sound kernel could potentially be automated by pairing a code agent with a feedback harness, without building domain-specific proof strategies.
  • The HHL harness language could become a reusable interface layer: the same harness description could drive different agent backends (Claude Code, Codex, others) and different proof assistants (Coq, Lean), making the approach portable across the verification ecosystem.
  • The finding that the agent independently discovers the strategy of mimicking structurally similar nearby proofs—rather than following an externally imposed search policy—suggests that future improvements may come from better context assembly rather than more elaborate proof-search machinery.
  • The capability gap observed between private and open-source models on long proofs (beyond ~50 lines) identifies a concrete frontier: open-source models that can maintain correctness over long multi-step constructions would democratize the approach.

Where Pith is reading between the lines

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

  • The 100% success rate on Iris—a widely-cited, publicly available Coq development—cannot fully rule out memorization without knowing Claude Opus 4.7's training corpus composition. The iris-lean experiment (72 novel lemmas with no prior Lean proofs) partially addresses this, but the small sample and structural similarity to existing Coq versions limit its force as a counterexample. A stronger test w
  • If the approach scales beyond Iris to arbitrary Coq/Lean developments, it could shift the human expert's role from writing proofs to writing specifications—the unautomated upstream task the authors flag as a natural next step. This would change the economics of verified software: specification design becomes the bottleneck rather than proof construction.
  • The 380-hour model time for 4,257 lemmas (averaging ~321 seconds per lemma) suggests the approach is practical for library-scale verification but may face cost and latency challenges for interactive development workflows where a developer needs a proof in seconds, not minutes.
  • The observation that splitting developments into smaller lemmas improves the agent's first-attempt rate (90.3% on finer-grained iris-lean lemmas vs. 75.5% on coarser Coq versions) implies that proof structure itself is a lever: library authors could optimize lemma granularity for automated provability, not just human readability.

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 presents Aria, a system that pairs a general-purpose LLM code agent (Claude Code on Claude Opus 4.7) with a verification harness to automatically prove lemmas in Coq and Lean. The harness enforces soundness (kernel acceptance), completeness (no dropped goals), and termination (tactic timeouts), and is expressed in a declarative language called HHL. The central empirical claim is full coverage: all 4,257 Iris core lemmas, 217 RustBelt lemmas, all 318 reglang lemmas, and 72 iris-lean lemmas are proved with zero failures and no expert intervention. The paper compares favorably against prior LLM-based Coq provers (12–48% coverage) and includes a cross-prover (Lean) experiment and a private-vs-open-source model comparison.

Significance. The paper's strengths are substantial. The verification harness design is sound: trust is anchored in the Coq/Lean kernel, and the completeness check (no silently dropped or weakened lemmas) addresses a real gap in verifier-in-the-loop agent setups. The HHL abstraction is a genuine contribution, making the harness policy auditable and retargetable. The empirical scope—4,859 total lemmas across four independent benchmarks including the demanding Iris separation logic—is beyond what prior LLM prover evaluations have attempted. The reproducible code repository and the cross-model comparison (Opus 4.7 vs. Kimi K2.6) add credibility. The falsifiable claim of zero failures across the entire Iris core is a strong, testable prediction.

major comments (4)
  1. Section VI-B: The memorization concern is the most load-bearing issue for the central claim of genuine proof synthesis. The paper states that 'the proofs Aria generates differ from the upstream Iris proofs—it constructs them rather than recalling them,' but provides no systematic structural comparison (e.g., tactic sequence overlap, case-split order, lemma-application frequency). A textually different proof can reproduce the same proof structure from memory. Without quantification, the claim that generated proofs differ from upstream (Section VI-B) is unsupported. A structural diff metric or a comparison of tactic-graph isomorphism would substantially strengthen this.
  2. Section VI-F: The iris-lean experiment (72 lemmas) is presented as the strongest counter to memorization because 'no Lean proof exists.' However, the paper itself notes these are 'the same algebra' as the corresponding Coq modules (functions.v, mra.v, ufrac.v), whose proofs are publicly available in the Iris repository. The model could be translating memorized Coq proof structure into Lean syntax. The paper should explicitly acknowledge this translation-from-memory pathway and discuss why the structural similarity to existing Coq proofs does not undermine the novelty claim. Ideally, a held-out benchmark with no publicly available proof in any prover would be included, or the iris-lean lemmas should be shown to require proof structures not present in the Coq versions.
  3. Section VI-B: The 79.2% first-attempt success rate on Iris core is high for proofs the paper describes as taking 'hours or even days' for experts. While not impossible for a capable model, this rate is the metric most directly explained by training-time familiarity with the publicly available Iris repository. The sandbox protocol (Section VI-A: no network, no git) prevents inference-time retrieval but cannot prevent recall. The paper would benefit from an experiment on lemmas added or modified after the model's training cutoff, or from reporting the distribution of first-attempt successes across lemma difficulty tiers to show that the rate is not dominated by trivial lemmas. Without such evidence, the memorization concern remains a correctness-risk for the central claim.
  4. Sections V-B, VI-A: Several free parameters—the retry cap of 30, the session reuse window of 6, the tactic timeout of 300 s, and the polish rounds of 2—are set to specific values without sensitivity analysis. The retry cap in particular is load-bearing: the paper reports that no lemma exhausted the budget (max 28 retries on Iris core), but it is unclear whether the zero-failure result depends on this specific cap or would hold under a tighter budget. A sensitivity analysis on at least the retry cap and session reuse window would clarify whether the full-coverage claim is robust or contingent on a finely tuned parameter set.
minor comments (6)
  1. Figure 4 caption mentions 4,123 lemmas (96.9%) with module-qualified log paths, with 134 omitted due to ambiguous file names. The main text (Section VI-B, Table III) reports 4,257. The discrepancy should be noted earlier or the figure should use the full count to avoid confusion.
  2. Section VI-G: The comparison between Opus 4.7 and Kimi K2.6 is on only 40 lemmas (frac_auth.v). The claim of a 'genuine capability gap on long proofs' beyond 50 lines is stated qualitatively without supporting data. Either include the data for longer proofs or soften the claim to match what is reported.
  3. Section IV-A, Figure 2: The HHL example is helpful but the compilation target (Table II) could include a brief note on how the Turn post-hook is implemented in the driver, as this is flagged as having 'no native counterpart.' A one-sentence clarification would improve reproducibility.
  4. Section VI-H: The rubric criteria for proof polishing are illustrated with a single example (discrete_cmra_mixin). It would help to report what fraction of proofs passed all rubric criteria without polishing, and how many rounds were typically needed, to give a sense of the polish stage's practical impact.
  5. The paper uses 'Claude Opus 4.7' throughout, but the model's training data cutoff and corpus composition are not publicly known. This should be explicitly acknowledged in the memorization discussion (Section VI-B), as it directly affects the interpretability of the first-attempt success rates.
  6. Section VIII: Cobblestone is cited as reaching 48% (58% with oracle guidance) on general Coq. The comparison would be sharper if the paper noted whether Cobblestone was evaluated on any Iris or separation-logic benchmarks, or if the comparison is strictly on different corpora. This affects the strength of the 'Aria differs on both axes' claim.

Simulated Author's Rebuttal

4 responses · 2 unresolved

We thank the referee for a careful and constructive report. The referee recognizes the soundness of the harness design, the value of HHL as an auditable abstraction, the unprecedented empirical scope, and the testability of the zero-failure claim. The major comments all concern the memorization threat to the central claim and the robustness of the parameter choices. We address each below.

read point-by-point responses

  1. Referee: Section VI-B: The memorization concern is the most load-bearing issue. The paper claims generated proofs differ from upstream but provides no systematic structural comparison (tactic sequence overlap, case-split order, lemma-application frequency). A textually different proof can reproduce the same proof structure from memory.

    Authors: The referee is correct that our current evidence—a qualitative statement that proofs differ textually—is insufficient to rule out structural memorization. We will add a quantitative structural comparison in revision. Specifically, we plan to: (1) compute tactic-sequence overlap (edit distance over normalized tactic tokens) between Aria-generated and upstream proofs; (2) compare case-split structure (bullet nesting depth and branching order); (3) compare lemma-application frequency distributions. We will report these metrics across all 4,257 Iris core lemmas. We note that the example in Section VI-H already shows a concrete structural difference (the LLM enumerates subgoals explicitly while the human proof uses 'try done' to collapse them), but we agree this should be systematic rather than illustrative. We cannot fully rule out that some proofs share structural templates with upstream—this is an inherent limitation of evaluating on a public library with a model whose training data is unknown. We will state this limitation explicitly. revision: yes

  2. Referee: Section VI-F: The iris-lean experiment is presented as the strongest counter to memorization because no Lean proof exists, but the same algebra exists in publicly available Coq proofs. The model could be translating memorized Coq proof structure into Lean syntax.

    Authors: This is a fair point that we should and will acknowledge explicitly. The iris-lean lemmas are indeed the same algebraic content as the corresponding Coq modules (functions.v, mra.v, ufrac.v), and the model could in principle translate memorized Coq proof structure into Lean. The iris-lean experiment therefore demonstrates cross-prover transfer and the retargetability of the harness, but it is not a clean memorization control. We will revise Section VI-F to state this limitation clearly and downgrade the claim accordingly. Regarding the ideal experiment—a held-out benchmark with no publicly available proof in any prover—we agree this would be the strongest control. We are investigating whether recently added Iris lemmas postdating the model's training cutoff can serve this purpose, but we cannot commit to having results ready in time for the next revision. We will be transparent about this gap. revision: partial

  3. Referee: Section VI-B: The 79.2% first-attempt success rate is high for proofs described as taking experts hours or days. This rate is the metric most directly explained by training-time familiarity with the publicly available Iris repository. The sandbox prevents inference-time retrieval but cannot prevent recall. An experiment on lemmas added or modified after the model's training cutoff, or a difficulty-tier breakdown, would help.

    Authors: We agree that the 79.2% first-attempt rate is the metric most vulnerable to the memorization explanation, and we should provide more evidence. Two responses: (1) We will add a difficulty-tier breakdown of first-attempt success rates, stratified by proof length and retry count, to show the rate is not dominated by trivial lemmas. The per-module breakdown in Figure 4 already shows variation (71.9% in algebra vs. 87.3% in base_logic), but a within-module difficulty stratification is more informative. (2) Regarding lemmas added after the training cutoff: we are actively investigating this. The Iris repository is continuously updated, and if we can identify a sufficient number of lemmas added after Claude Opus 4.7's training cutoff, we will run Aria on them and report the results. However, we cannot guarantee a large enough sample exists at this time. We acknowledge that without such an experiment, the recall-from-training pathway cannot be fully eliminated. We will state this as a standing limitation rather than claim we have closed the gap. revision: partial

  4. Referee: Sections V-B, VI-A: Several free parameters (retry cap of 30, session reuse window of 6, tactic timeout of 300s, polish rounds of 2) are set without sensitivity analysis. The retry cap is load-bearing: no lemma exhausted the budget (max 28 retries), but it is unclear whether zero-failure depends on this specific cap. A sensitivity analysis on at least the retry cap and session reuse window would clarify robustness.

    Authors: The referee is right that a sensitivity analysis is needed, particularly for the retry cap since it is most directly tied to the zero-failure claim. We will conduct and report a sensitivity analysis varying the retry cap (e.g., 5, 10, 15, 20, 25) and the session reuse window (e.g., 1, 3, 6, 12) on at least a representative subset of the Iris core, and ideally the full benchmark if compute permits. We note that the max retry count observed was 28 out of 30, which means the result is indeed contingent on the cap being at least 28—a tighter cap would have produced failures. This is an important fact that we should make more prominent. We will report the distribution of retry counts in finer detail (not just the mean and max) so readers can see how many lemmas are near the cap. For the tactic timeout and polish rounds, we will add brief discussion of why those values were chosen and whether results are sensitive to them, though we expect these to be less critical. revision: yes

standing simulated objections not resolved
  • The memorization concern cannot be fully eliminated without knowledge of the model's training data, which is not publicly available. No experiment on a public benchmark with a proprietary model can definitively rule out that the model has seen the proofs during training. We can mitigate this with structural comparisons, difficulty stratification, and post-cutoff lemmas if available, but the concern is fundamental to evaluating LLM-based proof synthesis on public libraries.
  • A fully clean memorization control—a benchmark with no publicly available proof in any prover—does not currently exist at the scale needed to replicate the Iris core evaluation. The iris-lean experiment is the closest available but, as the referee correctly notes, shares algebraic content with public Coq proofs.

Circularity Check

0 steps flagged

No circularity found: the derivation chain is self-contained against external oracles and external benchmarks.

full rationale

The paper's central claim—that pairing an LLM code agent with a verification harness achieves full coverage on four benchmark suites—does not exhibit circularity. The proof candidates are generated by the LLM agent and checked by an independent external oracle (the Coq kernel or Lean kernel), which is not under the authors' control and whose acceptance is the sole criterion for success. The benchmarks (Iris, RustBelt, reglang, iris-lean) are independent, publicly available external artifacts. No parameter is fitted to a subset of data and then 'predicted' on closely related data. No load-bearing self-citation chain exists: the HHL language is introduced within the paper itself, and the Claude Code SDK, Iris, RustBelt, reglang, and iris-lean are all third-party artifacts. The paper does not invoke a uniqueness theorem from prior work by the same authors. The memorization concern raised by the reader is a validity/data-contamination risk (correctness risk), not a circularity issue: it questions whether the model genuinely synthesizes proofs versus recalls them, but either way the Coq/Lean kernel independently verifies correctness, so the claim 'every lemma is proved' is not circularly defined. The derivation chain is self-contained.

Axiom & Free-Parameter Ledger

4 free parameters · 4 axioms · 1 invented entities

The axiom ledger captures the key parameters and assumptions. The free parameters (retry cap, session window, timeout, polish rounds) are hand-chosen without sensitivity analysis. The most critical axiom is the non-memorization assumption, which is acknowledged but not verified. HHL is a new entity without independent evidence of correctness.

free parameters (4)
  • retry cap = 30
    Maximum retries per lemma before declaring failure (Section V, Figure 2). Chosen by hand; no sensitivity analysis provided.
  • session reuse window = 6
    Maximum consecutive lemmas sharing a session before reset (Section V-B). Described as a 'rule of thumb'.
  • tactic timeout = 300s
    Per-tactic timeout for divergent tactics (Section V-A.2). No justification given for this specific value.
  • polish rounds = 2
    Maximum style-polishing rounds after proof acceptance (Section VI-H).
axioms (4)
  • standard math Coq/Lean kernel is a sound proof oracle
    The entire approach depends on the proof assistant's kernel correctly rejecting invalid proofs. This is a standard, well-established assumption in formal methods.
  • domain assumption Claude Opus 4.7 has not memorized the Iris proof corpus
    The 100% success rate is interpreted as genuine proof synthesis. If the model has seen these proofs during training, the result measures recall. The paper acknowledges this (Section VI-B) but does not verify it.
  • domain assumption The four Iris core modules are representative of verification difficulty
    The paper generalizes from 100% success on these modules to the claim that verified software development can be automated. The modules may not represent the difficulty distribution of novel verification targets.
  • domain assumption HHL hooks correctly enforce completeness (no dropped goals)
    The verify_proof post-hook checks that target lemmas are present and proved. The correctness of this check is not formally verified; a bug in the hook could allow incomplete proofs to pass.
invented entities (1)
  • HHL (Harness Hook Language) no independent evidence
    purpose: Declarative language for specifying verification harness policies around LLM agents
    HHL is a new DSL introduced by this paper. Its compiler lowers to Python scripts targeting the Claude Code SDK. No formal semantics are provided; its correctness depends on the implementation of the lowering rules in Table II. No independent reproduction or formalization exists.

pith-pipeline@v1.1.0-glm · 23017 in / 2931 out tokens · 960055 ms · 2026-07-08T09:10:44.066477+00:00 · methodology

0 comments
read the original abstract

Formal verification offers the strongest guarantee of software correctness, but it does not scale: the proofs demanded by interactive theorem provers such as Coq require enormous expert effort. Large language models (LLMs) promise to generate these proofs automatically, yet existing approaches wire a fixed, human-designed proof strategy into the system and constrain the model to follow it (retrieving premises and predicting tactics one step at a time, or splitting goals by divide-and-conquer), and still prove only a fraction of their target theorems. We show that imposing such a strategy is unnecessary and limiting. Handing the whole lemma to a general LLM code agent (for example, Claude Code), free to choose its own approach, and wrapping it in a verification harness is both simpler and more effective, achieving full coverage: every targeted lemma proved, with no failures and no Coq expert intervention. The agent writes the proofs under feedback and hard constraints from the harness that keep each one sound (accepted only when the prover's kernel closes it), complete (no obligation left unproved or silently dropped), and terminating (no divergent tactics). We evaluate this harness plus code agent along three dimensions. (1) Core logic: on Iris, the state-of-the-art separation logic for concurrent and memory-manipulating programs, Aria proves all 4,257 lemmas of the four core modules and the 217 lemmas verifying Rust's standard libraries built on it, fully automatically. (2) Comparison with prior LLM provers: on reglang, where prior provers manage barely one in eight, Aria proves all 318. (3) Generality: on iris-lean, the unfinished Lean 4 port of Iris, it proves 72 not-yet-ported lemmas, showing the approach is not specific to Coq. A state-of-the-art model (Claude Opus 4.7) can write proofs for verified software development fully and automatically.

Figures

Figures reproduced from arXiv: 2607.06341 by Sebastian Ertel, Shuanglong Kan, Shuangxiang Kan.

Figure 1
Figure 1. Figure 1: Three-layer architecture of Aria. That reach comes at a cost. Iris proofs are among the hardest in all of software verification: a single non-trivial lemma can take an expert hours or even days, because the proof must account for every way concurrent threads can interleave and share state, with little syntactic guidance on what step to take next [23], [24]. Because Iris demands such deep understanding, dev… view at source ↗
Figure 3
Figure 3. Figure 3: Aria’s multi-agent proof loop. Each LLM role (Extractor, Prover, [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Per-module results on the Iris core (base = base_logic, prog = program_logic). Over the 4,123 lemmas (96.9%) with module-qualified log paths; the remaining 134 have ambiguous file names (e.g. big_op.v occurs in two modules) and are omitted [PITH_FULL_IMAGE:figures/full_fig_p007_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Cross-benchmark comparison of Aria on the Iris core (4,257 lemmas), [PITH_FULL_IMAGE:figures/full_fig_p008_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Private (Claude Opus 4.7) vs. open-source (Kimi K2.6). [PITH_FULL_IMAGE:figures/full_fig_p009_6.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

65 extracted references · 65 canonical work pages · 2 internal anchors

  1. [1]

    (2025) Claude code sdk

    Anthropic. (2025) Claude code sdk. Programmatic runtime for building agents on the Claude Code agent harness (hooks, tool dispatch, and model access). [Online]. Available: https://docs.claude.com/en/docs/ claude-code/sdk

    work page 2025

  2. [2]

    The coq proof assistant,

    C. D. Team, “The coq proof assistant,”Available at: https://coq.inria.fr, 2004

    work page 2004

  3. [3]

    Bertot and P

    Y . Bertot and P. Cast´eran,Interactive Theorem Proving and Program De- velopment: Coq’Art–The Calculus of Inductive Constructions. Springer Science+ Business Media, 2004

    work page 2004

  4. [4]

    Nipkow, L

    T. Nipkow, L. C. Paulson, and M. Wenzel,Isabelle/HOL: A Proof Assistant for Higher-Order Logic, ser. Lecture Notes in Computer Science. Springer, 2002, vol. 2283

    work page 2002

  5. [5]

    Local reasoning about programs that alter data structures,

    P. W. O’Hearn, J. C. Reynolds, and H. Yang, “Local reasoning about programs that alter data structures,” inComputer Science Logic (CSL 2001), ser. Lecture Notes in Computer Science, vol. 2142. Springer, 2001, pp. 1–19

    work page 2001

  6. [6]

    Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning,

    R. Jung, R. Krebbers, L. Birkedal, and A. Bizjak, “Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning,” in Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, 2015, pp. 637–650

    work page 2015

  7. [7]

    Iris from the ground up: A modular foundation for higher- order concurrent separation logic,

    R. Jung, R. Krebbers, J.-H. Jourdan, A. Bizjak, L. Birkedal, and D. Dreyer, “Iris from the ground up: A modular foundation for higher- order concurrent separation logic,”Journal of Functional Programming, vol. 28, p. e20, 2018

    work page 2018

  8. [8]

    Learning to prove theorems via interacting with proof assistants,

    K. Yang and J. Deng, “Learning to prove theorems via interacting with proof assistants,” inProceedings of the 36th International Conference on Machine Learning (ICML), ser. Proceedings of Machine Learning Research, vol. 97. PMLR, 2019, pp. 6984–6994

    work page 2019

  9. [9]

    Generating correctness proofs with neural networks,

    A. Sanchez-Stern, Y . Alhessi, L. Saul, and S. Lerner, “Generating correctness proofs with neural networks,” inProceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages (MAPL). ACM, 2020, pp. 1–10

    work page 2020

  10. [10]

    The tactician: A seamless, interactive tactic learner and prover for coq,

    L. Blaauwbroek, J. Urban, and H. Geuvers, “The tactician: A seamless, interactive tactic learner and prover for coq,” inIntelligent Computer Mathematics (CICM), ser. Lecture Notes in Computer Science, vol. 12236. Springer, 2020, pp. 271–277

    work page 2020

  11. [11]

    Graph2tac: Online representation learning of for- mal math concepts,

    L. Blaauwbroek, M. Ols ´ak, J. Rute, F. I. Schaposnik Massolo, J. Piepen- brock, and V . Pestun, “Graph2tac: Online representation learning of for- mal math concepts,” inProceedings of the 41st International Conference on Machine Learning (ICML), ser. Proceedings of Machine Learning Research, vol. 235. PMLR, 2024, pp. 4046–4076

    work page 2024

  12. [12]

    Baldur: Whole-proof generation and repair with large language models,

    E. First, M. N. Rabe, T. Ringer, and Y . Brun, “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 (ESEC/FSE). ACM, 2023, pp. 1229–1241

    work page 2023

  13. [13]

    Draft, sketch, and prove: Guiding formal theorem provers with informal proofs,

    A. Q. Jiang, S. Welleck, J. P. Zhou, W. Li, J. Liu, M. Jamnik, T. Lacroix, Y . Wu, and C. Szegedy, “Draft, sketch, and prove: Guiding formal theorem provers with informal proofs,” inProceedings of the 11th International Conference on Learning Representations (ICLR), 2023

    work page 2023

  14. [14]

    Leandojo: Theorem proving with retrieval-augmented language models,

    K. Yang, A. Swope, A. Gu, R. Chalamala, P. Song, S. Yu, S. Godil, R. Prenger, and A. Anandkumar, “Leandojo: Theorem proving with retrieval-augmented language models,” inAdvances in Neural Informa- tion Processing Systems 36 (NeurIPS), Datasets and Benchmarks Track, 2023

    work page 2023

  15. [15]

    DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data

    H. Xin, D. Guo, Z. Shao, Z. Ren, Q. Zhu, B. Liu, C. Ruan, W. Li, and X. Liang, “Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data,”arXiv preprint arXiv:2405.14333, 2024

    work page internal anchor Pith review Pith/arXiv arXiv 2024

  16. [16]

    Generative Language Modeling for Automated Theorem Proving

    S. Polu and I. Sutskever, “Generative language modeling for automated theorem proving,”arXiv preprint arXiv:2009.03393, 2020

    work page internal anchor Pith review Pith/arXiv arXiv 2009

  17. [17]

    Proof automation with large language models,

    M. Lu, B. Delaware, and T. Zhang, “Proof automation with large language models,” inProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering (ASE). ACM, 2024, pp. 1509–1520

    work page 2024

  18. [18]

    Rango: Adaptive retrieval-augmented proving for automated software verification,

    K. Thompson, N. Saavedra, P. Carrott, K. Fisher, A. Sanchez-Stern, Y . Brun, J. F. Ferreira, S. Lerner, and E. First, “Rango: Adaptive retrieval-augmented proving for automated software verification,” inPro- ceedings of the IEEE/ACM 47th International Conference on Software Engineering (ICSE). IEEE, 2025, pp. 347–359

    work page 2025

  19. [19]

    An in- context learning agent for formal theorem-proving,

    A. Thakur, G. Tsoukalas, Y . Wen, J. Xin, and S. Chaudhuri, “An in- context learning agent for formal theorem-proving,” inProceedings of the 1st Conference on Language Modeling (COLM), 2024

    work page 2024

  20. [20]

    Cobblestone: A divide-and-conquer approach for automating formal verification,

    S. R. Kasibatla, A. Agrawal, Y . Brun, S. Lerner, T. Ringer, and E. First, “Cobblestone: A divide-and-conquer approach for automating formal verification,” inProceedings of the 48th IEEE/ACM International Conference on Software Engineering (ICSE). ACM, 2026, pp. 714–726

    work page 2026

  21. [21]

    Proofcoop: Collaborative automated formal verification,

    Z. Kaufman, E. First, A. Sanchez-Stern, K. Thompson, S. Lerner, and Y . Brun, “Proofcoop: Collaborative automated formal verification,” inProceedings of the 48th IEEE/ACM International Conference on Software Engineering (ICSE). ACM, 2026, pp. 1339–1352

    work page 2026

  22. [22]

    Survey of hallucination in natural language generation,

    Z. Ji, N. Lee, R. Frieske, T. Yu, D. Su, Y . Xu, E. Ishii, Y . Bang, A. Madotto, and P. Fung, “Survey of hallucination in natural language generation,”ACM Computing Surveys, vol. 55, no. 12, pp. 1–38, 2023

    work page 2023

  23. [23]

    R. Jung, R. Krebbers, and L. Birkedal. (2023) Iris: Proof mode documentation and case studies. [Online]. Available: https://iris-project. org/

    work page 2023

  24. [24]

    The essence of higher-order concurrent separation logic,

    R. Krebbers, R. Jung, A. Bizjak, J.-H. Jourdan, D. Dreyer, and L. Birkedal, “The essence of higher-order concurrent separation logic,” inProgramming Languages and Systems (ESOP). Springer, 2017, pp. 696–723

    work page 2017

  25. [25]

    Rustbelt: Securing the foundations of the rust programming language,

    R. Jung, J.-H. Jourdan, R. Krebbers, and D. Dreyer, “Rustbelt: Securing the foundations of the rust programming language,”Proceedings of the ACM on Programming Languages, vol. 2, no. POPL, pp. 66:1–66:34, 2018

    work page 2018

  26. [26]

    Rusthornbelt: A semantic foundation for functional verification of rust programs with unsafe code,

    Y . Matsushita, X. Denis, J.-H. Jourdan, and D. Dreyer, “Rusthornbelt: A semantic foundation for functional verification of rust programs with unsafe code,” inProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI). ACM, 2022, pp. 841–856

    work page 2022

  27. [27]

    Refine- drust: A type system for high-assurance verification of rust programs,

    L. G ¨aher, M. Sammler, R. Jung, R. Krebbers, and D. Dreyer, “Refine- drust: A type system for high-assurance verification of rust programs,” Proceedings of the ACM on Programming Languages, vol. 8, no. PLDI, pp. 1115–1139, 2024

    work page 2024

  28. [28]

    Rustbelt meets relaxed memory,

    H.-H. Dang, J.-H. Jourdan, J.-O. Kaiser, and D. Dreyer, “Rustbelt meets relaxed memory,”Proceedings of the ACM on Programming Languages, vol. 4, no. POPL, pp. 34:1–34:29, 2020

    work page 2020

  29. [29]

    Iris-wasm: Robust and modular verification of webassembly programs,

    X. Rao, A. L. Georges, M. Legoupil, C. Watt, J. Pichon-Pharabod, P. Gardner, and L. Birkedal, “Iris-wasm: Robust and modular verification of webassembly programs,”Proceedings of the ACM on Programming Languages, vol. 7, no. PLDI, pp. 1096–1120, 2023

    work page 2023

  30. [30]

    Refinedc: Automating the foundational verification of c code with refined ownership types,

    M. Sammler, R. Lepigre, R. Krebbers, K. Memarian, D. Dreyer, and D. Garg, “Refinedc: Automating the foundational verification of c code with refined ownership types,” inProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI). ACM, 2021, pp. 158–174

    work page 2021

  31. [31]

    Quiver: Guided abduc- tive inference of separation logic specifications in coq,

    S. Spies, L. G ¨aher, M. Sammler, and D. Dreyer, “Quiver: Guided abduc- tive inference of separation logic specifications in coq,”Proceedings of the ACM on Programming Languages, vol. 8, no. PLDI, pp. 889–913, 2024

    work page 2024

  32. [32]

    Verifying concurrent, crash-safe systems with perennial,

    T. Chajed, J. Tassarotti, M. F. Kaashoek, and N. Zeldovich, “Verifying concurrent, crash-safe systems with perennial,” inProceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP). ACM, 2019, pp. 243–258. 11

    work page 2019

  33. [33]

    Gojournal: A verified, concurrent, crash-safe journaling system,

    T. Chajed, J. Tassarotti, M. Theng, R. Jung, M. F. Kaashoek, and N. Zeldovich, “Gojournal: A verified, concurrent, crash-safe journaling system,” in15th USENIX Symposium on Operating Systems Design and Implementation (OSDI). USENIX Association, 2021, pp. 423–439

    work page 2021

  34. [34]

    Verifying the daisynfs concurrent and crash-safe file system with se- quential reasoning,

    T. Chajed, J. Tassarotti, M. Theng, M. F. Kaashoek, and N. Zeldovich, “Verifying the daisynfs concurrent and crash-safe file system with se- quential reasoning,” in16th USENIX Symposium on Operating Systems Design and Implementation (OSDI). USENIX Association, 2022, pp. 447–463

    work page 2022

  35. [35]

    Vmsl: A separation logic for mechanised robust safety of virtual machines communicating above ff-a,

    Z. Liu, S. Stepanenko, J. Pichon-Pharabod, A. Timany, A. Askarov, and L. Birkedal, “Vmsl: A separation logic for mechanised robust safety of virtual machines communicating above ff-a,”Proceedings of the ACM on Programming Languages, vol. 7, no. PLDI, pp. 1438–1462, 2023

    work page 2023

  36. [36]

    Aneris: A mechanised logic for modular reasoning about distributed systems,

    M. Krogh-Jespersen, A. Timany, M. E. Ohlenbusch, S. O. Gregersen, and L. Birkedal, “Aneris: A mechanised logic for modular reasoning about distributed systems,” inProgramming Languages and Systems (ESOP), ser. Lecture Notes in Computer Science, vol. 12075. Springer, 2020, pp. 336–365

    work page 2020

  37. [37]

    Grove: A separation-logic library for verifying distributed systems,

    U. Sharma, R. Jung, J. Tassarotti, M. F. Kaashoek, and N. Zeldovich, “Grove: A separation-logic library for verifying distributed systems,” inProceedings of the 29th ACM Symposium on Operating Systems Principles (SOSP). ACM, 2023, pp. 113–129

    work page 2023

  38. [38]

    Trillium: Higher-order concurrent and distributed separation logic for intensional refinement,

    A. Timany, S. O. Gregersen, L. Stefanesco, J. K. Hinrichsen, L. Gondel- man, A. Nieto, and L. Birkedal, “Trillium: Higher-order concurrent and distributed separation logic for intensional refinement,”Proceedings of the ACM on Programming Languages, vol. 8, no. POPL, pp. 241–272, 2024

    work page 2024

  39. [39]

    Actris: Session-type based reasoning in separation logic,

    J. K. Hinrichsen, J. Bengtson, and R. Krebbers, “Actris: Session-type based reasoning in separation logic,”Proceedings of the ACM on Programming Languages, vol. 4, no. POPL, pp. 6:1–6:30, 2020

    work page 2020

  40. [40]

    A separation logic for effect handlers,

    P. E. de Vilhena and F. Pottier, “A separation logic for effect handlers,” Proceedings of the ACM on Programming Languages, vol. 5, no. POPL, pp. 33:1–33:28, 2021

    work page 2021

  41. [41]

    Cosmo: A concurrent separation logic for multicore ocaml,

    G. M ´evel, J.-H. Jourdan, and F. Pottier, “Cosmo: A concurrent separation logic for multicore ocaml,”Proceedings of the ACM on Programming Languages, vol. 4, no. ICFP, pp. 96:1–96:29, 2020

    work page 2020

  42. [42]

    Zoo: A framework for the verification of concurrent ocaml 5 programs using separation logic,

    C. Allain and G. Scherer, “Zoo: A framework for the verification of concurrent ocaml 5 programs using separation logic,”Proceedings of the ACM on Programming Languages, vol. 10, no. POPL, pp. 1702– 1729, 2026

    work page 2026

  43. [43]

    Simuliris: A separation logic framework for verifying concurrent program optimizations,

    L. G ¨aher, M. Sammler, S. Spies, R. Jung, H.-H. Dang, R. Krebbers, J. Kang, and D. Dreyer, “Simuliris: A separation logic framework for verifying concurrent program optimizations,”Proceedings of the ACM on Programming Languages, vol. 6, no. POPL, pp. 28:1–28:31, 2022

    work page 2022

  44. [44]

    Islaris: Verification of machine code against authoritative isa semantics,

    M. Sammler, A. Hammond, R. Lepigre, B. Campbell, J. Pichon- Pharabod, D. Dreyer, D. Garg, and P. Sewell, “Islaris: Verification of machine code against authoritative isa semantics,” inProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI). ACM, 2022, pp. 825– 840

    work page 2022

  45. [45]

    Cerise: Program verification on a capability machine in the presence of untrusted code,

    A. L. Georges, A. Gu ´eneau, T. Van Strydonck, A. Timany, A. Trieu, D. Devriese, and L. Birkedal, “Cerise: Program verification on a capability machine in the presence of untrusted code,”Journal of the ACM, vol. 71, no. 1, pp. 1–59, 2024

    work page 2024

  46. [46]

    Melocoton: A program logic for verified interoperability between ocaml and c,

    A. Gu ´eneau, J. Hostert, S. Spies, M. Sammler, L. Birkedal, and D. Dreyer, “Melocoton: A program logic for verified interoperability between ocaml and c,”Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA2, pp. 716–744, 2023

    work page 2023

  47. [47]

    Dimsum: A decentralized approach to multi-language semantics and verification,

    M. Sammler, S. Spies, Y . Song, E. D’Osualdo, R. Krebbers, D. Garg, and D. Dreyer, “Dimsum: A decentralized approach to multi-language semantics and verification,”Proceedings of the ACM on Programming Languages, vol. 7, no. POPL, pp. 775–805, 2023

    work page 2023

  48. [48]

    Compositional non- interference for fine-grained concurrent programs,

    D. Frumin, R. Krebbers, and L. Birkedal, “Compositional non- interference for fine-grained concurrent programs,” in2021 IEEE Sym- posium on Security and Privacy (SP). IEEE, 2021, pp. 1416–1433

    work page 2021

  49. [49]

    Cryptis: Cryptographic reasoning in separation logic,

    A. Azevedo de Amorim, A. Ahmed, and M. Gaboardi, “Cryptis: Cryptographic reasoning in separation logic,”Proceedings of the ACM on Programming Languages, vol. 10, no. POPL, pp. 2555–2585, 2026

    work page 2026

  50. [50]

    (2024) The iris coq development

    The Iris Team. (2024) The iris coq development. [Online]. Available: https://gitlab.mpi-sws.org/iris/iris

    work page 2024

  51. [51]

    (2024) Thelambda-rust(rustbelt) coq devel- opment

    The RustBelt Team. (2024) Thelambda-rust(rustbelt) coq devel- opment. [Online]. Available: https://gitlab.mpi-sws.org/iris/lambda-rust

    work page 2024

  52. [52]

    Doczkal, J.-O

    C. Doczkal, J.-O. Kaiser, and G. Smolka. (2024) Regular language representations in coq. [Online]. Available: https: //github.com/coq-community/reglang

    work page 2024

  53. [53]

    (2025) iris-lean: A port of the iris separation logic framework to lean 4

    The Iris-Lean Developers. (2025) iris-lean: A port of the iris separation logic framework to lean 4. [Online]. Available: https: //github.com/leanprover-community/iris-lean

    work page 2025

  54. [54]

    (2025) iris-lean: Porting progress tracker

    The Iris-Lean Developers. (2025) iris-lean: Porting progress tracker. [Online]. Available: https://leanprover-community.github.io/iris-lean/

    work page 2025

  55. [55]

    Hammer for coq: Automation for dependent type theory,

    Ł. Czajka and C. Kaliszyk, “Hammer for coq: Automation for dependent type theory,”Journal of Automated Reasoning, vol. 61, no. 1–4, pp. 423– 453, 2018

    work page 2018

  56. [56]

    Sledgehammer: Judgement day,

    S. B ¨ohme and T. Nipkow, “Sledgehammer: Judgement day,” inInterna- tional Joint Conference on Automated Reasoning (IJCAR). Springer, 2010, pp. 107–121

    work page 2010

  57. [57]

    Thor: Wielding hammers to integrate language models and automated theorem provers,

    A. Q. Jiang, W. Li, S. Tworkowski, K. Czechowski, T. Odrzyg ´o´zd´z, P. Miło´s, Y . Wu, and M. Jamnik, “Thor: Wielding hammers to integrate language models and automated theorem provers,” inAdvances in Neural Information Processing Systems 35 (NeurIPS), 2022

    work page 2022

  58. [58]

    Interactive proofs in higher- order concurrent separation logic,

    R. Krebbers, A. Timany, and L. Birkedal, “Interactive proofs in higher- order concurrent separation logic,” inProceedings of the 44th ACM SIG- PLAN Symposium on Principles of Programming Languages (POPL). ACM, 2017, pp. 205–217

    work page 2017

  59. [59]

    Mosel: A general, ex- tensible modal framework for interactive proofs in separation logic,

    R. Krebbers, J.-H. Jourdan, R. Jung, J. Tassarotti, J.-O. Kaiser, A. Timany, A. Chargu ´eraud, and D. Dreyer, “Mosel: A general, ex- tensible modal framework for interactive proofs in separation logic,” Proceedings of the ACM on Programming Languages, vol. 2, no. ICFP, pp. 77:1–77:30, 2018

    work page 2018

  60. [60]

    Diaframe: Automated ver- ification of fine-grained concurrent programs in iris,

    I. Mulder, R. Krebbers, and H. Geuvers, “Diaframe: Automated ver- ification of fine-grained concurrent programs in iris,” inProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI). ACM, 2022, pp. 809– 824

    work page 2022

  61. [61]

    Gpass: A goal-adaptive neural theorem prover based on Coq for automated formal verification,

    Y . Chen, Z. Sun, G. Wang, and D. Hao, “Gpass: A goal-adaptive neural theorem prover based on Coq for automated formal verification,” inProceedings of the 47th IEEE/ACM International Conference on Software Engineering (ICSE). IEEE, 2025, pp. 653–665

    work page 2025

  62. [62]

    Diversity-driven automated formal verification,

    E. First and Y . Brun, “Diversity-driven automated formal verification,” inProceedings of the 44th International Conference on Software Engi- neering (ICSE), 2022, pp. 749–761

    work page 2022

  63. [63]

    Hypertree proof search for neural theorem proving,

    G. Lample, T. Lacroix, M.-A. Lachaux, A. Rodriguez, A. Hayat, T. Lavril, G. Ebner, and X. Martinet, “Hypertree proof search for neural theorem proving,” inAdvances in Neural Information Processing Systems 35 (NeurIPS), 2022

    work page 2022

  64. [64]

    Towards neural synthesis for SMT-assisted proof-oriented programming,

    S. Chakraborty, G. Ebner, S. Bhat, S. Fakhoury, S. Fatima, S. K. Lahiri, and N. Swamy, “Towards neural synthesis for SMT-assisted proof-oriented programming,” inProceedings of the 47th IEEE/ACM International Conference on Software Engineering (ICSE), 2025, pp. 1755–1767

    work page 2025

  65. [65]

    RepairAgent: An autonomous, LLM-based agent for program repair,

    I. Bouzenia, P. Devanbu, and M. Pradel, “RepairAgent: An autonomous, LLM-based agent for program repair,” inProceedings of the 47th IEEE/ACM International Conference on Software Engineering (ICSE), 2025, pp. 2188–2200. 12

    work page 2025