Pith. sign in

REVIEW 2 major objections 5 minor 42 references

Formal Disco uses LLM workers and entropy maximization to generate large synthetic corpora of verified programs, training open models that match frontier systems on verification tasks.

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-11 16:06 UTC pith:HJ5QDOFT

load-bearing objection Solid systems paper that actually ships the data and shows open models catching Claude on verification tasks; the entropy story is useful but secondary to the engineering. the 2 major comments →

arxiv 2607.04631 v1 pith:HJ5QDOFT submitted 2026-07-06 cs.AI

Formal Disco: Scalable Open-Ended Generation of Formally Verified Programs

Gabriel Poesia , Simon Henniger , Tzu-Han Hsu , Yilun Du , Nada Amin This is my paper
classification cs.AI
keywords formal verificationsynthetic data generationDafnyVerusFrama-Centropy maximizationLLM agentsprogram synthesis
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 verification gives the strongest correctness guarantees for code, but verification-aware languages have almost no public training data, so AI models cannot help write or prove them. This paper argues that the data barrier can be broken by open-ended synthetic generation: a distributed system of LLM workers that sketch programs from random open-source READMEs and language documentation, repair them under compiler and verifier feedback, and extend working programs into larger ones. A principle of maximum entropy over program features steers both the system design and iterative fine-tuning so that each round produces not only more successes but more diverse programs, avoiding the usual collapse of self-training. The released datasets in Dafny, Verus, and Frama-C contain over 100,000 verified programs; fine-tuning an open 32B coder on data extracted from them roughly doubles annotation success on human Dafny benchmarks and matches Claude 4.5 Opus Pass@1 on Verus annotation. If the approach holds, new formal languages need not wait decades for human corpora before AI assistance becomes useful.

Core claim

Coordinating three classes of LLM workers—initiators seeded by random READMEs and documentation snippets, fixers that patch verifier errors, and extenders that grow verified programs—together with iterative supervised fine-tuning that keeps only the most feature-surprising successful traces, yields large, increasingly diverse synthetic corpora of formally verified programs. Training open models on data extracted from those corpora produces substantial gains on human-written verification benchmarks, in places matching Claude 4.5 Opus.

What carries the argument

The principle of maximum entropy for synthetic program generation: Shannon entropy over discrete program features (annotations per method, lemma and method body sizes, loop skeletons) is maximized by ranking successful worker traces by minimum surprisal rank and fine-tuning only on the top third each iteration, so successive corpora grow both in success rate and in feature diversity.

Load-bearing premise

That maximizing entropy over a small hand-chosen set of program features, seeded by random READMEs and documentation, yields synthetic data diverse enough that fine-tuning on it improves models on real human-written verification tasks.

What would settle it

Fine-tune the same open model on a size-matched Formal Disco corpus versus a non-entropy-maximized or randomly varied synthetic corpus and check whether the entropy-maximized model fails to outperform the baseline on DafnyBench and VerusBench annotation and lemma-proving Pass@k.

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

If this is right

  • New verification-aware languages can launch with large synthetic training sets instead of waiting for human corpora.
  • Open models can reach competitive verification performance without proprietary data or closed-model APIs at inference time.
  • Explicit entropy objectives over program features can counteract diversity collapse when models train on their own outputs.
  • Rarefaction curves of feature entropy become a practical way to compare heterogeneous program datasets beyond raw size.
  • The same agenda-and-worker architecture can be retargeted to other formal domains that have a machine-checkable correctness signal.

Where Pith is reading between the lines

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

  • The same initiator–fixer–extender loop with entropy ranking could generate training data for interactive theorem provers where human formalizations are scarce, not only for auto-active verifiers.
  • If hand-chosen features leave annotation-template diversity below human corpora, automatically searching for features that best predict downstream benchmark gains would further close the remaining gap.
  • Joint multi-language runs might transfer verification idioms across Dafny, Verus, and Frama-C rather than training each language in isolation.

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

2 major / 5 minor

Summary. The paper introduces FormalDisco, a distributed multi-agent system for open-ended synthetic generation of formally verified programs. Three LLM workers (Initiator, Fixer, Extender) collaborate via a shared agenda, seeded by random GitHub READMEs and language-reference snippets. The authors propose a maximum-entropy principle over program features and operationalize it via iterative supervised fine-tuning that retains only the top third of successful traces by minimum surprisal rank. They release large verified corpora in Dafny, Verus, and Frama-C (>100k programs), show that self-improved open models match or exceed the seed Claude workers on generation tasks while increasing feature entropy, and demonstrate that fine-tuning Qwen2.5-Coder-32B on data extracted from these corpora roughly doubles Pass@16 on DafnyBench annotation, matches Claude 4.5 Opus Pass@1 on VerusBench annotation, and yields large gains on Dafny lemma proving.

Significance. Data scarcity has long limited LLM progress on verification-aware languages. FormalDisco supplies a language-agnostic, verifier-grounded pipeline that produces large public datasets and open models competitive with a frontier system on several verification tasks. Strengths include: (i) an external, non-circular success signal from compilers/verifiers; (ii) held-out evaluation on human-written DafnyBench and VerusBench; (iii) rarefaction-curve comparisons and ablations of the multi-worker design, READMEs, and documentation snippets; (iv) released code and datasets. The entropy-maximization framing and the demonstration that self-training need not collapse diversity are methodologically useful beyond this domain. If the transfer results hold under broader scrutiny, the work offers a practical path for new formal languages to bootstrap AI assistance without decades of human corpora.

major comments (2)
  1. Abstract and §1 claim that fine-tuned models often match or exceed Claude Opus 4.5. On VerusBench annotation Pass@1 this is accurate (43% = 43%), and on DafnyBench annotation Pass@16 matches Opus Pass@1. On the lemma-proving task (§4.3, Fig. 6), however, Opus remains substantially stronger (61.6% vs 25.5% Pass@1). The fine-tuned models are also trained without chain-of-thought while the Opus baseline uses CoT. The claim should be scoped explicitly to the annotation tasks (or to Pass@k regimes) so that the abstract does not overstate the lemma-proving result.
  2. §3.3 and §5: entropy maximization is performed over four hand-chosen features (annotations per method, lemma body size, loop skeletons, method body size). Rarefaction curves (Fig. 4) show that on unoptimized features—especially annotation templates—human DafnyBench remains more diverse. The paper already notes this limitation, but the central transfer story would be stronger with either (a) a sensitivity analysis over alternative feature sets or (b) an explicit argument why the four chosen features are the ones most relevant to the downstream annotation and lemma tasks. Without that, it remains possible that gains come mainly from scale and verifier filtering rather than from the entropy objective itself.
minor comments (5)
  1. Downstream evaluation (§4.3) covers Dafny and Verus only; Frama-C is used for generation and diversity analysis but not for task transfer. A short note on why Frama-C was omitted from SFT evaluation (or a small pilot) would round out the three-language claim.
  2. Figure numbering in the manuscript dump is inconsistent: the main rarefaction panel is labeled Figure 4 in the text but later referred to as Figure 8; appendix rarefaction figures are also numbered 8–10. Please renumber for the camera-ready version.
  3. Table 3 reports that Verus lemma-body median size decreases slightly under Qwen self-improvement (5 → 3) while p90 rises modestly. A one-sentence interpretation in §4.2 would help readers who might otherwise read this as partial diversity collapse on that feature.
  4. The free parameters of the pipeline (msr top-1/3 fraction, max repair attempts = 3, K = 10k/30k, LoRA r=32) are listed in the appendix but not ablated. Even a brief statement that the top-1/3 threshold was not tuned on the downstream benchmarks would reassure readers about selection bias.
  5. Related work on synthetic data for Lean/Isabelle (AlphaGeometry, DeepSeek-Prover, Goedel-Prover) is cited; a sentence contrasting open-ended joint generation of specs+impls+proofs with statement-conditioned proof search would sharpen the positioning.

Circularity Check

0 steps flagged

No significant circularity: verifier feedback and held-out human benchmarks supply external signals; entropy ranking is an explicit training objective, not a claimed first-principles prediction.

full rationale

FORMALDISCO is a systems/ML paper whose load-bearing claims are empirical, not a derivation that reduces outputs to inputs by construction. Success of initiator/fixer/extender workers is judged by an external compiler/verifier (Dafny, Verus, Frama-C), independent of the generation model. Entropy maximization (Eqs. 1–5, Section 3.3) ranks distillation examples by minimum surprisal rank over four hand-chosen features and filters SFT to the top third; subsequent rises in those same feature entropies (Figure 3) are the intended effect of the filter, not a disguised prediction of an external quantity. Diversity on unoptimized features is separately reported via rarefaction curves (Figure 4), and ablations remove READMEs and documentation snippets to show external-seed contributions (Figure 7). Downstream evaluation extracts annotation and lemma-proving SFT data from the synthetic corpora and measures Pass@k on held-out human-written DafnyBench and VerusBench programs never seen during generation (Figures 5–6), with a SAFE-matched control on Verus. Self-citations (e.g., dafny-annotator) are background, not uniqueness theorems or load-bearing premises. No equation equates a claimed prediction to a fitted parameter; no ansatz is smuggled in via overlapping-author uniqueness results. The transfer assumption (entropy over four features yields useful human-benchmark data) is a scientific hypothesis already tested by the paper’s own benchmarks, not a circular reduction.

Axiom & Free-Parameter Ledger

5 free parameters · 3 axioms · 2 invented entities

The central claims rest on standard LLM fine-tuning practice, the soundness of the three external verifiers, and a small set of design choices (feature set, filtering fraction, seed sources). No new physical or mathematical entities are postulated; free parameters are ordinary hyperparameters.

free parameters (5)
  • msr top-1/3 filtering fraction
    Only the top third of successful examples ranked by minimum surprisal rank are used for each SFT iteration; the fraction is chosen by hand.
  • max repair attempts = 3
    Hard-coded limit before a repair task is marked failed.
  • task attempts K (10k Claude / 30k Qwen)
    Budget per generation run, chosen for cost/scale trade-off.
  • LoRA rank r=32, α=64, 15k steps, lr=2e-4
    Standard fine-tuning hyperparameters listed in Table 2; not derived.
  • four hand-chosen entropy features
    Annotations-per-method, lemma size, loop skeleton, method size; selection is design choice, not learned.
axioms (3)
  • domain assumption The external verifiers (Dafny, Verus, Frama-C/WP) correctly classify programs as verified or not.
    All success signals and training labels rest on this; standard for the field.
  • ad hoc to paper Shannon entropy of the empirical feature distribution is a useful proxy for dataset quality for downstream verification tasks.
    Core design principle of Section 3.1; supported by ablations but not proven optimal.
  • domain assumption Random GitHub READMEs and language-reference snippets supply non-collapsing theme and feature entropy.
    Ablations in Section 4.4 confirm collapse without them; assumed transferable.
invented entities (2)
  • FORMALDISCO agenda + three specialized workers (Initiator/Fixer/Extender) independent evidence
    purpose: Coordinate open-ended verified-program generation at scale
    New system architecture; independent evidence is the released code and datasets.
  • minimum surprisal rank (msr) ranking for entropy-max SFT independent evidence
    purpose: Select training examples that most increase feature entropy
    New filtering rule derived from the entropy decomposition; evidence is the rising entropy curves.

pith-pipeline@v1.1.0-grok45 · 38677 in / 2821 out tokens · 45201 ms · 2026-07-11T16:06:26.010341+00:00 · methodology

0 comments
read the original abstract

The cost of producing code is rapidly diminishing with increasingly capable AI agents, while quality assurance of generated programs has not kept pace. Formal verification provides the strongest possible guarantees, but the ability of AI models to work with verification-aware languages is hindered by the scarcity of human-written examples of programs in those languages. To tackle this prevalent data scarcity issue, we propose Formal Disco: a distributed system for coordination of LLM-based workers that can be easily applied to open-ended synthetic data generation at scale. We use Formal Disco to share tasks and programs between three classes of workers: "initiators", which read random READMEs from open-source repositories and documentation snippets to sketch a related verified program, "fixers" which take compiler and verifier feedback and attempt to resolve issues, and "extenders" that take working programs and propose patches to expand them. Formal Disco records all agent-generated traces and uses them both for initial distillation from a stronger model as well as self-improvement. We also propose a principle of maximum entropy for synthetic program generation, and use entropy maximization via iterative supervised fine-tuning to learn to generate increasingly diverse programs over time. We release large datasets of synthetic verified programs in three languages - Dafny, Verus, and Frama-C -, and fine-tune open models for verification-relevant tasks, often matching or exceeding the performance of Claude Opus 4.5. Overall, our work offers a path to create synthetic data at scale for formal reasoning domains and overcome the long-standing data barrier.

Figures

Figures reproduced from arXiv: 2607.04631 by Gabriel Poesia, Nada Amin, Simon Henniger, Tzu-Han Hsu, Yilun Du.

Figure 1
Figure 1. Figure 1: Overview of FORMAL DISCO. The system is centered around a distributed agenda, where LLM-based workers collaborate on completing tasks and store objects — mainly synthetic programs being written, extended and repaired. The Initiator worker sketches initial programs in the given verification-aware language, including specifications and proofs, taking ideas from README files sampled from open-source repositor… view at source ↗
Figure 2
Figure 2. Figure 2: Task success rates for FORMAL DISCO worker tasks backed by varying LLMs. Each color indicates a different worker task (Initiator, Fixer and Extender workers from Section 3.2). The dashed line shows performance for the seed Claude Sonnet 4.5 and Opus 4.5 workers; solid lines show the Qwen 2.5 Coder 32B model after fine-tuning either on the Claude distillation data (SFT iteration 1) or on the aggregate datas… view at source ↗
Figure 3
Figure 3. Figure 3: Feature entropy on the program corpora generated by [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Rarefaction curves over 4 features, including three that we do not optimize for in our [PITH_FULL_IMAGE:figures/full_fig_p011_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Success rate on the logical annotation task as a function of the number of independent [PITH_FULL_IMAGE:figures/full_fig_p013_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Success rate on the lemma proving task as a function of the number of independent [PITH_FULL_IMAGE:figures/full_fig_p014_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Ablations of the two external entropy sources in the Initiator’s seed context, on Dafny. [PITH_FULL_IMAGE:figures/full_fig_p015_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Rarefaction curves across (1) Number of logical annotations per method, (2) Proof/Body [PITH_FULL_IMAGE:figures/full_fig_p044_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Rarefaction curves across self-improvement iterations, in the same features shown in [PITH_FULL_IMAGE:figures/full_fig_p045_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Rarefaction curves across self-improvement iterations, in the same features shown in [PITH_FULL_IMAGE:figures/full_fig_p046_10.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

42 extracted references · 11 linked inside Pith

  1. [1]

    Claude Opus 4.5 system card

    Anthropic. Claude Opus 4.5 system card. Technical report, Anthropic, November 2025

    2025

  2. [2]

    Mantas Baksys, Stefan Zetzsche, Olivier Bouissou, Remi Delmas, Soonho Kong, and Sean B. Holden. ATLAS: Automated toolkit for large-scale verified code synthesis, 2026

    2026

  3. [3]

    Knowledge transfer from high-resource to low-resource programming languages for code llms.Proc

    Federico Cassano, John Gouwar, Francesca Lucchetti, Claire Schlesinger, Anders Freeman, Carolyn Jane Anderson, Molly Q Feldman, Michael Greenberg, Abhinav Jangda, and Arjun Guha. Knowledge transfer from high-resource to low-resource programming languages for code llms.Proc. ACM Program. Lang., 8(OOPSLA2), October 2024

    2024

  4. [4]

    MultiPL-E: A scalable and polyglot approach to benchmarking neural code generation.IEEE Trans

    Federico Cassano, John Gouwar, Daniel Nguyen, Sydney Nguyen, Luna Phipps-Costin, Donald Pinckney, Ming-Ho Yee, Yangtian Zi, Carolyn Jane Anderson, Molly Q Feldman, Arjun Guha, Michael Greenberg, and Abhinav Jangda. MultiPL-E: A scalable and polyglot approach to benchmarking neural code generation.IEEE Trans. Softw. Eng., 49(7):3675–3691, July 2023

    2023

  5. [5]

    Automated proof generation for rust code via self-evolution, 2026

    Tianyu Chen, Shuai Lu, Shan Lu, Yeyun Gong, Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Hao Yu, Nan Duan, Peng Cheng, Fan Yang, Shuvendu K Lahiri, Tao Xie, and Lidong Zhou. Automated proof generation for rust code via self-evolution, 2026

    2026

  6. [6]

    Frama-C: A software analysis perspective

    Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. Frama-C: A software analysis perspective. InInternational conference on software engineering and formal methods, pages 233–247. Springer, 2012

    2012

  7. [7]

    Z3: An efficient SMT solver

    Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. InInternational conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337–340. Springer, 2008. 16

    2008

  8. [8]

    Lorch, Yuan Yao, and Xiaoxing Ma

    Nongyu Di, Tianyu Chen, Shan Lu, Shuai Lu, Yeyun Gong, Peng Cheng, Jacob R. Lorch, Yuan Yao, and Xiaoxing Ma. Reducing the costs of proof synthesis on rust systems by scaling up a seed training set, 2026

    2026

  9. [9]

    Raft: Reward ranked finetuning for generative foundation model alignment.arXiv preprint arXiv:2304.06767, 2023

    Hanze Dong, Wei Xiong, Deepanshu Goyal, Yihan Zhang, Winnie Chow, Rui Pan, Shizhe Diao, Jipeng Zhang, Kashun Shum, and Tong Zhang. Raft: Reward ranked finetuning for generative foundation model alignment.arXiv preprint arXiv:2304.06767, 2023

    Pith/arXiv arXiv 2023

  10. [10]

    Stp: Self-play llm theorem provers with iterative conjecturing and proving.arXiv preprint arXiv:2502.00212, 2025

    Kefan Dong and Tengyu Ma. Stp: Self-play llm theorem provers with iterative conjecturing and proving.arXiv preprint arXiv:2502.00212, 2025

    Pith/arXiv arXiv 2025

  11. [11]

    Tinystories: How small can language models be and still speak coherent english?arXiv preprint arXiv:2305.07759, 2023

    Ronen Eldan and Yuanzhi Li. Tinystories: How small can language models be and still speak coherent english?arXiv preprint arXiv:2305.07759, 2023

    Pith/arXiv arXiv 2023

  12. [12]

    Reinforced self-training (rest) for language modeling.arXiv preprint arXiv:2308.08998, 2023

    Caglar Gulcehre, Tom Le Paine, Srivatsan Srinivasan, Ksenia Konyushkova, Lotte Weerts, Abhishek Sharma, Aditya Siddhant, Alex Ahern, Miaosen Wang, Chenjie Gu, et al. Reinforced self-training (rest) for language modeling.arXiv preprint arXiv:2308.08998, 2023

    Pith/arXiv arXiv 2023

  13. [13]

    Data quality for machine learning tasks

    Nitin Gupta, Shashank Mujumdar, Hima Patel, Satoshi Masuda, Naveen Panwar, Sambaran Bandyopadhyay, Sameep Mehta, Shanmukha Guttula, Shazia Afzal, Ruhi Sharma Mittal, et al. Data quality for machine learning tasks. InProceedings of the 27th ACM SIGKDD conference on knowledge discovery & data mining, pages 4040–4041, 2021

    2021

  14. [14]

    Collapse of self-trained language models.arXiv preprint arXiv:2404.02305, 2024

    David Herel and Tomas Mikolov. Collapse of self-trained language models.arXiv preprint arXiv:2404.02305, 2024

    Pith/arXiv arXiv 2024

  15. [15]

    LoRA: Low-rank adaptation of large language models

    Edward J Hu, yelong shen, Phillip Wallis, Zeyuan Allen-Zhu, Yuanzhi Li, Shean Wang, Lu Wang, and Weizhu Chen. LoRA: Low-rank adaptation of large language models. In International Conference on Learning Representations, 2022

    2022

  16. [16]

    Qwen2.5-Coder technical report.arXiv preprint arXiv:2409.12186, 2024

    Binyuan Hui, Jian Yang, Zeyu Cui, Jiaxi Yang, Dayiheng Liu, Lei Zhang, Tianyu Liu, Jia- jun Zhang, Bowen Yu, Keming Lu, et al. Qwen2.5-Coder technical report.arXiv preprint arXiv:2409.12186, 2024

    Pith/arXiv arXiv 2024

  17. [17]

    Verus: A practical foundation for systems verification

    Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chanhee Cho, Hayley LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Hawblitzel, et al. Verus: A practical foundation for systems verification. InProceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles, pages 438–454, 2024

    2024

  18. [18]

    Verus: Verifying rust programs using linear ghost types.Proceedings of the ACM on Programming Languages, 7(OOPSLA1):286–315, 2023

    Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. Verus: Verifying rust programs using linear ghost types.Proceedings of the ACM on Programming Languages, 7(OOPSLA1):286–315, 2023

    2023

  19. [19]

    Dafny: An automatic program verifier for functional correctness

    K Rustan M Leino. Dafny: An automatic program verifier for functional correctness. In International conference on logic for programming artificial intelligence and reasoning, pages 348–370. Springer, 2010

    2010

  20. [20]

    Lenat and John Seely Brown

    Douglas B. Lenat and John Seely Brown. Why am and eurisko appear to work.Artificial Intelligence, 23(3):269–294, 1984

    1984

  21. [21]

    Textbooks are all you need ii: phi-1.5 technical report.arXiv preprint arXiv:2309.05463, 2023

    Yuanzhi Li, Sébastien Bubeck, Ronen Eldan, Allie Del Giorno, Suriya Gunasekar, and Yin Tat Lee. Textbooks are all you need ii: phi-1.5 technical report.arXiv preprint arXiv:2309.05463, 2023

    Pith/arXiv arXiv 2023

  22. [22]

    Goedel-prover: A frontier model for open-source automated theorem proving.arXiv preprint arXiv:2502.07640, 2025

    Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, et al. Goedel-prover: A frontier model for open-source automated theorem proving.arXiv preprint arXiv:2502.07640, 2025

    Pith/arXiv arXiv 2025

  23. [23]

    DafnyBench: A benchmark for formal software verification.arXiv preprint arXiv:2406.08467, 2024

    Chloe Loughridge, Qinyi Sun, Seth Ahrenbach, Federico Cassano, Chuyue Sun, Ying Sheng, Anish Mudide, Md Rakib Hossain Misu, Nada Amin, and Max Tegmark. DafnyBench: A benchmark for formal software verification.arXiv preprint arXiv:2406.08467, 2024

    Pith/arXiv arXiv 2024

  24. [24]

    Lopes, Iris Ma, and James Noble

    Md Rakib Hossain Misu, Cristina V . Lopes, Iris Ma, and James Noble. Towards AI-assisted synthesis of verified Dafny methods.Proceedings of the ACM on Software Engineering, 1(FSE):812–835, July 2024. 17

    2024

  25. [25]

    On the impact of formal verification on software development.Proceedings of the ACM on Programming Languages, 9(OOPSLA2):3642–3668, 2025

    Eric Mugnier, Yuanyuan Zhou, Ranjit Jhala, and Michael Coblenz. On the impact of formal verification on software development.Proceedings of the ACM on Programming Languages, 9(OOPSLA2):3642–3668, 2025

    2025

  26. [26]

    Building a c compiler with a team of parallel claudes

    Nicholas Carlini. Building a c compiler with a team of parallel claudes. https://www. anthropic.com/engineering/building-c-compiler, February 2026

    2026

  27. [27]

    Learning formal mathemat- ics from intrinsic motivation.Advances in Neural Information Processing Systems, 37:43032– 43057, 2024

    Gabriel Poesia, David Broman, Nick Haber, and Noah D Goodman. Learning formal mathemat- ics from intrinsic motivation.Advances in Neural Information Processing Systems, 37:43032– 43057, 2024

    2024

  28. [28]

    dafny-annotator: AI-assisted verification of Dafny programs, 2024

    Gabriel Poesia, Chloe Loughridge, and Nada Amin. dafny-annotator: AI-assisted verification of Dafny programs, 2024

    2024

  29. [29]

    Taxonomic diversity estimation using rarefaction.Paleobiology, 1(4):333–342, 1975

    David M Raup. Taxonomic diversity estimation using rarefaction.Paleobiology, 1(4):333–342, 1975

    1975

  30. [30]

    Agentic much? adoption of coding agents on github.ACM Transactions on Software Engineering and Methodology, 2026

    Romain Robbes, Théo Matricon, Thomas Degueule, Andre Hora, and Stefano Zacchiroli. Agentic much? adoption of coding agents on github.ACM Transactions on Software Engineering and Methodology, 2026

    2026

  31. [31]

    Ai models collapse when trained on recursively generated data.Nature, 631(8022):755– 759, 2024

    Ilia Shumailov, Zakhar Shumaylov, Yiren Zhao, Nicolas Papernot, Ross Anderson, and Yarin Gal. Ai models collapse when trained on recursively generated data.Nature, 631(8022):755– 759, 2024

    2024

  32. [32]

    Clover: Closed-loop verifiable code generation

    Chuyue Sun, Ying Sheng, Oded Padon, and Clark Barrett. Clover: Closed-loop verifiable code generation. InAI Verification: First International Symposium, SAIV 2024, Montreal, QC, Canada, July 22–23, 2024, Proceedings, page 134–155, Berlin, Heidelberg, 2024. Springer- Verlag

    2024

  33. [33]

    Solving olympiad geometry without human demonstrations.Nature, 625(7995):476–482, 2024

    Trieu H Trinh, Yuhuai Wu, Quoc V Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations.Nature, 625(7995):476–482, 2024

    2024

  34. [34]

    V oyager: An open-ended embodied agent with large language models

    Guanzhi Wang, Yuqi Xie, Yunfan Jiang, Ajay Mandlekar, Chaowei Xiao, Yuke Zhu, Linxi Fan, and Anima Anandkumar. V oyager: An open-ended embodied agent with large language models. arXiv preprint arXiv:2305.16291, 2023

    Pith/arXiv arXiv 2023

  35. [35]

    Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data.arXiv preprint arXiv:2405.14333, 2024

    Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data.arXiv preprint arXiv:2405.14333, 2024

    Pith/arXiv arXiv 2024

  36. [36]

    something went wrong

    Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jacob R Lorch, Shuai Lu, et al. Autoverus: Auto- mated proof generation for rust code.Proceedings of the ACM on Programming Languages, 9(OOPSLA2):3454–3482, 2025. A Hyperparameters We report the hyperparameters used for (1) synthetic da...

    2025

  37. [37]

    The repository is most likely unrelated to verified programming, so freely adapt or reinterpret its theme

    Come up with a concise idea for a Dafny program inspired by the repository’s theme. The repository is most likely unrelated to verified programming, so freely adapt or reinterpret its theme

  38. [38]

    Your program should NOT try to implement the entire idea, which is likely to be overly ambitious to write in one go

    Immediately implement that idea as a self-contained Dafny program. Your program should NOT try to implement the entire idea, which is likely to be overly ambitious to write in one go. Start with e.g. a few functions at most, or a very basic class with only a couple of core methods, or prove a basic lemma, etc. You can also add comments on ideas to extend ...

  39. [39]

    The repository is most likely unrelated to verified programming, so freely adapt or reinterpret its theme

    Come up with a concise idea for a Verus program inspired by the repository’s theme. The repository is most likely unrelated to verified programming, so freely adapt or reinterpret its theme

  40. [40]

    Your program should NOT try to implement the entire idea, which is likely to be overly ambitious to write in one go

    Immediately implement that idea as a self-contained Verus program. Your program should NOT try to implement the entire idea, which is likely to be overly ambitious to write in one go. Start with e.g. a few functions at most, or prove a basic lemma, etc. You can also add comments on ideas to extend the program later. 35 The output must be valid Verus code ...

  41. [41]

    The repository is most likely unrelated to formal verification, so freely adapt or reinterpret its theme

    Come up with a concise idea for a C program with ACSL annotations inspired by the repository’s theme. The repository is most likely unrelated to formal verification, so freely adapt or reinterpret its theme

  42. [42]

    Hello, World!

    Immediately implement that idea as a self-contained C program with ACSL annotations. Your program should NOT try to implement the entire idea, which is likely to be overly ambitious to write in one go. Start with e.g. a few functions at most, or prove a basic lemma, etc. You can also add comments on ideas to extend the program later. Include function cont...