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

(authored by agents unless marked 🧑)

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

AeroReq2LTL (2026)
- title: Automated LTL Specification Generation from Industrial Aerospace Requirements
- what: Before translating requirements to LTL (a logic for statements about sequences of events), it adds a domain data dictionary and controlled requirement templates. It compares the results to formalizations written by experts for aerospace requirements.
- number: 85% precision and 88% recall
- limits: It covers one industrial domain, and its authors overlap with those of Req2LTL. It is not shown to work for the intent of distributed services.
- how much was read: most of it read
- source; notes: Natural language to temporal logic and TLA+
- record id: aeroreq2ltl-2026
Agentic Proving for Program Verification (Claude Code on CLEVER, Lean 4) (2026)
- what: Runs Claude Opus 4.6 in Claude Code, with Lean tools, on the 161 CLEVER algorithm tasks. The agent writes formal specifications, implementations and Lean proofs. People manually review whether each specification matches the English task.
- number: 159/161 tasks get an arguably valid specification (98.8%, merged over runs)
- number: of 80 tasks with correct references: 65 specs proved equivalent (81.3%), 70 implementations certified (87.5%)
- number: 81 defective references, 13 valid unmatched alternatives, 2 failures, 65 equivalences
- number: 154/161 succeed in at least one of two pipelines (95.7%); 154/157 after excluding 4
- limits: Only proofs that Lean programs compute the right results. No proofs about distributed progress. The 98.1% headline number merges two runs. The authors review the reference-error count themselves. Human effort is not measured.
- how much was read: most of it read
- source; notes: Agentic Proving for Program Verification; notes: Agentic Proving for Program Verification; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_agents.md
- record id: agentic-proving-for-program-2026
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 outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_intent.md; 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
- notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_google.md
- 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; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_intent.md
- record id: autospec-protocol-2026
Beyond Basic Specifications? A Systematic Study of Logical Constructs in LLM-based Specification Generation (2026)
- 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 ; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_intent.md
- record id: beyond-basic-specifications-a-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?; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_gaps.md
- record id: can-code-specify-a-2026
Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation (2026)
- what: It evaluates how well LLMs generate TLA+ from comments in community examples. It uses syntax checks and TLC model-checker runs on a corpus of 205 specifications.
- 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: A passing TLC run only checks the configuration it was given. Zero scores include infrastructure failures. Each pair is run once per strategy. The notes find a contradiction inside the paper’s discussion of model size.
- how much was read: most of it read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_agents.md; notes: Natural language to temporal logic and TLA+; notes: Two further TLA+ evaluation papers already in collection
- record id: can-llms-write-correct-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 outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_eval.md; 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
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
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
FM-Agent (2026)
- title: FM-Agent: Scaling Formal Methods to Large Systems via LLM-Based Hoare-Style Reasoning
- what: An agent writes function contracts in natural language from callers, code and domain knowledge. It reasons about blocks and loops in Hoare style (what holds before and after each piece of code). It then generates and runs system-level tests to confirm suspected bugs.
- number: 277k source lines and 8,549 functions across four systems; 522 new bugs total
- number: Claude’s C Compiler 339 bugs (143k lines), VibeTensor 141, VibeOS 23, Bespoke OLAP 19
- number: cost 2 days and 3.4 billion tokens total
- number: ablation on compiler: 57 bugs vs 339, removing two components at once
- limits: It handles sequential functions only. It cannot ensure soundness, and its reasoning is not machine-checked. The prose says 4,910 functions but the table says 4,957.
- how much was read: most of it read
- source; notes: FM-Agent: useful bug finding, without sound proofs; notes: FM-Agent: useful bug finding, without sound proofs; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_agents.md
- record id: fm-agent-2026
Intent Formalization (2026)
- title: Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents
- what: This research agenda argues that only the user can judge whether a spec is correct. It calls for support from tests, mutation, interaction and rich logic.
- number: TiCoder study with 15 professional developers: correct evaluation of AI code from 40% to 84%; cognitive load dropped (p = 0.007)
- limits: It is not a controlled benchmark.
- how much was read: most of it read
- source; notes: Intent formalization: why one number is insufficient; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_intent.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_shortlist.md
- record id: intent-formalization-2026
JS-SAM (2026)
- title: Executable JavaScript as a Checkable Specification Language: A JS-SAM Case Study on SysMoBench
- what: This controlled study compares LLMs writing JavaScript (SAM) specs against TLA+ specs of real systems. The authors check the specs by bounded exploration, plus replay against traces captured from the running systems.
- number: 4 models, 5 generations per cell
- number: Spin traces: 28 windows, 8 of 18 observable input combinations covered
- number: small tasks 40/40 complete passes; Raft scale 0/20 initially, 6/20 after one repair round
- number: state-changing conformance of original models ranges 0-86.4% though all pass syntax and invariants
- limits: It checks no liveness or temporal properties. It explores only to a bound. It does not prove that the implementation matches the model. The author designed the instrumentation, the reference model and the prompts.
- how much was read: most of it read
- source; notes: JS-SAM: a controlled case study separating specification shape from la; notes: JS-SAM: a controlled case study separating specification shape from la
- record id: js-sam-2026
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 outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_google.md; notes: Additional tools, not counted as papers
- record id: kiro-2026
LeetProof (2026)
- title: Certified Program Synthesis with a Multi-modal Verifier
- what: LeetProof checks generated specifications against examples and reference implementations. It then synthesizes Velvet/Lean code, using SMT solvers to discharge proof goals automatically. A person finishes the remaining goals interactively.
- number: GPT-5.2 Velvet pipeline fully proves 28 of 50 tasks vs Lean-only 17
- number: 16 issues in VERINA (of 189 specs, 8.5%) and 18 in CLEVER (of 161, 11.2%) via property-based testing
- number: Verina issues took 9 minutes of property-based testing vs about 8 hours of LLM equivalence checking
- limits: It synthesizes algorithms with simple types. It has no distributed models and no liveness.
- how much was read: most of it read
- source; notes: Dafny, C verification, and the specification-intent gap; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_eval.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_eval.md
- record id: leetproof-2026
OSVBench (2026)
- title: OSVBench: Benchmarking LLMs on Specification Generation Tasks for Operating System Verification
- what: A benchmark in which an LLM writes a Python/Z3 specification of a syscall from a description. The spec is scored by whether it detects the same injected errors in code variants as the reference spec does. Declaration specs stay fixed.
- number: 245 tasks from 49 system calls, 5 variants each (1 correct, 4 with injected bugs)
- number: 12 LLMs; best pass@1 55.10% (Doubao-1.5-pro); five zero-shot models score zero
- number: five-example prompts use 20,000-30,000 tokens
- number: 245 tasks from 49 system calls (each: one correct and four vulnerable variants)
- limits: It covers functional and safety properties only, with no liveness. The LLM is given a description, assumptions and an abstract kernel model.
- how much was read: most of it read
- source; notes: OSVBench: executable specifications with a fixed external oracle; notes: OSVBench: executable specifications with a fixed external oracle; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/verified_primary_notes_20261012.md
- record id: osvbench-2026
Proofs Promptly (2026)
- title: Proofs Promptly: An Experience Report on Proof-Oriented Programming with AI Agents
- what: The report uses Copilot CLI with Opus 4.5, with skills, subagents and a REPL. It writes Pulse/F* separation-logic proofs of concurrent locks and semaphores, the MSQuic receive buffer, and a port of the OCaml garbage collector.
- number: Table 1 p. 3: 1 week/ $1229, 1 w ee k /$ 583, 2 weeks/ $1580; ab o u t am o n t han d$ 3,392 total (notes’ addition)
- number: Six-month manual estimate is the authors’ estimate, not a controlled comparison
- number: manual proof-engineering cost estimated at roughly half a year
- number: three experts, two weeks, versus about half a year manually (authors’ estimate)
- limits: Experts review the specs and supply the invariants that decide the proof. It has no theorem about distributed fairness or eventual progress.
- how much was read: most of it read
- source; notes: Proof-oriented programming at Microsoft; notes: papers; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_shortlist.md
- record id: proofs-promptly-2026
Reality Is the Final Verifier: On Two Key Gaps in Agentic Software Engineering (2026)
- what: Argues that verification stops short in two places. The written requirements may not match what the stakeholder wants (the requirement gap). The model used to evaluate code may not match the real environment (the model gap). Proposes an inner loop, which revises code against the requirements, the environment model and the evaluator. Proposes an outer loop, which uses observations from deployment to revise those inputs.
- number: no new theorem, experiment, or implementation proof; Table 2 incidents are cited from other reports
- number: No measured completion rate or human-hours; Table 2 incidents are cited from other reports
- limits: A proposed architecture. No measured rate of autonomous completion and no human-hours result.
- how much was read: most of it read
- source; notes: Reality Is the Final Verifier: On Two Key Gaps in Agentic Software Eng; notes: Reality Is the Final Verifier: On Two Key Gaps in Agentic Software Eng; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_shortlist.md
- record id: reality-is-the-final-2026
RFC2TLA+ (2026)
- title: RFC2TLA+: Extracting and Verifying Formal Models from RFC Documents using Continuous LLM Feedback
- what: An LLM agent with 22 tools extracts communicating state machines and invariants from an RFC and emits TLA+. It refines the result using TLC counterexamples, for up to three rounds.
- number: 14 real RFCs; all get a TLC-accepted model in best-of-three
- number: correct models pass 36/42 runs; injected faults found 69/84 (33/42 deadlocks, 36/42 invariant violations)
- number: synthetic RFCs 16/18
- number: avg 710 TLA+ lines (262-1,944); state F1 0.97, transition F1 0.61 vs 0.49/0.21 for RFC2PSM
- limits: It uses TLC models checked within bounds, not code. Deadlock detection is weaker than liveness checking. The agent may change invariants, so a passing run does not show fidelity. No wall time or manual effort is reported. The artifact record is restricted.
- how much was read: most of it read
- source; notes: RFC2TLA+: extract both a model and invariants from a supplied RFC; notes: RFC2TLA+: extract both a model and invariants from a supplied RFC
- record id: rfc2tla-2026
Seeking Specifications: The Case for Neuro-Symbolic Specification Synthesis (2026)
- what: DeepSeek-R1 generates ACSL function contracts for C code. Optionally it also uses PathCrawler tests or Frama-C EVA alarms. The researchers check whether the contracts recover the intent, rather than preserve a recognized bug.
- number: Table 1 bug recognition: Basic 47/60, Famous 9/30, Anonymized Basic 50/60, Anonymized Famous 14/30
- number: 50 programs, four variants, three generations each; 55 PathCrawler examples
- limits: The study is qualitative. It has no end-to-end correctness proof of the generated contracts. By default the contracts encode the code, not the inferred intent. Figures 6 and 7 print the same contract despite opposite captions.
- how much was read: most of it read
- source; notes: Seeking Specifications: The Case for Neuro-Symbolic Specification Synt
- record id: seeking-specifications-the-case-2026
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
Spec-Harness (formerly VeriAct) (2026)
- title: VeriAct / Spec-Harness: Beyond Verifiability — Agentic Synthesis of Correct and Complete Formal Specifications
- what: The paper adds agent repair around JML spec generation. It scores specs in a harness that the evaluator owns, using four fractions: valid outputs accepted, bad outputs rejected, valid inputs admitted, invalid inputs excluded.
- number: v2 uses thresholds such as PostCorr >= 0.75 and PostComp >= 0.75 (operational choice)
- number: 120 SpecGenBench methods and 662 FormalBench methods
- number: SpecGen falls from 54% verifier acceptance to 24% meaningfully verified on SpecGenBench (§5.4)
- number: three refinement cycles; improvement of 5 points on SpecGenBench and 12 on FormalBench (§6.1)
- limits: Success is relative to the generated cases and the reference. The task supplies existing code, so eliciting intent is not tested. Feedback on the scoring set can inflate scores. Use withheld tests.
- how much was read: most of it read
- source; notes: Generated contracts and independent evaluation; notes: Spec-Harness, formerly VeriAct; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_agents.md
- record id: spec-harness-formerly-veriact-2026
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; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_intent.md
- 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 outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_agents.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings_agents.md; notes: SysMoBench
- record id: sysmobench-2026
SysSpec / SpecFS (2026)
- title: Sharpen the Spec, Cut the Code: A Case for Generative File System with SysSpec
- what: Humans write structured specs for 45 modules, with pre/postconditions, invariants and locking. Agents generate C code, and an LLM reviews it. The result is SpecFS, an in-memory FUSE file system.
- number: about 4,300 C lines, 45 modules
- number: 754 xfstests, 64 fail from unsupported features
- number: Gemini-2.5-Pro and DeepSeek-V3.1 reach 100% module accuracy vs 81.8% best baseline
- number: extent support 4.5 vs 1.5 hours; directory rename 13 vs 2.4 hours (manual vs SysSpec)
- limits: The verification stage is an LLM, not a theorem prover. The evidence of correctness is tests and inspection. Crash consistency is out of scope. The timings cover specific tasks only.
- how much was read: most of it read
- source; notes: SysSpec / SpecFS: sharp human specifications, empirical code checking; notes: SysSpec / SpecFS: sharp human specifications, empirical code checking
- record id: sysspec-specfs-2026
TESTDAFNY110 (2026)
- title: Automatic Generation of Formal Specification and Verification Annotations Using LLMs and Test Oracles
- what: LLMs write Dafny contracts, invariants, assertions and lemmas from code, comments and test methods with expected results. They repair them using verifier errors. Dafny proves the result.
- number: 98.2% of problems within at most 8 attempts
- number: 106 of 110 (96.4%) logically equivalent to expert specs
- number: seven-student crossover study: 85.7% vs 42.1% success, 6.2 vs 11.1 minutes (the notes call these assisted/manual success and average task minutes)
- number: 98.2% on 110 Dafny programs within 8 repair iterations
- limits: Two number-theoretic tasks are unsolved. Four contracts differ from the expert ones until failing tests are added. It needs human tests that discriminate between right and wrong.
- how much was read: most of it read
- source; notes: Automatic Generation of Formal Specification and Verification Annotati; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_eval.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/verified_primary_notes_20261012.md
- record id: testdafny110-2026
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 outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_google.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/verified_primary_notes_20261012.md; notes: 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: Across 25 LLMs the best public baseline is 26.6% syntactic parse and 8.6% semantic model-check
- limits: Success means a small model passes its own invariant. It does not mean agreement with a human requirement or a system. The text says six domains, but Table 3 lists ten. There is no refinement or liveness proof. The result was not reproduced.
- how much was read: most of it read
- source; notes: paper; notes: meaning for evaluation; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_agents.md
- record id: tla-prover-2026
Toward Safe LLM Agents: A Survey of Specification, Verification, and Enforcement (2026)
- what: A survey of 38 studies on specifying, verifying and enforcing safety for LLM agents. It distinguishes model checking of an extracted model from runtime enforcement on actual actions.
- number: 38 studies from six databases
- number: headline 24% to 35% concerns PDDL planning formalization only
- number: 94% interception with under 5% safe completion comes from one study
- number: single reviewer
- limits: Focuses on safety. No new measurement. Certainty is mostly Low or Very Low. Its broad claims about limits should be audited.
- how much was read: most of it read
- source; notes: Toward Safe LLM Agents: A Survey of Specification, Verification, and E; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_google.md
- record id: toward-safe-llm-agents-2026
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; notes outside this site: `/ssd1/sichangheagent/verus_distributed/lit_a/findings2_model_to_code.md`; notes outside this site: `/ssd1/sichangheagent/verus_distributed/lit_a/findings2_shortlist.md` - record id: `tracefix-2026` - Validating Formal Specifications with LLM-generated Test Cases (2026) - what: GPT-5 generates positive and negative Alloy instances from English requirements, before the requirement is formalized. Expert formulas label the instances. The authors test whether the instances expose wrong student specifications. - number: Table 3: Few prompt, 258 tests, 255 syntax-valid, 252 previous-consistent, 247 valid (96%),$ 3.56
- number: Table 6: 35 requirements with complete suites, 4816 wrong specs, 348 missed, mean missed 6.43%
- number: 258 requested tests; few-shot GPT-5 247 valid (96%, 30 per high/medium/low bug
- limits: The authors say the quality of the generated properties is the main limit.
- how much was read: only abstract or first pages read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_intent.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/verified_primary_notes_20261012.md; notes: specification-anchored auditing
- record id: speca-2026
Specifications for Humans, Agents, and Tooling (2026)
- what: Describes the Bosque API ecosystem for agent-driven development. It has polyglot specs, test generation, validation and sandboxing. Specs are shared artifacts for people, agents and tools.
- limits: A position on tooling. No refinement theorem and no evaluation on a distributed protocol. Not evidence that intent can be recovered automatically.
- how much was read: only abstract or first pages read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_leads.md; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/verified_primary_notes_20261012.md
- record id: specifications-for-humans-agents-2026
SpecLoop (2026)
- title: SpecLoop: An Agentic RTL-to-Specification Framework with Formal Verification Feedback Loop
- what: Candidate specs are used to rebuild the RTL (hardware design code). Formal equivalence checking feeds counterexamples back to refine the spec. It improves over baselines that use only an LLM.
- limits: Results depend on the RTL reconstructor and the equivalence checker. Bounded resource limits can block feedback. It reverse-engineers a spec from a design, and does not recover an unconstrained request.
- how much was read: only abstract or first pages read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/verified_primary_notes_20261012.md; notes: SpecLoop; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_b/agent_evaluation_procedure.md
- record id: specloop-2026
FLAG (2025)
- title: FLAG: Formal and LLM-assisted SVA Generation for Formal Specifications of On-Chip Communication Protocols
- what: It takes unstructured protocol documents to checked properties. It generates candidate properties from a grammar, filters them with timing diagrams and checks them formally.
- limits: It covers a constrained domain: hardware protocols.
- how much was read: only abstract or first pages read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/verified_primary_notes_20261012.md; notes: FLAG; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_b/agent_evaluation_procedure.md
- record id: flag-2025
Specifications: The Missing Link to Making the Development of LLM Systems an Engineering Discipline (2024)
- what: This position paper argues that explicit specifications are the missing engineering layer for LLM systems.
- limits: The pages the review notes inspected show no formal verification artifact or proof result.
- how much was read: only abstract or first pages read
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_leads.md
- record id: specifications-the-missing-link-2024
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
APG (2026)
- title: Generating Protocol Code from RFC Specifications
- what: It generates C/C++ protocol code from RFCs for ICMP, IGMP, NTP and TCP, and judges the code by testing.
- number: 95% compile success and behavioral correctness for stateless protocols like ICMP
- number: 90% interoperability for complex stateful protocols such as TCP
- limits: It has no formal spec. The notes’ author only skimmed it.
- how much was read: not read; title and metadata only
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_google.md
- record id: apg-2026
HumanEvalComm (2024)
- what: A benchmark with communication metrics that measure whether models ask clarifying questions.
- limits: The review notes saw it only as a search snippet.
- how much was read: not read; title and metadata only
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_eval.md
- record id: humanevalcomm-2024
An Experiment in Formal Verification with Claude
- what: Claude Opus 4.6/4.7 wrote the Lean 4 statements and most of the proofs for the soundness and zero-knowledge theorems of Succinct’s VEIL compiler. A CLAUDE.md file with simple rules guided it. Humans revised the statements and checked the Lean against the English descriptions.
- number: human revised statements over dozens of iterations
- number: human time roughly 1-2x the time of writing the paper versus about 10x typical
- number: a full protocol can mean auditing about 1,000 lines of Lean
- limits: This is a blog post, not a peer-reviewed paper. The notes rest on a tool summary, not on the page text. It is not about distributed systems. Claude sometimes silently swapped ‘for all, there exists’ for ‘there exists, for all’ in zero-knowledge claims. It also defined malicious provers that were too weak.
- how much was read: not read; title and metadata only
- source; notes outside this site: /ssd1/sichangheagent/verus_distributed/lit_a/findings2_google.md
- record id: an-experiment-in-formal

Last edited: 2026-10-13

Keyboard shortcuts

Steven Hé (Sīchàng)

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