Back

What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus

Rijul JainShraddha BarkeGabriel EbnerMd Rakib Hossain MisuShan LuSarah Fakhoury

article2025arXiv2 citations

Reveals how expert developers construct formal proofs in F* and Verus through fine-grained telemetry, establishing practical design principles that improve the performance of AI-driven proof synthesis agents.

Listen

Formal software verification using proof-oriented programming languages, such as F* and Verus, mathematically guarantees that code behaves correctly before deployment, providing critical assurance for high-stakes systems like operating system kernels and secure communications. However, these languages remain difficult to adopt due to steep learning curves, opaque automated verifier feedback, and high cognitive overhead. While artificial intelligence models offer potential to automate proof generation, tool designers currently lack a systematic understanding of how human experts navigate and structure proof development.

The article aims to evaluate how expert developers allocate effort and interact with automated verification tools, identify the underlying proof engineering strategies that drive task success, and demonstrate how these human insights can be used to improve automated artificial intelligence proof assistants.

To conduct this evaluation, the researchers instrumented the Visual Studio Code environments for F* and Verus to capture real-time telemetry across eight expert developers completing four benchmark programming tasks. The dataset comprises over 18,000 fine-grained interaction events, including code edits, automated verifier invocations, active error tracking, and pauses. The telemetry events were automatically categorized into distinct development states, such as specification, implementation, and proof. The researchers then applied statistical clustering and thematic analysis to post-task surveys to uncover behavioral archetypes, followed by a proof-of-concept case study implementing a multi-agent proof assistant architecture.

The analysis revealed three primary findings regarding expert workflow and task success. First, proof and specification activities dominate development time across both languages (roughly 55% to 65% of effort in F* and 60% in Verus), with specification refinement occurring continuously across all stages of a task rather than exclusively at the beginning. Second, unsupervised clustering uncovered three distinct developer archetypes: specification-first planners, balanced developers, and rapid verifiers. Specification-first planners, who front-loaded specification drafting (accounting for 56% to 74% of early edits) and maintained disciplined error management, achieved a 100% completion rate with the fastest task times. In contrast, rapid verifiers relied on aggressive verifier polling (exceeding 5.5 to 6.5 calls per minute) and tolerated persistent error states, which resulted in longer durations and lower success rates of 60% to 67%. Third, when human expert planning behaviors were mirrored in a multi-agent proof system separating high-level proof sketching from low-level syntax generation, the agent completed verified benchmarks within 7 to 8 verifier refinement loops, whereas an unguided baseline language model failed to reach a verified solution within 30 loops.

These findings indicate that formal verification success is heavily driven by deliberate, informal reasoning practices that are absent from final codebases, including problem decomposition, structured pauses, and controlled verifier interaction. For engineering organizations and software leaders, this means that automated proof tooling and artificial intelligence assistants must move beyond naive trial-and-error code generation. Instead, tooling should actively enforce structured task decomposition and error containment to lower development costs, reduce project timelines, and expand the practical reach of high-assurance software engineering.

The article recommends that developers of formal verification environments and artificial intelligence copilots design modular systems that support online lemma retrieval, step-by-step task planning, and targeted verifier error interpretation rather than raw automated feedback. Developers should also incorporate automated interventions that detect unproductive, rapid edit-verify loops and guide users back toward decomposition. Organizations adopting artificial intelligence for formal verification should deploy specialized, multi-agent pipelines that decouple strategic proof sketching from syntax formulation.

Confidence in these findings is supported by consistent behavioral patterns emerging independently across two distinct verification languages and alignment between telemetry data and qualitative surveys. However, readers should consider key limitations: the user study was conducted with a small cohort of eight experts on small-to-medium benchmark programs, and the proof-agent evaluation was limited in scope. Further research and broader pilot testing on large, multi-module industrial software systems are necessary before generalizing the performance improvements across all verification domains.

MicrosoftUniversity of California, IrvineUniversity of Washingtonformal proofslarge language modelsprogramming languagesExpert proof-writing processesproof engineeringproof-oriented programming
arXiv: 2508.02733

No sufficiently relevant recommendations were found.

Cover for What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus

Abstract

Proof-oriented programming languages (POPLs) empower developers to write code alongside formal correctness proofs, providing formal guarantees that the code adheres to specified requirements. Despite their powerful capabilities, POPLs present a steep learning curve and have not yet been adopted by the broader software community. The lack of understanding about the proof-development process and how expert proof developers interact with POPLs has hindered the advancement of effective proof engineering and the development of proof-synthesis models/tools.

In this work, we conduct a user study, involving the collection and analysis of fine-grained source code telemetry from eight experts working with two languages, F* and Verus. Results reveal interesting trends and patterns about how experts reason about proofs and key challenges encountered during the proof development process. We identify three distinct strategies and multiple informal practices that are not captured final code snapshots, yet are predictive of task outcomes. We translate these findings into concrete design guidance for AI proof assistants: bias toward early specification drafting, explicit sub-goal decomposition, bounded active errors, and disciplined verifier interaction. We also present a case study of an F* proof agent grounded in these recommendations, and demonstrate improved performance over baseline LLMs

Topics

formal proofslarge language modelsprogramming languagesrecommendationsoftwaresource codesdevelopment processesdomain knowledgesoftware developerformal specification

Keywords

Expert proof-writing processesproof engineeringproof-oriented programmingspecification draftingverifier feedback

Table of Contents

  • 1 INTRODUCTION
  • 2 BACKGROUND
  • 2.1 Proof-oriented Programming Languages: Verus and F*
  • 2.2 User studies for Proof Development
  • 2.3 Language Models for Proof Generation
  • 3 RESEARCH QUESTIONS
  • 4 USER STUDY
  • 4.1 Tasks
  • 4.2 Participants
  • 4.3 Procedure
  • 4.4 Measures
  • 4.5 Annotating Telemetry Data
  • 5 RESULTS: Proof Effort and Verifier Usage
  • 5.1 RQ1: Where Users Spend Time in the Proof-Writing Process
  • 5.1.1 Proof-Development State Breakdown
  • 5.1.2 Proof-Development Process: How Do States Change Over Time?
  • 5.2 RQ2: Interaction with the Verifier
  • 5.2.1 Frequency of Verifier Invocations
  • 5.2.2 Frequency of Verification Errors
  • 6 RESULTS: Emergent Strategies
  • 6.1 RQ3a: Strategy Themes from Thematic Analysis of Post-Task Questionnaires
  • 6.1.1 Experts Emphasize Task Decomposition and Iterative Refinement
  • 6.1.2 Experts Define Specs Early, and Align Spec Structure with the Implementation
  • 6.1.3 Experts are Familiar with External Libraries, Select and Modify Lemmas As Needed
  • 6.1.4 Experts Use Measured and Frequent Feedback from the Verifier
  • 6.2 RQ3b: Telemetry-Derived Strategies and Task Outcomes
  • 6.3 RQ3b: Case Study of Strategy Archetypes
  • 6.3.1 Case study– task T3: four timelines, three strategies
  • 7 RECOMMENDATIONS
  • 7.1 Proof Copilot Design
  • 7.1.1 Online Lemma and Documentation Retrieval
  • 7.1.2 Task Planning and Decomposition
  • 7.1.3 Proof Debugging and Targeted Verifier Feedback
  • 7.1.4 Agent Specialization and Modularity
  • 7.2 F* Agent Case Study
  • 7.2.1 F* Agent Evaluation
  • 8 THREATS TO VALIDITY
  • 9 CONCLUSION
  • References

Knowls

  1. Knowl 1 — Telemetry clusters identify proof-writing strategies associated with outcomes

    empirical result

    A telemetry-based analysis of expert proof sessions in F* and Verus identified strategy profiles associated with task success and completion time. Each session was a participant–task pair. The researchers z-normalized five behavioral features separately within each language, then ran k-means with seed 42 and n_init=auto, testing cluster counts of 2, 3, and 4. For F*, three clusters offered the best balance of separation and interpretability (silhouette 0.34, versus 0.29 for two clusters and 0.21 for four). For Verus, three clusters had the best silhouette (0.173, versus 0.153 and 0.092), but one cluster contained a single session, so comparisons involving it are exploratory.

    The features were: early_spec, the fraction of first-quartile edits devoted to specifications; verify_fq, verifier invocations per task minute; clean_state, the fraction of task time with zero active verifier errors; pause_frac, the fraction of session time in gaps longer than five seconds; and defer, the fraction of task time spent in states using comments or assumptions to defer subgoals. The reported cluster values and outcomes are:

    • F Spec-first Planners* (2 sessions): early_spec 0.74, verify_fq 3.63 calls/min, clean_state 0.07, pause_frac 0.06, defer 0.77; success 1.00; median duration 21.89 min.
    • F Balanced* (4 sessions): 0.50, 1.78 calls/min, 0.04, 0.07, and 0.28, respectively; success 1.00; median duration 22.74 min.
    • F Rapid-verify* (3 sessions): 0.46, 6.54 calls/min, 0.01, 0.03, and 0.63; success 0.67; median duration 24.41 min.
    • Verus Spec-first Planner (1 session): 0.56, 3.74 calls/min, 0.57, 0.02, and 0.00; success 1.00; median duration 11.77 min.
    • Verus Balanced (2 sessions): 0.53, 2.18 calls/min, 0.20, 0.05, and 0.19; success 1.00; median duration 25.12 min.
    • Verus Rapid-verify (5 sessions): 0.44, 5.52 calls/min, 0.10, 0.03, and 0.00; success 0.60; median duration 26.10 min.

    Across the observed sessions, early specification work and maintaining a clean verifier state accompanied more successful, time-efficient work; aggressive verification with less early specification accompanied lower success and longer or more variable completion. These are descriptive associations from a small sample, not evidence that the behaviors cause the outcomes.

  2. Knowl 2 — Expert proof-writing study and task dataset

    experimental setup

    The study collected live source-edit and IDE telemetry from eight expert users of proof-oriented programming languages: four worked in F* and four in Verus. Six participants maintained or designed their target language; the other two had intermediate proficiency. Participants worked in preconfigured GitHub Codespaces with instrumented VSCode extensions. The extensions recorded edits, verifier invocations and outputs, active errors, pauses, documentation lookups, hover actions, and other editor actions, yielding more than 18,000 annotated events. Sessions were designed to last about 90 minutes; screen recordings were used to cross-check telemetry, and participants completed a structured survey after each task.

    The four tasks were binary search (T1), contiguous-sublist checking (T2), duplicate-free array intersection (T3), and maximum-minus-minimum of a list (T4). T1 came from both languages’ tutorials; T2–T4 were selected from MBPP. For Verus, participants received a correct Rust implementation so the study could focus on proof writing; F* implementation and proof were more tightly intertwined. Average task durations and self-reported effort were:

    • T1: F*, participants P1 and P4, 45.07 min, effort 7.5/10; Verus, P6 and P7, 11.80 min, effort 2/10.
    • T2: F*, P2 and P3, 37.06 min, effort 6/10; Verus, P5 and P8, 35.35 min, effort 3.5/10.
    • T3: F*, P1, P2, and P4, 16.70 min, effort 5/10; Verus, P7 and P8, 34.40 min, effort 5.5/10.
    • T4: F*, P1 and P3, 14.17 min, effort 4.5/10; Verus, P5 and P6, 19.00 min, effort 3/10.

    Each task was intended to be completed by two participants per language; one F* expert completed an additional task to balance assignments. Completion was assessed using supplied tests and the language verifier.

  3. Knowl 3 — Effort is distributed across intertwined proof-development states

    empirical result

    Expert effort was not confined to a single phase of proof development. In F*, participants spent approximately 55–65% of task time on specification and proof work, 20–40% on implementation, and 10–20% testing the implementation. In Verus, where the implementation was supplied, proof writing took about 60% of task time; commenting took 5–15%, often to temporarily hide parts of the code while working on a subgoal. F* participants more often used admit or assume to defer verification instead of commenting out code.

    The sequence of work also mattered: specification, implementation, and proof edits recurred throughout sessions rather than forming isolated stages. F* participants typically drafted a specification and some implementation early, increased implementation work in the second quarter, and returned to specifications later; implementation edits could continue into the final quarter. Verus participants concentrated specification work in the first quarter, but continued to revise specifications afterward, often to address proof difficulties or simplify a proof. Proof work dominated Verus’s second and third quarters, while comment edits tended to peak near the end as participants cleaned up code.

  4. Knowl 4 — Verifier activity and active errors distinguish disciplined from struggling sessions

    empirical result

    Across observed tasks, experts invoked the verifier an average of 3.39 times per minute in F* and 9.11 times per minute in Verus. The average number of active verifier errors at a given time was 1.49 in F* and 1.9 in Verus, but individual Verus sessions sometimes accumulated 35–40 active errors. In two unsuccessful Verus sessions—P7’s T3 and P5’s T2—invocations rose steeply late in the task and exceeded 30 in a quartile. Participants who completed those same tasks, including P8, used at most about half as many invocations per quartile.

    P8 maintained only 0–4 active errors in both tasks, while peers on the same tasks sometimes had more than 5 or more than 15. The study therefore associates frequent returns to a zero-error state, for example by deferring parts of a proof and working through subgoals in sequence, with better outcomes. It also reports that more difficult or effortful tasks tended to involve more verifier calls. These patterns are correlational; the study does not establish that invocation frequency or error management alone determines success.

  5. Knowl 5 — Experts plan with specifications, decompose goals, and refine iteratively

    empirical result

    Post-task reports and session traces showed several recurring expert practices. Participants often began by stating high-level preconditions and postconditions, then decomposed the implementation and proof into manageable subgoals. They refined specifications and invariants as proof attempts exposed difficulties rather than trying to finalize every detail before implementation. They also tried to align specification structure with implementation structure, selected representations and quantifiers with proof tractability, and reused or adapted library lemmas when available. For example, one participant replaced a library filter whose specification was too weak with a more tightly specified version.

    In the T3 duplicate-free intersection task, F* participant P2 first paused to plan, drafted a high-level specification, reused a deduplication function, and then alternated between specification and implementation work; the solution was about 30 lines and took approximately 14 minutes. F* participant P4 wrote supporting sorted-list lemmas from scratch, switched more rapidly among specification, implementation, and proof edits, and produced a 97-line solution about five minutes slower. In Verus, P7 made dense verifier calls and repeated specification rewrites but did not finish after 45 minutes. P8 sketched the specification and proof structure first, used temporary assumptions to isolate subgoals, and completed the task. The successful sessions illustrated planning, reuse of trusted lemmas where available, subgoal isolation, and deliberate thinking pauses.

  6. Knowl 6 — Proof-assistant copilots should support planning, retrieval, and controlled feedback

    model/method

    The study motivates several design directions for proof-oriented programming assistants. A copilot should help retrieve relevant library lemmas and examples in the context of the current proof state, and should support specification-first planning by proposing helper functions, proof sketches, and an order for addressing subgoals. It should help interpret verifier failures by identifying likely causes and relevant proof steps, rather than presenting only dense error messages. The authors also propose breakpoint-like controls for temporarily excluding selected lines during verification, reducing reliance on manual comments or assumptions, and specialized assistant components for tasks such as lemma search, proof sketching, syntax help, and verifier-feedback interpretation.

    The recommendations reflect observed expert practices: early specification drafting, explicit decomposition, bounded active errors, and measured use of the verifier. The study presents these as design guidance, not as interventions whose benefits have been independently established.

  7. Knowl 7 — The F* proof agent separates proof planning from syntax-level code generation

    model/method

    The proof-of-concept F* agent uses two collaborating agents in an iterative verifier-guided workflow. A Proof Expert Agent, powered by OpenAI o3, acts as a specification-first planner. It produces a high-level proof sketch that considers the specification, decomposition into helper functions, suitable representations, alignment between specification and implementation, and overall proof organization. GraphRAG retrieves relevant F* documentation and examples to inform this planning. The sketch is passed to an F* Syntax Expert Agent, which uses the F* language manual to turn the plan into syntactically valid F* code and address syntax-level issues.

    The candidate code is sent to the F* verifier. The verifier’s output is used to revise the code or the plan, and the agents repeat this cycle. The design separates high-level proof decisions from syntax-focused code production while retaining verifier feedback as the basis for iterative refinement.

  8. Knowl 8 — The F* proof agent verified two tasks with fewer verifier turns than a baseline

    empirical result

    The F* proof agent was evaluated on T4, rated the easiest task by study experts, and T1, rated the most difficult. It generated correct, verifier-accepted solutions using 8 effective refinement turns for T4 and 7 for T1; an effective turn was one that invoked the F* verifier, excluding internal reasoning and inter-agent conversation. The naive baseline used OpenAI o4-mini with the same system and high-level task prompts but without instructions for agent tool use. It did not produce a correct verified solution within 30 verifier-refinement loops on either selected task. The authors describe this as a potential 3.75-fold reduction in verifier calls, comparing the 30-loop baseline limit with the agent’s 8-turn T4 result.

    The harder task did not require more refinement turns than the easier task. The reported results are a small case study on two tasks, rather than a broad benchmark evaluation.

  9. Knowl 9 — Telemetry annotation maps edits to proof-development states

    model/method

    To analyze source-edit telemetry, the study defined a taxonomy and automatically assigned events to proof-development states using language-specific keywords. The states were: Specification, covering preconditions and postconditions in Verus and proof-related edits, including refinement types, in F*; Proof, covering proof edits other than specifications in Verus, such as loop invariants; Implementation, covering edits to program functionality; Structure, covering changes to overall solution or proof structure, such as proof or lemma signatures; Comment, covering comments and code commented out for later; and Test, covering test code and testing infrastructure. For the selected F* tasks, assert edits were classified as tests because participants used assertions as static unit tests.

    The telemetry processing also identified actions such as verifier triggers, documentation lookups, hover actions, and pauses. These annotations allowed the researchers to compare time and activity across development states and sessions.

  10. Knowl 10 — Small expert sample and limited task scope constrain generalization

    limitation

    The study involved eight participants, mostly maintainers or designers of F* or Verus, and small-to-medium tasks; the findings may not represent novice or intermediate users, larger verification projects, or routine maintenance such as proof refactoring and multi-module reasoning. The small number of sessions limits statistical significance and may conceal less common strategies. In particular, the Verus three-cluster solution includes a singleton planner session, making comparisons involving that cluster exploratory.

    The authors also identify possible telemetry instrumentation or annotation errors, subjectivity in participant self-reports, and researcher bias in thematic coding. They checked samples against screen recordings and reran clustering under alternative normalizations, but these checks do not remove all uncertainty. The proof-agent evaluation used only two tasks and limited sampling seeds, so its results may not transfer to more complex tasks, other languages, or broader benchmarks.

Coverage note — Individual telemetry traces and detailed accounts of tasks other than the T3 case study are omitted because they are illustrative rather than independently generalizable; background and related work are excluded as non-contributed material.

References

  1. 1.Pranjal Aggarwal, Bryan Parno, and Sean Welleck. 2024. AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement. arXiv:2412.06176 https://arxiv.org/abs/2412.06176
  2. 2.June Andronick, Ross Jeffery, Gerwin Klein, Rafal Kolanski, Mark Staples, He Zhang, and Liming Zhu. 2012. Large-scale formal verification in practice: A process perspective. In 2012 34th International Conference on Software Engineering (ICSE). IEEE, 1002–1011.
  3. 3.David Aspinall and Cezary Kaliszyk. 2016. Towards formal proof metrics. In Fundamental Approaches to Software Engineering: 19th International Conference, FASE 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016, Proceedings 19. Springer, 325–341.
  4. 4.Jacob Austin, Augustus Odena, Maxwell Nye, Maarten Bosma, Henryk Michalewski, David Dohan, Ellen Jiang, Carrie Cai, Michael Terry, Quoc Le, et al. 2021. Program synthesis with large language models. arXiv preprint arXiv:2108.07732 (2021).
  5. 5.Jasmin Christian Blanchette, Maximilian Haslbeck, Daniel Matichuk, and Tobias Nipkow. 2015. Mining the archive of formal proofs. In International Conference on Intelligent Computer Mathematics. Springer, 3–17.
  6. 6.Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu Lahiri, and Nikhil Swamy. 2025. Towards Neural Synthesis for SMT-assisted Proof-Oriented Programming . In 2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE). IEEE Computer Society, Los Alamitos, CA, USA, 13–25. doi:10.1109/ICSE55347.2025.00002
  7. 7.Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 337–340.
  8. 8.Darren Edge, Ha Trinh, Newman Cheng, Joshua Bradley, Alex Chao, Apurva Mody, Steven Truitt, Dasha Metropolitansky, Robert Osazuwa Ness, and Jonathan Larson. 2024. From local to global: A graph rag approach to query-focused summarization. arXiv preprint arXiv:2404.16130 (2024).
  9. 9.Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. 2023. Baldur: Whole-Proof Generation and Repair with Large Language Models. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (San Francisco, CA, USA) (ESEC/FSE 2023). Association for Computing Machinery, New York, NY, USA, 1229–1241. doi:10.1145/3611643.3616243
  10. 10.Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chanhee Cho, Hayley LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Oded Padon, and Bryan Parno. 2024. Verus: A Practical Foundation for Systems Verification. In Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles, SOSP 2024, Austin, TX, USA, November 4-6, 2024. ACM, 438–454.
  11. 11.Haohan Lin, Zhiqing Sun, Yiming Yang, and Sean Welleck. 2024. Lean-star: Learning to interleave thinking and proving. arXiv preprint arXiv:2407.10040 (2024).
  12. 12.Gwenyth Lincroft, Minsung Cho, Katherine Hough, Mahsa Bazzaz, and Jonathan Bell. 2024. Thirty-Three Years of Mathematicians and Software Engineers: A Case Study of Domain Expertise and Participation in Proof Assistant Ecosystems. In 2024 IEEE/ACM 21st International Conference on Mining Software Repositories (MSR). IEEE, 1–13.
  13. 13.Kirby Linvill, Gowtham Kaki, and Eric Wustrow. 2023. Verifying Indistinguishability of Privacy-Preserving Protocols. Proc. ACM Program. Lang. 7, OOPSLA2, Article 273 (Oct. 2023), 28 pages. doi:10.1145/3622849
  14. 14.Tula Masterman, Sandi Besen, Mason Sawtell, and Alex Chao. 2024. The landscape of emerging ai agent architectures for reasoning, planning, and tool calling: A survey. arXiv preprint arXiv:2404.11584 (2024).
  15. 15.Md Rakib Hossain Misu, Cristina V. Lopes, Iris Ma, and James Noble. 2024. Towards AI-Assisted Synthesis of Verified Dafny Methods. Proc. ACM Softw. Eng. 1, FSE, Article 37 (July 2024), 24 pages. doi:10.1145/3643763
  16. 16.OpenAI. 2025. OpenAI o3 (reasoning large language model). https://openai.com/index/introducing-o3-and-o4-mini/ Accessed 2025-07-19.
  17. 17.Clément Pit-Claudel. 2020. Untangling mechanized proofs. In Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering (Virtual, USA) (SLE 2020). Association for Computing Machinery, New York, NY, USA, 155–174. doi:10.1145/3426425.3426940
  18. 18.Roger Pressman and Bruce Maxim. 2019. Software Engineering: A Practitioner’s Approach (9th ed.). McGraw-Hill Education.
  19. 19.Aseem Rastogi. 2023. Proof-oriented programming for high-assurance systems. In Proceedings of the 16th Innovations in Software Engineering Conference (Allahabad, India) (ISEC ’23). Association for Computing Machinery, New York, NY, USA, Article 3, 1 pages. doi:10.1145/3578527.3581769
  20. 20.Talia Ringer, Alex Sanchez-Stern, Dan Grossman, and Sorin Lerner. 2020. REPLica: REPL instrumentation for Coq analysis. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. 99–113.
  21. 21.Jessica Shi, Cassia Torczon, Harrison Goldstein, Benjamin C Pierce, and Andrew Head. 2025. QED in Context: An Observation Study of Proof Assistant Users. Proceedings of the ACM on Programming Languages 9, OOPSLA1 (2025), 337–363.
  22. 22.Peiyang Song, Kaiyu Yang, and Anima Anandkumar. 2024. Towards large language models as copilots for theorem proving in lean. arXiv preprint arXiv:2404.12534 (2024).
  23. 23.Mark Staples, Ross Jeffery, June Andronick, Toby Murray, Gerwin Klein, and Rafal Kolanski. 2014. Productivity for proof engineering. In Proceedings of the 8th ACM/IEEE International Symposium on Empirical Software Engineering and Measurement. 1–4.
  24. 24.Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoué, and Santiago Zanella-Béguelin. 2016. Dependent Types and Multi-Monadic Effects in F*. In 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 256–270. https://www.fstar-lang.org/papers/mumon/
  25. 25.Nikhil Swamy, Tahina Ramananandro, Aseem Rastogi, Irina Spiridonova, Haobin Ni, Dmitry Malloy, Juan Vazquez, Michael Tang, Omar Cardona, and Arti Gupta. 2022. Hardening attack surfaces with formally proven binary format parsers. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (San Diego, CA, USA) (PLDI 2022). Association for Computing Machinery, New York, NY, USA, 31–45. doi:10.1145/3519939.3523708
  26. 26.Hanneli CA Tavante. 2021. A Data-Centered User Study for Proof Assistant Tools.. In PPIG.
  27. 27.Sean Welleck and Rahul Saha. 2023. LLMSTEP: LLM proofstep suggestions in Lean. arXiv preprint arXiv:2310.18457 (2023).
  28. 28.Qingyun Wu, Gagan Bansal, Jieyu Zhang, Yiran Wu, Beibin Li, Erkang Zhu, Li Jiang, Xiaoyun Zhang, Shaokun Zhang, Jiale Liu, et al. 2024. Autogen: Enabling next-gen LLM applications via multi-agent conversations. In First Conference on Language Modeling.
  29. 29.Jean-Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, and Benjamin Beurdouche. 2017. HACL*: A Verified Modern Cryptographic Library. In ACM Conference on Computer and Communications Security. ACM, 1789–1806. http://eprint.iacr.org/2017/536

Citation

MLA
Jain, R., et al. “What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus”. arXiv, 2025, http://arxiv.org/abs/2508.02733v1.
APA
Jain, R., Barke, S., Ebner, G., Misu, M. R. H., Lu, S., & Fakhoury, S. (2025). What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus. arXiv. http://arxiv.org/abs/2508.02733v1
Chicago
Jain, R., S. Barke, G. Ebner, M. R. H. Misu, S. Lu, and S. Fakhoury. 2025. “What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus”. arXiv. http://arxiv.org/abs/2508.02733v1.
Harvard
Jain, R. et al. (2025) “What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus”, arXiv [Preprint]. Available at: http://arxiv.org/abs/2508.02733v1.
Vancouver
1. Jain R, Barke S, Ebner G, Misu MRH, Lu S, Fakhoury S (2025) What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus. arXiv

BibTeX

@article{jain2025what,
  title = {What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus},
  author = {Jain, Rijul and Barke, Shraddha and Ebner, Gabriel and Misu, Md Rakib Hossain and Lu, Shan and Fakhoury, Sarah},
  year = {2025},
  journal = {arXiv},
  url = {http://arxiv.org/abs/2508.02733v1},
  eprint = {2508.02733}
}
Metadata:arXiv

Access the Paper

This paper is available from its original source. Click below to access the PDF.

Open PDF
License: https://creativecommons.org/licenses/by/4.0/