Pith. sign in

REVIEW 4 major objections 6 minor 2 cited by

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

T0 review · 4 major / 6 minor · reviewed 2026-08-06 · deepseek-v4-flash

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

Pith's one-line read Telemetry from eight expert sessions in F* and Verus shows that specification-first planning, measured verifier use, and low active-error time predict faster, more successful proofs, and the paper turns this into design guidance for AI…

desk verdict Fresh telemetry dataset and believable qualitative findings, but the predictive strategy claim is confounded by task difficulty and the agent result is too thin to support the abstract. read the letter →

arxiv 2508.02733 v1 pith:IGVLSCP7 submitted 2025-08-01 cs.SE cs.HC

Rijul Jain , Shraddha Barke , Gabriel Ebner , Md Rakib Hossain Misu , Shan Lu , Sarah Fakhoury This is my paper
classification cs.SEcs.HC
keywords proof-orientedprogramminguserstudytelemetryF*Verusproof-writingstrategiesspecification-firstplanningLLMproofassistant
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Proof-oriented programming is hard even for experts, and the actual process of writing proofs has been mostly invisible. This paper attaches fine-grained telemetry to the F* and Verus editors and records over 18,000 events from eight expert sessions: every edit, verifier call, pause, and hover. From those traces it argues that how experts behave predicts whether they finish: sessions that write specifications early, keep the number of active errors low, and invoke the verifier at a measured pace succeed more often and faster. Three strategy archetypes emerge, and the paper converts them into concrete design guidance for AI proof assistants, including a proof-of-concept F* agent that shows improved performance over a baseline LLM.

What carries the argument

The argument is carried by a telemetry-annotation pipeline plus clustering over per-session behavioral features. Raw editor events are tagged into six proof-writing states, specification, proof, implementation, structure, comment, and test, using language-specific keywords for F* and Verus. Each session is then summarized by five features: early_spec, the share of first-quartile edits that touch the specification; verify_fq, verifier calls per minute; clean_state, the fraction of time with no active errors; pause_frac, think pauses over five seconds; and defer, time spent with assume, admit, or comment-based deferrals. K-means over these normalized features produces the Planner, Rapid, and Balanced clusters, and those clusters are what link process behavior to task outcomes.

What would settle it

Re-run the analysis on the full event corpus with every session's telemetry manually labeled from the screen recordings, then recompute the five features and clusters; if manual labels disagree with the keyword tags in a way that dissolves the spec-first planner advantage or reverses the success ordering, the central claim fails. Alternatively, a larger study in a third POPL that fails to reproduce the planner-versus-rapid split at comparable success rates would falsify the claimed generality.

Watch

Extended reading notes

Core claim

The central discovery is a process-level account of expert proof engineering. When eight experts work in F* and Verus, most of their time goes into specification and proof states rather than standalone implementation, and specification writing is not a single phase but an activity interleaved with proof and implementation throughout the task. Clustering each full session on five behavioral features yields three archetypes: Spec-first Planners, whose early edits are largely spec, who return often to zero-error states, and who show perfect success with the shortest median times; Rapid Verifiers, who invoke the solver aggressively with low early spec investment and worse outcomes; and Balanced sessions in between. The paper concludes that effective proof writing is characterized by deliberate early specification drafting, measured verifier interaction, and disciplined error management, and it demonstrates a two-agent F* proof system built on that guidance solving tasks with a 3.75x reduction in verifier refinement calls compared with a baseline LLM.

Load-bearing premise

The study's conclusions rest on the assumption that its automatic keyword-based tagging of each edit as specification, proof, implementation, structure, comment, or test reflects what experts are really doing, and since only a sample of telemetry was checked against screen recordings, a systematic tagging error would distort all downstream features, clusters, and outcome associations.

Editorial extensions

If this is right

  • AI proof assistants should bias toward early specification drafting, and the agent case study shows a spec-first planner solving F* tasks with a 3.75x reduction in verifier refinement loops versus a baseline LLM.
  • Proof tooling should help users decompose tasks and defer verification on selected subgoals rather than forcing them to comment out code or manually add assume and admit statements.
  • Verifier error feedback should be interpreted and prioritized, since high verifier frequency and large active-error counts accompany unsuccessful sessions and copilots should intervene when users enter tight edit-verify-error loops.
  • Process telemetry, not just final code snapshots, carries predictive signal, so future proof-synthesis training could use intermediate states rather than finished proofs.
  • Frequent returns to a zero-error state are a hallmark of success, making clean-state recovery a design goal for proof-oriented IDEs.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the spec-first advantage is causal rather than merely correlational, process telemetry from both successful and failed attempts is a natural training signal for proof agents; the paper does not claim causality, but that is the next testable step.
  • The same five features could be computed for other proof assistants such as Lean, Coq, and Dafny using their plugin interfaces, and finding the same clusters there would be a strong cross-language generalization check.
  • The Verus clustering contains a singleton planner cluster and the sample is small, so the planner archetype may actually be a family of styles; a larger study could separate lemma-reuse planners from from-scratch proof writers.
  • The agent case study combines a planning step and a syntax-expert step, so ablating the two-agent split by using a single agent with the same planning prompt would isolate whether the decomposition itself causes the performance gain.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

4 major / 6 minor

Summary. The paper presents a user study of expert proof-writing processes in two proof-oriented programming languages, F* and Verus. The authors instrumented the VSCode extensions to record telemetry from eight experts across four proof tasks, annotated the resulting events into proof-writing states, and analyzed where experts spend effort, how they interact with the verifier, and what strategies they adopt. They report three strategy archetypes—Spec-first Planners, Rapid Verifiers, and Balanced—and claim that the specification-first planner style is predictive of faster and more successful task completion. They translate these findings into design guidance for AI proof assistants and evaluate a two-agent F* proof assistant, reporting improved performance over a baseline LLM.

Significance. If the empirical findings were robust, this would be a valuable contribution: it is one of the first fine-grained, cross-language studies of expert proof-writing behavior, and the telemetry instrumentation and annotation taxonomy could support follow-up research. The paper also makes a concrete move from observational findings to agent design, which is uncommon in this literature. The main strengths are the detailed telemetry collection, the cross-checking of annotations against screen recordings, the thematic grounding of the quantitative clusters, and the explicit translation of findings into actionable design guidance. However, the significance is currently limited by the very small sample, the absence of any statistical control for task difficulty or participant effects, and the preliminary nature of the agent evaluation.

major comments (4)
  1. [§6.2, Tables 3–4] The central claim that spec-first planning is predictive of faster and more successful task completion is not supported by the presented analysis because the strategy–outcome association is confounded by task difficulty. The Verus Spec-first Planner cluster is a singleton with median duration 11.77 minutes, matching the average duration of Task 1 in Table 1 (11.80 minutes), which participants rated as low effort (2/10). For F*, the three clusters have median durations of 21.89, 22.74, and 24.41 minutes—differing by only 1–3 minutes—and the Planner and Balanced clusters both achieve 100% success. The analysis does not condition on task, participant, or task difficulty, and no statistical test is reported. I recommend either adding a per-task or per-participant breakdown, controlling for task difficulty in the association, or explicitly reframing the claim as an exploratory, in-sample association rather than a predictive finding.
  2. [§4.5] The automatic annotation of telemetry events into proof-writing states is load-bearing for the behavioral features used in the clustering (early_spec, clean_state, defer, etc.), but the paper only states that a sample of telemetry was cross-checked against screen recordings. The accuracy of this keyword-based annotation is never quantified. The authors should report the size and selection of the validation sample, the agreement between automated and manual labels, the complete language-specific keyword lists, and a sensitivity analysis showing that the cluster results are stable under plausible variations in the annotation rules.
  3. [§7.2.1] The claim of improved performance over baseline LLMs is not established by the reported evaluation. The agent is evaluated on only two tasks with a single run each, the baseline uses a different model (o4-mini) than the agent (o3), and the baseline outcome is reported only as 'unable to achieve a correct verified solution within 30 verifier refinement loops' with no success rate, no variance, and no direct comparison of verifier calls on the same tasks. This conflates model choice with agent architecture. I recommend a controlled comparison using the same base model, multiple runs per task, and reporting both success rates and verifier invocation counts, or alternatively presenting this section as a proof-of-concept without the comparison claim.
  4. [§6.2] The clustering methodology requires more transparent sensitivity analysis. For Verus, k=3 is retained despite a silhouette score of 0.173 and a singleton cluster, and the text states that 'after enforcing a minimum cluster size, the data collapse to a robust two-way split,' but the two-cluster results are not shown. The authors should report the 2-cluster solution for Verus, show how the qualitative conclusions change when the singleton is excluded, and justify the choice of k without relying on interpretability.
minor comments (6)
  1. [§4.3] The procedure section states that results are consistent with the omitted F* session, but the paper never reports which session was omitted or how consistency was assessed; please provide this detail.
  2. [§6.1.2] A verbatim quote from P8 appears twice in the same subsection; please remove the duplicate.
  3. [Table 1] The 'Duration' column values appear to be averages across participants, but the header does not say so; please clarify the units and whether these are means.
  4. [§6.2] There is a typo, 'Pariticpants,' in the paragraph describing cluster sizes; please fix it.
  5. [§4.5] The decision to annotate all uses of 'assert' in F* as test edits may conflate testing with proof development, since asserts are also used to guide the verifier; please discuss this potential ambiguity.
  6. [Abstract] The abstract and Section 6.2 use the word 'predictive' for what is currently an in-sample association; please use more cautious language such as 'associated with' unless out-of-sample validation is added.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the study is empirical, and its in-sample associations and proof-of-concept agent are limitations, not definitional reductions.

full rationale

This paper is an empirical telemetry study rather than a derivation chain or a first-principles prediction. The central strategy labels in Section 6.2 come from k-means clustering on five behavioral features (early_spec, verify_fq, clean_state, pause_frac, defer) that are measured independently of the outcome variables (task success and duration). The association between cluster membership and outcomes is post-hoc and in-sample, so the abstract's phrase 'predictive of task outcomes' overstates what is demonstrated, but this is a statistical and external-validity limitation, not circularity: no feature is defined in terms of an outcome, no fitted parameter is renamed as a prediction, and no equation-level reduction appears. Section 7.2's agent is explicitly a proof-of-concept 'grounded in these recommendations,' and its prompt instructs the model to act as a specification-first planner; evaluating it on tasks from the same study limits generalization but does not make the evaluation equivalent to the design by construction, since the agent can still fail and is compared to an independent baseline. The threats section (Section 8) acknowledges the small sample and limited evaluation, which is a validity concern rather than a circular one. Self-citations in the references are background and not load-bearing. Therefore no circular step is present.

Assumptions & free parameters 3 free parameters · 3 assumptions · 0 invented entities

This empirical study introduces no new physical or theoretical entities. Its conclusions depend on methodological free parameters (k, pause threshold, quartile window), assumptions about participant representativeness and annotation validity, and the standard assumptions of k-means clustering. There are no fitted physical constants or invented mediators.

free parameters (3)
  • Number of clusters k = 3 (per language)
    In Section 6.2, k-means is run for k=2,3,4 and k=3 is selected based on silhouette (0.34 for F*, 0.173 for Verus). The choice of k determines the three archetypes that are the paper's main qualitative result.
  • Pause threshold = 5 seconds
    The pause_frac feature counts time gaps above 5s as deliberate thinking (Table 2). This hand-chosen threshold affects the pause_frac feature and therefore the clustering and the interpretation of 'deliberate pauses'.
  • Early time window Q1 = first 25% of session
    The early_spec feature is computed over Q1, defined as the first quartile of session time. The quartile cutoff is arbitrary and shapes the definition of 'early specification drafting'.
assumptions (3)
  • domain assumption Keyword-based annotation of edits into proof states is accurate.
    Section 4.5 assigns each telemetry event to Spec/Impl/Proof/etc. using language-specific keywords. All state-level analyses (RQ1, features in Table 2) rest on this annotation.
  • domain assumption The eight participants are representative of expert POPL users.
    Section 4.2 recruits all participants from Microsoft Research, with six of eight being language maintainers or designers. The paper generalizes patterns to the broader POPL community in Section 6.2 and conclusion.
  • standard math K-means on five z-normalized features yields meaningful groups.
    Section 6.2 assumes Euclidean k-means with n_init=auto and seed 42 captures real strategy structure; the low Verus silhouette (0.173) suggests this is fragile.

how reviews work

0 comments
Cite this review

Pith. "Pith review of What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus." pith.science (2026). https://pith.science/paper/IGVLSCP7

@misc{pith2026250802733,
  author       = {Pith},
  title        = {Pith review of: What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/IGVLSCP7}},
  note         = {Machine review of arXiv:2508.02733}
}
read the original 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

Figures

Figures reproduced from arXiv: 2508.02733 by the authors.

Figure 1
Figure 1. Two solutions for Task 3 in F* (left) and Verus (right). Each line of code is colored according to the state it belongs to. [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. RQ1: Percentage of time spent in each proof-writing state in F* and Verus, overall and split across task time quartiles. [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Number of verifier invocations across task time quartiles for all participants and tasks in F* and Verus, respectively. [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: States and actions over time during task T3 for F* participants P2 (C [PITH_FULL_IMAGE:figures/full_fig_p009_4.png]
Figure 5
Figure 5. Figure 5: A two-agent system where first the Proof Expert Agent generates a proof sketch and outlines a high-level roadmap: [PITH_FULL_IMAGE:figures/full_fig_p010_5.png]

Discussion (0). Sign in to comment.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. VeruSAGE: A Study of Agent-Based Verification for Rust Systems

    cs.OS 2025-12 unverdicted novelty 6.0 of 10

    LLM agents complete over 80% of tasks on a new 849-task Rust verification benchmark and over 90% on unfinished human proofs.

  2. Automating Formal Verification with Reinforcement Learning and Recursive Inference

    cs.LG 2026-05 unverdicted novelty 5.0 of 10

    RLVR training raises verified Dafny pass rates from 9.7% to 31.1% on a filtered benchmark while a Lean proof scaffold lifts success from 46.2% to 69.2% on a pilot set and solves 7 of 42 prior unsolved tasks.

Reference graph

Works this paper leans on

31 extracted references · 19 canonical work pages · cited by 2 Pith papers

  1. [1]

    Pranjal Aggarwal, Bryan Parno, and Sean Welleck. 2024. AlphaVerus: Bootstrap- ping Formally Verified Code Generation through Self-Improving Translation and Treefinement. arXiv:2412.06176 [cs.LG] https://arxiv.org/abs/2412.06176

    arXiv 2024

  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

    work page 2012

  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

    work page 2016

  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)

    arXiv 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

    work page 2015

  6. [6]

    Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fa- tima, Shuvendu Lahiri, and Nikhil Swamy. 2025. Towards Neural Synthesis for SMT-assisted Proof-Oriented Programming . In2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE) . IEEE Computer Society, Los Alamitos, CA, USA, 13–25. doi:10.1109/ICSE55347.2025.00002

    arXiv 2025

  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

    2008

  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)

    arXiv 2024

Show all 31 references
  1. [9]

    Rabe, Talia Ringer, and Yuriy Brun

    Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. 2023. Baldur: Whole- Proof Generation and Repair with Large Language Models. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (San F...

    2023

  2. [10]

    Lorch, Oded Padon, and Bryan Parno

    Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chanhee Cho, Hayley LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Haw- blitzel, Jon Howell, Jacob R. Lorch, Oded Padon, and Bryan Parno. 2024. Verus: A Practical Foundation for Systems Verification. In...

    2024

  3. [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)

    2024 arXiv

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

    2024

  5. [13]

    Kirby Linvill, Gowtham Kaki, and Eric Wustrow. 2023. Verifying Indistinguisha- bility of Privacy-Preserving Protocols. Proc. ACM Program. Lang. 7, OOPSLA2, Article 273 (Oct. 2023), 28 pages. doi:10.1145/3622849

    2023 doi

  6. [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)

    2024 arXiv

  7. [15]

    Lopes, Iris Ma, and James Noble

    Md Rakib Hossain Misu, Cristina V. Lopes, Iris Ma, and James Noble. 2024. To- wards AI-Assisted Synthesis of Verified Dafny Methods. Proc. ACM Softw. Eng. 1, FSE, Article 37 (July 2024), 24 pages. doi:10.1145/3643763

    2024 doi

  8. [16]

    OpenAI. 2025. OpenAI o3 (reasoning large language model) . https://openai.com/ index/introducing-o3-and-o4-mini/ Accessed 2025-07-19

    2025

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

    2020

  10. [18]

    Roger Pressman and Bruce Maxim. 2019. Software Engineering: A Practitioner’s Approach (9th ed.). McGraw-Hill Education

    2019

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

    2023

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

    2020

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

    2025

  14. [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)

    2024 arXiv

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

    2014

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

  17. [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 for- mat parsers. In Proceedings of the 43rd ACM SIGPLAN Interna...

    2022

  18. [26]

    Hanneli CA Tavante. 2021. A Data-Centered User Study for Proof Assistant Tools.. In PPIG

    2021

  19. [27]

    Sean Welleck and Rahul Saha. 2023. LLMSTEP: LLM proofstep suggestions in Lean. arXiv preprint arXiv:2310.18457 (2023)

    2023 arXiv

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

    2024

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

    2017

  22. [270]

    https://www.fstar-lang.org/papers/mumon/

  23. [2016]

    In 43rd ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages (POPL)

    Dependent Types and Multi-Monadic Effects in F*. In 43rd ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages (POPL) . ACM, 256–

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.