{"id":"b1f02531-4dbe-49b6-ac7b-dbe2c62d7483","arxiv_id":"2508.02733","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"A user study of eight experts shows that specification-first planning, low active errors, and measured verifier use predict proof task success, informing an AI proof agent design.","lead":"This paper logs the keystrokes, verifier calls, and pauses of eight expert programmers writing formal proofs in F* and Verus. It finds that experts who draft specifications early, keep errors low, and use the verifier sparingly succeed more often, and it uses these habits to build an LLM proof assistant.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Strategy–outcome association is confounded by task difficulty; the Verus 'planner' cluster is a singleton on the easiest task, so the central predictive claim is not supported.","rationale":"I read the paper in good faith: it is an honest exploratory study, and the telemetry instrumentation is a valuable contribution. However, the central claim that three strategies emerge and predict outcomes is not supported by the evidence as presented. The most load-bearing weakness is not the keyword annotation (which the authors partially cross-checked) but the study design: with 8 participants, 4 tasks of widely varying difficulty, and no control for task or participant, the observed associations between behavioral features and outcomes are likely confounded. The Verus singleton 'planner' cluster being the easiest task is a concrete instance. This confound matters more than annotation error because even perfect annotation cannot fix it. The agent case study compounds this with a model mismatch (o3 vs o4-mini), but the primary claim is the strategy finding. I therefore recommend the same conditional verdict as the reader, conditioned on the authors qualifying the predictive/causal language and performing a stratified or mixed-effects analysis. My agreement with the reader is partial: I share their concern about cluster validity but identify the task-difficulty confound as the core weak point rather than the annotation mapping.","tokens_in":14561,"tokens_out":9436,"duration_ms":112285,"concrete_test":"Report the participant-task mapping for each cluster (whether P1's three F* sessions are in the same cluster). Then re-run the outcome analysis stratified by task: e.g., control for self-reported effort (Table 1) in a logistic regression of success on early_spec and clean_state, or compare early_spec/clean_state only among sessions on the same task (e.g., T3 across languages). For Verus specifically, identify the singleton CS session; if it is P6 or P7 on T1, the strategy label is indistinguishable from task ease. A permutation test on cluster-outcome association with participant as a random effect would also quantify how fragile the n=9 F* finding is.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 6.2 clusters 17 sessions (9 F*, 8 Verus) from 8 participants without controlling for task, participant, or task difficulty. The feature set (early_spec, verify_fq, clean_state, pause_frac, defer) is strongly influenced by task complexity: Verus T1 averaged 11.8 min with self-reported effort 2/10, while T3 averaged 34.4 min and effort 5.5/10 (Table 1). The Verus 'Spec-first Planner' cluster (Table 4) is a singleton with the shortest duration (11.77 min), near-zero defer, and success; this is almost certainly an easy T1 session. Calling this a 'strategy' conflates task ease with a reproducible expert style. For F*, the three clusters have median durations 21.89, 22.74, and 24.41 min—differences of 1–3 min among 9 sessions—and the Planner and Balanced clusters both achieve 100% success; the only failing cluster is Rapid (2/3 success). Thus the data do not show a meaningful predictive advantage of 'spec-first planning' after accounting for task. The paper's threat section acknowledges small sample but does not address this confound; because the design guidance (Section 7) is causal ('bias toward early specification drafting'), the confound directly undermines the central claim.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":14850,"tokens_out":3223,"duration_ms":41370,"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":[{"comment":"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.","section":"§6.2, Tables 3–4"},{"comment":"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.","section":"§4.5"},{"comment":"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.","section":"§7.2.1"},{"comment":"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.","section":"§6.2"}],"minor_comments":[{"comment":"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.","section":"§4.3"},{"comment":"A verbatim quote from P8 appears twice in the same subsection; please remove the duplicate.","section":"§6.1.2"},{"comment":"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.","section":"Table 1"},{"comment":"There is a typo, 'Pariticpants,' in the paragraph describing cluster sizes; please fix it.","section":"§6.2"},{"comment":"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.","section":"§4.5"},{"comment":"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.","section":"Abstract"}],"recommendation":"major_revision","confidential_remarks":"The paper has a genuinely interesting dataset and a sensible descriptive narrative, but the central predictive claim is currently overstated relative to the evidence. The required revisions are feasible within the manuscript's scope: add task/participant controls or soften the claim, report annotation validation, and either strengthen or reframe the agent evaluation. I do not see grounds for rejection, but the current version would not support the abstract's claims as written."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper is worth reading for the telemetry dataset and the qualitative themes, but the central claim that a spec-first planner strategy predicts success is not supported by the data as analyzed. The Verus 'planner' cluster is one session on the easiest task; the F* clusters have near-identical completion times and success rates. That said, the descriptive effort/verifier patterns (RQ1/RQ2) are new and credible, and the qualitative analysis is grounded and useful.\n\nWhat's new: first cross-language telemetry study of F* and Verus proof sessions, 18k+ annotated events, with a clear methodology for state annotation and a released dataset (if released). The finding that experts interleave spec/proof/implementation throughout, and the different defer patterns between F* (assume/admit) and Verus (comments), are concrete and believable. The themes from post-task surveys (decomposition, early specs, lemma reuse, measured verifier use) line up with the telemetry, which is a good sign.\n\nSoft spots: the strategy clustering is the load-bearing part and it is thin. n=16 sessions, k-means with weak silhouette for Verus, and the association with outcomes is in-sample and confounded by task difficulty. The stress-test point holds: the Verus singleton planner is the T1 easy session; the F* planner cluster's median duration is only 2.5 minutes shorter than Balanced, and both have 100% success. Calling the spec-first style 'predictive' is an overreach. The agent case study compares against a baseline that is given the same prompts but no tool use instructions; two tasks, one run each, and the '3.75x reduction' is versus a baseline that never succeeds within 30 loops. That is too weak to support the abstract's claim of 'demonstrated improved performance.' The threats section is honest about small sample but does not address the task-difficulty confound.\n\nThe paper should be revised to reframe the strategy findings as descriptive, not predictive; report outcome associations as exploratory; and either remove or heavily qualify the agent claims. The design guidance in Section 7 is reasonable as hypotheses, not conclusions. I would send this to a serious referee: the dataset and descriptive analysis are valuable to the proof-engineering community, and the flaws are fixable with reframing, not fatal.","headline":"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.","tokens_in":15374,"tokens_out":1775,"would_cite":true,"duration_ms":21546,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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…","keywords":["proof-oriented programming","user study","telemetry","F*","Verus","proof-writing strategies","specification-first planning","LLM proof assistant"],"falsifier":"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.","tokens_in":14407,"feed_emoji":"🧩","tokens_out":8229,"duration_ms":90411,"temperature":0.7,"pith_summary":"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.","feed_headline":"Proof experts win by writing specs first, telemetry shows","feed_subtitle":"Eight experts' keystrokes show spec-first drafting and clean error states predict proof success.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Defines Verus, one of the two proof-oriented languages whose editor plugin is instrumented for telemetry and whose proof states are annotated.","marker":"[10]"},{"why":"Defines F*, the other proof-oriented language, including the dependent-type style that shapes how specification edits are identified.","marker":"[24]"},{"why":"Provides the prior IDE-instrumentation approach the study adapts and the earlier finding that most proof attempts involve rewriting specifications.","marker":"[20]"},{"why":"Supplies the prior observation study of proof assistant users whose themes the paper compares its qualitative findings against.","marker":"[21]"},{"why":"Supplies the coding-task benchmark from which tasks T2 through T4 are selected.","marker":"[4]"},{"why":"Supplies the reasoning LLM backing the agent and its baseline, against which the 3.75x reduction in verifier loops is measured.","marker":"[16]"},{"why":"Provides the multi-agent architecture used to implement the two-agent F* proof system.","marker":"[28]"},{"why":"Provides the documentation-retrieval method the agent pipeline uses to mimic expert lemma and library knowledge.","marker":"[8]"}],"fun_headline_variants":["Spec-first proof planners beat rapid verifiers in study","Telemetry data exposes three proof strategies, one wins","Proof experts draft specs early, not in one go","Why spec-first beats solver-spam in proof programming","Proof agent built on study tips cuts verifier calls"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Spec-first proof planners beat rapid verifiers in study","Telemetry data exposes three proof strategies, one wins","Proof experts draft specs early, not in one go","Why spec-first beats solver-spam in proof programming","Proof agent built on study tips cuts verifier calls"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000542,"raw_usage":{"total_tokens":2595,"prompt_tokens":939,"completion_tokens":1656,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":555,"completion_tokens_details":{"reasoning_tokens":1580}},"tokens_in":555,"tokens_out":1656,"duration_ms":16398,"temperature":1.0,"reasoning_tokens":1580,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T05:50:13.950924+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"Lorch, Oded Padon, and Bryan Parno","cited_arxiv_id":null,"evidence_quote":"Defines Verus, one of the two proof-oriented languages whose editor plugin is instrumented for telemetry and whose proof states are annotated."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Defines F*, the other proof-oriented language, including the dependent-type style that shapes how specification edits are identified."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the prior IDE-instrumentation approach the study adapts and the earlier finding that most proof attempts involve rewriting specifications."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the prior observation study of proof assistant users whose themes the paper compares its qualitative findings against."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the reasoning LLM backing the agent and its baseline, against which the 3.75x reduction in verifier loops is measured."}],"review_version":1}