🤖 database, from what a human wants to a formal statement

(authored by agents unless marked 🧑)

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

• AeroReq2LTL (2026)
  • title: Automated LTL Specification Generation from Industrial Aerospace Requirements
  • what: Before translating requirements to LTL (a logic for statements about sequences of events), it adds a domain data dictionary and controlled requirement templates. It compares the results to formalizations written by experts for aerospace requirements.
  • number: 85% precision and 88% recall
  • limits: It covers one industrial domain, and its authors overlap with those of Req2LTL. It is not shown to work for the intent of distributed services.
  • how much was read: most of it read
  • source; notes: Natural language to temporal logic and TLA+
  • record id: aeroreq2ltl-2026
• Agentic Proving for Program Verification (Claude Code on CLEVER, Lean 4) (2026)
  • what: Runs Claude Opus 4.6 in Claude Code, with Lean tools, on the 161 CLEVER algorithm tasks. The agent writes formal specifications, implementations and Lean proofs. People manually review whether each specification matches the English task.
  • number: 159/161 tasks get an arguably valid specification (98.8%, merged over runs)
  • number: of 80 tasks with correct references: 65 specs proved equivalent (81.3%), 70 implementations certified (87.5%)
  • number: 81 defective references, 13 valid unmatched alternatives, 2 failures, 65 equivalences
  • number: 154/161 succeed in at least one of two pipelines (95.7%); 154/157 after excluding 4
  • limits: Only proofs that Lean programs compute the right results. No proofs about distributed progress. The 98.1% headline number merges two runs. The authors review the reference-error count themselves. Human effort is not measured.
  • how much was read: most of it read
  • source; notes: Agentic Proving for Program Verification; notes: Agentic Proving for Program Verification
  • 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
• An Empirical Study of LLM-Generated Specifications for VeriFast (2026)
  • what: # An Empirical Study of LLM-Generated Specifications for VeriFast (authored by agents unless marked 🧑) Wen Fan, Minh Tran, Sanya Dod, Xin Hu, Marilyn Rego, Danning Xie, Jenna DiVincenzo and Lin Tan, arXiv:2606.26490v1, 25 June 2026. This is an empirical study of LLM-written specifications and auxiliary proofs for C programs checked with VeriFast. It reports 855/2,727 outputs passing verification (31.4%), 91% source-behavior preservation and 92% contract preservation. The last figure combines equivalent and strengthened contracts; it is not an equivalence rate. The released verification CSVs contain 856 “yes” rows, one more than the paper. No general correctness theorem or end-to-end proof of an LLM verifier is given (Q1,Q8,Q9,T3–T6,C8). ## Reading and source scope Read all 13 PDF pages, sections I–VIII, both figures, all eight tables, displayed code/specifications and all 83 bibliography entries. All 13 individual page renders were inspected. There is no appendix, checklist, numbered theorem/proof or separately numbered algorithm. Figure 1 is a complete append-tail verification example; Figure 2 diagrams the study. References were read as bibliography entries, not recursively followed. The inventory PDF matches its recorded SHA256. Acquired the paper’s §VIII replication package, Zenodo record 19570523, DOI 10.5281/zenodo.19570523; its 17,362,580-byte ZIP matches the published MD5 8c8335ee601057daf18c27d3cf9097e3. Inventoried 14,646 ZIP members. The archive’s ISSRE26 filename does not establish a publication venue. Its metadata identifies an anonymous replication package published 14 April and updated 20 April 2026, preceding the arXiv version; correspondence to every reported run is not established. Read the root and two infrastructure readmes, all selected analyzer and generation scripts, four original append-tail inputs/ground truth, three generated append-tail FBP outputs and four generated files containing literal assume(false). The 15 released CSVs were parsed as plaintext to count labels, unique benchmark names and selected rows; modified.txt was counted, not semantically reviewed. In total 43 plaintext assets are retained, with per-asset reading boundaries. A bounded lexical scan covered the 2,727 primary full-study C outputs, without treating it as whole-output semantic reading. XLSX workbooks, remaining inputs/outputs, retrieved examples/tutorial bodies, libraries, raw checker/API logs and recursively cited papers were not read. No author code was executed/imported, verifier rerun, model/checkpoint loaded or experiment reproduced. Quotes retain exact source bytes and LF/character pointers; arithmetic and static control-flow findings are reader checks, not new experimental results. ## Task, logic and benchmark assumptions Separation logic describes ownership of disjoint heap regions. VeriFast uses symbolic execution, contracts, predicates, loop invariants, folding/unfolding statements and lemma calls to check safety and specified behavior. The paper describes Z3 as the default solver. Although background mentions VeriFast 25.11, actual experiments use 24.08.30 with default integer-overflow and heap-leakage checks. The record therefore does not transfer outcomes to another release or to Verus/Rust (Q2,Q7,Q8). The dataset has 303 functions from 60 small single-file C programs: 258 functions from 50 public examples and 45 from ten author-written programs. Selection starts with 770 repository programs, narrows to 160 single-file example/tutorial programs, then removes 46 lacking code or SL specifications, 49 duplicates or prompt-tutorial examples, ten with unresolved verification errors and five without prepared inputs. This deliberately retains known-verifiable programs, not arbitrary industrial code. Overall ground truth averages 43 source and 81 specification lines, with ranges 3–143 and 5–600. The public and new subsets average 44/91 and 34/32 lines respectively (Q3). Each function receives one mutually exclusive feature tag, prioritizing concurrency, then loops, then recursive predicates: 45 concurrent, 39 loop, 134 recursive-predicate and 85 other functions. A function tagged concurrency may also contain a loop; these are not independent feature effects. The authors’ ten new programs resemble the public set and are used for both selection and the full study. Their non-leakage is asserted, not independently established; a low overall verification rate cannot itself measure contamination (Q3,Q12). Three inputs retain executable code but differ in guidance: NL gives informal behavior, FB formal pre/postconditions, and FBP adds allocation ownership or integer constraints needed for verification. FBP is closer to a complete solution and asks a different completion task from NL. Paper Table I’s append-tail example specifies an acyclic input/output list; Figure 1’s contract tracks ownership and acyclic shape, not a value sequence, preserved prefix or insertion of exactly one value. A program satisfying only that contract has not thereby proved the full usual append operation. The retained artifact’s list nodes omit the value field and its append_tail takes only head; this is a simpler example variant, not a byte-identical implementation of Figure 1 (Q2,Q3,T1,F1,C10). ## Prompt/model selection and measured workflow Four prompt contents, Basic, chain-of-thought, sparse retrieval and dense retrieval, cross whole-program versus function input for eight choices. The first pilot uses GPT-4o and the 45 new functions’ FBP variants. Sparse retrieval with function splitting verifies 64%, versus at most 56% for alternatives, with 63 errors versus more than 67; its three logical errors and two behavior changes also influence selection. These are selection-set results, not independent held-out estimates (Q4). A second pilot chooses Claude 3.7 Sonnet, Gemini 2.5 Pro and GPT-4o from ten models: selected models verify at least 60%, have at most 73 errors and at most two behavior changes. A follow-up crosses ten models with eight prompts over the same 45 FBP functions; however, deprecated Claude 3.7 is replaced by Haiku 4.5. It therefore supplies broader prompting evidence without evaluating exactly the same model set. Sparse split and unsplit tie at median 16 verified functions; selected model families’ reported medians are 23, 22.5 and 20.5, versus at most 15 for the rest. It does not remove reuse of the selection set or isolate all input/model interactions (Q5). The full study fixes sparse retrieval with splitting and evaluates three models × three input types × 303 functions, producing 2,727 outputs. Temperature is zero, with one output per condition, not repeated sampling. Sparse retrieval uses BM25, dense retrieval TextEmbedding, and vectors reside in Qdrant. The retained prompt code retrieves ten program/library entries and five tutorial entries, caps concatenated example text at 300,000 characters and extracts C-fenced blocks. Main generation calls each model once per input, without a verifier-feedback loop. The code’s active model list is the later ten-model configuration including Haiku, not a preserved exact full-study configuration; historical correspondence needs logs (Q4–Q8,Q12,C6,C7). Reported local hardware is a Yoga 14sACH 2021, 16 AMD Ryzen 7 5800HS CPUs, 16 GiB RAM, 1 TB SSD, Ubuntu 24.04 and Python 3.12; Qdrant has 0.5 vCPU, 1 GiB RAM and 4 GiB disk. Full-study API costs per model are Gemini $233,Claude$232 and GPT-4o 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` - 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` - ASSESS (2026) - title: ASSESS: A Semantic and Structural Evaluation Framework for Statement Similarity - what: It parses two Lean statements into trees and tries to prove them equal. If that fails, it scores partial similarity by counting the tree edits that remain. - number: EPLA benchmark 1,247 pairs: 831 miniF2F, 416 ProofNet - number: search limits 32 nodes, 10 minutes - number: miniF2F precision/recall/accuracy/Kappa 87.97%/69.06%/70.16%/0.35; ProofNet 68.49%/81.97%/67.31%/0.30 - limits: It covers mathematics only. The distance is an upper bound that is cheap to compute. The thresholds were tuned on the same benchmark they were tested on. - how much was read: most of it read - source; notes: ASSESS: A Semantic and Structural Evaluation Framework for Statement S - record id: `assess-2026` - Assessing Postcondition Completeness in Auto-Generated Function Contracts for Software Verification (2026) - what: For a deterministic program, a postcondition (what must hold after the function runs) is complete exactly when it fixes one output for each valid input. That is the strongest possible postcondition. Checking this needs only the candidate spec, with no tests and no reference implementation. A proof of concept is in OpenJML. - number: completeness feedback loop: up to 50.0% effectiveness in improving completeness, up to 10.7% of total complete successes - number: SpecGen rerun with GPT-3.5 Turbo: non-incorrect rates 58.6% (SpecGen) and 51.4% (conversational) versus 72.3% and 64.2% originally reported - limits: It works only for deterministic functions in Java with JML specs. The one-output test does not carry over to non-deterministic distributed protocols. - how much was read: most of it read - - record id: `assessing-postcondition-completeness-in-2026` - AutoSpec (protocol) (2026) - title: Synthesizing Precise Protocol Specs from Natural Language for Effective Test Generation - what: It extracts states, messages and constraints from RFCs into executable grammars. It tests Dovecot, Postfix, vsFTPd and Pigeonhole with Fandango, and repairs the grammars from traces. Experts wrote golden grammars to serve as the oracle (the reference answer). - number: POP3 295 lines/3.5 h; SMTP 373/9.5 h; IMAP 676/14 h; FTP 576/5.5 h; ManageSieve 449/5 h (golden grammars) - number: average recall 92.8% and 80.2% for client/server messages and independent constraints, 16.7% and 0.0% for dependent constraints (the notes list four values after 'Average') - number: abstract average 81.5% message acceptance - number: Message types recovered 92.8% (client), 80.2% (server) - limits: It misses dependent constraints entirely. Repair guided by execution may end up matching a buggy server. FTP data channels are excluded. Counts in the tables are inconsistent. The tool release is only planned. - how much was read: most of it read - source; notes: Synthesizing Precise Protocol Specs from Natural Language for Effectiv - record id: `autospec-protocol-2026` - Beyond Benchmarks / Vostd FVT (2026) - title: Beyond Benchmarks: A Case Study of LLM-Generated Verus Specification Failures on Asterinas Vostd - what: The authors ran three LLMs to write Verus specifications for six real verification targets in Asterinas, a Rust OS kernel, directly inside its repository, then hand-labelled every failed attempt by where it broke: the code did not fit the repository, broke Verus's own rules, modeled the wrong thing, or lacked proof structure. They also checked whether the verifier's error message pointed at the real cause. - number: 6 targets, 156 function-level tasks, 50 Rust files, 7,149 lines - number: 1,587 reviewed failure episodes: Stage I repository integration 442 (28%), Stage II Verus legality 502 (32%), Stage III semantic modeling 420 (26%), Stage IV proof construction 223 (14%) - number: benchmark verify rates 66.0% to 82.6% (Table 3 subtotals); on the 6 targets AutoVerus 22.7-24.5%, VeruSAGE 34.4-41.7%, the authors' workflow 66.3-68.7% - number: visible verifier diagnostic matched the true source stage in 1,152 of 1,587 episodes (72.6%) - limits: One project (Vostd, Entity-Model proof style) and three LLMs; stage labels come from the authors' manual review with no second reviewer reported; the authors' own workflow was built for this study. Covers specification generation, not distributed protocols or liveness, and the paper itself says the three LLMs are not a leaderboard. - how much was read: most of it read - source; notes: Beyond Benchmarks, Verus specification failures on Asterinas Vostd (20 - record id: `beyond-benchmarks-vostd-fvt-2026` - Can Code Specify a System Precisely Enough to Formally Verify It? (2026) - what: Audits a deployed restaurant point-of-sale payment workflow (register, payment terminal, Finix backend). The authors built TLA+ models with Claude agents under their supervision. They also compared LLMs generating specifications from the TypeScript source in three forms: library-based JavaScript, a bare JavaScript next-function, and TLA+. - number: pre-fix models have 43-103 states, check in under a second, counterexamples 6-9 steps - number: 7 original gaps found, 3 reproduced on the unmodified code with its emulator - number: final failure-enabled model has 376 distinct states; 24-hunk patch; passes all 23 scenario tests - number: 105 generations (7 models x 3 contracts x 5), each replayed on 101 observed transition windows - limits: Every checked property is a safety invariant (a fact true in every reachable state) on finite, simplified models, not on all executions of the TypeScript. Timeout liveness is not checked. The model and the emulator shared a wrong reading of how Finix responds to a duplicate key. There is no mechanical proof that code matches model. Crashes and power loss remain accepted risks. - how much was read: most of it read - source; notes: Can Code Specify a System Precisely Enough to Formally Verify It?; notes: Can Code Specify a System Precisely Enough to Formally Verify It? - record id: `can-code-specify-a-2026` - Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation (2026) - what: # Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation (authored by agents unless marked 🧑) Bisharat, Ortiz, Spencer, Bhadauria, Wang, Thiruvathukal, Läufer and Abuhamad evaluate generation and completion of TLA+ specifications. The useful contribution is a public task, four prompt designs, checker outcomes, reference-text comparisons and a concrete error taxonomy. The experiment reports 2,600 open-weight runs and 130 proprietary-model runs. Its headline “semantic correctness” means an operational TLC outcome for a finite configuration. It does not establish correspondence to the natural-language requirements or equivalence to a reference behavior. Infrastructure failures, inconsistent counts and released evaluator differences materially limit the proposed ranking of strategies. The saved arXiv version is 2606.05792v1, dated 4 June 2026. The publisher first page identifies ICSOFT 2026, pages 39–50, DOI 10.5220/0015070400004088 (B1). This record reads the entire 12-page arXiv paper, including all 34 references and 11 tables. All 12 pages were inspected as rendered images. There are no figures, numbered theorems, mathematical proofs, appendix, checklist or separate algorithm listing. The publisher PDF was acquired and its first-page bibliography inspected; no byte identity or complete final-version comparison is claimed. The FormaLLM source is pinned to b159f5df093e7ed71f4793bba99459b97a2bb23d, dated 2 April 2026. Twenty-four selected plaintext files were read: documentation, split and prompt code, SANY/TLC evaluators and collectors, completion metrics, four pipeline files and three graph helpers. Identical files were checked by bytes and read once. The complete 1,864-entry tree was inventoried, not wholly read. Original/generated specifications, recorded checker outputs, full corpus/splits, run.sh, unselected analysis scripts and cited papers were not read. No author code was executed or imported; no models, checkpoints or serialized datasets were loaded. Source correspondence to the published historical runs remains unknown. quotes.json preserves 43 exact excerpts with source, line, character and section pointers; numeric_tables.json preserves all 11 literal table blocks and reader arithmetic. ## Task, inputs and experiment The corpus contains 205 specifications from 98 TLA+ Examples projects, including consensus protocols, concurrency examples and puzzles. Table 1 lists 92 with both comments and configuration, 14 with only configuration, 95 with only comments and four with neither; totals are 106 with configurations and 187 with comments. Thus “205 paired specifications” needs qualification. The paper reports a project-stratified 143/31/31 train/validation/test split, with five test exclusions leaving 26 evaluated specifications (Q1,T1). Training supplies examples; validation tunes prompts/hyperparameters. These are public repository comments rather than new, independently elicited requirements. No contamination or memorization analysis is supplied. Twenty-five open-weight models use four strategies; five proprietary models use only few-shot prompting. This gives 25×26×4=2,600 plus 5×26=130 runs. Table 2 preserves model aliases, reported token counts and contexts. Its many `latest` aliases, missing Qwen3:4b context cell and unexplained extreme totals such as 1,141.7K for r1:1.5b limit exact model/budget reconstruction. These token summaries are not measured end-to-end time, price or energy. The “eight families” combine architecture families with overlapping categories such as code specialization and proprietary APIs; they are the authors' grouping, not eight independent experimental factors. Few-shot (FS) supplies three training comment/specification examples and target comments. Progressive (Prog.) supplies three examples plus instructional messages about module structure, variables, operators and temporal properties. Fill-in-middle (FIM) supplies the first and last 30% of the reference and asks for the middle 40%. Half-completion (HC) supplies the first 50%, comments and configuration and asks for the remainder (Q2–Q4). Completion therefore receives substantial correct reference code and tests a different task from full generation. In selected source, full-generation prompts also include the original configuration, while the written generated configuration becomes the preferred checker input (C10–C11). The paper says SANY passes on “Parsing completed” with a 30-second timeout, then sends passing specifications with configurations to TLC (Q5). Textual measures apply to the generated reference segment: BLEU, ROUGE-L, edit distance, exact match and line accuracy. Source C13 defines line accuracy by matching line subsequences divided by reference line count, character similarity by SequenceMatcher, character edit distance, whitespace-token BLEU and default ROUGE tokenization. These are textual measures; different but equivalent specifications can score poorly, and reference overlap does not establish correct behavior. ## What the tables report Table 3 reports SANY FS173/650, HC80/650, Prog162/650 and FIM92/650. TLC is FS0, HC0, Prog56 and FIM0, with the Prog rate 8.6%. These are printed experimental outcomes, not independently rerun results. Table 5 distributes those outcomes across models, and Table 10 across specifications. The strongest listed individual open-model TLC result is DeepSeek r1:8b with14/26=53.8% under Prog; Qwen235b has12, Qwen30b10, GPT-OSS20b6 and Phi-mini4. These individual rates differ from the aggregate 8.6% headline. Table 6 is essential to the headline's scope: under FS, GPT-5 reports SANY26/26 and TLC7/26; Sonnet4.5 reports24/26 and3/26, Haiku4.5 reports21/26 and3/26, Opus4.1 reports23/26 and1/26, GPT-4o reports20/26 and1/26. Thus “only progressive” applies to the open-weight multi-strategy experiment; it is false as an unqualified statement about all30 models. Likewise 26.6% is an aggregate open-strategy syntax rate, not the maximum individual result. The sentence calling GPT-5's26.9% TLC “comparable to the open-weight FS ceiling” conflicts with the reported open FS0% (Q7,T3,T6). Tables 7 and9 preserve all per-model completion similarities. Table 3 reports mean BLEU HC.062/FIM.077, ROUGE-L .189/.213, line accuracy10.90%/12.27%, and exact matches0/650 versus1/650. Table 7 instead prints FIM average12.37%; reported dispersions also differ across summary and detailed tables. The one FIM exact match together with zero TLC passes is another reason to inspect infrastructure/configuration before interpreting zero as behavioral failure. Table 8 reports bad-module-body first errors FS228,HC264,Prog243,FIM290; other parse errors72/227/70/191; unexpected-token errors82/29/65/17. These are not all categories. Its first-error location counts sum to477/570/488/558, matching 650 minus the Table 3 SANY totals. A first detected error does not count all defects. Early/middle/late thirds are the paper's definition; the selected collector instead labels absolute line numbers below10 and below50 (C14), so the published calculation needs a different, identified analysis path. Table 10 gives examples rather than a simple “distributed is harder” result. YoYoNoPruning has100% SANY for HC/FIM; HDiskSynod has FS32%, Prog20% and FIM48%, contradicting the prose example that it scores0%. BinarySearch has12%FS/24%Prog syntax and8%Prog TLC. The highest listed per-spec Prog TLC rate is16%, shared by EnvironmentController, MultiPaxos, VoucherCancel and YoYoNoPruning. MCDieHarder has zero TLC across strategies. Multiple spelling/wrapping forms are retained in literal rows; no semantic equivalence across similarly named modules is assumed (Q10,T10). ## Infrastructure confounding and inconsistent totals Table 3's footnote explicitly says zero TLC rates “reflect failures (i.e., State Directory Conflicts and Module Not Found errors).” Table 4 labels97.2%/99.2%/99.2% of FS/HC/FIM failures as infrastructure and9.8% for Prog. A pipeline unable to load a module has not tested its behavior. Calling invalid configuration a “genuine semantic” failure also does not establish a mismatch between the generated transition system and intended requirements. These failures can be important practical generation defects while remaining distinct from behavioral incorrectness (Q6,T3–T4). Table 4 is internally incomplete or inconsistent. Its displayed module/configuration rows sum FS177,HC164,FIM161 against totals650 each; an unlisted state-directory category might explain some gaps but is not numerically supplied. For Prog it gives122 TLC failures,455 parse failures and56 passes, totaling633 rather than650. Table 3's162 SANY passes imply488 parse failures. Moreover122+56=178 exceeds162. The record retains these printed claims and cannot reconstruct a valid common denominator from them. Reader arithmetic over Table 5 gives column totals FS173/0,HC78/0,Prog162/56,FIM92/0. Table 10 implies HC80, matching Table 3 but conflicting with Table 5. Table 5's averages6.92,3.17,6.38,2.08,3.71 differ from row-derived6.92,3.12,6.48,2.24,3.68 for the corresponding nonzero columns. Also80/650=12.31%, whereas Table 3 prints12.2%; Qwen30b's23/26 is88.46%, whereas its best-model cell prints92.3%. No source output logs were inspected to settle which transcription or analysis is wrong. ## Claims about models, causes and error repair The observed results support some nonmonotonic size comparisons. They do not support “r1:8b outperforms70b across all strategies”: HC SANY is1 versus3 and FIM3 versus3. The claim that LLaMA1b's12 Prog SANY passes are highest among all LLaMAs conflicts with both3.3 variants'18. “Just three model families” conflicts with the paragraph listing DeepSeek,Qwen,GPT-OSS,Phi and Table 5's Gemma pass. Model training, instruction alignment, context limits, prompt interaction and output processing are not separated by a controlled factorial study (Q6,Q8–Q9,T5). The authors attribute poor code-model performance to negative transfer, operator substitutions to rendered mathematics and reasoning leakage to training. These are proposed explanations. They did not manipulate training data, measure causal mediation, run controlled fine-tuning ablations or establish statistical significance. “Not noise” is especially strong given their explicit limitation: “We run each model-specification pair once per strategy” (Q14). More heterogeneous tasks do not substitute for repeated measurements of a given model/task condition. Table 11 and §4.4 give five categories: Unicode operator substitutions, syntax from other languages, reasoning/formatting leakage, length miscalibration and module structure. Semicolon first-error counts are18/11/25/10, while file-presence scans count49/23/82/22; these have different denominators and meanings. Backtick counts are28/10/21/13; think-block counts15/30/not-applicable/28. The paper says QwQ contributes26/26 HC and FIM think blocks. It reports mean output/target length HC3.46× and FIM2.24×, with9.84× as an extreme. These are observed author counts, not a controlled explanation of accuracy (Q11–Q13,T11). The claimed243+ missing Prog terminators numerically matches Table 8's243 bad-module-body first errors, but that broad parser category is not equivalent to an independently counted missing terminator. The selected generator also appends a terminator. The historical counting path is unresolved. A semicolon-presence scan is not itself a syntax-error test: semicolons can occur within comments, strings or PlusCal text. Similarly a blanket claim about all Unicode needs a tool-version/context boundary. Suggested grammar constraints, retrieval, normalization, fence removal and checker-guided repair are future interventions here. Their correctness and benefit were not measured; indiscriminate character deletion could change intended content (Q13,Q15,C16). ## Released source qualifications The primary parse step checks return code0 plus a success substring (C1–C2). Its separate metrics collector computes `parse_success` from that substring and error keywords but never uses it to return status: it returns PASSED whenever its line-number regexes find no errors (C3–C4). By static inspection, a present empty/unrecognized-error log can therefore receive PASSED in that collector. This is a source-level possibility; it is not a measured false-positive rate in the paper. The selected TLC loops iterate every parsed dictionary entry and ignore `parse_status`, contrary to the paper's stated filtering. They prefer any generated configuration file, even an empty one, before fallback to the corpus; full generation writes one. Hence the checker may assess model-selected properties/configuration rather than an independently fixed behavioral oracle. The success collector accepts “Model checking completed. No error has been found.” before checking exit status. The alternate progressive evaluator instead accepts “The specification is correct”; the two strings are different. TLC subprocess calls have no Python timeout, despite TIMEOUT classification later; clearing `generated/states` without setting a working directory/metadir does not establish isolation of TLC's actual state directory. These observations require run-path/log validation before assigning them to historical results (C5–C7,C11). The split helper performs unseeded flat `random.shuffle`, not project stratification, and floor slicing205 gives143/30/32 rather than143/31/31. Selected prompts read val.json rather than test.json. Those labels may have been repurposed by uninspected run tooling; this record cannot certify the published test set from the selected code (C8,C15). The `fifty-fifty` and `fill-in-middle` prompt files are byte-identical and implement30/40/30 completion; their metric files are also identical. This does not reproduce two distinct completion designs. The progressive prompt accumulates instructional messages and makes one `llm.invoke` per target; it does not execute separate checked module/variable/operator generation stages. Its cleaner removes fences and explanatory text, adjusts headers and appends `====`, as do other selected generators. Thus Table 11's FIM cleanup footnote does not establish cleanup unique to FIM. The source/documentation mix should not be silently treated as the exact experimental pipeline (C9,C11–C12,C16). ## Contribution to this literature effort The paper is directly relevant to evaluating LLM-written distributed-system specifications. It supplies task definitions, public examples, prompt contrasts and failure cases. Its strongest lesson is methodological: separate parser success, tool execution, checked finite properties and faithfulness to intended behavior. The evidence does not justify treating an8.6% pipeline pass fraction as a measured semantic-equivalence rate, or infrastructure-confounded zero passes as proof that a strategy cannot generate valid behavior. A reader recommendation is to use fixed independent configurations/properties, inspect explored states and vacuity, compare behaviors or traces against requirements, isolate checker paths, publish per-run logs and exact model versions, repeat runs, and report infrastructure failures separately. The recommendation extends beyond the paper's measured interventions. This study verifies no Verus/Rust implementation and proves no distributed protocol. It evaluates draft TLA+ artifacts rather than an autonomous multi-agent proof process. Prose consultation is complete; independent review is pending. REVIEW.md records consultation scope and disposition. This is a whole-paper reading with selected static source inspection, not an experimental reproduction. Fresh independent review found no material conclusion issue; two table-packaging defects were corrected (REVIEW.md). All11tables/34refs,43literalquotes,16diagnostics;operational-vs-behavioral correctness,infra confounding,count arithmetic,proprietaryresults,source evaluator/split/prompt discrepancies. - number: 143 training, 31 validation, 31 test specs; 26 eligible test specs used - number: GPT-5 26/26 syntax and 7/26 TLC passes (26.9%) - number: 8.6% aggregate open-model TLC success (56/650); DeepSeek r1:8b 14/26 - number: 2,600 open-model runs plus 130 proprietary runs - limits: Public comments and26finite configured test specs;one run percondition;inconsistent counts;infra failures;NLfaithfulness notestablished;no authorcode/checker rerun;selected release correspondence uncertain. - how much was read: most of it read - source; notes: Natural language to temporal logic and TLA+ - record id: `can-llms-write-correct-2026` - CircuitProver (2026) - title: CircuitProver: Agentic Lean 4 Theorem Proving with Reusable Circuit Proof Library for Hardware Verification - what: Introduces CircuitProver, a Lean 4 framework that translates parameterized Chisel hardware and natural-language specifications into Lean, uses an agent to iteratively construct machine-checked proofs, and distills proof trajectories into reusable guidance and theorem libraries. The deterministic Chisel-to-Lean translator preserves parameters, interfaces, registers and width-aware bitvector transitions; small-width co-simulation checks the translation. Agents formulate Lean specifications, build hardware-aware scaffolds, prove one-step/invariant lemmas, and repair scripts using Lean feedback. Two libraries separate reusable proof plans from module-independent checked theorems. The carry-skip-adder case extracts a block recurrence, full-width radix closure and targeted representation repair. The 63-task suite spans arithmetic/control/memory/miscellaneous designs plus XiangShan/Rocket arithmetic modules, with ablations isolating guidance and theorem-library effects and model-scaling comparisons. - number: 63 benchmark tasks: 34 arithmetic, 9 control, 9 memory, 11 miscellaneous - number: 63/63 CircuitProver; 58/63 vanilla; 31/63 Chicala/Stainless - number: 50.0% fewer proof rounds - number: 23.2% lower verification time - limits: The frontend supports only a subset of Chisel and generated Lean models are validated by exhaustive small-bit-width co-simulation, not all parameter widths. Success requires a final Lean file with no sorry/admit/axiom/unsafe. Cost averages are over solved tasks, so comparisons have different coverage. Results use Claude agents and a benchmark authored by the researchers; industrial RTL, richer properties and broader designs remain future work. Natural-language specification formalization still requires semantic agent reasoning. - how much was read: most of it read - - record id: `circuitprover-2026` - ClarifySTL (2026) - title: ClarifySTL: An Interactive LLM Agent Framework for STL Transformation through Requirements Clarification - what: Detects vague or ambiguous timed requirements written in plain language. Asks the person targeted questions. Then generates signal temporal logic (a formal language for timed properties). - number: AmbiEval dataset 9,200 labeled instances - number: ten participants with at least three years of STL experience - number: Table 3: ClarifySTL DeepSTL formula score 67.12, semantic agreement 82.7; STL-DivEn 70.74 and 84.9 - number: +13.92% formula accuracy over the prior best on DeepSTL - limits: Formula accuracy is measured by how many tokens match, not by exact equivalence. Tested only with experienced users. No safety proof for cyber-physical systems. No public artifact. - how much was read: most of it read - source; notes: ClarifySTL: An Interactive LLM Agent Framework for STL Transformation ; notes: papers - record id: `clarifystl-2026` - CodeSpecBench (2026) - title: CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation - what: CodeSpecBench is a benchmark where a model writes executable Python pre- and postconditions. The input is either a function description or a real repository issue. A harness checks that the conditions accept valid tests and reject invalid ones. - number: 2,494 function tasks and 500 repository tasks from 12 projects - number: 96.3% statement and 93.6% branch coverage - number: 67.8 incorrect test cases per problem - number: best strict pass: 47.0% (GPT-5-mini) on function tasks, 20.2% (Claude-4.5-Sonnet) on repository; Appendix table says 21.0 - limits: It uses finite tests only. Localization and tests are supplied. The repository figures are inconsistent across tables. The comparison of solution generation mixes in numbers from model reports. - how much was read: most of it read - source; notes: CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specificati - record id: `codespecbench-2026` - COINS specification evaluation (2026) - title: How Powerful Are LLMs in Generating Formal Program Specifications? - what: Introduces COINS (COq-based INstantiated Specification evaluation), which judges a generated input/output predicate by Rocq proofs on positive and mutated negative test cases. It separates specification quality from implementation conformance and makes successful proofs sound evidence while treating failed proofs as ambiguous. Sections 2–3 define implementation-agnostic pre/post specifications, the four-stage SYNTAX, PASSfirst, PASSall and REJECTall pipeline, and the sort-third example. Appendix A gives AST and LLM mutation operators, input perturbation, one-second execution limits and 1,640 generated negatives. Appendix B models an LLM prover probabilistically and proves that failed verification cannot distinguish a false specification from a hard true one. The main experiments compare six API models, study Fixpoint versus Inductive styles, equivalence to human specifications, input-type difficulty, Rocq compiler errors, and proof failures such as phantom goals, library predicates and normalization resource exhaustion. HumanEval/12 exposes a compiling but contradictory longest-string specification on duplicate maxima. - number: 164 tasks - number: 123,952 positive tests - number: 1,640 negatives - number: >100,000 proof attempts - limits: Specifications are functional input/output Props and intentionally omit exceptions, memory layout and other operational artifacts. The 164 human references were manually reviewed but are not absolute ground truth. Positive evidence is sound only because Rocq checks proofs; rejection of negatives is incomplete because an LLM may fail to find an available proof. Candidates can still miss behaviors outside the test suite. Scope is 164 HumanEval tasks, Python descriptions/implementations and Rocq; scaling requires substantial annotation and compute (over 100,000 proof attempts). - how much was read: most of it read - - record id: `coins-specification-evaluation-2026` - Collaborative and AI-Supported Requirements Elicitation: An Empirical Study (2026) - what: Compares ways of gathering requirements. Stakeholder collaboration plus AI synthesis produced the requirements documents that were rated highest. - limits: Ratings of documents do not show how strong a formal guarantee is, and do not replace validation with the affected users. - how much was read: most of it read - source; notes: Clarification and stakeholder requirements - record id: `collaborative-and-ai-supported-2026` - Decompose, Structure, and Repair: A Neuro-Symbolic Framework for Autoformalization via Operator Trees (2026) - what: Presents DSR, a statement-autoformalization pipeline: Gemini 3.0-Pro decomposes informal mathematics into conditions and conclusion, a Qwen2.5-7B-Instruct formalizer produces Lean components and operator trees, and Qwen3-Max repairs compiler-localized subtrees before a mandatory whole-statement semantic review. Introduces PRIME, 156 manually formalized textbook statements with informal proofs. Reports highest LeanScorer consistency scores among main Table 2 methods (84.00/79.51/67.95% on ProverBench/ProofNet/PRIME), while syntax scores and supplementary FATE results are more mixed. This evaluates statements ending in admitted proofs, not completed verified theorem proofs. Operator trees are labeled ordered scope trees derived with ASSESS/Lean Language Server, adapted to component granularity with parentheses retained. Training constructs 283,958 NL-component/Lean-component/tree triples from 120,627 NuminaMath-LEAN+ATLAS-Synthetic statements, using Qwen3-Max backtranslation. It filters extreme tree complexity, retains 281,209 examples in simple/moderate/complex tiers, and applies four one-epoch LoRA phases with replay. Assembly prioritizes tree reconstruction and falls back to linear components for malformed trees. Repair maps compiler row/column to a tree node, expands bottom-up from parent subtrees through component and full statement, with one pass per repair attempt. Local prompts omit informal text; component prompts see the informal component; the final whole-statement prompt restores full informal context and checks semantics even when compilation succeeds. - limits: Syntax Check (SC) is Lean 4 v4.15.0 compilability. Outputs intentionally end in by sorry; passing SC establishes a well-formed admitted statement, not its truth, consistency of premises, semantic correspondence or a proved theorem. Consistency Check (CC) is LeanScorer using DeepSeek-V3.2 at threshold 0.6, not a kernel certificate of NL/Lean equivalence. The framework uses larger external models: Gemini 3.0-Pro for decomposition, Qwen3-Max for backtranslation and repair, and DeepSeek-V3.2 for evaluation. Calling the system 7B describes only its trained formalizer. No all-components fixed-parameter comparison follows from the smaller formalizer. Decomposition may infer missing domains or assumptions incorrectly; the source explicitly acknowledges error propagation. A 90-item manual sample reports 95.56% decomposition accuracy for Gemini versus 87.78% Qwen3-Max, not universal correctness. The final semantic check is another LLM repair call and supplies no formal semantic guarantee. PRIME covers 156 textbook theorems, not distributed-system specifications. Expert formal statements and informal proofs are supplied, but no full formal proofs or independent statement-quality audit is reported here. Textbook/domain selection and judge limitations constrain generalization. Appendix B.1 says PRIME Lean references were private/manual and shares only 4 conceptual overlaps with FATE-M. Domain separation and new reference strings do not exclude semantic overlap, textbook NL pretraining exposure, reuse of library facts or alternative formalizations; no exhaustive model-training-data audit is supplied. The stated four-call budget measures calls, not tokens, dollars or equal model compute. Calls differ across decomposition, component generation and local/global repair; exact component batching/counting and strict per-problem truncation are insufficiently specified. §4.2 says four total calls, but §4.4.2 says four refinements following initial generation. No seeds, confidence intervals or significance tests accompany the small main CC margins. On PRIME the best external main baseline is66.67% versus 67.95% DSR, roughly two of 156 items. Benchmark-level differences do not isolate structural complexity as the cause. Tree construction details are delegated to ASSESS; source lacks full LoRA rank/alpha, hardware, decoding and complexity-tier threshold/combination details. Table 1 specifies one epoch per phase, batch 128/128/128/64, learning rates 2e−4/1e−4/5e−5/1e−5 and replay ratios, but not every reproducibility choice. All results are author-reported. No model, benchmark repository, LeanScorer, compilation trace or proof artifact was rerun by this reader. - how much was read: most of it read - - record id: `decompose-structure-and-repair-2026` - Djinnlang (2026) - title: Djinnlang: Higher-Level Programming by Unambiguous Specification with an LLM in the Compiler - what: Proposes Djinnlang, a specification-only language whose translator emits Dafny relations and proof/implementation obligations, then uses an LLM to fill implementations and proofs checked by Dafny. Its central unambiguity constraint requires the specification relation to be deterministic, eliminating semantic freedom for the generated implementation; procedures add ordered effects through generated step machines. The paper formalizes unambiguity as pre(x) ∧ q(x,o1) ∧ q(x,o2) ⇒ o1=o2 plus an existence obligation, and distinguishes deterministic funcs, nondeterministic rels, and effectful procs. The translator pins regenerated declarations, scans solutions for Dafny escape hatches, and re-translates the source before verification. Examples show sorting via a permutation relation, string parsing as a preimage, Sudoku and optimal LZ77 specifications, and a step-function compilation of procedures. Bootstrapping djinnc itself required 2,106 obligations and found four genuine specification bugs before synthesis succeeded. Two LLM implementers discharged all benchmark obligations, but generated performance differed by hundreds-fold. - number: three benchmark programs; 256 obligations - number: djinnc: 4,088 Djinnlang lines, 487 declarations, 2,106 obligations - number: Codex 33 minutes/47 versus Claude 21 hours/1,026 - number: Sudoku optimized 0.13s Claude versus 47.84s Codex - limits: The trusted base includes the human specification, translator, Dafny/Boogie/Z3, ambient types/helpers, generated drivers, and external I/O glue. Compilation may time out without distinguishing unsatisfiable specs from hard proofs or weak models; concurrency, interleaving, timing side channels, and performance bounds are outside the current language. The specification is still the main source of intent errors. Benchmarks use Dafny and LLM-generated specs that authors checked manually; results do not establish general LLM reliability. - how much was read: most of it read - - record id: `djinnlang-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` - 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` - 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` - 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` - 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` - Intent Formalization (2026) - title: Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents - what: This research agenda argues that only the user can judge whether a spec is correct. It calls for support from tests, mutation, interaction and rich logic. - number: TiCoder study with 15 professional developers: correct evaluation of AI code from 40% to 84%; cognitive load dropped (p = 0.007) - limits: It is not a controlled benchmark. - how much was read: most of it read - source; notes: Intent formalization: why one number is insufficient - record id: `intent-formalization-2026` - JS-SAM (2026) - title: Executable JavaScript as a Checkable Specification Language: A JS-SAM Case Study on SysMoBench - what: This controlled study compares LLMs writing JavaScript (SAM) specs against TLA+ specs of real systems. The authors check the specs by bounded exploration, plus replay against traces captured from the running systems. - number: 4 models, 5 generations per cell - number: Spin traces: 28 windows, 8 of 18 observable input combinations covered - number: small tasks 40/40 complete passes; Raft scale 0/20 initially, 6/20 after one repair round - number: state-changing conformance of original models ranges 0-86.4% though all pass syntax and invariants - limits: It checks no liveness or temporal properties. It explores only to a bound. It does not prove that the implementation matches the model. The author designed the instrumentation, the reference model and the prompts. - how much was read: most of it read - source; notes: JS-SAM: a controlled case study separating specification shape from la; notes: JS-SAM: a controlled case study separating specification shape from la - record id: `js-sam-2026` - 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` - 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` - 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` - 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` - NL2VC-60 (2026) - title: From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification - what: Introduces NL2VC-60, 60 complex algorithmic problems paired with Dafny code/specifications, and evaluates seven open-weight LLMs under contextless, signature-guided and verifier-feedback prompts. uDebug tests combat vacuous proofs by requiring executable functional correctness. Tiered prompting supplies method signatures as structural anchors, then iterative Dafny compiler feedback repairs annotations/code. The study categorizes errors (compilation, specification, proof, functional) and compares verify@k. Contextless prompts almost universally fail; signatures reverse performance, and self-healing further improves models. - number: Gemma 4-31B reached 90.91% verification success - number: GPT-OSS 120B rose from 0% to 81.82% with signature feedback - number: Contextless peak verify@5 27.27% at T=0.8 - number: NL2VC-60 contains 60 problems; seven open-weight models; 11 randomly selected sets - limits: Dafny specifications and uDebug tests are trusted; tests cannot establish full semantic correctness. Dataset has 60 problems and 11 selected sets; generated solutions may overfit signatures/prompts. Open-weight model results and Dafny syntax may not transfer to Verus/Rust. - how much was read: most of it read - - record id: `nl2vc-60-2026` - OSVBench (2026) - title: OSVBench: Benchmarking LLMs on Specification Generation Tasks for Operating System Verification - what: A benchmark in which an LLM writes a Python/Z3 specification of a syscall from a description. The spec is scored by whether it detects the same injected errors in code variants as the reference spec does. Declaration specs stay fixed. - number: 245 tasks from 49 system calls, 5 variants each (1 correct, 4 with injected bugs) - number: 12 LLMs; best pass@1 55.10% (Doubao-1.5-pro); five zero-shot models score zero - number: five-example prompts use 20,000-30,000 tokens - number: 245 tasks from 49 system calls (each: one correct and four vulnerable variants) - limits: It covers functional and safety properties only, with no liveness. The LLM is given a description, assumptions and an abstract kernel model. - how much was read: most of it read - source; notes: OSVBench: executable specifications with a fixed external oracle; notes: OSVBench: executable specifications with a fixed external oracle - record id: `osvbench-2026` - Proofs Promptly (2026) - title: Proofs Promptly: An Experience Report on Proof-Oriented Programming with AI Agents - what: The report uses Copilot CLI with Opus 4.5, with skills, subagents and a REPL. It writes Pulse/F* separation-logic proofs of concurrent locks and semaphores, the MSQuic receive buffer, and a port of the OCaml garbage collector. - number: Table 1 p. 3: 1 week/1229, 1 week/$583,2weeks/$1580; about a month and 3,392 total (notes' addition) - number: Six-month manual estimate is the authors' estimate, not a controlled comparison - number: manual proof-engineering cost estimated at roughly half a year - number: three experts, two weeks, versus about half a year manually (authors' estimate) - limits: Experts review the specs and supply the invariants that decide the proof. It has no theorem about distributed fairness or eventual progress. - how much was read: most of it read - source; notes: Proof-oriented programming at Microsoft; notes: papers - record id: `proofs-promptly-2026` - Reality Is the Final Verifier: On Two Key Gaps in Agentic Software Engineering (2026) - what: Argues that verification stops short in two places. The written requirements may not match what the stakeholder wants (the requirement gap). The model used to evaluate code may not match the real environment (the model gap). Proposes an inner loop, which revises code against the requirements, the environment model and the evaluator. Proposes an outer loop, which uses observations from deployment to revise those inputs. - number: no new theorem, experiment, or implementation proof; Table 2 incidents are cited from other reports - number: No measured completion rate or human-hours; Table 2 incidents are cited from other reports - limits: A proposed architecture. No measured rate of autonomous completion and no human-hours result. - how much was read: most of it read - source; notes: Reality Is the Final Verifier: On Two Key Gaps in Agentic Software Eng; notes: Reality Is the Final Verifier: On Two Key Gaps in Agentic Software Eng - record id: `reality-is-the-final-2026` - RFC2TLA+ (2026) - title: RFC2TLA+: Extracting and Verifying Formal Models from RFC Documents using Continuous LLM Feedback - what: An LLM agent with 22 tools extracts communicating state machines and invariants from an RFC and emits TLA+. It refines the result using TLC counterexamples, for up to three rounds. - number: 14 real RFCs; all get a TLC-accepted model in best-of-three - number: correct models pass 36/42 runs; injected faults found 69/84 (33/42 deadlocks, 36/42 invariant violations) - number: synthetic RFCs 16/18 - number: avg 710 TLA+ lines (262-1,944); state F1 0.97, transition F1 0.61 vs 0.49/0.21 for RFC2PSM - limits: It uses TLC models checked within bounds, not code. Deadlock detection is weaker than liveness checking. The agent may change invariants, so a passing run does not show fidelity. No wall time or manual effort is reported. The artifact record is restricted. - how much was read: most of it read - source; notes: RFC2TLA+: extract both a model and invariants from a supplied RFC; notes: RFC2TLA+: extract both a model and invariants from a supplied RFC - record id: `rfc2tla-2026` - Seeking Specifications: The Case for Neuro-Symbolic Specification Synthesis (2026) - what: DeepSeek-R1 generates ACSL function contracts for C code. Optionally it also uses PathCrawler tests or Frama-C EVA alarms. The researchers check whether the contracts recover the intent, rather than preserve a recognized bug. - number: Table 1 bug recognition: Basic 47/60, Famous 9/30, Anonymized Basic 50/60, Anonymized Famous 14/30 - number: 50 programs, four variants, three generations each; 55 PathCrawler examples - limits: The study is qualitative. It has no end-to-end correctness proof of the generated contracts. By default the contracts encode the code, not the inferred intent. Figures 6 and 7 print the same contract despite opposite captions. - how much was read: most of it read - source; notes: Seeking Specifications: The Case for Neuro-Symbolic Specification Synt - record id: `seeking-specifications-the-case-2026` - SHADOWBENCH (2026) - title: SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization - what: ShadowBench has 178 math problems. Humans repaired Lean 'shadow' statements, which let Lean check implication in both directions between a generated statement and the reference. This scores semantic alignment without a human reviewing each output. - number: 178 problems, eight areas - number: about 10 minutes of human construction per problem; 85% initial-draft coverage - number: strongest configuration compilation/soft/full alignment 61.8 / 18.3 / 11.2 - number: agreement with experts 0.988, precision 1.000, recall 0.930 - limits: It covers mathematics, not software. Completeness depends on a trusted interpretation. Adapter failures give false negatives. - how much was read: most of it read - source; notes: SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignmen - record id: `shadowbench-2026` - SPCA (2026) - title: Robot Planning via LLM Proposals and Symbolic Verification - what: Sense–Plan–Code–Act combines LLM-produced world descriptions and PDDL with Fast Downward planning/TAMER validation, LLM-generated Python skills, compiler checks, and execution feedback in MiniGrid and Gazebo. Fresh/replan/repair PDDL uses o3; trusted-domain reuse uses o4-mini. Code generation uses codex-mini-latest. Domains become trusted after success in the same curriculum category. Planning repair permits eight attempts; syntax/interface code repair permits five per call, with separately bounded execution retries. Appendices A–F specify contact-based robot task verdicts, all prompts, context boundaries, AST patch merging and callback execution. The robot planner receives only a textual camera summary; the referee's ground-truth contacts are unavailable to SPCA. - number: MiniGrid 76/102 = 74.51%; 325 runs - number: Gazebo 22/31 = 70.97%; 131 runs - number: 8 planning repairs; 5 syntax/interface code repair attempts per call - number: 213 MiniGrid semantic repairs; 79.8% in ten levels - limits: Simulation-only; symbolic validation checks the LLM-supplied model and does not establish real-world correctness. The robot setup has single-view occlusion. Reported completion rates cover the full curricula, while runtime/repair statistics use the successful evaluated subsets (76 MiniGrid and 22 robot levels). Five trials per model/problem in the isolated planning test are explicitly indicative, not conclusive. Skill context growth and concentrated semantic repairs limit efficiency; no real robot or independent artifact execution was examined. - how much was read: most of it read - source - record id: `spca-2026` - Spec-Harness (formerly VeriAct) (2026) - title: VeriAct / Spec-Harness: Beyond Verifiability — Agentic Synthesis of Correct and Complete Formal Specifications - what: # Spec-Harness: Assessing and Guiding LLM-Synthesized Formal Specifications Beyond Verifiability (authored by agents unless marked 🧑) Md Rakib Hossain Misu, Cristina V. Lopes, Iris Ma, Yuangang Li and Shuvendu Lahiri, arXiv 2604.00280v3, 9 October 2026. This empirical study separates verifier acceptance from how well a generated contract describes behavior, then supplies four test-based scores to specification-writing agents. It reports stronger postconditions on held-out tests, with extra time and sometimes fewer verified tasks. These are finite empirical adequacy results, not proofs that generated contracts capture every intended behavior (Q0,Q14,Q17). ## Reading and evidence Read all 22 pages, sections 1–9, data availability and all 49 reference entries. Inspected all six figures, five tables and eleven numbered equations; viewed individual renders of pages 4–18. Official and inventory PDFs are byte-identical. No appendix appears. Reference entries were read but their papers were not recursively followed. The placeholder journal header is not treated as an identified peer-reviewed publication. The paper links Mondego/vACT. Inspected its metadata, complete nontruncated tree and fifteen acquired text/code blobs at commit 5b158553a05c38c39b3a029e38a99b020eb203c6, dated 29 June 2026. Four READMEs and the small configuration file were read completely; source-scope.json lists selected code ranges. The repository README describes the earlier title “VeriAct: Beyond Verifiability – Agentic Synthesis of Correct and Complete Formal Specifications” (C0). The pinned source predates the October paper and differs materially from its method. No experiment results were reproduced or independently attributed to this commit. No author code was executed/imported, no compiler/verifier/solver was run and no serialized benchmark, model or experiment was loaded. ## What the method measures The motivating changeCase contract restricts inputs to A through z and promises only an uppercase-range result for lowercase inputs. It excludes legitimate punctuation inputs and leaves the exact output underconstrained. The desired repairs go in opposite directions: weaken the precondition and strengthen the postcondition. The original, empty and exact specifications get reported mutation completeness rates of 0.36, 0.09 and 0.94. Of 33 code mutants, two are equivalent; some failures arise from a range check rather than the contract. A single mutation-kill score therefore neither isolates the defective clause nor proves that every failed verification detected a wrong output (Q1). Spec-Harness instead checks small harness programs with fixed inputs and outputs. Let ψ be the precondition and φ the postcondition. Postcondition checks use ψ⇒φ, with each JML specification case guarded by its own precondition. Precondition checks additionally include implicit non-null requirements from the stated verifier configuration. This guard makes a rejected valid input vacuously pass the postcondition check; the separate precondition metric is essential (Q7–Q9). PostCorr is the fraction of decided valid input/output checks satisfying ψ⇒φ. PostComp is the fraction of decided mutated-output checks satisfying ¬(ψ⇒φ), requiring both an admitted input and a rejected wrong output. PreCorr is the fraction of decided normally returning inputs admitted by the effective precondition. PreComp is the fraction of decided failing inputs rejected by it. Thus true postconditions can have perfect PostCorr and zero PostComp; false preconditions can have perfect PostCorr/PreComp but fail PreCorr/PostComp. These are complementary finite-test scores, not universal correctness/completeness theorems (Q7–Q9; reader examples). For each concrete check, the paper describes two parallel proof obligations, one for the predicate and one for its negation. Neither proving within 300 seconds makes the check undecided and removes it from the within-specification denominator. With contracted helpers, exactly one must prove; this guards against inconsistent helper assumptions proving both. The verdict is a proof about the generated stub under its encoding and verifier assumptions. It is not a proof about all inputs to the original method (Q7). For benchmark aggregation, a specification must also verify against the original method. Missing postconditions and changed code receive zero on all four metrics and remain in aggregate denominators. Pure helpers, annotations and braces around a single statement are permitted edits. A failed synthesis or a metric with no decided checks does not reach any positive threshold. PreComp denominators include only tasks with known failing inputs. PostHarness@τ is the fraction of all synthesis attempts whose PostCorr and PostComp both reach τ; it is distinct from the conditional share among only verified outputs (Q11). Input generation combines EvoSuite, parameter boundaries and inputs killing additional Major code mutants. The unchanged reference implementation/test driver labels normal returns as valid and exceptions/timeouts as candidate invalid inputs. Pools of at least 100 pairs are divided into disjoint feedback/evaluation lists, ranked by added branch and mutation coverage; five evaluation pairs are scored. Up to five deterministic output perturbations are intended, all different from the reference output. This assumes the reference behavior is an adequate oracle. A reference bug or a permissible alternative outcome is not ruled out merely by matching one recorded execution (Q10; reader oracle qualification). The first five pairs reportedly cover 98.7%/97.9% of branches and kill 89.1%/89.3% of Major mutants on SpecGenBench/FormalBench, versus 96.7%/92.3% and 81.3%/76.9% for shipped examples. Evaluation-side invalid inputs average 3.4/5.6 per task; 55/146 tasks have none. Array3d is excluded for unparsable output. High coverage of selected branch/mutant sets does not establish adequacy over untested behavior (Q10). ## Experiments and reported findings RQ1 compares Houdini, Daikon and eleven prompt configurations of SpecGen, AutoSpec and FormalBench using six models. The datasets have 120 SpecGenBench methods and 662 filtered FormalBench methods, drawn from 700 after excluding void/Object cases. Class/method names are normalized to Solution/solve. This evaluates reconstructing behavior from implementation, not formalizing independent natural-language intent. Void methods can in general have meaningful heap postconditions; excluding them limits this result rather than establishing that such contracts cannot be evaluated (Q2; reader qualification). The six models are GPT-4o (2024-08-06), Gemini 2.0 Flash, Claude Sonnet 4.6, Qwen2.5-Coder-32B, DeepSeek-Coder-33B and CodeLlama-34B. Prompt runs use temperature 0.7, up to ten SpecGen/AutoSpec refinement rounds versus three for FormalBench. There are 132 prompt/model/benchmark configurations plus four classical runs. OpenJML 21-0.21, Java 21.0.4, cvc4, non-null defaults, quiet arithmetic failures and a 300-second limit are stated. Sixty-four outputs with internal errors are excluded despite a verified indication (Q2,Q3). Table 2 reports Houdini verifying 113/120 and 443/662 tasks, Daikon 34/120 and 159/662. Best prompt-based results are SpecGen 82/120 (68.3%), FormalBench prompts 249/662 (37.6%); AutoSpec's FormalBench best in this table is 200/662 (30.2%). Figure 3 nevertheless prints 0.39 for AutoSpec zero-shot/Qwen on FormalBench. Section 5.8 explains that configuration verifies 255 unannotated outputs (38.5%) and Figure 5 selects the best configuration among outputs containing JML. Table 2's “Best” heading and RQ1 prose do not clearly state that same exclusion. Preserve these distinct selection rules instead of reporting 30.2% as the unrestricted maximum (Q3,Q4,Q14; reader cross-reference). Across 14,936 verified outputs, 3,395 (22.7%) lack postconditions, 1,888 lack JML entirely, 840 (5.6%) change code and 657 alter the method body. The union of no-postcondition/changed-code outputs is 3,839 (25.7%), so categories overlap; summing their percentages would double-count. Table 2's full per-approach counts and Figure 3's two heatmaps are retained in numeric-evidence.json (Q3,Q4). RQ2 uses GEPA/DSPy with GPT-4o as generator and reflection model, a medium budget and a stratified FormalBench split of 101/50/511 train/validation/test methods. Two SpecGenBench few-shot examples are removed from its 118-task evaluation. The numeric reward is 1 for verification, 0.3 for one verification error without syntax errors, 0.1 for multiple verification errors and zero for syntax errors/empty output; classified feedback also guides revision (Q5). Table 3's seed→optimized rates are: zero-shot 39.83→46.61% on SpecGenBench and 17.81→18.59% on FormalBench; few-shot chain-of-thought 46.61→44.07% and 19.18→19.77%; least-to-most unchanged at 45.76%/19.96%. No optimized prompt beats the best seed on either dataset. This finite experiment does not prove an inherent ceiling for verifier feedback, other optimizers, models or budgets (Q6; reader inference boundary). RQ3 scores 14,934 verified specifications after excluding two Array3d outputs. It does not reevaluate optimized prompts. Only 65.2% reach PostCorr≥0.75, 40.1% reach PostComp≥0.75 and 35.6% reach both; these percentages condition on verified outputs. Eighteen-point-nine percent have perfect PostCorr but PostComp below 0.25. Houdini's aggregate PostHarness@0.75 falls to about 2%/0%; 90.7% of its verified outputs with postconditions reject every valid tested input. Daikon often accepts observed outputs without discriminating wrong ones: 45.6% have perfect PostCorr and PostComp<0.25. Among verified prompt outputs, FormalBench prompts reach both thresholds on 64.4%/42.1%, versus SpecGen 44.0%/28.9% and AutoSpec 41.1%/25.3% (Q13,Q14). The instrument is imperfect. On 360 sampled specifications, five versus twelve evaluation pairs change threshold attainment by 2.1/1.6 percentage points on average and at most 5.6 points. The authors treat differences up to roughly six points as measurement resolution. Two blinded senior PhD raters assess 100 specifications and 64 individual checks. Before discussion, κ is 0.93 for completeness, 0.75 for adequacy and 0.94 for individual checks. Against consensus, PreCorr/PreComp κ are 0.72/0.70 and PostComp's completeness correlation is ρ=0.64. PostHarness@0.75 agrees on adequacy for only 67/100 specifications (Q12). On the 55 of those 100 specifications for which FormalBench CR is defined, CR correlates with human completeness more strongly than PostComp (ρ=0.72 versus 0.45). Only 27% of CR detections are postcondition rejections, versus 32% timeouts and 40% other verification failures; rounded percentages sum to 99%. The study supports more interpretable clause feedback, not uniformly superior correlation with expert judgment (Q12). RQ4 runs Claude Code 2.1.284/Sonnet 4.6, Codex 0.159.2/gpt-6.1-sol and VeriAct/gpt-6.1-sol at medium reasoning effort. Each gets ten tool calls, with or without the harness, on 120 tasks from each benchmark. Final evaluation uses disjoint held-out pairs and requires verification, a postcondition and unchanged code. Each agent runs once per task. The 12 agent/condition/benchmark combinations imply 1,440 task sessions; the paper's 720 sessions receiving harness feedback are the six with-harness combinations (Q15–Q18; reader accounting). PostHarness@0.75 increases on SpecGenBench from 0.52→0.62 for Claude Code, 0.60→0.75 for Codex and 0.57→0.63 for VeriAct. On FormalBench-120 it goes 0.23→0.28, 0.25→0.41 and 0.25→0.28. Exact McNemar tests find significance for Codex on both datasets and Claude Code on SpecGenBench (p≤0.005), but not the other three comparisons (p=0.18–0.45). Small gains also sit near the instrument's stated resolution; significance on the sampled task labels does not remove uncertainty about broader adequacy (Q12,Q17; reader qualification). Verification can worsen: Claude Code drops 0.86→0.74 and 0.68→0.45, Codex 0.88→0.88 and 0.74→0.69, VeriAct 0.90→0.88 and 0.87→0.68. Thirty-seven Claude Code tasks meet the harness target without verifying. Harness runs use 1.3–2.3 harness calls per task and take 1.4–2.2 times as long. Table 5 preserves all thresholds and precondition scores; at threshold1, VeriAct on FormalBench-120 drops 0.24→0.23. Neither universal improvement on every metric nor a free speedup follows (Q17). ## Static artifact comparison The acquired June source implements an earlier scorer. The following are explicit differences from the October description, not evidence that the reported October experiments used this source (C0–C9). The selected runner classifies generic warning/verification-failure/error text as FAIL. Pair evaluation credits FAIL as a killed output or rejected input, using one obligation rather than a proof of the negated predicate. Aggregation divides by all recorded details, retaining unknown checks; no exactly-one-of-two-helper-proof gate appears in these paths. The earlier standalone SpecHarness class behaves similarly. These paths cannot independently substantiate the later paper's “every verdict is a proof” implementation claim (C1,C2,C6,C9). The selected scalar mutator does not remove unchanged outputs: for an integer result0 its printed candidate list is [1,−1,2,−2,0]. String/float/map cases can likewise retain unchanged values or duplicates; arrays explicitly filter them. An exact contract for the correct result cannot reject that unchanged value. This differs from the paper's “no mutant equals” requirement; it is a direct static counterexample, not an observed run (C3,Q8). The earlier input generator labels null, empty, singleton and −1 variants invalid without running the reference to confirm failure in this function. The selected evaluate_problem calls that generator directly. A negative integer need not be invalid, for example for absolute value. This differs from the paper's confirmed-failure test construction; the final October labeling pipeline was not acquired or verified (C4,C6,Q9,Q10). The selected post/pre stubs declare nullable_by_default, while the command also supplies nonnull-by-default. That source does not straightforwardly establish the October effective-precondition account. Precondition stubs include and call the submitted annotated code, so they are not the stated body-free predicate stubs. These are encoding differences; no OpenJML interpretation or diagnostic was replayed (C5,C1,Q7). In the inspected external-agent CLI paths, verify sends the submitted code to OpenJML and harness reads its annotations; neither compares it with the original body. submit derives its passed flag from saved harness scores, without requiring a successful verification of the final code or binding those scores to its content. The scaffold writes the same five visible pairs into tests/ and task.json; a separate held-out split is not implemented in that path. Other offline selection/scoring could impose the paper's rules, but it was not audited or established here (C7,C8,Q11,Q15–Q17). The verifier wrapper also defaults to 180 seconds rather than the paper's 300-second configuration. The standalone scorer/agent scorer use different defaults, and READMEs describe earlier model/tool setups. Pin, version and actual experiment configuration must therefore remain separate. All fifteen blob identities are verified against the pinned Git tree; that proves which bytes were read, not that they generated the paper's measurements (C0,C10). ## Limits and relevance The paper excludes frame conditions and exceptional postconditions, cannot express in-place array updates in the stubs, and acknowledges overflow/rounding and small-output-domain limitations. Its finite pairs, chosen mutants, reference implementation, verifier semantics and helper contracts bound every score. Removing undecided checks prevents treating solver failure as falsity but can change which cases/specifications contribute; a high decided-case score should be reported with decided coverage. A contradiction in assumptions can also make individual stub proofs vacuous unless excluded. These are reasons to retain the score components and coverage rather than treat them as a correctness certificate (Q7–Q12,Q18; reader qualification). This paper directly informs evaluation of LLM-generated specifications: code preservation, vacuity, separate input/output obligations, failure versus refutation, held-out feedback and verification/adequacy/cost tradeoffs. Its study is Java/JML, not distributed-protocol, TLA+ or Verus verification. Verus/Rust and Frama-C ports are proposed future work. For distributed proof agents, analogous checks would require protocol execution oracles, message/schedule coverage and relational safety/liveness properties; transferring the four method-contract scores unchanged is a reader proposal, not a demonstrated result (Q19,Q20). - number: v2 uses thresholds such as PostCorr >= 0.75 and PostComp >= 0.75 (operational choice) - number: 120 SpecGenBench methods and 662 FormalBench methods - number: SpecGen falls from 54% verifier acceptance to 24% meaningfully verified on SpecGenBench (§5.4) - number: three refinement cycles; improvement of 5 points on SpecGenBench and 12 on FormalBench (§6.1) - limits: Finitebehavioraladequacy;referenceoracle/verifier/encoding/testselection;singlerun;coverageandunknownverdicts;JuneartifactnotestablishedOctexperimentrevision - how much was read: most of it read - source; notes: Generated contracts and independent evaluation; notes: Spec-Harness, formerly VeriAct - record id: `spec-harness-formerly-veriact-2026` - SpecCoder (2026) - title: Teaching Code LLMs to Reason with Intermediate Formal Specifications - what: Fine-tunes code LLMs to insert runnable assertions at internal program points (not just final postconditions), keeping only assertions that hold on correct runs and fail on buggy mutants. Also releases HumanExec, 150 Codeforces tasks with real buggy submissions. - number: prompted Qwen2.5-Coder-32B: 0.8989 syntax validity, 0.6313 correctness, 0.2604 completeness (Table I) - number: after SpecCoder, Qwen2.5-Coder-14B inline completeness 0.1989 to 0.7713 and validity 1.0000 (Table II) - number: average inline completeness over three model sizes 0.2112 to 0.7459 - number: HumanExec: 150 tasks, 48-279 tests each (mean 79.53) - limits: Sequential, single-run Python programs from competitive programming; no distributed or concurrent systems and no proofs, only assertions checked on test runs. Completeness is measured against available faulty runs, not all possible bugs; training data came from a teacher LLM plus test-suite filtering. - how much was read: most of it read - source; notes: ## SpecCoder and HumanExec (2026) - record id: `speccoder-2026` - SpecLoop (2026) - title: SpecLoop: An Agentic RTL-to-Specification Framework with Formal Verification Feedback Loop - what: Generates natural-language RTL specifications, reconstructs RTL from them, and uses formal equivalence counterexamples to iteratively refine specifications. The verifier separates compilation, reconstruction and equivalence errors; pass/fail-only and full-diagnosis loops are compared with single-round generation. Feedback is withheld from the reconstructor to avoid leaking original RTL semantics. VerilogEval and RTLLM benchmarks are scored by RTL Reconstruction (RR), making specifications operationally testable. - number: Verified specs have RR=1 ratios 81.3–91%; unverified 34.6–45% across settings - number: Verification loop ranks first in 4/12 (pass/fail) and 9/12 (full diagnosis) settings vs single round - number: Qualitative reset case corrected after equivalence counterexample - limits: End-to-end results depend on reconstructor quality, FEC resource bounds and heuristic feedback parsing. RR uses testbenches in addition to formal equivalence and may not capture all semantics. The method stops on invalid original RTL or exhausted retries. - how much was read: most of it read - source; notes: SpecLoop - record id: `specloop-2026` - SpecSyn (2026) - title: SpecSyn: LLM-based Synthesis and Refinement of Formal Specifications for Real-world Program Verification - what: SpecSyn combines top-down AST/dependency decomposition and sketch planning with bottom-up ACSL generation, verifier-guided repair, and variant-discrimination refinement. Semantic-non-equivalent mutations test whether candidate specifications reject changed programs; undistinguished variants are fed back for stronger specifications. Tarjan SCCs produce dependency-respecting segments, and depth-first postorder handles nested POIs such as loop invariants and function postconditions. At each POI, Frama-C/WP verifies generated candidates, returns errors for repair, and deduplicates accepted specifications. Variant discriminative rate measures the fraction of 188 mutation operators (35 equivalent operators removed; GCC -O2 TCE filters equivalents) rejected by the specification set. Experiments use 50 real-world C programs, seven verification benchmarks totaling 1,421 targets, three LLMs, and 17 trained reviewers. - number: GPT-5 SpecSyn average precision 96.68%, recall 75.91% across 14 repositories - number: SpecSyn verifies 1,022/1,421 targets vs Codex 883, Preguss 510, AutoSpec 259 - number: Ablating decomposition lowers precision/recall by 19.39/15.72 points; refinement by 11.39/12.66; sketch by 2.05/5.34 - number: 17 reviewers rated SpecSyn 3.78 (understanding) and 4.07 (semantic accuracy) out of 5 - limits: Semantic strength is operationalized by a finite mutation set and may miss behaviors not exercised by mutations. Precision/recall use manually authored ground truth, which may omit valid alternative specifications; Frama-C/WP and Z3 incompleteness can reject correct statements. The method is computationally expensive, with hundreds of verifier calls per file, and benchmark scale is 50 programs with potential leakage from prior X509 data. ACSL-compatible deterministic C functions are selected, excluding many OS-dependent functions. - how much was read: most of it read - source - record id: `specsyn-2026` - Specy (2026) - title: Specy: Automatically Learning Specifications for Distributed Systems from Event Traces - what: It learns event-based formulas from traces of distributed systems (P models or logs). It builds monitors from them and checks fresh traces to reject guesses that are too strong. For six deductive-verification experiments, the learned formulas were translated by hand. - number: all 43 goal specs recovered, 28 (65%) without help, 15 needed guidance - number: 14 benchmarks incl. 3 industrial, 10,000 traces each - number: about 9% of extra learned formulas fail on fresh traces, no designated goal formula does - number: pruning speeds up by geometric mean 14.8 - limits: The only guarantee is consistency with the supplied traces. Hard properties need predicates, event choices or ghost state. The deductive results cover selected safety properties of P models. There is no refinement to production code. - how much was read: most of it read - source; notes: Specy: Learning Specifications for Distributed Systems from Event Trac; notes: Specy: Learning Specifications for Distributed Systems from Event Trac - record id: `specy-2026` - Supporting Stakeholder Requirements Expression with LLM Revisions: An Empirical Evaluation (2026) - what: Participants wrote requirements and rated LLM-generated revisions for completeness, clarity and alignment. - number: 26 participants produced 130 requirement statements - limits: Perceived completeness is not formal completeness. A fluent revision may change a requirement without anyone noticing. - how much was read: most of it read - source; notes: Clarification and stakeholder requirements - record id: `supporting-stakeholder-requirements-expression-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` - 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` - 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` - 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` - Traceable and Verifiable Software Requirements: A Synthesis of AI-Enabled Formal Methods (2026) - what: A survey plus an experience report. The authors ran Frama-C (RTE, EVA, WP with several solvers) and PathCrawler on C functions to see what automation gives for requirements. - number: tutorial experiment 36 programs; five-program subset goals proved 6/6, 5/7, 6/8, 4/8, 13/13 - number: triangle classification: 20 goals, Alt-Ergo/CVC5 prove 15, Z3/CVC4 prove 13 - number: fifty base programs (150 instances) vs Table 4 files 52+60+53=165 - number: PathCrawler succeeds on 4 of 20 files, then 15 of 20 after adaptation; quicksort: 11 cases from 110 paths, 99 infeasible - limits: The accounting in Table 4 conflicts with the prose. The ResearchGate version is unreadable. An oracle was unavailable. No LLM starts from a vague request. - how much was read: most of it read - source; notes: AI-Enabled Formal Methods for Verifiable Software Requirements: A Surv - record id: `traceable-and-verifiable-software-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 4.33 per task
  • number: 48 tasks, 16 scenario families, all fully TLC-verified; 62.5% first attempt; none over four repairs
  • limits: Progress is not checked. Repairs for timeouts can reduce fidelity. The runtime monitor checks the topology, not the order of steps. A bounded model-checking pass does not prove that real agents terminate.
  • how much was read: most of it read
  • source; notes: TraceFix: generated PlusCal coordination protocols, with important lim
  • record id: tracefix-2026
• TrojanSpec-Bench (2026)
  • title: TrojanSpec-Bench: An Adversarial Benchmark for LLM-Based Formal Specification Elicitation
  • what: Treats the LLM that turns English requirements into a formal spec as a possible attacker. Builds 1,024 cases in Dafny, Lean 4 and Verus where a spec is subtly wrong yet still accepted by the verifier together with a bad implementation, then tests six detectors for such specs.
  • number: 1,024 admitted cases of 1,798 generated (57.0%): Dafny 319, Lean 4 417, Verus 288
  • number: four attack types admitted: implementation leak 377/450, vacuity 348/450, domain restriction 187/450, predicate swap 112/448
  • number: detector asking an LLM four yes/no questions and flagging when at least 2 fail: F1 0.967, false-positive rate 0.068, recall 1.000
  • number: single LLM-judge vote baseline: F1 0.871, false-positive rate 0.297
  • limits: Same model family (Claude Sonnet 4.6) generates most trojans and judges them; the LLM detector was not tested against adaptive attackers; ‘honest’ labels come from the verifier, not from humans; attack mix reflects the generator, not real-world frequency.
  • how much was read: most of it read
  • source; notes: TrojanSpec-Bench (2026)
  • record id: trojanspec-bench-2026
• Validating Formal Specifications with LLM-generated Test Cases (2026)
  • what: GPT-5 generates positive and negative Alloy instances from English requirements, before the requirement is formalized. Expert formulas label the instances. The authors test whether the instances expose wrong student specifications.
  • number: Table 3: Few prompt, 258 tests, 255 syntax-valid, 252 previous-consistent, 247 valid (96%), $3.56-number:Table6:35requirementswithcompletesuites,4816wrongspecs,348missed,meanmissed6.43-number:258requestedtests;few-shotGPT-5247valid(96$3.56); one-shot 205 (79%); zero-shot 118 (46%)
  • number: By model: GPT-5 96%, Gemini 81%, Claude 76%, Mini 67%
  • limits: It covers bounded structural models only. Suites are compared only over requirements that have complete valid suites. The persistent failures involve ambiguous English.
  • how much was read: most of it read
  • source; notes: Validating Formal Specifications with LLM-generated Test Cases
  • record id: validating-formal-specifications-with-2026
• VClare imperfect-spec repair (2026)
  • title: VClare: Resolving Imperfect Specifications in LLM-Based Verilog Generation
  • what: Introduces VClare, which repairs vague, contradictory, or incomplete Verilog specifications using specification-level inconsistency mining and simulation-level behavioral clustering, optionally combined in a hybrid pipeline. Two defect datasets inject three semantic defect types into VerilogEval-human and ComplexVDB tasks. Spec-level repair edits requirements before generation; Sim-level repair clusters multiple generated implementations by behavior and can arbitrate with test-time checks. Experiments compare no repair, blind fixes, VRank, SpecFix-no-oracle, and hybrid configurations across DeepSeek and GPT backbones.
  • number: VerilogEval-Defect Hybrid reaches 50.0% DS and 44.4% GPT overall Pass@1
  • number: ComplexVDB-Defect Sim-level reaches 49.8% DS and 39.9% GPT, versus no repair 34.2%/28.1%
  • number: five runs per configuration; n=10 candidates for pass@k
  • number: Hybrid contradiction accuracy reaches 59.5% DS and 57.4% GPT on VerilogEval-Defect
  • limits: Pass@1 uses ten sampled candidates and a golden testbench only for final evaluation, not during repair; outcomes depend on backbone, temperature/reasoning settings, simulator, and injected defects. Spec-level repair can harm complex tasks by introducing spurious modifications, while no claim is made that synthetic defects represent all industrial specification errors.
  • how much was read: most of it read
  • record id: vclare-imperfect-spec-repair-2026
• VeriSpecGen (2026)
  • title: Intent-aligned Formal Specification Synthesis via Traceable Refinement
  • what: It splits a description into requirements and ties tests and Lean clauses to each one. It repairs only the clauses implicated by a failed test.
  • number: 86.6% pass@1 on Verina’s official harness
  • number: 25 refinement iterations, 60 generated tests per problem
  • number: 86.6% on the Verina SpecGen task with Claude Opus 4.5; up to 31.8 points over baselines
  • number: 343,827 training pairs; training gives 15.6-18.2 points
  • limits: Labels come from a reference implementation that may itself be LLM-written. The LLM judge fallback is only guidance. It has no distributed or liveness tasks.
  • how much was read: most of it read
  • source; notes: Generated contracts and independent evaluation; notes: Intent-aligned Formal Specification Synthesis via Traceable Refinement
  • record id: verispecgen-2026
• VeriStruct (2026)
  • title: VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus
  • what: Two-stage LLM workflow jointly generates Verus views, type invariants, function contracts and proof/loop annotations for Rust modules with supplied tests. A planner chooses generation modules, candidate sampling selects verified-function progress, and Verus error classes route bounded repair prompts. Code and tests are intended to remain unchanged. [Q1,Q5–Q16] Complete RingBuffer abstraction and invariant example; distinct view-refinement pass; n-sample candidate selection; mode/type/mutability/arithmetic/contract/test repair; interprocedural postcondition strengthening. Complete source evaluation, budget/model confounds, verbatim-only training-overlap claim, contradictory test-origin prose, progress regressions, Bitmap abstraction and printed repair-loop last-check boundary are recorded in ANALYSIS.md. [Q4–Q34] Entire alternate arXiv v4 and its additional AppendixA/Table4 read; all12repair-heuristic rows recorded separately from the publisher chapter. [Q35–Q37]
  • number: 11 modules;129 functions including test functions
  • number: VeriStruct 10 solved modules,128 functions; baseline 4 and 52; Claude Code 8 and 102
  • number: n=3 samples per module;m=5 repair iterations;13 baseline calls/benchmark
  • number: Approximate mean tokens 22 k VeriStruct,24 k Claude Code
  • limits: Proof acceptance is relative to generated annotations and supplied test assertions; semantic adequacy outside those uses is not established. Eleven substantially modified modules; verbatim nonoverlap with the named training snapshot is an author assertion with no check method given. Baseline has 13-call cap; Claude Code uses Sonnet 4.5 rather than o1 and lacks a stated matched cap. Repeated-run count and variance are unreported, so exact once-only execution is not established. Introduction claims LLM test generation while conclusion requires manual tests and calls automated generation future work. Resource algebra synthesis is future work; no distributed protocol or TLA+ verification. [Q1–Q3,Q17,Q20–Q23,Q28–Q29] The baseline “invokes the LLM once to generate all annotations simultaneously,” whereas VeriStruct requests n samples per module and sets n=3. The paper does not clearly reconcile candidate sampling with its unit of “LLM invocation”; the13-call cap alone does not establish equal candidate-generation effort. No exact API-call multiplier is inferred [Q8,Q20,Q22].
  • how much was read: most of it read
  • source
  • record id: veristruct-2026
• Verus-SpecGym (2026)
  • title: Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization
  • what: It judges agent-written Verus specifications by running them against official and adversarial Codeforces tests.
  • number: 581 tasks; best Gemini-3.1-Pro 77.8%; LLM judges miss 26% of detected failures
  • number: 581 specification-writing tasks
  • number: an LLM judge misses 26% of failures the evaluator catches
  • number: 75-minute timeout per run
  • limits: The tasks are algorithms. Testing is evidence, not a proof of equivalence in general.
  • how much was read: most of it read
  • source; notes: Dafny, C verification, and the specification-intent gap; notes: Generated contracts and independent evaluation; notes: Verus-SpecGym / Verus-SpecBench
  • record id: verus-specgym-2026
• A Short Survey on Formalising Software Requirements with Large Language Models (2025)
  • what: Summarizes 35 papers on using LLMs to write formal specifications from English requirements, grouped by method and domain. Concludes that helper assertions come out better than whole contracts.
  • number: 35 papers surveyed
  • number: Laurel generates over 50% of needed Dafny helper assertions
  • number: SpecGen: verifiable specs for 279 of 384 programs
  • number: Req2Spec: 71% of 222 Bosch requirements formalized
  • limits: Numbers are reported from the surveyed papers and not re-checked; the survey was selected with the AI tool Elicit and checked by hand. No distributed systems or liveness focus, and its comparisons mix very different tasks.
  • how much was read: most of it read
  • source; notes: ## A short survey on formalising software requirements using LLMs (202
  • record id: a-short-survey-on-2025
• AssertCoder multimodal SVA generation (2025)
  • title: AssertCoder: LLM-Based Assertion Generation via Multimodal Specification Extraction
  • what: Introduces AssertCoder, a pipeline that classifies PDF specification blocks, extracts signal-level semantics from text/tables/diagrams/formulas, synthesizes SystemVerilog assertions through structured multi-step prompting, and iteratively refines them using mutation-based model checking feedback. The framework uses LayoutParser plus an LLM to label modality and semantic categories, converts blocks to a unified intermediate representation, and decomposes each assertion into precondition, consequence, timing, pattern selection, temporal binding and syntax synthesis. Design-aware retrieval supplies patterns; SymbiYosys checks assertions and Mantra injects roughly 100–300 mutants per DUT. The mutation score averages detected mutants per assertion, while MDR is the fraction of mutants detected by any assertion and FPR manually distinguishes semantically wrong failures from real DUT bugs. On I2C, AES and Openmsp430, AssertCoder averages 97.8% syntax correctness, 87.6% functional correctness, 85.6% MDR and 3.2% FPR, beating AssertLLM (79.2% functional, 79.8% MDR, 5.5% FPR) and zero-shot GPT-4o (17.2%, 38.1%, 21.7%). Ablations show CoT most affects correctness and iterative refinement most affects mutation detection; RAG has comparatively small impact.
  • number: 3 RTL designs
  • number: 100–300 mutants per DUT
  • number: AssertCoder average 97.8% syntax, 87.6% functional, 85.6% MDR, 3.2% FPR
  • number: AssertLLM 79.2% functional and 79.8% MDR
  • limits: The evaluation uses three open-source RTL modules and their multimodal specifications, GPT-4o generation, SymbiYosys model checking and manually judged failed assertions; results may not generalize to other designs, specification quality or models. Mutation adequacy depends on Mantra bug-derived operators and MDR is not proof of complete functional coverage. The pipeline relies on accurate PDF layout parsing and LLM semantic classification; assertions can be syntactically valid yet semantically misaligned. No distributed-system protocol is evaluated.
  • how much was read: most of it read
  • record id: assertcoder-multimodal-sva-generation-2025
• Astrogator (2025)
  • title: Towards Formal Verification of LLM-Generated Code from Natural Language Prompts
  • what: Introduces Astrogator, a verifier for LLM-generated Ansible programs. A user-readable Formal Query Language gives a precise, reviewable specification of natural-language intent; a State Calculus models stateful system effects; a symbolic interpreter and unifier compare generated playbook behavior with the query and report extra assumptions/actions. The formalization separates user intent U from an approved but possibly under-specified query semantics and explicitly defines the unresolved gap p∖s for user review. The State Calculus models attributes, nested elements, stateful functions, reads, writes, conditionals, cases and symbolic loops; unknown reads branch over possibilities, and symbolic lists are approximated by one representative element. Ansible modules are specified in a small module-definition language, while a hand-curated knowledge base maps high-level descriptions such as apache server or zsh configuration file to OS-specific packages and paths. On 1,260 generated playbooks from six LLMs, Astrogator accepts most test-correct programs and rejects most incorrect ones, but under-specified queries permit incorrect programs unless users review reported assumptions.
  • number: 21 benchmarks
  • number: 1,260 generated programs
  • number: 334 correct (26.5%)
  • number: 277/334 accepted (82.9%)
  • limits: The formalizer cannot always infer intent from ambiguous natural language, so the user must approve the formal query. The query is intentionally incomplete and the evaluation accepts all programs satisfying it without user review of p∖s. The Ansible compiler does not support all features, especially shell commands, blocks and handlers; symbolic-loop handling is imprecise and arbitrary loops are future work. Ground truth for 1,260 programs is based on tests across Debian 12.11, Ubuntu 24.04.2 and RHEL 9.6 VMs, not a proof of real-world correctness. Knowledge-base single-valued choices cause false rejections when multiple implementations are valid.
  • how much was read: most of it read
  • source; notes: ## Astrogator, checking LLM Ansible code against a readable query (202
  • record id: astrogator-2025
• ATLAS (2025)
  • title: Constrained LTL Specification Learning from Examples.
  • what: ATLAS learns LTL formulas (formulas about behavior over time) from good and bad example traces. It also takes user constraints and priorities, and solves with MaxSAT, an optimizing solver. It uses no LLM. Cases: Peterson mutual exclusion, a voting machine, robot-arm repair, and weakening an invariant.
  • number: Table I: 30/30 tasks mean 43.65 s (Peterson); 10/10, 3.08 s (voting); 20/20, 37.25 s (robot arm); 53/78, 66.75 s (invariant weakening)
  • limits: It finds the best formula only within the formula-size bound. A formula that fits the traces may not capture what the user meant. The benchmarks were built around the authors’ use cases. Using it needs formal-methods expertise.
  • how much was read: most of it read
  • source; notes: Constrained LTL Specification Learning from Examples (ATLAS)
  • record id: atlas-2025
• BEq+ / ProofNetVerif (2025)
  • title: Reliable Evaluation and Benchmarks for Statement Autoformalization
  • what: BEq+ tries to prove both directions of implication between a generated Lean statement and a reference statement. ProofNetVerif and RLM25 are labeled benchmarks for whether a statement is correct.
  • number: ProofNetVerif: 3752 labeled pairs, 1142 correct; RLM25: 619 pairs from six projects
  • number: BEq+ precision/recall/F1 98.0/48.3/64.7; Pearson 0.974, Kendall 0.872
  • number: 118 entries (31.8%) with formalization errors in Lean 4 ports
  • number: GPT-4o 50 samples: ProofNet# manual 45.1, BEq+ 23.4; RLM25 BEq+ 31.6
  • limits: It covers mathematics only. The equivalence procedure is incomplete. People are needed for the references and the final labels. Results with no context are near zero.
  • how much was read: most of it read
  • source; notes: Reliable Evaluation and Benchmarks for Statement Autoformalization
  • record id: beq-proofnetverif-2025
• CLEVER (2025)
  • title: CLEVER: A Curated Benchmark for Formally Verified Code Generation
  • what: CLEVER is a Lean benchmark. A model generates a spec, which must be proved equivalent to a hidden, human-written reference spec. The model then generates code, which must be proved against that reference. The reference specs are noncomputable so that models cannot copy code logic.
  • number: 161 problems (from 164 HumanEval; 3 excluded)
  • number: default budget 600 seconds for pass@k-seconds
  • number: human effort per problem: 25 minutes plus an additional 15 minutes, in places over an hour
  • number: reference proofs 10-225 lines
  • limits: It depends on the quality of the reference. Failed equivalence proofs give false negatives. HumanEval data may have leaked into training. It covers only list and numeric tasks, and has no liveness.
  • how much was read: most of it read
  • source; notes: Generated contracts and independent evaluation; notes: CLEVER
  • record id: clever-2025
• CodeMetaAgent (2025)
  • title: LLM Assisted Coding with Metamorphic Specification Mutation Agent
  • what: CodeMetaAgent rewrites programming task descriptions with nine transformations: negation, translation, step decomposition, paraphrase, plus transformations of tests. It filters the rewrites with BERT similarity. It checks tests against an oracle implementation (a reference that gives the right answers).
  • number: HumanEval-Pro 164 and MBPP-Pro 378 problems
  • number: GPT-OSS MBPP-Pro pass@1 53 to 70
  • number: oracle branch coverage 99.36 vs 99.81
  • number: SWE-bench Lite: 69 bugs/23% baseline vs 90 bugs stated 30.3% (90/300 is 30.0%)
  • limits: It handles only prose specifications and finite tests. BERT similarity does not certify that quantifiers or negation are preserved. Several arithmetic figures are inconsistent (233/300 is 77.7%, not 78.6%).
  • how much was read: most of it read
  • source; notes: LLM Assisted Coding with Metamorphic Specification Mutation Agent
  • record id: codemetaagent-2025
• Formal requirements engineering and large language models: A two-way roadmap (2025)
  • what: A vision paper on how LLMs can help create, explain and translate formal requirements. It has a worked example of a bounded sender/receiver protocol, modeled in PROMELA and checked with SPIN.
  • number: passing model: 77 states, 86 transitions, 128.730 MB; failing model 52 states
  • number: maximum of ten messages
  • limits: It checks safety within bounds only. Message loss and corruption are excluded by construction. There is no proof that the model matches the Python code. LLM translation is future work. The ChatGPT-3.5 examples were edited illustrations.
  • how much was read: most of it read
  • source; notes: Formal requirements engineering and large language models: A two-way r
  • record id: formal-requirements-engineering-and-2025
• FormalAlign (2025)
  • title: FormalAlign: Automated Alignment Evaluation for Autoformalization
  • what: FormalAlign is a trained Mistral-7B. It scores whether a formal Lean statement matches its informal statement. It was trained on wrong statements made by automatic mutation.
  • number: 21 negative examples per positive
  • number: alignment-selection: FormL4-Basic 99.21, MiniF2F-Valid 66.39, MiniF2F-Test 64.61 (Tables 4-6 give 66.70, unresolved)
  • number: human 79.58% vs FormalAlign 65.00%; humans 3 hours for 80 items vs under 2 minutes
  • limits: The score is learned. It is not a proof of equivalence. Accuracy on mutated statements is not evidence of agreement with intent. The review notes read v1, not the final ICLR version.
  • how much was read: most of it read
  • source; notes: FormalAlign: Automated Alignment Evaluation for Autoformalization
  • record id: formalalign-2025
• FormalBench (2025)
  • title: Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference
  • what: Introduces FormalBench, a benchmark of manually validated Java/JML programs and semantic-preserving variants for evaluating LLM specification inference using deductive consistency, mutation-based completeness, robustness and self-repair metrics. FormalBench-Base contains 700 validated Java programs; 18 semantics-preserving transformations produce 6,219 diverse variants. OpenJML determines success/failure/unknown and Major generates mutants; completeness is the fraction of non-equivalent mutants rejected. The study evaluates eight open-source/proprietary LLMs under zero-shot, few-shot, chain-of-thought and least-to-most prompts, diagnoses syntax/quantifier/loop-bound errors, and tests targeted self-repair prompts.
  • number: 700 manually validated programs and 6,219 augmented variants
  • number: 14 LLMs reported in conclusion; core table covers eight models/settings
  • number: Best listed success: DeepSeek-V3 + LTM 16.6%; GPT-4o + LTM 15.0%; Claude-3.5 + LTM 15.4%
  • number: Robustness flip rates: DeepSeek-V3 27.2%, Claude-3.5 39.2%, GPT-4o 29.2%
  • limits: Mutation completeness is a proxy: equivalent mutants can evade detection (3 of 232 manually checked, 1.3%). Unknown verifier results are separated from failures but complicate metrics. The benchmark is Java/JML-specific; generated specifications may be syntactically invalid or semantically incomplete. Experiments omit OpenAI-o1 and DeepSeek-R1 due cost/access and use finite token/GPU budgets.
  • how much was read: most of it read
  • source
  • record id: formalbench-2025
• Formalising CXL Cache Coherence (2025)
  • what: An Isabelle model of the CXL.cache protocol, written from its English standard. It proves a single-writer/multiple-reader safety property, strengthening the invariants repeatedly. A tool called super_sketch drives Sledgehammer to generate proofs.
  • number: around 211k lines of code
  • number: 12 person-months
  • number: 796 invariant conjuncts, 68 rules, 53,332 lemmas (796x68=54,128 conflicts with it)
  • limits: The model has two devices and one location, with perfect tracking, and omits several messages. Data-value correctness, deadlock freedom and liveness are unproved.
  • how much was read: most of it read
  • source; notes: Related work absent from the first pass: Formalising CXL Cache Coheren
  • record id: formalising-cxl-cache-coherence-2025
• FormalSpecCpp: A Dataset of C++ Formal Specifications created using LLMs (2025)
  • what: # Whole-paper read: FormalSpecCpp: A Dataset of C++ Formal Specifications created using LLMs (authored by agents unless marked 🧑) Madhurima Chakraborty, Peter Pirkelbauer and Qing Yi; arXiv2502.15217v1,21February2025,5pages. The paper constructs105small C++ programs/contracts and translated tests using GPT-4-turbo, starting from verified Dafny-synthesis programs. Its evidence is compilation, finite tests and expert review of a subset. The introductory description of “verified C++ programs” is an author claim; no C++ deductive verification, verified translator or preservation theorem is supplied. [Q0,Q1,Q4,Q5,Q6,Q7] ## Construction, contracts and trust Only Dafny programs containing both preconditions and postconditions were selected. GPT-4-turbo translates their code and specifications; MBPP tests are separately translated to C++. Figure1 shows the Python→Dafny→C++ provenance and test/manual-inspection branches. This is translation from existing specifications, rather than an evaluation of inferring unknown C++ contracts. Figure2 asks the model to select signed/unsigned integer types, identify failure conditions, express preconditions with REQUIRE, loop invariants with assert, postconditions with ENSURE, and omit main. Both macros expand to assert. These are executable checks on reached states, not discharged proof obligations over all allowed inputs. They may also be disabled by the usual C++ assertion mechanism. [Q2,Q3,Q4,Q5,S2] The paper argues that translating verified Dafny specifications preserves correctness and avoids unnecessary constraints. That does not follow just from a verified source: integer domains, containers, evaluation order, exceptional behavior and the translation of the property itself also need a correspondence argument. The paper’s own manual review found semantically incorrect but syntactically valid specifications. The source Dafny verifier, selection, language mapping, generated tests and reviewer judgment therefore remain trust dependencies. There is no independent exhaustive audit of all105contracts in this paper or in this reading. [Q4,Q6,Q7,Q10] The paper contrasts unbounded Dafny integers with C++ fixed-width types, but incorrectly says C++ has “well-defined overflow behavior for signed integers.” Ordinary out-of-range signed arithmetic has undefined behavior. The saved C++ draft’s expression rules state that arithmetic-expression behavior is undefined when the mathematical result is outside representable values (with specified floating-point exceptions); unsigned modular arithmetic is distinct. This is a reader correction of a language claim, not an executed counterexample to every translated program. [Q10,L0] ## What the evaluation establishes The initial linked-test run had62programs pass all tests and43fail due to assertions, linking or compilation; 62/105≈59.05% is my arithmetic, not a reported semantic-correctness rate. Authors found misordered test arguments, incorrect expected outputs and unsigned-int/double mismatches. Compiling successfully did not exclude incorrect contracts or logical inconsistencies. One author reviewed/refined failing cases and a subset of successes; the paper gives no exact reviewed-subset size, final complete semantic-pass count, independent reviewer agreement or measured coverage. [Q6,Q7] TableI/§IV report105/105first-attempt program compilations,105files,$2.07program-translationcost(about$0.02/file),17.3average Dafny lines,33.1average C++ lines and91.2%growth. The text reports about27minutes for programs and an additional1.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 and no compilation errors, agreeing with TableI. The report is author-supplied evidence, not a reproduced run. The code’s cost tracker counts only the initial response, so hypothetical repair costs would be omitted; because this report says all attempts were first attempts, this observation does not establish an undercount for the reported run. [S2,S7] getTests.py uses temperature0/max_tokens500 and up to5attempts to extract a code block, then writes a test including the translated program. The script labels response.usage.total_tokens as input_tokens and also charges completion_tokens at output rates. Static accounting therefore charges completion tokens once at input rates as well as output rates; only the final successful response’s usage is returned, omitting failed extraction attempts. Actual request histories are unavailable, so I do not compute a corrected1.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 (base*height*length)/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` - 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 0.29
  • limits: Inferred specifications are heuristic facts, not certified contracts: EESI approximations and LLM hallucinations remain after filters. LLM provenance tracks all supplied context because actual causal contribution is unknown. Six C benchmarks use manually supplied knowledge; ground truth is exhaustive only for small benchmarks and sampled for larger ones. Main effectiveness results use GPT-4, whereas cost and repeated-run analyses use GPT-4o-mini, so those numbers cannot be combined as one configuration. Fallibility and incorrect background facts remain substantial error sources; inference-path length and number of LLM calls do not reliably identify errors. No downstream bug-finding or distributed-correctness guarantee is established. Source PDF prints the exact requested DOI.
  • how much was read: most of it read
  • source
  • record id: interleaving-static-analysis-and-2025
• LLM document-to-temporal-spec extraction (2025)
  • title: Extracting Formal Specifications from Documents Using LLMs for Automated Testing
  • what: Builds a dataset of 603 temporal specifications from 37 ArduPilot, PX4 and Autoware documents and evaluates GPT-4o, Claude-3.5-Sonnet and Llama-3.1-405B extracting formal requirements. A two-stage annotation-then-conversion pipeline improves coverage and accuracy over direct end-to-end prompting. Experts cross-validated ground truth; prompts first mark requirement-bearing sentences and then convert annotations into temporal logic, reducing oversimplification and hallucinated clauses. The paper quantifies false positives and studies a DeepSTL non-LLM conversion baseline. Documents average 2,966 words; each model runs three times and unique outputs are aggregated.
  • number: 603 validated specifications from 37 documents
  • number: End-to-end accuracy: Claude 51.7%, GPT-4o 47.1%, Llama 45.4%
  • number: Annotation-then-conversion best accuracy 71.6%; +14.0 percentage points average and +29.2% correctly extracted
  • number: Best false-positive rate 14.5%; each LLM run three times
  • limits: Ground truth may be incomplete or contain expert errors; temporal formulas require interpretation of informal documents. LLMs oversimplify dense requirements and fabricate plausible but unsupported conditions. Dataset is limited to three open-source autonomous-system projects and temporal logic; extraction quality does not prove implementation correctness.
  • how much was read: most of it read
  • record id: llm-document-to-temporal-spec-extraction-2025
• LLM plan verification with NuSMV (2025)
  • title: Bridging LLM Planning Agents and Formal Methods: A Case Study in Plan Verification
  • what: Introduces an LLM pipeline that translates natural-language plans into NuSMV Kripke structures and LTL properties, then uses model checking to classify plan validity on a simplified PlanBench task. The method maps facts to Boolean variables, natural-language initial conditions to init, action preconditions/effects to guarded transitions, and a stage variable to enforce action sequence; goals become LTL reachability properties such as F(goal). NuSMV bounded model checking labels generated models valid (SAT), invalid (UNSAT) or unknown (parse/model failure). A one-shot GPT-4o/GPT-5 comparison reports formal-verification metrics against direct LLM judgments and analyzes unknown handling, syntax versus semantic fidelity and risk-sensitive precision/recall.
  • number: GPT-5 one-shot: 95.89% accuracy, 99.44% precision, 93.34% recall, 96.30% F1, 6.87% unknown, 47.08 time units
  • number: GPT-4o one-shot: 52.06% accuracy, 59.19% precision, 45.54% recall, 51.48% F1, 34.61% unknown
  • number: direct GPT-5 baseline: 99.59% accuracy/F1 with no unknowns, illustrating comparison mismatch
  • number: direct GPT-4o baseline: 80.37% accuracy, 79.95% F1
  • limits: The benchmark is simplified and reduced to binary validity; it does not explain invalidity reasons or test broad software/circuit settings. Unknown outputs are excluded from headline metrics, so treating them differently changes apparent reliability. Syntactically valid models can still misrepresent plan intent and pass verification; one-shot prompting, GPT-5 low reasoning effort and small qualitative semantic analysis limit generalization.
  • how much was read: most of it read
  • source
  • record id: llm-plan-verification-with-nusmv-2025
• LLMs as Planning Formalizers: A Survey for Leveraging Large Language Models to Construct Automated Planning Models (2025)
  • what: The survey covers about 80 works in which LLMs generate planning domains and problems from natural language.
  • number: approximately 80 existing works
  • limits: The review notes found no 24.8/35.1 percent statistic. So the headline number in the Safe Agents survey is unsupported by this citation.
  • how much was read: most of it read
  • source; notes: LLMs as Planning Formalizers: A Survey for Leveraging Large Language M
  • record id: llms-as-planning-formalizers-2025
• miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward (2025)
  • what: Re-checks the miniF2F Lean statements against the original competition questions and corrects them. Separates simplified tasks from tasks faithful to the competition.
  • number: 488 problems; over 300 Lean 4 statements corrected; 16 problems with no solution
  • number: Herald test accuracy automated judge 97.5% vs human 62.7% on v1
  • number: Kimina+Goedel-V2-7B test 49.2 / 69.7 / 61.5 for v1/v2s/v2c; validation 54.9 / 70.1 / 62.3
  • number: Pipeline about 36% (40% on the original) vs 97% and 69% for the two stages alone
  • limits: About mathematics, not software. Judging fidelity needs a human.
  • how much was read: most of it read
  • source; notes: miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forw
  • record id: minif2f-lean-revisited-reviewing-2025
• NL2Contract (2025)
  • title: Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification?
  • what: LLMs write executable preconditions and postconditions for Python from signatures and docstrings. CrossHair searches for violations. Mutation tests estimate how well the contracts tell correct from wrong code.
  • number: GPT-5 accept@1/5/10 and sound@1/5/10: 89.0 94.6 95.1 81.1 88.7 90.0
  • number: real buggy cases: 14 of 31 found with each model
  • number: contract unsound only if CrossHair finds a violation in 60 s
  • limits: Its notion of soundness counts unknown results and timeouts as sound. It has no liveness. A code release is promised but no URL is given.
  • how much was read: most of it read
  • source; notes: Beyond Postconditions: Can Large Language Models infer Formal Contract
  • record id: nl2contract-2025
• On the Effectiveness of Large Language Models in Writing Alloy Formulas (2025)
  • what: The paper tests LLMs on eleven familiar graph and relation requirements. The LLMs write Alloy formulas from English, write them from a reference, or complete partial formulas. Automated bounded equivalence checks grade the results.
  • number: both LLMs find at least one valid solution among twenty requested per property
  • number: each LLM completes all but 1 sketching task; both failures fixed with syntax feedback
  • number: default scope three
  • limits: The checks cover bounded equivalence only. Familiar small tasks are weak evidence for unfamiliar distributed-system guarantees.
  • how much was read: most of it read
  • source; notes: On the Effectiveness of Large Language Models in Writing Alloy Formula
  • record id: on-the-effectiveness-of-2025
• P2FGPT (2025)
  • title: Constructing formal models of cryptographic protocols from Alice&Bob style specifications via LLM
  • what: A prompt-based pipeline that reads a security protocol written as ‘A -> B: message’ steps and writes the declarations part (types and functions) of a ProVerif model. ProVerif is a security-protocol checker. A checker step runs ProVerif’s parser, and a repair step re-prompts the LLM on syntax errors.
  • number: dataset: 4 ProVerif demo protocols cut into 53 + 25 + 14 + 14 = 106 sub-protocols
  • number: syntax-correct rate with GLM4.0: 65% (generator alone) to 82% (with repair step)
  • number: repair step helped GLM4.0 only; it made no difference for Llama3-8b and little for Qwen2.5-7b
  • number: content score (BLEU/F1) with GLM4.0: BLEU 0.34 to 0.39, F1 0.58 to 0.62 with repair; Qwen2.5-7b BLEU 0.61, F1 0.60
  • limits: Generates only declarations, not the protocol steps or the security goals the user cares about; no check that the model says what the protocol says, only that it parses and looks like a reference text. Prompts were tuned by hand on GLM4.0 and transfer poorly to other models.
  • how much was read: most of it read
  • source; notes: P2FGPT, Alice&Bob to ProVerif (2025)
  • record id: p2fgpt-2025
• ParCleanse (2025)
  • title: Validating Network Protocol Parsers with Traceable RFC Document Interpretation
  • what: GPT-4o extracts packet layouts and constraints from RFCs, with links back to the source text. Z3 generates valid packets and packets that break exactly one rule, and real parsers in C, Go and Python run them. An LLM diagnoses whether each failure is a spec error or an implementation error.
  • number: Table 2 precision/recall: Total 100/100 99/95 94/91 98/82 73/44
  • number: Table 3: 69 unique, 68 new, 36 confirmed bugs
  • number: golden formats: Babel 171 lines/5 h; BGP-4 164 lines/6 h
  • limits: It recalls dependent rules poorly. Every discrepancy was checked by hand. It covers input-validation safety, with no liveness.
  • how much was read: most of it read
  • source; notes: Validating Network Protocol Parsers with Traceable RFC Document Interp
  • record id: parcleanse-2025
• PAT-Agent (2025)
  • title: PAT-Agent: Autoformalization for Model Checking
  • what: Turns a natural-language system description, properties and expected outcomes (VALID or INVALID) into a CSP# model for the PAT model checker. Repairs the model from counterexamples for up to five rounds.
  • number: 40 tasks (26 PAT, 6 textbook, 8 Alloy4Fun), 133 assertions
  • number: 100% full-pass after repair; 75% before repair, 77.5% after one, 87.5% after two; direct models 37.5-52.5%
  • number: 4.34 minutes per system average
  • number: 20-person user study, separate
  • limits: Finite models only, not application code. No progress proofs at unbounded size and no refinement. Section VI says a repair pipeline gave negligible gain, which conflicts with the repair-loop results.
  • how much was read: most of it read
  • source; notes: PAT-Agent: users supply descriptions and the outcomes they want checke; notes: PAT-Agent: users supply descriptions and the outcomes they want checke
  • record id: pat-agent-2025
• Position: Formal Mathematical Reasoning—A New Frontier in AI (2025)
  • what: A position paper arguing that formal mathematics should complement language-model reasoning to supply checked reasoning steps, automatic training feedback and a path toward verified software/hardware generation. It organizes research challenges around data scarcity, faithful autoformalization, proof search, abstraction, retrieval, specification trust and proof maintenance. Its main original contribution is an agenda with separate levels for autoformalization, theorem proving, verified natural-language reasoning and verified system generation; it supplies no new proving algorithm, experiment or formal theorem. The paper separates producing a proof of a fixed formal statement from ensuring that the statement captures human intent. It proposes collecting human repairs and synchronizing informal/formal pairs, using semantic rather than string-match autoformalization metrics, comparing provers under explicit hardware/time budgets, growing libraries through useful subgoals and abstractions, and evaluating agents on projects and change histories. Software verification receives a distinct treatment: bespoke datatypes, repetitive case splits, large evolving codebases and specification management differ from isolated mathematical theorem proving. It discusses an alternative neural-only view and identifies self-verification and easy-to-hard generalization as unresolved prerequisites rather than demonstrated impossibilities.
  • limits: This is an explicitly selective position paper, not a systematic survey or controlled comparison. The claim that formal reasoning is indispensable and forecasts of lower verification cost are author positions, not results established by experiments in this paper. Formal proof checking establishes the exact encoded claim relative to the proof system, its assumptions and trusted implementation. The paper itself makes fidelity of generated specifications a key open problem; checker acceptance alone does not establish developer intent or correctness of the translation. The milestone levels are proposed organizing categories, with no validated thresholds, measured reliability requirements, human-cost study or proof that capability rises in the stated order. Theorem-proving level 2 explicitly includes human-built tactics without machine learning. Numbers about NuminaMath, Proof Pile, AlphaProof and seL4 are cited contextual examples, not new measurements. IMO 2025 claims are explicitly attributed to blogs/X without further details, and no such external evidence was fetched in this reading. The discussion of current systems is tied to the supplied 2025 proceedings version. Its model capability and benchmark-availability claims are historical author assessments, not a current exhaustive inventory. Arguments that informal scaling alone cannot resolve advanced mathematics and that neural-only self-verification remains weak draw on prior work; no impossibility theorem or decisive experiment rules out future neural-only systems. Software, hardware and mathematical verification are discussed broadly. Verus and AutoVerus appear as examples, but Rust memory/concurrency semantics, TLA+ specifications, distributed protocols and their fault assumptions are not evaluated. Formalizing or solving selected substeps while interleaving natural language does not by itself certify every unformalized claim or the full natural-language conclusion. This boundary follows from which parts are actually checked, not a new end-to-end guarantee shown here.
  • how much was read: most of it read
  • record id: position-formal-mathematical-reasoning-2025
• Position: Vibe Coding Needs Vibe Reasoning: Improving Vibe Coding with Formal Verification (2025)
  • what: Advocates a side-car system that maintains specifications during conversational code development, selects lightweight verification tools, feeds actionable results to the coding model, and lets developers review constraints. Distinguishes verifier-feedback filtering (Type I), postprocessing/constrained generation (Type II), and collaborative specification maintenance (Type III). A small TypeScript prototype hooks Claude Code changes and instantiates four templates: exhaustive switches, discriminated unions, shared union aliases, and satisfies Record guards. Toy order-status examples show missing shipped UI handling and missing cancelled processing.
  • number: 4 specification templates
  • number: 2 bugs in the order-status toy example
  • number: no quantitative evaluation
  • limits: This is a position paper with a small proof of concept, not a quantitative effectiveness study. Verification is currently syntactic checks and compiler acceptance; broader formal tools, provenance, and application-specific specification maintenance remain proposed work. Its claims about inevitable decay and general bug absence are arguments, not experimentally established guarantees. Compiler checks apply only to the chosen templates and modeled type constraints.
  • how much was read: most of it read
  • source
  • record id: position-vibe-coding-needs-2025
• ProofSeek (2025)
  • title: Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification
  • what: Presents a three-module framework that turns natural-language statements into formal Isabelle proofs: statement generation, LLM proof generation and heuristic proof structuring. SFT teaches syntactic Isabelle, RL rewards proofs checked by PISA, and recursive proof search uses ATPs, ERP and backtracking. The proof representation is a state-transition system; each generated step is checked by ATPs, with ERP repairing failures and heuristic tactics/backtracking reorganizing proof trees. The framework targets both miniF2F-test mathematics and AWS S3 bucket policy verification, and curates an FVELER-derived training dataset. The authors emphasize whole-proof generation plus structured subproof reuse.
  • number: Two-stage SFT then RL training
  • number: Framework validated on miniF2F-test and Isabelle
  • number: AWS S3 policy used as application case; detailed success tables are in §4 of extraction
  • limits: Formal correctness is relative to Isabelle/PISA/ATP checking and the formalized statement; natural-language translation can misrepresent program intent. RL and heuristic search depend on finite budgets and solver availability. The supplied experiments report benchmark results but do not establish coverage of arbitrary software policies.
  • how much was read: most of it read
  • record id: proofseek-2025
• PSMBench (2025)
  • title: PSMBench: A Benchmark and Dataset for Evaluating LLMs Extraction of Protocol State Machines from RFC Specifications
  • what: A benchmark of 14 protocols with human-annotated state machines. It scores nine LLMs on extracting state machines from RFC text.
  • number: 14 protocols, 1,580 RFC pages, 108 states, 297 transitions
  • number: annotation about three days per protocol
  • number: best state F1 0.715 (DeepSeek-V3), transition F1 0.378
  • number: 14 protocols, 1,580 RFC pages, 108 states, 297 transitions; annotation about three days per protocol
  • limits: It scores agreement with the annotations, not protocol safety. The annotations themselves need auditing, since RFC2TLA+ finds missing behaviors. Settings in the appendix give other scores.
  • how much was read: most of it read
  • source; notes: PSMBench / RFC2PSM: extraction accuracy, with human ground truth; notes: PSMBench / RFC2PSM: extraction accuracy, with human ground truth
  • record id: psmbench-2025
• Req2LTL (2025)
  • title: Bridging Natural Language and Formal Specification — Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMs
  • what: It separates decomposing the meaning in an intermediate language from building LTL formulas (formulas about behavior over time) by rules.
  • number: 88.4% semantic accuracy and 100% syntactic correctness
  • number: 112 aerospace requirements
  • limits: Its binary accuracy compares formula strings without normalizing or checking semantic equivalence, so it penalizes formulas that are equivalent.
  • how much was read: most of it read
  • source; notes: Natural language to temporal logic and TLA+
  • record id: req2ltl-2025
• ShieldAgent: Shielding Agents via Verifiable Safety Policy Reasoning (2025)
  • what: An LLM guardrail converts natural-language policies into logical rules, refines their predicates, clusters relevant rules by action, assigns observed predicate values through tools and generated code, then thresholds a learned probabilistic rule model. Reports improved classification and conditional online policy compliance for web agents. The paper calls its probability comparison a dynamic safety guarantee, but supplies no invariant theorem establishing it. Separates action constraints from background state rules; uses GPT-4o policy extraction, verifiability refinement and redundancy pruning; learns soft Markov-logic weights rather than requiring every rule to hold. Gives a hybrid history/workflow memory, specialized search/check tools, an action-circuit training algorithm, attack-generated data and a fully worked Reddit bio example. Appendices expose translation, predicate-binding and probability inconsistencies that formal checking alone does not repair.
  • limits: Logical checking is conditional on correct policy extraction, refinement, merging, action retrieval and assignment of observed facts. GPT-4o performs policy translation and optional human experts may correct rules. No equivalence proof establishes fidelity to original policies or completeness of retrieved constraints. Rules have finite learned weights, explicitly allowing tradeoffs to reduce false positives. A positive likelihood margin is not a requirement that every policy holds. Negative rule weights are not explicitly excluded. Classification accuracy is an empirical property of the learned rule model, not a universal enforcement guarantee. Equation 5 compares probabilities with one action bit flipped and state predicates fixed. The source supplies neither environment transition dynamics nor a proved inductive invariant/control-barrier condition linking that comparison to safe future trajectories. Current-state likelihood improvement does not by itself prove temporal safety. Predicates are grounded by learned search/binary-check models, moderation APIs, external sources and generated code. Observability and truthful, complete interaction history are required. Specialized operations use fine-tuned InternVL2-2B; formal tools include Stormpy in the main text and Prover9/Mace4 in the worked appendix. LTL over finite traces is defined in Appendix C.3, but most displayed rules and the worked code are propositional. The paper does not specify an end-to-end implementation or correctness argument for temporal monitoring, finite-trace termination, solver unknowns, missing observations or an inability to assign every predicate. The training recipe allows real labels or simulated pseudo-labels but does not give sufficient actual training/test splits, model hyperparameters, number of optimization steps, specialized-tool training data or random seeds to independently reproduce all reported scores. Algorithm 1 loops until all predicates are assigned without an explicit fallback budget. Human annotators manually label safety and violated policies. Annotator count, disagreement resolution, agreement rates and a detailed labeling protocol are absent. Policies include empirically constructed constraints as well as platform documents. Benchmark attacks are targeted to extracted policy violations. Existing benchmarks are augmented with policies and safe/unsafe trajectories. Scores concern those augmented guardrail tasks, not the original benchmarks unchanged. AWM is the protected web agent; results do not establish safety of arbitrary agents or environments.
  • how much was read: most of it read
  • record id: shieldagent-shielding-agents-via-2025
• SpecGen (2025)
  • title: SpecGen: Automated Generation of Formal Program Specifications via Large Language Models.
  • what: It generates JML annotations with an LLM. It then mutates candidate specs and selects among them using verifier feedback.
  • number: SpecGenBench: 120 Java tasks with expert references
  • number: blinded study: 15 Ph.D. students rated 15 programs
  • number: verifiable specifications for 279 out of 385 programs (SV-COMP Java tasks plus a manual 120-program set)
  • limits: Repair driven by the verifier can look like progress when an obligation is simply removed. Its verification rate is not comparable to equivalence rates. The human study covers only programs that were commonly solved.
  • how much was read: most of it read
  • source; notes: Generated contracts and independent evaluation; notes: SpecGen and StarVerus: human and model judges need an adequacy audit
  • record id: specgen-2025
• Specification Consensus (2025)
  • title: LLM-as-Specification-Judge: Multi-Model Consensus for Trustworthy Cryptographic Verification
  • what: Several different LLMs each write a formal spec in F* from the same standard (SHA-256, AES-128, ML-KEM). The proof assistant then tries to prove each pair equivalent, and a failed proof flags an error or a vague spot in the standard.
  • number: 3 primitives, 3 LLMs (GPT-4, Claude 3.5 Sonnet, Gemini 1.5 Pro)
  • number: all 9 specs generated; type-check 3/3, 3/3, 2/3
  • number: pairwise equivalence proved: SHA-256 3/3, AES-128 2/3, ML-KEM 1/3
  • number: discrepancies found: 0, 1 (wrong MixColumns polynomial), 2 (edge cases in polynomial arithmetic)
  • limits: Assumes LLM errors are independent; the paper admits correlated failures and ambiguous standards remain. Sample is three primitives with one run each and no baseline against single-author specs; no figures on how many human-written spec errors it caught, despite the abstract’s claim.
  • how much was read: most of it read
  • source; notes: ## LLM-as-Specification-Judge (2025)
  • record id: specification-consensus-2025
• SpecMAS (2025)
  • title: SpecMAS: A Multi-Agent System for Self-Verifying System Generation via Formal Model Checking
  • what: Agents turn a Standard Operating Procedure into a NuSMV model with CTL/LTL properties (statements about behavior over time). They revise both the model and the set of properties until model checking passes. The backbone is Qwen3-32B.
  • number: 10 example models (MiniSpecBench), 5 reported in detail
  • number: final compliance BRP 0.76+-0.08, autopilot 0.76+-0.01, mutual exclusion 0.77+-0.08, robot 0.69+-0.07, cache coherence 0.70+-0.05 (LLM-judge scores)
  • number: about 5-6 debugger iterations per case
  • number: MiniSpecBench: 10 models, 5 with detailed numbers
  • limits: Scores are weighted scores from an LLM judge. They do not show that requirements were proved. The SOPs were generated from expert examples. Properties can change, so the original intent may be lost. There is no link from model to code. Effort counts are not comparable to the baseline.
  • how much was read: most of it read
  • source; notes: SpecMAS: model and property repair must be distinguished; notes: SpecMAS: model and property repair must be distinguished
  • record id: specmas-2025
• SpecVerify (2025)
  • title: Supporting Software Formal Verification with Large Language Models: An Experimental Study
  • what: SpecVerify converts natural-language requirements and implementation code into an intermediate formalized requirement/test design, then generates C assertions checked with ESBMC. It compares Claude-based verification with FRET/CoCoSim and SLDV on Simulink-generated aerospace C code. Analyzes variable mapping and precondition/function/postcondition correspondence, gives triple-redundant voting and missing aircraft-weight-assumption cases, and traces a floating-point median-selection bug that rational arithmetic missed. Counterexamples are replayed against code when results differ. The authors report a mistaken +1-to-0 connection in a prior REG model.
  • number: 9 systems; 58 requirements; 41–251 C lines
  • number: 46/58 logical equivalence (79.31%)
  • number: Claude+ESBMC completion 27/58 (46.5%)
  • number: Table V false negatives: CoCoSim 6; Claude+ESBMC 2
  • limits: Nine retained systems contain only 41–251 C lines; one original benchmark cannot be converted. Benchmark code is generated and structured; larger manually written programs are untested. The logical-equivalence assessment is manual and can oversimplify temporal relationships. LLM and verifier effects are confounded. ChatGPT model naming varies across the source; Llama 3.1 8B failed tasks and was excluded. Table II/full-automation claims coexist with a stated need for considerable manual checking of generated code. Arithmetic inconsistencies remain in the source: 29/58 undetermined is labeled 39%; Table V false negatives are 6 versus 2, while the conclusion claims 6 fewer. These are source issues, not corrected measurements.
  • how much was read: most of it read
  • source; notes: Supporting software formal verification with LLMs (2025)
  • record id: specverify-2025
• The Coming Need for Formal Specification (2025)
  • what: An opinion piece proposing a workflow. First an English spec. Then several TLA+ models at different levels of detail. Then a formal proof, for example in Rocq, of the components the system depends on most. Finally an LLM audits the rest against the TLA+ spec.
  • number: seL4: 8,700 lines of C, 20 person-years, 200,000 lines of Isabelle (quoting Kleppmann)
  • limits: Opinion only, with no evidence.
  • how much was read: most of it read
  • source
  • record id: the-coming-need-for-2025
• TLAiBench (2025)
  • title: tlaplus/TLAiBench
  • what: 9 puzzle descriptions (for example DieHard, DiningPhilosophers, TowerOfHanoi) and 6 gold specs. A script asks an LLM to translate each description, then runs the syntax check and TLC.
  • number: 9 puzzle descriptions
  • number: 6 gold specs
  • number: inspected commit of 6 Feb 2026: ten puzzle descriptions, six gold models
  • number: no distributed implementation tasks; dining philosophers has no gold model
  • limits: No results are reported. Checking against the gold spec by refinement is only stated as a grading idea, and is not run at scale.
  • how much was read: most of it read
  • source; notes: Additional tools, not counted as papers; notes: TLAiBench
  • record id: tlaibench-2025
• Trustworthy agents LLM-FM position (2025)
  • title: Position: Trustworthy AI Agents Require the Integration of Large Language Models and Formal Methods
  • what: Argues for bidirectional LLM/formal-method integration: LLMs automate specification and proof work, while model checkers, theorem provers, SMT solvers, testing and runtime monitors constrain and certify LLM actions. The proposed six-stage pipeline starts from natural-language requirements, auto-formalizes them, runs model checking/theorem proving/SMT, tests edge cases, monitors executions and iteratively refines outputs. It sketches a Coq theorem-prover agent and a miniF2F even-number example. Sections 2–5 distinguish failure modes of LLM-only reasoning (hallucination, non-determinism, no traceability), FM-only workflows (specification effort, scalability and unpredictable environments), and hybrid trade-offs. The auto-formalization workflow creates a proof outline with placeholders, delegates algebraic gaps to external tools and revises failed proof steps. The model-checking discussion targets safety/liveness, deadlock and refinement; theorem proving targets machine-checkable proofs; SMT handles satisfiability; testing and monitoring cover behaviors outside proofs. Appendix A gives explicit Coq interaction steps and an Isabelle/HOL formalization attempt, making the proposal concrete but not an implemented benchmark. The implemented PAT prototype repairs GPT-4o car-lock modeling errors using model-checker traces: leavekey must require an open door, and locking receives explicit owner/key guards. Appendix A also gives Z3 meeting scheduling with missing unavailable-day constraints and a Dafny palindrome specification/implementation; these illustrate semantic alignment risks rather than measured success rates.
  • number: six pipeline stages: auto-formalization, model checking, theorem proving, SMT, testing, monitoring
  • number: Coq workflow has four steps from natural language to verified explanation
  • number: Appendix example uses sum of two even numbers
  • limits: This is a position/conceptual paper with case studies, not a controlled empirical evaluation. It assumes formal specifications and verifiers are available and sufficiently expressive; hybrid integration incurs representation mismatch and complexity. Formal methods can miss unmodeled or emergent behavior, while LLM-generated specifications/proofs still require verifier feedback and possibly human refinement. The Coq example is illustrative and does not establish agent success rates.
  • how much was read: most of it read
  • record id: trustworthy-agents-llm-fm-position-2025
• VerifyThisBench (2025)
  • title: VerifyThisBench: Generating Code, Specifications, and Proofs All at Once
  • what: Models generate code, spec and proof together for VerifyThis competition challenges. They use seven tools: Dafny, Why3, Frama-C, Verus, VeriFast, VerCors and TLA+. Each model gets five attempts with checker feedback. The XS variant removes parts of the verified submissions.
  • number: 41 challenges / 154 tasks; XS total 580 (226 code, 233 spec, 121 loop); 481 is stale
  • number: original human contest: 90 minutes per challenge
  • number: 41 challenges, 154 tasks, 580 sub-tasks
  • number: o3-mini under 4% zero-shot, 9.37% after five feedback rounds
  • limits: Alignment confidence is the model’s self-assessment (the paper calls it an ‘optimistic upper bound’). There is no independent exhaustive oracle for alignment. The notes did not establish that assume, admit or axiom is enforced. TLA+ gets no scoring for fairness or liveness. The human contest judges correctness, completeness, elegance and automation.
  • how much was read: most of it read
  • source; notes: VerifyThisBench / XS; notes: VerifyThis: human assessment supplies an intent layer
  • record id: verifythisbench-2025
• VeriGuard (2025)
  • title: VeriGuard: Enhancing LLM Agent Safety via Verified Code Generation
  • what: Given a security request, an LLM writes a Python policy and its constraints, asks clarifying questions, and tests the policy. Nagini verifies the policy against the contract before the policy gates agent actions.
  • number: average ASB attack success 0.0 percent for each backbone; Gemini-2.5-Flash task success 63.3 vs 40.2 for direct LLM guardrail
  • number: EICU-AC accuracy 100.0 for three backbones; Mind2Web-SC below perfect
  • limits: It is not a proof that the policy is equivalent to the request. The user must validate the intent. LLM-based argument extraction can feed in wrong facts. When no one is present to answer, clarification picks plausible defaults. There is no public code.
  • how much was read: most of it read
  • source; notes: VeriGuard: Enhancing LLM Agent Safety via Verified Code Generation
  • record id: veriguard-2025
• VeriPlan: Integrating Formal Verification and LLMs into End-User Planning (2025)
  • what: GPT-4 agents generate plans and translate natural-language constraints through LTL templates into PRISM properties. Users approve back-translated rules and set constraint strictness; an external checker feeds violations back to the planner. [Q1–Q3] The implementation separates mapping, LTL translation, PRISM translation, plan-to-PRISM translation, and checking using PRISM/Stormpy. Sliders implement weighted sampling of constraints: a soft rule may not be checked. Plans receive at most three iterations before users revise constraints. The within-subjects study compares the full UI with removal of sliders, rule confirmation, or all verification features. [Q1–Q4]
  • number: 12 participants
  • number: 3 scenarios; 2 assigned per participant
  • number: 4 study conditions
  • number: 3 plan iterations
  • limits: Checker acceptance is relative to LLM-translated models and approved/sampled properties; this is a reader inference from the pipeline, not proof that natural-language plans satisfy every intended constraint. The study measures perceived performance/usefulness/satisfaction rather than an objective correctness benchmark; 12 participants from university mailing lists cover only three scenarios. Linked OSF prompts/code/questionnaires were not inspected. §3.4 says seven mapping categories before listing six; §5.2 says no significant differences despite §5 reporting slider-removal usefulness p=.047. [Q2,Q4–Q7]
  • how much was read: most of it read
  • source
  • record id: veriplan-integrating-formal-verification-2025
• VLTL-Bench (2025)
  • title: Verifiable Natural Language to Linear Temporal Logic Translation: A Benchmark Dataset and Evaluation Suite
  • what: It scores four steps of translating natural language to LTL. The steps are finding propositions, translating temporal structure (judged by logical equivalence, not string match), grounding to executable predicates, and classifying satisfying and violating traces.
  • number: datasets: Kitchen Assistant 10,000, Search-and-rescue 7,304, Traffic-light 7,319, Warehouse 7,457
  • number: built from 36 expert nl2spec templates
  • number: Table 2: four generated datasets of 10,000; 7,304; 7,319; 7,457 entries (32,080 total) reusing 43 templates
  • number: 36 expert-crafted lifted NL-LTL pairs plus 7 new ones
  • limits: Its equivalence check only flags a difference. It does not say whether one formula is weaker or stronger. Two traces cannot establish equivalence or liveness. It has no proof, no code, and no audit of how far to trust agents. The text says three datasets but the table lists four.
  • how much was read: most of it read
  • source; notes: Temporal requirement translation: VLTL-Bench and GraFT; notes: papers
  • record id: vltl-bench-2025
• Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency (2024)
  • what: # Whole reading: Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency (authored by agents unless marked 🧑) The framework generates ten Isabelle statement candidates, ranks them using symbolic agreement and back-translation similarity, and selects results. SymEq checks premise and conclusion equivalence after numerical standardization or heuristic variable matching, then scores equivalence-class size. SemCo asks an LLM to informalize each candidate and computes BERT cosine similarity to the original problem. Log, linear and quadratic combinations weight normalized scores, with alpha=0.5 selected empirically. It is a candidate-selection method; it neither supplies a verified translation relation to natural language nor proves that a majority class expresses the intended problem. [Evidence: Q2, Q3, Q4, Q5, Q8 in quotes.json.] The prose before Definition 1 requires noncontradictory premises, but Definition 1 says premises are not tautologies. Those conditions differ: False is not a tautology but is contradictory; True is noncontradictory but is a tautology. The proposed P implies False check can establish contradiction when a sound prover succeeds; failure or timeout does not establish satisfiability. Premise-equivalence plus conclusion-equivalence is stronger than equivalence of whole implications. The text also calls the true product statement symbolically equivalent to 4=4; that claim requires the later auxiliary-variable projection/simplification interpretation, not the literal componentwise definition alone. These are written-definition qualifications, not an implementation audit. [Evidence: Q3, Q4, Q13 in quotes.json.] Numerical standardization introduces alpha=f(x) and compares residual-value relations, leaving original variables auxiliary. The quantifier/projection semantics must be specified: the printed free-variable equivalence in Appendix C is false if x,y,a,b remain independent (x=2/3,y=6,alpha=0,a=0 makes its left premise true and right premise false). Existentially quantifying auxiliaries makes that example work but can discard modeling structure and identify unrelated solved true problems through the same residual set. Non-numerical matching uses edit-distance weights and top-k maximum bipartite matchings; maximizing raw distance favors dissimilar names unless the weight is negated or converted to similarity. Finite heuristic matching and incomplete ATP search can miss genuine equivalences; no completeness theorem is provided. Appendix C Example 2 asks for five positive integers, but both displayed nat statements admit all five equal to zero, with n=0 in No.1. Then 4^0=1 is not divisible by 2. No.1 also retains an extra variable n and its sum assumption, so the displayed variable counts differ and the projection/elimination step needs specification. This is a manual boundary check, not a checked formal counterexample. [Evidence: Q3, Q13, Q4, Q20 in quotes.json.] Back-translation is fallible model output, and embedding similarity is a numerical proxy rather than a proof of preserved meaning. The paper itself notes that notation changes can alter mathematical meaning while embeddings miss them. Its power example explicitly maps both powr and natural-exponent power back to the same word, which can hide the very distinction being checked. Shared model errors and correlated wrong candidates remain possible; consensus does not establish the correct domain, quantifiers, definitions or assumptions. [Evidence: Q4, Q12, Q14 in quotes.json.] Section 3.3 and Algorithm 1 call normalization softmax, while the displayed formulas divide each score by the sum of scores without exponentials. For scores 1,2 these give 1/3,2/3; actual softmax gives about 0.269,0.731. This can change a combined ranking. Raw cosine scores need not all be positive and their sum can be zero, so the printed division/log combination needs positivity and nonzero-denominator conditions or a stated transform. The publication does not specify that safeguard. This identifies ambiguity in written mathematics, not which normalization author code executes. [Evidence: Q5, Q4 in quotes.json.] MATH evaluation randomly selects 400 problems; miniF2F contains 488 problems with formal oracles. Five models are Mistral-7B,Llemma-34B,DeepSeek-v2,Codex completion API and GPT-4(version 0710), temperature 0.7, ten candidates and declared eight-shot examples. MATH candidates are manually labeled; miniF2F correctness is automated equivalence against the supplied oracle. n@k denotes whether the top n of k candidates includes a correct version. The log-probability baseline changes to prompted ranking for Codex/GPT-4; Naive filters provable candidates, and Cluster uses adaptive k-means on formal-statement BERT embeddings. The checker uses scala-isabelle, twelve listed Isabelle tactics including Sledgehammer timeout 300 s, and Z3/CVC5. The authors report eight examples, but Appendix F prints two generic instruction templates without an identifiable complete block of eight demonstration pairs. Their archive contents remain uninspected. [Evidence: Q6, Q5, Q14 in quotes.json.] miniF2F scores measure agreement with a finite automatic oracle-equivalence procedure, which shares the SymEq machinery and can miss valid alternate encodings or inherit flawed oracles. They are not independently human-adjudicated semantic-correctness rates. Manual MATH labeling lacks a fully described annotator count, agreement/adjudication protocol and blinded treatment of methods in this publication. The paper itself discusses human errors and problematic formal oracles. Passing a prover for a generated statement establishes only that statement relative to its assumptions and trusted checking, not that the natural-language task was formalized faithfully. [Evidence: Q6, Q12, Q14, Q16, Q17 in quotes.json.] Table 1 GPT-4 MATH1@10 is37.5% baseline,42.0% SymEq,39.5% SemCo; miniF2F is32.9%,41.1%,34.9%. Figure 5 log-comb gives45.3% and43.6%, improvements of7.8 and10.7percentage points over those baselines and3.3/2.5points over SymEq. Codex MATH log-comb reaches49.4%. These are reported empirical selection gains under the stated labeling procedure, not formal guarantees or evidence on distributed-system specifications. SymEq is not best in every Table 1 cell: Mistral MATH3@10 SemCo38.8 exceeds SymEq37.9. [Evidence: Q6, Q7, Q8 in quotes.json.] Do not silently merge differing displayed values. Figure 5 Llemma MATH SymEq41.4/SemCo35.4 differ from Table 1 41.1/36.5; miniF2F SymEq31.2 differs from32.0. Figure 5 Mistral MATH SymEq26.7 to log-comb42.6 is15.9percentage points (about59.6%relative), not the RQ2 prose22.6% when read as that comparison. Table 2 geometry SymEq28.1 exceeds SemCo25.1, so the narrative about geometry favoring semantic sensitivity is a hypothesis, not a demonstrated category gain. The paper does not resolve these table/figure/text discrepancies. Figure 5 miniF2F labels its pink series SemCo but prints 7.5,20.5,27.6,29.7,34.8, versus Table 1 SemCo 8.8,27.2,27.6,33.2,34.9. Figure 5 MATH Codex SemCo is 42.6 versus Table 1 44.9. Figure 4, captioned GPT-4 MATH log-comb, has visually estimated endpoints near 46.6–46.7 and a peak near 47.5. These disagree with Table 1 semantic/symbolic endpoints 39.5/42.0 and Figure 5 log-comb 45.3. At alpha=0 the log combination ranks only by semantic score. Appendix D Figure 7 also uses a 45.5–48 range. No undocumented split, model or correction is inferred to reconcile these displays. [Evidence: Q6, Q7, Q8 in quotes.json.] RQ3 prints sigma=sum over n=2..k-1 of n times(q_n-q_(n-1)) plus(1-q_k), with q_n=n@k. Under ordinary sequential inspection of up to k candidates, expected checks are sum over n=1..k of n times(q_n-q_(n-1)) plus k(1-q_k), q_0=0. The printed formula gives0 if the first candidate is always correct,0 if only the kth is correct, and1 if none is correct, instead of1,k,k. Thus it is not the stated ordinary average number of formal statements labeled without an additional unreported cost convention. Table 3 reports17.7–21.6% MATH and8.4–21.9% miniF2F relative savings for log-comb; these are derived scores, not measured human-time reductions. No author-code recalculation performed. [Evidence: Q9 in quotes.json.] At k=10 there are at most45unordered candidate pairs before transitivity shortcuts, plus ten informalizations. The full checker versus auto/simp-only GPT-4 ablation reports 1@10 both 41.1%, 2@10 48.1 versus 47.5, and 3@10 49.3 versus 48.7. Its values match miniF2F in Table 1, but Figure 6 and the RQ4 paragraph do not explicitly name the dataset. The prose lists2.13vs2.33equivalences while saying the normal checker proves more, without ordering these two values clearly. Table 4 GPT-4 MATH log-comb declines from75.6% at difficulty1 to27.0% at5, but level3 SymEq57.1 exceeds log-comb53.8, so combination is not universally better by subgroup. Checklist 7 explicitly reports no statistical significance due to cost. Full walltime/API expenditure and independent repeat-run variability are not reported in the28-page publication; checklist 8 points to supplementary resources. [Evidence: Q10, Q20, Q5 in quotes.json.] The source reports a nonexistent reflection_matrix in Example 3 and omitted Vieta constraints in Example 4. Its surrounding prose says rst=8 is incorrect, although the cubic4x^3-59x^2+32x-32 actually has product8; the displayed bad output instead uses32. The pairwise-root sum8 is indeed omitted, and r+s+t=59/4 is correct. This distinction preserves the actual displayed error rather than copying the prose typo. These cases motivate library grounding and exact assumption validation. [Evidence: Q14, Q15 in quotes.json.] Example 5 attributes failure to using ^ with real bases a,b. Natural-exponent powers permit real bases; the displayed exponent is the natural number2, so that reason does not follow. The text conflates base and exponent typing. Powr and ordinary powers can differ outside positive-base domains, and log-domain constraints must be handled explicitly; Examples 9–10 report failed equivalence attempts, not proof that every displayed difference is mathematically inequivalent. No Isabelle run was made to validate a specific historical checker trace. [Evidence: Q4, Q14, Q15, Q17, Q18 in quotes.json.] Example 8 labels the rational-equation oracle wrong because it omits explicit nonzero denominators, and says dividend rather than denominator. Under Isabelle/HOL real division totalized by inverse0=0, the equality itself excludes x=1/3 (0 versus3/2) and x=-1 (-1/4 versus0). Elsewhere cross multiplication gives x+1=6x-2, hence x=3/5. The extra denominator assumptions are therefore redundant for this particular equality. This manual domain/algebra check does not support the claimed oracle defect; no formal checker or author artifact was run. [Evidence: Q17, Q14 in quotes.json.] Example 11 attributes a failed equivalence to spaces around4 and says the two4types cannot be inferred identical. Its displayed comparison explicitly annotates both4::nat and repeats the same set expression up to ordinary whitespace, so the printed text does not establish that diagnosis. Both original claims also omit positive n and are false at n=0 because2 does not divide1, although false statements can still be equivalent. The distinction between equivalence and truth matters here. A missing historical context or implementation parsing error remains unverified. [Evidence: Q18, Q14 in quotes.json.] Example 13 No.2 replaces the midpoint theorem with the assumed numerical relation DE=BC/2, reducing geometry to arithmetic; the source calls this over-simplification. No.1 also explicitly fixes dist as an arbitrary function, rather than requiring Euclidean distance. Choose A=(0,0),B=(2,0),C=(0,2),D=(1,0),E=(0,1), and a function with dist(B,C)=6 and dist(D,E)=0: all printed premises hold but conclusion dist(D,E)=3 fails. Thus that displayed version has a concrete missing semantic constraint, beyond a human preference about abstraction. This is a manual model of the printed statement, not an executed counterexample. [Evidence: Q19, Q12 in quotes.json.] Example 6 contrasts human labels on two cardinality encodings; Example 7 highlights positive-integer versus nat-domain oracle issues; Example 12 uses a real parameter2*n to represent even integers, which does not itself enforce integrality. These illustrate that equivalence search, domain checks, library grounding and human review must be separated when evaluating generated specifications. This is directly relevant methodology for LLM-written statements and proofs; transfer to Verus, verified Rust, TLA+ or distributed protocols is reader inference. No such artifact or end-to-end systems-verification result is contributed. The complete 28-page publication, 13 examples,bibliography and checklist were read. The 946-member official archive was saved and its manifest inspected; code,data and plot assets were not executed or loaded as scientific results. [Evidence: Q16, Q19, Q12, Q20, Q1 in quotes.json.] Primary excerpt R2, §3.1, Definition 1 and premise test; lit_venues/full_text_recovered/formal1239/paper.raw.txt, characters 14019–14969: > The formal definition of symbolic equivalence is presented in the following. Within this definition, > we further assume that the premises are not intrinsically contradictory, ensuring that the two involved > mathematical statements are well-defined. > Definition 1 (Symbolic equivalence) Let two mathematical statements Ψ1 and Ψ2 in formal lan- > guage be expressed as P1 → Q1 and P2 → Q2, and suppose their premises P1 and P2 are > not tautologies. Then, the two statements are called symbolically equivalent if the two logical > equivalences, i.e., P1 ≡ P2 and Q1 ≡ Q2, both hold. > The two logical equivalences induced by the symbolic equivalence can be determined through existing > automated theorem provers (ATPs). Additionally, the validity of the premises can also be checked by > replacing the conclusion Q with a contradictory result (e.g., 0 = 1) and verifying P → Q. If this > vacuous form can be proved, then the corresponding premise P is a contradiction. Primary excerpt R4, §3.1, matching heuristic; lit_venues/full_text_recovered/formal1239/paper.raw.txt, characters 16934–17109: > we simply set the edge weight of the graph by the string edit distance [61, 62], and only partially > enumerate variable mappings corresponding top-k maximum bipartite matching. Primary excerpt R10, §4.1, correctness labels; lit_venues/full_text_recovered/formal1239/paper.raw.txt, characters 25928–26156: > statements, we manually check each formalization result. For the miniF2F dataset, the correctness is > automatically derived by checking the symbolic equivalence between the formalization result and the > provided oracle using ATPs. Primary excerpt R20, Appendix B, embeddings limitation; lit_venues/full_text_recovered/formal1239/paper.raw.txt, characters 55414–55828: > Embeddings may neglect the nuances in natural language. When using embeddings to check > semantic consistency, we assume embeddings can reflect the differences between the informalized > statement and the original. However, there are many nuances in math statements that even a single > notation change can result in totally different semantics. Current embeddings may not differentiate > the minor but significant change. Primary excerpt R29, Appendix F, prompt examples claim; lit_venues/full_text_recovered/formal1239/paper.raw.txt, characters 62055–62243: > We set up instructions and eight gold examples with both symbolic and semantic correctness to > improve the generation performance of GPT-4. Our detailed prompts are shown in Prompt 1 and 2. Primary excerpt R31, Checklist 7, uncertainty; lit_venues/full_text_recovered/formal1239/paper.raw.txt, characters 78816–79144: > 7. Experiment Statistical Significance > Question: Does the paper report error bars suitably and correctly defined or other appropriate > information about the statistical significance of the experiments? > Answer: [No] > Justification: We cannot provide statistical significance of the experiments due to the > extensive evaluation cost.
  • limits: The framework generates ten Isabelle statement candidates, ranks them using symbolic agreement and back-translation similarity, and selects results. SymEq checks premise and conclusion equivalence after numerical standardization or heuristic variable matching, then scores equivalence-class size. SemCo asks an LLM to informalize each candidate and computes BERT cosine similarity to the original problem. Log, linear and quadratic combinations weight normalized scores, with alpha=0.5 selected empirically. It is a candidate-selection method; it neither supplies a verified translation relation to natural language nor proves that a majority class expresses the intended problem. MATH evaluation randomly selects 400 problems; miniF2F contains 488 problems with formal oracles. Five models are Mistral-7B,Llemma-34B,DeepSeek-v2,Codex completion API and GPT-4(version 0710), temperature 0.7, ten candidates and declared eight-shot examples. MATH candidates are manually labeled; miniF2F correctness is automated equivalence against the supplied oracle. n@k denotes whether the top n of k candidates includes a correct version. The log-probability baseline changes to prompted ranking for Codex/GPT-4; Naive filters provable candidates, and Cluster uses adaptive k-means on formal-statement BERT embeddings. The checker uses scala-isabelle, twelve listed Isabelle tactics including Sledgehammer timeout 300 s, and Z3/CVC5. The authors report eight examples, but Appendix F prints two generic instruction templates without an identifiable complete block of eight demonstration pairs. Their archive contents remain uninspected. miniF2F scores measure agreement with a finite automatic oracle-equivalence procedure, which shares the SymEq machinery and can miss valid alternate encodings or inherit flawed oracles. They are not independently human-adjudicated semantic-correctness rates. Manual MATH labeling lacks a fully described annotator count, agreement/adjudication protocol and blinded treatment of methods in this publication. The paper itself discusses human errors and problematic formal oracles. Passing a prover for a generated statement establishes only that statement relative to its assumptions and trusted checking, not that the natural-language task was formalized faithfully. RQ3 prints sigma=sum over n=2..k-1 of n times(q_n-q_(n-1)) plus(1-q_k), with q_n=n@k. Under ordinary sequential inspection of up to k candidates, expected checks are sum over n=1..k of n times(q_n-q_(n-1)) plus k(1-q_k), q_0=0. The printed formula gives0 if the first candidate is always correct,0 if only the kth is correct, and1 if none is correct, instead of1,k,k. Thus it is not the stated ordinary average number of formal statements labeled without an additional unreported cost convention. Table 3 reports17.7–21.6% MATH and8.4–21.9% miniF2F relative savings for log-comb; these are derived scores, not measured human-time reductions. No author-code recalculation performed. Example 6 contrasts human labels on two cardinality encodings; Example 7 highlights positive-integer versus nat-domain oracle issues; Example 12 uses a real parameter2*n to represent even integers, which does not itself enforce integrality. These illustrate that equivalence search, domain checks, library grounding and human review must be separated when evaluating generated specifications. This is directly relevant methodology for LLM-written statements and proofs; transfer to Verus, verified Rust, TLA+ or distributed protocols is reader inference. No such artifact or end-to-end systems-verification result is contributed. The complete 28-page publication, 13 examples,bibliography and checklist were read. The 946-member official archive was saved and its manifest inspected; code,data and plot assets were not executed or loaded as scientific results. Source diagnostics independently reviewed.
  • how much was read: most of it read
  • source
  • record id: autoformalize-mathematical-statements-by-2024
• Autoformalizing Euclidean Geometry (2024)
  • what: Introduces LeanEuclid, 173 manually formalized Euclidean geometry statement/proof/diagram examples, and a Lean implementation of a variant of system E. A symbolic SMT engine fills implicit diagrammatic proof gaps and evaluates statement equivalence as E3. January2024 GPT-4/GPT-4V few-shot experiments report up to21.0% solver-proved statement equivalence and23.1% proof acceptance across the143-item evaluation set. SMT answers are admitted through an explicitly unsound axiom rather than reconstructed as Lean proof terms, so results require trusting the translation and SMT solvers as well as the Lean kernel. Separates explicit construction steps, chosen by humans/models, from non-construction diagrammatic/metric/transfer reasoning handled by SMT refutation. euclid_apply instantiates a rule, proves missing premises with SMT, and adds conclusions/witnesses; euclid_finish/assert discharge goals. E3 checks both implication directions plus contradiction detection; approximate comparison requires matching numbers/types of bound variables, selects top-n renamings by string similarity, and counts four directions of pre/postcondition obligations, adding preconditions to postcondition comparisons only after precondition equivalence. Dataset contains all48 Elements BookI propositions and125 UniGeo examples (25 each in five categories); texts are manually augmented/abridged. Appendices give a full axiom catalogue, a missing-case reconstruction for Elements24, formalization comparisons, exact prompts, partial semantic outcomes, and before/after repair scripts.
  • limits: Correctness is relative to the chosen geometric axioms and Lean-to-SMT encoding. AppendixC explicitly introduces an unsound axiom to admit successful SMT queries; there is no end-to-end kernel certification or SMT proof reconstruction. The reader did not audit or execute the released implementation. SystemE soundness/completeness is attributed to Avigad etal for its original axioms. This implementation adds construction, diagrammatic and transfer rules, strengthens one construction rule, and uses SMT real-number theories. The supplied paper does not mechanize a soundness proof of the modified implementation. The diagrammatic engine uses diagrammatic,metric,transfer rules. Equivalence checking additionally uses nine simple construction rules. Limited construction/instantiation makes E3 incomplete; failure to establish equivalence is not proof of inequivalence. Logical equivalence of closed true theorems can be weaker than faithful correspondence of hypotheses,objects and informal meaning. The paper itself reports a logically equivalent but unfaithful quadrilateral/parallelism example; success should not be read as comprehensive intent validation. Approximate equivalence is a bounded heuristic over variable unifications and clause counts, not a semantic distance with a correctness theorem. It excludes formulas with differing variable counts/types and depends on chosen clauses and names. Evaluation uses gpt-4-1106-preview and gpt-4-1106-vision-preview in January2024, one domain, manually prepared prompts and a small curated test split. No significance intervals or multiple-run variance are reported. Proof autoformalization receives a correct formal statement and informal proof, whereas statement autoformalization is evaluated separately. Proof success cannot establish an end-to-end informal-statement-to-correct-proof rate. Manual Elements repairs use ground-truth proofs and a minimum-change preference; Levenshtein ratios measure textual alteration, not time,semantic effort,independent automation success or proof validity. Data-contamination improbability is the authors inference from LeanEuclid being unpublished at experiment time. Models may have seen Elements/UniGeo or other formalizations; no pretraining audit is supplied. No distributed systems,Verus,Rust or TLA+ evaluation occurs. Reuse of domain rules and semantic equivalence checks in those settings is a reader hypothesis, not established transfer.
  • how much was read: most of it read
  • record id: autoformalizing-euclidean-geometry-2024
• Clover (2024)
  • title: Clover: Closed-Loop Verifiable Code Generation
  • what: GPT-4 reconstructs code, contracts and English documentation from one another. Dafny and cross-checks then inspect whether they agree.
  • number: 52 of 60 correct examples accepted at ten attempts; tested adversarial examples rejected (Section 4)
  • limits: LLM reconstructions are correlated, so they can share a mistake. Agreement does not prove the English intent was encoded faithfully.
  • how much was read: most of it read
  • source; notes: Dafny, C verification, and the specification-intent gap; notes: Generated contracts and independent evaluation
  • record id: clover-2024
• Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages (2024)
  • what: Scores LLM-written Dafny specs by checking concrete input/output pairs symbolically, including pairs with deliberately wrong outputs. In a set-intersection example, the contract says every result is in both inputs. It does not require every common element to appear.
  • number: applied to 64 of 153 MBPP-DFY specifications
  • limits: A failed verification usually means ‘unknown’, not ‘refuted’. Rejecting bad pairs measures only the pairs chosen. It does not show the spec rejects bad outputs in general.
  • how much was read: most of it read
  • source; notes: Testing strength, mutations, and vacuity; notes: User-intent formalization in verification-aware languages
  • record id: evaluating-llm-driven-user-2024
• IronSpec (2024)
  • title: IronSpec: Increasing the Reliability of Formal Specifications
  • what: Tests whether a Dafny specification matches what developers expect. It uses three methods: checks with unconstrained inputs and outputs, small proofs of cases that should or should not be allowed, and mutations of the specification.
  • number: 14 specifications including six real verified systems; ten spec bugs confirmed by authors
  • number: 70 small test proofs, 21 needed help averaging 1.7 added lines
  • number: 61 surviving mutations, 13 judged intended
  • number: human effort hours to days; DaisyNFS about one to two hours
  • limits: The checks expose suspicious differences. They do not show the spec perfectly matches intent. It gives no success rate for autonomous spec generation.
  • how much was read: most of it read
  • source; notes: Specification errors and auditing; notes: IronSpec
  • record id: ironspec-2024
• MoSt (2024)
  • title: Modeling and Verification of Natural Language Requirements based on States and Modes
  • what: Engineers write requirements in a controlled language that names states, modes and transitions. A tool generates NuSMV models and automatically checks that each state is reachable. It reports results at the requirement IDs.
  • number: car: 5 states, 2 modes, 37 requirements, 88 NuSMV lines
  • number: washing machine: 15 states, 5 modes, 64 requirements, 213 NuSMV lines
  • number: 14 injected errors all detected
  • number: check times 0.003/0.042/0.032 s (car) and 0.005/13.371/13.467 s (washer)
  • limits: Humans must first identify the states, modes and properties. Extracting them from free prose is future work. It has two authored examples only. It has no code proof.
  • how much was read: most of it read
  • source; notes: MoSt: humans structure requirements before automatic model checking; notes: MoSt: humans structure requirements before automatic model checking
  • record id: most-2024
• nl2postcond (2024)
  • title: Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?
  • what: Has LLMs generate executable postconditions from plain descriptions. Measures both correctness and whether they reject known buggy implementations (bug-completeness).
  • number: catches 64 real-world historical bugs from Defects4J
  • limits: Rejecting those bugs does not fully describe which outputs are acceptable. Reference programs and tests remain part of the oracle. Correctness is only with respect to the provided tests.
  • how much was read: most of it read
  • source; notes: Testing strength, mutations, and vacuity; notes: Natural-language postconditions and known faulty implementations
  • record id: nl2postcond-2024
• PropertyGPT (2024)
  • title: PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation
  • what: PropertyGPT retrieves human-written Certora properties by embedding their associated code, prompts GPT-4-turbo to generate Solidity-like PSL properties for new contracts, repairs candidates with compiler/static feedback, ranks them by code/property similarity, and verifies them with source-level symbolic execution, modular verification and bounded model checking. The PSL intermediate language expresses invariants, function pre/postconditions and scenario rules in Solidity-like syntax. A conservative code-similarity threshold retrieves roughly 10–20 references; generated properties are iteratively repaired (up to nine attempts in the implementation), checked for inclusion of the target function, then ranked using four raw/summary embedding similarities with learned weights α=.134, β=.556, γ=.141, η=.168. The prover uses strongest-postcondition symbolic execution and Z3, over-approximates unknown on-chain calls, and bounds model checking to depth three (five loop iterations). The dataset contains 623 properties from 23 Certora projects; tests include 90 held-out properties, 13 CVEs, 24 attack incidents and four bounty projects.
  • number: 623 properties from 23 projects
  • number: 90 held-out properties
  • number: recall 0.80, precision 0.64, F1 0.71
  • number: 9/13 CVEs
  • limits: Certora CVL and generated PSL properties lack an automated equivalence checker; three authors manually judged semantic equivalence. On-chain calls are assumed to succeed with symbolic return data, and nonlinear functions use uninterpreted approximations. Bounded checking can miss deeper behavior, runtime context is not modeled, and top-K ranking/generation depends on GPT-4-turbo and a hand-curated knowledge base. The reported zero-day findings require manual confirmation and responsible-disclosure fixes.
  • how much was read: most of it read
  • source
  • record id: propertygpt-2024
• Synthetic Programming Elicitation for Text-to-Code in Very Low-Resource Programming and Formal Languages (2024)
  • what: SPEAC makes an LLM generate a familiar intermediate language, repairs that output with compiler checks and weighted MAX-SMT, then translates it into a language poorly represented in training data. Eudoxus instantiates this with a subset of Python that describes UCLID5 transition systems. It prunes unsupported syntax, replaces inconsistent syntax-tree nodes with holes, infers repairs from a satisfying model and asks the LLM to fill remaining holes. The evaluation measures compiler acceptance and a single author’s manual semantic scores on 33 textbook tasks. Preserves how the intermediate language was manually designed, exact pruning/constraint/repair contracts and minimality conditions, the traffic-light input ownership mistake, type and timer concerns, every result-table cell and denominator, three dataset roles, baseline and call settings, manual scoring, timing components and limits of the semantic claim. Distinguishes satisfying static constraints from preserving intended behavior or proving the generated transition system.
  • limits: §3–§5: Requires a target language T, familiar parent P, child subset C and compiler f:C→T. Here T is UCLID5, P Python and C an abstract Module subclass with declaration/init/next methods. The language design and syntax-directed translator are supplied by people; the paper does not prove compiler semantic preservation or automatically derive a correct modeling language. §5.1: Synthetic elicitation is a manual lightweight grounded-theory analysis of LLM outputs, not a human-subject study. People label output fragments, group codes into concepts/categories and design C. The object-oriented category is chosen for ease of translation; no experiment establishes universal LLM naturalness or superiority over every alternative child language. §5.1, p.6: GPT-3.5-turbo-0125 and GPT-4-turbo-2024-04-09 each generate ten samples on each of 33 curated regression tasks: 660 direct-UCLID5 attempts, none parses. This is a result for those models/tasks, not a universal inability theorem. Imaginary FormalVerificationLibrary prompts elicit from-scratch Z3, procedural API and object-oriented subclass styles. §5.2/Figure 4: Initial prompt specifies parent, task, unique code block and child description, ending with an affirmative assistant prefix. Repair prompt asks to replace every ?? and repeats the task. The templates are partial; the PDF does not include every concrete benchmark prompt or the complete child grammar. §5.3: Error-tolerant parsing first builds a parent-language AST, then removes constructs outside C. This initial pruning may lose program intent. Static checks are encoded as soft clauses per node; MAX-SMT keeps a satisfiable weighted subset and rejected clauses identify nodes to replace with holes. Hard clauses and algebraic data types constrain legal structure. §5.3, p.7: Minimum node-edit guarantee is conditional on uniform weights and exactly one clause per node. Actual depth-proportional weights favor edits near leaves and explicitly break syntactic minimality guarantees. Largest consistent subtree therefore does not imply globally fewest edits in the implementation or smallest semantic change. §5.4: A satisfying model can infer a hole’s type, e.g. integer from integer-literal assignment; unresolved holes return to the LLM. Satisfying static constraints establishes a well-formed intermediate program, not equivalence to its original candidate, natural-language task satisfaction or a verified safety/liveness property. §3/Figure 1: Compiler-accepted traffic-light output declares pedestrian with var and initializes it false, although the task requires a nondeterministic input from another subsystem. Authors explicitly identify var→input as a semantic correction. Inference for distributed modeling: changing an environment input into locally controlled state can remove executions and make a property misleadingly easy to satisfy. Figure 1 lines 13–15 and Figure 5: The shown state-zero branch resets count to zero immediately before checking count<60 and incrementing it. Under the sequential step semantics suggested by the excerpt, that prevents this branch reaching 60. This is an apparent concern in a partial excerpt, not a confirmed full-model counterexample; the complete generated model and execution were not inspected. Authors discuss the pedestrian mistake, not this timer concern. Figures 5–6: Repairs replace BitVector declarations with int to match integer literal use, and replace Boolean()/False values in declarations with bool. Changing a bounded bitvector to integer changes wraparound/range behavior; static consistency alone does not preserve a bounded-state interpretation. Final snippets also show declarations/init separately and contain ellipses. §3/Figure 5: Figure 5 caption identifies (a) initial output and (b) repair; overview prose reverses these references. Figure 6 likewise contains partial outputs. Preserve the caption/code reading rather than treating the displayed snippets as a complete executable proof artifact. §6: Python implementation uses tree-sitter and Z3 MAX-SMT; local solver machine is a 2.3 GHz quad-core Intel Core i7 with 32 GB RAM, LLMs through OpenAI Python API. Repository is https://github.com/FedericoAureliano/eudoxus. This read covers the PDF, not repository code or a reproduced run. §6/Table 1: Text says allow repair loop five times; caption says limited to five LLM calls per benchmark. Self-repair baseline uses five iterations starting from zero-shot. Exact initial-call versus repair-count convention is not reconciled in the PDF; use the caption’s reported cap without silently adding an initial sixth call. §6: Three datasets have distinct roles: 33 curated developer regression tests with hand-written descriptions for language design; 317 repository regression tests self-summarized by the LLM for fine-tuning; 33 textbook exercises/examples for end-to-end evaluation. Textbooks are Baier/Katoen 2008, Lee/Seshia 2016 and Huth/Ryan 2004. No explicit split-overlap/contamination audit is given. §6: Fine-tunes GPT3t for 284 steps with learning-rate multiplier .16; no GPT4t fine-tune is reported. Baselines include one/three examples, with/without chain of thought, each on two models; two compiler-feedback self-repair variants; and fine-tuning. That is eleven baseline variants plus two Eudoxus variants, thirteen Table 1 rows; prose saying all eleven approaches is a counting slip. Abstract/§6: Abstract mentions retrieval baselines, but the specified baseline is repository few-shot prompting; no operational retrieval pipeline, retriever-quality measurement or retrieval ablation is described. Do not infer a separate implemented RAG system from that phrase. §6.1: Parse is shorthand for passing all compiler checks, including static typing, rather than grammar alone. Semantic assessment is one author’s manual reasoning plus hand-written specifications, performed only for compiled outputs. Scores run from 1 entirely wrong to 5 fully correct; ≥4 means authors believe useful, allowing minor errors. This is not an independently machine-checked end-to-end correctness result. Table 1: GPT3t Eudoxus parses 28/33=84.8%; GPT4t 24/33=72.7%. Combined 52/66=78.8% explains approximately 78% prose. Fine-tuning Table 1 is 2/33=6.1%, inconsistent with introduction 9.1%; preserve the discrepancy. Best GPT4t few-shot parses 4/33=12.1%. Percentages here are derived from printed counts. Table 1: Fully correct score-5 outputs are GPT4t 11/33 and GPT3t 9/33, not 24/33 or 28/33. Useful score≥4 outputs are 19/33 and 14/33 respectively. These derived unconditional denominators differ from the table’s conditional semantic denominators of 24 and 28 compiled outputs. §6.1: Across both Eudoxus variants, 30/33 unique tasks have at least one compiled output; across all eleven baseline variants, only 6/33 do. Eudoxus has 33/52 compiled outputs scoring ≥4, covering 24 unique tasks. Four unique baseline-useful tasks are also useful under Eudoxus. These unions are not a single model’s success rate or 33 verified specifications. §6.1: Four benchmarks hit iteration cap and three suffer implementation syntax/output-extraction/printing bugs. Their scope across model variants is unclear: the two table rows together have fourteen non-compiling outputs. Do not assign the seven reported cases independently to both models or invent an overlap explanation. §6.1, p.10: Reported GPT3t mean repair time .9 s (SD .6), LLM time 7.2 s (SD 4.6); GPT4t repair 1.8 s (SD 2.0), LLM 35.1 s (SD 24.7). These components support that LLM calls dominate reported local repair time. They are not total project compute, API dollars, token counts or a precisely specified aggregate wall-clock distribution. §6.1–§6.2: Authors explicitly caution that few baseline outputs compile, making conclusions about semantic performance difficult. No ablation separates child-language design, pruning, model-based repairs and repeated LLM calls; no broad budget-matched repeated-sampling comparison is reported. §6.2/Checklist: Only one target language, two LLMs and one semantic rater. No inter-rater agreement, semantic-score confidence intervals or statistical-significance claim; checklist item 7 explicitly calls this a case study. Generalization to other languages/models remains open. Checklist items 3–8: No theoretical results claimed. Code/data are said to be in supplemental material/GitHub; not executed here. Checklist says temperature settings are reported, but no numerical temperature is supplied in the PDF’s experimental description. Solver/compiler versions, exact seeds, repeated-run counts and solver timeouts are not disclosed there. Checklist items 10–15: Broader impacts answer No because work targets compiler checks; existing UCLID5 license stated as 3-clause BSD, textbook examples cited, new code/documentation claimed public. Human-subject and IRB questions marked NA. These are disclosure statements, not independent license or artifact verification. Whole paper: No generated distributed protocol, Verus/verified Rust proof, TLA+ specification, termination argument, concurrency refinement proof or validated natural-language specification oracle is evaluated. Formal tools repair syntax/types; UCLID5’s verification capabilities do not by themselves make generated models faithful to the task.
  • how much was read: most of it read
  • record id: synthetic-programming-elicitation-for-2024
• TiCoder (2024)
  • title: LLM-Based Test-Driven Interactive Code Generation: User Study and Empirical Evaluation
  • what: Asks the user whether concrete tests are right, and uses the answers to refine and rank generated programs.
  • number: user study with 15 programmers
  • limits: The larger benchmark uses an idealized stand-in for user feedback. Answers taken from a gold solution say little about real stakeholder clarification.
  • how much was read: most of it read
  • source; notes: Clarification and stakeholder requirements
  • record id: ticoder-2024
• Toward Auto-Modeling of Formal Verification for NextG Protocols: A Multimodal Cross- and Self-Attention Large Language Model Approach (2024)
  • what: AVRE uses CAL, a pretrained GPT-2 combined with cross/self attention, to classify relationships between identifiers in protocol prose, assemble dependency graphs, and use HyFuzz experiments to refine uncertain or unintended dependencies. Defines six relationship labels (confidentiality, integrity, authentication, accounting, include, generate), describes label-balanced training, and compares CAL with GPT-2+LSTM and LSTM. RRCSetupRequest/SecurityModeCommand examples show experiment-filtered relations and a rejected KRRCenc–CipherAlgorithm integrity relationship. Nodes are manually extracted, and ProVerif conversion is described as following earlier work.
  • number: 16,428 samples; train/validation 9:1
  • number: CAL accuracy 95.94%; reported AUC 0.98
  • number: LLM+LSTM accuracy 66.76%; LSTM 50.21%
  • number: 12 GPT-2 layers; 100 epochs
  • limits: The downloaded IEEE PDF is the accepted author version: its repeating header carries the requested 2024 DOI, but the first-page template has a different placeholder 2023 DOI and 2023 volume labels. Evaluation measures relationship classification, not verified protocol correctness. Training/validation ratio is 9:1, with no clearly described held-out protocol test or repeated-trial uncertainty. Rare positive labels and scope confined to 3GPP RRC sections 5.3.1–5.3.5 limit generalization. The paper says 1,218 domain-expert samples but Table 2 positive counts sum to 205 across six labels; the relationship between these counts is not explained. Text claims 100% recall, while Table 4 displays only accuracy. Manual postverification is advised for extraneous predicted dependencies. No standalone ProVerif proof result or exploit success-rate evaluation is displayed in this source.
  • how much was read: most of it read
  • source
  • record id: toward-auto-modeling-of-2024
• TSL+LLM pipeline (2024)
  • title: Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesis
  • what: The paper splits generation between an LLM and correct-by-construction Temporal Stream Logic (TSL) synthesis. GPT-4 converts structured natural-language assumptions/guarantees into TSL; a reactive synthesizer generates the control structure; an LLM fills data/predicate functions and either wraps the synthesized code or uses it as prompt seed for a complete implementation. The authors evaluate five small reactive tasks (Ball, Game of Life, Vending Machine, Space Invaders, Rotating Cube), a scaling arbiter with 10/20/30 conditions, and Conway’s Game of Life prompt seeding. The TSL pipeline’s arbiter success is 61.5%, 45.4%, and 16.7% for 10, 20, and 30 conditions versus 0% for LLM-only; it uses 22, 31, and 40 average lines of verified synthesized code. Prompt seeding reaches 0.80 success on Game of Life at 15 trials versus GPT-4’s 0.40. Small tasks show mixed success and many unverified integration lines; failures include unsynthesizable TSL generated by few-shot prompting.
  • number: 5 small reactive tasks, 5/10/15-trial success rates
  • number: arbiter (10/20/30 conditions): TSL 61.5%/45.4%/16.7%, LLM-only 0%
  • number: arbiter synthesized verified lines: 22/31/40
  • number: Game of Life prompt-seeding success 0.80 vs GPT-4 0.40 at 15 tries
  • limits: The LLM must correctly express the natural-language requirements in TSL; an invalid or unsynthesizable specification is rejected. TSL separates temporal control from data/predicate implementation, but integration and function terms remain unverified LLM code. The study is small, uses GPT-4 few-shot prompting, and treats repeated trials/success as the metric; it does not establish correctness of natural-language interpretation or distributed-system safety. Authors state that the simple benchmarks do not always expose the pipeline’s benefit and that complex unknown TSL syntax causes weak performance.
  • how much was read: most of it read
  • source
  • record id: tsl-llm-pipeline-2024
• Lang2LTL (2023)
  • title: Grounding Complex Natural Language Commands for Temporal Tasks in Unseen Environments
  • what: It separates referring expressions and landmarks from the temporal formula, then reconnects them to the environment. Experiments are on robot navigation.
  • limits: Success at navigation does not show that software contracts in general are complete.
  • how much was read: most of it read
  • source; notes: Natural language to temporal logic and TLA+
  • record id: lang2ltl-2023
• nl2spec (2023)
  • title: nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models.
  • what: nl2spec uses an LLM to map pieces of English to pieces of a temporal formula. Users can edit the mappings and regenerate. It reports confidence as how much the votes agree.
  • number: 36 expert-written requirements; Codex 16/36 initially, Bloom 5/36
  • number: interactive correction fixed 15 of 20 failures within three loops, Codex 31/36
  • number: four sampled examples raised initial Codex to 21/36, but they stayed in the set
  • number: 36 benchmark instances
  • limits: An expert assists it. It is not autonomous. Correctness means what the submitting expert meant. The confidence is not a calibrated probability.
  • how much was read: most of it read
  • source; notes: Natural language to temporal logic and TLA+; notes: papers
  • record id: nl2spec-2023
• FRET realizability (2022)
  • title: Realizability Checking of Requirements in FRET
  • what: It checks whether requirements can be implemented, using Lustre and JKind/Kind2. It finds minimal unimplementable sets of requirements with delta debugging, and shows counterexample traces of the environment.
  • number: aircraft study: 11 requirements; removing the hover-initialization requirement made a conflicting requirement realizable
  • number: infusion pump: 12 requirements rewritten to 26 scoped ones, 8 minimal unrealizable cores
  • limits: This is a technical report, not the CAV 2022 version. Results depend on which variables the environment controls.
  • how much was read: most of it read
  • source
  • record id: fret-realizability-2022
• RFCNLP (2022)
  • title: Automated Attack Synthesis by Extracting Finite State Machines from Protocol Specification Documents
  • what: Extracts partial protocol state machines from RFCs with BERT/CRF. Translates them to Promela. Uses KORG/SPIN to synthesize attacks on safety and progress properties, checked against a canonical model.
  • number: six protocols extracted
  • number: TCP: 17 of 20 transitions correct or partly correct
  • number: automated TCP models find attacks on 1 property, canonical model on all 4
  • number: Six protocols extracted; TCP: 17 of 20 transitions correct or partly correct
  • limits: The attacks work against models, not deployed code. Experts write the canonical models and four LTL properties each. A progress property can pass vacuously (hold trivially, because the condition that should trigger it never occurs).
  • how much was read: most of it read
  • source; notes: RFCNLP: learned extraction followed by model-level attack synthesis; notes: RFCNLP: learned extraction followed by model-level attack synthesis
  • record id: rfcnlp-2022
• Verifiable Aircraft Engine Methodology (2021)
  • title: A Methodology for Developing a Verifiable Aircraft Engine Controller from Formal Requirements
  • what: Presents a three-phase, requirements-driven methodology for developing and verifying an aircraft engine controller: elicit and formalize requirements in FRET, verify through FRET-supported Simulink/Kind2 and FRET-guided formal models, then assemble a traceable verification report. The paper details the fretish intermediate language, FRET-generated LTL and CoCoSpec contracts, the parallel Phase 2A/2B toolchains, and feedback loops that revise requirements when verification exposes errors. The industrial use case translates 14 natural-language requirements and uses 20 supplied test cases to add detail; the authors explain how combining independent designs can expose inconsistencies.
  • number: 14 aircraft-engine requirements translated into fretish
  • number: 20 supplied test cases informed requirement elaboration
  • number: two parallel verification streams (FRET-supported and FRET-guided)
  • limits: The methodology is demonstrated on one industrial aircraft-engine-controller use case and remains ongoing work rather than a completed large-scale evaluation. Phase 2A checks are limited to properties expressible in fretish and Simulink/Kind2 tooling can lack scalability for complex requirements; Phase 2B model construction and translations may be manual. Requirement and design updates still require human work.
  • how much was read: most of it read
  • record id: verifiable-aircraft-engine-methodology-2021
• FRET (2020)
  • title: Formal Requirements Elicitation with FRET
  • what: FRET lets users write requirements in a restricted English called FRETish. Each requirement has scope, condition, component, timing and response fields. FRET turns them into temporal formulas, explanations and diagrams. It also has a simulator for trying out signals.
  • number: industrial autopilot case; no large quantified benchmark
  • limits: The translation is checked against the language’s own semantics, not against what the customer meant. Mapping variables to the model is a separate source of error. New users need help with subtle points of meaning.
  • how much was read: most of it read
  • source
  • record id: fret-2020
• Bayesian temporal specification inference (2018)
  • title: Bayesian Inference of Temporal Task Specifications from Demonstrations
  • what: Learns posterior distributions over a restricted LTL-template family from positive, state-only demonstrations. Known proposition labels and three graph priors reduce inference to global, eventual and precedence clause subsets. Synthetic navigation and 71 dinner-table demonstrations test clause-set similarity and top-five recovery. Printed Until semantics and epsilon/likelihood definitions contain unresolved problems confirmed in the PDF.
  • limits: Known propositions, labeling functions, task/condition mappings; independent acceptable demonstrations; restricted conjunction/graph templates; approximate MCMC; domain-independent likelihood is explicitly a proxy. The printed epsilon expression lacks a closing cardinality bar; under reader normalization to |τ| it exceeds1 for the evaluated nontrivial task sets and contradicts probability Eq.8; Eq. 7 assumes a satisfying numerator candidate without an explicit case. Until includes its endpoint and strictly future witness, unlike ordinary strong Until. These unresolved printed definitions limit independent interpretation/reproducibility; no author code was inspected to repair them. Similarity is clause Jaccard, not a proof of semantic equivalence/generalization.
  • how much was read: most of it read
  • record id: bayesian-temporal-specification-inference-2018
• Specification inference from demonstrations (2018)
  • title: Learning Task Specifications from Demonstrations
  • what: Formulates learning a temporal Boolean task specification from finite demonstrations as maximum-a-posteriori inference over a candidate concept class. A maximum-entropy likelihood depends on the teacher’s task-satisfaction rate and the probability that uniformly random actions satisfy the candidate; the posterior is proportional to an indicator that the demonstrator is at least as good as random times a Bernoulli KL information gain. For concept classes represented as chains/lattices, monotonicity enables binary-search or breadth-first algorithms that minimize expensive random-satisfaction queries. In a gridworld, the method learns a missing wet/recharge constraint and composes it safely with an existing recharge-and-avoid-lava specification.
  • limits: Demonstrations are modeled as i.i.d. fixed-length traces from a teacher in a finite probabilistic automaton; candidate specifications form a finite concept class with known subset relations (chain or bounded lattice). The posterior assumes the demonstrator is at least as good as random and uses empirical satisfaction N_phi/|X|. Computing random satisfaction is generally #P-complete, so Monte Carlo/BDD or SAT approximations are needed. The experiment uses discrete gridworlds and finite-horizon traces; future work explicitly lists infinite-horizon specifications and continuous dynamics. The paper notes Boolean specifications cannot directly encode every objective (for example ‘run as fast as possible’).
  • how much was read: most of it read
  • source
  • record id: specification-inference-from-demonstrations-2018
• Maximal Specification Synthesis (2016)
  • what: Given an incomplete program and a desired postcondition, this work derives the most permissive assumptions about unknown callees that still prove the client’s property. It solves by trying candidates and refining them from counterexamples.
  • number: six Windows-driver variants; 6-7 procedures; 1 to 184 seconds for initialization constraints
  • limits: It covers the safety of an imperative model. It does not prove that real libraries meet the assumptions. It is not an LLM system. Drivers abstract the heap.
  • how much was read: most of it read
  • source; notes: Maximal Specification Synthesis
  • record id: maximal-specification-synthesis-2016
• Looney (2015)
  • title: Analysing Sanity of Requirements for Avionics Systems
  • what: Checks a set of temporal-logic requirements before any model exists: finds every smallest group of requirements that contradict each other, finds requirements implied by others, and suggests new requirements to cover behavior the set leaves open. Tested on random formulas, a plane-landing example, and four Honeywell avionics models.
  • number: Honeywell sets of 3, 5, 10 and 10 formulas: all consistent; two redundancies found; consistency took 0.1 s, 0.1 s, 73.6 s and 210879 s for the largest (pbit)
  • number: Landing example: R4 vs R6 and R1, R2, R5 were inconsistent; A5 and A6 were redundant; coverage rose 0% to 9.1%, 39.4%, 54.9% with 3 suggested formulas
  • number: Switching to the SPOT translator sped up checking by several orders of magnitude on larger sets
  • number: Honeywell engineers: tool-supported formalization took under 5 minutes per requirement after a week; requirement-elicitation stages took 18 per cent less time
  • limits: Needs requirements already written in LTL (Honeywell used a pattern tool, ForReq, from English). Largest industrial set was 10 formulas, which the authors call hardly a demonstration of industrial scale. Completeness needs a human to separate assumptions, required and forbidden behavior, and was not tested on Honeywell data. Honeywell requirements are confidential.
  • how much was read: most of it read
  • source; notes: Analysing Sanity of Requirements for Avionics Systems (2015)
  • record id: looney-2015
• PROPEL (2002)
  • title: PROPEL: An Approach Supporting Property Elucidation
  • what: Presents property patterns both as disciplined natural language and as finite-state automata. It shows the person writing the property the alternative meanings (repeats, response, scope boundaries).
  • limits: The notes read the author’s technical report, not the typeset proceedings.
  • how much was read: most of it read
  • source; notes: Requirements methods predating LLMs
  • record id: propel-2002
• Goal-Oriented Requirements Engineering: A Guided Tour (2001)
  • what: The paper breaks goals into smaller obligations assigned to software or environment actors. Obstacles and conflicts help find missing requirements. A spec is complete with respect to a set of goals when the goals follow from the spec plus domain properties.
  • how much was read: most of it read
  • source; notes: Requirements methods predating LLMs
  • record id: goal-oriented-requirements-engineering-2001
• Property Specification Patterns (1998)
  • title: Property Specification Patterns for Finite-State Verification
  • what: The paper gives reusable patterns and scopes for properties, such as absence, response and precedence. It maps them to formal languages.
  • limits: A pattern cannot tell the agent which guarantee the human left out. Users must still know enough to express the requirement.
  • how much was read: most of it read
  • source; notes: Requirements methods predating LLMs; notes: papers
  • record id: property-specification-patterns-1998
• Four Dark Corners of Requirements Engineering (1997)
  • what: The paper separates three things: facts about the environment that are wanted, facts about it that are assumed, and behavior the machine can enforce at its interface. The spec plus domain knowledge must imply the requirements.
  • how much was read: most of it read
  • source; notes: Requirements methods predating LLMs
  • record id: four-dark-corners-of-1997
• Beyond Compilation (2026)
  • what: A study of turning math into Lean statements automatically. It shows that Lean accepting a statement does not mean the statement says what the user meant.
  • number: Tool-augmented GPT-5.2 agent compiles 87.2% of statements but is faithful on 57.7% (29.5 point gap)
  • limits: About mathematics, not systems.
  • how much was read: parts read
  • source
  • record id: beyond-compilation-2026
• ClarifyCodeBench (2026)
  • what: Measures how well code models ask for clarification of requirements, using the metrics TKQR and ORA.
  • how much was read: parts read
  • source
  • record id: clarifycodebench-2026
• COINS (2026)
  • title: How Powerful Are LLMs in Generating Formal Program Specifications? (COINS)
  • what: It instantiates a spec on trusted tests to produce concrete proof obligations in Rocq. These serve as an oracle (a reference check) for whether the spec is correct.
  • number: All 164 HumanEval ground-truth specs hand-written over several person-weeks
  • number: Top 28.05% (Gemini 3 Pro Preview) down to 1.22% (DeepSeek-V3.1)
  • number: 164 HumanEval problems
  • limits: Failing to find a proof that a test is accepted is weaker evidence than proving that it is rejected. The LLM judge can skip the formal proof. It does not cover distributed liveness.
  • how much was read: parts read
  • source; notes: How Powerful Are LLMs in Generating Formal Program Specifications?
  • record id: coins-2026
• LeetProof (2026)
  • title: LeetProof: Certified Program Synthesis with a Multi-modal Verifier
  • what: LeetProof synthesizes programs together with proofs that they are correct. The notes audit how it checks its specs. The checks are generated examples, an LLM judge, randomized checks of preconditions and postconditions, mutations that produce incorrect outputs, a Lean proof of equivalence to VERINA, and manual judgment.
  • limits: The earlier note found that development and evaluation statistics were pooled. It also found that unresolved specs were classified without blinding, and that the synthesis subjects had no independent labels.
  • how much was read: parts read
  • source; notes: LeetProof: examples and equivalence provide complementary intent evide
  • record id: leetproof-2026-2
• LiveFMBench (2026)
  • title: LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation
  • what: 630 C programs annotated with ACSL (360 collected in 2025 to avoid training leaks), verified with Frama-C/WP. Models generate loop invariants and assertions. A faithfulness check requires that the ASTs are equal and that every original assertion appears in the output.
  • number: true accuracy drops about 20% after excluding unfaithful cases
  • number: pass@5 doubles pass@1; pass@32 triples it
  • number: incorrect loop invariants are the dominant error type
  • number: After removing unfaithful behaviors true accuracy drops about 20%
  • limits: One notes file says the full claims await deeper reading. Another read the faithfulness section.
  • how much was read: parts read
  • source
  • record id: livefmbench-2026
• SWE-Proof (2026)
  • title: SWE-Proof / BenchProofer
  • what: Takes SWE-bench Verified issues, given as natural language plus a repository, with Nagini, Velvet and Lean backends. Three adversarial LLM auditors check the specs that agents write. It is the only benchmark the review notes found that starts from a vague task in a real repository.
  • number: 500 instances
  • number: A correct formal spec lifts resolution from 85% to 95%; only 56% of agent-written specs pass the audit
  • number: Specs from unresolved instances fail audit 92% of the time vs 51% for resolved
  • number: 26.8% of test-passing patches overturned by the audit; Lean faithfulness failure 37.2%
  • how much was read: parts read
  • record id: swe-proof-2026
• Veil blog (Sergey) (2026)
  • title: Verifying Distributed Protocols in Veil
  • what: Reports Claude Code finding agreement and validity invariants for FloodSet, using feedback from the checker. The faulty model lumped all crashes together with the broadcast and left out partial delivery, which made agreement hold trivially.
  • limits: A case study by a single author, not a comparative score.
  • how much was read: parts read
  • source; notes: papers inspected; notes: Veil: proofs in Lean with automatic first-order checks
  • record id: veil-blog-sergey-2026
• Beyond Code Generation: Assessing Code LLM Maturity with Postconditions (2024)
  • what: It extends the EvalPlus benchmark with several kinds of postcondition (what must hold after a function runs): boundary, equality, container, Boolean and string. It checks that the assertions are correct and which buggy programs they catch.
  • limits: It evaluates algorithms with a finite set of tests. It does not cover proofs or progress in distributed systems.
  • how much was read: parts read
  • source; notes: Natural-language postconditions and known faulty implementations
  • record id: beyond-code-generation-assessing-2024
• 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
• Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal Logic. (2024)
  • what: The study examines how people read and write linear temporal logic, across five deployments.
  • number: Writing a formula wrong: 21.11-25.00% (alpha), 33.68% (LTL-aware audience), 66.13% and 63.33% (student course)
  • number: Trace matching wrong: 1.85% to 27.24%
  • limits: The notes are unsure about the authors after the first. Percentages across different instruments cannot be compared.
  • how much was read: parts read
  • source
  • record id: misconceptions-in-finite-trace-2024
• Towards a Notion of Unsatisfiable and Unrealizable Cores for LTL (2012)
  • what: The paper defines cores. A core isolates the part of a requirement set that is unsatisfiable or unrealizable (no implementation could meet it). The paper defines cores at several granularities, from whole requirements to proof structures. It also discusses vacuity (a requirement that passes for no real reason).
  • number: lift example: 6 of 49 conjuncts isolate an inconsistency (§8.1)
  • limits: A core explains a failure, but not necessarily every failure. It does not tell which restrictions on the environment the customer intended. The normal-form proofs were not checked.
  • how much was read: parts read
  • source
  • record id: towards-a-notion-of-2012
• Property Specification Patterns (1999)
  • title: Patterns in Property Specifications for Finite-state Verification
  • what: This is a catalog of reusable requirement patterns, about what occurs and in what order. It also lists scopes: global, before, after, between, and after-until. Each pattern is mapped to formal languages for describing behavior over time. The authors also surveyed real specifications.
  • limits: The notes read the authors’ pattern repository, not the ICSE PDF. The repository labels a formula about all branching futures (AG/AF) as LTL.
  • how much was read: parts read
  • source
  • record id: property-specification-patterns-1999
• quint-llm-kit
  • what: Supplies workflows for agents that write specs and code. The Quint LLM-era post links spec generation, implementation generation and feedback from models.
  • limits: No theorem was found that the generated Rust refines Quint (matches it as an abstract model).
  • how much was read: parts read
  • source; notes: R06. Quint Connect, Choreo, and LLM-driven implementation; notes: Quint: production case studies, not a measured proof benchmark
  • record id: quint-llm-kit
• Ambig-SWE (2026)
  • title: Interactive Agents to Overcome Underspecificity in Software Engineering
  • what: Measures the clarifying-question step for coding agents with an LLM-simulated user holding the missing facts.
  • number: Interactivity boosts performance up to 74%
  • number: Claude Sonnet 4 recovers 89% of full-information performance with interaction
  • limits: It covers coding, not specs.
  • how much was read: only abstract or first pages read
  • source
  • record id: ambig-swe-2026
• Automated Trace Link Recovery Between Natural Language Requirements and Formal Specifications via LLMs (2026)
  • what: LLMs link each item in a structured English requirements document to the matching part of an existing formal specification. The paper compared GPT-4o, Gemini 3.1 Pro and DeepSeek V3 with retrieval baselines on four projects, including an ATM and the avionics system Sun Search.
  • number: four projects
  • limits: The review notes read only the abstract, which is behind a subscription. It gives no precision, recall or timings. The links help an audit but do not show the two texts mean the same thing.
  • how much was read: only abstract or first pages read
  • source; notes: Automated Trace Link Recovery Between Natural Language Requirements an
  • record id: automated-trace-link-recovery-2026
• Beyond Type-checking: Towards Holistic Evaluation of Formal Specification Generation (2026)
  • what: The paper evaluates Lean specs written by LLMs, using more than type-checking. It measures whether the spec is well-formed, whether it is similar or equivalent to a reference spec, and whether it describes the intended behavior.
  • number: 350 Lean tasks (189 VERINA, 161 CLEVER)
  • number: LeanAide returns only 135 of 161 candidates on CLEVER, though every returned one typechecks
  • limits: The notes did not record the authors.
  • how much was read: only abstract or first pages read
  • source
  • record id: beyond-type-checking-towards-2026
• claimcheck (2026)
  • title: claimcheck: Narrowing the Gap between Proof and Intent
  • what: One model describes a Dafny lemma in English without seeing the requirement. A second model compares that description to the requirement and labels the pair confirmed or disputed.
  • number: Own benchmark: 36 pairs, 5 domains, 8 bogus lemmas; two-pass 96.3%, single prompt 86.1%, Claude Code default 69.4%
  • number: 36 requirement/lemma pairs, 8 deliberately bad, 3 runs: 108 comparisons
  • number: 96.3% accuracy across 108 comparisons; other modes 86.1% and 69.4%
  • number: About 108 s per run vs 353 s single prompt, 693 s via Claude Code prompt
  • limits: It is small and self-made. The post calls it a probabilistic sanity check.
  • how much was read: only abstract or first pages read
  • source; notes: claimcheck: check whether the proven claim is what the user asked for
  • record id: claimcheck-2026
• Comet-H (2026)
  • title: Theory Under Construction: Orchestrating Language Models for Research Software Where the Specification Evolves
  • what: It proposes a prompt automaton that repeatedly grounds code, benchmarks and papers in each other. The goal is to counter the buildup of hallucinations and the drift between code and theory when a spec keeps changing.
  • limits: It addresses spec drift. It does not address refinement or liveness.
  • how much was read: only abstract or first pages read
  • source
  • record id: comet-h-2026
• Faithful Autoformalization via Roundtrip Verification and Repair (2026)
  • what: Formalize a sentence, translate the formula back to English, formalize that again, then use an SMT solver to check that the two formulas are equivalent. If they differ, repair the stage that diverged.
  • number: Rules failing the check show 1.4x-2.5x more natural language inference drift
  • number: 150 Texas Transportation Code rules and 77 Parks and Wildlife rules; Claude Opus 4.6 and GPT-5.2
  • limits: It uses first-order logic on legal rules. A second signal, natural-language inference, judged the results, not people.
  • how much was read: only abstract or first pages read
  • source
  • record id: faithful-autoformalization-via-roundtrip-2026
• Fidelity Probes (2026)
  • title: Fidelity Probes for Specification-Code Alignment
  • what: Probes pair behavioral questions with reference answers derived from the code. An LLM answers from the spec alone. Its answers are compared with the code’s answers, and the requirements are revised.
  • number: CardDemo held-out fidelity rises from 0.59 to 0.89
  • limits: Repairs can cause regressions. It measures agreement with the behavior of existing code. It is not a proof, and it does not cover liveness over time.
  • how much was read: only abstract or first pages read
  • source
  • record id: fidelity-probes-2026
• Isolde (2026)
  • what: Isolde is a SAT tool, with no LLM. It produces examples that one isolation level allows and another does not. It also checks whether two definitions are equal.
  • limits: The notes have only a summary.
  • how much was read: only abstract or first pages read
  • source
  • record id: isolde-2026
• Monty (2026)
  • title: Faithful Autoformalization of Natural Language Assertions
  • what: Monty keeps formalizations whose clause-by-clause back-translation scores above a threshold. It tests them against code. Then it asks the user to pick among the candidates.
  • number: Precision from 75% to 91.6% on one dataset and 64% to 85% on another
  • number: 541 tasks from 22 Java classes
  • limits: The experiments use a simulated user who holds the ground truth. A round trip through translation is not always a reliable stand-in for correctness.
  • how much was read: only abstract or first pages read
  • source
  • record id: monty-2026
• Spec-Agent (2026)
  • title: Agentic Separation Logic Specification Synthesis
  • what: Synthesizes specs for open-source C++. It picks a spec language from a ladder, from propositional logic up to first-order separation logic. It turns tests into fuzz harnesses. It refines the specs using counterexample feedback.
  • number: valid specifications for 85% of target functions
  • limits: Produces specs, not proofs. A spec counts as ‘valid’ based on fuzzing and expert review. Abstract only.
  • how much was read: only abstract or first pages read
  • source
  • record id: spec-agent-2026
• SPECA (2026)
  • title: Beyond Code Reasoning: Specification-Anchored Auditing of Multi-Implementation Distributed Protocols
  • what: SPECA has an LLM read protocol specs (Ethereum consensus) and write categorized properties. It then audits each client against them. These are not proofs.
  • number: 15/15 in-scope Fusaka vulnerabilities with expert augmentation, 8/15 automated
  • number: About $30perhigh/medium/lowbug-limits:Theauthorssaythequalityofthegeneratedpropertiesisthemainlimit.-howmuchwasread:onlyabstractorfirstpagesread-[source](https://arxiv.org/abs/2604.26495);[notes:specification-anchoredauditing](../distribute{d}_{v}erificatio{n}_{p}rimar{y}_{e}xtensio{n}_{2}0261012.md)-recordid:‘speca-2026‘-SpecificationsforHumans,Agents,andTooling(2026)-what:DescribestheBosqueAPIecosystemforagent-drivendevelopment.Ithaspolyglotspecs,testgeneration,validationandsandboxing.Specsaresharedartifactsforpeople,agentsandtools.-limits:Apositionontooling.Norefinementtheoremandnoevaluationonadistributedprotocol.Notevidencethatintentcanberecoveredautomatically.-howmuchwasread:onlyabstractorfirstpagesread-[source](https://arxiv.org/abs/2606.15084)-recordid:‘specifications-for-humans-agents-2026‘-FLAG(2025)-title:FLAG:FormalandLLM-assistedSVAGenerationforFormalSpecificationsofOn-ChipCommunicationProtocols-what:Ittakesunstructuredprotocoldocumentstocheckedproperties.Itgeneratescandidatepropertiesfromagrammar,filtersthemwithtimingdiagramsandchecksthemformally.-limits:Itcoversaconstraineddomain:hardwareprotocols.-howmuchwasread:onlyabstractorfirstpagesread-[source](https://arxiv.org/abs/2504.17226);[notes:FLAG](../distribute{d}_{v}erificatio{n}_{p}rimar{y}_{e}xtensio{n}_{2}0261012.md)-recordid:‘flag-2025‘-TransformingNaturalLanguageRequirementstoFormalismUsingLLMs(2025)-what:GEAerospaceResearchbuiltanLLMtoolthatinteractivelyturnsplain-Englishrequirementsintologicalformulas,withanEnglish-languageinterfacemeanttoletnon-expertsconfirmthetranslationisright.Itwastriedonanindustrylanding-gearcase.-limits:Fulltextnotobtained(Wileypaywallbehindabotcheck;Unpaywalllistsnoopencopy),sonumbers,formalismused,andevaluationmethodareunknown;onlytheabstractwasread.-howmuchwasread:onlyabstractorfirstpagesread-[source](https://doi.org/10.1002/sys.70023);[notes:LLMtranslationofnatural-languagerequirementstoformalism(2025)](claud{e}_{r}eadings.md)-recordid:‘transforming-natural-language-requirements-2025‘-Specifications:TheMissingLinktoMakingtheDevelopmentofLLMSystemsanEngineeringDiscipline(2024)-what:ThispositionpaperarguesthatexplicitspecificationsarethemissingengineeringlayerforLLMsystems.-limits:Thepagesthereviewnotesinspectedshownoformalverificationartifactorproofresult.-howmuchwasread:onlyabstractorfirstpagesread-[source](https://arxiv.org/abs/2412.05299)-recordid:‘specifications-the-missing-link-2024‘-AcompositionalproofframeworkforFRETishrequirements.-what:ACMReferenceFormat:StructurednaturallanguagesprovideatradespacebetweenEstherConrad,LauraTitolo,DimitraGiannakopoulou,ThomasPressburger,andAaronDutle.2022.ACompositionalProofFrame-ambiguousnaturallanguagesthatmakeupmostwrittenworkforFRETishRequirements.-howmuchwasread:onlyabstractorfirstpagesread-[source](https://doi.org/10.1145/3497775.3503685)-recordid:‘a-compositional-proof-framework‘-AccessibleSmartContractsVerification:SynthesizingFormalModelswithTamedLLMs-what:Whenblockchainsystemsaresaidtobetrustless,whatthisreallymeansisthatallthetrustisputintosoftware.Thus,therearestrongincentivestoensureblockchainsoftwareiscorrect—vulnerabilitiesherecostmillionsandbreakbusinesses.Oneofthemostpowerfulwaysofestablishingsoftwarecorrectnessisbyusingformalmethods.-howmuchwasread:onlyabstractorfirstpagesread-[source](https://doi.org/10.1109/icst\mathrm{62969.2025.10989026})-recordid:‘accessible-smart-contracts-verification‘-AGVTS:AutomatedGenerationandVerificationofTemporalSpecificationsforAeronauticsSCADEModels-what:.SCADEisbothaformallanguageandamodel-baseddevel-opmentenvironment,widelyusedtobuildandverifythemodelsofsafety-criticalsystem(SCS).TheSCADEDesignVerifier(DV)providesSAT-basedverification.-howmuchwasread:onlyabstractorfirstpagesread-[source](https://doi.org/10.1007/978-3-031-71177-0_{2}1)-recordid:‘agvts-automated-generation-and‘-AssertLLM:GeneratingHardwareVerificationAssertionsfromDesignSpecificationsviaMulti-LLMs-what:Table1:ExistingworksongeneratingSVAsfromnaturallanguagespecifications.AssertLLMisthefirstworkthatcanAssertion-basedverification(ABV)isacriticalmethodtoensurearXiv:2411.14436v1[cs.AR]4Nov2024handlefull-sizespecificationfilesandgeneratecomprehen-logicdesignscomplywiththeirarchitecturalspecifications.ABVsivetypesofSVAsforeacharchitecturalsignal.-limits:Abstract-levelreadingfromopenlyavailablePDF;detailedlimitationsrequirefullpaperreview.-howmuchwasread:onlyabstractorfirstpagesread-[source](https://doi.org/10.1145/3658617.3697756)-recordid:‘assertllm-generating-hardware-verification‘-AutomatingCryptographicProtocolLanguageGenerationfromStructuredSpecifications.-what:latterisamanualrefinementfromthespecificationlanguage,thatisSecurityofcryptographicprotocolscanbeanalysedbycreatingoftenamixofmathsandnaturallanguage,toaformallanguageofarXiv:2105.09150v2[cs.CR]5Apr2022amodelinaformallanguageandverifyingthemodelinatool.choice,withlimitedsemantics,thatconsequentlymayonlycaptureAllsuchtoolsfocusonthelastpartoftheanalysis,verification,asubsetoftheinitialspecification.andtheinterpretationofthespecificationisonlyexplainedinThemodelinterpretingthedesignofaprotocolisthefirstmath-papers.-howmuchwasread:onlyabstractorfirstpagesread-[source](https://doi.org/10.1145/3524482.3527654)-recordid:‘automating-cryptographic-protocol-language‘-AutoSVA:DemocratizingFormalVerificationofRTLModuleInteractions-what:ToAppearinProceedingsofthe58thACM/IEEEDesignAutomationConference(DAC’21)AutoSVA:DemocratizingFormalVerificationofRTLModuleInteractionsMarceloOrenes-Vera,AnindaManocha,DavidWentzlaffandMargaretMartonosiDepartmentofComputerScienceandElectricalEngineering,PrincetonUniversityPrinceton,NewJersey,USAEmail:movera,amanocha,wentzlaf,mrm@princeton.eduAbstract—ModernSoCdesignreliesontheabilitytoseparatelyArianeCoreOpenPitonTileverifyIPblocksrelativetotheirownspecifications.FormalLSUL1-I$ Issue lsu_load L2$NoCL1.5$ arXiv:2104.04003v1 [cs.AR] 8 Apr 2021 verification (FV) using SystemVerilog Assertions (SVA) is an stage L1-D$ slice effective method to exhaustively verify blocks at unit-level. Unfor- lsu_store MMU tunately, FV has a steep learning curve and requires engineering effort that discourages hardware designers from usin
  • how much was read: only abstract or first pages read
  • source
  • record id: autosva-democratizing-formal-verification
• 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
• 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
• Counter-strategy guided refinement of GR(1) temporal logic specifications
  • what: Counter-Strategy Guided Refinement of GR(1) Temporal Logic Specifications Rajeev Alur, Salar Moarref, and Ufuk Topcu University of Pennsylvania, Philadelphia, USA. {alur,moarref,utopcu}@seas.upenn.edu Abstract—The reactive synthesis problem is to find a finite- to give the user insight into the specification. They also state controller that satisfies a given temporal-logic specification provide ways to correct the specification.
  • how much was read: only abstract or first pages read
  • source
  • record id: counter-strategy-guided-refinement
• Creating Formal Models from Informal Design Artefacts
  • what: The use of robust software engineering processes is essential in the design and devel- opment of interactive systems. This ensures that software is both functionally correct and also usable in the required context. There are a variety of software engineering techniques that can be used to consider different aspects of a system under construc- tion, and at different stages in the development process.
  • how much was read: only abstract or first pages read
  • source
  • record id: creating-formal-models-from
• 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
• 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
• LEGOS-SLEEC: Tool for Formalizing and Analyzing Normative Requirements.
  • what: —Systems interacting with humans, such as assistive engineers [2]–[5]. For instance, the requirement Ra is ex- robots or chatbots, are increasingly integrated into our society. pressed in SLEEC DSL rule r2 in Tbl.
  • how much was read: only abstract or first pages read
  • source
  • record id: legos-sleec-tool-for
• Low-Effort Specification Debugging and Analysis
  • what: Low-Effort Specification Debugging and Analysis Rüdiger Ehlers Vasumathi Raman University of Bremen & DFKI GmbH California Institute of Technology Bremen, Germany Pasadena, CA, United States Reactive synthesis deals with the automated construction of implementations of reactive systems from their specifications. To make the approach feasible in practice, systems engineers need effec- tive and efficient means of debugging these specifications. In this paper, we provide techniques for report-based specification debugging, wherein salient properties of a specification are analyzed, and the result presented to the user in the form of a report.
  • how much was read: only abstract or first pages read
  • source
  • record id: low-effort-specification-debugging
• 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
• RATSY – A New Requirements Analysis Tool with Synthesis
  • what: . Formal specifications play an increasingly important role in system design-flows. Yet, they are not always easy to deal with.
  • how much was read: only abstract or first pages read
  • source
  • record id: ratsy-a-new-requirements
• 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
• The Challenges in Specifying and Explaining Synthesized Implementations of Reactive Systems
  • what: The Challenges in Specifying and Explaining Synthesized Implementations of Reactive Systems∗ Hadas Kress-Gazit Hazem Torfah† Sibley School of Mechanical and Aerospace Engineering Reactive Systems Group Cornell University, Ithaca, NY, USA Saarland University, Saarbrücken, Germany hadaskg@cornell.edu torfah@react.uni-saarland.de In formal synthesis of reactive systems an implementation of a system is automatically constructed from its formal specification. The great advantage of synthesis is that the resulting implementation is correct by construction; therefore there is no need for manual programming and tedious debugging tasks. Developers remain, nevertheless, hesitant to using automatic synthesis tools and still favor manually writing code.
  • how much was read: only abstract or first pages read
  • source
  • record id: the-challenges-in-specifying
• 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
• Uncertainty-Aware Signal Temporal Logic Inference
  • what: 1 Uncertainty-Aware Signal Temporal Logic Inference Nasim Baharisangari, Jean-Raphaël Gaglione, Daniel Neider, Ufuk Topcu, Zhe Xu Abstract—Temporal logic inference is the process of extracting such STL formulas is incorporating satisfibilty modulo the- formal descriptions of system behaviors from data in the form ories (SMT) solvers such as Z3 theorem prover [15]. Such of temporal logic formulas. The existing temporal logic inference solvers can determine whether an STL formula is satisfiable methods mostly neglect uncertainties in the data, which results in or not, according to some theories such as arithmetic theory limited applicability of such methods in real-world deployments.
  • how much was read: only abstract or first pages read
  • source
  • record id: uncertainty-aware-signal-temporal
• Validation Obligations: A Novel Approach to Check Compliance between Requirements and their Formal Specification.
  • what: Validation Obligations: A Novel Approach to Check Compliance between Requirements and their Formal Specification 1st Atif Mashkoor 2nd Michael Leuschel 3rd Alexander Egyed Johannes Kepler University Heinrich Heine University Johannes Kepler University Linz, Austria Düsseldorf, Germany Linz, Austria atif.mashkoor@jku.at leuschel@hhu.de alexander.egyed@jku.at arXiv:2102.06037v1 [cs.SE] 11 Feb 2021 Abstract—Traditionally, practitioners use formal methods pre- quality-assurance procedure. While the verification of a for- dominately for one half of the quality-assurance process: verifica- mal specification emphasizes on proving its internal consis- tion (do we build the software right?). The other half – validation tency, validation addresses another important question entirely: (do we build the right software?) – has been given comparatively little attention.
  • how much was read: only abstract or first pages read
  • source
  • record id: validation-obligations-a-novel
• 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
• 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
• 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
• 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
• Investigating the Role of Formal Verification in Software Development: From Automatic Specification Generation to Usability of Verification Languages (2025)
  • what: Per the input list and a search summary of its abstract: a 4-page doctoral plan studying how formal annotations affect code comprehension, how LLMs generate formal specs from code comments, and how usable two verification tools are.
  • limits: Full text not read: the ACM PDF returned HTTP 403 to automated download (bot protection, not worked around) and no open copy was found. Which tools and what results are unknown.
  • how much was read: not read; title and metadata only
  • source; notes: ## Role of formal verification in software development, doctoral paper
  • record id: investigating-the-role-of-2025
• HumanEvalComm (2024)
  • what: A benchmark with communication metrics that measure whether models ask clarifying questions.
  • limits: The review notes saw it only as a search snippet.
  • how much was read: not read; title and metadata only
  • source
  • record id: humanevalcomm-2024
• Consistency Checking in Requirements Analysis (title the input gave: Online enumeration of minimal inconsistent subsets of temporal requirements) (2017)
  • what: A doctoral-symposium proposal: a framework to list every minimal inconsistent subset (a smallest group of requirements that cannot all hold together) of requirements written in temporal logic such as LTL, one at a time.
  • limits: Full text not obtained: the ACM page returned no PDF and no open copy was found (the arXiv paper 1708.00400 is a different, later paper). Only the title and abstract-level description from a web search were seen; record is metadata only. Input file title does not match what the DOI resolves to.
  • how much was read: not read; title and metadata only
  • source; notes: ## Online enumeration of minimal inconsistent subsets of temporal requ
  • record id: consistency-checking-in-requirements-2017
• 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

Last edited: 2026-10-31