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

(authored by agents unless marked 🧑)

370 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
AGENT LTL procedural compliance (2026)
- title: AgentLTL: A Trace-Verification Framework for Measuring, Enforcing, and Training Procedural Compliance in Tool-Using LLM Agents
- what: Introduces AGENT LTL, a first-order linear temporal logic for typed tool traces. The same constraints yield deterministic judge-free compliance scores, online tool-call blocking or warnings, and dense reinforcement-learning rewards, including grounding checks tying answer entities to tool outputs. Defines six weighted constraint layers over ordering, branching, argument extraction, pair ordering, global sequence, and grounding; builds 12 workflow templates and held-out transfer splits; compares baseline, soft-block, and block-and-warn harnesses; and finetunes Qwen3-4B with the compliance score. A trace-grounding predicate exposes answers based on parametric memory rather than retrieved evidence.
- number: Block-and-warn improves compliance on five of seven models and raises accuracy by +0.019 on average (§5.1)
- number: Finetuning yields +38 and +17.5 percentage-point gains in accuracy and compliance on held-out patterns (Abstract)
- number: Benchmark has 12 workflow templates; 1,917 valid traces collected for grounding (§4.3–4.4)
- number: Production benchmark contains 360 instances; held-out splits are 83/100/39/39 instances (§4.3)
- limits: Compliance is relative to authored constraints, typed tool signatures, trace logging, and regex/AST grounding extraction. Block-and-warn can alter trace length and strong models may regress; grounding is a sufficient evidence predicate, not complete semantic truth. Finetuning and held-out results cover seven models and the supplied templates rather than arbitrary agent tasks.
- how much was read: most of it read
- record id: agent-ltl-procedural-compliance-2026
Agentic-IC3: Enabling Semantic Proof Search in IC3 Model Checking (2026)
- what: Integrates a language-model agent into a persistent word-level IC3 model checker so RTL semantics and solver feedback guide lemma generalization, derived observations and backtracking. Specifies an agent-oriented interface over Pono/Bitwuzla proof state, with SAT and UNSAT batches, solver-checked lemma admission, observation definitions and revision of earlier proposals. Detailed trajectories show semantic equalities for multiplier completion, occupancy observations relating shift-register and ring FIFOs, and state-guarded backtracking for floating-point adders. The evaluation and ablations separate proof success from interaction cost and demonstrate where semantic actions help or fail.
- number: 10/14 Agentic-IC3 cases solved within 3,600 seconds; rIC3 and A-IC3 each solve 5, Pono-IC3Bits solves 0
- number: four cases are unsolved by all three baselines
- number: agent responses account for 87% of aggregate completed-run time
- number: batching reduces lemma-proposal generalizations 515 to 137 (73%) and solves all ten
- limits: The backend remains the soundness boundary: proposed lemmas are admitted only after SAT/SMT checks. Experiments use Codex CLI GPT-5.6-Sol, one CPU core, 16 GiB, one-hour timeout, 14 selected RTL benchmarks and fresh conversations, so stochastic repeatability and model dependence are unresolved. Current observations are stateless; quantified lemmas and stateful history require future backend extensions. Agent waiting dominates runtime.
- how much was read: most of it read
- record id: agentic-ic3-enabling-semantic-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
- record id: agentic-proving-for-program-2026
Agentic requirement formalization (2026)
- title: Towards an Agentic LLM-based Approach to Requirement Formalization from Unstructured Specifications
- what: Proposes a modular agentic pipeline: extract requirements from unstructured text, classify compatibility with a target formalism, translate suitable requirements into UPPAAL statistical model-checking queries, then semantically evaluate outputs against manually built ground truth. Separating extraction, verifiability filtering and translation avoids forcing one prompt to infer both intent and model limitations. Three cyber-physical scenarios provide 19 natural-language requirements, 12 verifiable; Gemini 3.1 Pro preview performs each stage and an LLM judge assesses semantic equivalence beyond exact string matching.
- number: Requirement extraction combined accuracy 81.8%
- number: Verifiability classification 88.7% accuracy, 94.2% recall
- number: Translation relaxed semantic accuracy 77.8%; exact textual match 34.7%
- number: Scenario SC3 exact 20.6% versus semantic 94.1% after judge
- limits: Ground truth is manually constructed and semantic judge can introduce bias. UPPAAL SMC constraints restrict which requirements are expressible; model abstractions explain discarded requirements. Single model and three scenarios limit external validity; no end-to-end proof that translated queries capture all informal intent.
- how much was read: most of it read
- source
- record id: agentic-requirement-formalization-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 70, about two hours compute, and one day of human review (§6.4)
- number: Human and AI Isabelle developments were 1,938 lines/ $139 an d 2, 071 l in es /$ 140 (§6.4)
- number: Autogeneralization experiment cost 233, Claude $232 an d GP T - 4 o$ 171. The paper supplies no repeated-run uncertainty, formal significance test for its “significantly” wording or complete token/latency account (Q7,Q10). ## What the outcomes establish RQ1 manually compares source behavior and contracts, with at least two authors coding independently and resolving conflicts. Source changes include compiler errors as well as semantic changes. Table III has 246 changes: NL 64, FB 82, FBP 100; Claude 86, Gemini 98 and GPT-4o 62. Source inter-rater Cohen’s kappa is 0.73. The prose divides 246 changes into 102 semantic edits and 143 compile-related cases, which sum to 245. Their overlap or an omitted case is not resolved by the paper (Q6,Q8,T3). Table IV reports 2,375 equivalent, 146 strengthened, 116 weakened and 90 other contracts. The advertised 92% combines 2,375+146=2,521, while exact-equivalence coding is 87.1%. The authors define strengthening jointly for pre- and postconditions, without a formal behavioral-refinement criterion. A stronger postcondition can add guarantees; a stronger precondition can exclude previously allowed inputs. Thus eq+str does not automatically mean preservation of the original contract on its whole domain. This is a logical qualification, not a finding that all strengthened examples are wrong. NL accounts for 114 of 116 weakened cases; 66/90 other cases have missing or duplicate specifications. Contract-coding kappa is 0.38, explicitly “fair” in §IV-A2, despite §V calling the pair “moderate to substantial”; more than 275 NL coding conflicts were resolved (Q6,Q9,Q12,T4). RQ2’s 31.4% is a checker-success rate, not a reported joint rate of unchanged source, adequate original contract and complete verification. Table V gives NL/FB/FBP averages 24.6/29.5/39.9%, and Claude/Gemini/GPT-4o averages 29.8/39.7/24.5%. Gemini is highest for every input type; Claude FB is lower than its NL result, so formal guidance does not improve every individual cell. FBP success also changes the supplied information, rather than proving a particular prompting mechanism causes better reasoning (Q8,Q10,T5). Table VI’s feature averages are 51.2% other/basic SL, 30.9% recursive predicates, 12.3% concurrency and 11.4% loops. Gemini’s hard-case figures are 21.5% concurrency and 21.4% loops, versus Claude 10.4/9.4% and GPT-4o 5.2/3.4%. These describe this curated, tagged dataset and one output per condition; they do not establish distribution-free model rankings (T6,Q10,Q12). ## Error analysis and concrete cases RQ3 selects 50 low-success functions, then examines their 354 failing variants. It is not a random sample of every failure: category success thresholds are 33/33/44/56%, quotas 7/7/22/14, all eligible author cases are chosen first and public cases fill remaining quotas randomly. Authors repair each failing output until verification, record errors/severity/location/fix and reconcile independent analyses, preferring fewer modifications when repairs differ. The coding and repair order affect which errors become visible; no RQ3 agreement metric is reported (Q6,Q11,Q12). Table II gives four useful distinctions. Misplaced queue pre/postconditions cause a compile error. Opening heap predicates reveals that both null heaps have INT_MAX minimum values, a practical automation step. A list-segment concatenation lemma restores an invariant after advancing a pointer. An array loop invariant recording only ten arbitrary elements is logically too weak to prove ten zeros and needs an initialized-prefix invariant. The last example is a genuine missing property, not merely absent predicate unfolding (T2). Tables VII–VIII contain 1,652 coded errors: 383 compile, 1,167 practical and 102 theoretical, or 93.8% in the first two categories. Component totals are predicates/contracts 381, open/close/assert/leak 767, lemmas 331, invariants 61, source 55 and other 57. The 94% headline is this operational taxonomy; it does not experimentally identify models’ internal knowledge or prove that errors are unrelated to general reasoning. There are 858 required-heap-chunk failures, 51.9% of all errors, and 58 missing/incorrect malloc-block cases. These are errors in selected failing outputs, not percentages of all generated functions (Q11,T7,T8). Of the 767 open/close/assert/leak errors, reported causes are missing 58%, redundant 31%, misplaced 7% and wrong 4%. Lemma errors are 62% missing and 23% redundant. Invariant errors include 20% missing, 25% too weak and 20% too strong. For the 381 predicate/contract errors the prose’s 44% compiler share matches 167/381, but its syntax 22% plus type 13% totals only 35%; the missing percentage is not explained. The table, finer prose fractions and denominators should remain distinct (Q11,T7). The authors report VeriFast’s automatic folding/unfolding can fix 39.4% of open/close errors. This is not 39.4% of all errors, all functions, or an evaluated end-to-end increase in passing functions. Heap-state feedback, better error messages and retry loops are proposals; the measured main study does not deploy a feedback agent (Q11,Q13). ## Static artifact checks and trust boundary The analyzer keeps a named target function and replaces other parsed executable bodies with //@ assume(false). Therefore passes concern a selected function under remaining declarations/contracts; they are not whole-program proofs that all generated callees were independently verified. The extractor accepts C function declarations and function typedefs as well as definitions, while target eligibility checks names rather than requiring a body. This further limits treating every row as verification of an implemented function. These are inspected source behaviors, not measured false-positive rates (C1–C3). The subprocess wrapper labels success by the substring “0 errors found”; it does not check the process exit status, set a timeout or reject assumption markers. The contract prefilter compares nonempty dumped AST strings of declarations and initial definitions, then marks the rest “unknown” for manual review. That is syntactic triage, not a proof of semantic equivalence or strengthening. The shell source prefilter strips comments, preprocessor directives and whitespace before diffing; it is also triage. Neither prefilter replaces the paper’s manual resolved coding (C1,C4,C5). Each of the nine verification CSVs has 303 distinct benchmark names. Their yes counts in Claude/Gemini/GPT order are NL 79/109/36, FB 73/118/77 and FBP 119/135/110, totaling 856. In particular Gemini FBP is 135/303=44.55%, whereas Table V prints 44.2% (compatible with 134/303). The current wrapper emits “parse error” or “other error”, but the released CSVs use “no”; source and published reports therefore cannot be assumed to be an unchanged exact run snapshot. The six formal-contract CSVs contain 1,307 syntactically equivalent and 511 unknown cases; these are prefilter results, not the 2,375 final manually equivalent count that also includes NL. The source-change prefilter lists 780 candidate paths, not 780 final semantic changes. No raw logs or resolved XLSX coding were inspected to settle provenance or join all outcome dimensions (C8,C9,reader-static-scan.json). A lexical scan finds “assume” in 32/2,727 primary output files and exact “assume(false)” in four. The four were then read whole. Gemini’s generated thread_start explicitly uses contradiction to trust its stub; its CSV label is “no”. Claude’s charreader contains an assumed helper lemma and is also “no”. Gemini’s barrier_thread2 is “no”; barrier_main is “yes”, but its assumptions occur in a non-target barrier helper. The analyzer removes that helper’s executable body when checking main, so this does not establish that the passing target relied on those exact assumption statements. It does establish that a “yes” row and unchanged executable behavior do not by themselves document the complete proof trust boundary. These literal counts are neither counts of unsound verified targets nor exhaustive checks for all spellings of assumptions (C11–C14,C8). All three retained generated append-tail FBP outputs are “no” in their CSVs. They attempt segment lemmas/invariants but differ from ground truth; this is a concrete artifact example of proof-structure difficulty, not a reader-reproduced verifier failure. Shape contracts and the artifact’s simpler value-free node representation remain explicit (C10,C15,C8). ## Contribution to the requested topics The authors position this study as an extension of Rego et al.‘s preliminary separation-logic work: “We extend and refine their preliminary work to explore more LLMs, prompting approaches, and benchmarks.” They additionally claim function-level analysis, error severity coding and actionable insights as extensions. Their AutoVerus comparison explicitly distinguishes its multiple-agent refinement from this study’s lack of LLM feedback loops. These are the authors’ related-work comparisons (§VI,p11,Q14); the cited studies were not independently read as part of this record. This directly informs evaluation of LLM-written specifications and proofs: report checker success alongside contract meaning, allowed source changes, proof assumptions, function-versus-program scope, dataset selection, repeated sampling and evidence provenance. Its error examples explain why heap ownership, unfolding and segment lemmas challenge automation even when the intended property is understood. The manually coded dataset and released outputs can support further work, subject to the recorded discrepancies and unread coding workbooks. There is no distributed protocol theorem, Verus/Rust development or TLA+ model in this study. Concurrency is a C benchmark category, not a proof of a message-passing distributed service. Applying its lessons to Verus agents or distributed-system proof pipelines is a reader proposal: preserve the original code/contracts, audit trusted assumptions, distinguish auxiliary-proof completion from specification synthesis, and count the joint validated outcome rather than checker acceptance alone. The paper does not measure those proposed pipelines.
- number: 303 C functions from 60 programs
- number: overall verifier success 31.4%
- number: Cohen kappa 0.73 and 0.38
- limits: Curatedsmallknown-verifiableC;oneoutputpercondition;selection-setreuse;manualcoding;faircontractagreement;functionlevelunderremainingcontracts;equivalentplusstrongerdoesnotestablishequivalence;CSV/paperdiscrepancy;no checker rerun.
- how much was read: most of it read
- source; notes: Empirical VeriFast study: score changed code and changed claims explic
- record id: an-empirical-study-of-2026
APE-Bench repository-scale proof engineering (2026)
- title: APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries
- what: Defines Automated Proof Engineering (APE) for repository-scale Lean/Mathlib maintenance and releases APE-Bench plus APE-Harness. Contracts pin repository/toolchain, objectives, access boundaries and verification protocols. APE-Bench mines real Mathlib commits, synthesizes natural-language instructions and validates patches with dual checks: Lean compilation and LLM-judge semantic requirement/scope validation. APE-Harness provides isolated workspaces, version-scoped retrieval, execution services and interchangeable APE-Agent, Claude Code and Codex scaffolds. The benchmark contains 100 tasks from 67 Mathlib commits (2026-01-06–12), 10–284 changed lines, 17 mathematical domains, and is evaluated against miniCTX (334 tasks) and miniF2F (244). Under $3 an d 100 t u r n s p er t a s k, G e mini 3 F l a s h r e a c h es 47$ 12.9K to $197. L imi t a t i o n s a r e L e an / M a t h l ib - o n l y, s in g l e - f i l e m o d i f i c a t i o n s an d LL M - j u d g esco p eer r or s . A pp e n d i x A t r a ces a s q r t co n t in u i t y / f i l t er t a s k so l v e d in 32 t u r n s an d$ 0.79, while Appendix B gives judges accepting unauthorized declaration deletions and rejecting benign refactoring; these cases explain why compilation and LLM consensus still need calibrated scope checks.
- number: 100 tasks, 67 commits, 17 domains; 10–284 diff lines (median 30)
- number: APE-Bench success: Flash 47%, GPT-5.2 27%, Pro 24% under $3 - n u mb er : mini C T X : F l a s h 87.1 - n u mb er : 95/100 g o l d so l u t i o n s u secr oss - f i l e d ec l a r a t i o n s - l imi t s : E v a l u a t i o n p in s L e an / M a t h l ib v er s i o n s an d b l oc k s t a r g e t f i l es w hi l ee x p os in g r e a d - o n l y co n t e x t; a g e n t s ha v e n o in t er n e t an d o n l y A P E - H a r n essser v i ces . S e man t i ccor r ec t n ess d e p e n d so nmaj or i t y - v o t e d LL M j u d g es, d es p i t ee x p er t v a l i d a t i o n . T a s k s a r es in g l e - f i l e m o d i f i c a t i o n s min e df r o m co mmi t s, so m u l t i - f i l ee n g in eer in g an d o t h er p r oo f ecosy s t e m s a r e n o t co v er e d . F i x e d$ 3/100-turn budgets confound reasoning capability with cost efficiency; the paper itself finds model ranking is budget-sensitive.
- how much was read: most of it read
- record id: ape-bench-repository-scale-proof-engineering-2026
ARTEMIS (2026)
- title: Automating Requirements Formalization: Using LLMs and Low-Complexity Distinguishing Traces for Semantic Validation
- what: ARTEMIS translates English into a restricted English, and then into temporal logic. It shows users simple example executions that tell the candidate meanings apart. Users accept or reject these traces, so they do not have to read formulas.
- number: 218 requirements: ventilator 121, robotics 46, Lockheed autopilot 15, DeepSTL 14, Thales 22
- number: 1.57x (Gemini) and 1.43x (GPT) improvement over best baseline
- number: 2.52x fewer traces on average for candidate sets over 10, up to 10.83x; mean 1.74x overall
- number: 14.22% of requirements lacked a plausible generated spec
- limits: Accuracy means that at least one candidate matches a vetted meaning. User effort is simulated by an expert formula. The atomic propositions (the basic true/false facts) are given. The conclusion says 10.38x but section 7.3 says 10.83x.
- how much was read: most of it read
- source; notes: Automating Requirements Formalization: Using LLMs and Low-Complexity D
- record id: artemis-2026
Autogram (2026)
- title: Invariant Discovery for Networked Systems
- what: An LLM proposes typed expressions using telemetry metadata, not raw values. Then deterministic enumeration, logic checks and statistical tests keep the approximate relations that usually hold between live network measurements.
- number: Full recall on Abilene and GÉANT vs NetNomos 19.8% and 15.1%
- number: GÉANT: 101 relations vs NetNomos 1,645 (946 vacuous, 27 match reference)
- number: Production WAN (about 100 routers, 1000 links): 41 relations in ten minutes; link hold rate 96.5%
- number: full recall on Abilene and GÉANT vs NetNomos 19.8% and 15.1%
- limits: The relations are approximate. They are not inductive invariants (facts that hold initially and are preserved by every step). The paper states no safety or liveness contract, program proof or measure of human effort. It admits false acceptances but gives no rate. Proofs are left to future work.
- how much was read: most of it read
- source; notes: Invariant Discovery for Networked Systems; notes: Invariant Discovery for Networked Systems
- record id: autogram-2026
Automating Formal Verification with Agent-Guided Tree Search (2026)
- what: # Automating Formal Verification with Agent-Guided Tree Search (authored by agents unless marked 🧑) Leo Yao’s 78-page MIT MEng thesis measures Lean code/proof completion on 423 selected benchmark specifications. Its strongest result is a persistent single-agent baseline: “GPT-5.4 hits 95.0% on the 423-spec subset at K = 50 LLM calls” (§5, p63). The final context tree search reaches 88.2%, with some benefits at intermediate token budgets. Neither search design provides a formal correctness, completeness or optimality theorem. This is empirical verification automation, with Lean acceptance as the reported outcome. All 78 pages, 94 references, 18 tables and eight figures were read. All page renders/contact sheets and 13 larger dense-page views were inspected. There is no appendix, checklist, numbered algorithm, numbered equation or formal theorem. Exact quotations with PDF and printed pages are in quotes.json; all table pages, including complete captions/cells, are retained in tables.json. The original pool and official arXiv PDFs are byte-identical. The abstract states, “Code available upon request by contacting the author at leoy@mit.edu.” (p3; Q1). No public thesis implementation or separate supplement was linked on the acquired arXiv page. The author was not contacted. No author code was run/imported, and no serialized data/model/checkpoint was loaded. ## Tasks and what verifier success means The population is deliberately selected: “We evaluate on three Lean subsets: bignum, verified_cogen, and verina, totaling 423 problems.” (§3.1.1, p25; Q2). BigNum has 62 arithmetic tasks originally authored in Dafny, then LLM-translated to Lean. VerifiedCogen has 172 Verus tasks for memory safety/functional correctness, also LLM-translated. Verina contributes 189 original Lean data-structure, algorithm and mathematical tasks. Six other Lean subsets are excluded because of autoformalization, informal/Python or GitHub-derived provenance. The thesis does not independently audit translation fidelity, task contracts or contamination. The Vericoder returns textual replacements for implementation/proof holes. “Each new set of replacements is always inserted into the unmodified original spec rather than into the previous iteration’s output.” (§3.1.2, p26; Q3). Lean compiler success ends an attempt. The described rejection step disallows known generated proof bypass patterns, including sorry, admit, axiom, unsafe, Unchecked.cast and @[extern]. This is an explicit description of the Vericoder harness, not an independently checked claim that every later orchestrator preserves the contract or rejects every possible bypass. The implementation, accepted proofs and full run logs were unavailable. Thus the measurements concern reported completion of these Lean targets under this harness. They do not independently establish correctness of the original Rust/Verus programs, distributed protocols or production software. The trusted boundary includes Lean/libraries, supplied contracts, the translation into Lean and the harness. The state orchestrator can change the base and its hole structure; original-contract preservation is an additional audit obligation (proof-audit.json). ## Baselines, parsing and accounting The targeted reproduction uses ten author-labelled models, five iterations uniformly, no retrieval/tools and a 16,384-output-token cap (§3.1.2–4, pp26–33). The earlier benchmark allowed ten BigNum attempts. Original reasoning settings were unspecified, and provider/quantization choices differ, so sibling-generation comparisons are qualified. Table3.1 reports GPT-5.4 at 24.6%, 47 versus Claude 21 hours/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
Euclean (2026)
- title: Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean
- what: Euclean translates informal geometry into native Lean 4/MATHLIB statements through four stages: constraint explication, prove-first configuration anchoring, retrieval-based mapping to canonical MATHLIB primitives, and compiler-feedback iterative repair. It uses Plane = EuclideanSpace R (Fin 2), injects affine-independence, distinctness, positive-radius and strict-betweenness hypotheses, and contrasts this kernel-checked analytic foundation with custom-axiom geometry DSLs. OMNI-Geometry and Numina-Geometry are generated with DeepSeek-V3; examples show mapping ‘D, A, B collinear in that order’ to Sbtw and triangle non-degeneracy to AffineIndependent. Downstream Goedel v2 training tests whether the corpus transfers to unified theorem proving.
- number: OMNI starts with 780 problems; 768 compile (98.5%). Numina starts with 183,796; 177,597 compile (96.6%). On 30 ablation problems with 32 generations/configuration (960 each), compiling candidates rise Basic 125 (13.0%), +concept mapping 254 (26.5%), +repair 465 (48.4%), +constraint mapping 500 (52.1%), +anchoring 480 (50.0%). Human evaluation on 180 OMNI problems (difficulty ≥4) gives TOP1 48.89% and TOP5 73.33%; 8.0+ problems score 20.00%/60.00%. Goedel v2 Numina Pass@1 is 13.6% base, 15.1% after SFT and 15.0% after DPO. Aristotle proves 25/100 sampled cases after filtering, with 19 unresolved but unrebutted.
- limits: The method is text-only and assumes problem statements fully specify relevant geometry; it does not parse diagrams. Semantic validation at corpus scale is difficult, so Numina-Geometry is a candidate corpus needing expert review and prover filtering. LLMs may omit necessary constraints or add redundant/over-strong hypotheses, reducing generality. Coverage is limited by current MATHLIB geometry APIs. Compilation is only a proxy for semantic faithfulness. The pipeline relies on LLM-generated prove-first reasoning and iterative repair; no guarantee ensures the formal statement preserves the exact intended theorem.
- how much was read: most of it read
- record id: euclean-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
ExVerus (2026)
- title: EXVERUS: Verus Proof Repair via Counterexample Reasoning
- what: An LLM proof-repair pipeline for Verus synthesizes source-level Z3Py queries, generates concrete candidate counterexamples, diagnoses wrong versus weak annotations, proposes mutations and chooses repairs with verifier feedback. Final proofs are checked by Verus. Counterexample validation is implemented for loop-invariant failures only; other examples are heuristic reasoning aids. Avoids decoding lowered solver models by asking the LLM to encode the failing source obligation directly, with finite vector concretization, namespaced element variables and model blocking. The validation module extracts one loop body, translates invariants into start/end assertions and injects candidate assignments; expected assertion-error patterns distinguish establishment from preservation failures. Error triage chooses replace/relax versus strengthen, five candidate mutations are ranked by blocked validated examples for invariant errors or verified subgoals otherwise. Appendices supply all prompts, construction/filtering policies, toolchain sensitivity and failure cases. A separate qualitative Copilot/Sonnet temporal proof rerun illustrates lifting state invariants to execution-trace entailment in an Anvil Kubernetes controller.
- limits: A successful final Verus check certifies the supplied formal specifications under the verifier/SMT/toolchain trust assumptions; semantic fidelity to intended requirements and preservation of code/specifications remain separate obligations. Printed prompts forbid changing executable code and requires/ensures. No independent artifact replay was performed. LLM-generated queries can simplify or mistranslate obligations and concretize arrays. Finding no candidate proves neither absence of violating states nor correctness. Validation for non-invariant errors is explicitly future work; the loop module classifies verifier error symptoms rather than supplying a general independently checked concrete execution witness. An inductiveness counterexample may satisfy current invariants but be unreachable from program initialization. LLM reachability triage is heuristic, not a reachability proof. Blocking finitely many states is a search score, not proof that the repaired annotation is inductive; final verification is essential. Results use Verus0.2025.07.12.0b6f3cb/Z3Py4.15.1.0, temperature1.0, at most10 repair iterations and5 mutation responses. Model providers and stochastic generation limit exact reproducibility; AppendixC notes token costs and provider-side changes. No repeated-run uncertainty intervals or significance tests are supplied. Main tasks are146 VerusBench,67 Dafny2Verus,28 Leetcode-Verus and68 HumanEval-Verus. Four original VerusBench tasks were excluded because they no longer verify. Dafny filtering uses five LLM judgments with majority vote, not formal certification that retained specifications express meaningful intended behavior. ObfsBench has266 LLM-transformed tasks with verified versions repaired as needed. Verification of each transformed specification does not establish semantic equivalence to the original program, and obfuscation is not a guarantee that training contamination has been removed. InvariantInjectBench retains187 of426 mutations from142 seeds, with exactly one invariant different from a reference proof. Its one-repair experiment measures near-correct invariant repair, not arbitrary proof synthesis. Blocking/success associations are observational and the reported subsets do not account for all187 tasks. The system-level AppendixA.3 is one qualitative counterexample-augmented Hands-Off rerun, separate from the core query/validation pipeline. The cited81% over800+ VeruSAGE tasks/eight projects is prior work, not a new ExVerus suite result. Six supplied temporal axiom lemmas remain part of its trust/context boundary.
- how much was read: most of it read
- source; notes: What to retain from the already-collected function benchmarks
- record id: exverus-2026
Federated Formal Verification (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
- record id: federated-formal-verification-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: Table5: Codex5.2 High46assumes; Claude4.8 Max two index runs0assumes/0axioms; Claude4.6 High18assumes/1axiom; Standard/SlotMap0assumes/8axioms. Runs10–50min. Table6 rates all concrete Standard/SlotMap mutators fully opaque.
- 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
- record id: fewer-assumptions-by-design-2026
FLV formal logic verification training (2026)
- title: Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification in Language Models
- what: Introduces FLV, which interleaves formal symbolic verification with natural-language reasoning and trains Qwen2.5-7B/14B in two stages: execution-validated formal-logic supervised fine-tuning, then GRPO policy optimization with hierarchical rewards for format, correctness and verifier feedback. Formal modules return satisfiability, counterexamples or execution outputs during generation; a flexible mode allows direct numerical calculation with formal checks used as validation. The paper measures a logical-consistency gap before training: 39.3% of steps in chains with correct answers are formally disproved, rising to 52.4% for incorrect answers. Data synthesis uses DeepSeek-R1 reasoning, GPT-4o answer judging and Claude Sonnet formal translation; exact-match and semantic-equivalence checks retain executable traces. Training uses about 17k samples, 16 NVIDIA H800 GPUs, 120 RL steps and at most four verification rounds. Across KOR-Bench, BBH, MATH-500, AIME24, GPQA-Diamond and TheoremQA, FLV-RL averages 51.9 (7B) and 58.6 (14B), versus Natural-SFT 36.5 and FLV-RL-14B reaches 30.2% on AIME24 and 63.5% on TheoremQA. Ablations show FLV-SFT 49.8 versus Natural-SFT 36.5; symbolic/logic tools are 62.5% of FLV-RL calls. Verification roughly doubles RL training time and formalization errors limit open-ended generalization. A detailed MATH-500 appendix case is a caution: the smallest cube that is a sum of three consecutive integers is 27 (=8+9+10), but a flawed generated proof and Z3 script claim 81; the model rationalizes a DISPROVED result. This motivates the flexible mode that separates arithmetic calculation from logical validation.
- number: 39.3% formally disproved steps in correct-answer chains; 52.4% in incorrect-answer chains
- number: FLV-RL averages 51.9 (7B) and 58.6 (14B)
- number: FLV-SFT 49.8 versus Natural-SFT 36.5 average
- number: AIME24 30.2% and TheoremQA 63.5% for FLV-RL-14B
- limits: Formal translation must preserve the natural-language reasoning semantics; ambiguous or commonsense-heavy descriptions can generate incorrect feedback. Benchmarks are six curated reasoning datasets and use OpenCompass (greedy decoding except AIME avg@16), so gains do not prove deployment reliability. Real-time verification adds about 2x RL cost and is capped at four rounds. The enforced format initially suppressed direct arithmetic, motivating flexible post-hoc validation. The appendix exposes a correctness threat in generated verifier scripts: a solver call can be mis-specified and its failure rationalized, so executing a formal tool is not itself a guarantee unless the encoding is validated.
- how much was read: most of it read
- record id: flv-formal-logic-verification-training-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
- record id: fm-agent-2026
FormalJudge: A Neuro-Symbolic Paradigm for Agentic Oversight (2026)
- what: Post-hoc agent-trajectory oversight separates intent decomposition,atomic-fact extraction,formal predicate generation and Dafny/Z3 checking. Structured logs are parsed directly where possible;LLMs extract semantic facts and synthesize the constraints. Authors report improved agreement with an LLM-ensemble reference,including deception classification and feedback-based behavioral refinement. Formal guarantees are conditional on faithful facts and specifications,not proofs about an agent policy or natural-language intent. Provides explicit atomic taxonomies and composition formulas for file-grounded deception,tool safety and constraint compliance;localized context extraction separates tool errors,disclosure,document access and fabrication. Adds a trusted-trace evidence-manipulation boundary test,manual integrity atoms,latency breakdown,qualitative-intent proxy examples,multi-turn stress tests and action/task-level evaluation. Iterative feedback sends generated Dafny constraints and failed-predicate explanations back to an agent. Detailed appendices show which observed facts are composed and reveal semantic/specification mismatches that solver success alone cannot catch.
- limits: §3.4 explicitly requires faithful extracted facts and a Dafny specification capturing intended constraints. Errors can enter decomposition, semantic extraction and synthesis. The solver does not verify the LLM, policy, truth of observations or intended meaning. No theorem proves end-to-end soundness of this oversight architecture. Observed trajectories and trusted tool-observation logs must retain provenance. Agent-controlled files and self-reports may be fabricated. Appendix A.3 assumes attackers cannot overwrite the trusted trace; without external provenance a trajectory-only checker cannot recover rewritten original events. Reference labels in §4.1 are majority judgments from GPT-5.2, Gemini-3.0-Pro and Claude-4.5-Opus across three rounds. Metrics measure agreement with that ensemble, rather than independently established ground truth. Opus is also the main judge and specification compiler; correlated model errors remain possible. Seven main agents: GPT-4o, Gemini-3.0-Pro, Claude-4.5-Sonnet, Qwen-2.5 7B/14B/32B/72B. Table 1 uses an Opus judge. Extended robustness uses eight judges including GPT-5.2, Grok-3, Gemini-2.5-Pro, Sonnet and four Qwen sizes. The main five-judge description and extended eight-judge analysis describe different settings. Full benchmark sizes are 2,000 Agent-SafetyBench cases, 400 VitaBench tasks and 200 Deceivers tasks. Vita evaluation actually uses a 100-task split; robustness/cross-verifier analysis uses 30 tasks and 164 tool calls. Deceivers weak-to-strong analysis uses 200 deceptive plus 200 nondeceptive trajectories per agent size. Full benchmark size is not every experiment’s denominator. Agent-SafetyBench reference protocol in Appendix D combines fulfillable/risk annotations with actual actions and uses the ensemble for ambiguity, unlike the uniformly ensemble-based wording in §4.1. Deceivers design labels provide a consistency check; broken tools do not automatically make every resulting trajectory dishonest. Some atomic questions remain substantial semantic judgments: whether a file contains requested information, an answer ignores content, or fabrication follows disclosure. Boolean answers do not make these judgments objective. Qualitative intent uses observable proxies rather than an exact semantics of politeness or manipulation. Agent-SafetyBench refinement uses Opus for decomposition/specification synthesis, including small-agent experiments. For the 7B-judge versus 72B-agent claim, the exact allocation of extraction/synthesis roles matters; judge size alone does not specify the capacity of the complete pipeline. Verification audits completed traces. Refinement regenerates responses or attempts and cannot undo actions already executed. X-Teaming and OpenClaw additions measure unsafe-trace detection, not online prevention or reduction in the native attack success rate. Dafny/Z3 checking can time out or fail without proving the negation. The paper models V as binary but does not fully specify timeout, unknown or syntax-error handling. The 6.4% backend error share classifies an unspecified sample of errors; it does not establish logical unsoundness in Z3. No independent artifact reproduction, compiler/version audit, complete human-label audit or systematic correctness proof of generated checkers is supplied. Attribution to the solver alone is limited when decomposition, contexts, prompts and generated code differ.
- how much was read: most of it read
- record id: formaljudge-a-neuro-symbolic-2026
FormaLLM (2026)
- title: Automating TLA+ Model Synthesis with Large Language Models and Formal Verification Pipelines (WIP)
- what: A one-page poster on a benchmark built from the public TLA+ examples repository to test whether small open code LLMs write TLA+ models from English that pass TLA+’s syntax checker (SANY) and model checker (TLC).
- number: 297 TLA+ specifications, 149 configurations, 49,700 lines of TLA+
- number: Models listed: StarCoder 3B, CodeLlama Instruct 7B, CodeT5+ 2B, CodeT5 Base 220M, SantaCoder 1.1B, DeepSeekCoder V2 Lite 13B (in progress)
- limits: Work in progress: no results reported. ‘Passes TLC’ only means the model runs; it does not say the model matches the English. The poster text also contains an unrelated paragraph about racist tweets, apparently left over from a template.
- how much was read: most of it read
- source; notes: ## FormaLLM TLA+ poster (2026)
- record id: formallm-2026
Freer de Finetti human-steered Lean agents 2026 (2026)
- title: Three Roads to de Finetti’s Theorem in Lean 4
- what: Freer reports a Lean 4 formalization of the de Finetti–Ryll-Nardzewski equivalence for infinite random sequences: contractability iff exchangeability and conditional identical independent distribution. Three routes converge on one finite conditional-factorization interface; only reverse martingales cover general standard Borel targets, while the L2 and Koopman routes assume real square-integrable variables. Human-selected definitions, architecture and accepted edits guided Claude proof generation and GPT review/repair. The reported 42,745-line research artifact builds on a pinned Lean/mathlib toolchain, but needs substantial library refactoring. A reusable skill records proof patterns, concrete instance-management failures, LSP feedback and library search. Records exact theorem hypotheses; shared-interface inputs and kernel outputs; route-specific generality and indicator/embedding/L1/L2 transport obligations; human versus model responsibilities and model versions; original 2.5-page informal source and early common-ending design; reported build and axiom command; full Table 1 data and reader arithmetic discrepancy; code duplication/refactoring categories; skill size and repeated instance-pollution timeouts; absence of controlled proof-agent evaluation.
- limits: Figure 1 assumes StandardBorelSpace Ω, measurable/standard-Borel nonempty target α, probability measure µ and each X i measurable, with X indexed by natural numbers. It concludes Contractable µ X ↔ Exchangeable µ X ∧ ConditionallyIID µ X. The theorem concerns infinite sequences. The Ω standard-Borel assumption is explicitly attributed to Lean conditional-expectation infrastructure; this reading does not claim it is a minimal mathematical necessity (§2, Figure 1). Exchangeability is invariance under arbitrary index permutations; equivalence with finite-support finite-marginal invariance is also reported formalized. Contractability compares equally long increasing subsequences. Conditional i.i.d. is relative to a directing random probability kernel, not unconditional independence. The paper also reports the converse conditional-i.i.d.-to-contractable direction. Exact formal definitions of all predicates and complete proof bodies are not printed here (§2). The common ending takes a sub-sigma algebra G and conditional factorization for each finite initial block, constructs a G-measurable probability kernel and packages ConditionallyIID. It centralizes measurability/product-measure uniqueness. Three routes sharing this interface reportedly exposed definition/support-lemma drift; reader inference: this checks agreement between routes, but is not an independent oracle for intended semantics, and common definitions/ending can share an error (§3.1, §5). Route A alone handles general standard Borel target spaces. Contractability supplies reverse-filtration symmetries; reverse martingale convergence supplies factorization. Real-valued conditional expectations must be converted to event indicators and transported through measurable embeddings back to arbitrary target-valued finite blocks. Supporting work includes Levy downward convergence, time reversal of filtrations and demonstrating the reversed process is a forward martingale (§1, §3.2). Route B has stronger real-valued square-integrability premises. Correlation bounds from contractability and Cesaro/L2 convergence give factorization. Its 12,476 local lines do not mean mathlib lacked CDF/Stieltjes theory. Existing StieltjesFunction, MeasurableStieltjes, conditional-CDF and CDFToKernel APIs overlap. Local code connects particular L1 empirical indicator limits to rational-cut monotonicity, normalization, right continuity, conditioning measurability and finite-block factorization. Authors recommend refactoring against existing APIs before considering upstream contributions (§3.3). Route C is also real square-integrable. On path space a shift induces the Koopman L2 operator; mean ergodic convergence identifies the Cesaro limit as projection onto the invariant subspace. Formal work connects that subspace to the invariant sigma algebra, converts L2 convergence into L1 conditional-expectation/set-integral identities for finite indicator products, and packages the common interface. These three proofs are not equally general (§3.4, Figure 2). Human directed architecture, mathematical interfaces, main definitions/theorem statements and acceptance of edits. Primary proof generators were Sonnet 4/4.5 and Opus 4.5 in Claude Code, with Lean CLI/LSP MCP feedback and the skill; GPT Codex reviewed/repaired, GPT Pro occasionally helped mathematics. Opus 4.5/4.6 collated about 4,000 commit messages for writing history; GPT Codex 5.3, GPT 5.5 and Claude 4.7 reviewed paper text. Paper-writing models must not be conflated with proof-generation models. Skill was also written under human direction using Claude (§GenAI declaration). Project began from approximately 2.5 pages of Kallenberg proofs, without a detailed blueprint. LLMs suggested auxiliary lemmas/interfaces/proof structure and filled proof holes, followed by review/refactoring/golfing. The common ending was formalized early. Authors qualitatively call route efforts comparable, but report no per-route human/model time breakdown. Three months is calendar duration, not autonomous proof runtime or quantified human labor (§1, abstract). Author reports Lean 4.27.0-rc1, pinned mathlib, lake build, and #print axioms deFinetti returning only propext, Quot.sound and Classical.choice. That checked name differs from the exact equivalence name in Figure 1; this paper alone does not establish an independently audited dependency list for every route variant. Reader did not execute a build or axiom command. Kernel acceptance with standard axioms does not itself certify intended theorem selection, minimal assumptions or reusable code quality (§1 artifact). Table 1 reports 42,745 lines, 112 files and 783 declarations. Reader independently added printed component rows: 43,512 lines, 112 files, 783 declarations. Line discrepancy is 767. All values visually verified; printed total preserved rather than silently corrected. No checkout establishes which line count reflects the archived artifact, whether categories overlap or why the discrepancy occurs. Rows group project role, not mathematical novelty (Table 1). Library is explicitly a checked research formalization, not mathlib-ready code. Four categories: existing-mathlib replacement candidates, wrappers/adapters, reusable bridges needing refactoring, exploratory route-specific code. First triage replaces/deletes overlap, keeps needed adapters and extracts reusable lemmas. Naming, imports and slow generated proofs need checks. Reported code volume is not evidence of necessary proof complexity or agent efficiency (§3 assessment). Skill contains 36 domain references, 6 slash-command recipes, 4 role prompts plus hooks/scripts. Concrete repeated failure is measure-theory instance pollution causing timeouts; guidance covers sub-sigma-algebra instances, conditional expectations, domain patterns, error-to-fix mapping, LSP goals/diagnostics and mathlib search to avoid reimplementation. Claude-compatible packaging was also exercised through Codex. Reported other-project reuse, including Numina setup installing the skill, is qualitative and not independently checked here (§4, §1 related work). Formalization reference identifies v1.2; software archive 294caf4a04e4d205a7d1de2dd52dc1cbbc0691e9 and skill archive a332440301a2ed286a4051f57ece1e3eed09cc9e are author-provided reproducibility pointers. No artifact commands were run. Reading the described skill does not install or adopt its instructions (§front matter, Reference 7). No controlled baseline, success/pass rate, failed-attempt dataset, token/cost accounting, human effort measurement, skill ablation or proof-throughput benchmark is supplied. Main evidence is a reported completed checked artifact plus qualitative development history. No distributed protocol, safety/liveness proof, Rust/Verus or TLA+ implementation appears. Direct relevance is evaluating human-steered LLM proof construction, semantic supervision, library reuse and maintenance; generalization beyond this mathematical case remains unmeasured.
- how much was read: most of it read
- source
- record id: freer-de-finetti-human-steered-lean-agents-2026-2026
From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates (2026)
- what: NSPI learns approximate polynomial sum-of-squares structures with Qwen3-8B, refines their coefficients numerically, recovers exact rational certificates, and generates Lean identity/nonnegativity proofs from templates. PolyIneqBench has 522 goals with 3–10 variables: 102 literature/competition examples and 420 synthetic ones. Reported final success is 44/102=43.14% on literature examples and 109/420=25.95% on synthetic examples, totaling 153/522≈29.3%. It has the best reported higher-variable success, while Maple/Z3 and LIPS outperform it on relevant low-dimensional/literature subsets. Exact final checking can protect accepted proofs from faulty heuristic discovery; several supplied theoretical/benchmark listings contain errors that require qualification. Training synthesizes polynomial–certificate pairs through eigenvalue shifting, factorized PSD matrices, LMI shifting and diagonally dominant/scaled diagonally dominant matrices. Over one million pairs support supervised cold start, followed by GRPO on unsolved samples in 3–5,6–8,9–10 variable curricula. Rewards combine coefficient error, format and missing/spurious-monomial penalties. At inference, 32 conjectures are ranked by residual; Gauss–Newton refinement is followed by full-rank projection/rationalization or rank-deficient LDLᵀ/Diophantine reconstruction. A final exact identity and positive weighted squares, rather than an LLM judgment or numerical tolerance, support the claimed Lean result. Appendices supply all stages, source examples, training costs, budget curves, complete Lean scripts, failure analysis and proposed extensions.
- limits: A polynomial SOS certificate is sufficient for global nonnegativity, not necessary. Nonnegative polynomials outside polynomial SOS, inappropriate monomial support, rank constraints or failed rational recovery can remain unproved. Real-coefficient SOS existence does not itself establish a rational certificate in the chosen basis. The task is global nonnegativity over real variables, not general constrained inequalities, optimization algorithms, floating-point implementations or distributed protocols. Converting a constrained/informal problem to this target requires a separate faithful reduction, which Lean acceptance of the resulting polynomial alone does not certify. The final claimed trust boundary is Lean checking polynomial identity and nonnegativity using linear_combination and positivity. Heuristic generation, floating-point refinement and rational recovery need not be trusted if their concrete outputs are fully checked against the intended target. The reader did not run Lean or audit imports, bypass prevention, source conversion or repository implementation. Numerical YALMIP/SDP infeasibility or failure to produce an SOS is not a certified proof of non-SOS without an exact infeasibility witness. The source switches between numerical-certificate failure and categorical non-SOS claims; preserve the weaker measured evidence. Appendix D.2 explicitly states training is disjoint from evaluation. Both synthetic sets share the proposed construction families; no detailed deduplication, near-duplicate search, pretraining audit or independent distribution test is provided. Manual sampling of 50 examples per variable setting is not exhaustive semantic validation. One-hour cap and candidate budget 32 are reported. Mean runtimes are conditional on each method’s solved instances, which differ; reported speedups are not paired-instance or total-throughput comparisons. Baseline default prompts/configurations and API systems differ; no statistical uncertainty or repeated-seed variance is reported. Success at up to ten variables is empirical within the supplied datasets and certificate class. It does not prove asymptotic scalability, complete SOS discovery, human readability, neural novelty, convergence of numerical recovery or superiority on all polynomial inequalities. Future applications to global optimization and Lyapunov stability are proposals. No Verus, verified Rust, TLA+ or distributed-systems experiment appears. Transfer to generating invariant certificates would require an appropriate semantics, target reduction and checker.
- how much was read: most of it read
- record id: from-llm-generated-conjectures-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
GLARE: Scalable Neuro-Symbolic Reward Shaping for LLM Agents via Group-Level Automata (2026)
- what: GLARE shapes LLM-agent reinforcement-learning rewards by extracting observation triples, tracking their most recent values, asking a group-level LLM critic for milestones and bad behaviors, translating these into temporal logic and executing shared automata across the rollout group. ALFWorld and WebShop experiments compare task success and token usage with RL and direct LLM judges. Appendix E analyzes group-centered reward errors, but one claimed ranking lemma is false under its stated assumptions. Records all reward/normalization equations, complete experimental table values and uncertainty terms, exact token-chart labels, six behavioral templates and eight full prompts, all training settings, auditing denominators and concrete hallucination/translation failures. Checks the finite-trace/automaton boundary, supplies a bounded-noise counterexample to Lemma E.2, and preserves discrepancies in global-repeat templates, strict-sequence wording, normalization pseudocode and audit examples.
- limits: §3/§4: Environment interaction is modeled as a POMDP with text observations and sparse task success. The actor uses history, whereas observation extraction operates independently per observation with the goal; action strings are mapped by rules. Deterministic action-to-symbol mapping is conditional on the emitted action, not proof that the temperature-sampled actor is deterministic or that its action succeeds. §4.1/Eq5: For each subject/category pair, a partial function stores exactly one latest value and retains values not contradicted by later extracted observations. This assumes extraction fidelity and adequate frame/update rules. There is no Bayesian uncertainty or explicit unknown-state semantics; stale or hallucinated values can persist. Multiple simultaneous values for one pair have no specified resolution, and a coarse state category can lose independent attributes if represented as separate values. §4.1/Figure3: Identical observation strings within a group share extraction. This removes repeated computation, not semantically equivalent spelling variants. Location and state triples are joined with action propositions to scan each full trace. Figure 3 updates door closed→open, retains door kitchen and adds sliced apple; no correctness proof connects the partial state to the hidden environment. §4.2/Figure11: The critic sees a whole sampled group and goal, identifies state-driven milestones and temporal dependencies, and assigns bad behaviors to six predefined categories. All-failed groups can still supply actually achieved necessary partial milestones. Main counterfactual wording must be read with Figure11’s prohibition on unobserved invented milestones; the all-failure mechanism is not access to a ground-truth planner. §4.3/AppendixA.3/Figures13–14: Positive nested-eventuality clauses are conjoined; negative constraints are separate monitors. Templates and manual examples remain substantive specification engineering. The translator is instructed to replace missing APs with False despite an explicitly incomplete AP list. This is a closed-world approximation: missing observations can make a desired milestone impossible or prohibit a valid action. §3.3/§4.3: The paper mixes finite-state acceptance over finite episodes with Büchi acceptance over infinite traces. General infinite-trace LTL is not always expressible as a deterministic Büchi automaton, and a finite-prefix accepting state alone does not decide arbitrary infinite behavior. Nested eventual milestones and safety templates admit useful specialized monitors, but the paper does not define finite-trace endpoint semantics, end-of-episode handling for X, or a verified translation contract. Spot compilation success establishes accepted syntax/automaton construction, not intended task meaning. Figure13: F(A & F(B)) permits A and B at the same time under ordinary LTL semantics because F includes the present. It does not enforce the prompt’s strict temporal sequence. A trace where A and B both hold only at one instant is a counterexample to strict precedence. Parallel formula F((A & F(B)) | (B & F(A))) permits either order, including simultaneity. No implementation inspection established whether a custom strict-F interpretation is used. AppendixA.3 versus Figure14: Printed global_repeat template G(act_A -> G(!act_A)) forbids even a first A because the inner G includes the current instant. Figure14 instead inserts X, G(act_A -> X(G(!act_A))), which permits one occurrence and forbids later ones under ordinary infinite-trace semantics. Preserve both; do not silently treat the appendix template as a correct repeat-only restriction. §4.3/§6.1: Shared formulas and deterministic transitions ensure repeatable rewards given the same symbolic trace, chosen automata and reward procedure. They do not ensure that errors relative to true rewards are constant across trajectories. An incorrect shared constraint can penalize valid behavior selectively. Neural extraction/critic/translation are stochastic at temperature 1 and formulas are regenerated per group; determinism is conditional on these outputs. §4.4/Eq6: Positive rewards depend on a set P(q) of progressive successor states, described as moving toward acceptance without an explicit graph-distance or progress-ranking algorithm. Trend rewards cover strict intervals between milestone updates, hence can use later progress when retrospectively rescanning the trace. Initial timestamp, handling of empty milestones, repeated accepting states and whether an already rejecting safety state incurs repeated penalties are not fully specified. §4.4/Eq6/Eq7: A violation of any negative monitor triggers one penalty indicator, not a sum over violations. R_total=r_env+βr_LTL+r_fmt. Appendix sets λpos=2, λtrend=.5 and λneg=−.5, success10/failure0 and format−1; the separate shaping multiplier β is not numerically identified there and shares notation with KL β elsewhere. Dense positive rewards can reward time between milestones; no potential-based shaping theorem, policy invariance, optimal-policy guarantee, hard action shield or universal safety proof is supplied. §4.5/Eq8 versus AppendixC/Algorithm1 lines13–18: Main text explicitly pools all valid environment-step rewards in a group, without timestamp alignment. Pseudocode instead computes mean/std across trajectories separately at each timestamp t up to Tmax, with no explicit short-trajectory masking. These are different normalizations; the paper alone cannot resolve which generated reported results. Main pooled normalization weights long trajectories by their number of steps. §3.2/§4.5/AppendixE: Main Eq8 normalizes immediate scalar step rewards, then invokes a trajectory-ratio GRPO objective. Exact token/action weighting, reward-to-return propagation and masking implementation are not fully specified. Appendix E analyzes scalar trajectory reward rankings under a single common denominator; it is not a derivation that either differing step-level normalization yields an unbiased policy gradient or stable convergence. AppendixE/LemmaE.1: Under r_i=r_i+b+η_i and a common positive normalization denominator, group centering cancels a common additive b exactly. If all η_i are equal, true rankings are preserved. This algebra is valid; it does not remove trajectory-dependent systematic reward errors or establish that a shared automaton has equal η_i. AppendixE/LemmaE.2 and CorollaryE.3: The proof correctly derives reversal iff η_j−η_i exceeds the positive true reward gap Δ*. Its next claim that any nonzero intra-group error variance gives positive reversal probability does not follow. Counterexample: true gap1, independent errors each in {−.1,+.1}; errors are not almost surely equal and have nonzero variance, but their difference is at most .2, so reversal probability is zero. A deterministic difference in the favorable direction also disproves the stated generality. A support/tail condition P(η_j−η_i>Δ*)>0 is required; independent nondegenerate Gaussian errors satisfy it. Corollary’s otherwise clause is likewise too strong. §6.1/AppendixE remark: Fixed evaluation logic alone is insufficient for reliable ordering relative to true goals. For example, a shared but wrong prohibition on a task-required move can reverse rankings deterministically. The paper supplies no measured latent true rewards, bound on trajectory-dependent grounding/specification errors, or proof that GLARE has lower error-difference variance than judges. Reported learning stability is empirical within tested runs. §5/AppendixA.2: ALFWorld total benchmark size is stated as3,827 across six household task families; the paper does not specify its exact train/validation/test instance counts or task split. Models are Qwen2.5-1.5B/7B-Instruct in verl-agent. Baseline values are borrowed from GiGPO except GRPO rerun on author hardware; not every comparison is a fresh identically controlled run. Table1: Three random seeds, success rates per task and overall, with ± values whose statistic is not named. Overall success is not necessarily an unweighted average of six columns. No formal significance test is reported. For1.5B,84.5−72.4=12.1 and84.5−76.4=8.1 percentage points; the paper’s relative-gain percent wording is inaccurate. For7B,86.7−75.7=11 and86.7−82.4=4.3 points. GLARE is not best in every task column:1.5B direct judge Pick2=77.8 versus73.6;7B PPO Clean92.5 versus89.9. §5.2/§5.3: Direct group and trace judges are said to share judging policy, prompts, reward scale and trend rewards; context scope differs. Group judge is early-stopped for poor performance; trace judge supplies Table1’s best direct-judge comparison. 7B trace result is selected at peak step100 before later collapse. No complete group-judge success table or full learning curves quantify every stability claim. Step-level judge is excluded for reported20min/step versus100–200seconds for other settings, with the latter time scope not explicitly defined. §5.4/Figure4: Only the first50 training steps enter the token comparison, because trajectories change with learning. Chart labels are averages per training step, not per environment action. Completion tokens GLARE28,042.6/trace184,986.6=15.16%; prompt tokens215,479/294,921.8=73.06%; unweighted combined token count243,521.6/479,908.4=50.74%. These are token ratios, not15% total FLOPs, wall-clock time, monetary cost or end-to-end training compute. Group judge completion54,604.2 is also above GLARE. §6.3/AppendixB: Gemini-3-Flash audits800 textual observations and200 training-log trajectory groups; no human-ground-truth validation, judge agreement or confidence intervals. AP error4.4%, omission2.6%, redundancy1.1%; AppendixB.1 narrows omission to non-seen predicates. Exact triplet/formula counts and temporal sampling protocol are not supplied. The critic’s milestone adequacy/dependency judgments are not independently quantified by these two module audits. §6.3/AppendixB.2: Regex formatting repair and compiler-error retry precede discarding remaining noncompilable formulas. Semantic mismatch12% includes invalid/ineffective plus harmful errors, and harmful4% uses all formulas as denominator, not4% of mismatches. Rates do not measure raw syntax failure, discarded-formula frequency, or all end-to-end reward errors. Harmful errors can punish valid actions, beyond merely reducing reward density. Figures7–8: Concrete AP failures include missing seen(microwave), hallucinating drawer2 located at self, and butterknife/butterknive duplicate names. Redundancy-case prose also mentions a cabinet not present in the displayed example. Harmful negative LTL forbids moving a heated egg into the goal fridge. These illustrate observation/translation faults; no formal proof or exhaustive failure taxonomy follows from a few examples. Figure10: The extractor prompt says only visible facts, noun-normalized IDs and loc/state/goal_match/seen categories; its displayed input contains room, closed drawer and unsliced tomato, but output invents a held cup2 and omits instructed seen triples. The definition says underscores while most examples use spaces. Figure15 calls egg-state-heat and apple-state-hot redundant despite different subjects, contrary to its different-apple example. Figure16’s seen-false exception is not identical to Figure10’s seen-true demonstration. These printed audit/example inconsistencies limit the claim of a clean semantic reference; actual runtime prompt identity is unverified. §6.4/Figure6: Negative-only is reported worse than the sparse baseline, positive-only close to full GLARE with larger deficits on Cool/Pick2. Radar plot has no point labels, replicate counts or uncertainty; exact coordinates are not invented. Positive-only visually exceeds full on some axes, so the synergy conclusion is an aggregate interpretation. No separate ablation isolates state tracker, deduplication, critic or trend shaping, and harmful penalties preclude a hard-safety conclusion. §6.5/Table2a: WebShop preserves critic/translator and changes extractor few-shot examples plus free-form product attributes. Scores/success are GRPO75.8/56.8, direct judge78.8/61.2, GLARE80.2/63.4. This is manually adapted cross-environment evaluation, not zero-shot transfer of an unchanged system. WebShop model scale, split sizes, training/evaluation populations, repeat count and uncertainty are not specified in this comparison. §6.6/Table2b: Authors explicitly say GiGPO beats GLARE on original ALFWorld and WebShop. Perturbed ALFWorld injects random distractor descriptions while preserving task-relevant names/relations: GiGPO86.7original→71.4perturbed, GLARE83.3perturbed. Table2 does not give the corresponding original GLARE row or model scale. Do not equate unrelated86.7 entries without evidence. Perturbation construction/sampling/repeats/uncertainty are not documented; robustness scope is this textual distractor setting. AppendixD/Figure9: Across training, positive milestone triggers increase, unique observation counts fall and generated negative-LTL counts generally fall with spikes. Plots provide no raw series/uncertainty or causal control; falling negative counts alone does not prove penalties are never arbitrary or that behavior improves on every safety criterion. AppendixA.2: Prompt2048/response512tokens;50environmentsteps/episode; group8×16rollouts=128parallel environments; actorLR1e−6, PPOcritic1e−5; rollouttemperature1/validation.4; minibatch256/KL.01/150iterations. Auxiliary4B FP8model temperature1 is already pretrained; training-free refers to no auxiliary fine-tuning, not no policy RL.1.5B policy/reward share2H100,7Bpolicy4A800+reward1A800; these different hardware regimes are not a scale-normalized cost study. §7: This is an LLM-generated temporal reward/specification pipeline, not a proof of agent task correctness. No Verus/verified Rust, TLA+, distributed-protocol safety/liveness proof or mechanized proof kernel is evaluated. It adds concrete evidence about specification grounding, monitor execution, evaluation noise and the gap between deterministic checking and correct goals. Official README: repository is provided for reviewer verification of authenticity, with reorganization promised upon acceptance. Lists trpo/ reward/automata/extraction/evaluation/prompt modules, verl-agent/Spot/torch/numpy/vllm dependencies and training-script/configuration entry points. README names do not establish that the printed normalization or prompt discrepancies are resolved; no code was inspected or executed. §6.2/Figure5: Direct judges can identify bad behavior in reasoning but emit incorrect reward-step indices, described as off-by-one errors or hallucinated indices. Figure5 reasoning names steps27–31–32 while displayed penalty output includes20and26. This is an illustrative reasoning-to-output binding failure, with no measured frequency. Automaton rescanning removes direct neural step-index assignment conditional on correctly grounded events, adequate formulas and correct scanning implementation; it does not remove semantic errors upstream.
- how much was read: most of it read
- record id: glare-scalable-neuro-symbolic-2026
GSIRS TLA-LLM poster (2026)
- title: Large Language Models (LLM) and Temporal Logic of Actions (TLA): How Effective are LLMs for Verification Systems
- what: This poster reports a systematic natural-language-to-TLA+ evaluation over 205 community specifications, 30 models and four prompting strategies. It validates syntax with SANY and behavior with TLC, separating parsability from semantic correctness and cataloguing recurring generation failures.
- number: 205 TLA+ specifications across 98 projects
- number: 30 LLMs from eight families; 2,600 open-model runs and 130 proprietary-model runs
- number: up to 26.6% syntactic correctness but 8.6% semantic correctness; TLC passes occurred only with progressive prompting
- number: semicolon injection occurred in 12.6% of generated files; backticks in 5.9%; 234+ missing module terminators were reported
- limits: The poster is based on a separate published ICSOFT 2026 paper and gives an abstracted poster-level account; its evaluation uses finite TLC configurations and does not establish deployed-code correctness. The dataset is drawn from the TLA+ Examples repository, so its task mix is not a random sample of industrial requirements.
- how much was read: most of it read
- source
- record id: gsirs-tla-llm-poster-2026
HarnessLLM (2026)
- title: HarnessLLM: Rust Verification Harness Generation with Large Language Models
- what: An LLM workflow turns a Rust project’s existing unit tests into harnesses (small driver programs with symbolic inputs) for the Kani bounded model checker. It finds the call patterns in tests, builds symbolic arguments for the project’s own types by following constructors, and repairs compile errors without letting the LLM invent types.
- number: 9 Rust crates, 494 tests, 6651 lines of test code: 294 calling scenarios extracted, 94.66% preserved the original behavior
- number: 294 of 294 harnesses compile in Kani within 10 attempts; 97.3% within 3 attempts; about 1.4 generations per harness
- number: Average 145 s and 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
- record id: ids-2026
Improving LLM Code Reasoning via Semantic Equivalence Self-Play with Formal Verification (2026)
- what: # Improving LLM Code Reasoning via Semantic Equivalence Self-Play with Formal Verification (authored by agents unless marked 🧑) Poon Tsz Nok and Antonio Valerio Miceli Barone use generated Haskell program pairs to train a language model to reason about code. Alice generates a transformed program and either an equivalence proof (SEQ) or a distinguishing input (SINQ). Bob judges equivalence. The paper evaluates rejection-based supervised fine-tuning and downstream benchmarks. It supplies no new soundness theorem for Liquid Haskell or the complete training pipeline. Its reported verifier labels require an additional qualification: the inspected current wrapper does not independently enforce that the model submitted the intended equality obligation. This record covers arXiv:2604.17010v2, dated 3 May 2026, all 20 pages, 34 references, 19 figures, eight tables, two numbered listings and Appendices A–H. The official and inventory PDFs are byte-identical. ACL Anthology lists “Findings of the Association for Computational Linguistics: ACL 2026,” July 2026, pages32273–32292, DOI10.18653/v1/2026.findings-acl.1615 (saved publication metadata). That publication metadata is separate from the arXiv version actually read. The paper does not identify an experimental repository revision. Static findings below concern commit 490fe084d705cb501e0fe34e592f17db2eb44a7b, not an authenticated historical run. ## What the method establishes The reference corpus starts with OpenCodeInstruct programs translated into Haskell by DeepSeek-R1-Distill-Llama-70B. Compilation and execution on a generated input filter the candidates, yielding about 28,000 functions (§3.2, Figure2). Passing that filter establishes that a particular candidate compiled and executed on one input under the filter. It does not prove that the translation preserves the original task, that the reference function meets its intended specification, or that it behaves correctly on every input. AppendixA’s recursive versus fold-based reverse example illustrates alternative Haskell implementations; its typing discussion does not establish that every Haskell program is pure, total or safe. SEQ asks Alice to generate Q and a Liquid Haskell proof of equality with P for all inputs of the declared type. The intended mechanism uses reflected definitions and proof by logical evaluation (PLE). SINQ asks for an input on which their observations differ. AppendixB’s SEQ example compares double x = x + x with double' x = 2 * x; its SINQ example distinguishes "zero" from "non-positive" at zero. These are concrete proof and witness examples, not distributed-system specifications. Conditional equality in the checker semantics remains distinct from a specification of the original natural-language task. Bob samples answers, normally ten, and difficulty is 10 * (1 - N_success/N) (§3.4). Alice generates with target difficulty10 and separately learns to predict observed difficulty. The paper retains hard generator cases and a smaller easy sample, difficulty-prediction examples, and successful proof-generation traces. Bob is fixed throughout seven Alice rounds and fine-tuned once afterward. Each Alice training round restarts from the original base model on accumulated examples; generation uses the previous adapter. This is supervised fine-tuning with rejection sampling. AppendixC discusses reinforcement learning as a possible extension; it is not the evaluated implementation. The base model is DeepSeek-R1-Distill-Qwen-7B, with LoRA adapters. AppendixE gives temperature0.6, top-p0.95, top-k20, presence penalty1.5 and a32,768-token context. The actual reported hard threshold is3, rather than the example/default5. A main run takes “about 3 days on 4 NVIDIA L40S GPUs” (AppendixE.4). That is an author-reported duration, not a reproduced measurement. ## Static checks of the verification and selection boundaries Seven selected repository files were read completely: root and SEQ_v2 READMEs, run_liquidhaskell.py, SEQ.py, the seven-round launcher, the dataset compiler filter and the EquiBench evaluator. The full nontruncated repository tree was used only as metadata. Stored datasets, predictions, checkpoints and scientific result JSON were not loaded. No author code was imported or executed; no GHC, Liquid Haskell, solver or training run was performed. The main equivalence wrapper accepts a generated code block, post-thinking response or entire response as the proof body (generate_proof_body). Its fixed refinement lemma template is commented out. It inserts the model’s text into a module containing reflected P and Q, rejects an empty body, invokes GHC with the LiquidHaskell plugin and returns "proved" on exit0 (verify_equivalence). No inspected check independently requires a refinement annotation asserting the intended equality, fixes the proposition outside model control, or rejects model-supplied additional assumptions/options. A successful process exit alone therefore does not show that this wrapper submitted and checked the target equality. This is a static obligation-integrity issue, not a demonstrated successful bypass or evidence that any reported training example was mislabeled. The small run_liquidhaskell.py example overwrites its initial annotated double example with an addNumbers proof lacking an explicit equality refinement annotation; it is source text, not a saved successful run. The paper’s second few-shot proof example has the same omission. The inequivalence wrapper rejects a Q compilation error and accepts different successful stdout. It also accepts one successful and one failed execution, or differing failure statuses (check_divergence). Runtime and timeout statuses can thus contribute to labels. An observed timeout is not proof of semantic nontermination. Reference compilation is checked separately, but that does not remove every execution failure. The record does not infer the frequency or historical impact of these cases. Selection differs from the paper in the pinned driver. Both generator branches append candidates only when difficulty is at least the threshold; the later easy-generator sample therefore has no candidates. The difficulty-prediction sample takes at most 0.5 * n_hard easy items, at most one third of the resulting subset, rather than half the subset. SEQ generation training retains the original target10 prompt; SINQ generation training rebuilds its prompt with observed Bob difficulty. Both difficulty-prediction branches use observed difficulty as their output label. The source uses >=, while the paper’s hard-case definition uses >. The launcher sets threshold1, versus the paper’s reported3 and README example5. Its base-model restart and single final Bob training do support the described schedule. These differences do not identify the configuration actually used for the paper’s experiments. parse_bob_output normally returns a Boolean, but a missing match falls through as None and an exception returns (None,None). run_bob uses truthiness: ordinary missing output is treated as an inequivalence answer; the exception tuple is treated as an equivalence answer. That can affect difficulty and training selection. No stored-output audit establishes how often either case happened. The selected dataset validator checks function-binding heuristics and compilation; its input-argument filter is commented out. It does not itself implement the paper’s one-input execution stage, which may occur elsewhere. The EquiBench evaluator uses a Haskell-specific system prompt on the loaded benchmark pairs, extracts the first regex match rather than necessarily the final answer, and skips parse failures/exceptions before computing accuracy, precision, recall and F1. It saves parsed/unparsed counts, but the paper tables do not give those counts. These are current evaluation-path limitations, not a reanalysis of stored experimental outputs. ## Evaluation and numerical evidence The main E0 regime attempts SEQ/SINQ50/50 over500 reference programs per round. E1 is SINQ-only with500, E2 is96/4 with500, and E3 is SINQ-only with40 (Table1). Tables6/8 and Figures6/12/15/18/19 report total accepted pairs: - E0:34SEQ and903SINQ, total937 - E1:1,839SINQ - E2:62SEQ and78SINQ, total140 - E3:156SINQ AppendixF estimates E0 yields as34/1750≈1.94% and903/1750=51.6%, using expected branch-attempt counts. It defines expected accepted volume K=P*(p*r_SEQ+(1-p)*r_SINQ), predicts E2≈19.632 pairs per round and chooses E3≈38.04 references, rounded to40. This controls an estimated pair count. It does not equalize actual accepted counts, proof tokens, difficulty, class balance or compute. E2 and E3 actually have140 and156 pairs. The text’s “isolates the causal effect” and “fixed compute resources” claims exceed that control. The paper itself acknowledges residual difficulty/class differences and small samples, and asks for stronger statistical evidence (§7). No independent training-seed replication or uncertainty for those causal differences is established by averaging16 evaluation samples/trials. Intrinsic Bob accuracy increases87.57→91.34% on training-split generated challenges and88.24→88.79% on unseen-split challenges (Table2). The latter is0.55 percentage points. The seven overall difficulty means are0.50,0.50,0.65,0.87,0.66,0.93,1.18 (Figure3); they increase overall but not monotonically. Figure7’s SEQ means end1.89, after2.17,3.00 and1.00, so AppendixH’s “2.0−3.0 in later ones” is only a loose description of some rounds. Difficulty is performance relative to this Bob and these accepted cases, not an independent measure of semantic complexity. Table3 reports Haskell HumanEval Bob Pass@1 rising17.7→26.4%, with compilation errors130→110; final Alice is26.3%/104errors. On MBPP Bob rises26.7→36.9%, errors250→203; Alice is34.3%/218errors. Figure9 labels final Alice MBPP errors212 instead of Table3’s218. This discrepancy remains unresolved. Plot averages over16 trials do not establish independent repetitions of the complete training process. EquiBench’s largest E0 accuracy increase is OJ_V56.5→69.8%, or13.3points (Figures4–5). OJ_A rises50.2→57.4, OJ_VA55.8→55.9, STOKE48.0→51.8; DCE falls55.1→51.9 and TVM51.7→50.1. F1 improves on OJ_A/OJ_VA/OJ_V/STOKE and declines on DCE/TVM. PySecDB accuracy rises67.6→68.8 and F151.3→54.0 (Table4). CodeXGlue accuracy rises48.8→50.5, while recall falls51.1→41.7 and F147.9→43.2 (Table5). The authors describe near-random defect detection; no statistical chance-baseline analysis is supplied. Table7 does not support universal dominance by the mixed or volume-controlled SEQ arms. E0 loses to E1 on MBPP Bob36.9 versus38.8 and Alice34.3 versus39.3, and HumanEval Alice26.3 versus28.1. E2 loses to E3 on OJ_V accuracy63.2 versus65.8/F161.5 versus64.7, TVM accuracy48.8 versus50.8/F133.5 versus33.9, and CodeXGlue F144.1 versus48.5; PySecDB accuracy ties68.7. E2 wins several other comparisons, including the four Haskell generation scores. These small, mixed results support investigating complementary supervision, not a general proof that SEQ uniquely improves reasoning. The validated-count plots contain percentage-denominator errors. Figures12,15,18 divide labels by250, even though E1 uses500SINQ attempts, E2 expects480SEQ/20SINQ attempts, and E3 uses40SINQ attempts. E1 consequently prints yields above100%. For example248/500=49.6%, not99.2%; E3’s26/40=65%, not10.4%. Figure15’s actual branch counts are random, so480/20 are expected denominators rather than authenticated attempt totals. The reported raw accepted counts and Table8 totals need not be wrong merely because the percentage labels are wrong. Figure19 reuses the raw counts. All figures, tables, count trajectories and these qualifications are retained separately. ## Contribution and limits The useful contribution is a concrete way to generate semantic reasoning tasks and combine proof-oriented examples with distinguishing-input examples. The study exposes low positive-equivalence yield, verification-wrapper obligations, label handling and the need to compare training volumes and costs carefully. Its strongest direct relevance is to evaluating LLM agents that write proofs: successful verifier invocation must be tied to a fixed intended theorem, and benchmark gains require checks beyond accepted proof labels. The paper explicitly notes proof-generation failures, Liquid Haskell/reflection limitations, partiality/nontermination and the gap to low-level, stateful and memory-manipulating programs (§8). There is no Verus, Rust, TLA+ or distributed-protocol experiment. Applying these ideas to distributed verification is a reader inference. The record claims a whole paper and selected static-source read, not a fresh proof, experimental reproduction, exhaustive repository audit, historical configuration recovery or verification of every generated item.
- limits: checker-semantics/inputtypes/termination/reflection/currentwrapperdoesnotfixexpectedtheorem/expectedpairmatchingnotcomputecontrol/smallmixedablations/currentpinnotauthenticatedhistoricalrun
- how much was read: most of it read
- source
- record id: improving-llm-code-reasoning-2026
Integrating Symbolic Execution with LLMs for Automated Generation of Program Specifications (2026)
- what: # Integrating Symbolic Execution with LLMs for Automated Generation of Program Specifications (authored by agents unless marked 🧑) Yang, Ma, Wang, Xu, Cao, Zhan, Li and Gu present SESpec, a pipeline that combines QCP symbolic execution, LLM proposals and Frama-C checking to generate C/ACSL loop invariants and function contracts. Its main evidence is a benchmark evaluation, not a new soundness or completeness theorem. The authors seek specifications “as strong and informative as possible” (§1, p.2, Q2); the experiments measure syntax, invariant validity and sufficiency for supplied or masked goals. Those measurements do not establish that every accepted contract completely characterizes a program. This read covers the 27-page arXiv:2506.09550v4 dated 20 January 2026, initially submitted 11 June 2025. The PDF says “Manuscript submitted to ACM” and prints a placeholder DOI (Q1, Q47; saved arXiv history). The paper does not establish an accepted venue. Its linked repository now resolves to anon-hiktyq/TSE2026-SESpec; that name is not publication evidence. ## Method and assumptions (authored by agents unless marked 🧑) The input is C code with optional verification goals and potentially designer-supplied preconditions. The default precondition initializes and constrains reachable memory locations; the flattened memory model represents primitive locations and tracks validity, separation and aliasing. Other requirements are left to users (§§2.1, 3.1, Q6, Q8). Therefore a successful generated contract remains conditional on those input assumptions. It does not recover designer intent or establish that every caller satisfies the assumptions. For loop-free segments, symbolic execution constructs a disjunction of path conditions and symbolic stores, which the paper describes as the strongest postcondition under the chosen precondition (§3.1, p.8, Q8). Calls are processed bottom-up and their generated summaries are reused. At a loop, a single-iteration analysis identifies unchanged and non-inductive variables; the remaining variables receive inductive templates. Five template forms describe unchanged values, skipped loops, non-inductive updates, inductive updates and verification goals (§§3.2–4.3, Q9–Q13). LLMs fill ACSL placeholders using this context, with error-specific prompts for repair, weakening, adjustment, strengthening or regeneration (§4.4, Q14–Q15). The symbolic guidance has an explicit exception: nested loops are “processed purely via LLM” without the outer-loop preconditions and templates (§4.2, p.11, Q12). Recursive functions, library functions and system calls are outside the current supported scope (§6.2, Q22). Supporting singly linked data structures is distinct from supporting recursive function calls. Definition 1 checks initiation, preservation and Inv ∧ ¬B ⇒ Q. The last is called “Termination,” but states what follows if the loop exits (§4, p.10, Q10). It does not prove that the loop eventually exits. The inspected generation prompt says “Do not generate loop variant” (Q41). Algorithm 4 can reach an iteration limit and remove invalid invariants, leaving a valid subset; validity alone does not ensure that the retained subset proves the goal (Q14–Q15). The paper supplies no guarantee that arbitrary generation attempts succeed or converge. QCP supplies symbolic states and a predicate/lemma library; Frama-C checks ACSL obligations using SMT. A translator converts ACSL to QCPL and back, while the LLM sees natural language and ACSL skeletons (§5.1, Q16–Q17). The authors acknowledge that QCP “may introduce unproven lemmas that require additional Coq proofs” (Q16). They do not prove the combined translator/pipeline sound or show that every generated obligation has an independently checked Coq proof. Accepted results depend on the specified C/memory semantics, preconditions, predicate definitions, translation and verifier configuration. ## Concrete cases (authored by agents unless marked 🧑) The motivating CheckCalFun example sums up to ten array entries inside a struct and writes the checksum through a pointer. Its caller sets length to 3 and asserts equality with the first three array elements (§2, Fig.1, pp.4–5, Q4). The figure and saved benchmark input include validity assumptions, array values between 0 and 100, and length at most 10; these arithmetic and size assumptions are not all synthesized default memory conditions (Q46; figure-evidence.json). Negative length is permitted by the printed upper bound and skips the loop. SESpec’s templates distinguish that case from positive-length prefix summation and retain unchanged fields. The authors report that GPT-4o, GPT-5 and AutoSpec produced incorrect candidate annotations, including unsupported sum syntax and invariants that assume the loop is entered (Q4–Q5). This is an illustrative example, not a controlled GPT-5 benchmark. The evaluation also includes linear and nonlinear arithmetic loops, nested/multiple loops, structs and pointers, array operations, and singly linked lists. The three added datasets are numer-S, with 20 linear and 20 nonlinear loops; pIp, with 50 selected and adapted Sun Search aerospace-control cases; and list-S, with 24 singly linked-list cases derived from LIG-MM (§6.1, Q19, Q21). The pIp programs were explicitly “adapt[ed] and reformulate[d]” for Frama-C and QCP (Q19). The largest printed dataset average is 57 lines for pIp. This is evidence about selected small C functions, not verification of the complete aerospace system. ## Evaluation and measured results (authored by agents unless marked 🧑) The stated verifier is Frama-C 29.0 Copper with WP, Z3, the Typed memory model and a three-second timeout per query. The models are GPT-3.5-turbo, GPT-4o-mini, GPT-4o and Claude-3.7-sonnet, all at temperature 0.7 (§6.1, p.17, Q20). The main table reports Pass@1, Pass@3 and Pass@5. The paper does not give exact dated model identifiers, hardware, end-to-end runtime, measured token/cost totals, repeated-run variability or confidence intervals. The three rates have different meanings: syntax requires well-formed annotations; validity additionally requires semantic checks such as invariant initiation and preservation; accuracy additionally requires the verification goal (§6.3, Q23). Goal accuracy is stronger than validity but remains specific to that goal. The paper’s argument that a syntax/validity gap rules out trivial accepted invariants is insufficient: a gap shows some candidates fail, not that every accepted candidate is informative or nonvacuous. No general equivalence, maximality or specification-completeness score is reported. Table 1 reports 354/395 programs solved, about 89.62%, with dataset counts 133 SyGuS, 46 OOPSLA, 21 SV-COMP, 30 NLA, 40 numer-S, 51 Frama-C, 50 pIp and 24 list-S (§6.2, Q21–Q22). The dataset solved counts match the strongest-model Pass@5 results in Table 2: 133, 40, 16, 25, 34, 39, 44 and 23. Thus “nearly 90%” is an aggregate at that reported outcome, not a single-attempt success rate for all models. The printed category breakdown reports 197/204 linear, 41/53 nonlinear, 15/24 nested/multiple, 45/53 memory-and-loop, 56/58 iteration-free and 0/3 external/recursive-call cases. There is a counting discrepancy: the memory-and-loop cells sum to 55, not 53; the SV-COMP category cells sum to 23, not its summary 21. The dataset and category totals each print 395, while the cell matrix sums to 397. No value was silently corrected. Table 2 contains 32 model/dataset rows and 288 percentage cells, all retained in numeric-evidence.json (Q25). Representative accuracy results are: - GPT-4o: SyGuS 93.98% at Pass@1 and 100% at Pass@5; pIp 64% to 78%; list-S 54.17% to 79.17% - Claude-3.7-sonnet at Pass@5: SyGuS 100%, OOPSLA 86.96%, SV-COMP 76.19%, NLA 83.33%, numer-S 85%, Frama-C 76.47%, pIp 88%, list-S 95.83% - GPT-3.5-turbo at Pass@5: OOPSLA 52.17%, NLA 56.67%, pIp 76%, list-S 16.67%, showing substantial model dependence Some printed values need reconciliation. OOPSLA GPT-4o-mini accuracy decreases from 65.41% at Pass@1 to 43.48% at Pass@3 and 47.83% at Pass@5; syntax also decreases slightly. These do not behave as cumulative success counts would. The sampling/population explanation is unspecified. The Frama-C GPT-3.5 Table 2 accuracy is 54.17%, versus Table 3’s 51.0%; its Table 2 percentages align arithmetically with 48 cases rather than the stated 51, but that does not establish the actual denominator. The prose says GPT-4o and Claude match on numer-S, while the rows give 82.50% and 85.00% (Q24–Q25). These are reporting limitations, not independently reproduced failures. The ablation uses a stated random subset of 100 cases, 70 loops and 30 functions, caps refinement at three iterations, and says token usage is consistent (§6.4, Fig.5, Q26–Q27). It displays three configurations despite saying four: LLM alone and LLM+symbolic execution at Pass@3, and LLM+symbolic execution+refinement at Pass@1. Loop accuracy rises 28.75 → 60.00 → 87.21%; function accuracy rises 16.67 → 46.67 → 86.67%. The rows support a benefit from symbolic context and refinement on this subset. They do not show the “perfect scores across all metrics” claimed in the prose: the final loop syntax/validity are 95.71%, accuracy 87.21%. Several loop percentages are not integer fractions of 70, with no averaging or denominator explanation. No measured budget totals substantiate exact token equivalence, and the model used for this ablation is not identified in the paper. Table 3 compares 13 methods/model configurations over eight datasets, mixing cited and author-reproduced values marked by gray shading (Q28; figure-evidence.json). Stronger-model SESpec has clear gains on pIp and list-S. Broad dominance does not hold across configurations: SESpec-3.5 loses to AutoSpec-3.5 on OOPSLA, SV-COMP, NLA, numer-S and Frama-C; SESpec-4o ties ACInv-4o on OOPSLA and SV-COMP. Specialized HOLA scores 93.5% on OOPSLA versus SESpec-Claude’s 87.0%, and CLAUSE2INV scores 93.3% on NLA versus 83.3%. The authors’ causal explanations about model reasoning and baseline limitations are interpretations, not controlled causal measurements (Q29–Q31). The masked-goal experiment uses SESpec GPT-4o at Pass@1 and AutoSpec’s own configuration (§6.5, Fig.6, Q32–Q33). SESpec accuracy falls from 93.98% to 80.45% on SyGuS, and from 70.83% to 64.71% on Frama-C. AutoSpec falls from 85.71% to 57.89%, and 60.78% to 29.41%. These are decreases of 13.53/6.12 and 27.82/31.37 percentage points respectively. The Frama-C unmasked 70.83% differs from Table 2’s GPT-4o Pass@1 66.67%. This experiment supports useful generation when the goal is hidden, assessed against that goal afterward; it does not prove complete goal-independent semantics or compare identical model and sampling budgets. ## Threats, artifacts and relevance (authored by agents unless marked 🧑) The paper’s contamination assurance is too strong. Section 7 says it avoids “few-shot prompting” and concludes that outputs are grounded in program semantics “rather than in prior exposure to benchmark-related data” (Q34). Section 5.2 explicitly supplies two public array/list examples to calibrate inductive predicates (Q18), and Figure 4’s prompt includes example guidance. Avoiding fine-tuning does not establish the pretrained models never encountered these benchmarks. No contamination audit is reported. This is an unresolved assurance, not evidence that leakage actually occurred. SpecGen is excluded because it targets Java/JML and a different custom dataset (§7, Q35). The author repository was inspected at commit da17c126b159a06a5d1fecde5311737811a73145, retrieved 19 October 2026. The original URL redirects to TSE2026-SESpec. The recursive root tree is truncated, so a separate complete src tree was obtained; only metadata, README and 13 selected source/config/prompt/input files were read. Those files contain 1799 logical lines. Stored RESULTS, output programs, serialized vector databases and experiment spreadsheets were not loaded. No supplementary appendix was recovered in the inspected root/src listings; this record claims a whole read of the paper PDF, not an unseen appendix. Two concrete source differences limit reproducibility. The paper specifies three seconds per WP query, but both inspected verifier wrappers actively set ten seconds, with three-second commands commented out (Q38–Q39). The default-precondition code’s dynamic-array branch assumes the next parameter is length and adds length > 0 && length < 100 (Q40). Those bounds are stronger than memory safety alone for arbitrary safe arrays. Neither observation identifies what the historical experiments used. The default function config enables use_db and disables think; the loop config disables both. These snapshot switches do not prove retrieval was used in reported runs (Q42–Q43). The exact experimental revision/configuration is not pinned by the paper. The contribution to the requested topic is direct evidence for LLM-assisted specification writing: provide symbolic state and typed annotation templates, separate validity from goal strength, and use verifier feedback to refine candidates. It supplies numerical and pointer/data-structure benchmarks and a masked-goal evaluation. There is no distributed protocol, Verus, verified Rust or TLA+ experiment here. Transfer to agents writing distributed-system specifications or proofs is a reader inference: retain the assumptions, the exact verifier obligation, the translation boundary, and independent strength checks; do not equate successful annotation generation with a complete system proof. Read every line of the 1202-newline layout extraction, all 27 PDF pages, all 38 references, three tables and six figures. Viewed nine contact sheets and fullsize pages 5, 15, 17, 19, 20 and 21. The local and official v4 PDFs are byte-identical. The bundle preserves literal excerpts with page/line/character anchors, all table/plot values, raw hashes and reader-derived discrepancies. Only reader extraction, rendering, hashing, arithmetic and validation scripts were run. No author code was executed or imported, and no compiler, verifier, solver or prover was run. All experimental outcomes remain author-reported, statically inspected results.
- limits: C/ACSL, QCP symbolic execution, Frama-C/WP/Z3 and Typed memory semantics, generated or designer-supplied preconditions. Exact strongest postconditions apply to loop-free segments; LLM loop abstractions are checked for validity and optional goal sufficiency. No complete functional-summary, termination, translator-soundness or end-to-end Coq theorem. Nested loops lack the outer-loop template guidance; recursive/library/system calls unsupported. Reporting inconsistencies and current artifact differences are retained.
- how much was read: most of it read
- source
- record id: integrating-symbolic-execution-with-2026
INVWEAVER (2026)
- title: INVWEAVER: Deductive Feedback for Invariant Synthesis in Interacting-Loop Programs
- what: Presents INVWEAVER, a neuro-symbolic loop-invariant synthesizer for nested and sequential loops. A loop-level call graph exposes dependencies; obligation-guided LLM prompts and WP-derived targets drive iterative repair with delayed filtering. Defines state-transition and verification-dependency edges in the LCG, top-down/boundary-inward scheduling, failure diagnosis scopes, and a cycle-length delayed-filtering rule. Bubble-sort case derives missing inner invariants from outer WP obligations. Evaluates 67 prior plus 85 CLRS-Alg programs, comparing seven systems and ablations.
- number: 72/82 multi-loop; 68/70 single-loop
- number: 13 multi-loop instances uniquely solved
- number: GPT-5.5 ablation full 140 vs no OGI 117 and no WP 110
- limits: Uses ACSL/Frama-C WP and SMT solvers; dynamic allocation and separation logic are unsupported, making pointer structures difficult. Benchmarks are small and may leak into LLM training; GPT/Qwen/DeepSeek results depend on model and timeouts.
- how much was read: most of it read
- record id: invweaver-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
KaPilot (2026)
- title: KaPilot: LLM-Assisted Generation of Kani Specifications for Unsafe Rust Verification
- what: Five cooperating LLM agents write Kani contracts (preconditions, postconditions, loop invariants) for unsafe Rust functions, using the function’s documentation instead of its code as the source of what must hold. Kani is a bounded model checker: it checks all inputs up to a size bound.
- number: GoldSet (54 functions from verify-rust-std, with human-written contracts): 88.9% of functions got a contract Kani accepts; 57.4% of contracts equal to or stronger than the human ones (GPT-5: 31 good, 17 bad, 6 failure)
- number: ULSet (70 functions from popular crates, no reference contracts): 71.4% got an accepted contract (GPT-5: 50 pass, 20 failure)
- number: Versus AutoSpec adapted to Kani, same GoldSet and GPT-5: 31 vs 17 good, 6 vs 14 failures
- number: Ablation on GPT-5: dropping SafetyReq cut good from 31 to 6; naive prompt with Kani feedback (10 rounds) gave 8 good, 26 failures
- limits: Only memory safety and panics, not functional correctness. Kani is bounded, loop invariants only for while loops, and some Rust properties (lifetimes) cannot be written in Kani. Judging whether an accepted contract is good was done by hand; no automatic check exists. Output quality depends on documentation quality (ULSet docs shorter, failure 28.57% to 31.43% vs 7.41% to 20.37%).
- how much was read: most of it read
- source; notes: KaPilot (2026)
- record id: kapilot-2026
KBSpec (2026)
- title: KBSpec: LLM-driven Formal Specification Generation with Evolving Domain Knowledge Base
- what: It keeps a growing knowledge base, built from official documentation and from verifier feedback, to help generate and repair JML specs.
- number: GPT-5.2 KBSpec PR 73.96% vs SpecGen 41.63% (+32.33 points); fail rate 13.45%
- number: PR improvements over SpecGen: +19.17 points GPT-5-mini, +14.73 Claude-Sonnet-5
- number: C@All gains over SpecGen: +11.85, +10.04, +8.71 points respectively
- number: Passed completeness [0.5,1]: KBSpec 269 vs SpecGen 206 GPT-5.2; [0.75,1]: 177 vs 157
- limits: A knowledge base built from verifier successes can also store weak contracts. According to the notes, it is not independent evidence that specs are complete.
- how much was read: most of it read
- source; notes: Generated contracts and independent evaluation
- record id: kbspec-2026
Kiro (2026)
- title: Kiro specs (Analyze Requirements; Correctness with Property-Based Tests)
- what: Kiro works as a pipeline. An LLM refines requirements into EARS-style criteria and translates them to SMT-LIB. A solver checks consistency and completeness. For an ambiguity test (“semantic entropy”), it samples several formalizations and groups them by logical equivalence. Depending on how much they differ, it trusts one, discards them, or asks the user.
- limits: It is a product blog. It gives no accuracy numbers for Kiro’s own method.
- how much was read: most of it read
- source; notes: Additional tools, not counted as papers
- record id: kiro-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: Repository benchmarks: 183/359 tasks (51.0%) vs 4.5% multi-round prompting baseline
- number: Single-file: 251/313 (80.2%) vs AutoVerus 178/313 (56.9%) and AlphaVerus 78/313 (24.9%); 43.2% of AutoVerus tokens
- number: Ablation CortenMM 52 tasks full, 10 without code metadata, 7 without lemma knowledge, 22 without Verus knowledge
- 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
Lean-Agent Protocol (2026)
- title: Type-Checked Compliance: Deterministic Guardrails for Agentic Financial Systems Using Lean 4 Theorem Proving
- what: Proposes a gateway that turns English financial policies into Lean 4 statements (using Harmonic’s Aristotle model) and blocks any trading-agent action that Lean cannot prove compliant. It is a design and regulatory argument; the paper reports no experiment on its own system.
- number: Cites AWS Cedar: Lean model evaluates a differential-test input in 5 microseconds on average vs 7 microseconds for the Rust code (from an AWS blog, not measured by the authors)
- number: Proposes a 3-phase rollout: shadow mode, WebAssembly-sandboxed interception, enterprise scale
- limits: No evaluation of translation accuracy, latency or blocked actions on the authors’ own system; the claimed ‘microsecond latency’ and ‘compliance certainty’ come from other people’s results and from argument. The paper itself names the English-to-Lean translation step as the main weak point.
- how much was read: most of it read
- source; notes: Type-Checked Compliance (2026)
- record id: lean-agent-protocol-2026
Lean4Agent FormalAgentLib and LeanEvolve (2026)
- title: Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory
- what: Presents Lean4Agent, a Lean4 dependent-type framework with FormalAgentLib for structural, semantic and execution-trajectory verification of LLM-agent workflows, plus LeanEvolve for verification-guided workflow refinement. Workflows are typed heterogeneous graphs of read/write variables, natural-language instructions and execution types; trajectories record pre/post states and reasoning/tool traces. Layer 1 checks node reachability, edge validity and read/write consistency. Layer 2 translates explicit and implicit variables into decidable predicates and graph-level information-flow/context predicates, proving precondition entailment under an LLMExec local-correctness assumption. Layer 3 checks concrete trajectories using Lean propositions, Python validators and LLM-as-judge, localizing failed steps. LeanEvolve feeds diagnostics and optional test feedback to an LLM for targeted workflow edits, with a pure-LLM exploratory mode. Experiments generate 40 workflows, compare verification-passing/failing workflows across five LLMs on 50 hard SWE-Bench-Verified tasks and 100 ELAIP-Bench questions, and study graph-predicate and pure-LLM ablations.
- number: Layer-2 passing workflows improve SWE task rate by 14.80 percentage points (95% CI 10.00–19.60)
- number: ELAIP passing workflows improve by 9.07 points (95% CI 5.66–13.07)
- number: LeanEvolve adds 7.47 points on SWE, raising 56.93% to 64.40%
- number: formal-guided evolution solves 7.00 points more initially failed ELAIP cases than pure-LLM evolve
- limits: Layer-2 soundness depends on LLMExec: each step satisfying predicates is assumed to produce postconditions; this abstracts away failures of long-horizon black-box LLM behavior. Custom predicates may have only name existence and natural-language explanations, and trajectory checks can rely on an LLM judge. Evaluation uses small random subsets (50 SWE and 100 ELAIP), 40 generated workflows and contemporary model versions, so generalization and causal effects are limited. The paper is a preprint and reports no mechanized verification of the LLM internals or distributed-system protocols.
- how much was read: most of it read
- source; notes: ## Lean4Agent (2026)
- record id: lean4agent-formalagentlib-and-leanevolve-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
- 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: 364 total proofs (298 SV-COMP, 66 NTP4VC)
- number: 26.8% improvement over AutoRocq, 51.7% over Copra
- number: 78 unique successes; 61/69 helper-lemma proofs use BRIDGE strategy
- 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
- record id: lemmanet-2026
LIFT loop-bound termination verification (2026)
- title: LLM-Guided Loop Bound Generation for Program Termination Verification
- what: Introduces LIFT, a guess-and-check termination framework in which LLMs generate conjunctive or lexicographic loop bounds and a formal validator proves them or refutes them. A candidate bound b(V) is converted to a safety query by adding a counter initialized with b and asserting cnt>0 at each loop head. Constant bounds use bounded unrolling; symbolic bounds use ICE-DT or LLM invariant learners plus Boogie/SMT. If invariant proving fails, bounded violation analysis searches for a reachable counterexample state and feeds it back, while timeout and syntax diagnostics steer later prompts. Progressive generation starts with simple conjunctive bounds and escalates to lexicographic tuples; constant-offset correction and k-induction are included.
- number: 171 benchmarks
- number: 152 solved with Gemini
- number: 139 solved with DeepSeek
- number: 19 unsolved
- limits: A valid over-approximate loop bound implies termination, but bounded violation analysis can miss violations after depth m and then treats the witness as potentially spurious. The framework is presented for one loop and says it generalizes to multiple loops. It relies on LLM inference, ICE-DT invariant quality, Boogie/SMT arithmetic, fixed iteration/time budgets, and syntactic restrictions excluding division/nonlinear operators. Nineteen of 171 benchmarks remain unsolved: ten lacked precise bounds and nine exceeded validator capability.
- how much was read: most of it read
- record id: lift-loop-bound-termination-verification-2026
LLM ACSL evaluation (2026)
- title: Evaluating LLM-Generated ACSL Annotations for Formal Verification
- what: Empirically compares a rule-based Python annotator, Frama-C RTE, and DeepSeek-V3.2, GPT-5.2 and OLMo 3.1 32B for one-shot ACSL generation on filtered CASP C programs, checking annotations through Frama-C WP and multiple SMT solvers. Uses 355 retained programs from the 506-file CASP dataset, evaluates EVA preprocessing and hundreds of WP runs per source/solver, and reports proof success, solver timeouts and Qed time. It finds rule-based and RTE annotations more reliable; DeepSeek is the strongest LLM but remains variable and can produce weak contracts.
- number: 355 retained files from 506; 151 excluded
- number: EVA successfully analyzed 40.8%
- number: RTE mean proof success about 99.1%
- number: DeepSeek mean success about 93.8–94.9%
- limits: One-shot default decoding is used without iterative feedback or fine-tuning. The filtered dataset excludes 151 empty/incomplete files and focuses on C programs in CASP; proof success can overstate usefulness because annotations may be trivially true or overly conservative. Results vary substantially by solver and do not establish generalization beyond this benchmark.
- how much was read: most of it read
- source; notes: ## ACSL annotation evaluation (2026)
- record id: llm-acsl-evaluation-2026
LLM logical-construct study (2026)
- title: Beyond Basic Specifications? A Systematic Study of Logical Constructs in LLM-based Specification Generation
- what: Compares LLM-generated ACSL annotations for 49 C programs, checked with Frama-C, under four settings of allowed constructs: basic, proved lemmas, axioms, and all. Failing annotations are fixed by deleting or modifying them.
- number: 49 programs, 5 runs each; stable = at least 2 of 5
- number: GPT-5 NVP/stable: deletion basic 32/28, full 40/39; modification basic 39/37, full 42/41
- number: Gemini modification verifiable NVP 48, stable 46
- number: modification raises runtime generally over 100%
- limits: The annotations come from the code, not from requirements. Axioms are assumed true and can make the proof unsound, and nothing audits them. NVP counts a program as solved if any run solved it, not pass@1 (success on the first try).
- how much was read: most of it read
- source; notes: Beyond Basic Specifications? A Systematic Study of Logical Constructs
- record id: llm-logical-construct-study-2026
LORIS loop invariant synthesis (2026)
- title: Guiding LLM-based Loop Invariant Synthesis via Feedback on Local Reasoning Errors
- what: LORIS iteratively synthesizes C loop invariants: an LLM proposes an invariant, writes a natural-language proof of failed verification conditions, another LLM translates local steps into first-order implications, and Z3 checks those implications to produce targeted feedback. The framework checks local reasoning steps rather than demanding a fully formal proof script, maps an invalid implication back to a specific natural-language error, and feeds that diagnosis into subsequent invariant synthesis. It integrates Frama-C for inductiveness, Z3 for implication validity, and evaluates multiple model families against LaM4Inv and Clause2Inv, including a BMC combination study and manual auto-formalization checks.
- number: GPT-4.1 LORIS solves 445/460 main programs with 93.1% success, versus 84.6% and 84.9% baseline success rates
- number: best reported non-linear result is 47/50 programs; GPT-4.1 LORIS solves 45/50 at 83.2% success
- number: five runs produce 2,300 attempts on the main suite; per-run cap is 150,000 tokens and 600 seconds
- number: successful GPT-4.1 run costs about 50 per problem, about $300 f or B 6 an d ab o u t$ 1000 for A5
- number: A5 took 2040 minutes and 3263 lines of Lean; B1 took 55 minutes and 328 lines
- number: Brascamp-Lieb: more than 8,000 lines of Lean in under two weeks, about 70 new definitions, lemmas and theorems added by the agent
- number: On B4, iterative refinement of informal proofs finished in 5 rounds; independent sampling failed in 10 rounds
- limits: Formal-checking trust is relative to Lean,the exact formal statement,imported libraries and harness. Putnam uses Seed-Prover1.5 formal statements and disabled online API search,but existing library retrieval is enabled. No artifact or proof certificate was independently checked by this reader;supplied AppendixA statement ends by sorry and AppendixB lemma has no proof body. Twelve Putnam problems plus selected six-problem ablations are small evaluations. No multiple-run variance,random seeds,confidence intervals or standardized hardware/API latency accounting is provided. Inter-system timing/line comparisons are reported values,not demonstrated matched-compute causal comparisons. Default budget approximately $50/ p r o b l e mi sr ai se d t o$ 1000 A5 and1229, 1 week/ $583, 2 w ee k s /$ 1580; about a month 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: 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
- 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: 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: # Whole-paper read: Automatic Generation of Formal Specification and Verification Annotations Using LLMs and Test Oracles (authored by agents unless marked 🧑) João Pascoal Faria, Emanuel Trigo, Vinicius Honorato, Rui Abreu. arXiv 2601.12845v1, 19 January 2026, 37 pages. The title-page footnote says “Preprint. Intended for submission to Science of Computer Programming.” Treat this as a preprint; the inspected version supplies no acceptance claim. [Q1, Q2] The paper measures LLM generation of annotations for existing conventional Dafny programs: pre/postconditions, loop invariants, auxiliary predicates/functions, and assertions/lemmas. Its principal result is empirical: a Claude Opus 4.5/GPT-5.2 combination with verifier feedback solves 108/110 benchmark programs. It supplies a benchmark, prompts, repair/minimization workflow and IDE assistant. It does not prove that test-derived contracts completely express natural-language intent. The most useful contribution to evaluating proof agents is the distinction between a verifying program and an adequate contract. [Q3, Q20, Q30, Q46] ## What is checked The input retains implementation code, natural-language comments and outcome-checking test assertions while stripping formal annotations and helpers. Dafny 4.11.0 checks generated/postprocessed outputs with a one-minute timeout. Calls inside tests use the method contract and ignore its body: “These static test cases therefore act as specification-level oracles.” Thus a weak postcondition may allow the implementation to verify yet fail the caller’s assertion. For a tested input x and acceptable-output assertion R(y), §8.2 spells out P(x) ∧ ∀y.(Q(x, y) ⇒ R(y)). This constrains that input and permitted outputs under the generated contract. It does not establish correctness of a contract on untested inputs. Verification also depends on Dafny’s translation, SMT reasoning, trusted semantics and any retained/provided helper definitions. No new verifier-soundness theorem is given. [Q12, Q13, Q4, Q46] The direct and repair prompts were designed iteratively, with generic patterns and recurring fixes; no separate held-out prompt-design evaluation is described. Prompts prohibit implementation changes, unproved assume statements, decreases* and removal of test assertions. Postprocessing repairs formatting/placement issues such as misplaced invariants. These are guardrails, not a demonstrated enforcement theorem: §6.5 says “generated solutions should be manually inspected.” In the inspected generator acceptance path, success follows verification; I found no mechanical comparison enforcing unchanged original implementation there. That is a limited static observation, not evidence that a reported solution cheated. [Q8, Q9, Q37, Q51, Q59] ## Dataset and experimental protocol TESTDAFNY110 combines 85 refined loop-based MBPP-DFY programs, 15 LOOPINV100 academic/numerical/search/sort examples, and 10 new programs intended to reduce prior exposure. Selection excludes duplicates and cases solved trivially without loops. Table 1 totals 2505 original LOC, 1211 annotation LOC and 188 proof-helper annotations across 110 programs; 56% of programs require helpers. All eight category rows are transcribed in numeric-evidence.json. This is a collection of small-to-moderate algorithmic exercises, not a distributed implementation benchmark. [Q5, Q6, Q7, Q8] Direct prompting makes up to 5 independent attempts, stopping at success. Repair starts with a direct attempt and allows up to 9 feedback repairs, 10 attempts total. Models are Claude Opus 4.5 (claude-opus-4-5-20251101), GPT-5.2 (gpt-5.2-2025-12-11, reasoning none/low), DeepSeek-V3.2 chat and GPT-4 (gpt-4-0613). Claude is tried at temperatures 0.5 and 0; DeepSeek/GPT-4 at 0.5; the paper describes GPT-5.2 as fixed T=1. The multimodel method runs Claude T=0.5 and GPT-5.2 low in parallel each round, choosing syntax validity, verification, fewer LOC, then shorter verification time. Consequently one multimodel attempt can entail two API calls. pass@k/repair@k mean the empirical percentage of these 110 problems solved within the specified budget; no combinatorial pass@k estimator is used. [Q12, Q13, Q14, Q15] The experiments ran on an Intel Core Ultra 7 258V @2.20 GHz, 8 cores, 32 GB, Windows 11 Pro. Table 2 gives average cost/time per API call and extra program LOC among successful attempts. These are not task-total cost or end-to-end latency. There are no reported confidence intervals or repeated complete-dataset evaluations. The initial success rates differ between direct and repair runs; the strategies also have unequal budgets, so their difference is not a paired causal estimate of feedback alone. [Q16, Q17, Q12, Q13] ## Measured results Section 6.1 says the multimodel approach solved “98.2% of the problems within at most 8 attempts (repair@8)”. This is 108/110; the abstract instead calls them 8 repair iterations. I use the body’s attempts, which include the initial generation. The two failures are FastModularExponentiation and PrimeFactorization, with 4 and 10 manual lemmas. The downloaded manual files contain those corresponding lemma sets; the latter file is named PrimeFactors.dfy. No independent replay was performed. [Q20, Q18, Q70, Q71] All 14 Table 2 rows are retained. At budgets 5/10, the multimodel repair rates are 94.5%/98.2%, versus 57.3% for direct@5. Claude T=0.5 repair reaches 90.0%/96.4%; GPT-5.2 low 75.5%/89.1%; GPT-5.2 none 60.0%/70.0%; DeepSeek 62.7%/69.1%; GPT-4 30.9%/34.5%. Multimodel repair averages 7.86 US cents and 28.5 s per API call; Claude T=0.5 averages 4.41 cents and 15.8 s. DeepSeek is cheapest at 0.07 cents/call; GPT-5.2 none’s repair response time is 9.1 s. These are author-reported run prices/times, not current provider quotations. Table 2 labels the averages per API call; multimodel costs approximately sum the constituent entries, so whether its unit is a provider call or combined round remains unclear. No task-total cost is inferred. [Q17, Q22, Q15] Repair outputs have 63.2% more total program LOC than manual counterparts. Minimization removes 58% of annotation LOC and reduces total-program overhead to 10.6%, averaging 1.4 s/line removed. Those percentages use different denominators. It greedily tries generated-segment deletions subject to verification, using source alignment and dependency information; it does not establish a globally minimum proof. Appendix B uses 10 s for deletion checks; the current downloaded implementation instead starts at 5 s and adaptively caps at 30 s. Keep snapshot defaults separate from original experiment settings. Main verifier tasks average 9.7 s, or 1.9 s excluding timeouts. [Q21, Q52, Q53, Q65, Q64, Q66] Figure 6 pools all generation attempts, including failed repair rounds. For example, multimodel outcomes are 37% success, 32% incomplete, 25% potentially incorrect, 6% timeout and 0% syntax error. These are not eventual per-program success rates. “Incomplete” means that merging with the manual solution then verifies; the paper acknowledges this heuristic can undercount incomplete outputs. “Potentially incorrect” denotes remaining verification failure, not a demonstrated semantic bug. All five plotted distributions are preserved, including rounding. [Q24, Q25] ## Contract quality and concrete tests The manual contract comparison is separate from the headline solve rate. It covers all 110 programs: 108 selected first verified solutions after minimization, plus the first Claude output for each of the 2 unsolved cases. Authors judge 106/110 (96.4%) logically equivalent to expert pre/postconditions. No independent equivalence prover or inter-rater assessment is described. The four mismatches are one stronger postcondition and three weaker preconditions, all compatible with the implementation. Table 3’s nine category counts and their distinct denominators are preserved. [Q30, Q33] BinarySearch’s found/missing/duplicate tests require a result of 1 or 2 on [1, 4, 4, 6] when searching 4. Individual duplicate indices and an unsorted input appear as expected-failure tests. LinearSearch makes the central adequacy issue concrete. Clauses a+b permit results below−1; adding c sets −1≤index<length and makes the positive tests provable. Adding d requires the first occurrence, stronger than the natural-language request for an occurrence. The positive assertion k==0||k==3 cannot reject that stronger contract. An expected-nonprovable assert k==0 can expose it. MaxDistEqual illustrates the opposite: the intended input is nonempty, but the implementation safely handles empty arrays and generated preconditions omit that restriction. CountDistinct illustrates a different quality dimension: a recursive count mirroring the loop is less declarative than set cardinality despite expressing the same result. [Q10, Q32, Q33, Q31, Q67, Q72, Q73] After manual discovery of the four mismatches, authors add expected-failure tests and regenerate successfully for all four using Claude. This followup must not be folded into the original success rate or described as the original positive suites automatically detecting every intent mismatch. Negative tests are checked by uncommenting one at a time and rejecting the candidate if it verifies. Failure to prove such a test is not generally a semantic proof that its assertion is not implied: helpers, incomplete SMT reasoning and timeouts can also cause failure. [Q34, Q58] A further manual inspection finds 7 of 165 failed Claude repair attempts where method bodies verify but tests fail from weak/missing postconditions. This establishes useful detections in a selected failure sample. It is not a controlled ablation of test oracles and does not measure a general defect-detection rate. [Q35] ## Regression and contamination claims A logistic model uses original LOC, annotation LOC, proof-helper count and configuration intercepts over 1540 program/configuration pairs. Authors report βL=−0.0735, βA=−0.0475, βH=−0.5825, all Wald p<0.001, pooled AUC=0.907 and per-configuration AUC=0.80–1.00. These are conditional associations with predictors in different raw units. They do not measure causal helper difficulty or establish generalization. The saved analysis script fits on long and predicts on the same long data before computing both AUC summaries. Thus these are in-sample discrimination measures, despite §6.3’s phrase “generalizes across models.” [Q26, Q28, Q29, Q27, Q60, Q62, Q63] Each program appears 14 times; the paper does not describe correction for this dependence. The current artifact does contain program-clustered standard-error code and a random-intercept exploratory fit. I did not run it or inspect statistical outputs, so cannot establish whether the paper’s significance claims survive that correction. The script’s mixedlm call is a general linear mixed model, not logistic mixed regression. [Q61] Adding subdataset indicators gives χ²(2)=0.79, p=0.67, AUC 0.907→0.908. Authors interpret this and older GPT-4’s 29.1% versus GPT-5.2 none’s 36.4% direct@5 as evidence of low contamination risk. The inference remains uncertain: a nonsignificant dataset factor with only 10 new problems cannot prove absence of exposure, while model capability and age change along with possible exposure. No copying was observed in the authors’ manual comparison, but that is not a training-data audit. [Q29, Q23, Q39, Q5] ## IDE and user study The assistant adds pre/postcondition and invariant commands with diagnostic feedback, retries and provider fallback. Downloaded command/prompt sources corroborate that workflow; they are a current snapshot, not established as the original study build. Seven master’s students with six weeks’ Dafny experience perform six tasks: Catalan numbers, primality, recursive minimum, heap checking, selection sort and reversal. Groups of 4 and 3 use opposite tool/manual assignments, with 15 minutes per task and one hour overall. Authors report 85.7% versus 42.1% success, 6.2 versus 11.1 minutes, and SUS 74.6/100. [Q40, Q41, Q74, Q75, Q42, Q43] These are small-sample descriptive results without confidence intervals or significance tests. The assignments imply 21 tasks per condition, but 42.1% cannot equal an integer success count out of 21 rounded to one decimal. The study artifact’s questionnaire offers Did not try, Partial and Hybrid responses and time bins, so exclusions or a different denominator may explain it; neither the inspected protocol nor questionnaire specifies the aggregate denominator or averaging rule. Do not infer 8/19 as fact or call the reported rate erroneous. Time censoring, completion population and tool-versus-hybrid classification remain unclear. [Q42, Q43, Q76] ## Contribution to this collection This is direct evidence for LLM agents writing specifications and proof annotations in Dafny, with explicit repair budgets, mechanically checked test assertions, proof-helper failures and proof minimization. It supplies concrete cases where verification succeeds under an intent-mismatched contract and separates empirical verification from manual adequacy judgments. These are useful evaluation lessons for future Verus/verified-Rust or distributed-system proof agents, but that transfer is my inference. The paper has no Verus, Rust, TLA+ or distributed-system experiment. Related-work comparisons, including 87.5% pass@5 versus 100% repair@6 on 64 overlapping tasks, change models, budgets and helper permissions; they are attributed comparisons, not controlled superiority experiments. The claim of loop invariants for all 110 programs also differs from full annotation success for 108. [Q3, Q30, Q47, Q44, Q48, Q49] ## Read and source scope Read all 37 pages, §§1–9, acknowledgments, AI declaration, both Appendix A prompts, Appendix B algorithm and 37 references. Inspected 37 page renders/19 contact sheets, including 11 figures and 3 tables. Read primary artifact sources statically at the scope recorded in source-scope.json, including all manual examples above, the entire regression script and study-artifact text; larger generator/minimizer/IDE files were inspected in selected ranges. Downloads are pinned by blob/tree identities and hashes with fetch dates. The current snapshot is not asserted to be the exact experiment checkout. No author code, compiler, checker, prover or solver was executed; no experiment spreadsheets, serialized results or models were loaded. Exact literal excerpts with section, page, line and character anchors are in quotes.json and combined.quote-source.txt. Reader deductions and author measurements remain separate in reader-diagnostics.json and numeric-evidence.json.
- 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: Existing conventional Dafny implementations, natural-language comments, chosen static positive/negative tests, Dafny 4.11.0, SMT reasoning, helpers and timeouts. Fixed 110 algorithmic programs; modular tests constrain selected inputs, not globally complete intent. Manual equivalence judgment, in-sample AUC and unclear user-study denominators. No distributed/Verus/Rust/TLA+ experiment.
- how much was read: most of it read
- source; notes: Automatic Generation of Formal Specification and Verification Annotati
- 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+-Bench (2026)
- title: TLA+-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA+ Specification Generation
- what: TLA-Bench has TLA+ specs, each with a model-checker config and English descriptions. A model reads the description and writes a spec. TLC (the TLA+ model checker) runs it against the reference config. A pass means the spec parses and no listed property is violated.
- number: 403 model-checked gold and 897 parse-only silver specs from 13 public repositories
- number: on one fixed set of 300 outputs the correct rate moves from 10.0% to 1.7% depending on grading choices; 18.7% to 1.7% if the model is told the config’s names
- number: best model is correct 16% of the time by default and 26% given the interface names; open models at most 1%; best model parses 87%
- number: 12 of 30 passes meet the non-vacuity bar, so the plain correct rate overstates capability about 2.5 times
- limits: The descriptions are written by a model, not by practitioners. Composition and refinement are under-represented. The paper makes no claim that controls for contamination. A pass is exact only relative to the reference config. It does not prove that the spec reproduces the reference behavior. The notes’ later pass says the benchmark creators wrote the descriptions and the grading oracle.
- how much was read: most of it read
- source; notes: TLA+-Bench
- record id: tla-bench-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: Baseline 8.6% TLC model-check; TLA-Prover 9/30=30% Gold and Diamond
- 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
- record id: tla-prover-2026
TLA-Prover benchmark (2026)
- title: TLA-Prover repository benchmark documentation
- what: This repository documents a harness for checking whether LLMs produce and repair TLA+ that pass SANY and non-vacuous TLC. Its README freezes corpus/holdout gates and reports audited model results, including false passes caused by weakened or deleted properties.
- number: 206 specs in the corpus; 30-spec holdout
- number: Post-audit model-only repair 166/206; W4-diamond-gold post-prompt-fix 16/30 pass@32
- limits: Repository status is dated and reports were not rerun; results are self-reported in repository artifacts.
- how much was read: most of it read
- source
- record id: tla-prover-benchmark-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
- record id: tla-verus-2026
TLAi+Bench (2026)
- title: TLAi+Bench repository
- what: TLAi+Bench evaluates LLMs on natural-language-to-TLA+ puzzles and real-world scenarios with reference specifications and GenAIScript generation/verification utilities.
- number: Nine named puzzle categories/files are listed in the README; six gold reference modules are shown.
- limits: The current repository emphasizes puzzles and examples; repository status and task coverage can change.
- how much was read: most of it read
- source
- record id: tlai-bench-2026
TLAPS-Bench (2026)
- title: TLAPS-Bench repository
- what: TLAPS-Bench asks AI agents to prove invariants of TLA+ protocol/system specifications in a sandboxed runtime. Its current problem set includes ZooKeeper, etcd and HashiCorp Raft, MongoDB transactions and other protocols.
- number: Current problem set: 9 specs and 57 invariants
- number: Retired/next lists include Byzantine Paxos, broadcast, Paxos, 2PC, termination detection and WAL protocols.
- number: 9 specs and 56 proof targets (FLASH 15, ZooKeeper 9, etcd Raft 8, HashiCorp Raft 6, others)
- limits: The README says retired proofs are available by contact and current runs focus on a few hard tasks; no agent run was reproduced.
- how much was read: most of it read
- source
- record id: tlaps-bench-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
- 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 0.61/task for VeruSyn versus 54% for Sonnet at 2.07program-translation cost (about $0.02/ f i l e), 17.3 a v er a g eD a f n y l in es, 33.1 a v er a g e C + + l in es an d 91.2$ 1.31/about15minutes for tests. These are historical generation/compilation figures, not105proved C++ implementations. There is no contradiction merely between first-attempt program compilation and later failing linked tests: they are different stages. The artifact makes the distinction concrete with g++ -std=c++11 -c for generated functions and linked executables for tests. No hardware, exact GPT snapshot/date, seed, repeated-run distribution, token totals or human-review time is given in the paper. [Q8,S2,S4,S7] The introduction proposes precision, recall, correctness, fine-tuning and inference-tool evaluation as uses. It reports none of those downstream comparative experiments. No baseline, prompt ablation, contamination study or evidence of scaling to large legacy C++ is supplied. The authors’ efficiency/scalability language is broader than the measured105small-program conversion. Future work explicitly includes larger and more complex programs. [Q1,Q8,Q11,Q12] ## Pinned artifact and concrete cases The paper-linked GitHub repository was inspected at commit3f70080088d6d6ad3fe7923f94d2a91968cdc78c. Its README says the benchmark was published at MSR2025; I did not establish separate proceedings metadata. A nontruncated tree lists105with-contract C++ sources,105NoSpec sources and105test sources plus105same-basename executable entries. I did not download or execute those binaries. I read both READMEs, all four Python scripts, requirements, the human-readable conversion report, five program/test pairs (IDs3,14,101,105,106), and ID3’s NoSpec counterpart. That is a targeted static sample, not an audit of the entire dataset. Upstream Dafny source and raw serialized experiment logs were not acquired/loaded. [S0–S18] The translation script calls model gpt-4-turbo with temperature0 and max_tokens2000, extracts a fenced cpp block, compiles an object, and can repair compilation errors for up to10attempts. The checked analysis report records105first-attempt successes,105total attempts, $2.07 an d n oco m p i l a t i o n er r or s, a g r ee in g w i t h T ab l e I . T h er e p or t i s a u t h or - s u ppl i e d e v i d e n ce, n o t a r e p r o d u ce d r u n . T h eco d e^{'} scos tt r a c k er co u n t so n l y t h e ini t ia l r es p o n se, so h y p o t h e t i c a l r e p ai r cos t s w o u l d b eo mi tt e d; b ec a u se t hi sr e p or t s a y s a l l a tt e m pt s w er e f i r s t a tt e m pt s, t hi so b ser v a t i o n d oes n o t es t ab l i s han u n d er co u n t f or t h er e p or t e d r u n . [S 2, S 7] g e tT es t s . p y u ses t e m p er a t u r e 0/ ma x_{t} o k e n s 500 an d u pt o 5 a tt e m pt s t oe x t r a c t a co d e b l oc k, t h e n w r i t es a t es t in c l u d in g t h e t r an s l a t e d p r o g r am . T h escr i ptl ab e l sr es p o n se . u s a g e . t o t a l_{t} o k e n s a s in p u t_{t} o k e n s an d a l soc ha r g esco m pl e t i o n_{t} o k e n s a t o u tp u t r a t es . S t a t i c a cco u n t in g t h er e f or ec ha r g esco m pl e t i o n t o k e n so n ce a t in p u t r a t es a s w e l l a so u tp u t r a t es; o n l y t h e f ina l s u ccess f u l r es p o n s e^{'} s u s a g e i sr e t u r n e d, o mi tt in g f ai l e d e x t r a c t i o na tt e m pt s . A c t u a l r e q u es t hi s t or i es a r e u na v ai l ab l e, so I d o n o t co m p u t e a cor r ec t e d$ 1.31total or assert that these two effects cancel. The runner counts process success/failure, but its error-category tests search str(CalledProcessError) without captured stderr, limiting reliable diagnosis of assertion/linker/compiler categories. Neither issue turns a successful test return into a proof. [S3,S4] The static cases show what the annotations mean. IsNonPrime(ID3) checks a divisor-search invariant and a quantified-by-loop postcondition; its tests cover2,10,35. KthElement(ID101) checks1≤k≤array size and returns arr[k−1]; three tests confirm specified positions, not sorted-order statistics. CountTrue(ID105) compares the running count with a recursive helper and excludes empty vectors. AppendArrayToSeq(ID106) preserves the input prefix and appended elements with explicit loops; it requires !a.empty(), commented “equivalent to a != null in Dafny.” Nonempty and nonnull are different conditions: an empty C++ vector is a valid value. Without the upstream Dafny source I flag the local comment/contract mismatch, rather than claiming a checked source-to-target counterexample. All five sampled tests contain three explicit input cases. [S8–S17] TriangularPrismVolume(ID14) accepts positive unsigned arguments, computes (baseheightlength)/2, and asserts equality with that identical expression. The contract checks the same finite-width, integer-division expression, so by itself it does not establish unbounded arithmetic or fractional-volume semantics. Its tests use products with integral halves (10,8,6→240;3,2,2→6;1,2,1→1). IDs3/105/106 also execute additional loops or recursive helpers for assertions, which is actual checking work while assertions are enabled. No runtime-overhead measurement is reported. ID3’s NoSpec file removes those checks; the removal script is textual pattern matching rather than a verified transformation. [S5,S8–S18] ## Contribution and read scope This adds an accessible LLM-assisted contract dataset and concrete translation/test failures to the specification-evaluation collection. My inference for evaluating proof/specification agents is to separate source verification, target compilation, finite testing, expert repair and target proof; inspect input-domain restrictions and arithmetic semantics; and distinguish repeated computations from independently adequate contracts. The paper has no distributed-protocol, Verus/Rust, TLA+ or proof-writing-agent experiment. [Q4,Q6,Q7,Q10,Q12] Read all5pages,15references,both figures including the full prompt image,TableI and all printed code; viewed all5page renders. Official arXiv and inventory PDFs are byte-identical. Read19pinned static text files with SHA256/Gitblobidentities, plus the cited C++ draft paragraph. No author code was executed/imported; no compiler, checker, prover or solver was run; no serialized scientific experiment results were loaded. Reported outcomes remain author-reported.
- limits: 105smallDafny-derivedprograms;assertiontests/subsetexpertreviewnotdeductiveC++proof;signedoverflowclaimcorrected;targetedartifactsample
- how much was read: most of it read
- source
- record id: formalspeccpp-a-dataset-of-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
- record id: fvapps-2025
Generative transformations and patterns in LLM-native approaches for software verification and falsification (2025)
- what: author claim: The paper proposes treating prompt-induced LLM operations as typed “generative transformations” with conceptual input/output signatures, rather than reasoning directly about low-level prompts. It derives a hierarchical taxonomy of those transformations from LLM-based verification/falsification literature and catalogs recurrent ways transformations are composed into larger solutions. scope: The substantive study targets prompt-based LLM approaches to software testing/falsification, debugging/root-cause analysis, vulnerability/misuse/fault detection, static analysis, and program verification. The authors deliberately exclude primarily fine-tuned or non-prompt transformer systems and generally exclude program synthesis/repair and code review as end goals, while retaining papers that use in-scope verification/testing transformations inside such systems. taxonomy: The paper defines six top-level transformation categories: Generative, Evaluative, Extractive, Abstractive, Executive, and Consultative. More specific classes are described through externally visible dimensions such as generation/analysis criterion, artifact type, rationalization, reactivity, corrective feedback, and in-filling context. extraction model: The authors model solution proposals as dataflow graphs in which LLM-mechanized and conventional algorithmic transformations generate intermediate variables. They use this abstraction to recover intended transformations, conceptual signatures, and dependencies among them. patterns: The paper derives a large catalog of inter-transformation patterns. Examples include Enhance, Enrich with Precisions, Use Verbalized SWE, Generate and Fix, Rationalize then Summarize, Build Model, Extract to Focus, Reactively Consume Input, Fix with Sanity Check Signal, Fix with Goal Satisfaction Signal, Vote, Judge, Test Symbolically, Constrain Generation, Plan/Refine/Act/Update, and Filter before Expensive Call. mapping: It maps transformation classes to software-engineering problem areas and maps patterns to end-to-end transformative goals. This exposes where the reviewed literature frequently uses decomposition, feedback, extraction, verbalized abstractions, planning, or validation and where the authors found no such pattern. prospective analysis: The paper uses the taxonomy and pattern catalog to motivate future work on verbalized abstractions, reactive consumption of executable/inferential models, transformation-specific evaluation, constrained generation, symbolic integration, and compositional reasoning. appendix: Appendix A supplies the detailed taxonomy trees omitted from the main presentation, including mappings from individual tools/papers to observed choices for general/domain-specific code generation, annotations, data generation, behavior analysis, classification, extraction, verbalization/formalization, planning, execution, textual manipulation, and knowledge distillation. important non contribution: The study does not experimentally establish that the cataloged patterns are best practices, nor does it benchmark their causal effectiveness. It explicitly treats such judgments as out of scope.
- number: screening: approximately discarded after content review: 140 initial retained papers: 75 later added papers: 36 reported papers after expansion: 111 initial recovered transformations with repetitions: approximately 200 transformations in later 36 papers: 83 total recovered transformations: 284 proposal complexity table 1 total percent: 1 transformation type: 40% 2 transformation types: 30% 3 transformation types: 12% 4 transformation types: 9% 5 transformation types: 6% 6 transformation types: 2% 8 transformation types: 2% note: The displayed percentages sum to 101%, consistent with independent rounding. proposal complexity by problem area percent: testing fuzzing: 1: 39% 2: 31% 3: 11% 4: 13% 5: 3% 6: 2% 8: 2% debugging root cause analysis: 1: 15% 2: 62% 3: 15% 4: 8% vulnerability detection: 1: 61% 2: 15% 3: 15% 5: 6% 6: 3% static analysis: 1: 33% 2: 11% 3: 11% 4: 22% 5: 22% program verification: 1: 20% 2: 50% 5: 20% 8: 10% taxonomy: top level categories: 6 named transformation classes visible in figure 3 and figure 4: 23 named classes count note: 23 is a reader count of the labels shown in the supplied taxonomy/plot, not an explicit author-stated total. bibliography: numbered references present: 305
- limits: type: scope author claim: The technological scope is prompt-based LLM use. Primarily fine-tuned models, general transformer architectures, and approaches using transformer embeddings are excluded. type: topic_scope author claim: Program generation/synthesis, program repair, and code review are generally excluded as primary software-engineering goals, except when the approach prompts in-scope testing, verification, or fault-localization transformations as part of its larger workflow. type: time_scope author claim: The stated inclusion window covers journal, conference, or arXiv papers through the first week of June 2024, plus papers already announced at conferences through July 2024. ASE 2024 papers were subsequently used as a taxonomy-validation step. type: coverage author claim: Under the selected LLM and date criteria, the authors found no studies whose primary contribution directly addressed some traditional areas such as runtime verification, symbolic execution, and some model-checking challenges. type: interpretation author claim: Prompt-to-transformation mapping is manual and often nontrivial because papers describe LLM interactions heterogeneously and sometimes incompletely. type: signature_assumption author claim: Conceptual input signatures are recovered by reasoning about which variables should condition a transformation. The authors explicitly acknowledge that opaque attention mechanisms may depend on nominally irrelevant context through latent internal representations. type: granularity author claim: Prompts and transformations need not correspond one-to-one. One prompt can induce chained transformations, while autoregressive reasoning can create runtime stages that cannot be statically recovered. The study focuses on higher-level transformations intended by tool developers. type: conversation_structure author claim: The abstraction may omit or misstate whether transformations occur in one continuing conversation or separate LLM sessions. The authors acknowledge that such details can materially affect practical performance. type: modularity author claim: The analysis deliberately adopts a virtual modular/functional view of LLM interactions even though true probabilistic modularity cannot be assumed. type: taxonomy_generalization author claim: The taxonomy may be overfit to the analyzed literature and fail to accommodate future LLM-native systems, although the authors designed its property/choice dimensions to be extensible. type: pattern_evidence author claim: Pattern derivation uses peer-reviewed proposals, but whether identified patterns are best practices, their advantages/disadvantages, and catalog completeness are explicitly outside the paper’s claims. type: effectiveness author claim: The paper reports mappings, frequencies, examples, and qualitative relationships; it does not provide a controlled comparison showing that one transformation or composition pattern outperforms another. type: source_version author claim: The supplied source is arXiv v3 dated 6 Oct 2025 and identifies itself as a preprint submitted to Elsevier on October 8, 2025. It also refers to an earlier v2 technical report and says publication venues/tool names were later updated. type: source_access record note: Only the supplied extracted manuscript was used. Its bibliography entries were read, but the externally cited papers themselves were not provided and were not independently followed, inspected, or executed. The paper says its authors analyzed papers and associated repositories; this record does not independently verify that work. type: graphics record note: The extraction preserves most captions and textual labels from figures/taxonomy trees, but graphical semantics such as colors, arrows, framed ASE’24 boxes, exact tree layout, and some dense table alignment are partially lost. Table 2 in particular is visually linearized, so this record does not infer uncertain cell-to-column mappings from it.
- how much was read: most of it read
- source
- record id: generative-transformations-and-patterns-2025
GraFT (2025)
- title: Grammar-Forced Translation of Natural Language to Temporal Logic using LLMs
- what: It restricts the model’s output tokens with a grammar. It separates identifying propositions from translating them into temporal form.
- number: evaluates Navigation, GLTL and Cleanup World datasets with 1,000 examples each
- limits: A correct grammar cannot find missing requirements. The evaluation has no score for equivalence or strength.
- how much was read: most of it read
- source; notes: Natural language to temporal logic and TLA+; notes: Temporal requirement translation: VLTL-Bench and GraFT
- record id: graft-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+
- record id: informal-to-formal-2025
Interleaving static analysis and LLM prompting with applications to error specification inference (2025)
- what: Interleaves EESI abstract-interpretation analysis with LLM queries to infer function error return values in C. Analyzes bottom-up in the call graph, asks the LLM about unavailable library functions or functions left unknown by analysis, and propagates the results as new facts. Prompts combine error-code conventions, abstract-domain/format examples, and known callee specifications; missing-library queries receive available specification context. Recursive SCCs use a fixed point. Requeries for consistency, excludes known success values and results exceeding return ranges, and tracks the origin, dependency path and LLM-call count of inferred facts. Journal extension studies error propagation, infallibility classification and nondeterministic outcomes.
- number: 6 C programs; 2–288 KLOC
- number: recall 52.55% to 77.83%; F1 0.612 to 0.804
- number: precision 86.67% to 85.12%
- number: 973 GPT-4o-mini requests; reported 3,000 in subscriptions
- number: Ten xv6 bugs and one Sail bug found; median kernel-update re-proof 35 agent-minutes
- limits: It covers safety only, not liveness. Humans steered the layering and specs heavily.
- how much was read: parts read
- source
- record id: machcsl-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
- 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
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
- record id: case-study-on-llms-2025
DeepSeek-Prover-V2 (2025)
- title: DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
- what: It breaks Lean math problems into subgoals and proves them with a smaller model. It then trains on the assembled solutions.
- number: miniF2F 88.9% (217/244) at pass@8192
- number: ProverBench 325 problems
- number: PutnamBench: PDF says 47 accepted of 658; README says 49; only 649 evaluated
- limits: Success on mathematics does not show skill at writing specs for systems. The 47 vs 49 discrepancy comes from two benchmark statements that were misformulated.
- how much was read: parts read
- source
- record id: deepseek-prover-v2-2025
PSyn (2025)
- title: Guiding Likely Invariant Synthesis on Distributed Systems with LLMs
- what: Compares LLMs generating invariants directly against symbolic synthesis, on eight Promela distributed systems checked with Spin. In PSyn, the LLM proposes predicates from counterexamples.
- number: 8 Promela systems: Peterson, Bakery, Alternating Bit, Leader Election, UPPAAL Train/Gate, Distributed Lock Server, Producer Consumer, Smart Contract
- limits: The target is probably invariants for monitoring, not proofs.
- how much was read: parts read
- record id: psyn-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
Terzian TLA+-to-Rust (2025)
- title: A Tale of Two Refinements: LLM-assisted TLA+ to Rust
- what: The report repeatedly refines TLA+ models and asks Gemini to implement an image-cache example as multithreaded Rust. Its history records a livelock (threads keep running but make no progress) and a premature termination. Both needed correction.
- limits: This is a project report and is not peer reviewed. No Verus proof was found. The claim of “fully verified, spec-driven code generation” is only a possibility.
- how much was read: parts read
- source; notes: R01. A Tale of Two Refinements: LLM-assisted TLA+ to Rust
- record id: terzian-tla-to-rust-2025
ClarifyGPT (2024)
- title: ClarifyGPT: A Framework for Enhancing LLM-Based Code Generation via Requirements Clarification
- what: It notices when candidate programs disagree on generated tests. It then asks the user targeted clarifying questions to sharpen the requirement.
- limits: Agreement among candidates cannot show that a description has only one meaning, because the models may share an assumption. The final and earlier preprint versions have different evaluations.
- how much was read: parts read
- source; notes: Clarification and stakeholder requirements
- record id: clarifygpt-2024
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
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: specification-anchored auditing
- record id: speca-2026
Specifications for Humans, Agents, and Tooling (2026)
- what: Describes the Bosque API ecosystem for agent-driven development. It has polyglot specs, test generation, validation and sandboxing. Specs are shared artifacts for people, agents and tools.
- limits: A position on tooling. No refinement theorem and no evaluation on a distributed protocol. Not evidence that intent can be recovered automatically.
- how much was read: only abstract or first pages read
- source
- record id: specifications-for-humans-agents-2026
FASTRIC (2025)
- title: FASTRIC: Prompt Specification Language for Verifiable LLM Interactions
- what: A prompt language that makes explicit the finite-state machine hidden in a multi-turn LLM conversation. This allows checking that a conversation follows the protocol, using execution traces.
- limits: Checks that a run follows the protocol. It does not prove theorems. The pages inspected had no TLA+ or Verus refinement, and no progress proof.
- how much was read: only abstract or first pages read
- source
- record id: fastric-2025
FLAG (2025)
- title: FLAG: Formal and LLM-assisted SVA Generation for Formal Specifications of On-Chip Communication Protocols
- what: It takes unstructured protocol documents to checked properties. It generates candidate properties from a grammar, filters them with timing diagrams and checks them formally.
- limits: It covers a constrained domain: hardware protocols.
- how much was read: only abstract or first pages read
- source; notes: FLAG
- record id: flag-2025
Next Steps in LLM-Supported Java Verification. (2025)
- what: —Recent work has shown that Large Language Mod- Unfortunately, we are still far from reaching the golden age. els (LLMs) are not only a suitable tool for code generation but One reason for this is a lack of techniques to reliably elicit an- also capable of generating annotation-based code specifications. As the number of required annotations Scaling these methodologies may allow us to deduce provable grows with the size of the analyzed software system, a lack arXiv:2502.01573v1 [cs.SE] 3 Feb 2025 correctness guarantees for large-scale software systems.
- how much was read: only abstract or first pages read
- source
- record id: next-steps-in-llm-2025
Transforming Natural Language Requirements to Formalism Using LLMs (2025)
- what: GE Aerospace Research built an LLM tool that interactively turns plain-English requirements into logical formulas, with an English-language interface meant to let non-experts confirm the translation is right. It was tried on an industry landing-gear case.
- limits: Full text not obtained (Wiley paywall behind a bot check; Unpaywall lists no open copy), so numbers, formalism used, and evaluation method are unknown; only the abstract was read.
- how much was read: only abstract or first pages read
- source; notes: LLM translation of natural-language requirements to formalism (2025)
- record id: transforming-natural-language-requirements-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
- record id: specifications-the-missing-link-2024
A Contemporary Survey of Large Language Model Assisted Program Analysis
- what: : The increasing complexity of software systems has driven significant ad- Revised: 20 April 2025 vancements in program analysis, as traditional methods are unable to meet the demands Accepted: 28 April 2025 of modern software development. To address these limitations, deep learning tech- Published: 26 May 2025 niques, particularly Large Language Models (LLMs), have gained attention due to their context-aware capabilities in code comprehension. Recognizing the potential of LLMs, researchers have extensively explored their application in program analysis since their introduction.
- how much was read: only abstract or first pages read
- source
- record id: a-contemporary-survey-of
A dual perspective review on large language models and code verification
- what: TYPE Review PUBLISHED 24 November 2025 DOI 10.3389/fcomp.2025.1655469 A dual perspective review on OPEN ACCESS large language models and code veriﬁcation EDITED BY Novarun Deb, University of Calgary, Canada REVIEWED BY Livinus Obiora Nweke, Greta Dolcetti1 and Eleonora Iotti2* Noroff Education AS, Norway T. Gururaj, 1 Department of Environmental Sciences, Informatics and Statistics, Ca’ Foscari University of Venice, Visvesvaraya Technological University, India Venice, Italy, 2 Department of Mathematical, Physical and Computer Sciences, University of Parma, *CORRESPONDENCE Parma, Italy Eleonora Iotti eleonora.iotti@unipr.it RECEIVED 27 June 2025 Recent advances in Large Language Models (LLMs) have sparked signiﬁcant ACCEPTED 24 October 2025 interest in their application to code veriﬁcation and the assessment of PUBLISHED 24 November 2025 LLM-generated code safety. This review examines current research on the CITATION intersection of LLMs with software veriﬁcation, focusing on two main aspects: the Dolcetti G and Iotti E (2025) A dual perspective review on large language models and code use of LLMs as veriﬁcation tools and the veriﬁcation of code produced by LLMs.
- how much was read: only abstract or first pages read
- source
- record id: a-dual-perspective-review
Accessible Smart Contracts Verification: Synthesizing Formal Models with Tamed LLMs
- what: When blockchain systems are said to be trustless, what this really means is that all the trust is put into software. Thus, there are strong incentives to ensure blockchain software is correct—vulnerabilities here cost millions and break businesses. One of the most powerful ways of establishing software correctness is by using formal methods.
- how much was read: only abstract or first pages read
- source
- record id: accessible-smart-contracts-verification
AgentGuard: Runtime Verification of AI Agents.
- what: —The rapid evolution to autonomous, agentic AI from mathematics and formal methods with the existing theory systems introduces significant risks due to their inherent unpre- of these agentic systems [6]. dictability and emergent behaviors; this also renders traditional In this work, we present AgentGuard, a framework for verification methods inadequate and necessitates a shift towards probabilistic guarantees where the question is no longer if a system runtime verfication of Agentic AI systems.
- how much was read: only abstract or first pages read
- source
- record id: agentguard-runtime-verification-of
AGVTS: Automated Generation and Verification of Temporal Specifications for Aeronautics SCADE Models
- what: . SCADE is both a formal language and a model-based devel- opment environment, widely used to build and verify the models of safety-critical system (SCS). The SCADE Design Veriﬁer (DV) provides SAT-based veriﬁcation.
- how much was read: only abstract or first pages read
- source
- record id: agvts-automated-generation-and
AssertLLM: Generating Hardware Verification Assertions from Design Specifications via Multi-LLMs
- what: Table 1: Existing works on generating SVAs from natural language specifications. AssertLLM is the first work that can Assertion-based verification (ABV) is a critical method to ensure arXiv:2411.14436v1 [cs.AR] 4 Nov 2024 handle full-size specification files and generate comprehen- logic designs comply with their architectural specifications. ABV sive types of SVAs for each architectural signal.
- limits: Abstract-level reading from openly available PDF; detailed limitations require full paper review.
- how much was read: only abstract or first pages read
- source
- record id: assertllm-generating-hardware-verification
Automatically Improving LLM-based Verilog Generation using EDA Tool Feedback
- what: Automatically Improving LLM-based Verilog Generation using EDA Tool Feedback JASON BLOCKLOVE, NYU Tandon School of Engineering, USA SHAILJA THAKUR, NYU Tandon School of Engineering, USA BENJAMIN TAN, Universary of Calgary, Canada HAMMOND PEARCE, University of New South Wales, Australia SIDDHARTH GARG, NYU Tandon School of Engineering, USA arXiv:2411.11856v3 [cs.AR] 4 Mar 2025 RAMESH KARRI, NYU Tandon School of Engineering, USA Traditionally, digital hardware designs are written in the Verilog hardware description language (HDL) and debugged manually by engineers. This can be time-consuming and error-prone for complex designs. Large Language Models (LLMs) are emerging as a potential tool to help generate fully functioning HDL code, but most works have focused on generation in the single-shot capacity: i.e., run and evaluate, a process that does not leverage debugging and, as such, does not adequately reflect a realistic development process.
- limits: Read from the saved open PDF at abstract/opening-section depth; quote is copied from extracted PDF text.
- how much was read: only abstract or first pages read
- source
- record id: automatically-improving-llm-based
AutoTAMP: Autoregressive Task and Motion Planning with LLMs as Translators and Checkers
- what: — For effective human-robot interaction, robots need applying them to task execution [7], task planning [8], [9], to understand, plan, and execute complex, long-horizon tasks [10], [11] and TAMP [12], [13]. described by natural language. Recent advances in large Promising early efforts used LLMs as direct task planners language models (LLMs) have shown promise for translating natural language into robot action sequences for complex tasks.
- how much was read: only abstract or first pages read
- source
- record id: autotamp-autoregressive-task-and
Can Large Language Models Help Students Prove Software Correctness? An Experimental Study with Dafny
- what: Students in computing education increasingly use large lan- guage models (LLMs) such as ChatGPT. Yet, the role of LLMs in sup- porting cognitively demanding tasks, like deductive program verification, remains poorly understood. This paper investigates how students inter- act with an LLM when solving formal verification exercises in Dafny, a language that supports functional correctness by allowing programmers to write formal specifications and automatically verifying that the im- plementation satisfies the specification.
- how much was read: only abstract or first pages read
- source
- record id: can-large-language-models
CaStL: Constraints as Specifications Through Llm Translation for Long-Horizon Task and Motion Planning
- what: CaStL: Constraints as Specifications through LLM Translation for Long-Horizon Task and Motion Planning Weihang Guo, Zachary Kingston, and Lydia E. Kavraki Abstract— Large Language Models (LLMs) have demon- Some methods directly address this limitation and focus on strated remarkable ability in long-horizon Task and Motion more expressive formal languages to encode constraints (e.g., Planning (TAMP) by translating clear and straightforward AutoTAMP [12] and DELTA [11]). These methods also are natural language problems into formal specifications such as the Planning Domain Definition Language (PDDL).
- how much was read: only abstract or first pages read
- source
- record id: castl-constraints-as-specifications
Formal software verification using large language models
- what: //@ requires x >= 0.0; /*@ ensures JMLDouble This document gives a tutorial
- how much was read: only abstract or first pages read
- source
- record id: formal-software-verification-using
From Concept to Practice: an Automated LLM-aided UVM Machine for RTL Verification
- what: From Concept to Practice: an Automated LLM-aided UVM Machine for RTL Verification 0 30% Frontend Design 70% 1 0 0 % 30% Frontend Development 70% 100 % % 0 % IC Design IC Verification IC Design IC Verification Junhao Ye1,2 , Yuchen Hu1,2 , Ke 1 Xu1,2 , Dingrong Pan2 , Qichun Chen3 , Jie Zhou 1,2 Bottleneck 4 0 10% 70% 10% 10% 100 0 10% Shuai 70% Zhao , Xinwei 10% Fang 10% 0 5,∗ , Xi Wang 1,2,∗ , Nan Guan6 , Zhe Jiang1,2,∗ % Verification Formal % % 0 Sign-off 1 School Blueprint Functional Verification Verification Verification Review Formal Sign-off of Integrated Circuits, Southeast Function VerificationUniversity, % China 2 National Verification Center of Technology Innovation for EDA, China UVM-based Testbench 3 College of Economics, Shenzhen University, China UVM Testbench 1 0 10% 30% 10% 50% 100 0 10% 30% 4 School 10% of Computer 50% 0 Science and Engineering, % Sun Yat-sen University,Simulation China % % 0 Test Testbench Testcase Test Testbench Testcase5 Testcase Planning Generation Analysis Supplement Planning Generation Analysis Department Supplement of Computer % Science, University of York, UK 6 Department of Computer Science, City University of Hong Kong,Time HongConsumptio
- how much was read: only abstract or first pages read
- source
- record id: from-concept-to-practice
From Scientific Texts to Verifiable Code: Automating the Process with Transformers
- what: From Scientific Texts to Verifiable Code: Automating the Process with Transformers Changjie Wang Mariano Scazzariello Marco Chiesa KTH Royal Institute of Technology KTH Royal Institute of Technology KTH Royal Institute of Technology Abstract—Despite the vast body of research literature propos- and long, covering several pages of an article or book. The ing algorithms with formal guarantees, the amount of verifiable complexity of the structure of the proof and properties of data code in today’s systems remains minimal. This discrepancy stems types quickly escalates, making it difficult for humans to grasp from the inherent difficulty of verifying code, particularly due to the time-consuming nature and strict formalism of proof details the complexity.
- how much was read: only abstract or first pages read
- source
- record id: from-scientific-texts-to
FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware
- what: The remarkable reasoning and code generation capabilities of large language models (LLMs) have spurred significant interest in applying LLMs to enable task automation in digital chip design. In particular, recent work has investigated early ideas of applying these models to formal verification (FV), an approach to verifying hardware implementations that can provide strong guarantees of confidence but demands significant amounts of human effort. While the value of LLM-driven automation is evident, our understanding of model performance, however, has been hindered by the lack of holistic evaluation.
- how much was read: only abstract or first pages read
- source
- record id: fveval-understanding-language-model
How Effective are Large Language Models in Generating Software Specifications?
- what: —Software specifications are essential for many Soft- more defects. Several other attempts have been made to further ware Engineering (SE) tasks such as bug detection and test improve these processes in various domains [9], [11]–[13]. generation.
- how much was read: only abstract or first pages read
- source
- record id: how-effective-are-large
Hybrid-NL2SVA: Integrating RAG and Finetuning for LLM-based NL2SVA
- what: —SystemVerilog Assertions (SVAs) are critical for verifying generalize across diverse specifications and require substantial man- the correctness of hardware designs, but manually writing them from ual effort. More recently, LLM-based approaches like nl2spec [12] natural language property descriptions, i.e., NL2SVA, remains a labor- introduce interactive prompting frameworks where engineers refine intensive and error-prone task. Recent advances in large language models (LLMs) offer opportunities to automate this translation.
- how much was read: only abstract or first pages read
- source
- record id: hybrid-nl2sva-integrating-rag
LTRAG: Enhancing Autoformalization and Self-refinement for Logical Reasoning with Thought-Guided RAG
- what: A recent endeavor for logical reasoning over NL is neuro-symbolic methods based on autoformal- Logical reasoning is fundamental to intelli- ization, by combining translation with LLMs from gent systems. Large language models (LLMs) NLs to formal languages and rigorous reasoning have demonstrated promise in natural language (NL) reasoning, especially with techniques like of symbolic solvers. As long as the translations chain-of-thought (CoT) prompting.
- how much was read: only abstract or first pages read
- source
- record id: ltrag-enhancing-autoformalization-and
NL2LTL – a Python Package for Converting Natural Language (NL) Instructions to Linear Temporal Logic (LTL) Formulas
- what: The Thirty-Seventh AAAI Conference on Artificial Intelligence (AAAI-23) NL2LTL – A Python Package for Converting Natural Language (NL) Instructions to Linear Temporal Logic (LTL) Formulas Francesco Fuggitti1,2 , Tathagata Chakraborti3 1 Sapienza University, Rome (Italy) 2 York University, Toronto (Canada) 3 IBM Research, Cambridge (USA) fuggitti@diag.uniroma1.it, tathagata.chakraborti1@ibm.com Abstract This is a demonstration of our newly released Python pack- age NL2LTL which leverages the latest in natural language understanding (NLU) and large language models (LLMs) to translate natural language instructions to linear temporal logic (LTL) formulas. This allows direct translation to for- mal languages that a reasoning system can use, while at the Figure 1: NL2LTL components same time, allowing the end-user to provide inputs in natu- ral language without having to understand any details
- limits: Abstract-level reading from openly available PDF; detailed limitations require full paper review.
- how much was read: only abstract or first pages read
- source
- record id: nl2ltl-a-python-package
NL2TL: Transforming Natural Languages to Temporal Logics using Large Language Models
- what: spatial, temporal, and logical requirements of both Temporal Logic (TL) can be used to rigorously human languages and environmental constraints, specify complex high-level specification for and can be transformed into executable actions or systems in many engineering applications. The control inputs for robots (Gundana and Kress-Gazit, translation between natural language (NL) and 2022; Raman et al., 2013; Boteanu et al., 2016; Pa- TL has been under-explored due to the lack tel et al., 2020; Gopalan et al., 2018). of dataset and generalizable model across dif- Unlike many robotics works that try to use end- ferent application domains.
- how much was read: only abstract or first pages read
- source
- record id: nl2tl-transforming-natural-languages
Olympiad-level formal mathematical reasoning with reinforcement learning
- what: C A long-standing goal of artificial intelligence is to build systems capable of complex reasoning in vast domains, a task epitomized by mathematics with its boundless concepts and demand for rigorous proof. Recent AI systems, often TI reliant on human data, typically lack the formal verification necessary to guarantee correctness. By contrast, formal languages such as Lean [1] offer an interactive environment that grounds reasoning, and reinforcement learning (RL) provides a mechanism for learning in such environments.
- limits: Abstract-level reading from openly available PDF; detailed limitations require full paper review.
- how much was read: only abstract or first pages read
- source
- record id: olympiad-level-formal-mathematical
PaMpeR: proof method recommendation system for Isabelle/HOL.
- what: —Deciding which sub-tool to use for a given proof state it is possible to advise which proof methods are arXiv:1806.07239v1 [cs.LO] 19 Jun 2018 requires expertise specific to each ITP. To mitigate this problem, useful to a given proof state, based only on the meta- we present PaMpeR, a proof method recommendation system for information about the state and information in the Isabelle/HOL. Given a proof state, PaMpeR recommends proof methods to discharge the proof goal and provides qualitative standard library.
- how much was read: only abstract or first pages read
- source
- record id: pamper-proof-method-recommendation
Ranking LLM-Generated Loop Invariants for Program Verification
- what: foundational AI models that have revolutionized Language Processing applications. Though LLMs Synthesizing inductive loop invariants is fun- damental to automating program verification. were originally proposed for natural languages, In this work, we observe that Large Language they have exhibited great success in formal lan- Models (such as gpt-3.5 or gpt-4) are capa- guages such as programming languages (Chen ble of synthesizing loop invariants for a class of et al., 2021).
- limits: Abstract-level reading from openly available PDF; detailed limitations require full paper review.
- how much was read: only abstract or first pages read
- source
- record id: ranking-llm-generated-loop
Safeguarding AI-Based Software Development and Verification using Witnesses (Position Paper)
- what: . This position paper accompanies a presentation and discussion at AISoLA 2023 on the topic of how (generative) AI influences software engineering, namely, the development and verification of software pro- grams. We outline a few opportunities and challenges that are posed by the application of AI.
- how much was read: only abstract or first pages read
- source
- record id: safeguarding-ai-based-software
Self-HWDebug: Automation of LLM Self-Instructing for Hardware Security Verification
- what: —The rise of instruction-tuned Large Language Mod- process of crafting inputs that guide LLMs’ responses, has els (LLMs) marks a significant advancement in artificial intelli- been widely used for hardware security verification purposes gence (AI) (tailored to respond to specific prompts). For example, [8] has explored employing expert- popularity, applying such models to debug security vulnerabilities in hardware designs, i.e., register transfer language (RTL) crafted prompts to steer model behavior in specific debugging modules, particularly at system-on-chip (SoC) level, presents scenarios. However, this method suffers from scalability and considerable challenges.
- limits: Read from the saved open PDF at abstract/opening-section depth; quote is copied from extracted PDF text.
- how much was read: only abstract or first pages read
- source
- record id: self-hwdebug-automation-of
SpecRover: Code Intent Extraction via LLMs.
- what: SpecRover: Code Intent Extraction via LLMs Haifeng Ruan* Yuntong Zhang* Abhik Roychoudhury National University of Singapore {hruan,yuntong,abhik}@comp.nus.edu.sg Abstract—Autonomous program improvement typically in- with code generation via GitHub Copilot, one can envision volves automatically producing bug fixes and feature additions. trustworthy code construction from LLMs. Such program improvement can be accomplished by a combi- Program improvement or program repair, typically requires nation of large language model (LLM) and program analysis capabilities, in the form of an LLM agent.
- how much was read: only abstract or first pages read
- source
- record id: specrover-code-intent-extraction
StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs Through Knowledge-Reasoning Fusion
- what: mathematical reasoning (Zhou et al. 2024), and the genera- tion of verifiable code (Lin et al. 2024; Thakur et al.
- limits: Abstract-level reading from openly available PDF; detailed limitations require full paper review.
- how much was read: only abstract or first pages read
- source
- record id: stepfun-formalizer-unlocking-the
Towards AI-Assisted Synthesis of Verified Dafny Methods
- what: Towards AI-Assisted Synthesis of Verified Dafny Methods MD RAKIB HOSSAIN MISU∗ , University of California Irvine, USA CRISTINA V. LOPES, University of California Irvine, USA IRIS MA, University of California Irvine, USA JAMES NOBLE† , Creative Research & Programming, New Zealand arXiv:2402.00247v2 [cs.SE] 10 Jun 2024 Large language models show great promise in many domains, including programming. A promise is easy to make but hard to keep, and language models often fail to keep their promises, generating erroneous code.
- how much was read: only abstract or first pages read
- source
- record id: towards-ai-assisted-synthesis
Towards Specification-Driven LLM-Based Generation of Embedded Automotive Software
- what: . The paper studies how code generation by LLMs can be com- bined with formal verification to produce critical embedded software. The first contribution is a general framework, spec2code, in which LLMs are combined with different types of critics that produce feedback for itera- tive backprompting and fine-tuning.
- how much was read: only abstract or first pages read
- source
- record id: towards-specification-driven-llm
Unleashing the Power of LLM to Infer State Machine From the Protocol Implementation
- what: —State machines are essential for enhancing proto- significantly discrepant FSMs, and these discrepancies are col analysis to identify vulnerabilities. However, inferring state often hotspots for vulnerabilities. Therefore, FSMs extracted machines from network protocol implementations is challenging from specific protocol implementations are more accurate than due to complex code syntax and semantics.
- how much was read: only abstract or first pages read
- source
- record id: unleashing-the-power-of
VeCoGen: Automating Generation of Formally Verified C Code With Large Language Models.
- what: VeCoGen: Automating Generation of Formally Verified C Code with Large Language Models Merlijn Sevenhuijsen Khashayar Etemadi Mattias Nyberg Scania & KTH Royal Institute of Technology KTH Royal Institute of Technology Scania & KTH Royal Institute of Technology Södertälje, Sweden Stockholm, Sweden Södertälje, Sweden merlijn.sevenhuijsen@scania.com khaes@kth.se mattias.nyberg@scania.com Abstract—Large language models have demonstrated impres- the program candidates. If all generated program candidates sive capabilities in generating code, yet they often produce pro- arXiv:2411.19275v3 [cs.SE] 7 Apr 2025 fail compilation or verification, V E C O G EN continues to the it- grams with flaws or deviations from intended behavior, limiting erative code improvement step. In this step, V E C O G EN parses their suitability for safety-critical applications.
- how much was read: only abstract or first pages read
- source
- record id: vecogen-automating-generation-of
VerifyLLM: LLM-Based Pre-Execution Task Plan Verification for Robots
- what: — In the field of robotics, researchers face a critical challenge in ensuring reliable and efficient task planning. Veri- fying high-level task plans before execution significantly reduces errors and enhance the overall performance of these systems. arXiv:2507.05118v1 [cs.RO] 7 Jul 2025 In this paper, we propose an architecture for automatically verifying high-level task plans before their execution in simu- lator or real-world environments.
- how much was read: only abstract or first pages read
- source
- record id: verifyllm-llm-based-pre
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
ACSLAgent (2026)
- title: ACSLAgent: Verifier-Constrained Neural-Symbolic Synthesis of Formal Program Specifications
- what: A tool that asks LLMs for C specifications (function contracts, loop invariants, loop variants for termination) and uses the Frama-C WP verifier to reject wrong ones, repairing from verifier feedback.
- number: README claims 91.05% verification success (pass@5) across SyGuS, SV-COMP and industrial components
- number: README claims termination proofs via synthesized ranking functions upgrade partial to total correctness
- limits: No paper could be found: the Zenodo record is an anonymous code archive whose README is the only prose. Numbers are README claims with no method, baselines or tables; the full results are said to be on a Hugging Face space that was not read.
- how much was read: not read; title and metadata only
- source; notes: ACSLAgent (2026)
- record id: acslagent-2026
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
- record id: apg-2026
Formally Specifying the Intended Behavior of the Program: LLM-Driven Neuro-Symbolic Program Specification Synthesis (2026)
- what: Per the input file: uses an LLM plus symbolic methods to write formal specifications (contracts, loop invariants) from intended behavior. The only source found is a video lecture page on underline.io (uploaded 2026-06-03) with no description, transcript, or paper.
- limits: Blocked: DOI redirects to a video page; the page text has no abstract, authors, or transcript, and no PDF or preprint was found.
- how much was read: not read; title and metadata only
- source; notes: ## Neuro-symbolic specification synthesis talk (2026)
- record id: formally-specifying-the-intended-2026
From Natural Language to Formal Specifications: A Metamodel-Driven LLM Pipeline (2026)
- what: Per the input list: an LLM turns free-form natural-language requirements into an intermediate model and then into formal specifications that tools can verify.
- limits: Full text not read: the ACM page blocked automated download (HTTP 403 from the site’s bot protection, which I did not work around) and no open copy was found. Only the input description and Crossref metadata (authors, venue, 10 pages, Oct 2026) are known; nothing about results.
- how much was read: not read; title and metadata only
- source; notes: ## Metamodel-driven LLM pipeline (2026)
- record id: from-natural-language-to-2026
SG4PM (2026)
- title: Septemberember/SG4PM: Specification Generation for Program Maintenance via LLMs and Testing-Based Formal Verification
- what: Software record (Java tool) where an LLM writes a Functional Scenario Form, a list of input-output scenarios, for a Java program; the scenarios are checked for overlap and completeness and verified against the code by testing combined with Hoare-logic reasoning, so no loop invariants are needed.
- limits: This is a code release, not a paper: no experiments, numbers or limits are given in the README, and no paper could be found. Java programs only.
- how much was read: not read; title and metadata only
- source; notes: SG4PM (2026)
- record id: sg4pm-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
- 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
- record id: testing-llm-generated-distributed-2026
Verifier-supervised fine-tuning for Rust/Verus: vericoding dataset (restricted) (2026)
- what: A Zenodo record for a training dataset of Rust/Verus verified-code tasks used to fine-tune a code model with the verifier as the supervision signal. Only the record’s metadata could be read: the files are under embargo until 2026-12-31 and the record has no listed files.
- limits: Blocked: no full text exists and the data is embargoed (‘access_right’: ‘embargoed’, embargo_date 2026-12-31) with the author listed as ‘Anonymous’ (double-blind review). Everything here comes from the record’s description and keywords; content, size, and results are unknown.
- how much was read: not read; title and metadata only
- source; notes: Verifier-supervised fine-tuning for Rust/Verus dataset (2026)
- record id: verifier-supervised-fine-tuning-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: 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
- 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
- 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
- record id: leanagent

Last edited: 2026-10-31

Keyboard shortcuts

Steven Hé (Sīchàng)

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