🤖 database, LLM and agent systems that write specifications or proofs

(authored by agents unless marked 🧑)

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

AeroReq2LTL (2026)
- title: Automated LTL Specification Generation from Industrial Aerospace Requirements
- what: Before translating requirements to LTL (a logic for statements about sequences of events), it adds a domain data dictionary and controlled requirement templates. It compares the results to formalizations written by experts for aerospace requirements.
- number: 85% precision and 88% recall
- limits: It covers one industrial domain, and its authors overlap with those of Req2LTL. It is not shown to work for the intent of distributed services.
- how much was read: most of it read
- source; notes: Natural language to temporal logic and TLA+
- record id: aeroreq2ltl-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 1,380 retrospective API price
- number: Cat: 106.8M tokens, 64 h, 17 prompts
- number: Clipper 26/29 functions after 81h44m; Nouns Auction 18/20 after 94h28m with certificate check timing out
- limits: It does not show transaction availability, bounded gas, eventual completion or soundness of the supplied policy. The refinement relation permits vacuity through gas exhaustion (running out of gas makes a claim hold trivially). The trusted base includes the EVM formalization, imported Lean axioms and native_decide. A human supplies the high-level spec.
- how much was read: most of it read
- source; notes: Foundational Refinement Proofs for Deployed Bytecode, at the Price of ; notes: Foundational Refinement Proofs for Deployed Bytecode, at the Price of
- record id: eqivm-2026
Expecto (2026)
- title: Expecto: Extracting Formal Specifications from Natural Language Description for Trustworthy Oracles
- what: Builds specs top-down from informal programming requirements, in a Dafny-based language with recursive helper definitions. It can check examples before every helper is defined, and it yields executable oracles (programs that judge whether an output is correct).
- number: HumanEval+ 164 tasks; APPS 127 problems; Defects4J 501 methods from 336 bugs
- number: soundness threshold: reject over half of generated wrong output pairs (X=50), five shuffled alternatives per input
- limits: Soundness is shown by experiment against a threshold, not proved. Shuffled outputs may be accidentally correct. Cases where the solver timed out are excluded. Criteria differ across datasets. It is not a theorem that all wrong outputs are rejected.
- how much was read: most of it read
- source; notes: Generated contracts and independent evaluation; notes: Expecto
- record id: expecto-2026
Federated FV (2026)
- title: Federated Formal Verification: Cross-Backend Citation, Cross-Axis Convergence, and AI-Orchestrated Proof Dispatch for Production Systems
- what: This work sends the open TLA+ proof obligations of a production Raft system to Coq, Lean, Why3, Apalache, Z3 and CBMC. Claude Code specialists handle each backend. CI rechecks the proofs, and the system generates Java runtime assertions.
- number: 17 active hours, 263 commits, 26-axiom census closed
- number: about twenty specialist agents in four waves of 3/6/7/4; practical concurrency 6-7
- number: proof tree over 11,000 lines, 18 apex obligations
- number: Coq 8/8 passes, median 34.4 s; Apalache 0/3; TLC 0/5; PRISM 1/13
- limits: A human wrote the claim that the backends are equivalent. There is no artifact URL. The paper gives no prompts, no cost, and no breakdown of human effort. The Java assertions check test states only, not refinement. The speedup compares different protocols. Apalache refuted a property that Coq cited, at bound six.
- how much was read: most of it read
- source; notes: Federated Formal Verification: Cross-Backend Citation, Cross-Axis Conv; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_agents.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_liveness.md
- record id: federated-fv-2026
Feedback & Synthesis in LLM-Assisted Termination Proofs (2026)
- what: LLMs propose decreasing measures (quantities that shrink at each step, proving termination) for ACL2s functions. ACL2s checks them and returns errors and counterexamples. It splits failures into loops (termination cores) and combines the subproofs.
- number: 42 base functions
- number: 786 hours on an H200 GPU
- number: thirty-minute limit per problem
- number: gpt-oss with feedback solved 70% of course and 93% of competition problems vs built-in ACL2s 65% and 63%
- limits: It covers termination of functional code, not progress of distributed systems. The 39% compares the integrated search with the best LLM alone. The corpus is small.
- how much was read: most of it read
- source; notes: Feedback & Synthesis in LLM-Assisted Termination Proofs
- record id: feedback-synthesis-in-llm-2026
Fewer Assumptions by Design: A Reusable Skill for LLM-Assisted Verus Verification (2026)
- what: Verifies an index-based doubly linked list in Verus by hand, then with a Claude agent. It then packages a ‘skill’ (SKILL.md, templates, and a list of pitfalls) that tells the agent how to work. The goal is to use as few assume statements (unproven hypotheses) and axiomatic lemmas as possible.
- number: by hand: 16 assumes (Exp 1), 11 assumes (Exp 2)
- number: with Claude: assume count dropped from 75 to 11; final state 45 verified, 0 errors, 11 assumes
- number: agent cost: a couple of hours of reasoning plus manual prompting by the user
- number: Claude-assisted run’s assume count fell from 75 to 11 (45 verified, 0 errors)
- limits: It covers one data structure only. The evaluation is a rubric scored by the authors over 6 runs with Claude 4.6/4.8. No success rate is given.
- how much was read: most of it read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_google.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_agents.md
- record id: fewer-assumptions-by-design-2026
FM-Agent (2026)
- title: FM-Agent: Scaling Formal Methods to Large Systems via LLM-Based Hoare-Style Reasoning
- what: An agent writes function contracts in natural language from callers, code and domain knowledge. It reasons about blocks and loops in Hoare style (what holds before and after each piece of code). It then generates and runs system-level tests to confirm suspected bugs.
- number: 277k source lines and 8,549 functions across four systems; 522 new bugs total
- number: Claude’s C Compiler 339 bugs (143k lines), VibeTensor 141, VibeOS 23, Bespoke OLAP 19
- number: cost 2 days and 3.4 billion tokens total
- number: ablation on compiler: 57 bugs vs 339, removing two components at once
- limits: It handles sequential functions only. It cannot ensure soundness, and its reasoning is not machine-checked. The prose says 4,910 functions but the table says 4,957.
- how much was read: most of it read
- source; notes: FM-Agent: useful bug finding, without sound proofs; notes: FM-Agent: useful bug finding, without sound proofs; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_agents.md
- record id: fm-agent-2026
From Verification Failures to Reusable Guidance for Coding Agents (2026)
- what: Turns diagnosed proof failures into reusable procedures (a kit) for coding agents. The agents write specifications and proofs of execution in the K framework, with Lean for leftover math. Separate agents audit the result.
- number: 164/164 final AI audit PASS verdicts after two targeted repairs and heavy human-guided resource development
- number: at the common checkpoint with the kit: 97 Pass, 67 Concerns, 0 Fail
- number: 12-pair challenge: all 12 defects detected, all 12 clean accepted (Wilson interval 75.8-100%)
- number: controlled 31-program test: GPT-5.6 Luna 15/31, 15/31, 19/31; all four intervals include zero
- limits: The target is partial functional correctness (correct if it terminates), and termination is handled separately. The trusted base includes the translation, the semantics and the solver integration. The controlled evidence does not show a clear general benefit of the kit.
- how much was read: most of it read
- source; notes: From Verification Failures to Reusable Guidance for Coding Agents; notes: From Verification Failures to Reusable Guidance for Coding Agents
- record id: from-verification-failures-to-2026
GGMS (2026)
- title: Learning Provably Correct Distributed Protocols Without Human Knowledge
- what: A transformer-guided Monte Carlo tree search learns transition tables for synchronous crash-fault protocols (atomic commit and consensus). Exhaustive model checks give it feedback.
- number: atomic commit 2/1: 100%, 15 min; 3/2: 60%, 813 min; 4/2: 70%, 754 min
- number: consensus 4/2: 90%, 717 min; 4/3: 100%, 3358 min
- number: plain MCTS / DFS baselines often 0-50%
- number: timeouts 1, 2, 4 days for 2, 3, 4 processes; ten runs per setting
- limits: Humans supply the states, decisions, correctness formulas and bounds. The setting is synchronous, crash-only, with finite process counts. Termination is bounded, not asynchronous liveness. It is not an LLM agent.
- how much was read: most of it read
- source; notes: Learning Provably Correct Distributed Protocols Without Human Knowledg; notes: Learning Provably Correct Distributed Protocols Without Human Knowledg
- record id: ggms-2026
IC3Syn (2026)
- title: Synthesizing Inductive Invariants for Distributed Protocols via IC3 and Large Language Models
- what: An IC3 controller hands an LLM (Claude Opus 4.6) concrete bad states to block. The LLM proposes TLA+ clauses. TLC and Apalache check them on small instances. TLAPS then proves the invariant for all sizes.
- number: 29 of 29 protocols solved (Table 1 p. 9); direct Claude baseline 23/29; Gemini 3 Flash inside IC3 solves 27/29
- number: MLDR (MongoDB Raft model): 4525 s, 16 clauses, proof over 3,000 lines; EPR Paxos: 1806 s, 9 clauses
- number: Default synthesis timeout 30 minutes, 2 hours for the two hardest cases
- number: Paper’s rerun of Endive solves 24 shared cases
- limits: The models and safety goals are supplied. Liveness is not evaluated. The synthesis loop works on finite instances only. The proof stage used a scaffold plus Codex automation. The model, budget and log of human intervention are not stated. Full end-to-end automation is ongoing work. No public code or proof artifact was found. The results are the authors’ own reports.
- how much was read: most of it read
- source; notes: IC3Syn: a direct 2026 LLM invariant search result; notes: IC3Syn: agent-written proofs of unbounded distributed protocol safety; notes: IC3Syn protocol inventory
- record id: ic3syn-2026
IDS (2026)
- title: Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems
- what: Given a specification written by an expert in Rocq/Coq, a coordinator of GPT-5.4 workers writes an implementation and a proof that Coq’s kernel checks. It can throw away a data representation and start over. Code is extracted to OCaml.
- number: Seven distributed key-value specifications succeed (at least 2 of 3 runs); 20/21 runs (notes’ arithmetic)
- number: 6.8 hours and 1229, 1 week/ $583, 2 w ee k s /$ 1580; about a month and $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` - 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` - 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` - SpecRL (2026) - title: SpecRL: Reinforcement Learning with Test-Based Completeness Rewards for Formal Specification Synthesis - what: Trains a model with a reward for Dafny contracts that reject impossible input-output pairs. This adds to verification, which cannot tell a useful contract from `ensures true`. - limits: Learns the behavior of the given program. If that program is wrong against human intent, a strong spec encodes the wrong thing (the notes' inference). - how much was read: most of it read - source; notes: Generated contracts and independent evaluation - record id: `specrl-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$ 57 per system across 48 systems (§5.3)
- limits: Model checking plus reproduction gives concrete failures, not proofs for all executions. Its coverage of liveness is weak. The results pool several versions, and only 14 systems used the latest version.
- how much was read: most of it read
- source; 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; notes: Specula: close the model–code loop before calling a violation a bug
- record id: specula-2026
StarVerus (2026)
- title: StarVerus: LLM-Powered Multi-Agent Collaboration for Industrial Rust Code Verification Automation
- what: A multi-agent system that writes contracts and proofs. It uses call-graph context, contract alignment, planning, repair and rewriting. It was applied to six Asterinas memory components.
- number: 112 of 163 verification conditions (68.7%); only memory-region initialization reaches 100%, others 44.00%-79.41%
- number: Mutated-code pass rate 7.56% (Table 8)
- number: mutant admission 7.56% (Table 8)
- limits: There is no theorem for the whole OS. The obligations covered are partial.
- how much was read: most of it read
- source; notes: Repository retrieval and multi-function verification; notes: SpecGen and StarVerus: human and model judges need an adequacy audit
- record id: starverus-2026
Stepwise (2026)
- title: Neuro-Symbolic Proof Generation for Scaling Systems Software Verification (earlier title “Stepwise”)
- what: Stepwise uses fine-tuned small models to propose and rank individual Isabelle steps. They work inside a tree search over proof states, with premise selection, QuickCheck/Nitpick filtering and Sledgehammer. A REPL checks each step.
- number: Table 1 p. 8: Mistral 77.6% vs Sledgehammer 40.3%, rerun FVEL 7.8%, rerun Selene 5.6%
- number: 2,167 successful proofs; solved proofs cover 36.2% of original proof lines
- number: 120-minute search budget; 71.1% claimed human-effort saving is a simulation
- number: 77.6% total on seL4 vs Hammer 40.3%, Selene 5.6%, FVEL 7.8%
- limits: Its denominator differs from FVEL’s splits. Longer proofs still fail.
- 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/findings2_agents.md
- record id: stepwise-2026
SysMoBench (2026)
- title: SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems
- what: A benchmark of eleven concurrent and distributed systems. An AI writes a TLA+ model of each. The model is scored on syntax, execution, behavioral match to the code, and expected properties.
- number: source sizes from 175 lines (PGo dqueue) to 5,360 (ZooKeeper leader election)
- number: Etcd Raft with basic Sonnet agent: 7.69% conformance, 69.23% invariant correctness, 100% syntax
- number: liveness properties violated 41.9% vs safety 8.3% (§5, Figure 4c)
- number: each agent run five times, best output evaluated, at most three repairs
- limits: Covers only the finite executions and configurations supplied. A model can match buggy code and still fail the desired guarantee. The evaluator uses an LLM for some mappings.
- how much was read: most of it read
- source; 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; notes: SysMoBench
- record id: sysmobench-2026
SysSpec / SpecFS (2026)
- title: Sharpen the Spec, Cut the Code: A Case for Generative File System with SysSpec
- what: Humans write structured specs for 45 modules, with pre/postconditions, invariants and locking. Agents generate C code, and an LLM reviews it. The result is SpecFS, an in-memory FUSE file system.
- number: about 4,300 C lines, 45 modules
- number: 754 xfstests, 64 fail from unsupported features
- number: Gemini-2.5-Pro and DeepSeek-V3.1 reach 100% module accuracy vs 81.8% best baseline
- number: extent support 4.5 vs 1.5 hours; directory rename 13 vs 2.4 hours (manual vs SysSpec)
- limits: The verification stage is an LLM, not a theorem prover. The evidence of correctness is tests and inspection. Crash consistency is out of scope. The timings cover specific tasks only.
- how much was read: most of it read
- source; notes: SysSpec / SpecFS: sharp human specifications, empirical code checking; notes: SysSpec / SpecFS: sharp human specifications, empirical code checking
- record id: sysspec-specfs-2026
TESTDAFNY110 (2026)
- title: Automatic Generation of Formal Specification and Verification Annotations Using LLMs and Test Oracles
- what: LLMs write Dafny contracts, invariants, assertions and lemmas from code, comments and test methods with expected results. They repair them using verifier errors. Dafny proves the result.
- number: 98.2% of problems within at most 8 attempts
- number: 106 of 110 (96.4%) logically equivalent to expert specs
- number: seven-student crossover study: 85.7% vs 42.1% success, 6.2 vs 11.1 minutes (the notes call these assisted/manual success and average task minutes)
- number: 98.2% on 110 Dafny programs within 8 repair iterations
- limits: Two number-theoretic tasks are unsolved. Four contracts differ from the expert ones until failing tests are added. It needs human tests that discriminate between right and wrong.
- how much was read: most of it read
- source; notes: Automatic Generation of Formal Specification and Verification Annotati; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_eval.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/verified_primary_notes_20261012.md
- record id: testdafny110-2026
The Verifier Tax (2026)
- title: The Verifier Tax: Horizon Dependent Safety Success Tradeoffs in Tool Using LLM Agents
- what: The paper runs tau-bench experiments with an LLM verifier prompt that checks the steps of the planner and the actor. It reports that safety checks cut safe success sharply, while raising token use.
- number: 2,970 episodes, three runs, GPT-OSS-20B and GLM-4-9B
- number: GPT-OSS-20B retail Triad-Safety success 21.5 ± 2.7%, safe success 0.6 ± 0.5%
- number: tokens 2.0-2.8x
- limits: The verification is an LLM judgment, so it is not sound. After three failed revisions the last proposal is accepted by default, so the causal story is weak. There is no artifact.
- how much was read: most of it read
- source; notes: The Verifier Tax: Horizon Dependent Safety Success Tradeoffs in Tool U
- record id: the-verifier-tax-2026
TLA-Prover (2026)
- title: TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation
- what: It trains gpt-oss-20b with a small adapter, first supervised and then learning from repairs of rejected specs. The model writes TLA+ specs, which TLC grades. The top Diamond tier adds sensitivity to a mutation of an invariant.
- number: 9/30 pass@1 (30%) greedy; 11/30 best-of-eight; 13/30 union
- number: TLC: usually three processes, 60-second budget
- number: baseline: 25 models on 26 specifications, 650 runs per cell, 8.6% (not matched)
- number: Across 25 LLMs the best public baseline is 26.6% syntactic parse and 8.6% semantic model-check
- limits: Success means a small model passes its own invariant. It does not mean agreement with a human requirement or a system. The text says six domains, but Table 3 lists ten. There is no refinement or liveness proof. The result was not reproduced.
- how much was read: most of it read
- source; notes: paper; notes: meaning for evaluation; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_agents.md
- record id: tla-prover-2026
TLA-Verus (2026)
- title: TLA-Verus: Generating and Solving Temporal Proof Obligations with LLM Agents
- what: This work translates existing TLA+ models into Verus temporal proof tasks. The translator is either an algorithm or an LLM writer plus reviewer. It builds on Anvil’s temporal logic library, and agents prove the tasks. Checks freeze the task and reject new assumptions or admissions (unproved claims accepted as true).
- number: 16,459 model/property pairs attempted
- number: algorithmic: 5,160 usable translations, 3,094 proofs (304 liveness)
- number: agentic: 12,352 usable translations, 492 proofs in a 500-task sample
- number: evaluation: 40 paired tasks, ten per category, 32 models from 24 repositories
- limits: Showing that the implementation refines the model is future work, so a model proof is not a proof about Rust behavior. An LLM reviews whether the translation is faithful, and this is not proved. The dataset and pipeline are unreleased. The runs were not repeated. A Raft-style model was safe only because it could not make progress.
- how much was read: most of it read
- source; notes: closest related work; notes: reported results and populations; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_b/agent_evaluation_procedure.md
- record id: tla-verus-2026
Toward Safe LLM Agents: A Survey of Specification, Verification, and Enforcement (2026)
- what: A survey of 38 studies on specifying, verifying and enforcing safety for LLM agents. It distinguishes model checking of an extracted model from runtime enforcement on actual actions.
- number: 38 studies from six databases
- number: headline 24% to 35% concerns PDDL planning formalization only
- number: 94% interception with under 5% safe completion comes from one study
- number: single reviewer
- limits: Focuses on safety. No new measurement. Certainty is mostly Low or Very Low. Its broad claims about limits should be audited.
- how much was read: most of it read
- source; notes: Toward Safe LLM Agents: A Survey of Specification, Verification, and E; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_google.md
- record id: toward-safe-llm-agents-2026
TraceFix (2026)
- title: TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples
- what: Claude Opus 4.6 turns a task description into a topology of agents, locks and channels. It writes PlusCal for each agent, runs TLC, and repairs from failures. The checked processes become runtime prompts.
- number: 48 of 48 tasks reach TLC verification; 30/48 pass first try; hard tasks 4/16 first try
- number: 29 repair attempts: 20 deadlocks, 5 timeouts, 3 syntax errors, 1 undrained channel
- number: Mean about 594 s and about 70, two hours compute, one day of human review, vs about five days of human work
- number: Mechanization: 1938 lines at $139 v s 2071 l in es an d$ 140 for the AI-authored proof
- limits: The AI-written proof needed more human feedback to find places where it did not match the intent.
- 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: just-type-it-in-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
MachCSL (2026)
- title: xv6 on RISC-V with AI agents (MachCSL)
- what: Agents proved an xv6 operating-system kernel on RISC-V in Rocq, against a top-level statement: typing on the console prints only the typed text. Humans laid out the plan and designed the intermediate specs. Agents did the proofs.
- number: 93 days; 1,479,165 lines of Rocq (294,402 generated) for 6,593 lines of xv6
- number: 474 sessions, 2,620 sub-agent runs, 5,889 human prompts (median 13 words)
- number: 2,062 agent-hours, 1,205 wall-clock hours, 226.9M output tokens, under $3, 000 in s u b scr i pt i o n s - n u mb er : T e n xv 6 b ug s an d o n e S ai l b ug f o u n d; m e d iank er n e l - u p d a t er e - p r oo f 35 a g e n t - min u t es - l imi t s : I t co v er ss a f e t y o n l y, n o tl i v e n ess . H u man ss t eer e d t h e l a y er in g an d s p ecs h e a v i l y . - h o w m u c h w a sr e a d : p a r t sr e a d - [so u r ce] (h ttp s : // a r x i v . or g / ab s /2609.04043); n o t eso u t s i d e t hi ss i t e : ‘/ ss d 1/ s i c han g h e a g e n t / v er u s_{d} i s t r ib u t e d / l i t_{a} / f in d in g s 2_{a} g e n t s . m d ‘ - r ecor d i d : ‘ ma c h cs l - 2026‘ - M u nk r e s^{'} G e n er a l T o p o l o g y A u t o f or ma l i z e d in I s ab e l l e / H O L (2026) - w ha t : LL M co d in g a g e n t s (C ha tGP T 5.2, t h e n C l a u d e O p u s 4.6) w r o t e an I s ab e l l e / H O L f or ma l i z a t i o n o f a l l 39 sec t i o n so f M u nk r e s^{'} T o p o l o g y . T h ey u se d a w or k f l o w t ha tw r i t essor r y f i r s t, pl u ss l e d g e hamm er . - n u mb er : o v er 85, 000 l in es, 806 f or ma l r es u l t s, z er osor r y, 24 a c t i v e d a y s - n u mb er : 2.66 M o u tp u tt o k e n s, 17.2 bi l l i o n c a c h e - r e a d t o k e n s, es t ima t e d A P I cos t$ 8,895; effective cost about $160 o na$ 200/month subscription
- number: about 83% automated
- limits: The agent defined its own notions in parallel to Isabelle’s library. It also added “safe” extra hypotheses. There is no layer to reconcile them. The context for the 83% figure was not fully read.
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_leads.md
- record id: munkres-general-topology-autoformalized-2026
NLForge (2026)
- title: Natural Language based Specification and Verification
- what: This is not a formal proof. An LLM checks C/C++ memory safety bottom-up. It writes a natural-language summary of each function and reuses the summaries for the callers. The authors evaluate it on SV-COMP 2026 subsets.
- number: Sonnet-4.6: 1262 true positives, 4 false negatives, 354 false positives
- number: CPAchecker: no false positives or negatives but 247 cases unknown
- number: cited benchmark: 95.67% syntax correctness and 3.69% verification on compositional tasks
- limits: The notes cover about 50% of the paper. It is useful for finding bugs, not as a replacement for sound verification.
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_google.md
- record id: nlforge-2026
P3 (2026)
- title: P3: Joint Program-and-Proof Planning for Verified Code Generation
- what: P3 plans the implementation and the proof together before generating either. It also introduces Lean4Commit0, a benchmark built from real libraries.
- number: Lean4Commit0: 108 libraries, 511 code and 519 theorem placeholders
- number: also 189 Verina and 77 AlgoVeri tasks
- number: gains of 4.6-11.2 points over the stronger baseline; cost and time down up to about 40% and 37% on difficult subsets
- number: improves by 4.6-11.2 percentage points (as quoted)
- limits: The specifications are provided. The LLM review during curation can miss flaws in the specs.
- how much was read: parts read
- source; 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; notes: papers
- record id: p3-2026
Reward hacking in Dafny RLVR (2026)
- what: Reinforcement learning on Dafny raised the verified reward, but it also revealed specification hacking: trivial postconditions, and leaking the answer through helper functions.
- number: Verified reward 2.2% to 58.1% but with spec hacking; after filtering, multi-turn RLVR 9.7% to 31.1%
- number: Lean VeriCoding pilot 46.2% to 69.2%
- limits: For Dalek-Bench (repository-scale Lean), preliminary results remain weak.
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_agents.md
- record id: reward-hacking-in-dafny-2026
SaltBench (2026)
- title: SaltBench: A Referee-Gated Protocol for Measuring Method Effects in Machine-Checked Software Work
- what: A protocol with four arms: plain versus specify-and-verify, each with either an agent-written or a supplied spec. It uses five Rust components (Crc32, FreeList, LRU, LZW, Paxos). A referee holds back a test suite and grades behavior. For Lean it also checks reconstruction, replays the proof in the kernel, compares frozen expressions, and audits axioms.
- number: v3 post-hoc analysis: 447 cells pass, 40 fail
- number: 10 budget-censored and 4 unscorable cells
- number: allowed Lean axioms: propext, Classical.choice, Quot.sound
- number: asking for proofs cost more on all five components, no premium exceeded 2.8879x
- limits: The correctness analysis is post hoc and descriptive, with three cells per condition, so it supports no causal conclusion. Paxos as a task is not a proof of unbounded Paxos liveness. The September human note describes v1, not v3.
- how much was read: parts read
- source; notes: SaltBench: current October revision changes what can be cited; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_shortlist.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_b/agent_evaluation_procedure.md
- record id: saltbench-2026
SpecSyn (2026)
- title: SpecSyn: LLM-based Synthesis and Refinement of Formal Specifications for Real-world Program Verification
- what: SpecSyn checks how strong a spec is by using mutants that are not semantically equivalent to the original.
- number: precision above 90%, recall above 75% on target properties
- limits: The properties come from the program. They do not come from unconstrained intent.
- 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/verified_primary_notes_20261012.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_b/agent_evaluation_procedure.md
- record id: specsyn-2026
The Prover Is the Judge (2026)
- title: The Prover Is the Judge (Ada/SPARK, Codex CLI and Claude Code)
- what: GPT-5.5 under Codex CLI, then Claude Opus 4.8 under Claude Code, wrote and verified SPARK code for ML-KEM, TLS 1.3, IKEv2, X.509 and a Matrix client. The human never wrote code, contracts or proofs.
- number: GNATprove discharged 49,280 proof obligations
- number: Roughly 20-40 times lower supervision cost than comparable hand verification
- limits: The anti-cheat rules are enforced by skill text and human review, not automatically. The code is at https://github.com/tobiasphilipp/experimental-agentic-verified-software.
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_agents.md
- record id: the-prover-is-the-judge-2026
Towards an Agentic LLM-based Approach to Requirement Formalization from Unstructured Specifications (2026)
- what: LLM roles extract requirements. A judge filters out those the target formalism cannot express. The pipeline then translates the rest to UPPAAL SMC queries and checks syntax. The domain is human-robot interaction.
- number: extraction: 81.8% exact-or-partial semantic matches (exact 43.6%, partial 38.2%); recall 60.6%
- number: verifiability classification: accuracy 88.7%, recall 94.2%
- number: translation: 95.8% syntactically correct, 77.8% effective semantic accuracy
- number: reported as 77.8% across three scenarios
- limits: An LLM judged whether the meaning matched. It has no distributed systems and no liveness. Accuracy is specific to the scenario.
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_google.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/verified_primary_notes_20261012.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_b/agent_evaluation_procedure.md
- record id: towards-an-agentic-llm-2026
Veil blog (Sergey) (2026)
- title: Verifying Distributed Protocols in Veil
- what: Reports Claude Code finding agreement and validity invariants for FloodSet, using feedback from the checker. The faulty model lumped all crashes together with the broadcast and left out partial delivery, which made agreement hold trivially.
- limits: A case study by a single author, not a comparative score.
- how much was read: parts read
- source; notes: papers inspected; notes: Veil: proofs in Lean with automatic first-order checks
- record id: veil-blog-sergey-2026
VeriHarness (2026)
- title: VeriHarness: Scaling Agentic Verification for Long-Horizon Tasks
- what: This is not formal verification. It checks workspace artifacts that agents make (reports, spreadsheets) on five benchmarks that have no reference answers. The generator’s own model acts as the verifier, with tools.
- number: gain of 6.2 points with Gemini 3.5 Flash and 6.4 points with Claude Opus 4.8
- number: about 26,000 rollouts released at a cost over $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` - VeriSkill (2026) - title: VeriSkill: A Self-Evolution Framework for Program Verification Skills - what: VeriSkill improves skills for program verification, guided by the verifier. Its categories for diagnosing failures include termination. - limits: The review notes established no score for termination alone and no benchmark for distributed liveness. They did not verify the repository URL. - how much was read: parts read - source; notes: Recent agent termination evidence, with narrow scope - record id: `veriskill-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 vs 73.98 per solved problem
- limits: The review notes read only the web page.
- how much was read: parts read
- notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_eval.md
- record id: aleph-prover
quint-llm-kit
- what: Supplies workflows for agents that write specs and code. The Quint LLM-era post links spec generation, implementation generation and feedback from models.
- limits: No theorem was found that the generated Rust refines Quint (matches it as an abstract model).
- how much was read: parts read
- source; notes: R06. Quint Connect, Choreo, and LLM-driven implementation; notes: Quint: production case studies, not a measured proof benchmark
- record id: quint-llm-kit
_refinement
- title: _refinement (accompanying material for ‘A Tale of Two Refinements’)
- what: This is a chat-driven refinement of a TLA+ blueprint into multithreaded Rust, using an LLM (Gemini 2.5 Pro). It includes the steps, the chat history and code-review notes.
- limits: The README shows no proof, no Verus, and no model checker output. The refinement is informal and checked by reading. The notes did not open the steps and chat files.
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_leads.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_model_to_code.md
- record id: refinement
TLA-Prove
- what: This is the public repository of TLA-Prover at commit 6427de9. The audit found two case lists (a 30-row holdout and a 20-row suite called 30-case). It found a saved result (n=30, 1 Diamond, 3 Gold, retrieval on) that differs from the paper. It also found a mutation check that differs from the paper.
- number: holdout_v15.json: n=30, diamond=1, diamond_rate=0.033, three Gold
- limits: The notes did not reproduce the paper’s results, and did not rerun training or inference. The validator graded a two-state toggle with TypeOK as Gold and Diamond. This shows that Diamond does not check whether the spec fits the task. No trained model was run.
- how much was read: parts read
- source; notes: artifact observations
- record id: tla-prove
VeruSynth
- what: Verusynth is a package described as an annotation assistant for Verus, with the verifier in the loop. It handles loop invariants, decreases clauses and assertions.
- limits: The notes verified no paper, benchmark or distributed-liveness case. It is distinct from VeruSyn.
- how much was read: parts read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_agents.md
- record id: verusynth
A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report (2026)
- what: The authors translate production Rust cryptographic code into Lean 4 using Charon/Aeneas or Hax. The target is formal cryptography spec libraries. AI provers (Aristotle, Aleph) then finish the proofs that are still open. They applied this to Plonky3 and RISC Zero. Lean’s small trusted core checks every proof. Aleph proved two bounds theorems that had been left as unproved placeholders (sorry).
- limits: The abstract is cut off before the results on which proof goals the AI closed.
- 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
- record id: a-rust-to-lean-2026
Automating Formal Verification with Agent-Guided Tree Search (2026)
- what: Agent-guided tree search, tested on a Lean benchmark of verified code generation.
- number: GPT-5.4 reaches 95.0% on 423 specs with K = 50 LLM calls
- limits: Only the abstract was read. Code is available on request.
- how much was read: only abstract or first pages read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_leads.md
- record id: automating-formal-verification-with-2026
AxDafny (2026)
- title: AxDafny: Agentic Verified Code Generation in Dafny
- what: An agent system for Dafny. A reviewer LLM rejects cheating patterns (assume, {:extern}, {:verify false}).
- number: Verifies 725/782 (92.7%) of DafnyBench
- number: LCB-Pro-Dafny 56.4% vs 11.6% for direct GPT-5.5 generation
- number: 92.7% on DafnyBench proof-hint task (725/782), 6.5 points above the prior best
- number: 56.4% on LCB-Pro-Dafny versus 11.6% for direct GPT-5.5
- limits: The notes’ author read only the abstract. The ICML listing and arXiv disagree on the margin (6 vs 6.5 points). Both benchmarks are sequential programs.
- how much was read: only abstract or first pages 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: axdafny-2026
BenchShield (2026)
- title: BenchShield: Formal Model-Backed Instrumentation for Reward Integrity in LLM-Agent Evaluation Infrastructure
- what: BenchShield runs taint analysis (tracking where untrusted data flows) over agent-benchmark infrastructure. It looks for ways agents can cheat on benchmarks.
- number: improves full-chain recall from 23-94% to 77-100%
- number: runtime analysis 96% accuracy
- limits: The notes cover only the abstract.
- how much was read: only abstract or first pages 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_shortlist.md
- record id: benchshield-2026
CIll (2026)
- title: CIll: CTI-Guided Invariant Generation via LLMs for Model Checking
- what: An LLM proposes invariants (facts true in every reachable state) from counterexamples to induction (states where the induction check fails). Bounded model checking and induction check them, on two CPU cores.
- number: Targets (Table 1 p. 14): nerv, picorv32, serv and three RISC-V cores
- limits: This is hardware model checking, not distributed systems.
- how much was read: only abstract or first pages read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_agents.md; notes: Adjacent 2026 LLM result that is not a protocol benchmark
- record id: cill-2026
claimcheck (2026)
- title: claimcheck: Narrowing the Gap between Proof and Intent
- what: One model describes a Dafny lemma in English without seeing the requirement. A second model compares that description to the requirement and labels the pair confirmed or disputed.
- number: Own benchmark: 36 pairs, 5 domains, 8 bogus lemmas; two-pass 96.3%, single prompt 86.1%, Claude Code default 69.4%
- number: 36 requirement/lemma pairs, 8 deliberately bad, 3 runs: 108 comparisons
- number: 96.3% accuracy across 108 comparisons; other modes 86.1% and 69.4%
- number: About 108 s per run vs 353 s single prompt, 693 s via Claude Code prompt
- limits: It is small and self-made. The post calls it a probabilistic sanity check.
- 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: claimcheck: check whether the proven claim is what the user asked for
- record id: claimcheck-2026
COBALT-TLA (2026)
- title: COBALT-TLA: A Neuro-Symbolic Verification Loop for Cross-Chain Bridge Vulnerability Discovery
- what: Cobalt pairs an LLM with a TLC REPL. The LLM generates bounded TLA+ models of cross-chain bridges and gets structured traces back so it can repair them. The work was motivated by bugs in the order of events in cross-chain bridges.
- number: three bridge targets including Nomad
- limits: This is a model-checking workflow. Nothing proves that the generated spec is equivalent to the bridge code.
- how much was read: only abstract or first pages read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_leads.md
- record id: cobalt-tla-2026
Comet-H (2026)
- title: Theory Under Construction: Orchestrating Language Models for Research Software Where the Specification Evolves
- what: It proposes a prompt automaton that repeatedly grounds code, benchmarks and papers in each other. The goal is to counter the buildup of hallucinations and the drift between code and theory when a spec keeps changing.
- limits: It addresses spec drift. It does not address refinement or liveness.
- how much was read: only abstract or first pages read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_leads.md
- record id: comet-h-2026
Don’t Trust the Code, Check Its Effects: Runtime Refinement for Regenerated Systems Code Under an Adversarial Generator (2026)
- what: A position paper. Generated systems code only plans actions, and a trusted mediator owns the effects.
- limits: It bears on the trust story, not on distributed proofs.
- how much was read: only abstract or first pages read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_shortlist.md
- record id: don-t-trust-the-2026
Exponential Sample Complexity Separation between Flat and Hierarchical Agentic Theorem Provers (2026)
- what: Theory. It proves that hierarchical provers, which predict a reusable proof DAG (a graph of lemmas and their dependencies), can need exponentially fewer samples than flat provers that learn from fully inlined proof traces.
- limits: The result is theoretical. Only the abstract was read.
- 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
- record id: exponential-sample-complexity-separation-2026
ExVerus (2026)
- title: ExVerus: Verus Proof Repair via Counterexample Reasoning
- what: ExVerus generates counterexamples for failing Verus proofs. It uses them to guide repair, one step at a time.
- limits: Whether a repaired proof is valid depends on the spec it was given.
- 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: What to retain from the already-collected function benchmarks; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_b/agent_evaluation_procedure.md
- record id: exverus-2026
Goedel-Code-Prover (2026)
- what: An 8B model proves Lean program-verification tasks.
- number: 62.0% prove success rate, 2.6x the strongest baseline, on 427 Lean 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: goedel-code-prover-2026
LLM-assisted Verification of Protocol Implementations for Logic Flaws Using TLA+ (2026)
- what: A pipeline from code to Protocol Intermediate Language to TLA+ to TLC, with feedback. The abstract reports three logic flaws, including WolfSSL 5.8.2 accepting CertificateVerify before ClientKeyExchange.
- number: 3 logic flaws confirmed by the vendor
- number: Three logic flaws identified, confirmed by the vendor (abstract)
- limits: Only the abstract was available. The human inputs, the scope of the proofs and the method are unverified.
- how much was read: only abstract or first pages read
- source; notes: Located but full text unavailable; notes: Located but full text unavailable
- record id: llm-assisted-verification-of-2026
MechMath (2026)
- title: MechMath: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving
- what: An agent uses Lean’s sorry placeholder to isolate each unresolved subgoal in a clean context and solve it on its own. This avoids both regenerating the whole proof and long contexts.
- limits: The notes’ author read only the abstract.
- 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
- record id: mechmath-2026
Model-Bench (2026)
- what: 400 Python programs converted into specs for a model checker.
- number: 400 programs
- limits: The direction is code to model. Only a fetched summary was read.
- how much was read: only abstract or first pages read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_model_to_code.md
- record id: model-bench-2026
ModelWisdom (2026)
- title: ModelWisdom: An Integrated Toolkit for TLA+ Model Visualization, Digest and Repair
- what: It combines visualization with LLM assistance for TLA+ model checking. It targets two problems: reading raw counterexamples and handling large state graphs.
- limits: It is not a method for synthesizing intent.
- 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 outside this site: /ssd1/sichangheagent/verus_distributed/lit_b/agent_evaluation_procedure.md
- record id: modelwisdom-2026
NFV (2026)
- title: Neuro-Formal Verification: Agentic Language-Agnostic Formal Program Reasoning
- what: An agent writes a Dafny proof obligation from code in a mainstream language.
- number: correctly resolves 57% of all entries, with 92% precision among its verdicts
- limits: The notes’ author read only the abstract. It optimizes for empirical accuracy, not end-to-end soundness.
- how much was read: only abstract or first pages read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_shortlist.md
- record id: nfv-2026
OSFoundry (2026)
- title: OSFoundry: Building and Evolving Operating Systems with Specification-Guided Agents
- what: Agents guided by a spec build an OS. Tests check the result, not proofs.
- number: passes all 70 functional tests
- limits: The notes cover only the abstract.
- how much was read: only abstract or first pages read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_shortlist.md
- record id: osfoundry-2026
ProGS (2026)
- title: Formal Model Construction Guided by Model-Based Proof Sketches
- what: An LLM builds formal models guided by proof sketches, which are trees that are generated and repaired. This replaces generate-and-repair.
- number: 27-system benchmark
- limits: The review notes read the abstract only. The benchmark number comes from an earlier summary.
- how much was read: only abstract or first pages 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
- record id: progs-2026
ProofSaX (2026)
- title: Synthesizing Proofs Using Proof Sharding and Exploration
- what: ProofSAX is not an LLM. It splits a proof task into shards and searches annotations in parallel for safety proofs of distributed systems.
- number: finds the last proof annotation in 86 of 103 proof-completion tasks, runtimes one minute to two hours
- number: leader election fully automatic in under two minutes
- number: ten 20-core machines
- limits: It covers safety only. For Paxos and Raft it finds only the last annotation.
- how much was read: only abstract or first pages 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
- record id: proofsax-2026
ReCent-Prover (2026)
- title: On Reasoning-Centric LLM-based Automated Theorem Proving
- what: ReCent-Prover is a Rocq proof agent. It has validation-with-reflection, where the LLM scrutinizes its own tactics. It retrieves material based on proof plans that the LLM generated. It was evaluated on CoqStoq.
- limits: The abstract was cut off before the results.
- 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
- record id: recent-prover-2026
Scaling Verification of Cryptographic Software with Aeneas, Rust, and Lean (2026)
- what: The paper argues that verification still has friction (it takes expertise, and proofs must be maintained as code evolves). It says tools have appeared to reduce it.
- limits: The abstract text in the notes starts mid-sentence and is cut off.
- 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
- record id: scaling-verification-of-cryptographic-2026
Spec-Agent (2026)
- title: Agentic Separation Logic Specification Synthesis
- what: Synthesizes specs for open-source C++. It picks a spec language from a ladder, from propositional logic up to first-order separation logic. It turns tests into fuzz harnesses. It refines the specs using counterexample feedback.
- number: valid specifications for 85% of target functions
- limits: Produces specs, not proofs. A spec counts as ‘valid’ based on fuzzing and expert review. Abstract only.
- how much was read: only abstract or first pages read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_leads.md
- record id: spec-agent-2026
SPECA (2026)
- title: Beyond Code Reasoning: Specification-Anchored Auditing of Multi-Implementation Distributed Protocols
- what: SPECA has an LLM read protocol specs (Ethereum consensus) and write categorized properties. It then audits each client against them. These are not proofs.
- number: 15/15 in-scope Fusaka vulnerabilities with expert augmentation, 8/15 automated
- number: About 2.19 per API
- limits: It covers application-level properties, not distributed ones.
- how much was read: only abstract or first pages read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_shortlist.md
- record id: towards-automated-formal-verification-2025
Specifications: The Missing Link to Making the Development of LLM Systems an Engineering Discipline (2024)
- what: This position paper argues that explicit specifications are the missing engineering layer for LLM systems.
- limits: The pages the review notes inspected show no formal verification artifact or proof result.
- how much was read: only abstract or first pages read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_leads.md
- record id: specifications-the-missing-link-2024
Amazon Verus post (2026)
- title: Developing provably correct Rust code with Verus
- what: Reports that Amazon used Verus on basic building blocks of the Nitro Isolation Engine. It also says that fast automated feedback helps AI agents write Verus proofs.
- limits: It names no agent model, success rate, or count of human interventions. Do not read it as agents proving Nitro.
- how much was read: reading depth not recorded
- source; notes: AWS: production proofs exist; published accounts do not attribute them
- record id: amazon-verus-post-2026
AWS ARG decade post (2026)
- title: A decade of mathematical certainty: Reflections on the Automated Reasoning Group
- what: Lists AWS’s production verification work. Describes Kiro’s requirements checks and its enforcement of agent policies.
- limits: Does not name the verified components, the properties, the sizes, the models or the success rates.
- how much was read: reading depth not recorded
- source; notes: AWS: production proofs exist; published accounts do not attribute them
- record id: aws-arg-decade-post-2026
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
DafnyPro (2026)
- title: DafnyPro: LLM-Assisted Automated Verification for Dafny Programs
- what: It uses Sonnet 3.5/3.7 with strategy hints and assertion pruning. A parser check confirms the executable code is unchanged.
- number: 86% on DafnyBench
- limits: None of its four algorithm benchmarks gives evidence about proofs for distributed systems.
- how much was read: reading depth not recorded
- source; notes: Dafny, C verification, and the specification-intent gap
- record id: dafnypro-2026
Emerald Quint post (2026)
- title: Model-Based Testing EVM networks with Quint and AI
- what: An AI reads the Emerald code and writes a Quint spec, and humans refine it. The AI then generates most of the driver that replays model traces on the Rust code and compares state.
- number: Three validated invariants incl. agreement on decided blocks
- number: Coverage about 80% at the application layer
- number: Found a leak of completed streams
- limits: It gives no model version, no autonomous success rate, and no proof for unbounded cases. The consensus and execution engines are not modeled.
- how much was read: reading depth not recorded
- source; notes: Quint: production case studies, not a measured proof benchmark
- record id: emerald-quint-post-2026
Galois 5STARS (2026)
- title: Using AI to Autoformalize Network Security Properties into 5STARS
- what: It wraps a network-security verifier in MCP. Agents then specialize English security requirements (NIST SP 800-53, MITRE ATT&CK) to a particular network and formalize them. A state machine outside the agent’s workspace controls the phases.
- limits: Results are inconsistent. No model version, denominator or rate is given.
- how much was read: reading depth not recorded
- source; notes: Galois 5STARS: the harness must govern specification construction
- record id: galois-5stars-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
Galois essential post (2026)
- title: Formal Verification Has Become Essential: Let’s Solve the Last Bottlenecks
- what: Calls for common semantics and verified translation across the whole software stack.
- limits: A proposed direction. CompCert, seL4 and HACL* are earlier examples built by humans.
- how much was read: reading depth not recorded
- source; notes: Galois vision and benchmark initiatives: proposals, not completed kern
- record id: galois-essential-post-2026
lemmafit (2026)
- title: Introducing lemmafit: A Verifier in the AI Loop
- what: From an ordinary request, Claude Code writes structured requirements, Dafny state and action code, and lemmas. A file watcher runs Dafny. The verified logic is compiled into a TypeScript API that React uses.
- limits: It covers logic without side effects, in new React/TypeScript apps. The human must review the English spec. The agent model and success rate are not reported. It has no result on autonomous distributed protocols or liveness.
- how much was read: reading depth not recorded
- source; notes: lemmafit: Claude Code writes the specification, implementation, and pr
- record id: lemmafit-2026
LemmaScript (2026)
- title: LemmaScript: A Verification Toolchain for TypeScript via Dafny
- what: Contracts are written as TypeScript comments. The tool derives Dafny or Lean/Velvet models from them and verifies those, while ordinary TypeScript still runs as usual. Example repositories verify shared client/server cores, such as a quota booking app and a rate limiter.
- number: Quorum scheduler 100 Dafny VCs; quota booking 80; Hono rate limiter 23; Henri agent core 48 (README)
- limits: The author warns of gaps between the model and the real semantics. I/O, auth, network and UI stay trusted. No agent model or success rate. The corpus is ‘not an agentic proof benchmark’.
- how much was read: reading depth not recorded
- source; notes: LemmaScript and Velvet: verified TypeScript components, including shar
- record id: lemmascript-2026
Quint race post (2026)
- title: It Told Me No: How Quint Helped Us Fix a Long-Standing Race Condition
- what: A Quint model of the OpenHands Runtime API rejected two proposed fixes for duplicate Kubernetes pods. The accepted fix counted terminating pods and waited for them to disappear.
- limits: It is a case report from the team itself. It leaves open whether the model is too simple to capture another race. It gives no success rate or model version.
- how much was read: reading depth not recorded
- source; notes: Quint: production case studies, not a measured proof benchmark
- record id: quint-race-post-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
Harmonic Lean at scale (2025)
- title: Running Lean at Scale
- what: The post describes proof search over trees of tactics through a Lean REPL. It runs branches in parallel on preemptible compute (machines that can be taken away at any time).
- number: Compressed state about 8% of original size
- limits: It is proof-search infrastructure for training. It is not evidence about verifying distributed code.
- how much was read: reading depth not recorded
- source; notes: Harmonic Aristotle: 96.8% means proof-or-refutation resolution
- record id: harmonic-lean-at-scale-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
Malachite Quint post (2025)
- title: Reliable Software in the LLM Era
- what: A protocol refactor of Fast Tendermint (Malachite). AI updates the Quint spec. Humans check the reachable behaviors and properties. AI changes the code and writes glue for model-based tests.
- number: About 2 days for spec modification and validation, about one week for code and testing
- number: Spec validation found two small bugs in the English spec in one afternoon
- limits: An agent-assisted refactor. The agent did not invent the protocol, and there is no unbounded proof. No measured success rate.
- how much was read: reading depth not recorded
- source; notes: Quint: production case studies, not a measured proof benchmark
- record id: malachite-quint-post-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
dafny-annotator (2024)
- title: dafny-annotator: AI-Assisted Verification of Dafny Programs
- what: Dafny-annotator tests candidate annotations at valid insertion points. It keeps progress that the verifier backs. It learns from synthetic Dafny programs that have been checked.
- number: Fine-tuned Llama-3.1-8B improves from 15.7% to about 50.6% on function-level verification
- limits: The input code and contracts stay fixed. The abstract and the body differ by 0.1 percentage point. It does not test protocol modeling or fairness (the assumption that an enabled action eventually runs).
- how much was read: reading depth not recorded
- source; notes: Dafny, C verification, and the specification-intent gap
- record id: dafny-annotator-2024
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
Lemur (2024)
- title: Lemur: Integrating Large Language Models in Automated Program Verification
- what: Lemur uses an LLM to propose intermediate proof goals. A conventional verifier either establishes them or gives feedback.
- number: Section 5.2: 133 benchmarks (C program plus assertion)
- number: Section 5.3: 47 selected SV-COMP C programs
- limits: It covers sequential C programs. It has no list of distributed protocols.
- how much was read: reading depth not recorded
- source; notes: Lemur: a useful architecture, with no protocol benchmark
- record id: lemur-2024
APG (2026)
- title: Generating Protocol Code from RFC Specifications
- what: It generates C/C++ protocol code from RFCs for ICMP, IGMP, NTP and TCP, and judges the code by testing.
- number: 95% compile success and behavioral correctness for stateless protocols like ICMP
- number: 90% interoperability for complex stateful protocols such as TCP
- limits: It has no formal spec. The notes’ author only skimmed it.
- 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: apg-2026
Structured Abductive-Deductive-Inductive Reasoning (2026)
- what: A general scaffold for LLM reasoning, with property tests of its own code.
- limits: As the notes judge, it is unrelated to verifying programs or protocols.
- 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: structured-abductive-deductive-inductive-2026
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
AWS correctness practices (2025)
- title: Systems Correctness Practices at Amazon Web Services
- what: The paper was not read. Search summaries say it covers P, model checking, fuzzing, property-based testing, fault injection and simulation, with formal specs used as test oracles (the source of expected answers).
- limits: Fetching the paper returned HTTP 403. The claims are unverified search summaries.
- how much was read: not read; title and metadata only
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_gaps.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_humans.md; notes: P02. Systems Correctness Practices at Amazon Web Services
- record id: aws-correctness-practices-2025
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
LeanAgent
- what: LeanAgent is an agent that learns from one Lean repository after another. It manages its database dynamically and proves theorems with best-first tree search.
- limits: The review notes could not read the paper (arXiv 2410.06209) and found no performance number.
- how much was read: not read; title and metadata only
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_agents.md
- record id: leanagent

Last edited: 2026-10-13

Keyboard shortcuts

Steven Hé (Sīchàng)

🤖 database, LLM and agent systems that write specifications or proofs