Pith. sign in

REVIEW 3 major objections 5 minor 50 references

Given a security model and lemma breakdown, an agent system writes the EasyCrypt tactic scripts that used to take experts weeks or months.

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 · grok-4.5

2026-07-12 06:37 UTC pith:HMXERT75

load-bearing objection Solid systems paper: first real agent harness that finishes Phase-III EasyCrypt scripts for ChaChaPoly and MEE-CBC under expert decompositions, with honest ablations and a contamination-control set. the 3 major comments →

arxiv 2607.02847 v2 pith:HMXERT75 submitted 2026-07-03 cs.CR cs.PL

ShannonProver: Towards Automating Formal Cryptographic Proofs

Yiping Ma , Yu-Lin Tsai , Mayank Rathee , Deevashwer Rathee , Fran\c{c}ois Dupressoir , Pierre-Yves Strub , Raluca Ada Popa This is my paper
classification cs.CR cs.PL
keywords formal cryptographyEasyCryptagentic proof searchproof-state compilergame-based proofsChaCha20-Poly1305MEE-CBClemma automation
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.

Formal cryptographic proofs are too long for careful manual checking at the rate they are produced. Machine-checked scripts solve the verification problem, but writing those scripts in a system such as EasyCrypt is itself a major bottleneck even after the high-level argument is known. ShannonProver is built for the last phase of that workflow: the cryptographer supplies the security model and a decomposition of the main theorem into lemmas; the system then constructs the accepted EasyCrypt tactic scripts for those lemmas. Two design pieces make the automation practical. A proof-state compiler turns each checker state into a compact panel of live resources, program frontiers, and safe probes, so the agent spends its budget on strategy rather than name matching and type plumbing. A multi-agent tree orchestrator explores alternative branches, backtracks, and shares negative memory of failed routes. On a new corpus of EasyCrypt lemmas that includes textbook primitives, deployed protocols, and held-out expert case studies, the system fully automates Phase III for ChaCha20-Poly1305 and MEE-CBC within roughly a day and a few hundred dollars of API cost, and discharges a substantial share of the harder private CMAC lemmas. The practical claim is that cryptographers can now iterate on decompositions with machine-checked feedback instead of waiting weeks for mechanical proof engineering.

Core claim

Once a cryptographer has fixed the security model and a lemma-level decomposition, ShannonProver can automatically construct EasyCrypt proof scripts that discharge all lemmas of the public ChaCha20-Poly1305 and MEE-CBC developments (and a large share of important lemmas of a private CMAC development) in about one day of wall-clock time at a few hundred dollars of LLM cost.

What carries the argument

The proof-state compiler: a four-layer bridge that projects the EasyCrypt cursor, builds a typed ProofIR of the current layer, tracks resource liveness and the program frontier, and exposes a compact action surface of references, bindings, probes, and neutral diagnostics so the agent need not reconstruct context after every tactic.

Load-bearing premise

The expert-supplied lemma breakdown must already leave only obligations whose remaining search is mechanical for current frontier models; a single lemma that still needs a fresh high-level insight causes the system to time out and removes the claimed acceleration.

What would settle it

Re-run ShannonProver on the exact public ChaCha20-Poly1305 and MEE-CBC lemma sets with the same decomposition and models; if a non-trivial fraction of the previously solved hard invariant or game-hop lemmas now fail or require human tactic intervention beyond the reported give-up rule, the central automation claim fails.

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

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 5 minor

Summary. ShannonProver is an agentic system that automates Phase-III EasyCrypt tactic scripts once a cryptographer supplies the security model and a lemma-level decomposition of the target theorem. The system has two main components: a proof-state compiler that projects checker state into a structured, liveness-aware panel (goal layer, live resources, program frontier, probes/diagnostics), and a multi-agent tree orchestrator with backtracking, spawning, pruning, and negative memory. Evaluation comprises (i) controlled ablations of the compiler and tree policy on 40 stratified lemmas (procedural / invariant / game-hop) and (ii) case studies on ChaCha20-Poly1305, MEE-CBC, and a private CMAC development. The paper reports full automation of all lemmas in the two public case studies within roughly a day and a few hundred dollars of API cost, with EasyCrypt remaining the sole semantic authority for accepted scripts. A new EasyCrypt lemma corpus (~1.6K obligations) is assembled as a community benchmark.

Significance. If the reported results hold under the stated Phase-II/III interface, this is a substantial systems contribution to machine-checked cryptography. Writing EasyCrypt scripts for standardized schemes has historically cost expert-weeks to expert-months; automating the mechanical Phase-III layer at the scale of ChaCha20-Poly1305 and MEE-CBC is therefore practically meaningful. Strengths that should be credited explicitly: final artifacts are machine-checked by EasyCrypt (LLM errors cannot compromise soundness of accepted scripts); the evaluation includes a private CMAC corpus as a contamination control; the paper contributes what appears to be the first systematic EasyCrypt cryptographic-proof dataset; and the ablations cleanly separate interface effects (error friction) from search effects (solve rate on invariant/game-hop lemmas). The work is a credible first step toward agent-assisted formal crypto development, even if Phase-II decomposition remains expert-owned.

major comments (3)
  1. [§1, Fig. 1, §5.4] §1, Fig. 1, and §5.4: The central empirical claim—full Phase-III automation for ChaCha20-Poly1305 and MEE-CBC—is demonstrated only on expert decompositions from already-completed developments whose lemmas were known to be finishable. The paper correctly draws the Phase-II/III boundary and treats timeouts as decomposition feedback, but the broader claim that agents let cryptographers “iterate more quickly on new constructions” (§1, abstract) is not yet quantified: there is no measurement of how often a natural first-pass expert decomposition of a new construction leaves even one landmark lemma that still requires novel high-level insight rather than tactic search. Please strengthen the limitation discussion (and, if feasible, add a small analysis of near-timeout / high-cost lemmas as a proxy for decomposition sensitivity) so the workflow-acceleration narrative is proportionate to the evid
  2. [§5.1–§5.3, Fig. 7–8] §5.1–§5.3: The ablations rest on a single sample of 40 lemmas and (apparently) single-run agent trajectories under a stochastic frontier model (Opus 4.8, high thinking). Given that solve-rate gains for invariant and game-hop lemmas (67% → 90%) and the error-friction reductions are load-bearing for the systems claims, the manuscript should report either multi-seed/multi-run variance or a clear statement of how many independent attempts underlie each bar, plus the exact sampling procedure used to choose the 40 lemmas from the 1.6K corpus. Without this, it is hard to judge stability of the reported deltas.
  3. [§4.3, §5] §4.3 and §5: The orchestrator’s spawn/prune thresholds and negative-memory policy are free parameters of the search (also noted as such in the evaluation setup). The tree ablation attributes large solve-rate gains on I/G lemmas to multi-agent orchestration, but no sensitivity analysis is given. A short appendix table varying spawn/prune criteria (or at least documenting the concrete thresholds used for the reported runs) is needed so that the multi-agent gains can be reproduced and assessed as robust rather than tuned to the case studies.
minor comments (5)
  1. [§5.4, Fig. 9] Fig. 9 quality dots (C/M/S) and the “tesuji” stars are useful but under-specified in the main text; a short formal definition of the three axes and of how human vs. agent proofs were compared (including who labeled them) would help readers interpret the figure without Appendix D alone.
  2. [§5.2] The measurement pipeline in §5.2 uses an LLM to label some unproductive windows that a parser cannot classify. Please state which model was used for labeling and whether labels were spot-checked by humans, to avoid circular reliance on LLM judgment for the friction metric.
  3. [Appendix C, §5] Appendix C’s four-part benchmark design is a valuable contribution; consider elevating a one-paragraph summary of the public/private split and contamination-control rationale into the main evaluation section so readers see why CMAC is held out.
  4. [Throughout / References] Minor presentation: “ShannonProver” vs. “Shannon-Prover” hyphenation is inconsistent in a few places; also fix “François Dupressoir” / “Dupressoiret al.” typography in the references list where present.
  5. [Fig. 2, Fig. 5] Fig. 2 and Fig. 5 are dense but informative; ensure that in the camera-ready version the “LIVE / BLOCKED” and frontier annotations remain legible at single-column width.

Circularity Check

0 steps flagged

No significant circularity: empirical systems evaluation of agent-written EasyCrypt scripts, verified by an external deterministic checker on expert-supplied decompositions and a private contamination-control corpus.

full rationale

ShannonProver is a systems paper whose load-bearing claims are measured performance numbers (solve rates, API cost, wall-clock time, ablation deltas) on lemma-level EasyCrypt obligations. Success is defined solely by acceptance of the produced tactic scripts by the EasyCrypt checker; the checker is an independent, deterministic authority outside the authors’ control. The evaluation uses a newly assembled corpus of ~1.6K lemmas spanning textbook, deployed, and post-quantum developments, plus a private CMAC development held out precisely as a memorization/contamination control. Prior EasyCrypt developments co-authored by some of the present authors appear only as case-study targets (ChaCha20-Poly1305, MEE-CBC, CMAC), not as load-bearing uniqueness theorems, fitted parameters, or definitional premises that force the reported results. There is no self-definitional equation, no fitted input re-labeled as a prediction, no ansatz smuggled via self-citation, and no renaming of a known empirical pattern. The Phase-II/Phase-III boundary is an explicit scope assumption, not a circular reduction. Consequently the derivation chain is self-contained against external benchmarks and exhibits zero circularity of the kinds enumerated.

Axiom & Free-Parameter Ledger

2 free parameters · 3 axioms · 2 invented entities

The paper is an empirical systems contribution. Its load-bearing premises are the soundness of EasyCrypt, the availability of a frontier LLM with tool-use, and the assumption that expert lemma decompositions leave only mechanically searchable obligations. No numerical free parameters are fitted to produce the central performance claims; the invented entities are engineering constructs whose utility is measured by the evaluation rather than postulated as physical or mathematical objects.

free parameters (2)
  • LLM choice and thinking-effort setting (Opus 4.8 high)
    All reported solve rates and costs are obtained with one proprietary model and one thinking-effort setting; different models or temperatures would change absolute numbers.
  • Orchestrator spawn/prune thresholds and negative-memory policy
    The multi-agent policy contains discrete control parameters that affect solve rate; they are described but not systematically ablated beyond the single-agent vs. orchestrator comparison.
axioms (3)
  • domain assumption EasyCrypt’s probabilistic relational Hoare logic and tactic engine are sound; any script it accepts is a correct proof of the stated lemma.
    Stated throughout as the trust boundary; the system never overrides the checker.
  • domain assumption Current frontier LLMs, when given a sufficiently rich state-aware interface, can select and instantiate the next EasyCrypt tactic for a large class of cryptographic lemmas.
    The entire empirical claim rests on this capability; the paper demonstrates it for the evaluated set but does not prove it for arbitrary lemmas.
  • ad hoc to paper Expert-supplied lemma decompositions already isolate obligations that do not require further creative high-level insight.
    Explicit Phase-II / Phase-III boundary (Fig. 1 and §1); if false, the system times out and the claimed acceleration fails.
invented entities (2)
  • Proof-state compiler (four cumulative layers: state projection, ProofIR, resource liveness/frontier, action surface) independent evidence
    purpose: Deterministically assemble a compact, state-aware panel of live resources, bindings and probes so the agent need not reconstruct context after every tactic.
    Core architectural contribution; its utility is measured by the compiler ablation (error-friction reduction) rather than postulated a priori.
  • Multi-agent tree-based proof orchestration with negative memory independent evidence
    purpose: Explore alternative proof routes, spawn on stalls, prune unproductive branches and share failed tactic shapes across agents.
    Second core design idea; measured by the tree-search ablation (solve-rate lift on invariant and game-hop lemmas).

pith-pipeline@v1.1.0-grok45 · 32600 in / 3221 out tokens · 36904 ms · 2026-07-12T06:37:56.407128+00:00 · methodology

0 comments
read the original abstract

Cryptographic proofs are produced at a scale that increasingly exceeds the community's ability to verify them manually. Machine-checked proofs offer a path toward scalable proof verification, but writing proof scripts for expressive proof assistants such as EasyCrypt remains a major bottleneck: even when the high-level proof plan is known, converting it into proof tactics requires substantial reasoning effort. This paper presents ShannonProver, an agentic framework for automating cryptographic proofs. ShannonProver targets the setting in which a cryptographer provides the security model and a decomposition of the target theorem into lemma-level proof obligations, while the system automatically constructs EasyCrypt proof scripts for those obligations. We evaluate ShannonProver on a dataset of formal cryptographic proofs in EasyCrypt. The dataset spans textbook primitives, deployed protocols, and standardization efforts such as NIST proposals, and includes expert case studies drawn from a corpus that has not previously been available online. We show that ShannonProver can automate substantial portions of cryptographic proof engineering for case studies such as ChaChaPoly1305 and MEE-CBC. More broadly, this work suggests a path toward accelerating cryptographic research: as agents automate the proof-engineering burden, cryptographers can iterate more quickly on new constructions, obtain machine-checked assurance earlier, and bring trustworthy protocols from design to deployment faster.

Figures

Figures reproduced from arXiv: 2607.02847 by Deevashwer Rathee, Fran\c{c}ois Dupressoir, Mayank Rathee, Pierre-Yves Strub, Raluca Ada Popa, Yiping Ma, Yu-Lin Tsai.

Figure 1
Figure 1. Figure 1: Large-scale cryptographic formal proof development proceeds [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Agent interaction with EasyCrypt, with and without ShannonProver’s proof-context manager. In the direct checker-in-the-loop baseline, the agent [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: The tactic pyramid. The layers organize tactics by proof-state [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Cumulative layers for ShannonProver’s proof-state compiler. [PITH_FULL_IMAGE:figures/full_fig_p006_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: The compiler view at a single proof state. [PITH_FULL_IMAGE:figures/full_fig_p007_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: A proof tree evolving over a search. (a) Two agents start from the initial state (root) and each advances one state. (b) Both extend their branch by one more accepted edge. (c) Agent 1 stalls; the orchestrator spawns a child (Agent 1.0) from the parent node of Agent 1 to take a different edge, while Agent 2 keeps progressing. (d) The stalled branch makes no further progress and is pruned (×); the child con… view at source ↗
Figure 7
Figure 7. Figure 7: Compiler ablation on lemma pairs that both cases proved, grouped [PITH_FULL_IMAGE:figures/full_fig_p011_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Tree-search ablation, grouped by proof shape ( [PITH_FULL_IMAGE:figures/full_fig_p012_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Per-lemma API cost for ChaCha20-Poly1305 project solved by AI agents, grouped by proof shape ( [PITH_FULL_IMAGE:figures/full_fig_p013_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: ShannonProver’s current managed-prover architecture. A long-lived prover agent sees only a [PITH_FULL_IMAGE:figures/full_fig_p017_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Per-lemma API cost for MEE-CBC lemmas solved by AI agents, grouped by proof shape ( [PITH_FULL_IMAGE:figures/full_fig_p019_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Per-lemma API cost for held-out CMAC lemmas solved by AI agents, grouped by proof shape ( [PITH_FULL_IMAGE:figures/full_fig_p019_12.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

50 extracted references · 4 linked inside Pith

  1. [1]

    A plausible approach to computer-aided cryptographic proofs,

    S. Halevi, “A plausible approach to computer-aided cryptographic proofs,” Cryptology ePrint Archive, Paper 2005/181, 2005

    2005

  2. [2]

    FIPS 202: SHA-3 standard: Permutation-based hash and extendable-output functions,

    National Institute of Standards and Technology, “FIPS 202: SHA-3 standard: Permutation-based hash and extendable-output functions,” Federal Information Processing Standards Publication 202, 2015

    2015

  3. [3]

    FIPS 197: Advanced encryption standard (AES),

    National Institute of Standards and Technology, “FIPS 197: Advanced encryption standard (AES),” Federal Information Processing Stan- dards Publication 197, 2023

    2023

  4. [4]

    FIPS 203: Module- lattice-based key-encapsulation mechanism standard,

    National Institute of Standards and Technology, “FIPS 203: Module- lattice-based key-encapsulation mechanism standard,” Federal Infor- mation Processing Standards Publication 203, 2024

    2024

  5. [5]

    The transport layer security (TLS) protocol version 1.3,

    E. Rescorla, “The transport layer security (TLS) protocol version 1.3,” RFC 8446, 2018

    2018

  6. [6]

    The security impact of a new cryptographic library,

    D. J. Bernstein, T. Lange, and P. Schwabe, “The security impact of a new cryptographic library,” inProgress in Cryptology – LATINCRYPT 2012, ser. Lecture Notes in Computer Science, vol. 7533. Springer, 2012, pp. 159–176

    2012

  7. [7]

    libsodium documentation,

    libsodium contributors, “libsodium documentation,” https://doc. libsodium.org/, accessed 2026-05-09

    2026

  8. [8]

    OpenSSL: Cryptography and SS- L/TLS toolkit,

    OpenSSL Software Foundation, “OpenSSL: Cryptography and SS- L/TLS toolkit,” https://www.openssl.org/, accessed 2026-05-09

    2026

  9. [9]

    EverCrypt: A fast, verified, cross-platform cryptographic provider,

    J. Protzenko, B. Parno, A. Fromherz, C. Hawblitzel, M. Polubelova, K. Bhargavan, B. Beurdouche, J. Choi, A. Delignat-Lavaud, C. Four- net, N. Kulatova, T. Ramananandro, A. Rastogi, N. Swamy, C. M. Wintersteiger, and S. Zanella-Béguelin, “EverCrypt: A fast, verified, cross-platform cryptographic provider,” in2020 IEEE Symposium on Security and Privacy. IEE...

    2020

  10. [10]

    Using TLS to secure QUIC,

    M. Thomson and S. Turner, “Using TLS to secure QUIC,” RFC 9001, 2021

    2021

  11. [11]

    A formal security analysis of the Signal messaging pro- tocol,

    K. Cohn-Gordon, C. J. F. Cremers, B. Dowling, L. Garratt, and D. Stebila, “A formal security analysis of the Signal messaging pro- tocol,” in2017 IEEE European Symposium on Security and Privacy (EuroS&P). IEEE, 2017, pp. 451–466

    2017

  12. [12]

    WireGuard: Next generation kernel network tun- nel,

    J. A. Donenfeld, “WireGuard: Next generation kernel network tun- nel,” in24th Annual Network and Distributed System Security Sym- posium (NDSS 2017). Internet Society, 2017

    2017

  13. [13]

    Artifact for formally verifying kyber episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt,

    J. B. Almeida, S. A. Olmos, M. Barbosa, G. Barthe, F. Dupres- soir, B. Grégoire, V . Laporte, J.-C. Léchenet, C. Low, T. Oliveira, H. Pacheco, M. Quaresma, P. Schwabe, and P.-Y . Strub, “Artifact for formally verifying kyber episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt,” IACR Artifact Archive, crypto/2024/a3, 2024

    2024

  14. [14]

    A tight security proof for SPHINCS+, formally verified,

    M. Barbosa, F. Dupressoir, A. Hülsing, M. Meijers, and P.-Y . Strub, “A tight security proof for SPHINCS+, formally verified,” inAd- vances in Cryptology – ASIACRYPT 2024, ser. Lecture Notes in Computer Science, vol. 15487. Springer, 2024, pp. 35–67

    2024

  15. [15]

    Computer- aided security proofs for the working cryptographer,

    G. Barthe, B. Grégoire, S. Heraud, and S. Z. Béguelin, “Computer- aided security proofs for the working cryptographer,” inAdvances in Cryptology – CRYPTO 2011, ser. Lecture Notes in Computer Science, vol. 6841. Springer, 2011, pp. 71–90

    2011

  16. [16]

    The Lean 4 theorem prover and programming language,

    L. de Moura and S. Ullrich, “The Lean 4 theorem prover and programming language,” inAutomated Deduction – CADE 28, ser. Lecture Notes in Computer Science, vol. 12699. Springer, 2021, pp. 625–635

    2021

  17. [17]

    Bertot and P

    Y . Bertot and P. Castéran,Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions, ser. Texts in Theoretical Computer Science. Springer, 2004

    2004

  18. [18]

    Dependent types and multi-monadic effects in F*,

    N. Swamy, C. Hri¸ tcu, C. Keller, A. Rastogi, A. Delignat-Lavaud, S. Forest, K. Bhargavan, C. Fournet, P.-Y . Strub, M. Kohlweiss, J.- K. Zinzindohoué, and S. Zanella-Béguelin, “Dependent types and multi-monadic effects in F*,” inProceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 2016, pp. 256–270

    2016

  19. [19]

    Modeling and verifying security protocols with the applied pi calculus and ProVerif,

    B. Blanchet, “Modeling and verifying security protocols with the applied pi calculus and ProVerif,”Foundations and Trends in Privacy and Security, vol. 1, no. 1–2, pp. 1–135, 2016

    2016

  20. [20]

    The TAMARIN prover for the symbolic analysis of security protocols,

    S. Meier, B. Schmidt, C. Cremers, and D. Basin, “The TAMARIN prover for the symbolic analysis of security protocols,” inComputer Aided Verification, ser. Lecture Notes in Computer Science, vol. 8044. Springer, 2013, pp. 696–701

    2013

  21. [21]

    Verifiable side-channel security of cryptographic implementations: Constant- time MEE-CBC,

    J. B. Almeida, M. Barbosa, G. Barthe, and F. Dupressoir, “Verifiable side-channel security of cryptographic implementations: Constant- time MEE-CBC,” inFast Software Encryption (FSE), 2016

    2016

  22. [22]

    For- mal security proof of cmac and its variants,

    C. Baritel-Ruet, F. Dupressoir, P.-A. Fouque, and B. Grégoire, “For- mal security proof of cmac and its variants,” in2018 IEEE 31st Computer Security Foundations Symposium (CSF). IEEE, 2018, pp. 91–104

    2018

  23. [23]

    The last mile: High-assurance and high-speed cryptographic implementations,

    J. B. Almeida, M. Barbosa, G. Barthe, B. Grégoire, A. Koutsos, V . La- porte, T. Oliveira, and P.-Y . Strub, “The last mile: High-assurance and high-speed cryptographic implementations,” inIEEE Symposium on Security and Privacy, 2020

    2020

  24. [24]

    Formally verifying kyber: Episode iv: Implementation correctness,

    J. B. Almeida, M. Barbosa, G. Barthe, B. Grégoire, V . Laporte, J.-C. Léchenet, T. Oliveira, H. Pacheco, M. Quaresma, P. Schwabeet al., “Formally verifying kyber: Episode iv: Implementation correctness,” IACR Transactions on Cryptographic Hardware and Embedded Sys- tems, vol. 2023, no. 3, pp. 164–193, 2023

    2023

  25. [25]

    Formally verifying kyber episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt,

    J. B. Almeida, S. A. Olmos, M. Barbosa, G. Barthe, F. Dupres- soir, B. Grégoire, V . Laporte, J.-C. Léchenet, C. Low, T. Oliveira, H. Pacheco, M. Quaresma, P. Schwabe, and P.-Y . Strub, “Formally verifying kyber episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt,” inAdvances in Cryptology – CRYPTO 2024, ser. Lecture Notes i...

    2024

  26. [26]

    A. V . Aho, M. S. Lam, R. Sethi, and J. D. Ullman,Compilers: Principles, Techniques, and Tools, 2nd ed. Addison-Wesley, 2006

    2006

  27. [27]

    Generative language modeling for auto- mated theorem proving,

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

    Pith/arXiv arXiv 2009

  28. [28]

    MiniF2F: A cross-system bench- mark for formal olympiad-level mathematics,

    K. Zheng, J. M. Han, and S. Polu, “MiniF2F: A cross-system bench- mark for formal olympiad-level mathematics,” inICLR, 2022

    2022

  29. [29]

    Formal certification of code-based cryptographic proofs,

    G. Barthe, B. Grégoire, and S. Z. Béguelin, “Formal certification of code-based cryptographic proofs,” inPOPL, 2009

    2009

  30. [30]

    Principles for pRHL proofs,

    M. Barbosa, F. Dupressoiret al., “Principles for pRHL proofs,” Cryptology ePrint Archive, Paper 2026/1334, 2026

    2026

  31. [31]

    CryptHOL: Game- based proofs in higher-order logic,

    D. A. Basin, A. Lochbihler, and S. R. Sefidgar, “CryptHOL: Game- based proofs in higher-order logic,”Journal of Cryptology, 2020

    2020

  32. [32]

    Ssprove: A foundational framework for modular cryptographic proofs in coq,

    P. G. Haselwarter, E. Rivas, A. Van Muylder, T. Winterhalter, C. Abate, N. Sidorenco, C. Hri¸ tcu, K. Maillard, and B. Spitters, “Ssprove: A foundational framework for modular cryptographic proofs in coq,”ACM transactions on programming languages and systems, vol. 45, no. 3, pp. 1–61, 2023

    2023

  33. [33]

    The foundational cryptography frame- work,

    A. Petcher and G. Morrisett, “The foundational cryptography frame- work,” inPrinciples of Security and Trust (POST), 2015

    2015

  34. [34]

    A computationally sound mechanized prover for se- curity protocols,

    B. Blanchet, “A computationally sound mechanized prover for se- curity protocols,”IEEE Transactions on Dependable and Secure Computing, 2008

    2008

  35. [35]

    HACL*: A verified modern cryptographic library,

    J.-K. Zinzindohoué, K. Bhargavan, J. Protzenko, and B. Beurdouche, “HACL*: A verified modern cryptographic library,” inACM CCS, 2017

    2017

  36. [36]

    Jasmin: High-assurance and high-speed cryptography,

    J. B. Almeida, M. Barbosa, G. Barthe, A. Blot, B. Grégoire, V . La- porte, T. Oliveira, H. Pacheco, B. Schmidt, and P.-Y . Strub, “Jasmin: High-assurance and high-speed cryptography,” inACM CCS, 2017

    2017

  37. [37]

    Machine-checked security for XMSS as in RFC 8391 and SPHINCS+,

    M. Barbosa, F. Dupressoir, B. Grégoire, A. Hülsing, M. Meijers, and P.-Y . Strub, “Machine-checked security for XMSS as in RFC 8391 and SPHINCS+,” inAdvances in Cryptology – CRYPTO 2023, ser. Lecture Notes in Computer Science, vol. 14085. Springer, 2023, pp. 421–454. 15

    2023

  38. [38]

    Machine-checked proofs for cryptographic standards: Indifferentia- bility of sponge and secure high-assurance implementations of SHA- 3,

    J. B. Almeida, C. Baritel-Ruet, M. Barbosa, G. Barthe, F. Dupressoir, B. Grégoire, V . Laporte, T. Oliveira, A. Stoughton, and P.-Y . Strub, “Machine-checked proofs for cryptographic standards: Indifferentia- bility of sponge and secure high-assurance implementations of SHA- 3,” inACM CCS, 2019

    2019

  39. [39]

    Vcvio: Veri- fied cryptography in lean via oracle effects and handlers,

    D. Tuma, Q. Dao, J. Waters, A. Hicks, and N. Hopper, “Vcvio: Veri- fied cryptography in lean via oracle effects and handlers,”Cryptology ePrint Archive, 2026

    2026

  40. [40]

    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,”Advances in neural information processing systems, vol. 35, pp. 26 337–26 349, 2022

    2022

  41. [41]

    DeepSeek-Prover-V1.5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search,

    H. Xinet al., “DeepSeek-Prover-V1.5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search,” arXiv preprint arXiv:2408.08152, 2024

    Pith/arXiv arXiv 2024

  42. [42]

    DeepSeek-Prover-V2: Advancing formal mathemati- cal reasoning via reinforcement learning for subgoal decomposition,

    DeepSeek-AI, “DeepSeek-Prover-V2: Advancing formal mathemati- cal reasoning via reinforcement learning for subgoal decomposition,” arXiv preprint arXiv:2504.21801, 2025

    Pith/arXiv arXiv 2025

  43. [43]

    Goedel-prover: A frontier model for open-source automated theorem proving,

    Y . Lin, S. Tang, B. Lyu, J. Wu, H. Lin, K. Yang, J. LI, M. Xia, D. Chen, S. Aroraet al., “Goedel-prover: A frontier model for open-source automated theorem proving,” inSecond Conference on Language Modeling, 2025

    2025

  44. [44]

    Olympiad-level formal mathematical reasoning with reinforcement learning,

    T. Hubert, R. Mehta, L. Sartran, M. Z. Horváth, G. Žuži ´c, E. Wieser, A. Huang, J. Schrittwieser, Y . Schroecker, H. Masoomet al., “Olympiad-level formal mathematical reasoning with reinforcement learning,”Nature, pp. 1–3, 2025

    2025

  45. [45]

    ProofNet: Autoformalizing and formally proving undergraduate-level mathematics,

    Z. Azerbayev, B. Piotrowski, H. Schoelkopf, E. W. Ayers, D. Radev, and J. Avigad, “ProofNet: Autoformalizing and formally proving undergraduate-level mathematics,”arXiv preprint arXiv:2302.12433, 2023

    Pith/arXiv arXiv 2023

  46. [46]

    Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition,

    G. Tsoukalas, J. Lee, J. Jennings, J. Xin, M. Ding, M. Jennings, A. Thakur, and S. Chaudhuri, “Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition,”Advances in Neural Information Processing Systems, vol. 37, pp. 11 545–11 569, 2024

    2024

  47. [47]

    Leandojo: Theorem proving with retrieval-augmented language models,

    K. Yang, A. Swope, A. Gu, R. Chalamala, P. Song, S. Yu, S. Godil, R. J. Prenger, and A. Anandkumar, “Leandojo: Theorem proving with retrieval-augmented language models,”Advances in Neural Informa- tion Processing Systems, vol. 36, pp. 21 573–21 612, 2023

    2023

  48. [48]

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

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

    2022

  49. [49]

    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, 2023, pp. 1229–1241

    2023

  50. [50]

    CatCrypt,

    B. Spitterset al., “CatCrypt,” Cryptology ePrint Archive, Paper 2026/604, 2026. Appendix A. Deferred Explanations of Concepts A.1. Proof resources Byproof resources, we mean pieces of information that can help discharge the current goal, including facts already in the proof, previously proved lemmas, module and type information, and the program structure ...

    2026