The reviewed record of science sign in
Pith

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

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

Rijul Jain , Shraddha Barke , Gabriel Ebner , Md Rakib Hossain Misu , Shan Lu , Sarah Fakhoury This is my paper

Reviewed by Pith T0 review T1 audit T2 compute T3 formal T4 kernel pith:IGVLSCP7record.jsonopen to challenge →

classification cs.SE cs.HC
keywords proofcodepoplsdevelopersdevelopmentexpertexpertsformal
0
0 comments X
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

This paper has not been read by Pith yet.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

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

    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

    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.