🤖 database, how to judge specifications, proofs, and agents

(authored by agents unless marked 🧑)

223 sources, best-read first, then newest first. Generated from sources.jsonl; edit the reviews’ notes, not this page.

A Structured Benchmarking Dataset for TLA+ Specification Reasoning (poster) (2026)
- what: An early version of TLA+-Bench. It also reports how few datasets exist for TLA+ compared with other proof languages.
- number: 206 specs, 73 features per spec, 6,930 preference pairs
- number: survey behind it covers 144 papers
- how much was read: most of it read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_google.md
- record id: a-structured-benchmarking-dataset-2026
Agentic Proving for Program Verification (Claude Code on CLEVER, Lean 4) (2026)
- what: Runs Claude Opus 4.6 in Claude Code, with Lean tools, on the 161 CLEVER algorithm tasks. The agent writes formal specifications, implementations and Lean proofs. People manually review whether each specification matches the English task.
- number: 159/161 tasks get an arguably valid specification (98.8%, merged over runs)
- number: of 80 tasks with correct references: 65 specs proved equivalent (81.3%), 70 implementations certified (87.5%)
- number: 81 defective references, 13 valid unmatched alternatives, 2 failures, 65 equivalences
- number: 154/161 succeed in at least one of two pipelines (95.7%); 154/157 after excluding 4
- limits: Only proofs that Lean programs compute the right results. No proofs about distributed progress. The 98.1% headline number merges two runs. The authors review the reference-error count themselves. Human effort is not measured.
- how much was read: most of it read
- source; notes: Agentic Proving for Program Verification; notes: Agentic Proving for Program Verification; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_agents.md
- record id: agentic-proving-for-program-2026
Agentproof (2026)
- title: Agentproof: Static Verification of Agent Workflow Graphs
- what: Agentproof pulls a workflow graph out of LangGraph, CrewAI, AutoGen or ADK programs. It compiles temporal policies (rules about the order of events) into automata and checks every path in the model. It also has a runtime mode.
- number: 18 workflows with injected defects; 15 policies; 180 random traces
- number: human-gate check precision 0.75
- number: 5,000-node graph structural checks in 104.7 ms
- limits: It models only safety and structure. It finds whether an exit path is absent, but does not prove that the workflow eventually exits. The graph extractor is trusted. The test workflows are synthetic.
- how much was read: most of it read
- source; notes: Agentproof: Static Verification of Agent Workflow Graphs
- record id: agentproof-2026
AgentSpec (2026)
- title: AgentSpec: Customizable Runtime Enforcement for Safe and Reliable LLM Agents
- what: AgentSpec is a rule language for runtime monitors that intercept the actions of an LLM agent. Each rule has a trigger, a check, and an intervention. Rules are written by hand or generated by an LLM.
- number: 25 risk categories, 30 cases each
- number: manual rules: household hazard to zero, safe completion 58.62% to 54.26%
- number: generated embodied rules 95.56% precision, 70.96% recall; generated code rules detect 87.26% risky cases
- limits: It enforces safety only on executions that were tested. Nothing shows that the rules cover what the user intended. It does not cover liveness (the system eventually doing something good).
- how much was read: most of it read
- source; notes: AgentSpec: Customizable Runtime Enforcement for Safe and Reliable LLM
- record id: agentspec-2026
Agora (2026)
- title: Agora: Toward Autonomous Bug Detection in Production-Level Consensus Protocols with LLM Agents
- what: Three LLM agents propose adversarial scenarios under stated fault constraints. They also generate, repair and run unit tests against real consensus implementations (Raft, EPaxos, HotStuff, BullShark).
- number: 15 distinct previously unknown logic bugs (Raft 1, EPaxos 9, HotStuff 4, BullShark 1) vs 0 for ReAct baselines
- number: 46 reports, 34 judged real (26.1% false positives)
- number: three hours and at most 50 reflection iterations per run
- number: 58.6M tokens Gemini ablation; 5.32M tokens and about 106 per spec
- number: Plain Codex and Claude Code each solve 2/7
- number: Artifacts from 622 to 3,924 lines of code plus proof, 25-128 lemmas
- limits: The specification is supplied. Safety holds only within the supplied model, and there is no liveness. The comparison of human effort is not a controlled experiment.
- how much was read: most of it read
- source; notes: IDS: changing code and abstractions makes otherwise hard proofs tracta; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_shortlist.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_scholar.md
- record id: ids-2026
Intent Formalization (2026)
- title: Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents
- what: This research agenda argues that only the user can judge whether a spec is correct. It calls for support from tests, mutation, interaction and rich logic.
- number: TiCoder study with 15 professional developers: correct evaluation of AI code from 40% to 84%; cognitive load dropped (p = 0.007)
- limits: It is not a controlled benchmark.
- how much was read: most of it read
- source; notes: Intent formalization: why one number is insufficient; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_intent.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_shortlist.md
- record id: intent-formalization-2026
JS-SAM (2026)
- title: Executable JavaScript as a Checkable Specification Language: A JS-SAM Case Study on SysMoBench
- what: This controlled study compares LLMs writing JavaScript (SAM) specs against TLA+ specs of real systems. The authors check the specs by bounded exploration, plus replay against traces captured from the running systems.
- number: 4 models, 5 generations per cell
- number: Spin traces: 28 windows, 8 of 18 observable input combinations covered
- number: small tasks 40/40 complete passes; Raft scale 0/20 initially, 6/20 after one repair round
- number: state-changing conformance of original models ranges 0-86.4% though all pass syntax and invariants
- limits: It checks no liveness or temporal properties. It explores only to a bound. It does not prove that the implementation matches the model. The author designed the instrumentation, the reference model and the prompts.
- how much was read: most of it read
- source; notes: JS-SAM: a controlled case study separating specification shape from la; notes: JS-SAM: a controlled case study separating specification shape from la
- record id: js-sam-2026
KOSV (2026)
- title: KOSV: Kubernetes Ownership Safety Verifier
- what: It polls Kubernetes ownership state and normalizes it to JSONL traces. It checks two predicates written by the authors: at most one controller owns a resource, and no unexpected ownership transfer. Faults seeded into the observations test the checker itself.
- number: 20/20 runs pass (5 each: baseline, 500 ms delay, 2,000 ms delay, controller-manager restart)
- number: seeded faults 2/2 detected; denser-poll 6/6 pass
- number: experiments pinned to v0.1.10
- limits: It is sampled, finite testing. PASS is not proof that nothing is wrong. Transients shorter than the sampling interval can be missed. Delay faults do not affect controller-API traffic. The reproduction table is empty. Two of the four oracles are unimplemented.
- how much was read: most of it read
- source; notes: KOSV: Kubernetes Ownership Safety Verifier
- record id: kosv-2026
KVerus (2026)
- title: KVerus: Scalable and Resilient Formal Verification Proof Generation for Rust Code
- what: Claude Sonnet 4.0 generates proofs for Rust code as the proofs evolve. It uses a dependency graph, retrieval, verifier feedback and persistent memory.
- number: Table 4: MathSpec 81/104, allocator 50/89, CortenMM 52/166 vs baselines 10, 1, 5
- number: 251 of 313 tasks (80.2%)
- limits: It measures task completion in existing systems. It has no evaluation of distributed liveness.
- how much was read: most of it read
- source; notes: Repository retrieval and multi-function verification; notes: papers
- record id: kverus-2026
LeetProof (2026)
- title: Certified Program Synthesis with a Multi-modal Verifier
- what: LeetProof checks generated specifications against examples and reference implementations. It then synthesizes Velvet/Lean code, using SMT solvers to discharge proof goals automatically. A person finishes the remaining goals interactively.
- number: GPT-5.2 Velvet pipeline fully proves 28 of 50 tasks vs Lean-only 17
- number: 16 issues in VERINA (of 189 specs, 8.5%) and 18 in CLEVER (of 161, 11.2%) via property-based testing
- number: Verina issues took 9 minutes of property-based testing vs about 8 hours of LLM equivalence checking
- limits: It synthesizes algorithms with simple types. It has no distributed models and no liveness.
- how much was read: most of it read
- source; notes: Dafny, C verification, and the specification-intent gap; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_eval.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_eval.md
- record id: leetproof-2026
LemmaNet (2026)
- title: Automated Lemma Discovery in Agentic Program Verification
- what: GPT-5.2 plans reusable helper lemmas from C source, ACSL obligations and Rocq proof states. It adapts them to each obligation and proves them first.
- number: 298/641 SV-COMP and 66/300 NTP4VC tasks, 364/941 (38.7%, notes’ arithmetic), 10-minute/100-step budget
- number: 941 verification conditions: 641 SV-COMP from 131 programs plus 300 NTP4VC
- number: 364 solved vs AutoRocq 287 and Copra 240 with the same gpt-5.2 backend
- limits: The Linux scheduler/memory, Contiki and X.509 items are single verification conditions, not whole kernels.
- how much was read: most of it read
- source; notes: Dafny, C verification, and the specification-intent gap; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_agents.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_agents.md
- record id: lemmanet-2026
Liveness Proofs for Hardware Model Checking (2026)
- what: Certificates for checking hardware liveness (k-liveness, liveness-to-safety, rLive, stabilizer extraction). They are validated by eight SAT obligations on a witness circuit.
- number: 73 selected benchmarks found UNSAT
- number: certificate-checking overhead 4% (k-liveness), 7% (rLive), 59% (L2S)
- number: limits 14 GB, one hour
- number: older Sindoni pipeline: 16 optimized and 13 unoptimized rLive instances not certified; overhead 309%/469% over certified instances only
- limits: It covers finite-state hardware models. The soundness proof is mathematical, not mechanized. The aigunfair converter and the SAT checker are trusted.
- how much was read: most of it read
- source; notes: Liveness Proofs for Hardware Model Checking
- record id: liveness-proofs-for-hardware-2026
MutDafny (2026)
- title: MutDafny: A Mutation-Based Approach to Assess Dafny Specifications
- what: Mutates the Dafny implementation code and checks whether the spec still verifies. If it does, the contract may fail to exclude wrong behavior. A human must judge the mutants that survive.
- number: 40 mutation operators (30 adapted, 10 new)
- number: 794 files, 43178 LOC; 118,458 mutants generated: 76517 killed, 30459 survived, 10996 invalid, 486 timeout
- number: mean per-file mutation score 82%; pooled ratio computed by the notes is about 71.5%
- number: manual audit of 284 survivors in 24 files: 77 exposed five weak specs, 157 equivalent, 50 inconclusive; about 8 person-hours
- limits: A surviving mutant is not automatically a spec error. A killed mutant may only mean the proof annotations no longer suffice. It did not evaluate specs about time.
- how much was read: most of it read
- source; notes: Testing strength, mutations, and vacuity; notes: MutDafny: mutation survival needs adjudication; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_eval.md
- record id: mutdafny-2026
NTP4VC (2026)
- title: Neural Theorem Proving for Verification Conditions: A Real-World Benchmark
- what: 600 verification conditions (the proof goals a verifier produces) from C/Why3 programs are translated to Lean, Isabelle and Rocq with human-written rules. Annotations are removed to make them harder, and models must prove them.
- number: more than 7.5k VCs extracted, 600 selected; 300 C obligations from 17413 lines
- number: more than 2400 human-written mapping rules
- number: DeepSeek-Prover-V2-671B Lean pass@1/8 1.67/3.00; Minilang Isabelle 2.08/11.46; Sledgehammer 18.00; CoqHammer 5.67
- number: Why3 ATP baseline 22%; 10 min timeout
- limits: Each goal is a single condition, not a whole system. It has no distributed progress. The translation is trusted. Some cases may be unprovable. The prose says 11.56% but the table says 11.46.
- how much was read: most of it read
- source; notes: Neural Theorem Proving for Verification Conditions: A Real-World Bench
- record id: ntp4vc-2026
OSVBench (2026)
- title: OSVBench: Benchmarking LLMs on Specification Generation Tasks for Operating System Verification
- what: A benchmark in which an LLM writes a Python/Z3 specification of a syscall from a description. The spec is scored by whether it detects the same injected errors in code variants as the reference spec does. Declaration specs stay fixed.
- number: 245 tasks from 49 system calls, 5 variants each (1 correct, 4 with injected bugs)
- number: 12 LLMs; best pass@1 55.10% (Doubao-1.5-pro); five zero-shot models score zero
- number: five-example prompts use 20,000-30,000 tokens
- number: 245 tasks from 49 system calls (each: one correct and four vulnerable variants)
- limits: It covers functional and safety properties only, with no liveness. The LLM is given a description, assumptions and an abstract kernel model.
- how much was read: most of it read
- source; notes: OSVBench: executable specifications with a fixed external oracle; notes: OSVBench: executable specifications with a fixed external oracle; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/verified_primary_notes_20261012.md
- record id: osvbench-2026
PaxosLease Revisited: A Checked Model of Diskless Distributed Leases (2026)
- what: It has bounded checking in TLA+/TLC, six TLAPS arithmetic lemmas, and Python witnesses for the PaxosLease diskless lease protocol, with three acceptor changes. LLMs produced much of the artifacts, under line-by-line human review.
- number: Table 1 traces of 27, 36, 18, 36, 43 states
- number: Table 2: 491,037 base states, 37,425,056 crash/restart, 76,749,192 at quarantine; completed runs 2,179,760,458 and 2,411,951,538 states
- number: two larger searches stopped without violation at 3.86 and 4.46 billion states
- number: more than 40 hours on a 4-core Xeon, 64 GB
- limits: It covers safety only, with at most two proposers, three acceptors and three ballots. It does not show that the C++ code refines the model. The shipped binaries were not run. Searches that were stopped are not exhaustive. Fingerprint collisions qualify the largest runs.
- how much was read: most of it read
- source; notes: PaxosLease Revisited: A Checked Model of Diskless Distributed Leases
- record id: paxoslease-revisited-a-checked-2026
PLSemanticsBench (2026)
- title: LLMs Lean on Priors, Not Programming Language Semantics (PLSemanticsBench)
- what: A benchmark that tests whether LLMs follow explicitly given semantics of small imperative programs when the meanings of operators are changed. Models predict final states, rules or execution traces.
- number: 162 human-adapted, 165 model-translated, 165 fuzzer-generated programs; median sizes 19, 106, 794 lines
- number: 11 frontier LLMs; standard final-state accuracy about 90%, drops of 40-60 points under semantic changes
- number: full-trace accuracy nonzero for only four models, best just 35%
- number: 11 frontier LLMs; final-state accuracy about 90% on standard semantics, drops of up to 40–60 points under changes
- limits: It uses one-shot prompting, not proof search with compiler feedback. It is not an upper bound for agents with tools.
- how much was read: most of it read
- source; notes: LLMs Lean on Priors, Not Programming Language Semantics (PLSemanticsBe; notes: LLMs Lean on Priors, Not Programming Language Semantics (PLSemanticsBe
- record id: plsemanticsbench-2026
ProbGuard (2026)
- title: ProbGuard: Proactive Runtime Monitoring for LLM Agent Safety via Probabilistic Prediction
- what: ProbGuard learns a finite Markov model from recorded agent executions. It uses PRISM to predict unsafe states. It warns or halts when the predicted risk passes a threshold the user sets.
- number: 30 traces per scenario, below the theorem’s bounds
- number: household: no monitor 40.63% unsafe, 59.38% completion; reflection 14.07% unsafe, 47.74% completion
- number: 80.4% is relative retention of baseline completion
- number: early warning up to 38.66 s; zero-false-positive threshold max 15.84 s
- limits: The statistical theorem holds only with enough samples, which the experiments lack. It assumes the Markov property. The driving tests use Apollo software, not an LLM.
- how much was read: most of it read
- source; notes: ProbGuard: Proactive Runtime Monitoring for LLM Agent Safety via Proba
- record id: probguard-2026
Proofs Promptly (2026)
- title: Proofs Promptly: An Experience Report on Proof-Oriented Programming with AI Agents
- what: The report uses Copilot CLI with Opus 4.5, with skills, subagents and a REPL. It writes Pulse/F* separation-logic proofs of concurrent locks and semaphores, the MSQuic receive buffer, and a port of the OCaml garbage collector.
- number: Table 1 p. 3: 1 week/ $1229, 1 w ee k /$ 583, 2 weeks/ $1580; ab o u t am o n t han d$ 3,392 total (notes’ addition)
- number: Six-month manual estimate is the authors’ estimate, not a controlled comparison
- number: manual proof-engineering cost estimated at roughly half a year
- number: three experts, two weeks, versus about half a year manually (authors’ estimate)
- limits: Experts review the specs and supply the invariants that decide the proof. It has no theorem about distributed fairness or eventual progress.
- how much was read: most of it read
- source; notes: Proof-oriented programming at Microsoft; notes: papers; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_shortlist.md
- record id: proofs-promptly-2026
Re:Form (2026)
- title: Re:Form: Reducing Human Annotations in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny
- what: It trains models with supervised data and reinforcement learning to write Dafny annotations. It adds a reward that checks two things: the generated contract accepts every input the reference accepts, and it promises at least the reference’s outputs. This stops reward gaming with weak specs.
- number: 20,000-program collection, 3,000 supervised and 4,500 RL examples, 512 in-domain and 300 DafnyComp tests
- number: 14B RL verification 14.0% vs SFT 8.3%
- number: out-of-domain spec-superiority 0.077 vs 0.047
- number: 14B training: 64 GPUs for about 36 hours
- limits: The references are themselves autoformalized, so the implication does not certify fidelity to human intent. Mostly sequential functions.
- how much was read: most of it read
- source; notes: Re:Form: Reducing Human Annotations in Scalable Formal Software Verifi; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_agents.md
- record id: re-form-2026
Reality Is the Final Verifier: On Two Key Gaps in Agentic Software Engineering (2026)
- what: Argues that verification stops short in two places. The written requirements may not match what the stakeholder wants (the requirement gap). The model used to evaluate code may not match the real environment (the model gap). Proposes an inner loop, which revises code against the requirements, the environment model and the evaluator. Proposes an outer loop, which uses observations from deployment to revise those inputs.
- number: no new theorem, experiment, or implementation proof; Table 2 incidents are cited from other reports
- number: No measured completion rate or human-hours; Table 2 incidents are cited from other reports
- limits: A proposed architecture. No measured rate of autonomous completion and no human-hours result.
- how much was read: most of it read
- source; notes: Reality Is the Final Verifier: On Two Key Gaps in Agentic Software Eng; notes: Reality Is the Final Verifier: On Two Key Gaps in Agentic Software Eng; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_shortlist.md
- record id: reality-is-the-final-2026
RFC2TLA+ (2026)
- title: RFC2TLA+: Extracting and Verifying Formal Models from RFC Documents using Continuous LLM Feedback
- what: An LLM agent with 22 tools extracts communicating state machines and invariants from an RFC and emits TLA+. It refines the result using TLC counterexamples, for up to three rounds.
- number: 14 real RFCs; all get a TLC-accepted model in best-of-three
- number: correct models pass 36/42 runs; injected faults found 69/84 (33/42 deadlocks, 36/42 invariant violations)
- number: synthetic RFCs 16/18
- number: avg 710 TLA+ lines (262-1,944); state F1 0.97, transition F1 0.61 vs 0.49/0.21 for RFC2PSM
- limits: It uses TLC models checked within bounds, not code. Deadlock detection is weaker than liveness checking. The agent may change invariants, so a passing run does not show fidelity. No wall time or manual effort is reported. The artifact record is restricted.
- how much was read: most of it read
- source; notes: RFC2TLA+: extract both a model and invariants from a supplied RFC; notes: RFC2TLA+: extract both a model and invariants from a supplied RFC
- record id: rfc2tla-2026
Scope (2026)
- title: Detecting Inconsistencies in Arm CCA’s Formally Verified Specification
- what: Translates the Arm Realm Management Monitor spec into a Verus model checked by an SMT solver. It cross-checks different descriptions of the same behavior (conditions, effects, state diagrams, dependencies). It needs no reference implementation.
- number: 35 previously unknown bugs, all confirmed by Arm (of 38 candidates)
- number: 61.90% precision on one evaluated version/subset; do not mix with the 35 count
- number: about 11 months of effort, chiefly tool implementation
- limits: Consistency does not mean the spec is adequate: an omission shared by every view is missed. It also misses properties that are stated nowhere else. Its bit and byte semantics are incomplete, and uninterpreted functions cause false alarms. It has no benchmark for liveness over time.
- how much was read: most of it read
- source; notes: Specification errors and auditing; notes: Scope; notes: Appendix B: Concrete systems and theorem scope
- record id: scope-2026
Seeking Specifications: The Case for Neuro-Symbolic Specification Synthesis (2026)
- what: DeepSeek-R1 generates ACSL function contracts for C code. Optionally it also uses PathCrawler tests or Frama-C EVA alarms. The researchers check whether the contracts recover the intent, rather than preserve a recognized bug.
- number: Table 1 bug recognition: Basic 47/60, Famous 9/30, Anonymized Basic 50/60, Anonymized Famous 14/30
- number: 50 programs, four variants, three generations each; 55 PathCrawler examples
- limits: The study is qualitative. It has no end-to-end correctness proof of the generated contracts. By default the contracts encode the code, not the inferred intent. Figures 6 and 7 print the same contract despite opposite captions.
- how much was read: most of it read
- source; notes: Seeking Specifications: The Case for Neuro-Symbolic Specification Synt
- record id: seeking-specifications-the-case-2026
SHADOWBENCH (2026)
- title: SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization
- what: ShadowBench has 178 math problems. Humans repaired Lean ‘shadow’ statements, which let Lean check implication in both directions between a generated statement and the reference. This scores semantic alignment without a human reviewing each output.
- number: 178 problems, eight areas
- number: about 10 minutes of human construction per problem; 85% initial-draft coverage
- number: strongest configuration compilation/soft/full alignment 61.8 / 18.3 / 11.2
- number: agreement with experts 0.988, precision 1.000, recall 0.930
- limits: It covers mathematics, not software. Completeness depends on a trusted interpretation. Adapter failures give false negatives.
- how much was read: most of it read
- source; notes: SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignmen
- record id: shadowbench-2026
Software is infrastructure: failures, successes, costs, and the case for formal verification (2026)
- what: A chapter for teaching and policy. It collects secondary industrial reports on the costs of software failures and the benefits of formal verification (Philips ASD, 4SECURail, Dassault, AWS, CCF).
- number: Philips ASD: four-fold better quality, three-fold productivity
- number: 4SECURail projected benefit/cost 5.05
- number: Frama-C handled 85% of assertions on about 50 KLOC blocks at Dassault; a person-month saved per release
- number: six subtle bugs found binding CCF C++ traces to TLA+
- limits: The reports are heterogeneous and secondary. There is no common benchmark or controlled estimate. It proves no new theorem.
- how much was read: most of it read
- source; notes: Software is infrastructure: failures, successes, costs, and the case f
- record id: software-is-infrastructure-failures-2026
SoK consensus (2026)
- title: Systematization of Knowledge: Formal Verification of Consensus Protocols
- what: A survey that sorts consensus verification into model checking, deductive proofs, code proofs and hybrids.
- number: over 20 verified consensus protocols
- number: only about 30% of surveyed works address liveness
- number: Table 1 has 30 rows, 25 distinct protocols, 33 cited papers; only 8 rows list liveness
- number: Only about 30% of surveyed works address liveness
- limits: It gives no search date range and no count of how many papers were considered, so the reported fraction is not an unbiased census. Table 1 entries need checking against the cited papers.
- how much was read: most of it read
- source; notes: Systematization of Knowledge: Formal Verification of Consensus Protoco; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_liveness.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_tables.md
- record id: sok-consensus-2026
Spec-Harness (formerly VeriAct) (2026)
- title: VeriAct / Spec-Harness: Beyond Verifiability — Agentic Synthesis of Correct and Complete Formal Specifications
- what: The paper adds agent repair around JML spec generation. It scores specs in a harness that the evaluator owns, using four fractions: valid outputs accepted, bad outputs rejected, valid inputs admitted, invalid inputs excluded.
- number: v2 uses thresholds such as PostCorr >= 0.75 and PostComp >= 0.75 (operational choice)
- number: 120 SpecGenBench methods and 662 FormalBench methods
- number: SpecGen falls from 54% verifier acceptance to 24% meaningfully verified on SpecGenBench (§5.4)
- number: three refinement cycles; improvement of 5 points on SpecGenBench and 12 on FormalBench (§6.1)
- limits: Success is relative to the generated cases and the reference. The task supplies existing code, so eliciting intent is not tested. Feedback on the scoring set can inflate scores. Use withheld tests.
- how much was read: most of it read
- source; notes: Generated contracts and independent evaluation; notes: Spec-Harness, formerly VeriAct; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_agents.md
- record id: spec-harness-formerly-veriact-2026
Specula (2026)
- title: Specula: Scaling formal specifications for autonomous model checking of system code
- what: Specula writes TLA+ models and properties from system source code. It checks observed traces against the model and repairs disagreements. It then model checks for violations and tries to reproduce each one in the real code.
- number: 48 open-source systems; 249 reproduced bugs; 89 reported to maintainers; 68 confirmed and 24 fixed in that subset
- number: only 0.90% of generated properties are liveness; 99.10% safety
- number: 200 bugs via model checking, 49 during code reading/modeling
- number: median 3.69 hours and 4.33 per task
- number: 48 tasks, 16 scenario families, all fully TLC-verified; 62.5% first attempt; none over four repairs
- limits: Progress is not checked. Repairs for timeouts can reduce fidelity. The runtime monitor checks the topology, not the order of steps. A bounded model-checking pass does not prove that real agents terminate.
- how much was read: most of it read
- source; notes: TraceFix: generated PlusCal coordination protocols, with important lim; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_model_to_code.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_shortlist.md
- record id: tracefix-2026
Validating Formal Specifications with LLM-generated Test Cases (2026)
- what: GPT-5 generates positive and negative Alloy instances from English requirements, before the requirement is formalized. Expert formulas label the instances. The authors test whether the instances expose wrong student specifications.
- number: Table 3: Few prompt, 258 tests, 255 syntax-valid, 252 previous-consistent, 247 valid (96%), $3.56 - n u mb er : T ab l e 6 : 35 r e q u i r e m e n t s w i t h co m pl e t es u i t es, 4816 w r o n g s p ecs, 348 mi sse d, m e anmi sse d 6.43 - n u mb er : 258 r e q u es t e d t es t s; f e w - s h o tGP T - 5247 v a l i d (96$ 3.56); one-shot 205 (79%); zero-shot 118 (46%)
- number: By model: GPT-5 96%, Gemini 81%, Claude 76%, Mini 67%
- limits: It covers bounded structural models only. Suites are compared only over requirements that have complete valid suites. The persistent failures involve ambiguous English.
- how much was read: most of it read
- source; notes: Validating Formal Specifications with LLM-generated Test Cases; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_intent.md
- record id: validating-formal-specifications-with-2026
VeriContest (2026)
- title: VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation
- what: A Verus benchmark that scores spec, code and proof separately and end to end. Spec preconditions need proofs of equivalence in both directions. Postconditions are run on valid and invalid pairs. Proof-only mode rejects edits to the AST or contract and uses –no-cheating.
- number: 946 tasks (690 LeetCode, 256 Codeforces), 91 manual seeds
- number: median 276 positive and 2,670 negative examples per item
- number: GPT-5.5: 48.31% spec, 92.18% NL-to-code, 13.95% proof, 5.29% end-to-end
- number: 946 problems, median 276 positive and 2,670 negative tests each
- limits: Compatibility with one reference behavior is not general soundness. Negative examples the model generates itself may share its misunderstanding. Manual review is not shown to be blind. Possible contamination and selection bias. Algorithm tasks only, with no infinite distributed executions.
- how much was read: most of it read
- source; notes: VeriContest; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_eval.md
- record id: vericontest-2026
VERINA (2026)
- title: VERINA: Benchmarking Verifiable Code Generation
- what: A Lean benchmark that scores generation of code, spec and proof separately and in combination. It checks specs by trying to prove implications against a reference spec, then falls back to tests. A test pass without a proof returns ‘unknown’.
- number: 189 manually curated Lean problems
- number: ground-truth proofs for only 46 of 189
- number: 189 standalone programs
- limits: Finite tests miss missing constraints. It trusts the reference spec. Tasks are simple and standalone, with no interleavings, fairness or liveness. ‘Soundness/completeness’ here means containment between sets of programs, not soundness of the verifier.
- how much was read: most of it read
- source; notes: Generated contracts and independent evaluation; notes: VERINA; notes: papers
- record id: verina-2026
VeriSpecGen (2026)
- title: Intent-aligned Formal Specification Synthesis via Traceable Refinement
- what: It splits a description into requirements and ties tests and Lean clauses to each one. It repairs only the clauses implicated by a failed test.
- number: 86.6% pass@1 on Verina’s official harness
- number: 25 refinement iterations, 60 generated tests per problem
- number: 86.6% on the Verina SpecGen task with Claude Opus 4.5; up to 31.8 points over baselines
- number: 343,827 training pairs; training gives 15.6-18.2 points
- limits: Labels come from a reference implementation that may itself be LLM-written. The LLM judge fallback is only guidance. It has no distributed or liveness tasks.
- how much was read: most of it read
- source; notes: Generated contracts and independent evaluation; notes: Intent-aligned Formal Specification Synthesis via Traceable Refinement; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_intent.md
- record id: verispecgen-2026
Vero (2026)
- title: Vero: Can AI Agents Build Formally Verified Software Repositories?
- what: 43 multi-module Lean repositories with supplied APIs and 2,705 specifications. Agents either write code plus proofs, or fill in proofs for given code.
- number: Codex/GPT-5.5 xhigh: 27/43 joint, 25/43 proof-only
- number: verified_ironkv: 19/22 joint, 22/22 proof-only
- number: Audits find contradictory specs and proof/runtime mismatches
- number: 43 repository instances, 2,705 scored specifications
- limits: The 22 IronKV targets are not the full deployed IronKV proof. implemented_by lets tests run one implementation while the theorem describes another.
- how much was read: most of it read
- source; notes: Vero: repository generation, including a limited IronKV instance; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_agents.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_agents.md
- record id: vero-2026
Verus-SpecGym (2026)
- title: Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization
- what: It judges agent-written Verus specifications by running them against official and adversarial Codeforces tests.
- number: 581 tasks; best Gemini-3.1-Pro 77.8%; LLM judges miss 26% of detected failures
- number: 581 specification-writing tasks
- number: an LLM judge misses 26% of failures the evaluator catches
- number: 75-minute timeout per run
- limits: The tasks are algorithms. Testing is evidence, not a proof of equivalence in general.
- how much was read: most of it read
- source; notes: Dafny, C verification, and the specification-intent gap; notes: Generated contracts and independent evaluation; notes: Verus-SpecGym / Verus-SpecBench
- record id: verus-specgym-2026
Agent-C (2025)
- title: Enforcing Temporal Constraints for LLM Agents
- what: A small language for rules about the order of an LLM agent’s tool calls, their arguments, and state. Rules are translated to first-order logic and checked with the Z3 solver before each tool call. The paper proves that if every call is accepted, the whole trace obeys the rules.
- number: retail 115 benign tasks, airline 50, plus 17 adversarial tasks per domain
- number: GPT-5 utility 66.1% to 70.6% with 100% conformance and 0% harm
- number: LLM-translated rules on retail Qwen3-8B: 100% conformance, 42.11% utility, same as manual
- limits: It guarantees safety only relative to the rules it is given. It does not check that the rules capture what the user intended, nor that the task gets done. The survey’s claim that it reports only conformance is misleading.
- how much was read: most of it read
- source; notes: Enforcing Temporal Constraints for LLM Agents (Agent-C)
- record id: agent-c-2025
An Empirical Evaluation of Pre-trained Large Language Models for Repairing Declarative Formal Specifications (2025)
- what: Tests four OpenAI models on repairing faulty Alloy models, with the Alloy analyzer checking each attempt. Optionally a second agent turns the analyzer’s reports into repair advice.
- number: ARepair 38 faulty models; Alloy4Fun 1,936 unique models, GPT-4o on a 357-model subset
- number: 28 of 38 ARepair models repaired by GPT-4o / GPT-4-Turbo with second agent
- number: 201 of 357 Alloy4Fun models by GPT-4o
- number: at most six iterations
- limits: Covers only static Alloy models. No time-based behavior, no progress properties, no running code. Table 6 prints 55.7% where 206/357 is about 57.7%.
- how much was read: most of it read
- source; notes: Declarative-specification repair: repair the supplied model, check aga; notes: Declarative-specification repair: repair the supplied model, check aga
- record id: an-empirical-evaluation-of-2025
ATLAS (2025)
- title: Constrained LTL Specification Learning from Examples
- what: ATLAS learns LTL formulas (formulas about behavior over time) from good and bad example traces. It also takes user constraints and priorities, and solves with MaxSAT, an optimizing solver. It uses no LLM. Cases: Peterson mutual exclusion, a voting machine, robot-arm repair, and weakening an invariant.
- number: Table I: 30/30 tasks mean 43.65 s (Peterson); 10/10, 3.08 s (voting); 20/20, 37.25 s (robot arm); 53/78, 66.75 s (invariant weakening)
- limits: It finds the best formula only within the formula-size bound. A formula that fits the traces may not capture what the user meant. The benchmarks were built around the authors’ use cases. Using it needs formal-methods expertise.
- how much was read: most of it read
- source; notes: Constrained LTL Specification Learning from Examples (ATLAS)
- record id: atlas-2025
Atmosphere (2025)
- title: Atmosphere: Practical Verified Kernels with Rust and Verus
- what: Atmosphere is a verified kernel written in Rust and checked with Verus. The notes use it to count human effort and proof size.
- number: proof-to-code ratio 3.32:1; replay under 20 seconds; under 2.5 person-years
- number: 6K executable lines, 20.1K proof/spec lines: 14.3K spec and 5.8K proof/hints; 2.9K of specs for the top-level syscall model
- number: 6K executable lines, 3.32:1 proof/code ratio, under twenty seconds verification, under 2.5 person-years
- number: less than 2.5 person-years
- limits: The source contradicts itself. Section 6.3 says about two person-years, with fourteen months on verified code. The abstract and introduction say under 2.5 person-years in total and 1.5 for verification. The guarantees cover the kernel’s functional correctness and isolation. They do not cover liveness of distributed systems.
- how much was read: most of it read
- source; notes: Atmosphere: count specification work and acknowledge inconsistent tota; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_verus.md; notes: Atmosphere: Practical Verified Kernels with Rust and Verus
- record id: atmosphere-2025
AutoVerus / Verus-Bench (2025)
- title: AutoVerus: Automated Proof Generation for Rust Code
- what: An LLM agent that generates Verus proofs. Its checker, Lynette, compares the Rust syntax trees with proofs erased and compares the original and generated contracts. It also searches for admit and assume (which skip proof steps), so the agent cannot change the goal.
- number: 150 proof-only tasks (11 CloverBench, 38 Diffy, 78 MBPP, 23 Misc); 2,849 executable and 1,252 spec LOC
- number: 137/150 accepted with AutoVerus vs 67/150 direct GPT-4o
- number: 326 unsafe generated candidates caught (12.4%)
- number: 137/150 (91.3%) tasks proved after up to three complete attempts; 122/150 on the first attempt
- limits: The tasks are small and simple, with contracts fixed in advance. Spec quality is not scored. Deciding the intermediate function specs is itself part of systems verification (Sec. 7).
- how much was read: most of it read
- source; notes: AutoVerus / Verus-Bench; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_agents.md; notes: Recent agent termination evidence, with narrow scope
- record id: autoverus-verus-bench-2025
BEq+ / ProofNetVerif (2025)
- title: Reliable Evaluation and Benchmarks for Statement Autoformalization
- what: BEq+ tries to prove both directions of implication between a generated Lean statement and a reference statement. ProofNetVerif and RLM25 are labeled benchmarks for whether a statement is correct.
- number: ProofNetVerif: 3752 labeled pairs, 1142 correct; RLM25: 619 pairs from six projects
- number: BEq+ precision/recall/F1 98.0/48.3/64.7; Pearson 0.974, Kendall 0.872
- number: 118 entries (31.8%) with formalization errors in Lean 4 ports
- number: GPT-4o 50 samples: ProofNet# manual 45.1, BEq+ 23.4; RLM25 BEq+ 31.6
- limits: It covers mathematics only. The equivalence procedure is incomplete. People are needed for the references and the final labels. Results with no context are near zero.
- how much was read: most of it read
- source; notes: Reliable Evaluation and Benchmarks for Statement Autoformalization
- record id: beq-proofnetverif-2025
CLEVER (2025)
- title: CLEVER: A Curated Benchmark for Formally Verified Code Generation
- what: CLEVER is a Lean benchmark. A model generates a spec, which must be proved equivalent to a hidden, human-written reference spec. The model then generates code, which must be proved against that reference. The reference specs are noncomputable so that models cannot copy code logic.
- number: 161 problems (from 164 HumanEval; 3 excluded)
- number: default budget 600 seconds for pass@k-seconds
- number: human effort per problem: 25 minutes plus an additional 15 minutes, in places over an hour
- number: reference proofs 10-225 lines
- limits: It depends on the quality of the reference. Failed equivalence proofs give false negatives. HumanEval data may have leaked into training. It covers only list and numeric tasks, and has no liveness.
- how much was read: most of it read
- source; notes: Generated contracts and independent evaluation; notes: CLEVER; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_agents.md
- record id: clever-2025
CodeMetaAgent (2025)
- title: LLM Assisted Coding with Metamorphic Specification Mutation Agent
- what: CodeMetaAgent rewrites programming task descriptions with nine transformations: negation, translation, step decomposition, paraphrase, plus transformations of tests. It filters the rewrites with BERT similarity. It checks tests against an oracle implementation (a reference that gives the right answers).
- number: HumanEval-Pro 164 and MBPP-Pro 378 problems
- number: GPT-OSS MBPP-Pro pass@1 53 to 70
- number: oracle branch coverage 99.36 vs 99.81
- number: SWE-bench Lite: 69 bugs/23% baseline vs 90 bugs stated 30.3% (90/300 is 30.0%)
- limits: It handles only prose specifications and finite tests. BERT similarity does not certify that quantifiers or negation are preserved. Several arithmetic figures are inconsistent (233/300 is 77.7%, not 78.6%).
- how much was read: most of it read
- source; notes: LLM Assisted Coding with Metamorphic Specification Mutation Agent
- record id: codemetaagent-2025
DafnyBench (2025)
- title: DafnyBench: A Benchmark for Formal Software Verification
- what: Asks LLMs to restore missing assertions and loop invariants in Dafny programs that already have specs. The pass rate measures whether the proof gets finished. It does not measure whether the intent was formalized.
- number: 782 Dafny programs
- number: 782 verified ground-truth files; over 750 programs and about 53,000 lines (abstract)
- number: about 68% for the best model/prompt scheme
- number: built with Dafny 4.3.0
- limits: Only bans {:verify false} and assume false. This does not show that every way to cheat is caught. The public GitHub source may be in training data. Some specs just repeat the implementation. Scoring generated specs is only proposed (Appendix C). Verifying a weak contract that was handed in counts as success.
- how much was read: most of it read
- source; notes: DafnyBench; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_agents.md
- record id: dafnybench-2025
DafnyComp (2025)
- title: Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification
- what: The benchmark has 300 Dafny programs written by LLMs. Each has 2 to 5 chained functions, with contracts removed. The model must rebuild the contracts that connect the functions.
- number: 300 programs selected from 564 verified of 1,200 attempts
- limits: The review notes found no check against assume or admit (unproved assumptions) or against vacuous specs (specs that hold trivially). Over-restrictive requires clauses (preconditions) could make verification easier. The prompt in Appendix G contradicts Section 3.3. It excludes liveness, resource bounds and security policies. It has no concurrency.
- how much was read: most of it read
- source; notes: DafnyComp
- record id: dafnycomp-2025
DAISY (2025)
- title: Inferring multiple helper Dafny assertions with LLMs
- what: GPT-4.1 with heuristics over error messages finds where to insert missing helper assertions in verified Dafny programs taken from DafnyBench. Dafny and the Z3 solver then check the candidates.
- number: Table 3: w/o-one 153 (63.4%), w/o-two 76 (32.3%), w/o-all 8 (26.7%), combined 237 (46.8%)
- number: dataset 241 w/o-1, 235 w/o-2, 30 w/o-all instances
- number: default two insertion sites, ten candidates per site
- limits: The specs already exist. It excludes cases where removing an assertion still verifies. Faria et al. misquote single-assertion success as 63.2%.
- how much was read: most of it read
- source; notes: Inferring multiple helper Dafny assertions with LLMs (DAISY)
- record id: daisy-2025
FormalAlign (2025)
- title: FormalAlign: Automated Alignment Evaluation for Autoformalization
- what: FormalAlign is a trained Mistral-7B. It scores whether a formal Lean statement matches its informal statement. It was trained on wrong statements made by automatic mutation.
- number: 21 negative examples per positive
- number: alignment-selection: FormL4-Basic 99.21, MiniF2F-Valid 66.39, MiniF2F-Test 64.61 (Tables 4-6 give 66.70, unresolved)
- number: human 79.58% vs FormalAlign 65.00%; humans 3 hours for 80 items vs under 2 minutes
- limits: The score is learned. It is not a proof of equivalence. Accuracy on mutated statements is not evidence of agreement with intent. The review notes read v1, not the final ICLR version.
- how much was read: most of it read
- source; notes: FormalAlign: Automated Alignment Evaluation for Autoformalization
- record id: formalalign-2025
FSCQ LLM study (2025)
- title: Can Large Language Models Verify System Software? A Case Study Using FSCQ as a Benchmark
- what: It uses LLMs to fill existing unproved gaps in the proofs of FSCQ, a crash-safe file system. Search is best-first over tactics (proof commands) through Coq/SerAPI.
- number: GPT-4o 29.2% without hints, 38.1% with; hinted Gemini Flash/Pro 16.3%/25.7%
- number: Hinted GPT-4o: utilities 57.8%, Crash Hoare Logic 51.7%, file-system lemmas 20.8%
- number: No model solves a theorem whose human proof exceeds 512 tokens
- limits: It covers existing statements only. The proofs were public, so training leakage is a risk. There is no baseline using the prover alone, no new specification, and no liveness.
- how much was read: most of it read
- source; notes: FSCQ: file-system lemmas are harder than utility lemmas
- record id: fscq-llm-study-2025
FVAPPS (2025)
- title: Proving the Coding Interview: A Benchmark for Formally Verified Code Generation
- what: FVAPPS has Lean theorem statements that were auto-translated from APPS coding problems. They contain sorry placeholders (marks for missing proofs) that agents fill in. They come in three quality tiers.
- number: 4715 problems; 2089 pass the unit-test-guarded tier (later paper reports 1083 guarded)
- number: median 4 theorems per sample
- number: manual audit of 100 samples labels too trivial, nontrivial, unprovable
- number: 4,715 samples, 1,083 curated; Sonnet proves 30%
- limits: Type-checking does not certify that a statement is adequate. The notes infer that the election contract in Fig. 2 is satisfied by a constant zero. The quality of the natural-language intent is not independently certified.
- how much was read: most of it read
- source; notes: FVAPPS; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_eval.md
- record id: fvapps-2025
Informal to Formal (2025)
- title: From Informal to Formal – Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs
- what: It splits the path from English requirements to proofs into six tasks, across Coq, Lean, Dafny, ACSL and TLA+. It releases training data distilled with GPT-4o.
- number: 18k high-quality instruction-response pairs
- number: Pages 26984-27003
- number: about 18,000 instruction-response pairs from over 4,000 verified references; about 14,000 train and 4,000 evaluate
- limits: It is a benchmark of separate tasks. It does not show that the models are faithful to real distributed implementations.
- how much was read: most of it read
- source; notes: TLAiBench and the Foundation challenge: useful harnesses, limited meas; notes: Natural language to temporal logic and TLA+; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_agents.md
- record id: informal-to-formal-2025
LLMs as Planning Formalizers: A Survey for Leveraging Large Language Models to Construct Automated Planning Models (2025)
- what: The survey covers about 80 works in which LLMs generate planning domains and problems from natural language.
- number: approximately 80 existing works
- limits: The review notes found no 24.8/35.1 percent statistic. So the headline number in the Safe Agents survey is unsupported by this citation.
- how much was read: most of it read
- source; notes: LLMs as Planning Formalizers: A Survey for Leveraging Large Language M
- record id: llms-as-planning-formalizers-2025
LMGPA (2025)
- title: Towards Language Model Guided TLA+ Proof Automation
- what: An LLM splits hard TLAPS proof obligations into smaller claims. Symbolic provers check them. The invariant is given as input.
- number: 26 inductiveness proofs of distributed protocols plus 93 math theorems (119 total)
- number: Distributed protocols (Table 1 p. 13): symbolic-only 38.5%; DeepSeek-V3.2-Exp 50.0% with decomposition (13/26), 0% direct; Claude 3.7 Sonnet 42.3% vs 15.4% direct; GPT-5 42.3% vs 3.8% direct
- number: Runtime DeepSeek 9h 14m vs Claude 1h 32m
- number: Four decomposition attempts per claim; TLAPS timeouts Z3 5 s, Zenon 10 s, Isabelle 30 s
- limits: It tests proving a supplied invariant. It does not test finding one or reading vague requirements. Training leakage is possible from public protocol proofs (Section 4.2). The suite leaves out both learning switches, chord and hybrid broadcast.
- how much was read: most of it read
- source; notes: LMGPA: prove supplied invariants rather than discover them; notes: TLAPS proof generation grew beyond the January 2025 toy study; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_agents.md
- record id: lmgpa-2025
miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward (2025)
- what: Re-checks the miniF2F Lean statements against the original competition questions and corrects them. Separates simplified tasks from tasks faithful to the competition.
- number: 488 problems; over 300 Lean 4 statements corrected; 16 problems with no solution
- number: Herald test accuracy automated judge 97.5% vs human 62.7% on v1
- number: Kimina+Goedel-V2-7B test 49.2 / 69.7 / 61.5 for v1/v2s/v2c; validation 54.9 / 70.1 / 62.3
- number: Pipeline about 36% (40% on the original) vs 97% and 69% for the two stages alone
- limits: About mathematics, not software. Judging fidelity needs a human.
- how much was read: most of it read
- source; notes: miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forw; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_eval.md
- record id: minif2f-lean-revisited-reviewing-2025
NL2Contract (2025)
- title: Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification?
- what: LLMs write executable preconditions and postconditions for Python from signatures and docstrings. CrossHair searches for violations. Mutation tests estimate how well the contracts tell correct from wrong code.
- number: GPT-5 accept@1/5/10 and sound@1/5/10: 89.0 94.6 95.1 81.1 88.7 90.0
- number: real buggy cases: 14 of 31 found with each model
- number: contract unsound only if CrossHair finds a violation in 60 s
- limits: Its notion of soundness counts unknown results and timeouts as sound. It has no liveness. A code release is promised but no URL is given.
- how much was read: most of it read
- source; notes: Beyond Postconditions: Can Large Language Models infer Formal Contract; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_eval.md
- record id: nl2contract-2025
On the Effectiveness of Large Language Models in Writing Alloy Formulas (2025)
- what: The paper tests LLMs on eleven familiar graph and relation requirements. The LLMs write Alloy formulas from English, write them from a reference, or complete partial formulas. Automated bounded equivalence checks grade the results.
- number: both LLMs find at least one valid solution among twenty requested per property
- number: each LLM completes all but 1 sketching task; both failures fixed with syntax feedback
- number: default scope three
- limits: The checks cover bounded equivalence only. Familiar small tasks are weak evidence for unfamiliar distributed-system guarantees.
- how much was read: most of it read
- source; notes: On the Effectiveness of Large Language Models in Writing Alloy Formula
- record id: on-the-effectiveness-of-2025
ParCleanse (2025)
- title: Validating Network Protocol Parsers with Traceable RFC Document Interpretation
- what: GPT-4o extracts packet layouts and constraints from RFCs, with links back to the source text. Z3 generates valid packets and packets that break exactly one rule, and real parsers in C, Go and Python run them. An LLM diagnoses whether each failure is a spec error or an implementation error.
- number: Table 2 precision/recall: Total 100/100 99/95 94/91 98/82 73/44
- number: Table 3: 69 unique, 68 new, 36 confirmed bugs
- number: golden formats: Babel 171 lines/5 h; BGP-4 164 lines/6 h
- limits: It recalls dependent rules poorly. Every discrepancy was checked by hand. It covers input-validation safety, with no liveness.
- how much was read: most of it read
- source; notes: Validating Network Protocol Parsers with Traceable RFC Document Interp
- record id: parcleanse-2025
PAT-Agent (2025)
- title: PAT-Agent: Autoformalization for Model Checking
- what: Turns a natural-language system description, properties and expected outcomes (VALID or INVALID) into a CSP# model for the PAT model checker. Repairs the model from counterexamples for up to five rounds.
- number: 40 tasks (26 PAT, 6 textbook, 8 Alloy4Fun), 133 assertions
- number: 100% full-pass after repair; 75% before repair, 77.5% after one, 87.5% after two; direct models 37.5-52.5%
- number: 4.34 minutes per system average
- number: 20-person user study, separate
- limits: Finite models only, not application code. No progress proofs at unbounded size and no refinement. Section VI says a repair pipeline gave negligible gain, which conflicts with the repair-loop results.
- how much was read: most of it read
- source; notes: PAT-Agent: users supply descriptions and the outcomes they want checke; notes: PAT-Agent: users supply descriptions and the outcomes they want checke
- record id: pat-agent-2025
ProofWright (2025)
- title: ProofWright: Towards Agentic Formal Verification of CUDA
- what: An agent writes VerCors annotations (permissions, preconditions, invariants) for CUDA kernels. It repairs them using verifier errors. A second path derives a proof of equivalence to the PyTorch reference, via Rocq.
- number: 100 KernelBench L1 problems: 74 pass memory safety and race freedom, 17 solver instability, 9 agent failure
- number: 14 simple kernels get safety plus equivalence; 3 loss functions partial
- number: About 3 minutes per kernel
- number: Ablation: no guide gives 0, few-shot only 13%
- limits: A persistent annotation guide was seeded from 10 manual kernels, and every update was reviewed by hand. The link from Rocq to VerCors is untrusted and was checked manually. The proof agent’s model and budget are not stated. There is no liveness. There is no repository link.
- how much was read: most of it read
- source; notes: ProofWright verifies concurrent GPU code, with a human-reviewed transl
- record id: proofwright-2025
PSMBench (2025)
- title: PSMBench: A Benchmark and Dataset for Evaluating LLMs Extraction of Protocol State Machines from RFC Specifications
- what: A benchmark of 14 protocols with human-annotated state machines. It scores nine LLMs on extracting state machines from RFC text.
- number: 14 protocols, 1,580 RFC pages, 108 states, 297 transitions
- number: annotation about three days per protocol
- number: best state F1 0.715 (DeepSeek-V3), transition F1 0.378
- number: 14 protocols, 1,580 RFC pages, 108 states, 297 transitions; annotation about three days per protocol
- limits: It scores agreement with the annotations, not protocol safety. The annotations themselves need auditing, since RFC2TLA+ finds missing behaviors. Settings in the appendix give other scores.
- how much was read: most of it read
- source; notes: PSMBench / RFC2PSM: extraction accuracy, with human ground truth; notes: PSMBench / RFC2PSM: extraction accuracy, with human ground truth
- record id: psmbench-2025
RagVerus (2025)
- title: RagVerus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation (RepoVBench)
- what: GPT-4o with AutoVerus-style repair retrieves related repository code and proofs to complete tasks on the VeriSMo security module.
- number: 75 successful, permitted completions of 383 tasks (19.6%, notes’ arithmetic)
- number: 383 tasks from 2073 code pieces in 52 modules (52 no-dependency, 331 dependency)
- number: RAG 75/383 (19.6%) vs 59/383 (15.4%); unchecked Verus alone 84
- number: 27% relative improvement on RepoVBench (383 proof-completion tasks)
- limits: One proof was removed while the surrounding library remains. So it is not a fresh, complete proof.
- how much was read: most of it read
- source; notes: Repository retrieval and multi-function verification; notes: RagVerus / RepoVBench; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/verified_primary_notes_20261012.md
- record id: ragverus-2025
Rango (2025)
- title: Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification
- what: A fine-tuned DeepSeek-Coder 1.3B model retrieves related proofs and premises for each changing Coq goal, and searches over tactic rollouts.
- number: CompCert 1,977 (32.5%) of 6,091; all CoqStoq 3,325 (32.0%) of 10,396; held-out projects 352/1,171
- number: Ten minutes per theorem
- limits: Public proofs may have leaked into the training data. It does not regenerate proofs that a compiler preserves semantics.
- how much was read: most of it read
- source; notes: Coq: CompCert and Verdi lemmas, not newly built complete compilers/pro
- record id: rango-2025
Remix (2025)
- title: Multi-Grained Specifications for Distributed System Model Checking and Verification (Remix)
- what: Refines coarse TLA+ protocol actions into detailed ones where concurrency matters. It mixes levels of detail to keep model checking practical, and checks the model against implementation executions (ZooKeeper).
- number: six severe bugs violating five types of invariants
- number: Six deep ZooKeeper bugs found and fixes verified
- number: abstract: found six severe bugs that violate five types of invariants
- number: six severe bugs
- limits: The notes infer that matching the implementation and fixing bugs found by the model checker do not validate the chosen client guarantee, and do not prove liveness for unbounded cases.
- how much was read: most of it read
- source; notes: Choosing top-level distributed guarantees and trusted boundaries; notes: Appendix B: Concrete systems and theorem scope; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_model_to_code.md
- record id: remix-2025
super_sketch / super_fix (2025)
- title: The Burden of Proof: Automated Tooling for Rapid Iteration on Large Mechanised Proofs
- what: Isabelle tooling. super_sketch splits goals and runs Sledgehammer on them concurrently. super_fix repairs proof scripts after the model changes. Applied to the CXL safety proof.
- number: 310k lines of code, 54,128 lemmas
- number: about one day per obligation-matrix iteration
- number: fewer than 100 unresolved subgoals out of 50,000+
- number: two-year span is elapsed time
- limits: Unsolved goals stay as sorry (a placeholder for a missing proof). Neither tool designs the whole invariant.
- how much was read: most of it read
- source; notes: Related work absent from the first pass: The Burden of Proof
- record id: super-sketch-super-fix-2025
TickTock (2025)
- title: TickTock: Verified Isolation in a Production Embedded OS
- what: TickTock verifies isolation in an embedded OS. The notes use its distributions of replay time and its list of trusted functions.
- number: 3,603 lines of checked annotation across 2,581 functions
- limits: It lists the trusted functions, which are trusted because of tool limits, because they are ghost-only code (used only in proofs), or because they are out of scope. Its lower annotation ratios may reflect narrower guarantees. That last point is the notes’ inference.
- how much was read: most of it read
- source; notes: TickTock: measured replay distributions and explicit trust exemptions
- record id: ticktock-2025
TLAiBench (2025)
- title: tlaplus/TLAiBench
- what: 9 puzzle descriptions (for example DieHard, DiningPhilosophers, TowerOfHanoi) and 6 gold specs. A script asks an LLM to translate each description, then runs the syntax check and TLC.
- number: 9 puzzle descriptions
- number: 6 gold specs
- number: inspected commit of 6 Feb 2026: ten puzzle descriptions, six gold models
- number: no distributed implementation tasks; dining philosophers has no gold model
- limits: No results are reported. Checking against the gold spec by refinement is only stated as a grading idea, and is not run at scale.
- how much was read: most of it read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_google.md; notes: Additional tools, not counted as papers; notes: TLAiBench
- record id: tlaibench-2025
Veil (2025)
- title: Veil: A Framework for Automated and Interactive Verification of Transition Systems
- what: It embeds distributed transition systems in Lean. It sends first-order proof obligations to SMT solvers and leaves the rest as interactive Lean goals.
- number: 16 evaluated cases incl. Rabia, SCP, Suzuki-Kasami, Vertical Paxos
- number: 1704 non-empty, non-comment lines of Lean; 85 actions and 185 invariants; about 100 lines per file
- number: 16 case studies: 1704 lines of Lean, 85 actions, 185 invariants
- number: Veil verifies all, Ivy fails on two (Paxos and Vertical Paxos time out)
- limits: It evaluates checking supplied invariants, not finding them. It is not an LLM agent. All its guarantees are safety. The notes record no agent success rate.
- how much was read: most of it read
- source; notes: Veil: proofs in Lean with automatic first-order checks; notes: Veil: a promising proof interface, with no agent rate established here; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_systems.md
- record id: veil-2025
Vericoding benchmark (2025)
- title: A Benchmark for Vericoding: Formally Verified Program Synthesis
- what: Fixed formal specs in Dafny, Verus and Lean. Agents fill in implementation and proof holes. Validation blocks bypasses (assume, false/sorry), and fixed templates prevent changes to the spec.
- number: 12,504 specs: 3,029 Dafny, 2,334 Verus, 7,141 Lean; 6,174 new/translations
- number: about 9% of sampled successful specs too weak and another 15% had poor translations
- number: 12,504 specs (3,029 Dafny, 2,334 Verus, 7,141 Lean)
- number: Success: 82% Dafny, 44% Verus, 27% Lean
- limits: Quality statistics come from five sampled successes per language and source, not from all items. The cleanliness score is a heuristic. A checker establishes the contract that was submitted, even if it is lossy or weak.
- how much was read: most of it read
- source; notes: A Benchmark for Vericoding; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_agents.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_eval.md
- record id: vericoding-benchmark-2025
VerifyThisBench (2025)
- title: VerifyThisBench: Generating Code, Specifications, and Proofs All at Once
- what: Models generate code, spec and proof together for VerifyThis competition challenges. They use seven tools: Dafny, Why3, Frama-C, Verus, VeriFast, VerCors and TLA+. Each model gets five attempts with checker feedback. The XS variant removes parts of the verified submissions.
- number: 41 challenges / 154 tasks; XS total 580 (226 code, 233 spec, 121 loop); 481 is stale
- number: original human contest: 90 minutes per challenge
- number: 41 challenges, 154 tasks, 580 sub-tasks
- number: o3-mini under 4% zero-shot, 9.37% after five feedback rounds
- limits: Alignment confidence is the model’s self-assessment (the paper calls it an ‘optimistic upper bound’). There is no independent exhaustive oracle for alignment. The notes did not establish that assume, admit or axiom is enforced. TLA+ gets no scoring for fairness or liveness. The human contest judges correctness, completeness, elegance and automation.
- how much was read: most of it read
- source; notes: VerifyThisBench / XS; notes: VerifyThis: human assessment supplies an intent layer; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_eval.md
- record id: verifythisbench-2025
VeriStruct (2025)
- title: VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus
- what: OpenAI o1 plans the module’s abstractions and type invariants, orders the method proofs, and repairs them in Verus. Claude Code with Sonnet 4.5 is also evaluated.
- number: ten of the eleven modules; 128 out of 129 functions (99.2%)
- number: Claude Code/Sonnet 4.5: eight modules, 102 functions
- number: 11 modules and 129 counted functions; 10 modules and 128 functions verify
- number: simple iterative baseline: 4 modules, 52 functions; Claude Code: 8 modules, 102 functions
- limits: Eleven data structures do not establish ability on protocols or liveness.
- how much was read: most of it read
- source; notes: Repository retrieval and multi-function verification; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_agents.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_agents.md
- record id: veristruct-2025
VeruSAGE (2025)
- title: VeruSAGE: A Study of Agent-Based Verification for Rust Systems
- what: 849 proof-writing tasks from eight verified systems (IronKV, Anvil, Atmosphere, Vest and others). A proof body is removed, and an agent loop with a 20-minute budget must restore it.
- number: Table 5 model totals: o4-mini 41%, GPT-5 55%, Sonnet 4 64%, Sonnet 4.5 81%; Sonnet 4.5 with plain Copilot proves 688/849 (80.9%)
- number: Anvil library 100%, Anvil controller 37%, IronKV 84%, Atmosphere 83%
- number: Specialized harness about 1.6x time and 2.2x cost on whole projects
- number: 849 tasks from eight systems (nine projects): Anvil temporal library 104, Anvil vreplicaset controller 63, IronKV 118, mimalloc 89, Node Replication 29, NRKernel 204, Atmosphere 157, persistent storage 63, Vest 22
- limits: Failures center on discovering inductive invariants (facts that hold initially and stay true after every step). The Anvil library lemmas are not the same as proving that a new controller eventually reconciles.
- how much was read: most of it read
- source; notes: VeruSAGE: high overall rates hide controller-invariant difficulty; notes: VeruSAGE / VeruSAGE-Bench; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_agents.md
- record id: verusage-2025
VLTL-Bench (2025)
- title: Verifiable Natural Language to Linear Temporal Logic Translation: A Benchmark Dataset and Evaluation Suite
- what: It scores four steps of translating natural language to LTL. The steps are finding propositions, translating temporal structure (judged by logical equivalence, not string match), grounding to executable predicates, and classifying satisfying and violating traces.
- number: datasets: Kitchen Assistant 10,000, Search-and-rescue 7,304, Traffic-light 7,319, Warehouse 7,457
- number: built from 36 expert nl2spec templates
- number: Table 2: four generated datasets of 10,000; 7,304; 7,319; 7,457 entries (32,080 total) reusing 43 templates
- number: 36 expert-crafted lifted NL-LTL pairs plus 7 new ones
- limits: Its equivalence check only flags a difference. It does not say whether one formula is weaker or stronger. Two traces cannot establish equivalence or liveness. It has no proof, no code, and no audit of how far to trust agents. The text says three datasets but the table lists four.
- how much was read: most of it read
- source; notes: Temporal requirement translation: VLTL-Bench and GraFT; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_eval.md; notes: papers
- record id: vltl-bench-2025
Zhou TLAPS 2025 (2025)
- title: Retrieval-Augmented TLAPS Proof Generation with Large Language Models
- what: GPT-4o splits a goal into smaller obligations and tries OBVIOUS and BY AllProvers. If those fail, it writes a proof, using verified steps retrieved from the TLA+ Examples repository.
- number: Three selected obligations only
- number: Boyer-Moore majority safety theorem failed after ten decompositions
- number: Smaller initialization obligation: valid proofs in all three attempts, about two minutes
- number: three obligations only
- limits: The case is a sequence algorithm, not distributed consensus. There is no liveness result and no broad success rate.
- how much was read: most of it read
- source; notes: TLAPS proof generation grew beyond the January 2025 toy study; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_agents.md; notes: Two further TLA+ evaluation papers already in collection
- record id: zhou-tlaps-2025-2025
Clover (2024)
- title: Clover: Closed-Loop Verifiable Code Generation
- what: GPT-4 reconstructs code, contracts and English documentation from one another. Dafny and cross-checks then inspect whether they agree.
- number: 52 of 60 correct examples accepted at ten attempts; tested adversarial examples rejected (Section 4)
- limits: LLM reconstructions are correlated, so they can share a mistake. Agreement does not prove the English intent was encoded faithfully.
- how much was read: most of it read
- source; notes: Dafny, C verification, and the specification-intent gap; notes: Generated contracts and independent evaluation
- record id: clover-2024
Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages (2024)
- what: Scores LLM-written Dafny specs by checking concrete input/output pairs symbolically, including pairs with deliberately wrong outputs. In a set-intersection example, the contract says every result is in both inputs. It does not require every common element to appear.
- number: applied to 64 of 153 MBPP-DFY specifications
- limits: A failed verification usually means ‘unknown’, not ‘refuted’. Rejecting bad pairs measures only the pairs chosen. It does not show the spec rejects bad outputs in general.
- how much was read: most of it read
- source; notes: Testing strength, mutations, and vacuity; notes: User-intent formalization in verification-aware languages
- record id: evaluating-llm-driven-user-2024
IronSpec (2024)
- title: IronSpec: Increasing the Reliability of Formal Specifications
- what: Tests whether a Dafny specification matches what developers expect. It uses three methods: checks with unconstrained inputs and outputs, small proofs of cases that should or should not be allowed, and mutations of the specification.
- number: 14 specifications including six real verified systems; ten spec bugs confirmed by authors
- number: 70 small test proofs, 21 needed help averaging 1.7 added lines
- number: 61 surviving mutations, 13 judged intended
- number: human effort hours to days; DaisyNFS about one to two hours
- limits: The checks expose suspicious differences. They do not show the spec perfectly matches intent. It gives no success rate for autonomous spec generation.
- how much was read: most of it read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_foundations.md; notes: Specification errors and auditing; notes: IronSpec
- record id: ironspec-2024
miniCodeProps (2024)
- title: miniCodeProps: a Minimal Benchmark for Proving Code Properties
- what: Lean theorem statements about list, natural-number and sorting code, taken from TIPHaskell. It has a mode that writes the whole proof and a mode that searches over tactics.
- number: 201 theorem statements: 86 easy, 115 medium/hard
- number: pass@32 candidates
- number: 201 Lean 4 theorem statements
- number: GPT-4o 70/201 at pass@32 and 75/201 with refinement (Table 4)
- limits: It has no spec generation or equivalence checking. It has no broad adversarial harness and no audit of axioms. Termination of recursion is not liveness of a distributed system.
- how much was read: most of it read
- source; notes: miniCodeProps; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_agents.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_agents.md
- record id: minicodeprops-2024
nl2postcond (2024)
- title: Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?
- what: Has LLMs generate executable postconditions from plain descriptions. Measures both correctness and whether they reject known buggy implementations (bug-completeness).
- number: catches 64 real-world historical bugs from Defects4J
- limits: Rejecting those bugs does not fully describe which outputs are acceptable. Reference programs and tests remain part of the oracle. Correctness is only with respect to the provided tests.
- how much was read: most of it read
- source; notes: Testing strength, mutations, and vacuity; notes: Natural-language postconditions and known faulty implementations
- record id: nl2postcond-2024
PALM (2024)
- title: Proof Automation with Large Language Models
- what: GPT-3.5 drafts a whole Coq proof. Symbolic repairs, CoqHammer, premise retrieval and backtracking then fix lower-level errors.
- number: Formative study: 579 Verdi theorems, 520 errors
- number: CoqGym: GPT-3.5 4377/10842 (40.4%), GPT-4o 4614 (42.6%), Llama-3-70B 4155 (38.3%)
- limits: It has no result for a complete new Verdi/Raft proof.
- how much was read: most of it read
- source; notes: Coq: CompCert and Verdi lemmas, not newly built complete compilers/pro
- record id: palm-2024
Selene (2024)
- title: Selene: Pioneering Automated Proof in Software Verification
- what: It isolates existing Isabelle lemmas from seL4, supplies their dependencies and examples, and retries GPT-3.5/GPT-4 proofs with error repair and retrieval.
- number: Table 2 p. 1781: GPT-4 five-attempt rates 51.8, 12.5, 1.7, 15.8 percent across short, medium, long and proof-with-definition categories
- limits: It covers selected kernel lemmas only. Hints from the proof prefix are privileged information.
- how much was read: most of it read
- source; notes: seL4: from whole-proof guessing to proof-state search; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_agents.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_agents.md
- record id: selene-2024
Verus SOSP 2024 (2024)
- title: Verus: A Practical Foundation for Systems Verification
- what: A Rust verifier for systems code. In its EPR-enabled method (EPR is a restricted logic that the solver can decide), the developer writes the inductive invariant (a fact that holds initially and is preserved by every step) and the tool checks it automatically. The evaluation (Section 6, Figure 9) is at the component level.
- number: 6.1K lines of implementation and 31K lines of proof
- number: IronKV 1,533 exec / 4,509 proof / 1,613 trusted lines; verifies in 18 s on eight cores vs Dafny 201 s
- number: node replication verifies in 9 s vs 228 s
- limits: It applies to the paper’s EPR-enabled method, not to finding arbitrary invariants.
- how much was read: most of it read
- source; notes: S30; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_verus.md; notes: Verus: A Practical Foundation for Systems Verification
- record id: verus-sosp-2024-2024
nl2spec (2023)
- title: nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models
- what: nl2spec uses an LLM to map pieces of English to pieces of a temporal formula. Users can edit the mappings and regenerate. It reports confidence as how much the votes agree.
- number: 36 expert-written requirements; Codex 16/36 initially, Bloom 5/36
- number: interactive correction fixed 15 of 20 failures within three loops, Codex 31/36
- number: four sampled examples raised initial Codex to 21/36, but they stayed in the set
- number: 36 benchmark instances
- limits: An expert assists it. It is not autonomous. Correctness means what the submitting expert meant. The confidence is not a calibrated probability.
- how much was read: most of it read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_intent.md; notes: Natural language to temporal logic and TLA+; notes: papers
- record id: nl2spec-2023
FRET realizability (2022)
- title: Realizability Checking of Requirements in FRET
- what: It checks whether requirements can be implemented, using Lustre and JKind/Kind2. It finds minimal unimplementable sets of requirements with delta debugging, and shows counterexample traces of the environment.
- number: aircraft study: 11 requirements; removing the hover-initialization requirement made a conflicting requirement realizable
- number: infusion pump: 12 requirements rewritten to 26 scoped ones, 8 minimal unrealizable cores
- limits: This is a technical report, not the CAV 2022 version. Results depend on which variables the environment controls.
- how much was read: most of it read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_intent.md
- record id: fret-realizability-2022
SpecFuzzer (2022)
- title: Fuzzing Class Specifications (SpecFuzzer)
- what: Infers likely class invariants for Java. It fuzzes a fixed grammar of assertions, filters candidates with Daikon against Randoop tests, and ranks them by how many mutants they kill.
- number: 65 ground-truth assertions over 43 methods; up to 500 tests and 2,000 candidates per run, 10 runs, 90-minute timeout
- number: 20,277 assertions before selection, 975 after (95.1% reduction)
- number: 34/65 recall (52.3%), precision 65.8%, F1 0.57; GAssert 92.3%/27.6%/0.42; EvoSpex 88.5%/38.4%/0.53
- number: Evaluation on 43 methods and 65 ground-truth assertions; 20,277 assertions before selection, 975 after (95.1% reduction)
- limits: The output is likely invariants consistent with the tests, not proofs. The authors wrote the ground truth. Choosing by mutants can discard valid assertions. The intro’s 75% claim is not supported by the tables.
- how much was read: most of it read
- source; notes: Fuzzing Class Specifications (SpecFuzzer), Molina et al., ICSE 2022; notes: Fuzzing Class Specifications (SpecFuzzer), Molina et al., ICSE 2022
- record id: specfuzzer-2022
DistAlgo runtime checking (2020)
- title: Assurance of Distributed Algorithms and Systems: Runtime Checking of Safety and Liveness
- what: This work checks safety and bounded liveness of runnable DistAlgo programs while they run. It uses executable queries, fault injection and timeouts, and shows them on a polling example.
- number: Fig 1: 24-line polling program; Fig 2: 41-line safety checker
- number: timeouts q-r 0.00001 s, o-o 0.0001 s, total 1 s; raising o-o to 0.01 s gave no L2 timeout in dozens of runs
- number: 10% message loss produced timeout failures
- limits: It sees observed executions only. Bounded liveness turns liveness into safety. The paper gives no fixed denominator and no false-alarm rate.
- how much was read: most of it read
- source; notes: Assurance of Distributed Algorithms and Systems: Runtime Checking of S
- record id: distalgo-runtime-checking-2020
CoqGym (2019)
- title: Learning to Prove Theorems via Interacting with Proof Assistants
- what: CoqGym is a dataset and environment of Coq proofs. Train and test sets are separated by project. A proof succeeds only when the list of remaining goals is empty. Using Admitted (skipping a proof) returns GIVEN_UP.
- number: about 71K proofs from 123 projects
- limits: It completes existing theorems in a fixed environment. It does not score whether a spec is adequate. An agent that can use the filesystem faces a different threat model.
- how much was read: most of it read
- source; notes: CoqGym: project separation and checker-owned proof state
- record id: coqgym-2019
Fonseca study (2017)
- title: An Empirical Study on the Correctness of Formally Verified Distributed Systems
- what: The authors tested IronFleet, Verdi and Chapar. Over eight months they found 16 bugs, all at the edges between the specification, the tools and the unverified code. None were in the verified protocols.
- number: 16 bugs; the PK toolkit automated detection of 13
- number: disabling deduplication via seven implementation lines still passed IronFleet verification
- number: 16 bugs found, none protocol-level; the PK testing toolchain detects 13 of the 16
- number: IronFleet request-deduplication patch: about seven implementation lines changed, still verified
- limits: Finding no protocol bugs does not show that none existed. The source of the PK toolkit was not found.
- how much was read: most of it read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_foundations.md; notes: Specification errors and auditing; notes: Empirical distributed-systems study and PK
- record id: fonseca-study-2017
Who Guards the Guards? Formal Validation of the Arm v8-M Architecture Specification (2017)
- what: The authors build a higher-level account of the security of the Arm v8-M architecture, which processor designers can review. They then formally compare it with the detailed processor spec. They check both forbidden access and intended permitted access.
- number: twelve bugs found (including two security bugs)
- limits: The trusted secondary specification still needs validation by experts.
- how much was read: most of it read
- source; notes: Specification errors and auditing; notes: Appendix B: Concrete systems and theorem scope
- record id: who-guards-the-guards-2017
Trustworthy Specifications of ARM v8-A and v8-M System Level Architecture (2016)
- what: Describes executable Arm architecture specs that are generated alongside the architecture documents. They are validated against separate simulators, processor models and tests.
- limits: Agreement with another artifact helps only after one checks how independently it was built. This is a separate question from logical consistency.
- how much was read: most of it read
- notes: Specification errors and auditing
- record id: trustworthy-specifications-of-arm-2016
Creating an LLM benchmark suite for specification inference
- what: A proposed benchmark with four tasks: add memory-safety specs, strengthen them into specs of full behavior, repair wrong specs, and generate lemmas. Each task runs zero-shot, few-shot, or interactively with verifier feedback. The verifier is Viper.
- limits: A proposal, not a result. It gives no metrics.
- how much was read: most of it read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_google.md
- record id: creating-an-llm-benchmark
Aria (2026)
- title: Harnessing Code Agents for Automatic Software Verification
- what: Claude Code (Opus 4.7) proves one Coq lemma at a time inside a sandbox, and the Coq kernel checks each proof. There is no search over proof steps and no retrieval of related facts. The lemma statements are given. The agent writes the proofs.
- number: Proves all 4,257 lemmas of four Iris core modules and 217 lemmas for Rust standard-library verification
- number: 79.2% of Iris core lemmas proved on the first try; mean 0.51 retries; maximum 28
- number: Total model time 379.7 hours; mean 321.1 s per lemma
- number: Open model Kimi K2.6: 55% first-try vs 72.5% for Opus 4.7, about seven times as long
- limits: The statements were given, not written. Iris is public and probably in the training data. The paper argues that its proofs differ from the upstream ones. That does not test for contamination (the notes’ caveat).
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_agents.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_leads.md
- record id: aria-2026
AutoCLRS completeness-test artifact (2026)
- what: This artifact applies the intent-formalization completeness test to textbook algorithms written in F*/Pulse. Only the abstract interface, not the code body, should establish the expected result. The spec may allow multiple valid outputs.
- limits: The README lists unresolved build and path issues. The notes did not reproduce the reported outcomes.
- how much was read: parts read
- source; notes: User-intent formalization in verification-aware languages
- record id: autoclrs-completeness-test-artifact-2026
Beyond Compilation (2026)
- what: A study of turning math into Lean statements automatically. It shows that Lean accepting a statement does not mean the statement says what the user meant.
- number: Tool-augmented GPT-5.2 agent compiles 87.2% of statements but is faithful on 57.7% (29.5 point gap)
- limits: About mathematics, not systems.
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_eval.md
- record id: beyond-compilation-2026
ClarifyCodeBench (2026)
- what: Measures how well code models ask for clarification of requirements, using the metrics TKQR and ORA.
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_eval.md
- record id: clarifycodebench-2026
COINS (2026)
- title: How Powerful Are LLMs in Generating Formal Program Specifications? (COINS)
- what: It instantiates a spec on trusted tests to produce concrete proof obligations in Rocq. These serve as an oracle (a reference check) for whether the spec is correct.
- number: All 164 HumanEval ground-truth specs hand-written over several person-weeks
- number: Top 28.05% (Gemini 3 Pro Preview) down to 1.22% (DeepSeek-V3.1)
- number: 164 HumanEval problems
- limits: Failing to find a proof that a test is accepted is weaker evidence than proving that it is rejected. The LLM judge can skip the formal proof. It does not cover distributed liveness.
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_eval.md; notes: How Powerful Are LLMs in Generating Formal Program Specifications?
- record id: coins-2026
CryptoProver (2026)
- title: An AI Approach to Verified Production Cryptographic Libraries
- what: Agents write cross-file internal specs and proofs for a Rust crypto library. A human supplies a fixed external claim. Four things are frozen: the executable Rust, the public API contracts, the trusted library and the accounting of proof holes. The whole crate is then replayed to check it.
- limits: The result does not cover whether the contracts are adequate, cryptographic security or constant time. The notes infer that freezing all intermediate contracts would remove part of the intended task.
- how much was read: parts read
- source; notes: CryptoProver: preserve the public claim and audit the generated interi
- record id: cryptoprover-2026
LeetProof (2026)
- title: LeetProof: Certified Program Synthesis with a Multi-modal Verifier
- what: LeetProof synthesizes programs together with proofs that they are correct. The notes audit how it checks its specs. The checks are generated examples, an LLM judge, randomized checks of preconditions and postconditions, mutations that produce incorrect outputs, a Lean proof of equivalence to VERINA, and manual judgment.
- limits: The earlier note found that development and evaluation statistics were pooled. It also found that unresolved specs were classified without blinding, and that the synthesis subjects had no independent labels.
- how much was read: parts read
- source; notes: LeetProof: examples and equivalence provide complementary intent evide
- record id: leetproof-2026-2
LiveFMBench (2026)
- title: LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation
- what: 630 C programs annotated with ACSL (360 collected in 2025 to avoid training leaks), verified with Frama-C/WP. Models generate loop invariants and assertions. A faithfulness check requires that the ASTs are equal and that every original assertion appears in the output.
- number: true accuracy drops about 20% after excluding unfaithful cases
- number: pass@5 doubles pass@1; pass@32 triples it
- number: incorrect loop invariants are the dominant error type
- number: After removing unfaithful behaviors true accuracy drops about 20%
- limits: One notes file says the full claims await deeper reading. Another read the faithfulness section.
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_shortlist.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_scholar.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/verified_primary_notes_20261012.md
- record id: livefmbench-2026
Munkres’ General Topology Autoformalized in Isabelle/HOL (2026)
- what: LLM coding agents (ChatGPT 5.2, then Claude Opus 4.6) wrote an Isabelle/HOL formalization of all 39 sections of Munkres’ Topology. They used a workflow that writes sorry first, plus sledgehammer.
- number: over 85,000 lines, 806 formal results, zero sorry, 24 active days
- number: 2.66 M output tokens, 17.2 billion cache-read tokens, estimated API cost $8, 895; e f f ec t i v ecos t ab o u t$ 160 on a 100,000
- number: 917 consensus claims, 34% wrong (Fig. 2)
- limits: The review notes read about 25%. It is not about proofs or specs.
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_google.md
- record id: veriharness-2026
VeruSyn (2026)
- title: Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set
- what: VeruSyn grows a seed corpus into 6.9 million verified Rust programs with contracts and proofs, plus 4,557 reasoning trajectories. It fine-tunes a model on them.
- number: 560 held-out system proof tasks (849 minus 289 used for trajectory training)
- number: fine-tuned Qwen2.5-Coder-32B 49% with debugging vs Sonnet 4.5 54%
- number: estimated $0.61 v s$ 39.24 per task (Table 3)
- number: VerusBench headline 83% vs 76% with debugging
- limits: The prices are specific to this study and do not predict current costs. The existing contracts and code remain the target. No coding agent is evaluated.
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_agents.md
- record id: verusyn-2026
AlphaVerus (2025)
- title: AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement
- what: It translates Dafny programs that already have specs into Verus. It uses verified examples to improve later generation of code and proof. A tree search repairs several candidates. Critics reject candidates that change the contracts or exploit loopholes in the verifier.
- number: 32.9% HumanEval and 65.7% MBPP at pass@256 for the full open-model pipeline
- number: training uses 562 filtered DafnyBench programs, about 45% translated successfully (original 782 files)
- number: MBPP generation evaluation has 78 tasks
- number: proof annotation task: 75.7% (Table 2)
- limits: The reported rates are pass@256 (success within 256 tries), not single attempts. The task is not writing a spec from vague prose.
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_agents.md; notes: Recent agent termination evidence, with narrow scope; notes: P21. AlphaVerus: Bootstrapping Formally Verified Code Generation throu
- record id: alphaverus-2025
CapybaraKV (2025)
- title: CapybaraKV (verified-storage)
- what: CapybaraKV is a verified key-value store written in Verus. An earlier version appears in the OSDI 2025 paper PoWER Never Corrupts. It comes with a line-counting script that computes the ratio of proof lines to code lines.
- limits: The notes read only the README.
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_systems.md
- record id: capybarakv-2025
Case Study on LLMs in Verification with Proof Assistants (hs-to-coq, Verdi) (2025)
- what: Tests one-shot LLM proof generation (before agents existed) on Verdi and hs-to-coq. Verdi is a distributed-systems framework that contains a verified Raft.
- number: Verdi: 579 theorems, best setting 30.6% (o4-mini with in-file context)
- number: hs-to-coq up to 51.9%
- limits: One-shot baseline only.
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_agents.md
- record id: case-study-on-llms-2025
CCF smart casual verification (2025)
- title: Smart Casual Verification of the Confidential Consortium Framework (CCF)
- what: It ties a TLA+ spec to CCF’s C++ implementation. In CI, it checks that traces of the implementation are allowed by the spec. It uses model checking, not proof.
- number: Six subtle bugs found, five concerning safety and one liveness
- number: 400 LoC Trace spec; 88 commits to it and 107 changes to the consensus spec; implementation 63 kLoC C++
- number: six subtle bugs found
- number: 63 kLoC in C++ (§2)
- limits: It guarantees nothing about all runs. It only covers traces from CI tests and simulation.
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_humans.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_model_to_code.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_systems.md
- record id: ccf-smart-casual-verification-2025
Dafny students with ChatGPT (Carreira et al.) (2025)
- what: A study of Dafny students using ChatGPT.
- limits: Gains depended on how good the prompts were.
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_eval.md
- record id: dafny-students-with-chatgpt-2025
FormalBench (2025)
- title: Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference
- what: FormalBench measures how well models generate JML specs. It includes a flip rate: how often the result changes when the program is rewritten in a way that keeps its meaning.
- number: About 10% verification success on JML spec generation
- number: 700 Java reference programs, 6,219 transformed variants
- limits: The program rewrites do not measure contamination from pretraining. Deriving the intent from existing code can preserve a defect in that code.
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_eval.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_intent.md; notes: FormalBench and SpecEval: mutation strength and surface robustness
- record id: formalbench-2025
ImpossibleBench (2025)
- what: ImpossibleBench builds tasks where any pass implies a shortcut that violates the spec. It uses them to measure cheating.
- number: GPT-5 cheats on 76% of Oneoff-SWEbench tasks; a prompt change cuts one variant from 92% to 1%
- number: Monitors catch 86-89% of cheating on LiveCodeBench but 42-65% on SWE-bench
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_eval.md
- record id: impossiblebench-2025
Scimitar (2025)
- title: Interpretable Safety Verification of Distributed Protocols by Inductive Proof Decomposition
- what: Scimitar breaks a proof into a graph of lemmas and transitions. This exposes where guidance is needed. The target is Raft LogMatching, on a modified model of about 600 TLA+ lines.
- number: 21 hours, 33 total lemma nodes
- number: grammar has 173 predicates
- number: 33 lemma nodes
- number: 173 grammar predicates
- limits: The draft the notes inspected has a different title from earlier and later records, and a placeholder conference header. One property of an edited model is not a complete verification of Raft.
- how much was read: parts read
- source; notes: papers inspected; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_humans.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_systems.md
- record id: scimitar-2025
SpecEval (2025)
- title: SpecEval: Evaluating Code Comprehension in Large Language Models via Program Specifications
- what: It judges LLMs on JML tasks: judge correctness, pick the strongest of four specs, fill in an expression, and generate contracts and invariants. It scores precision and recall against reference properties, using implication in both directions. It also applies counterfactual perturbations (small changes that should change the answer).
- number: 204 Java programs
- limits: Precision alone rewards vacuous specs (specs that say nothing). Recall depends on how adequate the gold specs are. It has no evaluation of temporal liveness.
- how much was read: parts read
- source; notes: FormalBench and SpecEval: mutation strength and surface robustness
- record id: speceval-2025
Beyond Code Generation: Assessing Code LLM Maturity with Postconditions (2024)
- what: It extends the EvalPlus benchmark with several kinds of postcondition (what must hold after a function runs): boundary, equality, container, Boolean and string. It checks that the assertions are correct and which buggy programs they catch.
- limits: It evaluates algorithms with a finite set of tests. It does not cover proofs or progress in distributed systems.
- how much was read: parts read
- source; notes: Natural-language postconditions and known faulty implementations
- record id: beyond-code-generation-assessing-2024
Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal Logic (2024)
- what: The study examines how people read and write linear temporal logic, across five deployments.
- number: Writing a formula wrong: 21.11-25.00% (alpha), 33.68% (LTL-aware audience), 66.13% and 63.33% (student course)
- number: Trace matching wrong: 1.85% to 27.24%
- limits: The notes are unsure about the authors after the first. Percentages across different instruments cannot be compared.
- how much was read: parts read
- notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_intent.md
- record id: misconceptions-in-finite-trace-2024
SandTable (2024)
- title: SandTable: Scalable Distributed System Model Checking with Specification-Level State Exploration
- what: It model-checks a TLA+ spec quickly, then replays the bug traces in the code. A conformance checker replays model traces to find places where the spec and code differ.
- number: 23 bugs, 18 new, 17 confirmed, 13 fixed
- number: Half a person day to a few person days to fix modeling errors; two person weeks adapting ZooKeeper specs
- number: 114x-2989x faster state exploration
- number: abstract: 18 new bugs, 17 confirmed, 13 fixed (the note’s sentence adds ‘out of 23 total’ garbled)
- limits: It cannot guarantee that no differences remain between the spec and the implementation.
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_model_to_code.md; notes: P10. SandTable: Scalable Distributed System Model Checking with Specif
- record id: sandtable-2024
TLA+ trace validation (2024)
- title: Validating Traces of Distributed Programs Against TLA+ Specifications
- what: Instrumented Java executions give partial updates to the abstract state. TLC searches for a path compatible with them and infers missing values nondeterministically.
- limits: Checks only that some compatible behavior exists (S∩T≠∅). It does not check refinement. The more logged data is missing, the weaker the verdict.
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_agents.md; notes: P08. Validating Traces of Distributed Programs Against TLA+ Specificat; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_b/agent_evaluation_procedure.md
- record id: tla-trace-validation-2024
Mocket (2023)
- title: Model Checking Guided Testing for Distributed Systems (Mocket)
- what: Mocket finds inconsistencies between a TLA+ spec and a distributed system’s implementation. It annotates Java state and actions and exports TLC’s state graph. It generates paths through the graph. It then drives implementation runs with instrumentation and a testing server.
- limits: The notes could not find the publication’s authors, venue or year. Coverage depends on the paths, the action mapping, the instrumentation and the configured faults. The notes found no universal theorem about the implementation or progress.
- how much was read: parts read
- source; notes: Mocket; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_model_to_code.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_b/openalex_leads_20261012.md
- record id: mocket-2023
FoundationDB (2021)
- title: FoundationDB: A Distributed Unbundled Transactional Key Value Store
- what: Runs the real database actors in a deterministic simulated environment. The simulation replaces the network, disk, clocks and randomness. This gives reproducible schedules and recovery tests after failures stop.
- limits: Simulation needs assertions or an oracle to decide what is correct. Its coverage is not a refinement proof or a proof of progress at unbounded size.
- how much was read: parts read
- source; notes: P23. FoundationDB: A Distributed Unbundled Transactional Key Value Sto
- record id: foundationdb-2021
LISA / PISA (2021)
- title: LISA: Language Models of ISAbelle Proofs (PISA)
- what: It extracts Isabelle theorem data and trains proof-search models. PISA is the interface for interacting with Isabelle.
- number: 183K theorem/lemma statements, 2.16M steps; random 95/1/4 split
- number: 33.2% success on 4,000 theorems under 120 s / 100 queries
- number: universal test set of 3000 theorems
- limits: Random proof-level splits can leave related lemmas on both sides of a split. There is no exhaustive final audit of what is trusted. It evaluates given theorems, not formalization.
- how much was read: parts read
- source; notes: PISA: distinguish the interface from a particular extracted split
- record id: lisa-pisa-2021
ShardStore (2021)
- title: Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3
- what: Executable reference models and checks for the S3 ShardStore storage node.
- number: Reference models about 1% of implementation code
- number: Checks and harnesses 12% of the code base
- number: Prevented 16 issues from reaching production
- number: 18% of reference model and harness code written by the engineering team
- limits: Passing the checks does not mean the code is correct.
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_humans.md; notes: papers; notes: Using Lightweight Formal Methods to Validate a Key-Value Storage Node
- record id: shardstore-2021
eXtreme Modelling (2020)
- title: eXtreme Modelling in Practice
- what: MongoDB compared two ways to link a model to code. One is model-based trace checking (MBTC), which checks whether logged runs fit the model. The other is model-based test-case generation (MBTCG). Trace checking of replication was impractical. For Realm Sync’s operational-transformation rules, a Go generator turned TLC states into C++ tests.
- number: Realm Sync table (§5.2): 795 TLA+ lines, 755 Go lines, 4 weeks total effort
- number: Abandoned trace checking after 10 weeks
- number: 4913 generated tests reached 100% branch coverage vs 21% handwritten and 92% AFL fuzzer
- limits: Trace checking of replication struggled with the level of abstraction, concurrency, incomplete observations, and keeping code and model in sync. The generated tests cover local merge behavior, not the whole distributed product.
- how much was read: parts read
- source; notes: P04. eXtreme Modelling in Practice; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_humans.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_model_to_code.md
- record id: extreme-modelling-2020
Apalache (2019)
- title: Apalache: temporal properties tutorial, feature table and TLA+ model checking made symbolic
- what: Apalache is a model checker for TLA+ that works on symbols instead of listing states, using an SMT solver. It checks state, action and trace invariants, inductive invariants (a property that holds at the start and is preserved by every step) and temporal properties.
- limits: Apalache parses ASSUME but does not pass it to the solver. It does not use THEOREM. Its bounded checks do not prove properties for unbounded runs. The authors did not read the original paper.
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_distributed.md; notes: tools; notes: Model checking: what a successful run means
- record id: apalache-2019
QED at Large (2019)
- title: QED at Large: A Survey of Engineering of Formally Verified Software
- what: A survey of proof engineering (building and maintaining machine-checked proofs).
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_humans.md; notes: S12
- record id: qed-at-large-2019
Proof cost indicator (2015)
- title: Empirical Study Towards a Leading Indicator for Cost of Formal Software Verification
- what: It studies how the size of the formal statement relates to the size of the proof in Isabelle developments.
- limits: The notes found no predictive model.
- how much was read: parts read
- source; notes: S37
- record id: proof-cost-indicator-2015
Proof productivity (2014)
- title: Productivity for Proof Engineering
- what: Fits proof effort to proof size.
- number: Total Effort = 9.98 + 3.35*Final Size (R^2 = 0.914; person-weeks and kilo-lines of proof)
- limits: Proof lines are a limited measure. The fit applies to one particular population of projects. It is not a universal conversion.
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_humans.md; notes: S36
- record id: proof-productivity-2014
seL4 process study (2012)
- title: Large-Scale Formal Verification in Practice: A Process Perspective
- what: A study of the process of verifying seL4.
- number: Design verification consumed roughly 60-70% of time and effort
- number: Less than 14 person-years for kernel design, development and verification
- number: Integrity and authority confinement took 10 person months
- number: Maintenance about one full-time person
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_humans.md; notes: S35
- record id: sel4-process-study-2012
Towards a Notion of Unsatisfiable and Unrealizable Cores for LTL (2012)
- what: The paper defines cores. A core isolates the part of a requirement set that is unsatisfiable or unrealizable (no implementation could meet it). The paper defines cores at several granularities, from whole requirements to proof structures. It also discusses vacuity (a requirement that passes for no real reason).
- number: lift example: 6 of 49 conjuncts isolate an inconsistency (§8.1)
- limits: A core explains a failure, but not necessarily every failure. It does not tell which restrictions on the environment the customer intended. The normal-form proofs were not checked.
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_intent.md
- record id: towards-a-notion-of-2012
Aleph Prover
- what: A prover reported to solve all of PutnamBench.
- number: Solved all 672/672 problems on PutnamBench at about 30 per high/medium/low bug
- limits: The authors say the quality of the generated properties is the main limit.
- how much was read: only abstract or first pages read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_intent.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/verified_primary_notes_20261012.md; notes: specification-anchored auditing
- record id: speca-2026
SpecLoop (2026)
- title: SpecLoop: An Agentic RTL-to-Specification Framework with Formal Verification Feedback Loop
- what: Candidate specs are used to rebuild the RTL (hardware design code). Formal equivalence checking feeds counterexamples back to refine the spec. It improves over baselines that use only an LLM.
- limits: Results depend on the RTL reconstructor and the equivalence checker. Bounded resource limits can block feedback. It reverse-engineers a spec from a design, and does not recover an unconstrained request.
- how much was read: only abstract or first pages read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/verified_primary_notes_20261012.md; notes: SpecLoop; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_b/agent_evaluation_procedure.md
- record id: specloop-2026
VCoT-Bench (2026)
- what: VCoT-Bench has 1,988 tasks that reconstruct Verus proof steps.
- number: 1,988 tasks
- how much was read: only abstract or first pages read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_agents.md
- record id: vcot-bench-2026
How much Specification is Enough? Mutation Analysis for Software Contracts (2021)
- what: This work mutates implementations and then uses deductive verification (KeY) to judge how incomplete JML contracts are.
- limits: The notes read only the abstract and report no numbers. They infer that the result depends on which mutants were chosen.
- how much was read: only abstract or first pages read
- source; notes: Testing strength, mutations, and vacuity
- record id: how-much-specification-is-2021
A Theory of Mutations with Applications to Vacuity, Coverage, and Fault Tolerance (2008)
- what: Treats vacuity (a spec that holds for no useful reason) and coverage (how much of the system the spec checks) as the same thing: small deliberate changes, called mutations, made to either the specification or the implementation.
- limits: The notes read only the abstract. The applications are in hardware, which by themselves do not cover fault histories of distributed systems. That last point is the notes’ inference.
- how much was read: only abstract or first pages read
- source; notes: Testing strength, mutations, and vacuity
- record id: a-theory-of-mutations-2008
Coverage Metrics for Formal Verification (2006)
- what: It adapts several coverage notions from simulation to formal verification. It links successful checks, vacuity (a spec that holds trivially, so it says nothing) and incomplete specs.
- limits: The notes’ author read only the abstract and introduction.
- how much was read: only abstract or first pages read
- source; notes: Coverage Metrics for Formal Verification
- record id: coverage-metrics-for-formal-2006
Sanity Checks in Formal Verification (2006)
- what: Surveys vacuity checks (does the spec actually matter?) and coverage checks (does the system part matter?), run after model checking succeeds.
- limits: The notes read the abstract only.
- how much was read: only abstract or first pages read
- source; notes: Testing strength, mutations, and vacuity
- record id: sanity-checks-in-formal-2006
A Practical Approach to Coverage in Model Checking (2001)
- what: It measures how well a spec covers a model. Change one part of the model and see whether the spec still holds. If it does, that part is not covered. The paper gives algorithms for specs written in LTL (a logic for statements about sequences of events).
- limits: The notes’ author read only the abstract and introduction. The result depends on which changes and which properties you pick.
- how much was read: only abstract or first pages read
- source; notes: A Practical Approach to Coverage in Model Checking
- record id: a-practical-approach-to-2001
Vacuity Detection in Temporal Model Checking (1999)
- what: Checks whether every part of a temporal property actually affects whether it holds. Example: a property saying a request is eventually answered passes trivially if no request can ever occur.
- limits: A witness showing the property is not vacuous does not prove that all intended clauses were specified. The notes had only the abstract and introduction (the extraction was damaged).
- how much was read: only abstract or first pages read
- source; notes: Testing strength, mutations, and vacuity; notes: Vacuity Detection in Temporal Model Checking
- record id: vacuity-detection-in-temporal-1999
Claude C compiler (2026)
- title: Building a C compiler with a team of parallel Claudes
- what: Opus 4.6 agents run in a restart loop and coordinate through task-file locks and git. They build a C compiler in Rust that compiles Linux 6.9 on three architectures.
- number: 16 agents; nearly 2,000 Claude Code sessions; about $20,000; 100,000 lines of Rust
- limits: There is no proof that the compiler preserves program meaning. It was checked only by compiler test suites, builds, comparison with a reference, and CI. Failures included regressions, noisy context, duplicated effort and weak test feedback.
- how much was read: reading depth not recorded
- source; notes: Anthropic compiler: large agent-built code, assessed through tests
- record id: claude-c-compiler-2026
Galois benchmarks post (2026)
- title: Formal Verification Benchmarks Are the Key to Ironclad Software Infrastructure
- what: Introduces Metron and Praxis. Argues for benchmarks built from production tasks, for signals about intermediate failure and recovery, and for held-out evaluation.
- limits: The article releases no model, rate or result.
- how much was read: reading depth not recorded
- source; notes: Galois vision and benchmark initiatives: proposals, not completed kern
- record id: galois-benchmarks-post-2026
Galois eFMRL (2026)
- title: Advancing Cryptographic Verification with AI: Reflections on my Hiring our Heroes Fellowship at Galois
- what: It fine-tunes small local models (Gemma 4 26B-A4B-it) to write and repair Cryptol, a language for cryptography specifications. The reward comes from whether the compiler accepts the output.
- number: Base 44% overall; prompt-only 65-66%; trained 78% and 86%; broken-code repair 97% vs 71%
- number: 600 steps (about 50 hours)
- limits: Scores measure only whether the compiler accepts the spec. They do not show whether it encodes the intended behavior.
- how much was read: reading depth not recorded
- source; notes: Galois eFMRL: major gains in a rare specification language, measured b
- record id: galois-efmrl-2026
Scimitar (2026)
- title: Interactive Safety Verification of Distributed Protocols by Inductive Proof Decomposition
- what: It shows a human verifier small induction failures, each tied to one lemma and one action, while hiding irrelevant variables. This builds an inductive proof graph step by step. TLAPS checks the final invariants.
- number: Table 1: SimpleConsensus 111/18 lines, 8 lemmas; TwoPhase 192/140, 16; AbstractRaft 220/138, 10; Bakery 283/116, 27; AsyncRaft 638/920, 39
- number: AsyncRaft invariant development took approximately 3 human weeks
- limits: The cited fixed artifact (nfm26-artifact) was unavailable. The live repository has many more configurations than the five evaluated.
- how much was read: reading depth not recorded
- source; notes: Scimitar: distinguish the final interactive paper from an older automa; notes: Full live Scimitar configuration inventory (not an evaluated success l
- record id: scimitar-2026
SysMoBench blog (2026)
- title: Can LLMs model real-world systems in TLA+?
- what: The post explains concrete modeling mistakes. Models copy textbook Raft instead of the implementation’s own voting. Or they merge atomic guards and erase ZooKeeper’s higher-epoch transition.
- limits: Do not mix its newer aggregate results with the paper’s table.
- how much was read: reading depth not recorded
- source; notes: SysMoBench: real code exposes failures hidden by puzzle benchmarks
- record id: sysmobench-blog-2026
Harmonic Aristotle VERINA (2025)
- title: Aristotle Learns to Code, Achieving New State-of-the-Art of 96.8% on Code Verification Benchmark
- what: Harmonic’s Aristotle API proves or refutes pairs of Lean code and specification from the VERINA benchmark.
- number: 189 pairs: 160 proved correct, 23 shown false, 96.8% resolved; proof-only 160/189 = 84.7% (notes’ arithmetic)
- limits: Reports no distributed or progress test, no compute budget, no retries and no audited script.
- how much was read: reading depth not recorded
- source; notes: Harmonic Aristotle: 96.8% means proof-or-refutation resolution
- record id: harmonic-aristotle-verina-2025
Laurel (2025)
- title: Laurel: Unblocking Automated Verification with Large Language Models
- what: GPT-4o restores one missing Dafny assertion. It uses locations reported by the verifier, placeholders, and examples from the same project.
- number: 145 tasks from Cedar, Dafny libraries and a VM project; 82 successes (56.6%, notes’ arithmetic)
- limits: The surrounding proof and specs are supplied. No distributed progress.
- how much was read: reading depth not recorded
- source; notes: Dafny, C verification, and the specification-intent gap
- record id: laurel-2025
TLAi+ Challenge (2025)
- title: 2025 TLAi+ Challenge
- what: Challenge winners. First prize: Cheng, Xu, Huang (early Specula workflow). Second: Andrew Helwer (constrained TLA+ token generation with LlamaCpp/GBNF and Guidance). Third: Gregory Terzian (staged refinement from TLA+ toward multithreaded Rust).
- limits: The challenge solicited TLAPS work, but that is not evidence that any submission finished one. Grammar constraints give correct syntax, not faithful meaning.
- how much was read: reading depth not recorded
- source; notes: TLAiBench and the Foundation challenge: useful harnesses, limited meas
- record id: tlai-challenge-2025
FVEL (2024)
- title: FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving
- what: FVEL shows Isabelle verification states and checked feedback to fine-tuned Llama-3-8B and Mistral-7B proof generators. It trains on a seL4 corpus.
- number: 29,125 lemmas in the seL4 corpus
- number: Llama-3 proves 88 of 1077 ordinary test lemmas and 64 of 852 hard lemmas (8.17% and 7.51%, notes’ arithmetic)
- limits: Humans still add the imports and supply the statements as inputs.
- how much was read: reading depth not recorded
- source; notes: seL4: from whole-proof guessing to proof-state search
- record id: fvel-2024
primal-dual Houdini (2022)
- title: Induction Duality: Primal-Dual Search for Invariants
- what: The paper pairs Houdini with a dual search over states. Houdini drops candidate invariants until the remaining ones hold. The method also finds counterexamples for broken protocols.
- number: Table 2: 20 benchmarks (10 safe, 10 unsafe)
- number: Fixed VM artifact about 5.45 GB
- number: Pages 1-29
- limits: The publisher PDF returned HTTP 403, so the review notes read the artifact instructions and source instead.
- how much was read: reading depth not recorded
- source; notes: Primal-dual Houdini: full fixed 20-task evaluation
- record id: primal-dual-houdini-2022
Testing LLM-Generated Distributed Protocol Code (2026)
- what: A framework evaluates LLM-written Two-Phase Commit, Ring Election and Raft. It uses a simulator that injects message loss, delay and duplication. LLMs do well on simple protocols and code completion, struggle on complex consensus, and debug inconsistently.
- limits: Based on the schedule abstract, through a fetch-tool summary. The review notes have no full text and no numbers.
- how much was read: not read; title and metadata only
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_google.md
- record id: testing-llm-generated-distributed-2026
VeriBench (2026)
- title: VeriBench: An End-to-End Formal Verification Benchmark for AI Coding Agents
- what: A launch-draft blog for paired Python/Lean verification tasks, scored against human reference theorem statements. The requested paper titles (VeriBench, Veribench-FTP) could not be found as papers.
- number: gold theorem sorry rate about 0.57 despite claim that all close without sorry
- limits: There is no paper or artifact. The repositories returned 404. Treat it as a lead.
- how much was read: not read; title and metadata only
- source; notes: VeriBench and Veribench-FTP: exact requested publication not recovered
- record id: veribench-2026
A Specification Linter for Gobra (2025)
- what: A linter for specs in the Gobra verifier, aimed at the problem that verified programs only match their intended specs if the specs are right.
- limits: Seen only as a Google Scholar snippet. Not read.
- how much was read: not read; title and metadata only
- notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_gscholar.md
- record id: a-specification-linter-for-2025
Cazamariposas (2025)
- title: Cazamariposas: Automated instability debugging in SMT-based program verification
- what: The paper automates debugging of verification instability, where proofs pass or fail unpredictably. It targets SMT-based verifiers (verifiers that use a solver) such as Dafny and F*.
- limits: The review notes saw only a Google Scholar title and snippet and did not read the paper.
- how much was read: not read; title and metadata only
- notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_gscholar.md
- record id: cazamariposas-2025
Model Checking Guided Incremental Testing for Distributed Systems (2025)
- what: Listed as an unread search lead from OpenAlex. The notes give only its title, year and DOI.
- limits: Not read. Claims are unverified.
- how much was read: not read; title and metadata only
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_b/openalex_leads_20261012.md
- record id: model-checking-guided-incremental-2025
HumanEvalComm (2024)
- what: A benchmark with communication metrics that measure whether models ask clarifying questions.
- limits: The review notes saw it only as a search snippet.
- how much was read: not read; title and metadata only
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_eval.md
- record id: humanevalcomm-2024
Effective Concurrency Testing for Distributed Systems (2020)
- what: Listed as an unread search lead from OpenAlex. The notes give only its title, year and DOI.
- limits: Not read. Claims are unverified.
- how much was read: not read; title and metadata only
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_b/openalex_leads_20261012.md
- record id: effective-concurrency-testing-for-2020
Trace aware random testing for distributed systems (2019)
- what: A search lead from OpenAlex that the review notes have not read. The notes give only its title, year and DOI.
- limits: Not read, so its claims are unverified.
- how much was read: not read; title and metadata only
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_b/openalex_leads_20261012.md
- record id: trace-aware-random-testing-2019
Woodcock survey (2009)
- title: Formal methods: Practice and experience
- what: The survey covers industrial use of formal methods across specification, design and verification.
- limits: The full text was unavailable. The review notes take no claim about cost or success rate from it.
- how much was read: not read; title and metadata only
- source; notes: S28
- record id: woodcock-survey-2009
An Experiment in Formal Verification with Claude
- what: Claude Opus 4.6/4.7 wrote the Lean 4 statements and most of the proofs for the soundness and zero-knowledge theorems of Succinct’s VEIL compiler. A CLAUDE.md file with simple rules guided it. Humans revised the statements and checked the Lean against the English descriptions.
- number: human revised statements over dozens of iterations
- number: human time roughly 1-2x the time of writing the paper versus about 10x typical
- number: a full protocol can mean auditing about 1,000 lines of Lean
- limits: This is a blog post, not a peer-reviewed paper. The notes rest on a tool summary, not on the page text. It is not about distributed systems. Claude sometimes silently swapped ‘for all, there exists’ for ‘there exists, for all’ in zero-knowledge claims. It also defined malicious provers that were too weak.
- how much was read: not read; title and metadata only
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_google.md
- record id: an-experiment-in-formal
AutoReal
- what: A 7B model fine-tuned for theorem proving; a model, not an agent.
- number: 51.67% on 660 seL4 theorems
- number: 53.88% on 451 AFP security theorems
- limits: Known only from a search summary. Not opened.
- how much was read: not read; title and metadata only
- notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_leads.md
- record id: autoreal

Last edited: 2026-10-13

Keyboard shortcuts

Steven Hé (Sīchàng)

🤖 database, how to judge specifications, proofs, and agents