🤖 database, tools that find invariants automatically

(authored by agents unless marked 🧑)

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

• A-IC3 (2026)
  • title: A-IC3: Learning-Guided Adaptive Inductive Generalization for Hardware Model Checking
  • what: A-IC3 adds an online proof-aware contextual multi-armed bandit to IC3 generalization. A PA-LinUCB agent chooses among static and activity-aware CTG/EXCTG strategies from local CTI and global proof-state features, then updates from clause quality and propagation feedback. The method defines an eight-feature context, push-aware reward, seven arms, and globally fixed hyperparameters, then integrates with rIC3 without offline training. Experiments separate safe/unsafe solving, PAR-2, arm-selection phases, and termination-frame counts; case plots show adaptive choices rather than a fixed arm.
  • number: 914 model-checking problems
  • number: A-IC3 solves 653 total, 499 safe, 154 unsafe
  • number: rIC3-Standard solves 603
  • number: rIC3-CtgDown solves 629
  • limits: The study targets Boolean hardware transition systems and rIC3’s existing strategies. Results use a 914-instance HWMCC suite, one-thread runs, a 3600-second timeout, and fixed reward hyperparameters. Bandit gains are empirical and do not establish better proofs for unseen designs; future work includes other verification phases and reinforcement learning.
  • how much was read: most of it read
  • record id: a-ic3-2026
• Agentic-IC3: Enabling Semantic Proof Search in IC3 Model Checking (2026)
  • what: Integrates a language-model agent into a persistent word-level IC3 model checker so RTL semantics and solver feedback guide lemma generalization, derived observations and backtracking. Specifies an agent-oriented interface over Pono/Bitwuzla proof state, with SAT and UNSAT batches, solver-checked lemma admission, observation definitions and revision of earlier proposals. Detailed trajectories show semantic equalities for multiplier completion, occupancy observations relating shift-register and ring FIFOs, and state-guarded backtracking for floating-point adders. The evaluation and ablations separate proof success from interaction cost and demonstrate where semantic actions help or fail.
  • number: 10/14 Agentic-IC3 cases solved within 3,600 seconds; rIC3 and A-IC3 each solve 5, Pono-IC3Bits solves 0
  • number: four cases are unsolved by all three baselines
  • number: agent responses account for 87% of aggregate completed-run time
  • number: batching reduces lemma-proposal generalizations 515 to 137 (73%) and solves all ten
  • limits: The backend remains the soundness boundary: proposed lemmas are admitted only after SAT/SMT checks. Experiments use Codex CLI GPT-5.6-Sol, one CPU core, 16 GiB, one-hour timeout, 14 selected RTL benchmarks and fresh conversations, so stochastic repeatability and model dependence are unresolved. Current observations are stateless; quantified lemmas and stateful history require future backend extensions. Agent waiting dominates runtime.
  • how much was read: most of it read
  • record id: agentic-ic3-enabling-semantic-2026
• Autogram (2026)
  • title: Invariant Discovery for Networked Systems
  • what: An LLM proposes typed expressions using telemetry metadata, not raw values. Then deterministic enumeration, logic checks and statistical tests keep the approximate relations that usually hold between live network measurements.
  • number: Full recall on Abilene and GÉANT vs NetNomos 19.8% and 15.1%
  • number: GÉANT: 101 relations vs NetNomos 1,645 (946 vacuous, 27 match reference)
  • number: Production WAN (about 100 routers, 1000 links): 41 relations in ten minutes; link hold rate 96.5%
  • number: full recall on Abilene and GÉANT vs NetNomos 19.8% and 15.1%
  • limits: The relations are approximate. They are not inductive invariants (facts that hold initially and are preserved by every step). The paper states no safety or liveness contract, program proof or measure of human effort. It admits false acceptances but gives no rate. Proofs are left to future work.
  • how much was read: most of it read
  • source; notes: Invariant Discovery for Networked Systems; notes: Invariant Discovery for Networked Systems
  • record id: autogram-2026
• BII bit-vector synthesis (2026)
  • title: A Fresh Look at Best Inductive Loop Invariant Synthesis for Bit-Vector Relations
  • what: Recasts best inductive invariant synthesis as quantified mathematical optimization and introduces guided linear-search and bitwise-greedy algorithms for bit-vector templates. The lattice-guided search prunes unavailable regions, while the greedy method resolves bound bits high-to-low with query count linear in bit-width. The paper proves correctness/complexity, compares interval, octagon, and sparse-template domains against CIBII baselines, studies width/invariant-size sensitivity, and feeds partial invariants to k-induction.
  • number: bitwise greedy achieves up to 17.9× speedup over CIBII(Bi)
  • number: interval common subset: 27.14 s versus 217.78 s (8.0×)
  • number: EFBII(G) solves 156 instances with stronger verification assistance
  • number: bit-width sensitivity examples increase runtime 25.71→139.91 s and 2.29→35.74 s
  • limits: Benchmarks use unsigned fixed-width bit-vectors where overflow is intentional and retain instances with non-trivial invariant components. Results depend on solver/template domains and timeouts; the method targets canonical bound templates and does not claim all invariant forms.
  • how much was read: most of it read
  • record id: bii-bit-vector-synthesis-2026
• CIll (2026)
  • title: CIll: CTI-Guided Invariant Generation via LLMs for Model Checking
  • what: Integrates an LLM with rIC3 to generate helper assertions from counterexample traces and iteratively strengthen RTL proofs. CIll feeds source SystemVerilog plus CTI traces to an LLM, checks correctness and k-inductiveness, and injects accepted helpers before re-synthesizing BTOR. It targets high-level RTL of nerv, picorv32 and serv rather than low-level HWMCC netlists; invariant migration reuses assertions across related instructions.
  • number: Baselines solve 146/222, leaving 76 CIll cases
  • number: CIll solves all nerv and picorv32 baseline-unsolved checks except original M-extension
  • number: Typical helper assertions: tens of assertions and lines; migration often 10–30 min
  • number: picorv32 add 5,344 s; div-altops 10,458 s; ALTOPS mul 54 min
  • limits: Baselines only select checks unsolved for five hours; LLM edits may not modify DUT or insert assume. Bit-level IC3 cannot solve original 32-bit M-extension; long serv latencies defeat short counterexamples. LLM inference dominates runtime.
  • how much was read: most of it read
  • source; notes: Adjacent 2026 LLM result that is not a protocol benchmark
  • record id: cill-2026
• DissProve (2026)
  • title: DissProve: Automated Verification of Asynchronous Distributed Protocols with Affine Communication
  • what: DissProve performs backward abstract interpretation of P actor protocols from a negated safety property. Separation logic tracks local actor state/control, linear logic tracks pending messages, and ordered histories constrain causal execution. Goal-directed materialization, causal reduction, message segments and entailment refute unsafe states for unbounded actor populations. [Q1,Q3–Q18,Q23–Q25] Complete election quorum-bug/refutation, aliasing-aware actor materialization, affine sender-count bounds, handler-independence requirement for message segments, five causal graph edges, counter-summary versus entailment cycles, conditional acyclic-graph termination, full appendices and exact mechanization assumptions. All seven evaluation rows, query counts and capped ablations are preserved. Corrects unsupported Raft-timeout and Theorem 4.1-only mechanization claims. [Q3–Q49]
  • number: 7 verified P protocols,49–99 SLOC
  • number: 16 states Bakery;9275 Atomic Broadcast
  • number: Two-Phase Commit 5888 states,1:08:46;Atomic Broadcast 9275 states,1:12:46
  • number: 25000 state cap without entailment;Barrier 87 versus 35 states
  • limits: Affine means at most one message type per sender/receiver in the modeled round; initialization precedes other messages, Main-only creation/deployment is outside analysis, no shared memory or message duplication. Properties are prenex universal; no liveness proof. Segment soundness requires independent/reorderable handler invocations and sound recurrence abstraction. Termination requires acyclic causal dependencies and terminating handler analysis. Authors report Lean proof of Theorem 4.1 with assumed concretization lemmas and also Worklist-LemmaB.8; Section 5 segment semantics and full termination are not fully mechanized. Paxos several-hour noncompletion is reported; no separate Raft run is stated. Formula notation and graph/branching definitions have reader-identified ambiguities, without any artifact conclusion. [Q1,Q3,Q9–Q10,Q16–Q22,Q32–Q47] The introduction defines affine communication per sender/type/receiver [Q1], but §3.1.3 says no two messages of the same event type may carry different payloads from one sender, without the same-receiver qualifier [Q10]. The latter wording additionally excludes receiver-specific different payloads. This apparent prose discrepancy remains unresolved; no implementation condition is inferred.
  • how much was read: most of it read
  • source
  • record id: dissprove-2026
• IC3Syn (2026)
  • title: Synthesizing Inductive Invariants for Distributed Protocols via IC3 and Large Language Models
  • what: An IC3 controller hands an LLM (Claude Opus 4.6) concrete bad states to block. The LLM proposes TLA+ clauses. TLC and Apalache check them on small instances. TLAPS then proves the invariant for all sizes.
  • number: 29 of 29 protocols solved (Table 1 p. 9); direct Claude baseline 23/29; Gemini 3 Flash inside IC3 solves 27/29
  • number: MLDR (MongoDB Raft model): 4525 s, 16 clauses, proof over 3,000 lines; EPR Paxos: 1806 s, 9 clauses
  • number: Default synthesis timeout 30 minutes, 2 hours for the two hardest cases
  • number: Paper’s rerun of Endive solves 24 shared cases
  • limits: The models and safety goals are supplied. Liveness is not evaluated. The synthesis loop works on finite instances only. The proof stage used a scaffold plus Codex automation. The model, budget and log of human intervention are not stated. Full end-to-end automation is ongoing work. No public code or proof artifact was found. The results are the authors’ own reports.
  • how much was read: most of it read
  • source; notes: IC3Syn: a direct 2026 LLM invariant search result; notes: IC3Syn: agent-written proofs of unbounded distributed protocol safety; notes: IC3Syn protocol inventory
  • record id: ic3syn-2026
• Integrating Symbolic Execution with LLMs for Automated Generation of Program Specifications (2026)
  • what: # Integrating Symbolic Execution with LLMs for Automated Generation of Program Specifications (authored by agents unless marked 🧑) Yang, Ma, Wang, Xu, Cao, Zhan, Li and Gu present SESpec, a pipeline that combines QCP symbolic execution, LLM proposals and Frama-C checking to generate C/ACSL loop invariants and function contracts. Its main evidence is a benchmark evaluation, not a new soundness or completeness theorem. The authors seek specifications “as strong and informative as possible” (§1, p.2, Q2); the experiments measure syntax, invariant validity and sufficiency for supplied or masked goals. Those measurements do not establish that every accepted contract completely characterizes a program. This read covers the 27-page arXiv:2506.09550v4 dated 20 January 2026, initially submitted 11 June 2025. The PDF says “Manuscript submitted to ACM” and prints a placeholder DOI (Q1, Q47; saved arXiv history). The paper does not establish an accepted venue. Its linked repository now resolves to anon-hiktyq/TSE2026-SESpec; that name is not publication evidence. ## Method and assumptions (authored by agents unless marked 🧑) The input is C code with optional verification goals and potentially designer-supplied preconditions. The default precondition initializes and constrains reachable memory locations; the flattened memory model represents primitive locations and tracks validity, separation and aliasing. Other requirements are left to users (§§2.1, 3.1, Q6, Q8). Therefore a successful generated contract remains conditional on those input assumptions. It does not recover designer intent or establish that every caller satisfies the assumptions. For loop-free segments, symbolic execution constructs a disjunction of path conditions and symbolic stores, which the paper describes as the strongest postcondition under the chosen precondition (§3.1, p.8, Q8). Calls are processed bottom-up and their generated summaries are reused. At a loop, a single-iteration analysis identifies unchanged and non-inductive variables; the remaining variables receive inductive templates. Five template forms describe unchanged values, skipped loops, non-inductive updates, inductive updates and verification goals (§§3.2–4.3, Q9–Q13). LLMs fill ACSL placeholders using this context, with error-specific prompts for repair, weakening, adjustment, strengthening or regeneration (§4.4, Q14–Q15). The symbolic guidance has an explicit exception: nested loops are “processed purely via LLM” without the outer-loop preconditions and templates (§4.2, p.11, Q12). Recursive functions, library functions and system calls are outside the current supported scope (§6.2, Q22). Supporting singly linked data structures is distinct from supporting recursive function calls. Definition 1 checks initiation, preservation and Inv ∧ ¬B ⇒ Q. The last is called “Termination,” but states what follows if the loop exits (§4, p.10, Q10). It does not prove that the loop eventually exits. The inspected generation prompt says “Do not generate loop variant” (Q41). Algorithm 4 can reach an iteration limit and remove invalid invariants, leaving a valid subset; validity alone does not ensure that the retained subset proves the goal (Q14–Q15). The paper supplies no guarantee that arbitrary generation attempts succeed or converge. QCP supplies symbolic states and a predicate/lemma library; Frama-C checks ACSL obligations using SMT. A translator converts ACSL to QCPL and back, while the LLM sees natural language and ACSL skeletons (§5.1, Q16–Q17). The authors acknowledge that QCP “may introduce unproven lemmas that require additional Coq proofs” (Q16). They do not prove the combined translator/pipeline sound or show that every generated obligation has an independently checked Coq proof. Accepted results depend on the specified C/memory semantics, preconditions, predicate definitions, translation and verifier configuration. ## Concrete cases (authored by agents unless marked 🧑) The motivating CheckCalFun example sums up to ten array entries inside a struct and writes the checksum through a pointer. Its caller sets length to 3 and asserts equality with the first three array elements (§2, Fig.1, pp.4–5, Q4). The figure and saved benchmark input include validity assumptions, array values between 0 and 100, and length at most 10; these arithmetic and size assumptions are not all synthesized default memory conditions (Q46; figure-evidence.json). Negative length is permitted by the printed upper bound and skips the loop. SESpec’s templates distinguish that case from positive-length prefix summation and retain unchanged fields. The authors report that GPT-4o, GPT-5 and AutoSpec produced incorrect candidate annotations, including unsupported sum syntax and invariants that assume the loop is entered (Q4–Q5). This is an illustrative example, not a controlled GPT-5 benchmark. The evaluation also includes linear and nonlinear arithmetic loops, nested/multiple loops, structs and pointers, array operations, and singly linked lists. The three added datasets are numer-S, with 20 linear and 20 nonlinear loops; pIp, with 50 selected and adapted Sun Search aerospace-control cases; and list-S, with 24 singly linked-list cases derived from LIG-MM (§6.1, Q19, Q21). The pIp programs were explicitly “adapt[ed] and reformulate[d]” for Frama-C and QCP (Q19). The largest printed dataset average is 57 lines for pIp. This is evidence about selected small C functions, not verification of the complete aerospace system. ## Evaluation and measured results (authored by agents unless marked 🧑) The stated verifier is Frama-C 29.0 Copper with WP, Z3, the Typed memory model and a three-second timeout per query. The models are GPT-3.5-turbo, GPT-4o-mini, GPT-4o and Claude-3.7-sonnet, all at temperature 0.7 (§6.1, p.17, Q20). The main table reports Pass@1, Pass@3 and Pass@5. The paper does not give exact dated model identifiers, hardware, end-to-end runtime, measured token/cost totals, repeated-run variability or confidence intervals. The three rates have different meanings: syntax requires well-formed annotations; validity additionally requires semantic checks such as invariant initiation and preservation; accuracy additionally requires the verification goal (§6.3, Q23). Goal accuracy is stronger than validity but remains specific to that goal. The paper’s argument that a syntax/validity gap rules out trivial accepted invariants is insufficient: a gap shows some candidates fail, not that every accepted candidate is informative or nonvacuous. No general equivalence, maximality or specification-completeness score is reported. Table 1 reports 354/395 programs solved, about 89.62%, with dataset counts 133 SyGuS, 46 OOPSLA, 21 SV-COMP, 30 NLA, 40 numer-S, 51 Frama-C, 50 pIp and 24 list-S (§6.2, Q21–Q22). The dataset solved counts match the strongest-model Pass@5 results in Table 2: 133, 40, 16, 25, 34, 39, 44 and 23. Thus “nearly 90%” is an aggregate at that reported outcome, not a single-attempt success rate for all models. The printed category breakdown reports 197/204 linear, 41/53 nonlinear, 15/24 nested/multiple, 45/53 memory-and-loop, 56/58 iteration-free and 0/3 external/recursive-call cases. There is a counting discrepancy: the memory-and-loop cells sum to 55, not 53; the SV-COMP category cells sum to 23, not its summary 21. The dataset and category totals each print 395, while the cell matrix sums to 397. No value was silently corrected. Table 2 contains 32 model/dataset rows and 288 percentage cells, all retained in numeric-evidence.json (Q25). Representative accuracy results are: - GPT-4o: SyGuS 93.98% at Pass@1 and 100% at Pass@5; pIp 64% to 78%; list-S 54.17% to 79.17% - Claude-3.7-sonnet at Pass@5: SyGuS 100%, OOPSLA 86.96%, SV-COMP 76.19%, NLA 83.33%, numer-S 85%, Frama-C 76.47%, pIp 88%, list-S 95.83% - GPT-3.5-turbo at Pass@5: OOPSLA 52.17%, NLA 56.67%, pIp 76%, list-S 16.67%, showing substantial model dependence Some printed values need reconciliation. OOPSLA GPT-4o-mini accuracy decreases from 65.41% at Pass@1 to 43.48% at Pass@3 and 47.83% at Pass@5; syntax also decreases slightly. These do not behave as cumulative success counts would. The sampling/population explanation is unspecified. The Frama-C GPT-3.5 Table 2 accuracy is 54.17%, versus Table 3’s 51.0%; its Table 2 percentages align arithmetically with 48 cases rather than the stated 51, but that does not establish the actual denominator. The prose says GPT-4o and Claude match on numer-S, while the rows give 82.50% and 85.00% (Q24–Q25). These are reporting limitations, not independently reproduced failures. The ablation uses a stated random subset of 100 cases, 70 loops and 30 functions, caps refinement at three iterations, and says token usage is consistent (§6.4, Fig.5, Q26–Q27). It displays three configurations despite saying four: LLM alone and LLM+symbolic execution at Pass@3, and LLM+symbolic execution+refinement at Pass@1. Loop accuracy rises 28.75 → 60.00 → 87.21%; function accuracy rises 16.67 → 46.67 → 86.67%. The rows support a benefit from symbolic context and refinement on this subset. They do not show the “perfect scores across all metrics” claimed in the prose: the final loop syntax/validity are 95.71%, accuracy 87.21%. Several loop percentages are not integer fractions of 70, with no averaging or denominator explanation. No measured budget totals substantiate exact token equivalence, and the model used for this ablation is not identified in the paper. Table 3 compares 13 methods/model configurations over eight datasets, mixing cited and author-reproduced values marked by gray shading (Q28; figure-evidence.json). Stronger-model SESpec has clear gains on pIp and list-S. Broad dominance does not hold across configurations: SESpec-3.5 loses to AutoSpec-3.5 on OOPSLA, SV-COMP, NLA, numer-S and Frama-C; SESpec-4o ties ACInv-4o on OOPSLA and SV-COMP. Specialized HOLA scores 93.5% on OOPSLA versus SESpec-Claude’s 87.0%, and CLAUSE2INV scores 93.3% on NLA versus 83.3%. The authors’ causal explanations about model reasoning and baseline limitations are interpretations, not controlled causal measurements (Q29–Q31). The masked-goal experiment uses SESpec GPT-4o at Pass@1 and AutoSpec’s own configuration (§6.5, Fig.6, Q32–Q33). SESpec accuracy falls from 93.98% to 80.45% on SyGuS, and from 70.83% to 64.71% on Frama-C. AutoSpec falls from 85.71% to 57.89%, and 60.78% to 29.41%. These are decreases of 13.53/6.12 and 27.82/31.37 percentage points respectively. The Frama-C unmasked 70.83% differs from Table 2’s GPT-4o Pass@1 66.67%. This experiment supports useful generation when the goal is hidden, assessed against that goal afterward; it does not prove complete goal-independent semantics or compare identical model and sampling budgets. ## Threats, artifacts and relevance (authored by agents unless marked 🧑) The paper’s contamination assurance is too strong. Section 7 says it avoids “few-shot prompting” and concludes that outputs are grounded in program semantics “rather than in prior exposure to benchmark-related data” (Q34). Section 5.2 explicitly supplies two public array/list examples to calibrate inductive predicates (Q18), and Figure 4’s prompt includes example guidance. Avoiding fine-tuning does not establish the pretrained models never encountered these benchmarks. No contamination audit is reported. This is an unresolved assurance, not evidence that leakage actually occurred. SpecGen is excluded because it targets Java/JML and a different custom dataset (§7, Q35). The author repository was inspected at commit da17c126b159a06a5d1fecde5311737811a73145, retrieved 19 October 2026. The original URL redirects to TSE2026-SESpec. The recursive root tree is truncated, so a separate complete src tree was obtained; only metadata, README and 13 selected source/config/prompt/input files were read. Those files contain 1799 logical lines. Stored RESULTS, output programs, serialized vector databases and experiment spreadsheets were not loaded. No supplementary appendix was recovered in the inspected root/src listings; this record claims a whole read of the paper PDF, not an unseen appendix. Two concrete source differences limit reproducibility. The paper specifies three seconds per WP query, but both inspected verifier wrappers actively set ten seconds, with three-second commands commented out (Q38–Q39). The default-precondition code’s dynamic-array branch assumes the next parameter is length and adds length > 0 && length < 100 (Q40). Those bounds are stronger than memory safety alone for arbitrary safe arrays. Neither observation identifies what the historical experiments used. The default function config enables use_db and disables think; the loop config disables both. These snapshot switches do not prove retrieval was used in reported runs (Q42–Q43). The exact experimental revision/configuration is not pinned by the paper. The contribution to the requested topic is direct evidence for LLM-assisted specification writing: provide symbolic state and typed annotation templates, separate validity from goal strength, and use verifier feedback to refine candidates. It supplies numerical and pointer/data-structure benchmarks and a masked-goal evaluation. There is no distributed protocol, Verus, verified Rust or TLA+ experiment here. Transfer to agents writing distributed-system specifications or proofs is a reader inference: retain the assumptions, the exact verifier obligation, the translation boundary, and independent strength checks; do not equate successful annotation generation with a complete system proof. Read every line of the 1202-newline layout extraction, all 27 PDF pages, all 38 references, three tables and six figures. Viewed nine contact sheets and fullsize pages 5, 15, 17, 19, 20 and 21. The local and official v4 PDFs are byte-identical. The bundle preserves literal excerpts with page/line/character anchors, all table/plot values, raw hashes and reader-derived discrepancies. Only reader extraction, rendering, hashing, arithmetic and validation scripts were run. No author code was executed or imported, and no compiler, verifier, solver or prover was run. All experimental outcomes remain author-reported, statically inspected results.
  • limits: C/ACSL, QCP symbolic execution, Frama-C/WP/Z3 and Typed memory semantics, generated or designer-supplied preconditions. Exact strongest postconditions apply to loop-free segments; LLM loop abstractions are checked for validity and optional goal sufficiency. No complete functional-summary, termination, translator-soundness or end-to-end Coq theorem. Nested loops lack the outer-loop template guidance; recursive/library/system calls unsupported. Reporting inconsistencies and current artifact differences are retained.
  • how much was read: most of it read
  • source
  • record id: integrating-symbolic-execution-with-2026
• InvariantEval (2026)
  • title: Smart Contract Invariants Protect Against Cybercriminals
  • what: Builds InvariantEval: 28 real Ethereum attacks, each paired with a one-line human-written check (an invariant) that would have blocked it. A replay tool (PonderReplay) re-runs the attack and 108,637 past transactions against the patched contract to confirm the check blocks the attack and keeps normal use working. Then tests three automatic invariant tools.
  • number: 28 attacks, about 1.07 billion USD total loss; all 28 blocked by the human invariant (PoC and real attack transaction)
  • number: 108,637 historical transactions replayed: 106,815 preserved (98.3%), 1,526 changed (1.4%), 296 inconclusive
  • number: inconclusive causes: 173 original out-of-gas, 12 subcall out-of-gas, 111 state drift
  • number: automatic tools recovered 2 of 28 ground-truth invariants (FLAMES only); InvCon 0, InvCon+ 0
  • limits: Ground truth is hand-written by the authors after the attack, with the post-mortem in hand, and only for cases they could solve; the 28 are the ones that worked out of 359 Ethereum exploits. Benchmark and tool are available only on request. Matching an invariant to ground truth was done by checking whether it appears in tool output.
  • how much was read: most of it read
  • source; notes: Smart Contract Invariants Protect Against Cybercriminals (2026)
  • record id: invarianteval-2026
• INVWEAVER (2026)
  • title: INVWEAVER: Deductive Feedback for Invariant Synthesis in Interacting-Loop Programs
  • what: Presents INVWEAVER, a neuro-symbolic loop-invariant synthesizer for nested and sequential loops. A loop-level call graph exposes dependencies; obligation-guided LLM prompts and WP-derived targets drive iterative repair with delayed filtering. Defines state-transition and verification-dependency edges in the LCG, top-down/boundary-inward scheduling, failure diagnosis scopes, and a cycle-length delayed-filtering rule. Bubble-sort case derives missing inner invariants from outer WP obligations. Evaluates 67 prior plus 85 CLRS-Alg programs, comparing seven systems and ablations.
  • number: 72/82 multi-loop; 68/70 single-loop
  • number: 13 multi-loop instances uniquely solved
  • number: GPT-5.5 ablation full 140 vs no OGI 117 and no WP 110
  • limits: Uses ACSL/Frama-C WP and SMT solvers; dynamic allocation and separation logic are unsupported, making pointer structures difficult. Benchmarks are small and may leak into LLM training; GPT/Qwen/DeepSeek results depend on model and timeouts.
  • how much was read: most of it read
  • record id: invweaver-2026
• LemmaNet (2026)
  • title: Automated Lemma Discovery in Agentic Program Verification
  • what: GPT-5.2 plans reusable helper lemmas from C source, ACSL obligations and Rocq proof states. It adapts them to each obligation and proves them first.
  • number: 298/641 SV-COMP and 66/300 NTP4VC tasks, 364/941 (38.7%, notes’ arithmetic), 10-minute/100-step budget
  • number: 364 total proofs (298 SV-COMP, 66 NTP4VC)
  • number: 26.8% improvement over AutoRocq, 51.7% over Copra
  • number: 78 unique successes; 61/69 helper-lemma proofs use BRIDGE strategy
  • limits: The Linux scheduler/memory, Contiki and X.509 items are single verification conditions, not whole kernels.
  • how much was read: most of it read
  • source; notes: Dafny, C verification, and the specification-intent gap
  • record id: lemmanet-2026
• LLM logical-construct study (2026)
  • title: Beyond Basic Specifications? A Systematic Study of Logical Constructs in LLM-based Specification Generation
  • what: Compares LLM-generated ACSL annotations for 49 C programs, checked with Frama-C, under four settings of allowed constructs: basic, proved lemmas, axioms, and all. Failing annotations are fixed by deleting or modifying them.
  • number: 49 programs, 5 runs each; stable = at least 2 of 5
  • number: GPT-5 NVP/stable: deletion basic 32/28, full 40/39; modification basic 39/37, full 42/41
  • number: Gemini modification verifiable NVP 48, stable 46
  • number: modification raises runtime generally over 100%
  • limits: The annotations come from the code, not from requirements. Axioms are assumed true and can make the proof unsound, and nothing audits them. NVP counts a program as solved if any run solved it, not pass@1 (success on the first try).
  • how much was read: most of it read
  • source; notes: Beyond Basic Specifications? A Systematic Study of Logical Constructs
  • record id: llm-logical-construct-study-2026
• LORIS loop invariant synthesis (2026)
  • title: Guiding LLM-based Loop Invariant Synthesis via Feedback on Local Reasoning Errors
  • what: LORIS iteratively synthesizes C loop invariants: an LLM proposes an invariant, writes a natural-language proof of failed verification conditions, another LLM translates local steps into first-order implications, and Z3 checks those implications to produce targeted feedback. The framework checks local reasoning steps rather than demanding a fully formal proof script, maps an invalid implication back to a specific natural-language error, and feeds that diagnosis into subsequent invariant synthesis. It integrates Frama-C for inductiveness, Z3 for implication validity, and evaluates multiple model families against LaM4Inv and Clause2Inv, including a BMC combination study and manual auto-formalization checks.
  • number: GPT-4.1 LORIS solves 445/460 main programs with 93.1% success, versus 84.6% and 84.9% baseline success rates
  • number: best reported non-linear result is 47/50 programs; GPT-4.1 LORIS solves 45/50 at 83.2% success
  • number: five runs produce 2,300 attempts on the main suite; per-run cap is 150,000 tokens and 600 seconds
  • number: successful GPT-4.1 run costs about $0.038 on average; sampled auto-formalization evaluates 108 proof steps
  • limits: Results use single-loop, single-function C programs filtered from established suites; floating-point cases unsupported by the chosen Frama-C version were removed. Each method receives five independent runs, a 600-second limit, and 150,000 tokens per run; success means the verifier accepts the generated invariant. Feedback quality depends on LLM formalization of reasoning steps and solver-supported first-order implications, so it does not establish correctness of arbitrary natural-language reasoning outside the checked obligations.
  • how much was read: most of it read
  • source; notes: LORIS, loop invariants from local-reasoning feedback (2026)
  • record id: loris-loop-invariant-synthesis-2026
• MALICE: Memory-aware Loop Invariants Generation on Symbolic Execution Traces (2026)
  • what: A proposal-and-check framework generates separation-logic loop invariants for C memory-manipulating programs from bounded symbolic execution traces. Three prediction stages choose heap predicates, abstract spatial memory regions and infer pure constraints; a two-step explanation/correction refinement loop uses QCP feedback. Authors report82.69% ICL and86.15% SFT pass@8 on260 LIG-MM+ programs. Separates read/write-permission and region planning from heap abstraction and scalar constraints. Two alternative spatial strategies either fold one deeper unrolled assertion or align multiple states to infer a common predicate shape; the reported solved set is their union. QCP supplies detailed pre-failure states, error locations and symbolic histories. A postorder loop-dependency traversal resolves sequential loops in order and inner loops before outer ones. Successful refinement trajectories yield9698 explanation/correction examples for an8B LoRA refiner with program-grouped fivefold cross-validation. A long array_max example reveals the exact memory-safety specification and both useful trace information and limits of automated diagnosis.
  • limits: Correctness relies on QCP semantics, symbolic execution, entailment checking and supplied predicate/specification definitions. The paper invokes standard partial-correctness Hoare rules; no new soundness/completeness theorem, termination proof or successful-generation guarantee is supplied. Unrolling depth4 provides examples for proposing invariants, not a proof of induction over unbounded executions. Pure properties retained after all observed branch-specific states must still pass full QCP initialization, preservation and exit obligations. The method assumes annotated C tasks, pre/postconditions and a supplied library of separation-logic predicates such as data_at,listrep,lseg,array shapes. It selects/folds these predicates; it does not generally synthesize arbitrary recursive predicate definitions or discover intended requirements. LIG-MM+ has133 doubly-linked-list,96 singly-linked-list,8 array and23 other(tree/hash-table) programs,260 total,reported average35 lines. At least one loop and data structure per task; authors mention several two-loop cases but give no count or broad nested-loop stress test. Main pass@8 result takes the union of solved sets from two spatial strategies, with three prediction interactions and up to10 refinement iterations per run. The relationship between strategy union and the stated call budget is not fully specified; token/cost/latency equivalence across methods is not established. SFT changes the refiner to Llama3.1-8B but retains DeepSeek-V3.2 for prediction. Full-8B uses Qwen3-8B prediction plus distilled Llama refiner; inference uses only8B models, while training-data generation still used the large teacher. Fivefold splitting groups all trajectories from each program, preventing direct trajectory sharing across train/test folds. The paper does not establish project/family-level disjointness, deduplication of near-identical programs or absence of base-model contamination. AutoSpec is a numerical tool and obtains0 here; LIG-SE/SLING lack array support. The comparison measures tool applicability plus invariant generation on this benchmark; it does not isolate framework effects under identical models/predicate coverage. Same-backbone Vanilla and Full-8B/budget comparisons add narrower controls. No repeated-run confidence intervals, significance tests, total API costs, full per-category results or independent artifact replay are supplied. Broad deployment to larger C systems, concurrency, distributed protocols, Verus/Rust and temporal liveness is untested.
  • how much was read: most of it read
  • record id: malice-memory-aware-loop-2026
• NetNomos (2026)
  • title: Making Logic a First-Class Citizen in Generative ML for Networking
  • what: NetNomos learns logical rules that fit network traces, using a minimal-hitting-set encoding. It filters them with GPT-4.1 and retrieval. It then uses them to constrain a generative model.
  • number: over 75% reference coverage within 12 hours vs DuoAI under 60% at 24 hours
  • number: 1.6-6.5x scalability gain
  • number: GPT-4.1 with retrieval precision at least 98.1%, false positives at most 0.73%, vs 82.5%/9.2% without
  • number: generated data violates 0.3% of learned rules on MAWI
  • limits: The rules are only consistent with a finite dataset. It has no protocol liveness result and no theorem about an implementation. Human hours are not stated.
  • how much was read: most of it read
  • source; notes: Making Logic a First-Class Citizen in Generative ML for Networking (Ne; notes: Making Logic a First-Class Citizen in Generative ML for Networking (Ne
  • record id: netnomos-2026
• Occupation invariants probabilistic loops (2026)
  • title: Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops (Extended Version)
  • what: Introduces occupation invariants, dual to probabilistic martingales, for exact posterior distributions and positive almost-sure termination, with template-based synthesis of rational generating functions. The paper proves semantic equivalence between posterior-measure and operational Markov-chain semantics, relates occupation measures to expected runtime, gives a proof rule for exact posterior measures, and implements ProDiGy with breadth-first rational templates, symbolic backends GiNaC/SymPy, and positivity heuristics.
  • number: most successful benchmark synthesis times are below one second
  • number: thirds_geometric takes 6.681842 s; subdist_enter 0.568013 s
  • number: nontermination and sequential_loops fail
  • number: runs use Apple M3 Pro with 18 GB RAM; core synthesis only
  • limits: Template enumeration is theoretically exhaustive only if a rational invariant exists at finite degree; positivity checking uses sufficient heuristics because general rational FPS nonnegativity is difficult. Benchmarks are small to mid-sized, and two cases fail due to template/positivity limitations; reported times exclude preprocessing.
  • how much was read: most of it read
  • record id: occupation-invariants-probabilistic-loops-2026
• Quokka (2026)
  • title: Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis
  • what: Quokka directly validates LLM-generated loop invariants and retains only invariants that help a verifier prove assertions, avoiding unsound dynamic-analysis labels or heavy symbolic post-processing. The benchmark filters 866 SV-COMP loop problems and trains on 3,589 synthetic instances. UAutomizer is the baseline; end-to-end time includes inference. Quokka analyzes timeout failures: many outputs duplicate assertions, are trivial bounds, or are correct but too weak. LoRA fine-tuning and Best-of-N improve performance, while comparisons show gains over LEMUR, Clause2Inv, LaM4Inv and Loopy.
  • number: gpt-5.2: 710 verified invariants, 681 solved at 60 s, average 22.2 s; 710 solved at 500 s
  • number: claude-opus-4.5: 689 verified, 659 solved/24.2 s at 60 s
  • number: Qwen2.5-7B fine-tuning: 419→431 verified; additional solved 5→7
  • number: 50 timeout cases: 14% incorrect, 38% assertion duplicates, 18% trivial, 10% strong but timed out
  • limits: Correctness is defined by solver acceptance within 1.2× baseline timeout; acceleration is solver/tool dependent. Most failures are timeouts, and generated invariants may be tautological or too weak. Benchmark programs are SV-COMP C tasks; results may not transfer to other languages or verifiers.
  • how much was read: most of it read
  • record id: quokka-2026
• Scimitar proof decomposition (2026)
  • title: Interactive Safety Verification of Distributed Protocols by Inductive Proof Decomposition
  • what: Introduces inductive proof decomposition and the Scimitar tool for interactively constructing compositional safety proofs. An inductive proof graph decomposes lemmas by protocol actions; counterexample traces are localized and variable slicing hides irrelevant state. Scimitar combines TLC and Apalache to generate counterexamples to inductive proof obligations and TLAPS to validate final proof graphs. The user works backward from a target property, adding support edges and local lemmas; static slicing presents only variables relevant to each node. Five TLA+ protocols were proved, including industrial-scale AsyncRaft with asynchronous messaging and fine-grained local state. The authors report the first invariant effort at that Raft complexity and inspect proof-graph structure as a correctness insight.
  • number: 5 protocol specifications
  • number: AsyncRaft: 12 variables, 11 actions, 638 spec LOC/920 proof LOC, 39 lemmas, median slice 5 variables (0.42)
  • number: AsyncRaft inductive invariant developed in approximately 3 human-weeks
  • number: Other reported proof-development burdens: 1–2 human-months for smaller invariants
  • limits: TLC/Apalache counterexamples use finite parameter bounds and do not themselves prove arbitrary-size invariants; TLAPS validation is required for the final proof. Human guidance remains necessary to add lemmas and edges. Evaluation is on five TLA+ specifications and one implementation; generality to other formalisms is untested. AsyncRaft development took human effort despite automation.
  • how much was read: most of it read
  • source; notes: Scimitar: distinguish the final interactive paper from an older automa; notes: Full live Scimitar configuration inventory (not an evaluated success l
  • record id: scimitar-proof-decomposition-2026
• Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy (2026)
  • what: Proves consensus safety of first-order Paxos-family models and an abstract Raft model. Combines forward reasoning, backward reasoning and prophecy (a recorded guess about the future). Checked with mypyvy and Z3. All proofs were written by hand.
  • number: Table 1: 13 model variants, median of 15 runs
  • number: Paxos value-only: Q=4, A=1, B=5 and 0.59 s to universal clauses and 0.43 s
  • number: Fast Paxos value-only: Q=5, A=1, B=7, 1.5 s to 0.8 s
  • number: Raft: Q=7, A=2, B=9, 3.7 s to 2.8 s
  • limits: Safety only, on abstract models. No implementation or progress result. Human effort and lines of code are not reported. No measured rate of successful proof generation.
  • how much was read: most of it read
  • source; notes: Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
  • record id: simplifying-safety-proofs-with-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
• Timers (2026)
  • title: Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings
  • what: Turns a claim about time into a termination problem by adding timers that predict when formulas become true. A human supplies the model, the claim, the implicit ranking, the invariant and finite-set approximations. Z3 checks the generated conditions.
  • number: 17 tasks in Table 2, e.g. Ticket: 2 s, 20 invariant conjuncts, 256 proof tokens
  • number: Paxos: 101 s, 238 tokens; ABP: 4 s, 539 tokens; HRB-Correct: 135 s, 99 tokens; Dijkstra k-State: 64.8 s, 213 tokens
  • number: Ivy proof sizes for six tasks: 407, 521, 860, 446, 593, 748 tokens (Ticket, Paxos, ABP, HRB-Correct, HRB-Relay, Ackermann)
  • number: runtime is Z3 validation on Apple M1 Pro, Z3 4.13.3
  • limits: The guarantees cover first-order transition-system models, not deployed code. Rankings and invariants are not discovered automatically. Sizes count proof tokens, not human effort.
  • how much was read: most of it read
  • source; notes: Verifying First-Order Temporal Properties of Infinite-State Systems vi
  • record id: timers-2026
• Transitive Relation Learning (TRL) (2026)
  • title: Infinite State Model Checking by Learning Transitive Relations
  • what: Transitive Relation Learning (TRL) extends bounded model checking with learned transitive relations and blocking clauses so that finite-depth search exhaustion can prove safety of an infinite-state transition system. Uses model-driven conjunctive variable projection to select transition cases, recurrence-based transitive projections, loop detection, redundancy checks and backtracking. Learned relations need not over- or under-approximate a loop’s full transitive closure. Soundness instead depends on blocking only paths covered by the learned relations. Section 5 recursively substitutes accelerated under-approximations to validate possible counterexamples. Appendix A proves Theorems 22 and 28.
  • number: 626 unique LIA-Lin CHC competition 2023/2024 problems, 300 s and 10560 MiB each. TRL solves 386 (267 safe/119 unsafe), GSpacer 373 (287/86), ABMC 272 (142/130). Unique-proof counts depend on which overlapping solver configurations are excluded.
  • limits: May diverge; finite-image projection does not ensure complete loop closure. Implementation is limited to linear integer arithmetic; reals, arrays, bitvectors and temporal verification are future work. Main algorithm can return unknown when an error is reachable only through learned transitions. Author empirical and proof claims were read but neither code execution nor machine-checked proof was performed.
  • how much was read: most of it read
  • record id: transitive-relation-learning-trl-2026
• WONDA invariant curation (2026)
  • title: Not All Invariants Are Equal: Curating Training Data to Accelerate Program Verification with SLMs
  • what: Introduces WONDA, a verifier-filtered training-data pipeline: AST normalization removes semantic-preserving syntactic clutter, then an LLM proposes compact generalizations that are checked for inductiveness, sufficiency and speedup. Proposition 4.1 proves normalization equivalence and Proposition 4.3 proves pipeline outputs are correct and sufficient. Fine-tuning Qwen3, Llama-3.1 and Mistral SLMs on curated invariants improves correctness and virtual-best verification time versus raw or normalized data.
  • limits: Raw invariants come from UAutomizer and are correct by construction but may be verbose or not useful. LLM simplification is not semantics-preserving by assumption; every candidate is re-verified. Cast stripping can be unsound under overflow, so final verifier checks are essential. Evaluation is C programs/InvBench (219 programs expanded to 362 loops), with 123 hard instances selected by >15 s baseline and 20 hard timeouts; results measure verifier outcomes, not proof certificates. 80/20 training/validation split is by curated samples; the paper does not state program-group splitting, although multiple candidates may derive from one program. Evaluation contains multiple loop instances per program, so 123 instances are 72 unique hard programs (mean 63.9 LOC, 8.1 variables; 28 with nonlinear arithmetic). Claims of matching frontier models concern virtual-best end-to-end time, not equal correctness: Qwen3-14B-V2 correctness 43.4% versus GPT-5.2 72.4%. Training is one-shot supervised invariant generation; no intermediate reasoning or iterative verifier feedback is used.
  • how much was read: most of it read
  • record id: wonda-invariant-curation-2026
• 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
• b-invariant regular model checking (2025)
  • title: Regular Model Checking Upside-Down: An Invariant-Based Approach
  • what: Reverses regular model checking direction: intersects all inductive b-invariants represented by CNF formulas with at most b clauses, obtaining regular over-approximations converging to reachability. Defines regular transition systems with finite-word configurations and length-preserving transducers, then constructs automata for IndInv_b. For every b, unsafe-intersection emptiness is in EXPSPACE; b=1 has an exponential NFA and PSPACE-completeness. The proof uses tables/separation languages and a reduction from polynomial-space Turing machines. MONA experiments compute minimal DFAs for IndInv_1 across classic parameterized protocols and inspect cases needing b>1.
  • number: IndInv_1 proves 46/59 benchmark properties
  • number: minimal DFA and MONA times range <1 ms to 1920 ms
  • number: b=1 PSPACE-complete; every b EXPSPACE upper bound
  • number: dining philosophers with fork ownership needs b=1; unlabelled forks require b=3
  • limits: Only length-preserving finite-state transducer transitions and regular initial/unsafe sets are covered; safety problem for RTS is generally undecidable. EXPSPACE result is an upper bound and authors conjecture EXPSPACE-completeness for b≥2. IndInv_1 can be too coarse (e.g., some mutual exclusion/cache properties), while manual reasoning shows b=2 or b=3 can suffice.
  • how much was read: most of it read
  • source; notes: Regular Model Checking Upside-Down (2025)
  • record id: b-invariant-regular-model-checking-2025
• Basilisk (2025)
  • title: Basilisk: Using Provenance Invariants to Automate Proofs of Undecidable Protocols
  • what: A Dafny-based tool generates history-preserving asynchronous protocol models and mechanically checked provenance, monotonicity and ownership invariants. Atomic sharding traces current local values or collection entries to past steps and messages. Users supply host definitions, selected hints/labels and final safety proofs. Evaluation reports 16 protocol-model proofs, with 10 Kondo comparisons, final proof sizes and verifier times. Reconstructs host/network provenance and the atomic-shard algorithm, collection correlation failure and epoch-reset counterexample. Records formal safety obligations, all 16 protocol properties and every numerical comparison cell. Separates generated invariant proofs from user safety proofs, model correctness from implementation correspondence, and measured final LOC from development effort. Preserves incompleteness, syntax restrictions and all trust limits.
  • number: 16 protocols
  • number: Paxos: 418 lines, 0 user invariants, 486 proof lines, 24.6 s
  • number: Multi-Paxos: 447 lines, 0 user invariants, 565 proof lines, 61.5 s
  • number: Paxos row: 418 model lines, no user invariant clauses, five monotonicity annotations, no provenance hints, 444 safety-lemma lines, 486 total proof lines, 24.6 verification seconds
  • limits: §§3,5.2: Model has arbitrary host counts, nondeterministic single-host atomic steps, history of all Hosts snapshots and a monotonically growing set of sent messages. Receive selects an addressed message already sent; repeat selection and nondelivery overapproximate duplication, delay, reordering and loss. Messages carry sender identities; arbitrary Byzantine forgery or compromised hosts are not modeled. History is proof state, not a measured runtime logging cost. §3: Network provenance links a sent message to an adjacent pair of historical sender states and a matching send step. Host provenance for witness q requires q now, no initial state satisfying q, and a historical crossing from not-q to q through a candidate modifying step. These statements concern well-formed initialized protocol executions, not arbitrary malformed history sequences. §§3.3,5.3: Provenance alone identifies a past producing event. Monotonicity/non-equivocation invariants are needed to move from past sender conditions to present facts. Ownership invariants/labels are inherited from Kondo; generated invariants are individually/local mechanically checked, not assertions trusted merely because the generator produced them. §4.1: An atomic shard is a subset of local variables always modified together. If the current tuple is not an admissible initial tuple, it was established in one candidate update step. Maximal shards retain shared-message correlations lost by independent singleton witnesses. This does not mean every member of a collection remains correlated with the latest scalar value. §4.2: Static footprints overapproximate variables a step may update; excess candidates weaken the resulting provenance disjunction. Underestimating footprints would produce incorrect invariants. Prototype rejects a step updating different variables under different conditions, e.g. if c then x:=5 else y:=6. User must split this into separately guarded steps. §§4.2,5.3: Collection fields also receive refined singleton shards, allowing each noninitial set/map entry to be traced to its insertion step. Prototype supports explicit Dafny record-update syntax only, rather than general relational updates. A step can receive and send together; multiple sends/broadcasts in one step are described as an easy extension but not implemented or evaluated. §5.4 reader qualification: Formal obligations are Init⇒I∧φ and I∧φ∧Next⇒I′∧φ′. Thus the actual method proves safety with induction on I∧φ and may use current φ in the step proof. Figure 5/prose describing a proof that I implies safety must not be read as requiring or establishing the stronger standalone I⇒φ in every example. The final safety proof remains user-written. §§5.4,6.4: Failure may reflect a too-weak generated invariant or an unsafe model; the verifier points to the failing host-step obligation, but does not automatically decide which explanation is true. Reader qualification: SMT proof failure can also arise from solver incompleteness. Additional provenance witnesses or manually written invariant clauses may be needed; Basilisk is explicitly incomplete for undecidable logics. §6: First six protocols were used to develop/refine provenance and atomic sharding; the remaining ten were applied later. All sixteen models/invariants are reported outside EPR. This is an author-built benchmark suite, not a blinded independent user study or proof of completeness for all protocols outside EPR. §§6.1–6.2: Zero manually supplied invariant clauses across 16 does not mean zero user reasoning. Six of 64 host-provenance invariants need explicit witness hints, across Paxos-Dynamic, Raft election and Multi-Paxos; monotonicity annotations, ownership labels and safety lemmas remain. Distributed Lock and both ShardedKV variants already had fully automatic Kondo ownership proofs. §6.2: Kondo comparisons cover only ten protocols and modify models to split receive/send; Kondo also needs synchronous protocol definitions. Final proof LOC excludes failed/revised proof attempts and does not measure person-time, cognitive difficulty or novice success. Basilisk uses more proof LOC for some simple cases and is not faster for every ownership example. §6.3: Timings check final history-preserving asynchronous proofs including generated/user invariants and lemmas; Kondo synchronous-proof verification is excluded. Invariant generation is under two seconds in every case. Table 1 reports Multi-Paxos 61.5 seconds; the prose phrase in a minute is approximate, not a strict sub-60-second bound. No repetitions/variance or controlled proof-authoring experiment is reported. §6.4: Epoch resets create implicit multi-step relations that sharding cannot infer. Adding an event at current year and clearing events on year increment requires a witness relating every current entry to current year; merely finding its historic insertion year is too weak. All three hinted benchmark protocols have collection resets at epoch changes. Footprint imprecision is another possible weakness, not observed by authors in these protocols. §6.4: Safety specification is trusted. The user must trust the model describes actual code or separately prove correspondence; this work does not verify production implementations. Dafny, dependencies and hardware are trusted. Crash-fault safety is the scope; no liveness or Byzantine correctness proof is provided. §§6–8,Appendix A: No runtime throughput, production bug-finding or LLM-agent experiment is evaluated. Artifact developed/tested on M3 MacBook Pro with MacOS Sequoia; this appendix statement is not an explicit platform declaration for every published timing. Artifact and external proof bodies were not executed in this reading.
  • how much was read: most of it read
  • source
  • record id: basilisk-2025
• Compositional Inductive Invariant Inference via Assume-Guarantee Reasoning (2025)
  • what: This work splits a TLA+ protocol into components with assume-guarantee contracts (each component assumes something of the others and guarantees something in return). It uses Endive to search for local inductive invariants. It then proves safety with TLAPS for arbitrary instances.
  • number: two-phase commit: global search 34.82 s, 107 proof steps; local searches 15.44/30.43/6.13 s
  • number: Mongo Static Raft: global search fails, manual 17-conjunct invariant, 1686 proof steps; local proofs total 372 steps, only one of three local searches succeeds
  • number: Two-phase commit: global search 34.82 s, 10 conjuncts, 107 proof steps; components 15.44/30.43/6.13 s
  • number: Mongo Static Raft: global search fails; manual 17-conjunct invariant, 1686 proof steps; components total 372 proof steps but only one of three searches succeeds automatically
  • limits: Humans split up the spec and write all the contracts. It proves safety only. It uses abstract TLA+, not the MongoDB code. The authors did not measure effort.
  • how much was read: most of it read
  • source; notes: Compositional Inductive Invariant Inference via Assume-Guarantee Reaso; notes: Compositional Inductive Invariant Inference via Assume-Guarantee Reaso
  • record id: compositional-inductive-invariant-inference-2025
• DAISY (2025)
  • title: Inferring multiple helper Dafny assertions with LLMs
  • what: GPT-4.1 with heuristics over error messages finds where to insert missing helper assertions in verified Dafny programs taken from DafnyBench. Dafny and the Z3 solver then check the candidates.
  • number: Table 3: w/o-one 153 (63.4%), w/o-two 76 (32.3%), w/o-all 8 (26.7%), combined 237 (46.8%)
  • number: dataset 241 w/o-1, 235 w/o-2, 30 w/o-all instances
  • number: default two insertion sites, ten candidates per site
  • limits: The specs already exist. It excludes cases where removing an assertion still verifies. Faria et al. misquote single-assertion success as 63.2%.
  • how much was read: most of it read
  • source; notes: Inferring multiple helper Dafny assertions with LLMs (DAISY)
  • record id: daisy-2025
• Deriving Semantic Checkers from Tests to Detect Silent Failures in Production Distributed Systems (2025)
  • what: T2C transforms existing distributed-system tests into runtime semantic checkers. It slices assertions into parameterized functions, obtains symbolic triggering histories and constraints from instrumented test execution, mutates these histories, then filters candidates by compilation, JVM verification, self-validation and cross-validation. A production monitor matches traces and invokes checkers. The paper measures checker generation, detection after known failures are triggered, false alarms and performance; it does not prove transformation or checker soundness. Records exact extraction/precondition/mutation mechanisms, observational filtering and unsoundness, four validation levels, trace matching and distributed adapters, all study and generation counts, all twenty failure outcomes/times and issue identities, manual integration effort, false alarm denominators/counts, full cost tables, missed cases and newly added HB2 test, and a distinct newly reported ZooKeeper defect.
  • limits: §§2–3,8: Existing assertions encode useful intended semantics, and test-derived checks generalize beyond their original inputs/configurations. This is an explicit empirical assumption, not established for every test. The study randomly samples 35 tests per system, 210 total; subsequent percentages use only 183 assertion-bearing tests. Equal per-system sampling does not estimate the pooled distribution of all tests by test-count weight. §4.1: Backward data/control slicing preserves relevant branches, explicit aliases, local computations and assertion dependencies. It stops at operations classified as side-effecting by purity analysis plus manually supplied exclusions. No soundness guarantee; missed effects can survive. Section 4.1 says validation exposes missed operations, whereas §8 expressly denies a full guarantee of freedom from side effects. No formal refinement between a test and generated checker is established. §§4.2–4.3: Trigger preconditions are observed server-side call sequences before assertions, excluding operations performed by the checker itself. They are not Hoare-logic weakest preconditions. Analysis depends on chosen instrumentation, recorded execution, API wrappers and manual parsing/adapters. Unobserved paths and system configurations may affect applicability. Enum arguments remain concrete by default. §4.2.2: Equality of observed constants yields shared symbols; accidental equality can over-constrain and suppress checker activation. Simple less-than/contains constraints supported, arbitrary semantic relationships not inferred. Missing complex constraints or broad mutation can over-generalize and cause false alarms. Reduce/insert-wildcard/duplicate/reorder mutations are bounded enumeration; bounds, completeness and global coverage are not established. §4.4: The paper calls 672 outputs verified, meaning they passed empirical/syntactic filters: compilation, JVM sanity checks, rerunning source tests with the checker, then other passing-test workloads. Neither JVM verification nor passing tests proves semantic validity, absence of false positives, complete detection or freedom from side effects. Cross-validation assumes passing-test executions are suitable nonfailure examples; unexpected alerts could also expose real defects, a reader inference not systematically studied here. §5: Circular-buffer trace expiry bounds memory but can discard needed history; precise buffer capacity and complete-coverage guarantee are not given. Reversed precondition trie matches current trace suffix. Configuration requirements checked at startup, with no general claim of adaptation to later configuration changes. Instrumentation, runtime matcher, target methods queried, assertions, adapters, Java/Soot/Javassist and trace transport are trusted operational components. §5: Multiple clients may collectively supply a trigger sequence; cluster mode forwards traces and invokes assertions on respective nodes via RPC. No theorem establishing causal ordering, globally consistent observation, race-free semantic checking across arbitrary interleavings or distributed snapshot correctness. The runtime architecture avoids worker/evaluator buffer races according to authors; that claim is narrower than distributed checker soundness. Special concurrency properties still need carefully designed checks. §§6–7: Implementation is Java only; C/C++ port through LLVM is proposed, not evaluated. Setup includes core classes, about six unsafe operations and about three utility-adapter classes per system, beyond 42-line average configuration. HBase integration one person-week. Claims of little manual effort concern this measured support, not zero domain knowledge. §7.2: Tests selected by system-test package groups, excluding low-level data structure tests and assertion-free performance/stress tests. Target-test denominator 2172, generated functions for 2019, healthy 1933 and final 672. Final outputs cover available test semantics only. Section 4.1 describes one checker per assertion while §7.2 reports 4.3 assertions per checker; paper does not reconcile granularity, so both statements retained. §7.3: Benchmark construction starts with keyword-filtered issues, then 56 randomly inspected, 24 qualifying silent failures and 20 reproducible cases; four lack reproduction information. Reported 15/20 detection is conditional on failures already triggered, not a bug-triggering success rate or representative prevalence estimate. Reproduction takes about one week per case. Generation excludes tests reproducing benchmark failures, but baseline event checkers use historical failure examples; no universal equivalence of training information is claimed. §7.3: Missed five cases include absent semantic coverage and poor/non-generalizable assertions. HB2 only becomes detected after authors add a new test; this does not change original 15/20 result. New ZooKeeper 3.9.2 bug is a separate fault-injection finding, not an additional benchmark hit. Source calls version latest at publication; no current-version claim. §7.4: False alarm ratios use checker invocations in failure-free scenarios over 30 minutes, with Jepsen network faults every 10s. They are not alarms per hour or precision among alerts, and do not estimate arbitrary production workloads. 56% average checker activation leaves many checkers unexercised. No repetitions, confidence intervals or broad deployment duration reported. No noticeable harmful checker effects observed is empirical, not a safety theorem. §7.5: Four benchmark workloads give throughput losses 1.4/9.1/3.8/1.5%, mean 3.95% rounded 4.0. Low activation contributes to low overhead and also limits exercised semantics. No universal cost bound or worst-case under high checker activation. CPU percentages sum across cores; increases must not be read as fractions of a single total CPU. Offline build/validation take hours despite slicing taking minutes. Tables1–2: Same-version study/generation test counts differ (ZooKeeper 434 vs428, Cassandra 4118 vs3283, HDFS 3265 vs4304), without reconciliation. Table1 prints CephFS 1.11.0 and Mesos 18.2.0; preserved as printed rather than silently correcting versions. These are source discrepancies/labels, not independently checked software inventories. §8: LLM-assisted analysis, sandboxing and formal verification of generated checkers are future work. Paper evaluates no Verus, verified Rust, TLA+ or LLM-written proof system, and establishes no universal distributed-system correctness theorem.
  • how much was read: most of it read
  • source
  • record id: deriving-semantic-checkers-from-2025
• FORCE (2025)
  • title: Inductive First-Order Formula Synthesis by ASP: A Case Study in Invariant Inference
  • what: FORCE uses answer-set programming to list first-order formulas that are consistent with supplied traces, and to prune them. It plugs into DuoAI and Flyvy, which check that candidates are inductive.
  • number: times: sharded KV 0.17 s, toy consensus 0.31, Paxos 20.4, Flexible Paxos 56.3, Multi-Paxos 81.5
  • number: without quantifier restriction Multi-Paxos 842 s
  • number: about 13% smaller invariants for Paxos and 7% for Flexible Paxos
  • number: code: 250 ASP, 80 pruning, 400 C++, 200 integration lines
  • limits: The evaluation configuration contains the desired invariant. It has no liveness and no code refinement. Flyvy’s runtime did not improve notably.
  • how much was read: most of it read
  • source; notes: FORCE: Inductive First-Order Formula Synthesis by ASP: A Case Study in; notes: FORCE: Inductive First-Order Formula Synthesis by ASP: A Case Study in
  • record id: force-2025
• Formal Verification of Parameterized Systems based on Induction (2025)
  • what: # Formal Verification of Parameterized Systems based on Induction (authored by agents unless marked 🧑) Jiaqi Xiu and Yongjian Li, arXiv 2503.18030v1, 23 March 2025. This is a whole-paper record: all nine PDF pages, 23 references, two figures, four algorithms, nine numbered equations and both tables were read. All pages were visually inspected, including six dense pages at 1900px. No appendix or checklist appears. The acquired official PDF and pool copy are byte-identical. quotes.json supplies exact passages with section/page pointers; tables.json preserves the complete table pages, and the two row sidecars transcribe all cells. Cited papers were not independently read for this assignment. The paper presents wiseParaverifier, a system for discovering and generalizing auxiliary invariants of parameterized safety protocols. Its main contribution is a search procedure: use small protocol instances and counterexamples to suggest invariants, select quantifiers, merge related formulas, and ask Ivy to prove the parameterized result. It reports success on seven cache-coherence and ten distributed protocol models. The evidence is an algorithm description and benchmark measurements. The paper contains no numbered theorem, lemma or complete end-to-end soundness, completeness or termination proof. I did not run a solver, checker or author program, and acquired no generated proof files or verification logs. Section I p1 states the central limitation of starting small: an invariant’s inductiveness on a small instance “does not imply that these invariants will retain their inductive characteristics when applied to larger scale system concretizations” (Q1). The workflow addresses that gap with two stages. invFinder constructs concrete auxiliary invariants; Verifier generalizes them and checks induction (§III p2, Q2). Figure 1 p3 adds an essential detail: a successful Ivy proof yields “Passed”; a failed proof increases N and returns to invariant discovery. Thus the intended acceptance condition is parameterized induction, not agreement at two finite instance sizes. The paper says, “wiseParaverifier employs Ivy for automatic inductive verification” (§III.C p5, Q15). No acquired artifact lets this reading independently check that step. The initial concretization is based on overlap between parameters in an invariant F and transition rule R (§III.A.1 pp2–3). With two invariant parameters and one rule parameter, the rule may use either existing index or a fresh third index, so N=3 represents the listed overlap cases. With two rule parameters, representatives can require N=4, including the all-fresh pair. These are concrete examples of reducing redundant parameter instantiations. The stated selection principle requires the concrete protocol to simulate the same or symmetric transition behavior under arbitrary parameters (Q4). The article does not prove a general cutoff theorem or define a complete supported protocol language that makes that principle automatic. For each rule/invariant pair, the system constructs indOblg, a formula involving the rule guard, assignments, unchanged-variable equations and a violated postcondition (§III.A.2 p3, Eq1). Z3 satisfiability produces an assignment used to propose an auxiliary invariant by negating the conjunction of its state equations; unsatisfiability eliminates that obligation (Q7–Q10). Rules that do not change relevant invariant variables can be filtered. Candidate invariants are checked through a client/server service wrapping Murphi, NuSMV and NuSMV-BMC (§III.A p2, Q3). The server retains information about previously executed protocols, a detail relevant to interpreting timings (§IV p7, Q24). The heuristic Generalize search uses earlier invariants to narrow which equations matter (§III.A.3 pp4–5, Figure 2 and Algorithms 1–2). Shared terms form join; terms unique to the current counterexample form diff. It tests join plus increasingly large subsets of diff, then removes unnecessary terms or uses an increasing search to obtain a smaller checked candidate. It falls back to nonheuristic search if that fails (Q11–Q14). This is a useful concrete distinction: previous formulas guide candidate generation, while an external checker checks candidates against the concrete model. Although the paper repeatedly calls the result “most concise,” it gives no global minimality proof or formula-length/readability evaluation. Quantifier promotion uses type saturation γ(t)=#(Ω,t)/C(t), the number of concrete values of type t in a clause divided by that type’s concrete domain size (§III.C p5, Eq3). An unsaturated type is proposed as universally quantified. A saturated type triggers a check at N+1; a surviving clause can receive universal quantification, while failure prompts existential or finer mixed grouping. Equations 4–7 describe extending groupings and expressing existential alternatives. The following page says existentially treated groups may be joined by disjunction (Q16–Q20). These tests generate candidate quantifiers. They do not by themselves establish correctness at every size; the final Ivy induction check in Figure 1 remains necessary. The merger has three distinct cases (§III.C p6, Q21). Equivalent parameterizations share a representative. If one existing invariant implies the whole conjunction, Eq8 permits retaining it. Eq9 permits a strictly stronger replacement that implies the old conjunction while the converse fails. A stronger formula still needs an invariant proof: implication alone does not establish that initial states satisfy it or that transitions preserve it. Algorithms 3–4 add another optimization, generating symmetric formulas and asserting already accepted auxiliary invariants and their images to prevent redundant counterexamples. The paper distinguishes unrestricted universal-type permutations from restricted existential and mixed cases (Q22–Q23); a transfer must preserve those quantifier distinctions and the modeled protocol’s symmetry. Several printed details limit treating this presentation as a fully specified formal argument. Eq2 p3 writes f_k = eq_i ∨ ¬eq_i. Read literally as logical disjunction, each factor is a tautology and its negated conjunction is false. That conflicts with the surrounding candidate-invariant explanation; a notation or presentation error is plausible, but its intended repair was not established. Eq1 does not explicitly include a prestate F conjunct, so this record does not silently substitute the conventional F ∧ R ∧ ¬F′ formula. Algorithm 1 p4 line12 shows a function index without recursive arguments, and line24 converts solution while iterating over subS. These details were visually checked. They are unresolved presentation issues, not an independently demonstrated failure of an implemented verifier. reader-diagnostics.json separates these observations from the authors’ claims. The evaluation has a 17-model comparison and a four-strategy ablation (§IV pp7–9). The cache models are MutualExNodata, MutualEx, MutualEx_M2, GermanNodata, German, FlashNodata and Flash. The distributed models are Decentralized_lock, Lock_server, Multi_lock_server, Ricart-Agrawala, Shard, Two_phase_commit, two client/server variants and two consensus variants. Four distributed rows require mixed universal/existential quantifiers. The paper does not print the benchmark safety formulas, instance sizes, full transition models or failure/network assumptions. Verifying a model named Flash or Consensus_epr therefore supports that model-level claim; it does not establish correctness of a deployed cache implementation or every consensus variant. Experiments used an 18-core Intel Gold 6254 CPU at 3.10GHz. Table I reports completion seconds and final parameterized-invariant counts for wiseParaverifier, Paraverifier, DuoAI and IC3PO. Counting numeric successful entries gives 17, 7, 14 and 12, respectively; these are reader counts. “error” means compilation failed after modeling, while “fail” means verification could not complete (Q25). Neither means a discovered safety violation. The prose says Paraverifier failed on all distributed models (§IV.A p7, Q26), but its Two_phase_commit row succeeds in 6.18 seconds with ten invariants. The table supports one distributed success and nine compilation errors. That conflict is preserved rather than resolved in favor of the prose. The comparative gains vary. Flash takes wiseParaverifier 585.68 seconds and 135 invariants versus Paraverifier’s 589.23 seconds and 162 invariants; DuoAI and IC3PO fail. GermanNodata takes 19.14 seconds/39 invariants versus DuoAI’s 535.80 seconds/892, about 28× less time by reader arithmetic. On Consensus_epr, however, DuoAI takes 28.88 seconds/seven invariants, wiseParaverifier 43.10/16, and IC3PO 1248.26/eight. Coverage and low invariant count therefore do not imply universal speed or concision superiority. Table II compares simple increasing, simple decreasing, heuristic increasing and heuristic decreasing search using seconds and NuSMV calls. They complete 15, 15, 16 and 17 models; “/” denotes more than 86,400 seconds with continuing counterexample discovery. Heuristic decreasing is fastest or tied on 15 rows. For FlashNodata it reduces heuristic increasing’s 1669.69 seconds/1818 calls to 329.91/674. On Consensus_epr, simple increasing takes 183.23 seconds/2909 calls versus 43.10/753. The tradeoff reverses on small Ricart-Agrawala: simple decreasing takes 0.43 seconds/eight calls versus heuristic decreasing’s 0.54/ten. These are author-reported measurements, with no stated repetitions, seeds, variability or error bars. Software versions, memory use and a clear cold/warm-server timing boundary are absent. GermanNodata, Lock_server and Ricart-Agrawala have differing timings across Tables I–II; the row sidecars retain each printed value. Bibliographic provenance also needs care: §II’s “I4 [20]” points to a listed 2003 cache-coherence paper, “Ivy [21]” to Ironfleet, and reference13 retains a literal placeholder venue. This record does not treat those mappings as validated provenance. No author repository, model, log or certificate URL was identified in the paper or acquired arXiv metadata; this was not an exhaustive artifact search. The arXiv TeX and experimental HTML links were not acquired. For distributed-system verification, the paper contributes a practical combination of counterexample formulas, earlier-invariant-guided search, mixed-quantifier proposals and symmetry blocking, evaluated across two protocol categories. It presents no Verus or verified-Rust implementation, TLA+ experiment or LLM-agent study. A reader proposal for agents writing specifications and proofs is to reuse earlier invariant terms as search hints, make quantifier changes explicit, and require an independent parameterized induction check before accepting them. Its measurements suggest evaluating completion coverage, checker calls, runtime and formula size separately, while separating compilation failures, verification failures and timeouts. Those are transfers from the method and evaluation, not capabilities demonstrated for LLM agents by this paper. Whole9pages/23references/2tables/2figures/4algorithms/9equations. Reconstructs overlapcase concretizations, Z3CTIformulas, join/diffheuristic andfallback, type-saturationN+1quantifier proposals, three merging cases, quantifier-aware symmetry blocking and finalIvyfeedbackloop. Alltablecells transcribed, coveragecounted, representative speed/call/invariant tradeoffs and printedformula/pseudocode/citation/table/prose inconsistencies retained.
  • limits: Parameterized protocol safety models and representative overlap/symmetry cases; trustworthy translation and final symbolic Ivy induction. SmallN/N+1checks alone do not prove all sizes. No complete end-to-end soundness/completeness/termination theorem or acquired authorcode/models/logs/certificates.17successesauthorreported; no execution/reproduction. NoVerus/Rust/TLA+/LLMagentstudy.
  • how much was read: most of it read
  • source
  • record id: formal-verification-of-parameterized-2025
• HornStr (2025)
  • title: sfHornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses.
  • what: HornStr synthesizes regular-language inductive invariants for string-theory CHCs using SAT-based DFA learning or L* active learning. Standard SMT-LIB2.6 string solvers check initiation,transition closure and bad-state exclusion; reachability enumeration supports active membership and inductive-counterexample handling. It connects parameterized-protocol regular model checking to existing string solvers and generates string-query benchmarks. Describes restricted unary-predicate problem,learning/refinement flow,DFA-to-regex translation,heuristic reachability cutoff,incremental solver sessions and separate membership/equivalence backend choice. Reports complete query-solver and protocol results,including active-learner timeouts,unlisted hard protocols and prose/table inconsistencies. No general completeness theorem or verified implementation is supplied.
  • number: 18 benchmark protocols (Table 2); SAT-based learner solved all 18, mostly in under a second; MU puzzle 11.01 s with a 3-state automaton
  • number: The active learner timed out on 6 of the 18 (Burns, Mux-Array, Eqdist, MU Puzzle, Water-Jug, Dining-Crypt)
  • number: Z3-noodler solved all 848 non-incremental equivalence queries; cvc5, Z3, Z3-alpha solved 403 to 457
  • number: Generated more than 30000 string constraints (abstract) or more than 10,000 (Sec 5); the paper gives both numbers
  • limits: §2: one unary unknown predicate over strings; sought solutions regular languages. General CHC definition allows more predicates/nonlinearity, but that syntax is not evidence that implemented solver handles all general string CHCs. Symbolic alphabets and broader CHC support deferred in §5. §§2.1–2.2: safety expressed by initial inclusion,transition closure,error exclusion; configurations are modeled words. Correctness of protocol→CHC modeling/automatic translation assumed,not mechanized here. Arbitrary number of processes does not establish real Rust implementation correctness. §2.1: reachable/bad-predecessor languages can be nonregular while a separating inductive invariant is regular. Failure to find a regular invariant need not mean unsafe; no complete procedure for all infinite-state systems. §3: SAT unsat means current DFA size cannot fit examples and triggers larger size; string-query unsat means no violation of the particular checked clause. These are different meanings,not contradictory CHC conclusions. §3: active membership enumerates reachable words and may answer negative after same-length exhaustion or fixed cutoff. Explicit heuristic inspired by length preservation; bounded failure to find a word does not generally prove unreachable in length-changing rewriting. Could impair learning/completeness. Final all-clause validation remains distinct,conditional on solver correctness and handling of unknown/timeouts. §3: DFA→regex uses Brzozowski/McCluskey state elimination; induction counterexamples can be converted to positive/negative via reachability following strict-but-generous teacher. No in-paper full correctness/termination proof,complexity bound,formalized checker or proof-producing string backend. §3/Fig1: learners exchange regex equivalence queries and reachability membership queries through independent interfaces. Each CHC can have dedicated incremental solver thread with push/pop; optional single solver. Trust includes parsers,translation,learners,regex conversion and SMT solvers; artifact not executed. §4.1: query families have unequal counts: incremental523membership/396equivalence versus nonincremental30902/848. Raw aggregate runtimes cannot isolate causal per-query incrementality benefit without matched workloads. Table excludes timeouts from times; lower solved-time can simply reflect fewer solved queries. §4.1: prose calls523membership queries an average109.7s and says other solvers slightly higher runtimes. Table1 labels Time(s),caption solved time;Z3 33.7,cvc5 97.8,Z3-alpha86.4 are lower than109.7. Preserve table and inconsistent prose;109.7s as per-query average would exceed stated30s timeout. No silent correction or invented timing definition. §4.1: visual PDF p.8 confirms disequality x≠c; text extraction drops stroke and yields x=c. Regular-expression simplifier/flags marginal or harmful overall,not robust improvement;no quantitative ablation table. §4.2:18listed protocols all solved by SAT;active12solved/6timeouts. Kanban/German timeout60s in prose but absent from Table2;therefore SAT success on every listed row does not mean all benchmark protocols solved. Full-suite count and which learners timeout on unlisted protocols not supplied. §4/Table2: automaton sizes and learning seconds;no printed invariant automata/independent certificate or unsafe-trace count per row. MU3states/11.01s is reported discovery,not this reader rerunning solver or inspecting artifact invariant. First-solver claim is authors’ claim,not independently established priority. §4:IntelCorei7-10510U1.8GHz/16GB/Windows11.30s query and60s protocol limits;solver revisions,repeat counts/variance,full timeout overhead,independent baseline RMC comparison and frontend correctness unreported here. §§abstract/5:abstract says more than30000newQF_S constraints;conclusion says more than10000. Compatible lower bounds but inconsistent specificity;do not sum query categories as disjoint unique files. Liveness,bisimulation,further CHCs future work. No Verus/Rust/TLA+ or LLM experiments. Full version[30]arXiv2505.15959 and artifact[31]Zenodo15195124 contain deferred detail;not read/executed. This is proceedings-paper read only.
  • how much was read: most of it read
  • source; notes: ## HornStr (2025)
  • record id: hornstr-2025
• HornStr invariant synthesis (2025)
  • title: HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses (Technical Report)
  • what: Introduces HornStr, a solver that casts regular-model-checking invariant synthesis as constrained Horn clauses over SMT-LIB 2.6 strings. It combines SAT-based automata enumeration or active learning with string solvers answering membership and equivalence queries. HornStr parses parameterized protocols and string-rewriting systems into CHCs, uses incremental solver contexts, and supports Z3, Z3-alpha, Z3-noodler, cvc5 and OSTRICH. The evaluation separates string-solver oracle performance from end-to-end invariant learning across distributed protocols, MU and EqDist puzzles, and other benchmarks.
  • number: incremental membership: Z3-noodler solves 523 benchmarks in 109.7 s
  • number: incremental equivalence: Z3-noodler solves 396 queries in 15.5 s
  • number: non-incremental equivalence: Z3-noodler solves 848 queries in 17.9 s
  • number: membership query pool contains 30,902 benchmarks
  • limits: The learner represents invariants as regular constraints over strings and the active learner uses a bounded exploration heuristic for negative membership answers. Solver performance is sensitive to regex equivalence queries and a 30-second per-query timeout; some active-learning protocols hit a 60-second overall timeout. The paper covers safety-style invariant synthesis and leaves general CHCs, liveness and bisimulation for future work.
  • how much was read: most of it read
  • record id: hornstr-invariant-synthesis-2025
• Implicit rankings (2025)
  • title: Implicit Rankings for Verifying Liveness Properties in First-Order Logic.
  • what: The method compares old and new states through formulas, instead of computing a number that must shrink (a ranking function). Constructors combine them pointwise, lexicographically, by multiset or permutation, and across a whole domain. Z3 checks the conditions that result. It verifies toy stabilization, a binary counter, token-ring non-starvation, Chang-Roberts leader election, SAT backtracking and abstract CDCL termination. It also verifies Dijkstra’s k-, 4- and 3-state stabilization and Ghosh’s 4-state stabilization.
  • number: all examples verified within 10 minutes (§6, p.388)
  • number: all examples verified within 10 minutes
  • number: Dijkstra 3-state DomPerm(k=4) creates 18 existential quantifiers
  • number: toy stabilization bound n^2
  • limits: The user supplies how the ranking is composed, the other proof-rule formulas, and sometimes hints for existential witnesses. Domains are finite but unbounded. It does not cover unrestricted infinite domains in full. The review notes found no person-month figures.
  • how much was read: most of it read
  • source; notes: LVR and implicit ranking functions; notes: Ivy, ranking, Coq, and Iris case index
  • record id: implicit-rankings-2025
• LMGPA (2025)
  • title: Towards Language Model Guided TLA+ Proof Automation
  • what: An LLM splits hard TLAPS proof obligations into smaller claims. Symbolic provers check them. The invariant is given as input.
  • number: 26 inductiveness proofs of distributed protocols plus 93 math theorems (119 total)
  • number: Distributed protocols (Table 1 p. 13): symbolic-only 38.5%; DeepSeek-V3.2-Exp 50.0% with decomposition (13/26), 0% direct; Claude 3.7 Sonnet 42.3% vs 15.4% direct; GPT-5 42.3% vs 3.8% direct
  • number: Runtime DeepSeek 9h 14m vs Claude 1h 32m
  • number: Four decomposition attempts per claim; TLAPS timeouts Z3 5 s, Zenon 10 s, Isabelle 30 s
  • limits: It tests proving a supplied invariant. It does not test finding one or reading vague requirements. Training leakage is possible from public protocol proofs (Section 4.2). The suite leaves out both learning switches, chord and hybrid broadcast.
  • how much was read: most of it read
  • source; notes: LMGPA: prove supplied invariants rather than discover them; notes: TLAPS proof generation grew beyond the January 2025 toy study
  • record id: lmgpa-2025
• Neural model checking with invariants (2025)
  • title: Let a Neural Network Be Your Invariant
  • what: For hardware designs, one small neural network is trained to be both an inductive invariant (a set of states that contains all reachable states and is closed under steps; this proves safety) and a ranking function (a number that drops each time something bad could recur; this proves liveness). A solver then checks the network exactly, so a yes answer is a real proof. Training uses a constraint solver (MILP) rather than gradient descent.
  • number: 634-task benchmark: 11 SystemVerilog designs; 206 safety, 219 liveness, 209 safety+liveness tasks
  • number: solved: 190/206 safety (92%), 192/219 liveness (88%), 172/209 safety+liveness (82%)
  • number: nuXmv solved 82% of liveness and 74% of safety+liveness tasks; rIC3 50% and 61%; ABC 36% and 46%; prior neural method NMC’24 79% of liveness
  • number: pure liveness: faster than the best other tool on 66% of tasks, 10x faster on 46%
  • limits: Only finite-state hardware-style systems (no arrays or strings of parametric length, no procedure calls or dynamic data); the benchmark is the authors’ own, built from textbook-level designs, so results may not carry to other workloads; relies on sign-activation feed-forward networks.
  • how much was read: most of it read
  • source; notes: Let a Neural Network Be Your Invariant (2025)
  • record id: neural-model-checking-with-invariants-2025
• PSyn / ISyn (2025)
  • title: Guiding Likely Invariant Synthesis on Distributed Systems with Large Language Models
  • what: GPT-3.5 proposes predicates (PSyn) or whole candidate invariants (ISyn) for Promela models. It refines them using monitoring and Spin counterexamples. Likely invariants hold only for the states that were observed.
  • number: PSyn sound and sufficient on 7 of 8 models; ISyn sound on 8 of 8 but sufficient on 7
  • number: RunVS sound and sufficient on all 8; GPT-o3 direct sound 7, sufficient 3
  • number: observed/reachable ratio 0.00044 for producer-consumer, 0.000024 train/gate
  • number: Ethereum model 962 Promela lines
  • limits: Observing states is not a proof. The invariant must be sound and also sufficient. It has no refinement to code and no liveness. Humans provide the model, the grammar and the target safety properties.
  • how much was read: most of it read
  • source; notes: Guiding Likely Invariant Synthesis on Distributed Systems with Large L; notes: Guiding Likely Invariant Synthesis on Distributed Systems with Large L
  • record id: psyn-isyn-2025
• QSM-Cutoff (2025)
  • title: QSM-Cutoff: Systematic Derivation of Quantified Cutoff Formulas for Distributed Protocols
  • what: Enumerates reachable finite states using symmetry. Minimizes their logical description. Grows the domain sizes until a saturation test passes.
  • number: 19-model evaluation (Section 7, pp. 278-280), e.g. toy consensus forall: node=5, quorum=10, value=3
  • number: Pages 263-286
  • number: 19 protocols
  • number: 6000 s/run
  • limits: That the formula is a true reachability invariant for every size is still a conjecture. Ordered protocols such as Paxos and Bakery are future work.
  • how much was read: most of it read
  • source; notes: QSM-Cutoff: a full 19-model 2025 set
  • record id: qsm-cutoff-2025
• rIC3 (2025)
  • title: The rIC3 Hardware Model Checker
  • what: Introduces rIC3, a Rust bit-level IC3/PDR checker with a portfolio of IC3, BMC, and k-induction. It combines COI-reduced SAT queries, optimized VSIDS data structures, GipSAT, dynamic generalization (DynAMic), CTG/EXCTG, and optional internal-signal/localization abstractions. AIGER is handled directly; Btor2 word-level models are bit-blasted. Certificates are checked with Certifaiger and the tool integrates with SymbiYosys. The paper details architecture (ABC preprocessing to TranSys CNF, 11 IC3 + 4 BMC + 1 k-induction threads in portfolio), modular implementation (1,686 LOC IC3 core; 10,571 LOC total), ablations showing DynAMic and GipSAT matter, and systematic comparisons against IC3ref, ABC, nuXmv, AVR, Pono, and Avy.
  • number: Single-thread suite: 840 unique cases, 32 GB RAM, 3600 s; rIC3-ic3 solves 606 (225 timeout, 9 memory-out), PAR-2 2147.70, uniquely 61, fastest on 398
  • number: Single-thread competitors: nuXmv 533 solved/PAR-2 2777.30; ABC-pdr 516/2900.99; Avy 488/3142.87; IC3ref 486/3169.29
  • number: Portfolio HWMCC’24 (319 cases, 16 cores, 128 GB): rIC3 solves 245 (73 timeout, 1 memory-out), PAR-2 1809.74, unique 16, fastest 171; ABC-superprove solves 226
  • number: Ablation: disabling DynAMic (590 solved) or replacing GipSAT with Minisat (564) lowers solved count from 606; internal signals 564, localization abstraction 605
  • limits: Bit-level operation loses word-level arithmetic structure; bit-blasting arrays can explode and arrays are currently unsupported. Portfolio results use 16 cores/128 GB, while single-thread results use 32 GB and 3600 s. Some competitors uniquely solve cases rIC3 misses; internal signals/localization abstraction can reduce aggregate performance despite unique solves.
  • how much was read: most of it read
  • source
  • record id: ric3-2025
• rlive (2025)
  • title: Infinite-State Liveness Checking with rlive.
  • what: rlive is a model checker for liveness of infinite-state transition systems. It searches for counterexamples, learns abstraction predicates and synthesizes ranking functions. The ranking functions rule out loops that cannot run forever.
  • number: 835 liveness verification problems
  • number: timeout 1200 s, 8 GB per instance
  • number: solves 22 more instances than alpha-L2S
  • number: average speedup 6.47x on instances solved by both
  • limits: It handles Boolean and linear arithmetic constraints. It is model checking. It does not prove that software implements the model. It does not terminate on systems whose only counterexamples are not lasso-shaped (a prefix followed by a repeating loop).
  • how much was read: most of it read
  • source; notes: Infinite-State Liveness Checking with rlive
  • record id: rlive-2025
• SLD-Spec (2025)
  • title: SLD-Spec: Enhancing LLM-based Specification Generation via Program Slicing and Logical Deletion
  • what: SLD-Spec slices C functions and has an LLM generate ACSL annotations for each slice. It screens them. After integration, Frama-C/WP removes the ones that fail.
  • number: 37 of 51 programs and 10 of 11 complex programs
  • number: 37 SLD-Spec vs 36 SpecGen vs 27 AutoSpec
  • number: average runtimes 27.85 s, 42.04 s, 100.21 s
  • number: five runs; WP timeout 8 s
  • limits: It counts tasks solved across five runs, not pass@1. The complex dataset is composed from earlier small examples. It has no distributed progress.
  • how much was read: most of it read
  • source; notes: SLD-Spec: Enhancing LLM-based Specification Generation via Program Sli
  • record id: sld-spec-2025
• Tapis Horn-ICE array invariant learning (2025)
  • title: Data-Driven Verification of Procedural Programs with Integer Arrays
  • what: Introduces Tapis, a data-driven Horn-ICE decision-tree learner for procedural C-like programs with parametric-size integer/boolean arrays. It learns universally quantified loop invariants and procedure pre/postconditions by diagramizing array states into scalar samples, learning a quantifier-free decision tree, and lifting the classifier back to quantified array formulas; Z3 is the teacher that supplies counterexamples and inductiveness implications. The paper specifies finite-size array semantics (out-of-bounds reads return 0/false and writes have no effect), CHC encoding and Horn implications, then states the diagramization/lifting correctness results (proofs are deferred to the cited full version): Theorem 1 lifts a classifier of a consistent diagram sample; Theorem 2 guarantees consistency once each array has enough quantified indices. Attribute generation combines interval/octagon templates with patterns extracted from program assignments/guards. Bubble sort illustrates learned invariants; permutation preservation is explicitly outside that example. The implementation uses Clang frontend, C++ Tapis and Z3, tunes the teacher toward small arrays, and compares 215 programs: 121 SV-COMP array programs (84 safe, 37 unsafe) plus TAPIS-Bench (49 iterative, 37 recursive, 8 mutually recursive). Under 300-second runs on an 8-core 3.2GHz/16GB machine, Tapis solves 159/215 (95 safe iterative and 45 recursive safe plus 19 unsafe), versus Spacer 132 and Prophic3 118; it handles recursive procedures that several competitors cannot. Tapis uses at most two quantified variables per array/predicate in these sets and solves array-argmax for arbitrary N in 0.47 s where UAutomizer exceeds 36 minutes at N=5.
  • number: 215 programs total
  • number: 159 solved by Tapis; Spacer 132; Prophic3 118
  • number: 121 SV-COMP programs: 84 safe and 37 unsafe
  • number: TAPIS-Bench: 49 iterative, 37 recursive, 8 mutually recursive
  • limits: Programs are C-like, with finite parametric arrays, integer/boolean variables, loops and recursive procedures; specifications are first-order array formulas with universal index quantifiers and linear scalar constraints. The method requires fixed-size array values in counterexamples, so CHC-COMP unbounded-array benchmarks are excluded. Learner success depends on generated attributes, increasing quantifier count, sample consistency and Z3’s array-logic heuristics; quantifier alternation remains future work. Results are benchmark-specific and use manual translations to each competitor’s input language.
  • how much was read: most of it read
  • source
  • record id: tapis-horn-ice-array-invariant-learning-2025
• Veil (2025)
  • title: Veil: A Framework for Automated and Interactive Verification of Transition Systems.
  • what: It embeds distributed transition systems in Lean. It sends first-order proof obligations to SMT solvers and leaves the rest as interactive Lean goals.
  • number: 16 evaluated cases incl. Rabia, SCP, Suzuki-Kasami, Vertical Paxos
  • number: 1704 non-empty, non-comment lines of Lean; 85 actions and 185 invariants; about 100 lines per file
  • number: 16 benchmarks, 1,704 Lean lines, 85 actions, 185 invariants
  • number: Veil verifies 16/16; 14/16 under 15 s and 12/16 under 10 s
  • limits: It evaluates checking supplied invariants, not finding them. It is not an LLM agent. All its guarantees are safety. The notes record no agent success rate.
  • how much was read: most of it read
  • source; notes: Veil: proofs in Lean with automatic first-order checks; notes: Veil: a promising proof interface, with no agent rate established here
  • record id: veil-2025
• Verification of the CVM Algorithm with a Functional Probabilistic Invariant (2025)
  • what: The AFP document supplies a six-page informal proof, AppendixA.1–A.3 on printed/physical37–42. This reading inherits the20page main-paper account and source review from formal1417. The downloaded document is dated February6,2026, with a different title from the2025paper; correspondence to the exact version cited by that paper is unconfirmed. Only the prose appendix and opening title/contents were deliberately read. The TOC extraction accidentally also emitted the first formal-theory page3; it was not used as scientific evidence and no further formal-theory section was reviewed or executed. A.1 proves a distribution-level product invariant by alternating induction between the post-occurrence distributionΩ′ and post-subsampling distributionΩ. Insertion removes the current element then samples its reinsertion with current probabilityp; the argument separates whether that element belongs to the queried subsetS. Subsampling separates retained and absent elements, applies the assumed subsampler product bound, then the two scalar-function conditions. This avoids assuming independence of the buffer indicators. Lemma2 instantiates the class using nonnegative concaveh and a cutoff onp. A.2 sets A to the set of stream elements and q=n/(4|A|), reducing to|A|≥n. Lemma3 bounds the upper tail whilep≥q byexp(-nε²/12), usingt=qlog(1+ε), an affine exponential chord, Markov and the invariant. Lemma4 bounds the chance ofp<q by l exp(-n/12), union-bounding the first crossing fromf^j to f^(j+1). Its displayedf^j≤2ff^j usesf≥1/2; the retained main context is needed. Lemma5 uses negativet=qlog(1-ε), a nonnegative affine chord and the invariant to bound the lower tail byexp(-nε²/8). Theorem1 combines those three events: for0<ε,δ<1 and n≥12ε^-2 log(3l/δ), the displayed relative-error event has probability≤δ. This remains an abstract ideal-sampling theorem, not an executable implementation check. A.3 takes an almost-sure finite boundM onp^-1, suggestingM=f^-l. Applying the invariant to the two affine functionsx andM+1-x bounds both sides of the expected per-element scaled indicator, forcing its expectation to1. Linearity then gives E[|χ|/p]=|A|. The proof adds no empirical evaluation, implementation verification or distributed-system result. It makes the expected-value argument concrete but has strict/non-strict cutoff presentation gaps listed below. Exact source-page spansS1–S6 and individually viewed rendered pages preserve the printed reasoning.
  • limits: S1–S6: AppendixA.1–A.3 read completely, including every displayed induction calculation, Lemmas1–5, Theorem1 and unbiasedness derivation. Main20page reading inherited from formal1417. Current AFP document date February6,2026; exact identity with the cited2025 supplementary version not established. No formal tool or author implementation executed. S1: the appendix assumes subsample(chi) returns a subset and satisfies its referenced Eq1. That equation lies outside this new prose extraction and was not newly inspected in the formal-theory body. The original main paper context is inherited; this supplement is not treated as a self-contained proof of every subsampler premise. S1: Lemma1 prints phi:(0,1]×{0,1}→R_nonnegative but quantifies0<alpha<1,0<x≤1 while evaluatingphi(x/alpha,1). Forx>alpha that argument exceeds its domain. The displayed proof applications usex=p,alpha=p orx=pf,alpha=f, which keep the ratio in range, apart from the alpha=1 insertion boundary. This is a printed domain/boundary omission, not a claim that the uninspected formal theorem has that defect. S1–S2: the insertion step invokes condition1 withalpha=p, butcondition1 printsalpha<1 whilep=1 initially and before any subsampling. Atp=1 the needed inequality reduces to equality. A separate trivial endpoint case would close this presentation omission. S3–S6: Lemma2 states onlyq≤1 whileusingq^-1 as an interval endpoint; the applications requireq>0. More substantially it printsI(p>q), whereas upper/lower-tail calculations useI(p≥q). The lower-tail Markov calculation even changes the event top>q after startingp≥q. Equality can have positive probability becausep takes discrete powersoff. Do not silently certify these literal printed substitutions. S6: the unbiasedness display likewise usesI(p≥M^-1), where Lemma2 supplies a strict cutoff. Reader repair for this particular step: chooseq=1/(M+1), keepingh(x)=M+1-x nonnegative on[0,M+1]; thenp≥M^-1 impliesp>q and the same two bounds hold. This local repair is not a rereview or replay of the mechanized proof. S4–S6: Lemma4 needsf≥1/2 forf^j≤2ff^j and a positive finite streamlength for the displayedlog(3l/delta) capacity. The appendix relies on algorithm context instead of restating every parameter premise. Preserve the finite-stream and subsampling assumptions from the inherited main record. S1–S6: new proof-reading evidence leaves the main record printed negative-association Lemma6 concern intact. No formalization replay, proof-assistant output, random-number implementation, numeric arithmetic or Rust/distributed service has been verified by this reading.
  • how much was read: most of it read
  • source
  • record id: verification-of-the-cvm-2025
• AutoSpec (C/ACSL) (2024)
  • title: Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification (AutoSpec)
  • what: AutoSpec runs static analysis to split a program into parts. GPT-3.5 then writes ACSL contracts and loop invariants bottom-up. Frama-C/WP removes the candidates that fail, and the loop repeats until the given assertion is proved.
  • number: 79% (199/251) C programs verified; Table 1: 51 Frama-C, 133 SyGuS, 46 OOPSLA-13, 21 SV-COMP
  • number: six X.509 parser functions all succeed at least once; two succeed in only 2/5 runs, averaging 260.96 s and 957.14 s
  • number: 79% of 251 programs overall: 31/51 general, 114/133 SyGuS, 38/46 OOPSLA-13, 16/21 SV-COMP
  • number: 5 attempts per general problem; binary search 1/5, bubble sort 3/5
  • limits: A human chooses the target assertion. The paper compares against five months of annotating a whole parser, which had a different scope. It does not cover liveness.
  • how much was read: most of it read
  • source; notes: AutoSpec: Enchanting Program Specification Synthesis by Large Language; notes: Enchanting Program Specification Synthesis by Large Language Models us; notes: Enchanting Program Specification Synthesis by Large Language Models us
  • record id: autospec-c-acsl-2024
• Can ChatGPT support software verification? (2024)
  • what: Uses GPT-3.5 to fill ACSL loop invariants in C programs, validates candidates with Frama-C WP, and supplies validated invariants to Frama-C SV and CPAchecker through ACSL2Witness. The benchmark selects correct, single-loop SV-COMP Loops tasks already carrying human ACSL annotations. Up to five completions at temperature 0.2 generate candidates; individually validated candidates are conjoined. CPAchecker runs k-induction without loop unrolling, deliberately restricting its normal capability. The paper distinguishes validity from usefulness and proposes, rather than evaluates, nested validator/verifier feedback loops. Appendix A gives the complete uniform prompt and a sample answer.
  • number: 106 tasks; 75 with validated invariants
  • number: up to 5 completions; temperature 0.2
  • number: 10-second validation; 900-second verification limit
  • number: Frama-C: 22 GPT versus 28 human
  • limits: One loop and correct input assertions only; 106 selected tasks. Failure to validate within 10 seconds does not prove an invariant false. Frama-C syntax and typing can reject meaningful candidates. Copying nearby assertions explains many successes. Results concern a June 2023 GPT-3.5 snapshot and a restricted CPAchecker configuration. Read version is the later arXiv v2, not the publisher PDF for the DOI; artifacts were not executed.
  • how much was read: most of it read
  • source
  • record id: can-chatgpt-support-software-2024
• invariant-augmented interpolation model checking (2024)
  • title: Augmenting Interpolation-Based Model Checking with Auxiliary Invariants (Extended Version)
  • what: Augments McMillan interpolation-based model checking with externally generated invariants. Two variants strengthen fixed-point checks or interpolants so unreachable states are pruned, reducing program unrollings and interpolation queries while preserving safety verification. Defines invariant injection into IMC, compares fixed-point and interpolant strengthening, implements IMC variants in CPAchecker, and evaluates against IMC, invariant generators, and other verifiers on SV-COMP-derived tasks. The study reports task-level wins and analyzes overhead from invariant generation.
  • number: On 870 tasks with non-trivial invariants, plain IMC solved 534, fixed-point augmentation 536, interpolant augmentation 544 (§6.4)
  • number: Interpolant augmentation found proofs for 23 tasks where plain IMC timed out, while losing 13 plain-IMC proofs (§6.4)
  • number: Reduced unrollings on 35 tasks and interpolation calls on 56 tasks (§6.4)
  • number: Resource setup: 15-minute/15-GB task limits and 2.5-minute invariant generation (§6.3)
  • limits: Benefits require non-trivial inductive auxiliary invariants; trivial invariants add no information and generator time can erase gains. Evaluation uses bounded resource limits, selected domains and CPAchecker/MathSAT5 configurations. Augmented methods can lose tasks solved by plain IMC because of invariant-generation overhead.
  • how much was read: most of it read
  • record id: invariant-augmented-interpolation-model-checking-2024
• LLM-Generated Invariants for Bounded Model Checking Without Loop Unrolling. (2024)
  • what: ESBMC ibmc replaces C loops with LLM-generated invariants after Vampire proves initialization and inductiveness, then uses ESBMC to verify the resulting loop-free overapproximation. Havocs loop-modified variables, proves base and step conditions with previously proved invariants as strengthening assumptions, iterates proof attempts, and includes negated loop guards on exit. GPT-3.5-Turbo-Instruct generates candidates for labelled loops; retries vary requested invariant counts. Compares full/constrained/combined prompts with optional regex syntax filtering. Demonstrates universal/existential assertion examples using quantified invariants and special internal __forall semantics.
  • number: 133 one-loop benchmarks; largest 53 C lines
  • number: pooled 101 solves; single combined/no-filter 79
  • number: SeaHorn 115; VeriAbs 73; ibmc 2 unique
  • number: 30 iterations/600 s; combined 60/1200 s
  • limits: Soundness is argued for proving correctness, while transformed counterexamples may be spurious. Invariants can be too weak; no proved invariant aborts verification. Main experiment uses one-loop Code2Inv programs, largest 53 lines. The 101/133 result pools six configurations and comparison uses a hypothetical per-benchmark best configuration. Combined prompts receive 60 iterations/1200 seconds versus 30/600 for other configurations. Multiple runs were not reported. Vampire lacks bit-vector reasoning and pointer shape predicates are unsupported; larger and multi-loop benchmarks remain future work. Accepted manuscript, not publisher final version.
  • how much was read: most of it read
  • source
  • record id: llm-generated-invariants-for-2024
• LLM-Guided Formal Verification Coupled with Mutation Testing (2024)
  • what: Proposes a three-stage GPT-4 workflow: derive natural-language/Z3Py invariants from specifications, translate behavioral Verilog hierarchically into Z3Py, and assess invariants against single-edit mutants produced with Yosys. Separates specification extraction/cross-checking from invariant generation, uses bottom-up submodule modeling when an LLM declines a complex design, and translates only mutant-versus-original changed lines into the formal model. Failed invariant cases become Verilog testbench inputs. The case study uses two invariants for priority between buses and between bits within a bus.
  • number: 27-channel interrupt controller
  • number: 5 submodules; 2 invariants
  • number: 20/20 mutants detected; reported mutation score 1
  • limits: A two-page methodology/case-study paper, with one interrupt controller and 20 mutants. It does not establish correctness of the LLM-derived formal model, invariant completeness, or robustness across models/prompts/runs. The prose says an UNSAT result has a counterexample, which conflicts with ordinary SMT terminology; no supplied code was inspected to resolve the encoding. Claims about politeness and monetary tips improving output are uncontrolled observations. Automated interaction frameworks remain future work. DOI identity comes from matching institutional title/authors and Crossref metadata, not a DOI printed in this author PDF.
  • how much was read: most of it read
  • source
  • record id: llm-guided-formal-verification-2024
• LLMLIFT verified lifting (2024)
  • title: Verified Code Transpilation with LLMs
  • what: Introduces LLMLIFT, an LLM-based verified-lifting workflow that generates a DSL program summary and loop invariants in Python IR, verifies equivalence to side-effect-free source code with SMT, then rewrites the verified IR into concrete DSL syntax. The workflow uses oracle-guided inductive synthesis: prompts provide DSL operator semantics in Python, the LLM proposes summaries and invariants, a parser rejects unsupported syntax, and cvc5/Z3 check functional equivalence for all states. Four implementations target Spark/MapReduce, Domino programmable switches, TACO tensor algebra and TensIR. Two-phase summary-then-invariant generation is stronger than joint generation; smaller Llama3/Mistral models fail the complex tensor suite due to syntax adherence/context.
  • number: Spark 44/45 versus MetaLift 40/45; under one minute versus three minutes average
  • number: Domino 10/10, about 2 s versus MetaLift 6 s
  • number: TACO 60/60 versus C2TACO 57/60; about 2 s versus 41 s
  • number: TensIR 23/23; 95.89 s versus Tenspiler 115.14 s
  • limits: Source programs are side-effect-free and the supported subset excludes pointers and objects. Correctness is relative to the encoded IR semantics, rewrite rules and theorem-prover model; code performance is inherited from target DSLs rather than optimized by LLMLIFT. The verifier supplies Boolean feedback, and the authors identify semantic filtering/counterexamples as future improvements.
  • how much was read: most of it read
  • record id: llmlift-verified-lifting-2024
• LVR (2024)
  • title: LVR: Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions
  • what: LVR turns a progress goal into ranking obligations and safety obligations: the measure decreases, stays nonnegative, cannot leave the pending condition without reaching the good state, and no deadlock occurs. It infers integer variables, bounds and polynomial coefficients. mypyvy and P-FOL-IC3 discharge the safety obligations. Humans supply any missing variables, bounds and tiers.
  • number: 37 out of 40 (§9.2, p.35:27) automatically; the rest manually in a few hours each
  • number: each final coefficient-solving query takes less than a second
  • number: eight models: ticket lock 68 lines, hybrid reliable broadcast 137, alternating bit 127, TLB shootdown 361, Paxos 133, multi-Paxos 135, stoppable Paxos 160, sliding window 119
  • number: all eight protocols succeed: ticket lock, hybrid reliable broadcast, alternating bit, TLB shootdown, Paxos, Multi-Paxos, Stoppable Paxos, sliding window
  • limits: By default, scheduling assumes a globally bounded interval. This is a slightly stronger fairness than “infinitely often”. For example, scheduling at times 1, 2, 4, 8 satisfies “infinitely often” but not any fixed bound. Prophecy variables and a three-tier ranking keep the original fairness. LVR’s multi-Paxos leaves out the local scheduler and the I/O queue. So fewer lines than IronFleet does not mean equally less effort. A cheap solver query is not the whole cost.
  • how much was read: most of it read
  • source; notes: LVR and implicit ranking functions
  • record id: lvr-2024
• mypyvy repository (2024)
  • title: mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic.
  • what: mypyvy is a symbolic transition-system language inspired by Ivy. Its README documents inductive invariant checking and inference and gives a lock-server example.
  • number: 43 top-level examples, 83 more under misc and fbii
  • number: examples/misc/pd at the inspected checkout has 39 .pyv files covering cache, consensus, lock service, ring election, sharded KV, TLB and Paxos variants
  • limits: The README gives setup and examples, not benchmark results.
  • how much was read: most of it read
  • source
  • record id: mypyvy-repository-2024
• neuralmc (2024)
  • title: Neural Model Checking
  • what: NeuralMC trains neural ranking functions (measures that shrink toward the goal) from simulation samples. It targets LTL liveness of SystemVerilog hardware. It then validates the functions symbolically with SMT over all transitions.
  • number: Table 1: 194 tasks; own tool 180, ABC 57, nuXmv 117, commercial X 156
  • number: five hours per task
  • number: VGA solves 0 of 10
  • limits: It covers finite hardware models. Training failures and timeouts are separate from proved violations.
  • how much was read: most of it read
  • source; notes: Related work absent from the first pass: Neural Model Checking
  • record id: neuralmc-2024
• Wuldo unrealizability proof synthesis (2024)
  • title: Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs
  • what: The paper introduces Wuldo, the first proof-synthesis algorithm for Unrealizability Logic (UL), a Hoare-style logic over potentially infinite program sets described by regular tree grammars. Wuldo computes syntax-directed proof skeletons, generates parametric verification conditions, and checks or synthesizes nonterminal summaries and loop invariants using SMT/SyGuS solvers. Summaries are reusable inductive facts about grammar nonterminals, enabling compositional proofs of unrealizability and infinite-state/input properties. The implementation supports whole-cloth proof generation for some cases and emits interpretable proof certificates, unlike black-box satisfiability encodings.
  • limits: Wuldo’s main relative-completeness result is for loop-free program sets; loops require summaries/invariants and can be difficult. Effectiveness depends on solver support for quantified linear arithmetic, infinite arrays, and SyGuS grammars; Wuldo may prove unrealizability but does not generally establish realizability. Experiments use regular-tree grammars, finite benchmark suites, 5-minute timeouts, and a 4-core i7-7700HQ/16GB Windows machine. The authors note unsupported nondeterminism and hard quantified summaries as open limitations.
  • how much was read: most of it read
  • source
  • record id: wuldo-unrealizability-proof-synthesis-2024
• Akshay et al. affine MDP invariants (2023)
  • title: MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives.
  • what: Treats MDPs as transformers of probability distributions and synthesizes affine inductive distributional invariants together with strategies proving distribution-based safety. AlgMemLess targets memoryless strategies with relative completeness; AlgDist handles distribution-dependent general strategies with sound but incomplete Handelman-based constraints. The paper proves that distribution strategies depending only on the current distribution suffice, and that an inductive distributional invariant contained in the safe set is a sound and complete certificate. AlgMemLess templates action probabilities and a conjunction of affine inequalities, uses Farkas’ lemma to eliminate universal quantifiers, and has soundness, relative completeness, and PSPACE bounds. AlgDist uses quotients of affine expressions for action probabilities; positivity constraints remove denominators, and Handelman’s theorem produces a sound bounded-product translation, losing completeness. The framework handles initialized and uninitialized cases, restricted initial constraints, and can extend to polynomial invariants via Putinar’s Positivstellensatz. A prototype in Python/SymPy/PySMT with Z3 and MathSAT solved Running, Chain, Split, PageRank, and Insulin-131 I examples.
  • number: AlgMemLess PSPACE, sound and relatively complete
  • number: AlgDist PSPACE for fixed K, sound but incomplete
  • number: Running 3s, 92 vars, 123 constraints
  • number: Chain 10s, 69 vars, 82 constraints
  • limits: Safety sets are finite conjunctions of affine inequalities over finite-state MDP distributions; initialized safety is Positivity-hard even for Markov chains. AlgMemLess is complete only relative to affine invariants and memoryless strategies; AlgDist’s Handelman translation is incomplete, parameterized by product bound K, and assumes compact antecedent sets for the theorem motivation. Existential nonlinear real arithmetic is decidable but solver performance varies by orders of magnitude and can take hours. Experiments are unoptimized and small; no claim of scalability or complete decision procedure for general distribution safety is made.
  • how much was read: most of it read
  • source
  • record id: akshay-et-al-affine-mdp-invariants-2023
• ByMC (2023)
  • title: ByMC: Byzantine Model Checker, and Survey on Parameterized Verification with Threshold Automata
  • what: ByMC models nodes that count messages against thresholds, abstracts the counts, and uses an SMT solver to check safety and liveness for every allowed number of processes and faults. Verified for both safety and liveness: folklore and Srikanth-Toueg reliable broadcast, asynchronous Byzantine agreement, nonblocking atomic commit, condition-based consensus, CF1S, C1CS, and BOSCO. The randomised protocols (Ben-Or, Byzantine consensus, k-set agreement and RS-BOSCO) get safety plus almost-sure termination (they finish with probability 1).
  • number: Table 4 (§6.2, p.5:20) lists the verified protocols
  • limits: The randomised cases hold only against adversaries that respect round boundaries. The Tendermint one-round agreement analysis covers safety only. The benchmarks are compact models, not runnable implementations. The review notes did not recover the original 2018 ISoLA chapter and read the 2023 survey instead. The review notes found no human person-time.
  • how much was read: most of it read
  • source; notes: ByMC: fully parameterized model checking; notes: Ivy, ranking, Coq, and Iris case index
  • record id: bymc-2023
• Can Large Language Models Reason about Program Invariants? (2023)
  • what: Fine-tunes 430M, 1B, and 5B-parameter code language models to predict 18 classes of Java program invariants at function entry/exit and loop points. A scratchpad prompt predicts invariants at successive program points and then the target; the paper interprets this as learning in an abstract invariant space. On Code Contests Java programs, the best models reach about 86% precision and recall and outperform Daikon when Daikon receives at most five traces. The dataset is generated by instrumenting Java submissions with dummy loop calls, running Daikon on 200 available inputs, and splitting by problem to prevent near-duplicate leakage. The authors report 1,600,158 train, 86,346 validation and 24,509 test examples. Evaluation uses Jaccard similarity, precision, recall and F1 against 200-trace Daikon targets; models use greedy decoding, 20,000 steps, batch 128 on 64 TPU-v4 cores. Table 3 shows Daikon F1 .721 with one trace, .857 with five, .868 with six and 1.00 with 200. For ordered 5B scratchpad forward prediction, F1 is .858 in both combined and separated training; combined shuffled 5B scratchpad reaches .863. Oracle reaches .867 forward and up to .877 backward across settings. GPT-4 zero-shot is weak (listed pilot precision .44, recall .384 on paper listings and no ground-truth invariants for ten random test prompts). Case listings show model-discovered valid invariants omitted by Daikon, but also spurious predictions and dependence on model scale. The paper is empirical invariant prediction, not proof: Daikon targets are treated as ground truth although dynamic analysis can miss valid invariants or produce false positives. The oracle receives the Daikon target invariants at program points preceding its target and therefore uses dynamic information, unlike direct and scratchpad inference. Backward prediction also changes the dataset: it excludes the final program point and introduces class invariants, yielding 1,284,492 training, 61,431 validation and 21,576 test examples; forward/backward scores thus have different target and example populations.
  • number: {‘model_parameters’: [‘430M’, ‘1B’, ‘5B’], ‘train_examples’: 1600158, ‘validation_examples’: 86346, ‘test_examples’: 24509, ‘traces_per_program’: 200, ‘invariant_types’: 18, ‘daikon_f1_1_trace’: 0.721, ‘daikon_f1_5_traces’: 0.857, ‘daikon_f1_200_traces’: 1.0, ‘best_reported_precision_recall’: ‘about 0.86 each’, ‘training_steps’: 20000, ‘tpu_cores’: 64, ‘backward_train_examples’: 1284492, ‘backward_validation_examples’: 61431, ‘backward_test_examples’: 21576}
  • limits: An invariant is a Boolean predicate true whenever execution reaches a specified program point; the task is undecidable in general. Ground truth is the set Daikon emits from 200 inputs; the authors explicitly note this can miss invariants and overfit finite traces. The dataset consists of Java competitive-programming submissions with available inputs, not distributed protocols, Rust/Verus code or TLA+ specifications. Direct and scratchpad inference is static with respect to the target program and uses greedy decoding, but training labels come from dynamic traces. Oracle inference receives intermediate Daikon target invariants as additional dynamic information and is not a purely static comparator. The paper reports offline experiments and does not establish semantic correctness of model outputs beyond comparison with Daikon/manual inspection.
  • how much was read: most of it read
  • record id: can-large-language-models-2023
• Loopy (2023)
  • title: Finding Inductive Loop Invariants using Large Language Models
  • what: An LLM proposes pieces of loop invariants for C programs. Houdini prunes them. Frama-C/WP checks that they are inductive (hold at the start and are preserved by each step). The model repairs failures.
  • number: 469 positive tasks
  • number: Houdini raises solved cases from 293 to 383
  • number: eight generations plus seven repairs: 398 solved
  • number: Ultimate solves 430 of 469 vs Loopy 398; 31 solved only by Loopy
  • limits: Proves assertion safety for the supplied programs. No termination proof. Arrays and pointers are filtered out. One loop and one method.
  • how much was read: most of it read
  • source; notes: Finding Inductive Loop Invariants using Large Language Models (Loopy)
  • record id: loopy-2023
• Message Chains / UPVerifier (2023)
  • title: Message Chains for Distributed System Verification
  • what: Records the chain of messages that caused a later message, so causal facts can be stated directly without inventing ghost state (extra proof-only variables). It is used to check proofs of P-like programs for any system size.
  • number: 19 evaluated cases: 16 reused mypyvy models plus Tor/onion routing, GlobalClock (150 lines, under 2 s) and 2PC-MVCC (250 lines, about 12 minutes)
  • number: Pages 2224-2250
  • limits: It automates the bookkeeping for proofs that are supplied, and mines facts from examples. It does not discover invariants in general. The review notes did not locate a complete fixed archive of all 19 models.
  • how much was read: most of it read
  • source; notes: Message Chains / UPVerifier: full 19-case paper set recovered; notes: Message Chains for Distributed System Verification
  • record id: message-chains-upverifier-2023
• Automating cutoff proofs (2022)
  • title: Automating and Mechanizing Cutoff-based Verification of Distributed Protocols
  • what: Formalizes cutoff-based verification for parametric distributed protocols in the Relational Modeling Language (RML). A finite cutoff instance is sufficient when every safety violation in any larger instance can be simulated by a trace of the cutoff; the paper encodes this simulation in first-order logic and uses SMT to check it. The paper gives initial, step, and safety simulation conditions and a first-violation refinement that removes the need to simulate behavior after a violation. A backward static analysis starts from instantiated negated safety clauses, follows action updates into guards to a fixed point, and emits the relevant action set, simulation relation, and lockstep. In the sharded key-value example, the analysis reduces eight actions to four and proves a two-node cutoff. The implementation checks the formulas with Z3 and handles seven protocols: four cutoffs are synthesized automatically; three require small manual changes. Two-phase commit exposes a limit: universally quantified guards force actions of all larger-instance nodes into the simulation, requiring an extra failure-simulating node and constraints.
  • number: 7 protocols
  • number: 4/7 automatic synthesis; 3/7 small manual changes
  • number: 20–40 ms per protocol
  • number: 2-node sharded-key-value cutoff
  • limits: RML domains are finite per instance but may have infinitely many valid interpretations; safety properties are assumed universally quantified. The result is for safety, not liveness. Cutoff correctness depends on a simulation relation for every valid larger interpretation and on a safe finite cutoff. Automatic synthesis can fail when universal guards or side effects conflict, as in two-phase commit, and the basic key-value store needs an added precondition.
  • how much was read: most of it read
  • source; notes: Cutoff automation with seven concrete protocols
  • record id: automating-cutoff-proofs-2022
• Counterexample-Guided Prophecy (2022)
  • title: Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
  • what: Introduces Prophecize, which adds history and frozen prophecy variables during CEGAR refinement to target array terms at future time steps. The array abstraction and refinement reduce many quantified, array-valued invariant proofs to quantifier-free, array-free reasoning, implemented in prophic3. The paper proves soundness and no false positives for the refinement, describes weak versus strong array abstraction, unsat-core filtering of axioms, large-value abstraction, and a pre-state-property heuristic. The approach needs only a small number of relevant index instantiations close to a potential violation; prophecy variables average 1.2 (median 1) on solved quantified cases.
  • number: freqhorn: 81 benchmarks, prophic3 66 Q / 5 QF / 0 US
  • number: quic3: 43 benchmarks, 41 Q / 0 QF / 0 US
  • number: vizel: 33 benchmarks, 22 Q / 3 QF / 1 US
  • number: CHC-COMP-2020: 501 benchmarks, 42 Q / 159 QF / 56 US
  • limits: Termination is not guaranteed when no finite Prophecize calls capture all relevant indices. Array axiom enumeration assumes an infinite index domain. Performance is sensitive to transition-system encoding; SeaHorn translations solved 6 quic3 benchmarks versus 41 with direct Kratos2 translation. The method’s existential power is weak because history variables only retain finite delays, and it is not expected to work well for parameterized protocols without improvement.
  • how much was read: most of it read
  • record id: counterexample-guided-prophecy-2022
• Demystifying and Checking Silent Semantic Violations in Large Distributed Systems (2022)
  • what: Empirical study of 109 production silent semantic failures from nine systems, followed by Oathkeeper: a runtime checker that learns likely event-relation rules from patched regression traces, keeps rules failing on corresponding buggy traces, filters against the remaining patched tests, and monitors future execution. It detects six of seven selected newer known failures and reports activation-conditioned false-positive rates. This is trace-based inference and runtime detection, not an inductive proof of distributed-system correctness. Records the ticket-sampling population and bias, thirteen study findings, exact before/after regression workflow, event and state instrumentation boundaries, counter-based implication semantics, inactive-rule distinction, finite-window/recheck tradeoffs, all seven newer contracts, cross-case transfer limits, all throughput values and activation-conditioned false-positive denominators.
  • limits: §2: Semantics are guarantees about output, state and subsequent operations in response to requests, commands, messages, environment changes or time. Silent violations leave the system operational without explicit crash/timeout/exception signals. A later error in another operation can expose the earlier violation. The scope includes system-specific contracts beyond protocol consistency. §3: Tickets must be resolved server bugs above minor priority. Iterative random sampling balances candidate counts across systems; nonproduction/internal-test cases and explicit failures excluded. In-depth 109 cases prefer information-rich discussions among 268 candidates from 747 valid cases in 1,922 sampled tickets out of 38,786 total. Multiple inspectors reconcile classifications. Selection, reporting, survival and Java/C++ biases prevent interpreting percentages as universal production failure probabilities. §4: Reported mean 39% (range 20–57%) is the paper’s average of candidate/valid ratios across sampled systems. Priority labels normalized to blocker/critical/major; 45% of studied cases are blocker or critical. This is historical issue prioritization, not independent measurement of severity. Consequences in Figure 3 differ from the violated guarantee itself and can arise later. §5: 87% of violated semantics explicitly documented (53% API, 24% internal behavior, 10% configuration); remaining 13% implicit expectations. Documentation can be vague/incomplete and is not mechanically enforced. Old semantics means present in first major stable release. Their 68% share has no denominator of all old/new contracts, which authors explicitly did not count; it does not estimate per-contract risk. §5–7: 74% of violations judged locally, sometimes using replicated local session/node state; 26% need global information. This is case classification, not a proof that every locally observed trace represents a consistent distributed snapshot. Safety/liveness classification follows official documentation: 86% safety, 14% liveness. Finite absence of an eventual response alone cannot establish general liveness failure. §6–8: Only 12% assigned familiar memory/race/overflow bug patterns; most are varied system logic/design defects. Two-thirds violate guarantees extending beyond operation return, so single-entry assertions can miss later failures. Existing semantic test coverage in 73% of cases does not cover all triggering combinations. MongoDB’s production assertions correlate with its lower silent-failure fraction, without causal identification. §8.3: Observability percentages derive from only 34 tickets explicitly describing how users noticed the problem, not all 109. Every observed case had already been discovered, creating survival bias. Overlapping APIs and state-query APIs are recommendations from these observations rather than evaluated interventions. §9.1–9.2: Users provide build/test configuration and past failure commit IDs/test names, optionally classes and compatibility patches. Tool executes patched and preceding buggy versions; regression tests copied to buggy code may require interface fixes. Evaluation instead adds switches to enable/disable old patches. Useful input therefore depends on reproducible old failures and adequate regression tests. §9.2: Java load-time bytecode hooks at method entry, return and exception; state hooks target primitive/collection members in patch-affected classes plus optional user classes. These are selected observable events, not every semantic state or an automatically proved mapping from documentation. Event records contain context such as variable name/location/time. Operation-event uniqueness in the illustrated template uses method signature; paper does not prove per-client/object obligation matching or cross-node ordering soundness. §9.3: Eighteen manually designed templates constrain candidate search to event types and relation structures; seven examples appear in Table 3, full list deferred to technical report. Parameterized matches are likely invariants of the observed traces, not exact/full high-level semantics. No induction, model checker or universal proof validates unseen executions. Templates require domain knowledge but avoid writing each concrete rule manually. §9.3/Algorithm 2: p⇒q uses one counter per distinct ordered event pair. Each p increments outstanding count; subsequent q decrements positive count. Earlier q does not satisfy later p; one q discharges one outstanding p. Zero final counter yields candidate rule. This is stronger than existence of one later q for all p and still depends on event identity/context. Enumeration is affordable for reported test traces, not claimed scalable to arbitrary production histories. §9.4: PASS requires activated antecedent and no contradiction, INACTIVE means antecedent absent, FAIL means contradiction. Retain rules passing patched regression and failing buggy trace; then discard those contradicted by any patched test, excluding start/shutdown/thread-run regions via test markers. Inactivity is not positive evidence of universal correctness; test filtering can retain coincidences and eliminate desirable properties if tests differ in intended scope. Listing 1/Algorithms 1–2, p.100: Printed Verify interface says true means continue scanning; generic Algorithm 1 breaks when scan returns true, while Algorithm 2 returns true for every event. Generic Verify also omits the prescan initialization called for by the interface/example. Record these as apparent pseudocode inconsistencies; no implementation inspected, so do not infer a tool defect. §9.5–9.6: Production checker runs periodically, logs counterexamples, rechecks shortly to tolerate transient violations, and alerts rather than crashes the service. Recent-event window exceeds checking period; time-related events retained by parameter expiry. No formal proof of event completeness, buffer-loss freedom, ordering or preservation of arbitrarily long pending obligations under window expiry. Periodic finite-trace checks and short recheck are practical monitors, not general liveness verification. §9.6–9.8: Survivor optimization stops validating a rule once disproved; related tests prioritized. Ring buffers decouple emission/checking, reuse expired objects and preallocate per event type. Assumptions: contracts expressible through simple event relations, enough good tests, and old patches without major redesign/interface changes. Java/JDK 8, Javassist and JUnit implementation; no Rust/Verus/TLA+ or LLM specification/proof experiment. §10.1–10.2: Eight ZooKeeper, ten HDFS and eight Kafka old failures selected with regression tests. Seven later cases are known bugs chosen for related semantics but different root causes, nine to 34 months later. Six detections show transfer within that selected scope; not prospective discovery of six unknown bugs or recall over all failures. Unseen semantics expected to be harder. ZK-1667 fits a template but training test quality yields wrong rules. §10.2: Mean 0.91 s measured from violation onset after deliberately triggering reproduction soon, not client-operation start or production incident time. Comparator uses Daikon on instrumented state variables, the invariant engine underlying Dinv, and detects one case with noisy rules; not a comprehensive unchanged Dinv deployment comparison. §10.2 additional experiment: 22 ZooKeeper failures sorted by ticket time. Six individual failure-derived rule sets transfer to a median five failures; 16 detect only their own failure within the pool. Figure 11 aggregates a sliding subset as caption states. This assesses overlap in a historical pool, not independent prospective validation or a universal specification. §10.3–10.5: Runtime overhead measured on three stated workloads, not arbitrary production load; checker asynchronous. Only 11%, 66%, 48% of rules activate on ZooKeeper/HDFS/Kafka, respectively. False-positive rates 4%, 9%, 12% apply among activated rules, not all rules, requests or failures. Paper does not report observation duration, confidence intervals or exhaustive false-negative rates. Suggested profiling/banning false rules not evaluated here. Scope: All evidence below is read from the proceedings paper; no tool, benchmark, regression tests or repository executed. Artifact availability/functionality/reproduction badges are printed on p.91; they are not an independent reproduction by this reader.
  • how much was read: most of it read
  • source
  • record id: demystifying-and-checking-silent-2022
• DuoAI (2022)
  • title: DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols
  • what: Infers inductive safety invariants for Ivy distributed-protocol models by filtering formulas on reachable simulation states and refining candidates with Ivy/Z3. A finite directed implication graph organizes formula weakening. Runs top-down weakening, bottom-up universal-core strengthening and a universal-only search in parallel. Reports26of27protocols solved, including five Paxos variants; vertical Paxos exhausts memory. Completeness is relative to an adequate finite decidable formula space and graph/optimization correctness, with a reader counterexample to the printed arbitrary-alternation decomposition extension. Supplies exact/approximate implication graphs, sample-preserving coverage theorem, monotonic-refinement proof, counterexample-pruned powerset search proof, quantified-variable/type ordering, mutual-implication optimizations and all benchmark outcomes. Explains which refinement wins per protocol, why hundreds of existential candidates can stall SMT, what human choices baselines require, and how specification/retrofitting differences affect claims of automation. Reader checks distinguish sufficient invariant inference from implemented-system verification and identify a quantifier-dependency flaw in a printed optimization lemma.
  • number: solves 26 of 27 protocols including Paxos variants; Vertical Paxos runs out of memory
  • number: Fast Paxos takes 26,979 seconds (about 7.5 hours)
  • number: solves all but 1 of 27 protocols (Vertical Paxos unsolved)
  • number: evaluation permits a week per tool and protocol
  • limits: Inputs are an Ivy protocol transition model and safety property, not arbitrary executable distributed code. Trusted Ivy/Z3 checks initialization and transition preservation of the conjunction and safety implication for all modeled instances, rather than bounded simulation being the certificate. Scope is safety; no liveness, crash-recovery implementation refinement, verified Rust/Verus proof or LLM-agent evaluation. Sampled states are assumed genuinely reachable; incorrect simulation could discard needed true invariants and compromise completeness, though final sound SMT checks still guard returned results. Finite formula search space uses prenex DNF, relational predicates/equality; extension to uninterpreted functions referred to DistAI. Bounds are quantified variables per sort, max_exists, max_literal, max_and and max_or. Tautologies/contradictions excluded. Nonempty sorts are implicit in universal-to-existential implication. Quantifier alternation must follow a fixed sort order, inferred partly from axioms or supplied by user; absent user choice multiple orders are tried in parallel. The actual full verification condition, including protocol axioms/transitions, must remain in the intended decidable fragment. Exact graph is transitive reduction of strict implication over finite formulas; syntactic implementation instead uses five sound weakening shapes and may connect equivalent formulas. Lemmas1–5 establish claimed acyclicity, implication and coverage of nontrivial formulas from selected roots. No theorem says every semantic implication is an edge/path in the approximate graph; coverage plus sound directed weakening is what enumeration/refinement need. Enumeration checks original variable-length states at multiple finite instance sizes, rather than DistAI incomplete fixed-length subsamples. A candidate is retained if it holds on all sampled states; descendants can be skipped if dominated by an existing candidate. Theorem1 says every true invariant in S is either itself retained or has a stronger retained ancestor. Retained candidates can still be false on unseen reachable states; simulation removes candidates, not proof obligations. Top-down refinement checks conjunction plus safety, replaces a failed candidate by noninvalidated immediate successors not already dominated by a reachable ancestor, and returns NotProvable if safety fails. Reachable ancestor here means a graph path avoiding invalidated nodes, not a reachable protocol state. Theorem2 maintains domination of every member of an adequate inductive solution; finite formulas each invalidated at most once give finite refinement assuming every solver check terminates. Bottom-up first weakens all universal candidates until inductive, explicitly ignoring safety, to obtain universal core. noncore includes existential candidates AND universal candidates not in the core whose inductiveness may require existential support. Enumerates subsets by size, calls top-down on core plus subset, and skips subsets holding on an already returned negative prestate. A failed safety-induction counterexample is a possibly unreachable state that invariants must exclude; strengthening can remove it. Theorem3 eventually tries all noncore, reducing to full top-down, conditional on correct pruning and finite solver decisions. Relative completeness is not a guarantee to prove every correct distributed protocol. Needed inductive solution must be expressible in chosen finite S and decidable fragment, samples/graph/optimizations must preserve it, solver calls must terminate, and resources must suffice. NotProvable means this search space cannot prove the property, not the protocol unsafe. Increasing size in round-robin has no practical resource bound; vertical Paxos memout is concrete failure despite expert invariants existing. Defaults max_literal4,max_or3,max_and3,max_exists1 unless safety already has>=2existentials; quantified variables per sort initially maximum arity occurrence in any relation. On failure increments literal/OR/AND/existential/per-sort-variable bounds round-robin. Runs a third max_exists0top-down worker along with general top-down/bottom-up; benchmark walltimes benefit from parallel simulation/refinement and possible sort-order searches, with no separate CPU-time/worker-count-normalized comparison. Mutual implication optimization suppresses Q if retained P1…Pk jointly imply Q, then reintroduces Q if a supporting candidate invalidated. Equivalence decomposition suppresses a formula permanently only when conjunction of smaller formulas is truly equivalent. Examples separate two independent existential witnesses, same witness, and distinct witnesses: existential dependency matters to logical validity, not just speed. Decomposition can require representation of each component within allowed search space. Reader counterexample to Lemma6 claimed arbitrary-alternation/skolemization extension: sorts A,X each{0,1}, fixed order A before X. Let p(x) iff x=0, q(x) iff x=1, r(a,x) iff a=x. F=exists a forall x.((p(x) AND q(x)) OR r(a,x)) is false. The selected conjunction p(x) AND q(x) has two components sharing no existential variable. Claimed components exists a forall x.(p(x) OR r(a,x)) and exists a forall x.(q(x) OR r(a,x)) are both true, choosing a=1 and a=0 respectively. A globally chosen existential witness in the other disjunct cannot be chosen separately. Proof for forall-X exists-YZ is valid under its independence conditions; extending it to arbitrary alternation is unsupported and false as stated. Restrict prefix/dependency structure or preserve shared Skolem choices. This challenges printed optimization/completeness scope, not observed artifact behavior; final independent sound SMT checking can still reject unsafe outputs. Printed Lemma6 proof also calls f/g disjunctions of component literals although components of original conjunction must remain conjunctions for Eq19. This is a terminology/algebra transcription issue for multi-literal components, separate from the arbitrary-alternation counterexample. Lemma5 existential-root argument omits stated no-OR root condition; treat as proof detail needing completion rather than infer a specific artifact failure. Printed Algorithm2 loops only while candidates nonempty, then returns NotProvable; it omits explicit check for already-inductive safety when no strengthening candidates exist. For an unchanged Boolean b initiallyfalse and safety notb, an empty candidate set suffices but displayed procedure returns NotProvable without checking. Algorithm3 likewise needs defined empty universal core when Procedure1 returns no candidates. These are boundary/pseudocode qualifications; do not treat them as reproduced implementation failures. This empty-input example concerns the displayed procedure: default enumeration may retain not-b, and Theorem1 prevents an empty candidate set when a nonempty sufficient II-star is represented. It is not an end-to-end failure of default search. The O(m^2) discussion counts a possible pairwise invariant-dependency workload, not a formal polynomial bound on quantified SMT runtime. Solver cost can dominate even with few formulas. Paper compares14needed Paxos invariants verified in<1s, +10correctunnecessaryalternating invariants5min,+20over3h;149universal Chordinvariants8s. This motivates existential sparsity but is not repeated statistical scaling evidence. Evaluation27small Ivy models (21–123LOC,2–13relations),15universal-sufficient and12requiring existential solution in their presentations. Tools SWISS,IC3PO,FOL-IC3,DistAI,UPDR,I4, week cutoff. Fail,toolerror,Z3error,memout,timeout distinguished; no common success criterion should collapse these. Walltimes single reported numbers, no repeated-run distributions/seed sensitivity/memory measurements or solver-query-count ablations reported. Hardware paper reports DellPrecision5829,4.3GHz28-coreXeonW2175,62GBRAM,512GBSSDPro600p,Ubuntu18.04; reported core description preserved without independent hardware validation. Baselines configured with their documented settings: SWISS uses own published formula bounds per protocol; I4/IC3PO need finite-instance sizes, I4 starts minimum and increases on failure; FOL-IC3 runs universal/default modes and reports first success. Tablefootnotes attribute FOL-IC3Chord difference to threebugs in a competitor file and IC3PO successes to retrofitted protocols/manually supplied alternating clauses. These are DuoAI authors claims, not independently audited competitor defects or controlled equal-input performance results. Concurrent PFOLIC3 excluded from main comparison; its failure rates cited from other work, not own experiments. DuoAI solves26/27,15/15universal and11/12existential, fastest outright on15; SWISS19,IC3PO18,FOLIC318,DistAI14,UPDR14,I412. No competitor solves verticalPaxos here. Not every row is a speedup: Chord200.9s vsIC3PO17.1/DistAI58; locks/tablecontain subsecond differences and learning-ring alternatives. Paxos60.4s vsSWISS16665s(~275.91x),flexible78.7vs28337(~360.06x); comparison is measured selected tool/model configuration, not universal algorithmic superiority. Universal-only worker wins all15universal cases; top-down winsfive simpler existential cases and bottom-up wins hybridreliablebroadcast plusfivePaxosvariants. MultiPaxos615candidates/581alternating butonly2needed noncore; Paxos/flexible/multi/stoppable require subsetsize2,fastsize6. Vertical expert invariant8literals reduced7,60predicates/120signed gives search order120^7≈3.58e14; fast38predicates/5literals gives76^5≈2.54e9. These coarse powers are magnitude estimates ignoring syntax/equivalence, not measured exhaustive candidate counts. Implementation6.1KC++LOC(gcc7.5.0),2.3KPythonLOC(3.8.10) simulator. No machine-checked metatheory or independently executed artifact. Proof soundness/trust distinct from search completeness and practical automation; returned inductive safety certificates do not connect protocol abstraction to concurrent network code. Table1 has four IC3PO successes, three failures and five memory failures among the12existential rows. The §8,p.496 prose instead says six memory failures; the table, not that narrative count, is preserved in structured results. This discrepancy does not change IC3PO total18successes.
  • how much was read: most of it read
  • source; notes: papers inspected
  • record id: duoai-2022
• Endive (2022)
  • title: Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+
  • what: Samples candidate lemmas from a predicate grammar the user gives. Checks them on small finite instances. Greedily picks the lemmas that remove counterexamples to the induction step. A separate TLAPS proof is still needed for the protocol at unbounded size.
  • number: Invariant for 25 of 29 protocol benchmarks
  • number: Table I has 30 rows incl. MLDR; 2 rows have no TLA+ translation
  • number: Paper’s Endive rerun in IC3Syn solves 24 shared cases
  • number: endive solved 29 benchmark protocols plus MLDR; MLDR row: 2,025 s, 7,751 CTIs, 1,272 s checking, 651 eliminated, 102 s CTI generation (Table II)
  • limits: The generated invariant is not guaranteed to be truly inductive, because counterexamples are sampled at random. Needs a grammar from the user.
  • how much was read: most of it read
  • source; notes: Endive: TLA+ candidates, followed by an unbounded proof; notes: papers inspected
  • record id: endive-2022
• Invariant inference with quantifier alternations (2022)
  • title: Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion
  • what: Presents a PDR/IC3 invariant-inference algorithm that learns first-order invariants with quantifier alternations. It lifts quantifier-prefix choice to the inductive-generalization level for parallel breadth-first search, introduces k-term pseudo-DNF (k-pDNF) matrices, and combines EPR restrictions, incremental SMT, multi-block generalization and heuristic may-proof-obligations. The IG procedure partitions prefix space into categories/workers, orders prefixes by quantifier depth/alternations/universals/existentials, shares constraints only from immediate sub-prefixes, and interleaves separation with SMT checks of Init and relative inductiveness. k-pDNF represents a negated cube followed by up to k−1 cubes, expressing implication-shaped Paxos lemmas more compactly than CNF/DNF. The complete P-Fol-Ic3 algorithm has learning and heuristic tasks, optional EPR edge restrictions, and solver robustness via restarts, parallel Z3/CVC5, and incremental assertions. Evaluation covers 30 safe distributed-protocol problems, including Paxos variants, with ablations for pDNF, EPR, incremental SMT and multi-block generalization.
  • number: 30 benchmark problems
  • number: 5 trials per algorithm; 16 threads, 20 GiB RAM, 6-hour timeout
  • number: paxos-epr 920 s (5/5), flexible-paxos-epr 418 s (5/5), multi-paxos-epr 4272 s (4/5)
  • number: k=1 universal and k=3 non-universal pDNF settings
  • limits: Benchmarks are safe transition systems with known human invariants; inference success is not a refutation method for unsafe systems. EPR requires a user-provided acyclic set of allowed sort/function edges, and prenex separation may need a special push-down mode. Full FOL search can be intractable; the method failed vertical-paxos-epr and several hardest cases, and stochastic parallelism yields variable success. Experiments use fixed 6-hour timeouts and 16 threads/20 GiB; performance and learned lemmas depend on solver behavior, random seeds and prefix restrictions.
  • how much was read: most of it read
  • source; notes: P-FOL-IC3: full 30-model experiment recovered
  • record id: invariant-inference-with-quantifier-alternations-2022
• Learning to Find Proofs and Theorems by Learning to Refine Search Strategies: The Case of Loop Invariant Synthesis (2022)
  • what: Proposes self-training AlphaZero-style teacher and solver agents that refine generic nondeterministic programs for automated theorem proving without human proof examples. Demonstrates Looprl on loop-invariant synthesis: abductive strategy code defines a search space, a teacher generates constrained diverse Code2Inv problems, and a solver learns greedy action choices. On 132 single-loop C programs, trained policy solves 61.5% without backtracking versus 39.7% using an untrained-teacher dataset and 18.4% random actions; MCTS with the generic strategy solves all benchmarks but is not the learned no-search metric. Defines choose/event nondeterministic strategy operators, conditional generative teachers, abductive reasoning and bounded event rewards. A strategy induces an MDP whose choice points are actions; AlphaZero/MCTS policy and value heads refine both teacher and solver. Looprl compiles an OCaml DSL to RL environments, provides graph-format UI/debugging, integer-linear-arithmetic abduction, and parallel Gumbel AlphaZero. Teacher constraints include invariant shape, conditionals, usefulness of guard and equalities; solver reward penalizes proof steps. A complete run uses 20 teacher +20 solver iterations, 1.6M-parameter graph transformers, 50K solver training problems, and one16-hour RTX3080 run. Supplement findings: Appendix A expands the solver strategy to disjunctions of at most three atomic candidates, optional candidate strengthening, lazy constant metavariables with global constraints, and conjectures from preserved linear combinations, relaxed guards and unmodified initial variables. Conjecturing costs -0.3, abduction -0.2, each counted at most four times, with successful reward at least zero. Figure 7 provides all 94 lines of the strategy and a pending stack encoding. This makes the hand-designed search space and shaped reward explicit; the neural policy chooses within it. Appendix B/Table 3 lists 15 sampled constraint types; penalties are -0.5 except the last four at -0.2, and successful reward is at least -0.5. Table 4 hard constraints require correctness, nontrivial/nonredundant formulas, satisfiable invariants, entering the loop, and a restricted loop-terminates test. The paper explicitly says that test rules out only a subset of nontermination cases. It must not be described as a general termination guarantee. Constraint combinations and correlations are partly hardcoded; formula/program templates and parameter-abduction shape the generated distribution. Table 5 gives 12 final transformations, including irrelevant guards/formulas, commuting or shuffling instructions, comparison normalization, moving assumptions and weakening the final assertion. An application is cancelled if it violates a hard constraint or increases soft violations. Table 6 gives Code2Inv problems 3,7,93,110 and explanatory invariants: disjunctive x<5 or y≤z; x-y≤10; 3i=x+y with i≤n; i-s=1 with i≤n+1 or s=0. Table 7 prints three generated programs/invariants, with final transformations disabled for clarity and invariants hidden before solver training. They are illustrations, not additional held-out measurements. Appendix F uses Fourier–Motzkin elimination on negated CNF clauses in linear integer arithmetic. For a single clause, negations of derived consequences suggest sufficient assumptions; contradiction can prove validity. For multiple conjuncts, the implementation returns the union of clause-local suggestions rather than all conjunction combinations. F.2 explicitly withdraws the guarantee that any suggestion implies the entire input formula. Subsequent proof checks and recursive refinement matter; treating every abduction result as a complete proof would overstate the method. Table 8 specifies teacher 20×8000 generation episodes, 800 validation episodes/iteration, max 60 steps, 64 MCTS simulations; solver 20×20000 episodes, 5000 validation/iteration, max 12 steps, 32 simulations. Both use 600 asynchronous/parallel episodes, 128-dimensional embeddings, four attention heads, 6 state/3 action/1 combiner blocks, state/action encoding limits 80/12, 16 identifier IDs and 256-node MCTS cap. Teacher/solver dropout is 0.05/0.1, batch size 400/300, learning-rate maximum 5e-4/3e-4, maximum epochs 6/1. The last five teacher iterations and 10000 extra noiseless generated problems supply solver problems. The 20000 solver episodes per iteration are distinct from the inherited 50000-problem training pool. Appendix H uses separate Dynamic Graph Transformers for state probe and each action, a combiner for softmax action scores, and a value head for outcome/event predictions. AST Polish-order tokens retain syntactic edges, data/control-dependence edges and numerical comparison edges. Identifier IDs are randomized per choice point; overflow names share a flagged ID. H.2 describes binary constant encoding generally, but Table 8 sets const-emb-size=0 for both reported agents, disabling that binary value encoding. Numerical comparison edges remain enabled. Search exceeding state/action/step limits fails or discards actions; no unrestricted completeness claim follows. Figures 8–9 expose policy probabilities, outcome/event estimates and MCTS statistics. The solver example gives prior 0.81 for abduct x>0 and predicted value 0.46 versus described true shaped reward 0.4; teacher screenshot predicts success 0.97 and soft-constraint violation risk 0.31. These are individual UI examples, not calibration experiments. Figure 7 as printed has inconsistent/unbound names in prove_preserved (suggs/assum/action) and proved_invs versus invs_proved; it is explanatory pseudocode, not a standalone executable listing. No author code was inspected to resolve the differences.
  • limits: The proof domain is Code2Inv:132 C programs with one loop, linear integer arithmetic and selected conditionals/assumptions/nondeterministic tests. The authors leave other domains for future work; general theorem-proving claims are a design vision, not demonstrated coverage. The learned result evaluates greedy highest-policy actions with no search/backtracking. It measures ability to generate an invariant of minimal size; MCTS can solve all benchmark problems, so no-search success is the reported challenge. An invariant is accepted through the benchmark/verifier pipeline; the paper does not establish semantic robustness beyond those checks. Teacher generation uses manually defined constraints and validity-preserving transformations. Constraints can be incompatible; rewards are shaped so success beats failure. Generated problem distribution and benchmark generalization depend on strategy design, not an unrestricted theorem distribution. Training protocol uses two random seeds for error intervals; one complete run takes about16h on specified hardware. No comparison across many independent training runs, hardware settings or random datasets is reported. The approach formalizes expert strategy fragments and learns choices; it does not produce Lean/Coq/Rust/Verus proof terms or TLA+ specifications in this paper. Appendix B/Table 3 lists 15 sampled constraint types; penalties are -0.5 except the last four at -0.2, and successful reward is at least -0.5. Table 4 hard constraints require correctness, nontrivial/nonredundant formulas, satisfiable invariants, entering the loop, and a restricted loop-terminates test. The paper explicitly says that test rules out only a subset of nontermination cases. It must not be described as a general termination guarantee. Constraint combinations and correlations are partly hardcoded; formula/program templates and parameter-abduction shape the generated distribution. Appendix F uses Fourier–Motzkin elimination on negated CNF clauses in linear integer arithmetic. For a single clause, negations of derived consequences suggest sufficient assumptions; contradiction can prove validity. For multiple conjuncts, the implementation returns the union of clause-local suggestions rather than all conjunction combinations. F.2 explicitly withdraws the guarantee that any suggestion implies the entire input formula. Subsequent proof checks and recursive refinement matter; treating every abduction result as a complete proof would overstate the method. Appendix H uses separate Dynamic Graph Transformers for state probe and each action, a combiner for softmax action scores, and a value head for outcome/event predictions. AST Polish-order tokens retain syntactic edges, data/control-dependence edges and numerical comparison edges. Identifier IDs are randomized per choice point; overflow names share a flagged ID. H.2 describes binary constant encoding generally, but Table 8 sets const-emb-size=0 for both reported agents, disabling that binary value encoding. Numerical comparison edges remain enabled. Search exceeding state/action/step limits fails or discards actions; no unrestricted completeness claim follows.
  • how much was read: most of it read
  • record id: learning-to-find-proofs-2022
• NIS data-driven invariant synthesis (2022)
  • title: Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes.
  • what: Extends ICE-DT invariant learning with data-driven generation of linear attributes: positive/negative/implication samples are covered by join-maximal separators represented in interval, octagon or polyhedral abstract domains. The paper defines inductive safety conditions and ICE samples, explains decision-tree learning with implication closure, and introduces separator construction that joins convex abstract objects covering positive states while excluding negatives. Algorithm 4 computes a join-maximal separator; Algorithms 5–6 incrementally reuse separator stacks and parent indices when counterexamples arrive. Examples show the learned invariants evolve from simple equalities to disjunctive loop invariants. The C++ NIS prototype uses Z3 and APRON and solves 154/164 SyGuS-Comp LIA programs with polyhedra and 160/164 using a virtual best across intervals/octagons/polyhedra, outperforming enumerative ICE-DT/LoopInvGen in many cases while remaining complementary across domains.
  • number: 164 LIA programs, 2–10 variables
  • number: NIS(poly) solves 154/164; virtual best 160/164
  • number: 1,800 s timeout; 16-core Xeon, 128 GB RAM
  • number: three abstract domains: intervals, octagons, polyhedra
  • limits: The method targets linear integer arithmetic and predicates expressible through the selected numerical abstract domain; quantifier-heavy cases are unsupported. ICE learning is not guaranteed to terminate, and performance depends on SMT counterexample choices. Polyhedra joins can be expensive, while intervals/octagons are less expressive; benchmark programs exclude boolean encodings and useless-variable cases. Results are bounded by the 1,800-second timeout and SyGuS-Comp sample, with no proof that generated invariants are complete for arbitrary programs.
  • how much was read: most of it read
  • source
  • record id: nis-data-driven-invariant-synthesis-2022
• SpecFuzzer (2022)
  • title: Fuzzing Class Specifications (SpecFuzzer)
  • what: Infers likely class invariants for Java. It fuzzes a fixed grammar of assertions, filters candidates with Daikon against Randoop tests, and ranks them by how many mutants they kill.
  • number: 65 ground-truth assertions over 43 methods; up to 500 tests and 2,000 candidates per run, 10 runs, 90-minute timeout
  • number: 20,277 assertions before selection, 975 after (95.1% reduction)
  • number: 34/65 recall (52.3%), precision 65.8%, F1 0.57; GAssert 92.3%/27.6%/0.42; EvoSpex 88.5%/38.4%/0.53
  • number: Evaluation on 43 methods and 65 ground-truth assertions; 20,277 assertions before selection, 975 after (95.1% reduction)
  • limits: The output is likely invariants consistent with the tests, not proofs. The authors wrote the ground truth. Choosing by mutants can discard valid assertions. The intro’s 75% claim is not supported by the tables.
  • how much was read: most of it read
  • source; notes: Fuzzing Class Specifications (SpecFuzzer), Molina et al., ICSE 2022; notes: Fuzzing Class Specifications (SpecFuzzer), Molina et al., ICSE 2022
  • record id: specfuzzer-2022
• Bridging arrays and ADTs in recursive proofs (2021)
  • what: Presents a fully automatic method for synthesizing recursively defined relational invariants that prove equivalence of paired object implementations when one uses arrays and the other algebraic data types (ADTs). The method encodes initialization, paired transitions, applicability and output equality as CHCs; Algorithm 1 builds a recursive invariant schema, Algorithm 2/3 bridge producer/consumer operations for linear scans, and Algorithm 4/5 use noop observations for sets/maps. Candidate relations are validated by structural induction with AdtInd/Z3. The paper formalizes equivalence as an inductive invariant over a composition of two deterministic objects, with initialization, consecution for every paired operation, precondition applicability in both directions, and output equality. It defines producer/consumer/noop classifications via a partial ordering on ADT states and synthesizes a Skolem-like updated array state plus matching constraints. Recipe 1 handles stacks/queues with an index and can infer loop invariants; Recipe 2 handles sets, multisets and maps by updating only the observed array cell while preserving all other inputs. Validation is structural induction rather than recursion-free SMT checking, and user lemmas are optional (one multiset lemma was needed in evaluation).
  • number: 10 benchmark variants in Table 1
  • number: stack 2.81 s and queue 40.61–42.18 s
  • number: set 2.12/19.24 s; multiset 32.62/3.59 s; map 1.95/5.83 s
  • number: MacBook Pro 2 GHz Intel Core i5, 8 GB RAM
  • limits: Objects are modeled syntactically as predicates obtained from symbolic execution; loop effects must already be expressed as quantified formulas. Programs are deterministic and each enabled precondition has a successor/output. The approach targets finite sets of operations and list-shaped ADTs; it assumes suitable classifications/recipes and SMT quantifier-elimination/array reasoning. CHC solving is undecidable in general, proof search can dominate runtime, and the evaluation is textbook data structures rather than large real software. The method requires monotonic/structural-induction support in AdtInd and may need user lemmas for harder cases.
  • how much was read: most of it read
  • source
  • record id: bridging-arrays-and-adts-in-recursive-proofs-2021
• Diffy: Inductive Reasoning of Array Programs Using Difference Invariants (2021)
  • what: Diffy verifies selected parameterized array programs by induction on positive array-size parameter N. It splits PN into QN-1 plus a peeled suffix, relates QN-1 to PN-1 through product-program difference invariants, transfers the smaller-program postcondition, and verifies the peel with iterative strengthening or recursively reduced loop nesting. At60seconds it proves151/157 safe cases and detects142/146 unsafe cases on an enhanced303-program suite. Distinguishes QN-1 (only loop bounds truncated, with data-dependency repairs) from PN-1 (all N replaced), explains required precondition splitting and cross-program coverage, records conditional peel simplification and failed loop propagation, and retains the strengthen-transfer obligation rather than treating arbitrary quantifier elimination as sufficient. Complete category results, timeout sensitivity, baseline wins and source formula/indexing gaps qualify headline superiority.
  • limits: §3: program grammar has scalar/array assignments, conditions, sequential composition and well-nested for loops, each with a unique counter initialized0 and incremented1, never assigned by the body. Upper bounds use N, constants and enclosing counters, not arbitrary mutable data. N is a positive integer size parameter. It does not cover arbitrary C pointers, concurrency, recursion or distributed failures. §3: properties are universal arithmetic-index guards implying quantifier-free array/integer arithmetic predicates, or quantifier-free formulas. Scalars and arrays undergo SSA renaming, including separate array versions per loop and distinct writes. The mathematical domain is integers/arrays; the paper does not establish C overflow, pointer aliasing, division edge cases or machine memory-safety semantics end to end. §§2,4.1: PN-1 replaces all occurrences of N by N-1; QN-1 truncates loop-bound N while preserving data-expression N, then repairs uses affected by moving peels. Correct construction must establish PN semantically equivalent to QN-1;peel(PN). It is not enough to append last iterations without propagating all data/control dependencies. §4.1: nested-loop exposition assumes inner-body writes are not used later in outer fragments, and outer writes used by the inner body are not overwritten again. Relaxations are delegated to extended[13]. Algorithm1 aborts a needed substitution from a peel that is still a loop; implementation sometimes uses closed-form summaries, unused-write reasoning or conservative overapproximation. Thus it does not automatically transform every grammar-accepted nested array program. §4.1/Lemma1: strictly smaller maximum nesting depth is proved for linear upper bounds in N/enclosing counters, whose difference on replacing N by N-1 is constant. Corollary that a nonnested program has loop-free peel inherits conditions; general nonlinear bounds need not yield constant many peeled iterations. Missed-iteration construction also needs sensible nonnegative ordered bounds; grammar alone does not state all monotonicity/boundary conditions. The theorem should not be generalized to arbitrary decreasing/negative bounds without additional validation. §4.2: phi(N) must imply phi-prime(N-1) and delta-phi-prime(N), with split remainder facts not modified by PN-1/QN-1 as needed. For conjunction over indices0..N-1, restrict only index range for phi-prime and retain N inside each conjunct; remainder is last-index conjunct if untouched. If no iterated conjunction, proposed default is phi-prime=phi(N),delta=True. Correct input coupling between the two program runs is essential. §4.3: product graph has synchronized loop iteration structure; corresponding branches synchronize only after establishing equivalent guards, otherwise all four branch pairs are considered. Dataflow tracks equalities and disjunctions of equalities between corresponding variables/array elements at loop heads/exits/branches. At-most-quadratic N expressions are an experimental observation, not a theorem for arbitrary programs. Interval inequalities and template guess/check are possible extensions, not evaluated implemented capabilities. §§2,4.4: transferred postcondition is exists VP: psi(N-1) and D(VQ,VP,N-1). Equality substitution can eliminate VP, or SMT quantifier elimination is used. Stronger peel preconditions need corresponding original-program strengthenings satisfying xi(N) and D implies xi-prime(N). The paper explicitly notes this can require logical abduction; arbitrary existential projection over VQ does not by itself establish that universal transfer implication for nondeterministic/nonfunctional D. §4.4/Theorem2: soundness is conditional on valid original strengthened bases1..M, valid xi-and-D transfer for allN, sound program/precondition transformation and valid strengthened peel Hoare triple. Paper states Theorem1/equivalence and Theorem2/soundness without full proofs here; only nesting lemma has an explicit proof. No mechanized proof of transformation/dataflow/LLVM implementation or independently checked proof certificate is reported. §4.4/Algorithm2: initial base N1 failure reports counterexample; later inability to strengthen, invalid strengthening base or timeout returns False meaning unable to prove. A failed induction step or spurious strengthening is not evidence of an original-program counterexample. Text allows checking small fixed N values; unsafe detection is incomplete for bugs appearing only beyond checked sizes. Parameter induction proves safety obligations, not a stated total-correctness/termination theorem. §§2,4.4: strengthening iteration need not converge, and tool uses timeout. If weakest precondition cannot be obtained and peel has a loop, recursion invokes Diffy on the peel; the nesting argument is conditional as above. Difference invariants are postcondition independent and reusable, but strengthening is property dependent. Printed source issues, visually confirmed: Algorithm1 line4 ranges loop indices throughN though line1 givesm loops; line16 usesLi in helper parameterizedL. Algorithm2 shifts D argumentsN-1/N and line22 references chi-prime(N) while line16 computed chi-prime(N-1); prose points to line6 for elimination actually at22. These are schematic/indexing gaps, not verified implementation bugs. Printed example issues: §4.3 calls forall i in0..N-1:a-prime[i]-a[i]=1 a first-loop-head invariant, omitting the processed-prefix restriction or entry relation that would make it valid before all writes. §4.4 p927 prints peel precondition x-prime=(N-1)^3; for Fig2 peel x:=x+N^2 and final b[N-1]=x+N-1, required pre-peel x is N^3-N^2=(N-1)N^2. Thus displayed primed formula cannot be accepted literally with the shown update; this does not establish unsoundness of the tool source, which was not audited. §5: C++ prototype,LLVM6.0.0,Z3 4.8.7; benchmarks on i7-6500U2.5GHz,16GB,Ubuntu18.04.5. ComparatorsVajra1.0,VIAP1.1,VeriAbs1.4.1-12. Main timeout60s. No repeated-run variability, independent proof replay, random sampling or broad production-corpus evaluation supplied. §5:303 benchmarks combine entire prior Vajra suite with added challenging cases;157safe/146unsafe. C1 has no N-dependent branches,modulo or nesting; C2 has N-dependent branches/modulo without nesting; C3 has nesting. Success on this designed suite is not superiority on all SV-COMP submissions or arbitrary C array programs. Unsafe cases are described as unsafe versions of safe examples, not an independent production bug sample. §5/Table1:Diffy151safe with3inconclusive/3timeouts,142unsafe with4inconclusive;Vajra110safe/115unsafe;VeriAbs110safe/125unsafe;VIAP20safe/120unsafe. Diffy proves all safe benchmarks proved by Vajra/VIAP within 60 seconds but not VeriAbs: VeriAbs proves2C2+3C3 safe cases Diffy misses. These paired wins support portfolio use; totals alone hide complementarity. §5:3Diffy safe timeouts arise in modulus induction SMT queries;3safe inconclusive cases lack predicates. At100seconds Diffy/Vajra/VeriAbs outcomes remain unchanged, VIAP additionally proves89safe C1/C2 cases (reader total109), unsafe counts unchanged. The earlier claim VIAP takes70seconds more on average is not compatible with a straightforward60second completed-run comparison; aggregation/set/budget is unspecified. Do not present it as a verified common-instance speedup. §§6–7: existential-property generalizations and relaxed nested restrictions are delegated to extended arXiv paper, not read here. Synthesis of difference invariants remains future work. No Rust/Verus/TLA+ result, protocol/network model or LLM use/evaluation is reported. Artifact DOI10.6084/m9.figshare.14509467 not run.
  • how much was read: most of it read
  • source
  • record id: diffy-inductive-reasoning-of-2021
• DistAI repository (2021)
  • title: DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols
  • what: DistAI simulates a protocol, learns candidate invariants from traces, and refines them with Ivy and Z3 counterexamples until validated. The README gives commands for two-phase commit, distributed lock, database chain replication and blockchain.
  • number: solves 13 of 14 protocols; Paxos fails
  • number: verifies 13 common distributed protocols automatically
  • number: 14 protocols
  • number: Suite: 14 distributed protocols written in Ivy (e.g. Paxos, two-phase commit, Chord, Ricart-Agrawala)
  • limits: The README warns that its parser does not support the full Ivy 1.7 grammar; repository instructions and reported outputs were not rerun.
  • how much was read: most of it read
  • source
  • record id: distai-repository-2021
• IC3PO symmetry verifier (2021)
  • title: On Symmetry and Quantification: A New Approach to Verify Distributed Protocols
  • what: Introduces IC3PO, symmetric incremental induction extending finite-domain IC3/PDR. It infers the quantifier prefix of inductive invariants from protocol symmetries, then finds a finite cutoff whose proof generalizes to all instance sizes. Logical orbits map symmetry classes to quantified clauses; symmetry-aware clause boosting avoids searching fixed quantifier templates. A cutoff procedure checks that orbit representatives cover all relevant instances. IC3PO handles universal/existential alternations and produces compact quantified invariants automatically.
  • number: Evaluation set 29 protocols; IC3PO solved all 29, versus I4 13, UPDR 14, fol-ic3 23
  • number: 10 protocols solved by all: IC3PO total 232s/85 invariant assertions/12,160 SMT queries
  • number: IC3PO 1-hour timeout, 32GB memory, Intel Xeon X5670; Z3/Yices/CVC4 backends
  • number: ToyConsensus(3,3,3): IC3PO 192 SMT calls and 13 CTIs versus I4 7,814 calls and 443 CTIs
  • limits: Focuses on parameterized protocols whose sorts are sets of indistinguishable constants; ordered sorts and integer arithmetic are future work. Safety only, not liveness. Finite cutoff correctness depends on symmetry assumptions; evaluation uses bounded protocol models and SMT solver timeouts.
  • how much was read: most of it read
  • source; notes: papers inspected
  • record id: ic3po-symmetry-verifier-2021
• Invariant barrier certificates via DCP (2021)
  • title: Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming.
  • what: Defines an invariant barrier-certificate condition equivalent to inductive invariance for polynomial differential systems, reduces synthesis to BMI optimization using SOS/Putinar certificates, and solves BMIs with difference-of-convex iterations plus branch-and-bound. The paper derives finite Lie-derivative conditions, SOS encodings, BMI objective maximization, eigendecomposition-based psd-convex difference decomposition, and linearized LMI subproblems whose feasible sets under-approximate the original BMI constraints. It proves local convergence and a weak completeness theorem when a strictly valid template parameter exists and the partition/degrees are sufficiently fine. A branch-and-bound algorithm searches coefficient space, with pruning based on visited projections and negative objectives. The worked nonlinear ODE example obtains B(x)=−0.00363421x2; benchmarks compare BMI-DC, PENLAB, and SOSTOOLS with posterior Mathematica/Z3 validity checks.
  • number: 23 benchmark examples
  • number: 2.10 GHz Xeon, 376 GB RAM
  • number: 100 iterations in focus case
  • number: B(x)=−0.00363421x2 worked certificate
  • limits: Systems are autonomous polynomial ODEs with unique maximal trajectories; templates, multiplier degrees, and SOS degrees are fixed. DCP alone reaches only local optima, while branch-and-bound can be exponentially large and needs a strict-validity neighborhood for weak completeness. Numerical roundoff requires posterior validity checking; several high-dimensional examples were inconclusive, and the CAV version omits proof and benchmark details delegated to an extended version.
  • how much was read: most of it read
  • source
  • record id: invariant-barrier-certificates-via-dcp-2021
• MongoRaftReconfig TLA+ verification (2021)
  • title: Formal Verification of a Distributed Dynamic Reconfiguration Protocol
  • what: Machine-checks a TLA+ inductive invariant and TLAPS safety proofs for MongoRaftReconfig, proving LeaderCompleteness and StateMachineSafety for MongoDB Raft-based dynamic reconfiguration. Presents 359-line protocol spec, 140-line 20-conjunct invariant, decomposition into 160 proof goals, detailed TLAPS proof example, TLC-assisted invariant discovery, proof statistics and limitations.
  • number: 3189 lines TLA+ total
  • number: 359 lines protocol specification
  • number: 140 lines invariant
  • number: 20 invariant conjuncts
  • limits: Specification deliberately abstracts lower-level implementation details; finite TLC invariant search is probabilistic and not itself a proof. Safety only; liveness left future work. TLAPS backend solver can fail without distinguishing false from hard obligations; no verified runnable implementation. Full TLA+ and proof code supplied as supplementary material.
  • how much was read: most of it read
  • source
  • record id: mongoraftreconfig-tla-verification-2021
• Neural barrier certificate synthesis (2021)
  • title: Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models.
  • what: Presents a counterexample-guided inductive synthesis loop in which a neural network is trained as a barrier certificate and an SMT verifier proves its safety conditions or returns counterexamples. The paper states the barrier conditions (initial set non-positive, unsafe set positive, negative Lie derivative on the zero level set), translates trained networks symbolically, and adds bespoke losses, polynomial/tanh/sigmoid/ReLU architectures, prioritized and multiple counterexample generation, and numerical-robustness measures. It handles polynomial and transcendental ODEs, a piecewise hybrid model, and 4/6/8-dimensional ODEs. The CEGIS loop is sound when SMT returns unsat, but not complete; it retains weights and augments samples after each counterexample. SOS candidates are often numerically ill-conditioned and fail SMT verification.
  • number: 8 benchmarks; at most 9 CEGIS iterations
  • number: 0.5k–2.3k initial samples
  • number: up to 0.1% of prior method’s data
  • number: 50 randomized runs
  • limits: Models are continuous ODEs or a specified hybrid partition with continuous vector fields; the certificate must be differentiable and satisfy strict inequalities. SMT dReal uses δ=10^-6 and Z3 handles polynomial cases; timeout and architecture choices affect success. CEGIS may not terminate or find a certificate, random initialization causes high variance (8% success on the polynomial model and 12% on 8-D over 50 runs), and SOS comparisons are unsound unless separately verified.
  • how much was read: most of it read
  • source
  • record id: neural-barrier-certificate-synthesis-2021
• NRA Model Interpolation (2021)
  • title: Interpolation and Model Checking for Nonlinear Arithmetic
  • what: Introduces model interpolation through an SMT-modulo-partial-model API, implements it in MCSAT/Yices2, and uses it for invariant inference in nonlinear-arithmetic model checking. Algorithm 1 enumerates models of B and asks A for model interpolants that refute each model; finite convergence yields a Craig interpolant. The MCSAT implementation generalizes models with cylindrical-algebraic-decomposition cells, supporting complete nonlinear real arithmetic interpolation and PDR-style invariant inference. A Cauchy–Schwarz inequality is encoded as a transition-system invariant.
  • number: pdkind solves 82/114 benchmarks (59 valid, 23 invalid) in 1,971 s total; ic3-nra solves 73 (58/15) in 986 s; kind solves 48 (24/24) in 855 s
  • number: pdkind proves 59 properties, including 36 not proved by kind; it finds 23 invalid properties
  • number: pdkind proves 11 properties ic3-nra cannot, while ic3-nra proves 10 pdkind cannot
  • number: Cauchy–Schwarz property proved valid by pdkind in 1 s
  • limits: Completeness is limited to theories supported by MCSAT. Termination depends on finite convergence of model interpolation. CAD-derived interpolants can be large clausal formulas; unlike interval methods, the procedure does not cover arbitrary functions/ODEs. Experimental comparison uses one-hour CPU timeouts and only the selected benchmark suite.
  • how much was read: most of it read
  • record id: nra-model-interpolation-2021
• Porous invariants (2021)
  • what: Defines porous invariants for branching integer affine loops: structured semilinear sets that may have infinitely many holes. The paper computes strongest real-linear and integer-linear invariants, gives reachability and separator results for several target/system classes, proves undecidability in high-dimensional nondeterministic systems, and implements a complete one-dimensional affine procedure.
  • number: Theorem 5: undecidable with two 91-dimensional matrices
  • number: 8,128 random instances; 1,160 unreachable and 6,968 reachable
  • number: all instances built invariants; mean 0.209 s, maximum 20.252 s
  • number: all unreachable proofs; 5,828/6,968 reachable direct proofs within ~30 s
  • limits: The systems are integer LDSs with finitely many linear matrices, or one-dimensional affine maps. N-semilinear sets are Presburger-definable, so multiplication is unavailable in the invariant language. Full-dimensional Z-linear target reachability is decidable, but non-full-dimensional targets can be Skolem-hard or undecidable; N-semilinear invariant synthesis is undecidable for nondeterministic systems with two 91-dimensional matrices. The one-dimensional procedure is polynomial only with unary encoding; binary reachability is NP-hard and generated intervals can be exponentially large. Applicability to nested loops and richer specifications remains open.
  • how much was read: most of it read
  • record id: porous-invariants-2021
• SWISS (2021)
  • title: Finding Invariants of Distributed Systems: It’s a Small (Enough) World After All
  • what: SWISS searches finite spaces of quantified invariants for RML distributed protocol models. Breadth accumulates small relatively inductive clauses; Finisher searches for a final clause that, with safety, is inductive. Failed SMT verification conditions yield reusable finite-model filters, with symmetry and redundancy pruning, model minimization and parallel search. It proves selected models including Paxos/Flexible Paxos and guided Multi-Paxos, and measures successes, partial progress, costs and failed optimizations against I4 and first-order separators. Reconstructs exact Finisher/Breadth obligations, conditional coverage guarantee and its implementation timeout exception, all three counterexample filters and fast bitset/trie evaluations. Saves every benchmark/table number and failed-protocol result, manual search tuning, full-space versus first-hit timing and all appendix ablations. Distinguishes model/spec correctness from code, safety-relative partial clauses from independent proofs, and the small-world hypothesis from general completeness.
  • number: solves 19 of 27 benchmarks with a six-hour timeout, median of five runs
  • number: Paxos and Flexible Paxos take about 4.4 and 5.1 hours
  • number: Multi-Paxos succeeds only with supplied templates
  • number: Paxos: around 4 hours on an 8-core machine; with guidance 20 minutes
  • limits: §§2–3: Inputs are a formal RML protocol transition system, desired safety condition and candidate-space configuration. No executable implementation/refinement theorem is supplied. Encoding an intended protocol so checks remain in extended EPR may itself be challenging and is explicitly outside SWISS scope. Safety/transition semantics, solver/encoder/filter implementation and execution environment are trusted; output invariants can be independently validated but this reading did not replay them. §§2.1–2.4: Proofs address all reachable states of the supplied transition model, not just finite test runs; no liveness proof. Atomic transition/failure/network assumptions come from each input protocol. SDL running example uniquely disallows packet duplication; do not generalize that restriction to every benchmark. EPR satisfiability uses ∃∀ with no general functions; stratified functions and quantifier alternation are admitted in the extended fragment while preserving decidability. §§3.2–3.4: Finisher checks Init⇒S, Init⇒P, TR∧known∧S∧P⇒S′ and TR∧known∧S∧P⇒P′. Breadth checks initialization and inductiveness of new clauses relative to input clauses and S. Therefore intermediate clauses can be inductive only under safety, not independently proved reachable-state properties. Reader qualification: reuse partial output with its assumptions/joint invariant obligation intact; a partial clause count is not a partial correctness theorem about arbitrary code. §3.4 Claim 1: Ideal Solve succeeds only if a finite chain exists with all earlier clauses in B, final clause in F, each earlier prefix inductive relative to S, and final conjunction including S inductive; sound pruning must preserve valid candidates and VC checks must finish. This is relative completeness for the stated chain/space, not decidability of arbitrary invariant discovery. §§4.3,5.1 reader qualification: Actual implementation retries timed-out Z3 queries with CVC4 and may skip an invariant if timeout persists. Thus practical runs with skipped candidates do not retain the ideal exhaustive coverage guarantee. Skipping rejects potentially useful proofs; it does not justify accepting an unproved candidate. Unknown/timeout and finite search failure do not establish protocol unsafety. §4.1: User supplies formula term/depth limits k,d, quantified-variable limits m,q and quantifier type nesting order to retain extended-EPR VCs. Templates can be auto-enumerated within bounds or explicitly supplied. Auto mode is not no-user-configuration; search grows exponentially. Symmetry pruning imposes syntactic term order/first-variable order, not full logical-equivalence solving. §4.2: True(M) requires P on a model; False(M) requires not-P; Transition(M,M′) requires P(M)⇒P(M′). Filters are derived from failed VC obligations and are sound for candidates satisfying the same obligation context. False models need not be reachable; they are states every acceptable strengthening for that VC must reject, rather than arbitrary actual executions proving a bug. §§4.2–4.5: Precompute base-term evaluations on every variable instantiation in finite models and evaluate candidates with bitwise operations. FastImplies is a sound but incomplete syntactic implication check using subsequences/modulo variable renaming in a trie, with limited universal/existential substitution. allInv retains redundant clauses for filtering while indInv avoids redundant output. Model minimization has a 45-second budget, so a retained model need only be partially minimized. §4.5.2: Partition/randomize B/F and run independent per-thread searches, combining only phase results. Threads do not share counterexample filters or fresh invariants during a phase. This gives good filtering parallelism but replicates SMT model construction and does not establish universal linear speedup. §5.1: Defaults B(d,k,q,m)=(1,3,1,5), F=(2,6,1,6) were adjusted per benchmark after results: increase k/q on exhausted failed searches, shrink B on slow breadth. learning-switch-ternary uses q=0; async lock and sharded-kv enlarge k; no-lost-keys needs q=2. Results include manual tuning and guided Multi-Paxos, not a fixed blind default-only experiment. §§5.1–5.2 Table 1: 27 distinct benchmarks plus duplicate guided Multi-Paxos row. SWISS times are medians of five runs with six-hour budget, on eight-core i9-9900K 3.60GHz/125GB/Ubuntu19.10, eight threads unless noted. Z3 4.8.8 then CVC4 1.8-prerelease –finite-model-find after 45s. Baseline runtime entries are published comparisons without uniform per-baseline dispersion in this paper. §5.2.1: Paxos and Flexible Paxos complete automatically within the configured candidate templates; Multi-Paxos requires correct user templates and unguided run times out in Breadth. Fast/Stoppable/Vertical Paxos remain unsolved, despite introductory phrasing that can sound broader. I4/FOL/SWISS each win on some protocols; existential support alone does not dominate larger mutually inductive universal invariants. §5.2.2: Partial progress counts handwritten invariant clauses logically implied by generated clauses, not percent of execution space, correctness or remaining proof effort. Missing one essential clause can prevent the whole safety proof. Reported 79% Vertical Paxos is 14/17, about 82.4%; preserve printed discrepancy rather than treating prose percentage as exact. §§5.3.3–5.3.5: Table 2 timings enumerate entire template spaces even after finding a proof and start with supplied Breadth invariants. The claimed 20-minute/13.4× guided result concerns proof search stopping, not the listed 2036-second full-template enumeration. Table 3 is a single-thread single-template pruning experiment, not end-to-end automatic-template run. §5.3.4: mn/mn−1 are smallest known chain maximum term sizes, drawn from human or synthesized invariants; minimality is not proved. 25/27 have mn≤8 and 22 are smaller; mn≤6/mn−1≤3 is an empirical rule of thumb. Human comprehensibility implies finite intuition is motivation for a hypothesis, not a theorem guaranteeing succinct invariants. Appendices A–B: Formula-synthesis, BMC and eager invariant accumulation were unfavorable in tested cases; this is workload-specific evidence. Figure 5 uses preselected templates and a logarithmic y-axis. Parallelism experiments deliberately finish the whole F space to remove first-hit variance and analyze longest-running threads, so speedups do not directly imply normal first-proof latency. §§5–7: No production-code performance, LLM-agent experiment, verified Rust/Verus implementation or TLA+/TLC integration is evaluated. An unexpectedly easy Fast Paxos proof uncovered a disabled-action typo in the input spec, demonstrating the need to validate intended behavior despite valid invariants. External artifacts/proofs and source-code current state were not executed or audited.
  • how much was read: most of it read
  • source; notes: papers inspected
  • record id: swiss-2021
• AVR (2020)
  • title: AVR: Abstractly Verifying Reachability.
  • what: Presents AVR, a push-button word-level model checker for source-level transition systems. It combines syntax-guided abstraction/refinement with word-level IC3, SMT backends, BMC and interpolation, and emits independently checkable inductive-invariant certificates or BTOR2 counterexample witnesses. The paper details AVR architecture and interfaces (Verilog/Yosys, VMT/MathSAT, BTOR2/Btor2Tools), IC3+SA abstraction atoms, incremental refinement and caching, data abstraction, property-directed splitting, interpolation and extract/concat handling. Proof certificates are SMT-LIB inductive invariants externally checked by Z3/Yices; failed properties produce simulator-checkable BTOR2 traces. A multi-engine proof race runs configurations in parallel. Case studies cover patched Apache buffer overflows, Needham–Schroeder authentication, and finite-to-unbounded distributed-protocol invariant generalization.
  • number: less than one minute for each Apache case
  • number: 3 initiators and 3 responders in Needham–Schroeder instance
  • number: HWMCC 2019 single-bit-vector track
  • limits: Targets primarily safety properties over quantifier-free bit-vectors, arrays, uninterpreted functions and linear integer arithmetic. Word-level abstraction can be ineffective when bit-precise data dominates; current support is limited for nonlinear arithmetic, floating point, quantifiers, liveness and fairness. Distributed-protocol generalization is preliminary and requires human/generalization reasoning beyond finite AVR runs. Certificates rely on an external SMT checker and traces on a witness simulator.
  • how much was read: most of it read
  • source
  • record id: avr-2020
• CLN2INV (2020)
  • title: CLN2INV: Learning Loop Invariants with Continuous Logic Networks
  • what: It trains continuous logic networks on execution traces to propose loop invariants (facts that hold at every pass through a loop). It extracts SMT formulas from them. Z3 then checks the three conditions that make an invariant inductive: it holds at the start, each step preserves it, and it implies the goal.
  • number: solves all 124 valid tasks in one hour each; LoopInvGen 104, Code2Inv 90
  • number: average time 1.07 s vs 45.11 s and 266.71 s; 31.77 Z3 calls vs 3,605.43 and 16.62
  • number: without learning still solves 91 tasks
  • number: 12 extra author-built harder tasks solved; degree three to five polynomial representations fail
  • limits: It gives partial correctness of the source program only (if it finishes, the result is right). It does not handle nested loops. The trace bounds (50 iterations, width 10) limit what is learned. They do not limit the proof. The result that training reaches the global optimum holds only for linear equalities. Nine invalid Code2Inv tasks were removed.
  • how much was read: most of it read
  • source; notes: CLN2INV: Learning Loop Invariants with Continuous Logic Networks, Ryan; notes: CLN2INV: Learning Loop Invariants with Continuous Logic Networks, Ryan
  • record id: cln2inv-2020
• Code2Inv (2020)
  • title: Code2Inv: A Deep Learning Framework for Program Verification.
  • what: A neural network learns candidate loop invariants (facts true on every pass through a loop) from solver feedback. It is given an assertion, a checker, a grammar and rules for building graphs.
  • number: 133 C programs and 120 CHC instances
  • number: 94 of 120 CHC solved vs Spacer 112 and LinearArbitrary 118
  • number: 5 of 7 on a nonlinear case study
  • number: 90% of solved C cases within two hours, rest up to twelve
  • limits: It excludes programs with multiple loops, calls or recursion. It needs a predefined grammar and a long search budget.
  • how much was read: most of it read
  • source; notes: Code2Inv: A Deep Learning Framework for Program Verification
  • record id: code2inv-2020
• Config2Spec: Mining Network Specifications from Network Configurations (2020)
  • what: Config2Spec mines every policy in a chosen finite policy language that holds for all link-failure environments allowed by a model. It intersects policies inferred from sampled forwarding states with a candidate set, then uses grouped symbolic control-plane queries to verify remaining policies or produce counterexamples. Two runtime predictors choose between sampling and verification; policy-aware sampling, topology cuts and prefix grouping reduce work. A handwritten argument establishes exactness and termination conditional on exact terminating component tools and correct environment enumeration. Evaluation measures runtime, query reduction and specification size. Records the candidate/specification/verified invariant, universal failure semantics and finite policy-language boundary, complete predictor equations/initialization/smoothing, randomized unseen-environment requirement, dominator/shortest-path inference, SMT query polarity, fixed-link topology reduction, full algorithm/correctness argument, qualified forced-down environment-count concern, all table cells, parser/model edits to Internet2, and numeric discrepancies in summary claims.
  • limits: §§1/2: The mined specification describes behavior already enforced by the configuration, including mistakes or unintended restrictions. It does not discover operator intent or certify that existing behavior is desirable. An independent intended policy remains necessary to identify bugs; mined policies can support regression checking or refactoring only within the chosen semantics and failure scope. §2: Policy language includes reachability(r,p), isolation(r,p), waypoint(r,w,p), loadbalancing(r,p) on at least two paths. All policies means all instantiations of these supported templates, not arbitrary temporal/security/performance specifications. No convergence, transient update, quantitative bandwidth, timing or distributed liveness property is mined. §2: Failure model partitions links into forced-up, forced-down, symbolic; k bounds total down links including forced-down ones. Each concrete environment fixes all links and must satisfy that partition and count. Policy holds only if true in every admissible environment. Need consistent inputs k≥|Ldown|; empty-environment/vacuity handling not developed. Link-failure scope does not imply arbitrary router/software/Byzantine failures. §§3.2/Appendix A: Maintain verified⊆true specification⊆cands. Exact data-plane inference on a genuine admissible sample removes only false universal policies; sound complete control-plane query adds true policies or removes those violated by witness. Equality yields exact result; exhausting all genuine environments permits verified=cands. Proof assumes both tools model same configuration/policy semantics and their own results are correct. Appendix A: Termination relies on finite policy/environment spaces, PickCE always returning a previously unseen admissible environment, and every nonempty verifier query either proving policies or returning a real witness violating at least one. All component calls must terminate. No handling of solver unknown, timeout, parser errors or conflicting tool models is included in this theorem. Random sampling alone does not prove finite bounded runtime. Appendix A Algorithm1 line5 candidate listing error: totalEnvs=Σj=0..k binom(|Lsymbolic|,j), but §2 defines k as total failures including forced-down links. Correct admissible count uses k−|Ldown|. Example one forced-down link, one symbolic link, k1: one admissible environment, listing counts2; exhaustion branch may never trigger and PickCE can be asked for nonexistent unseen environment. Source §7 correctly subtracts forced-down count for topology trimming. This is a printed algorithm concern, not an executed artifact failure; experiments use empty forced sets. Appendix A Algorithm1: No explicit TopoTrim call or moving-average history appears despite §§3/4 implementation description; line25 divides by a set rather than its cardinality in print. Initialization calls verifier ten times and can classify policies before first data-plane sample, even though performance discussion says k1 only DPA. Read listing as schematic; exact code correspondence not proved. §4: Time-per-policy estimator=last runtime/newly classified policies, with infinity on zero DPA progress; remaining-time estimator=per-call time×unseen environments or unclassified policies. DPA selected when either estimator prefers it. Initial DPA times0, ten verifier policy sets initialize verifier averages, last ten calls smooth times. Heuristic choice affects cost, not exactness if underlying invariants/progress hold; no optimal scheduling bound. §5.1: Policy graph edge weight counts unclassified policies using a previous forwarding graph. Weighted random failed-link choice prioritizes many dependencies but rerouting can preserve them. Deterministic heaviest-link selection observed to oscillate; random fallback returns an unseen environment. Need legal fixed-link/count enforcement and finite unseen selection; no guarantee weighted sampler always needs fewer samples. §5.2: Batfish computes forwarding states, one graph per equivalence class of destination prefixes sharing forwarding. Dominator tree includes routers with at least one destination path, yields reachability and mandatory waypoint policies; isolation is inferred when reachability absent. Precise path quantification and treatment of ECMP branches/loops/drops must match verifier. Paper does not prove Batfish/Minesweeper correspondence for all supported policies. §5.2: Load balancing inferred from multiple equal-cost shortest paths. This is path multiplicity, not balanced byte counts, per-flow hashing fairness, disjoint paths or guaranteed throughput. Text says shortest paths in the network after describing forwarding graphs; ACL/route-policy-aware interpretation must be supplied by implementation, not assumed from raw physical connectivity alone. §6: Query formula φnet∧φfailure∧¬(∧policypredicates). UNSAT certifies whole group; SAT witnesses at least one failed policy, not all. Remove only actually violated policies; remaining ones unclassified. Group maximal same-prefix policies, arbitrary prefix choice. Claimed always at least as good follows query-count classification argument, not a wall-clock guarantee because larger conjunction can cost more or time out. §7: TopoTrim removes forced-down links, reduces residual budget k, replaces each forced-up edge with k extra parallel copies, then computes(k+1)-edge-connected components. Lack of required reachability/connectivity prunes reachability/load balancing and waypoint endpoints. This is necessary topology feasibility, not sufficient routing correctness. Requires compatible undirected link-failure model, prefix attachment and nonvacuous waypoint semantics; isolation is not trimmed. §8: Implementation5KPython/Java uses Batfish and Minesweeper extended with waypoint/load-balancing. Feature limits/parser bugs/SMT encoding become trusted boundaries. No mechanically checked framework proof, verified parser or proof of executable implementation. Tool-specific precision is assumed by mathematical argument rather than independently established through differential correctness evaluation. §8: Evaluated NetComplete-synthesized OSPF/BGP configs on three topologies and2/4/8/16prefix path-ordering specs, five config sets/type/topology. Large-network waypoints supplied by operator, simulated with random20%routers. Output completeness therefore relative to selected waypoint domain, not all possible waypoint devices. Not a benchmark of recovering independently authored human requirements. §8/Table2/3: Reported values are averages across generated configurations; fractional policies are averaged counts, not actual fractional policies. Candidates count after first all-symbolic-up sample, not entire template space. Increasing k shrinks true-policy set for same config; the paper does not explain why first-sample candidate averages differ across k. §8.1/Table2 discrepancy: source repeatedly claims OSPF completion within2.7hours, but USCarrier k2 OSPF cell10528.4s≈2.925h. BGP49151s≈13.653h agrees13.7. Source trend k1→2→3 describes averaged rows; time can decrease at more permissive failure bound because trimming eliminates nearly all policies. No monotone-runtime guarantee. §8.2: Baseline comparison only OSPF grids20/25/30routers because baselines do not scale to large topologies; five config sets, k1–3. At k2/3 DPA speedup mean10.2/max41, CPV mean3.8/max8.3. At k1 plain DPA wins by mean24/max37seconds due verifier initialization. Large-topology runtime is not direct large-topology measured baseline speedup. §8.3/Table4: Sampler comparison ten OSPF/BGP config runs per topology,k3; weighted policy-aware generally prunes more, but random transitions earlier in6/30runs due stalled pruning, not necessarily better results. More expensive sampling22.1–358.2ms versus random.5–1.4ms; overall DPA1.4–57.8s. AddedSamples>500 is censored, not precise mean. Candidate percentages use first sample as denominator. §8.3: Query reductions measured against one-query-per-policy baseline at first transition, not runtime speedups. BICS k2 text51.1%trim/41.5%group yields7.4%remaining arithmetically, whereas text/plot give9.6%; 90.3%overall reduction versus9.6%remaining differs rounding/definitions. USCarrier text1.15%trimremaining differs from the plotted trimming result; the text and plot relationship is unexplained. The final0.04%groupremaining is retained as a source claim. §8.4: Internet2 real May2015 configs modified before analysis: remove parsing/logging/anonymization/BFD lines and unsupported community/empty-prefix-list route-map matches. Authors say internal-prefix-only/noexternalpeers makes latter irrelevant, but no independent semantic equivalence proof. >90Klines,10routers/18links is small topology with large config text, not158routerproductiondeployment. §8: VMs32GBRAM/12vcores@2.3GHz. No exact CPUmodel, sourceversions/commits, solverlimit/unknownpolicy, seeds, standarderrors/confidenceintervals or per-run maxruntime provided. Timings and simulation/SMT outcomes measure performance under component assumptions, not tool code correctness. §§1/9: Operator anecdotes motivate need but no controlled user study of usability/specification review, bug detection accuracy or deployment benefit. CEGIS analogy concerns enumerating all valid finite policies with examples/oracles, not a learned or LLM-generated intent specification. No Verus/Rust/TLA+ or LLM agent result.
  • how much was read: most of it read
  • source
  • record id: config2spec-mining-network-specifications-2020
• GSPACER (2020)
  • title: Global Guidance for Local Generalization in Model Checking
  • what: Adds explicit global guidance to local IC3-style lemma generation. Three general rules—implemented as GS PACER on top of Z3 SPACER—use the current lemma set to introduce blocking states/lemmas and mitigate locality failures. The paper specifies subsume, concretize, and conjecture mechanisms, instantiates them for Linear Integer Arithmetic with model-based projection and anti-unification, and compares interpolation-enabled and interpolation-free configurations. Global guidance preserves the IC3 architecture and can support non-linear CHCs/LRA in the implementation.
  • number: Intel E5-2690 v2 3GHz, 128GB RAM, 10-minute timeout
  • number: SPACER solved 60% of CHC-COMP 2018 and 85% of 2019; GS PACER solved 214 safe/67 unsafe (CHC-18, fw) and 202/84 (CHC-19, fw)
  • number: Best GS PACER configurations solve significantly more instances than every SPACER configuration; interpolation-off GS PACER is best on CHC-18 and only slightly worse on CHC-19
  • number: On PLDI18, GS PACER solved 284 safe/68 unsafe versus SPACER 216/68 and Linear Arbitrary 270/65
  • limits: Main implementation targets LIA; LRA and non-linear CHC support are described as extensions, with details deferred. Results depend on CHC-COMP and artifact benchmark distributions and a 10-minute timeout on one CPU/memory setup. Authors note SMT runtime nondeterminism and leave theories lacking interpolation (e.g., bit-vectors) as future work.
  • how much was read: most of it read
  • record id: gspacer-2020
• MORA (2020)
  • title: MORA - Automatic Generation of Moment-Based Invariants
  • what: Presents MORA, a Python tool that automatically derives expected values and higher-order moment invariants for Prob-solvable probabilistic loops. It rewrites random polynomial updates into monomial expectation equations, solves resulting constant-coefficient recurrences, and emits text or LaTeX invariants. The grammar permits uniform/Gaussian random variables and probabilistic branches subject to linear self-dependence and polynomial dependence on earlier-updated variables. The parser computes only monomials needed by requested goals; the core orders triangular recurrences and reuses partial solutions. A random-walk example derives first/second moments and cross terms. The reimplementation is about 350 Python lines using diofant and scipy, and improves runtimes over the earlier Julia/SymPy proof of concept.
  • number: around 350 lines of Python
  • number: moments 1–3
  • number: STUTTERING C 2144→73.9 seconds at moment 3
  • number: SQUARE 8.70→1.67 seconds at moment 3
  • limits: Only grammar-conforming Prob-solvable loops are accepted; invalid input stops. The method depends on C-finite constant-coefficient recurrences and therefore does not cover arbitrary guards, distributions, or non-polynomial updates. This is a tool demonstration referring theoretical foundations to prior work, with a small benchmark subset rather than a broad probabilistic-program evaluation.
  • how much was read: most of it read
  • source
  • record id: mora-2020
• I4 (2019)
  • title: I4: Incremental Inference of Inductive Invariants for Verification of Distributed Protocols
  • what: I4 generates inductive invariants for distributed protocols by translating finite instances, running Averroes, removing redundant output and checking the candidate against the possibly infinite protocol in Ivy.
  • number: seven cases: lock server, ring leader election, distributed lock, Chord ring maintenance, learning switch, database-chain consistency, two-phase commit
  • number: Seven-model suite: chord_ring_maintenance, database_chain_replication, distributed_lock, leader_election_in_ring, learning_switch, lock_server, two_phase_commit
  • limits: README workflow requires legacy Python/Ivy/Averroes dependencies and does not report reproduced timings here.
  • how much was read: most of it read
  • source; notes: I4
  • record id: i4-2019
• Peuter Sofronie-Stokkermans invariant synthesis (2019)
  • title: On Invariant Synthesis for Parametric Systems
  • what: Develops goal-oriented invariant synthesis for transition systems over local theory extensions. Starting from a universal safety formula, Algorithm 2 repeatedly checks inductiveness and strengthens the candidate by eliminating primed and non-parameter symbols with symbol elimination; the paper proves partial correctness and derives termination conditions. The extended paper supplies the improved two-stage symbol-elimination algorithm, assumptions (A1)–(A5), proofs of Lemmas 7–8 and Theorem 9 (partial correctness), flat/linear-variable bounds (Theorems 12–13), array-property-fragment preservation (Theorem 17), and finite-term termination (Theorem 19). Worked examples cover linear arithmetic, sorted arrays, water-tank control, and nontermination when too many state symbols are retained; eliminating additional symbols can recover a finite invariant language. It also documents an implementation using H-PILoT plus Redlog and explains why manual variable selection was needed.
  • number: Algorithm 2 iterative synthesis
  • number: assumptions A1–A5
  • number: Theorems 6, 9, 12, 13, 17, 19
  • number: H-PILoT and Redlog toolchain
  • limits: Soundness depends on local theory-extension chains, decidable ground satisfiability, quantifier elimination or equality-defined updates, flat/linear clauses, and locality of all generated candidates. The algorithm is only partially correct if it terminates and may not terminate even for linear integer programs; formulas can grow exponentially or worse under Fourier–Motzkin elimination. The method targets universal invariants and selected function signatures, and the array examples rely on APF/locality assumptions rather than arbitrary programs.
  • how much was read: most of it read
  • record id: peuter-sofronie-stokkermans-invariant-synthesis-2019
• CD-NPI invariant synthesis (2018)
  • title: Invariant Synthesis for Incomplete Verification Engines.
  • what: Defines counterexample-guided invariant synthesis when a sound but incomplete verifier reduces undecidable verification conditions to a decidable theory. Extracts Boolean non-provability constraints from models of failed approximations, reduces the learning problem to ICE learning, proves conditional convergence, and evaluates a Dryad/Boogie heap-verification prototype on 82 routines. Separates undecidable theory U, decidable approximation D, propositional feedback theory B and invariant hypothesis class H. A D-model for a failed obligation may be spurious in U, so it supplies non-provability information rather than a concrete program counterexample. Normality requires unprovability to persist under Boolean weakening of preconditions or strengthening of postconditions. Ghost variables record predicate valuations before/after snippets. Failed establishment, use or preservation of an invariant yields disjunctive weakening, conjunctive strengthening or paired inductivity constraints. These translate to equiconsistent positive/negative/implication ICE samples. Theorem 2 guarantees convergence only when a normal engine can prove some annotation in a finite-predicate hypothesis class; Houdini learns conjunctions in at most n+1 rounds. The implementation instantiates shape/key/size templates over program variables, unfolds recursive Dryad properties and makes frame/heaplet reasoning explicit before Boogie. Evaluation removes loop invariants, weakens recursive contracts, and deletes five straight-line postconditions before learning replacements.
  • number: 82/82 routines verified across ten suites
  • number: Figure 2 suite sizes/categories in §3 source order: 16/3, 9/3, 3/1, 8/1, 8/1, 11/2, 3/2, 11/3, 9/2, 4/1
  • number: five straight-line programs used for postcondition inference
  • number: great majority of suites: median runtime <10 s (not every program/suite)
  • limits: Requires a sound U→D approximation and D-model construction on failed validity, not merely timeout/failure output. Engine normality is a substantive assumption, and integration is not automatic. Finite predicates and positive Boolean combinations underlie the stated convergence theorem; negated predicates may be added explicitly. Convergence is relative to the verifier’s provable annotation class, not completeness for all valid invariants/programs. Actual prototype learns conjunctions from generic finite templates whose category is chosen according to specification needs; annotated C/Dryad input and target specifications remain supplied. Dryad restricts negation in recursive definitions and spatial conjunction contexts. No comparative full-suite tool evaluation; authors explain they lack a comparable tool for the entire set. Main paper defers Theorems 1–2 proofs, full templates, detailed per-benchmark results and the separate universally quantified-program application to extended arXiv:1712.05581; that extension was not read in this batch. No distributed protocol, liveness, TLA+, Verus/Rust, or LLM experiment.
  • how much was read: most of it read
  • source
  • record id: cd-npi-invariant-synthesis-2018
• Code2Inv (2018)
  • title: Learning Loop Invariants for Program Verification (Code2Inv)
  • what: Learns loop invariants (facts that hold on every pass through a loop) for C programs with one loop. Uses graph neural networks and reinforcement learning. Z3 checks each candidate, and its counterexamples are fed back as rewards. Training needs no known-correct invariants.
  • number: 133 arithmetic C programs; 12 h / 4 GB limit: Code2Inv 106, ICE-DT 100, LoopInvGen 77, C2I 74 (abstract says 73)
  • number: 92 solved under one-hour limit
  • number: Figure 1 loop: 26 Z3 calls vs 1,119 for LoopInvGen, which then crashes
  • number: ablation without counterexamples and attention: 91 solved, 415,000 queries
  • limits: A human supplies the pre- and postcondition. Proves partial correctness only (the result is right if the loop terminates). Nine tasks were later found invalid. Invariants must be in CNF form. The gain is fewer Z3 queries, not less wall-clock time.
  • how much was read: most of it read
  • source; notes: Learning Loop Invariants for Program Verification (Code2Inv), Si et al
  • record id: code2inv-2018
• Code2Inv (2018)
  • title: Learning Loop Invariants for Program Verification
  • what: Code2Inv learns loop invariants (facts true on every pass through a loop) with graph neural networks and reinforcement learning. Z3 checks that each candidate holds at the start, stays true after each pass, and implies the postcondition. Counterexamples are fed back as rewards.
  • number: 133 single-loop arithmetic C programs; 12 h limit: Code2Inv 106 solved, ICE-DT 100, LoopInvGen 77, C2I 74 (abstract says 73); 92 under one hour
  • number: Max 276 Z3 queries; without counterexamples and attention 91 solved, 415,000 queries
  • number: 133 benchmarks
  • number: 106 solved vs 100/77/74 baselines
  • limits: Humans supply the precondition and postcondition. It shows partial correctness only: it does not show that the program terminates. The benchmark is invalid for 9 tasks. Invariants are constrained to conjunctive normal form. It has no wall-clock advantage over competing solvers.
  • how much was read: most of it read
  • source; notes: Learning Loop Invariants for Program Verification (Code2Inv), Si et al
  • record id: code2inv-2018-2
• Dinv (2018)
  • title: Inferring and Asserting Distributed System Invariants
  • what: It mines likely invariants over distributed snapshots of Go programs, using static slicing, vector clocks and Daikon. It turns chosen invariants into runtime assertions.
  • number: four Go systems, 1.7K-144K lines
  • number: Serf: about 1 million invariants reduced to 40 by manual refinement
  • number: Raft assertions 11, 13, 72 lines; detection 0.07, 0.36, 2.22 s
  • number: always-on check 52x slowdown, 1% sampling 1.02x
  • limits: The invariants are likely, not verified. It is designed for runs where no node fails. Humans choose which properties matter and write the assertion functions.
  • how much was read: most of it read
  • source; notes: Related-work omission: Inferring and Asserting Distributed System Inva; notes: Related-work omission: Inferring and Asserting Distributed System Inva
  • record id: dinv-2018
• FreqHorn-2 syntax-guided invariants (2018)
  • title: Accelerating Syntax-Guided Invariant Synthesis
  • what: Presents FreqHorn-2, a syntax-guided inductive-invariant synthesizer that deterministically bootstraps from program subexpressions and Craig interpolants, then samples grammar mutants while using Houdini inductive-subset extraction and counterexample-to-induction (CTI) second chances. The paper specifies the two-stage Algorithm 4 in detail: seeds from Init/Tr/Bad are augmented with bounded-safety interpolants; initiation filtering and Houdini extract an inductive subset; failed candidates are grouped by CTIs and retried after learned lemmas invalidate their blockers. It proves termination outcomes (bug or synthesized invariant), explains grammar normalization and pruning, and reports that merged seeds/interpolants solve 114 of 171 safe programs before randomized mutants; mutants are needed in 57 cases. On 128 instances FreqHorn-2 beats old FreqHorn in 90, reaches 233x speedup, and averages 4x faster, while showing anomalies from blind grammars, large disjunctions and interpolation.
  • number: 171 safe programs
  • number: 103 solved from seeds with inductive subset vs 63 one-by-one
  • number: 70 solved from interpolants
  • number: 114 solved from merged seeds and proofs
  • limits: The target is a transition system encoded as linear or nonlinear constrained Horn clauses, with a conjunction of lemmas as a safe inductive invariant checked by SMT. Bounded interpolation is limited to LIA, so 17 NIA benchmarks skip it; sampling remains nondeterministic and grammar construction may miss useful constants or large disjunctions. If BMC finds a counterexample below the configured bound N, no invariant exists and the algorithm reports a bug. Experiments are on 171 safe programs and unsafe instances only for testing, with 60-second timeout comparisons and three timing runs; no completeness guarantee for mutant search is given.
  • how much was read: most of it read
  • record id: freqhorn-2-syntax-guided-invariants-2018
• ICE refinement types (2018)
  • title: ICE-Based Refinement Type Discovery for Higher-Order Functional Programs
  • what: Extends the ICE invariant-learning framework to infer refinement types for recursive higher-order OCaml programs. It generalizes implication constraints from (x,y) to ({x1,…,xk},y) for nonlinear Horn clauses, learns multiple mutually dependent predicates, verifies candidates with SMT, and iterates counterexamples. Formalizes a simply typed call-by-value higher-order language with recursion and a refinement type system whose typability implies main never fails. Verification conditions become Horn clauses; the teacher extracts positive, negative and generalized implication samples from falsified clauses, while a decision-tree learner synthesizes predicates. Effect analysis and Horn-clause reduction shrink predicate sets. RType (OCaml frontend) plus HoIce (Rust solver using Z3) was evaluated on 162 safe programs; 63/164 OCaml programs generated nonlinear Horn clauses, and failures exposed missing qualifiers or type-system incompleteness.
  • number: 162 benchmark programs
  • number: 63 of 164 OCaml programs yielded nonlinear Horn clauses
  • number: 100 s timeout
  • number: HoIce solved 162 benchmarks
  • limits: Target language has integers (booleans encoded as 0/nonzero), no algebraic data types, and requires simple typing; type soundness is stated but the refinement system is incomplete. Benchmarks include only safe programs because RType is not refutation-sound. Qualifier mining misses forms such as x+y≥z unless explicit; nine cases are refinement-untypable. 100-second timeout and solver-dependent learning limit scalability; unsatisfiable Horn clauses are a poor fit.
  • how much was read: most of it read
  • record id: ice-refinement-types-2018
• Ivy liveness-to-safety (2018)
  • title: Reducing liveness to safety in first-order logic
  • what: After a finite prefix of an execution, picks a finite projection of the state (the freeze point). Proves that no two later states can agree on that projection while all fairness obligations are met. This turns a progress proof into a safety proof about a finite bad pattern. Cases: ticket, alternating bit, TLB shootdown, Paxos, Multi-Paxos, Stoppable Paxos.
  • number: finding the invariants ‘requires a sophisticated user’; conjecture counts for liveness are ‘2 - 4 times higher’ than for safety (§7.2, pp.26:27-28)
  • number: six cases: ticket protocol, alternating bit, TLB shootdown, Paxos, Multi-Paxos, Stoppable Paxos
  • number: checking takes 3.7 to 219 seconds excluding invariant discovery
  • number: liveness needs two to four times as many invariant conjectures as safety (§7.2)
  • limits: The user still supplies the inductive invariants (facts preserved by every step). Humans applied the reduction by hand. Paxos assumes that the actions of a chosen leader or quorum are fair, that messages are eventually delivered, and that competing proposals eventually stop. Multi-Paxos and Stoppable Paxos cover one incarnation with fixed membership. The comparison counts invariants, not person-time.
  • how much was read: most of it read
  • source; notes: Ivy: dynamic abstraction and temporal prophecy
  • record id: ivy-liveness-to-safety-2018
• Paxos Made EPR (2017)
  • title: Paxos Made EPR: Decidable Reasoning about Distributed Protocols
  • what: The paper transforms Paxos-family models so that checking a human-supplied proof falls in EPR. EPR is a first-order fragment where satisfiability is decidable (an algorithm always answers). It checks proofs. It does not discover invariants.
  • number: Six variants: Paxos, Multi-Paxos, Vertical Paxos, Fast Paxos, Flexible Paxos, Stoppable Paxos
  • number: Verified six protocol variants with EPR transformations
  • number: Z3 experiments repeated 10 times, 300s timeout, Linux Core-i7 1.8GHz
  • number: EPR verification conditions solved in a few seconds with no timeouts; semi-bounded runtimes grew with rounds; unbounded Z3 diverged
  • limits: Z3 did not terminate on unbounded checks of the original models. The URL of the original artifact returns 404, and the review notes found no verified copy.
  • how much was read: most of it read
  • source; notes: Paxos Made EPR
  • record id: paxos-made-epr-2017
• alpha-L2S (2016)
  • title: Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations
  • what: alpha-L2S checks that an infinite-state system eventually does something good (liveness). It reduces that question to a safety question, where nothing bad ever happens. It learns the needed predicates and ranking functions (measures that shrink toward the goal) by refining an abstraction. It is the direct predecessor of rlive and its baseline.
  • number: Fig 4: L2Sia-wfr solved 602 (477 valid, 125 violated) vs Ultimate-LTL 263 (185, 78)
  • number: timeout 1200 s, memory 6 GB
  • number: on 193 termination benchmarks T2 solves 191 vs 152 for this method
  • number: 835 total LTL instances
  • limits: It checks liveness on a model. Its benchmarks come from programs, so they test translated program semantics, not the programs themselves.
  • how much was read: most of it read
  • source; notes: Related work absent from the first pass: αL2S
  • record id: alpha-l2s-2016
• Automatic Abstraction in SMT-Based (2016)
  • title: Automatic Abstraction in SMT-Based Unbounded Software Model Checking
  • what: Spacer combines under-approximation 2BMC, proof-based abstraction and CEGAR in Horn-SMT/Z3. Alternates abstraction, feasibility and refinement; UNSAT proofs generalize safety while concrete counterexamples preserve bug guarantees.
  • number: 1990 initial; 608 evaluated; 369 unsafe solved by both; 42/55 hard safe solved within 15m
  • limits: No bit-vector/heap support; abstraction may hurt easy cases; results solver/time bounded.
  • how much was read: most of it read
  • record id: automatic-abstraction-in-smt-based-2016
• Automaton learning for infinite safety games (2016)
  • title: An Automaton Learning Approach to Solving Safety Games over Infinite Graphs.
  • what: Learns finite-state winning controllers for safety games over infinite or very large graphs. Rational arenas encode vertex sets as regular languages and edges as rational relations; an ICE-like teacher returns positive, negative, existential-implication or universal-implication counterexamples, and a SAT-based learner constructs minimal consistent DFAs. The paper proves closure properties of rational relations, defines winning sets and a generic automata-theoretic teacher, and gives SAT encodings whose satisfiability is equivalent to existence of an n-state DFA consistent with the sample. The minimal-consistent-DFA algorithm increments n and terminates at the minimum; the full learner terminates with a winning set when one exists. An RPNI heuristic is sound but incomplete and restricted to finite out-degree. Examples include unary encodings of grid positions, implication counterexamples, diagonal/box/evasion/follow games and program repair.
  • number: SAT learner solved all infinite-arena games; RPNI all but Follow
  • number: 9×9 planning: 7.8 s SAT, 2.1 s RPNI, 5.4 s TuLiP
  • number: RPNI m=50,000; SAT m=30,000; TuLiP m=10,000
  • number: 300 s timeout and 16 GiB memory
  • limits: Winner determination for rational safety games is undecidable, so the method is a semi-algorithm and assumes a winning set exists for the termination theorem. The SAT learner’s passive DFA identification is NP-complete in general; RPNI cannot guarantee minimality or completeness and handles only finite implication languages. Experiments use regular-language/transducer encodings and finite-state safety objectives; results do not establish liveness synthesis or arbitrary infinite-state game classes.
  • how much was read: most of it read
  • source
  • record id: automaton-learning-for-infinite-safety-games-2016
• generalized homogeneous invariant synthesis (2016)
  • title: Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis
  • what: Restricts polynomial invariant templates to generalized homogeneous (GH) polynomials whose monomials share inferred generalized degrees. It proves GH abstract semantics sound and complete at the semantic level, and the resulting invariant-inference algorithm sound, reducing template size. Defines g-degree assignments as Abelian-group dimensions, infers them by unification constraints, and proves every invariant has a homogeneous component that is also an invariant under the GH semantics. The algorithm InvInfH uses a GH template and has soundness inclusion in the unrestricted InvInf results; completeness of the algorithm itself remains open. A 20-program benchmark compares template monomials and solver times.
  • number: 13 of 20 programs had smaller templates
  • number: petter10 monomials 364 to 14
  • number: sumpower5 solver total 89.6 ms vs Fastind 670 ms
  • limits: Programs use polynomial assignments and single-polynomial guards; consistency requires all expressions GH under Γ. Remainder operation must preserve GH form. Constants normally infer degree 1, requiring an implementation workaround treating occurrences as variables. Choice of target g-degree τ is left to the user; semialgebraic extension is conjectural.
  • how much was read: most of it read
  • record id: generalized-homogeneous-invariant-synthesis-2016
• Ivy repository (2016)
  • title: Ivy: Safety Verification by Interactive Generalization
  • what: Ivy is a research tool for interactive development of protocols and correctness proofs, with interactive visualization of automated proofs and a human/tool workflow for exposing errors.
  • number: Bounded verification about 10 transitions in a few minutes
  • number: Pages 614-630
  • limits: README is brief and points to the website for details.
  • how much was read: most of it read
  • source; notes: tools
  • record id: ivy-repository-2016
• Model Checking C Programs with Loop (2016)
  • title: Model Checking C Programs with Loops via k-Induction and Invariants
  • what: Combines k-induction base/forward/inductive checks with affine polyhedral invariant inference for C loops. Iteratively increases k and injects inferred pre/post constraints; compares invariant and no-invariant implementations on loop benchmarks.
  • number: Polyhedral variant solves more tasks (abstract); exact table unavailable
  • limits: Affine domains omit nonlinear, heap and bit-vector invariants; bounded/solver limits can return unknown.
  • how much was read: most of it read
  • record id: model-checking-c-programs-with-loop-2016
• RAHFT Horn-clause verification tool (2016)
  • title: RAHFT: A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata
  • what: Introduces RAHFT, a modular CHC safety verifier combining constraint specialization, convex-polyhedra abstract interpretation, finite-tree-automata trace abstraction refinement and SMT feasibility checks. It returns safe, unsafe or an abstract counterexample and can be reconfigured to use each component separately. The abstraction module specializes clauses without unfolding, computes a convex-polyhedra fixed point containing at most one constrained fact per predicate, and records derivation traces as an FTA. A verifier accepts an inductive model or selects an abstract false trace; infeasible traces are generalized by interpolant automata. The refinement module computes FTA difference via optimized determinization, then generates equisatisfiable refined clauses that split predicates, so previous refinements need not be retained. Ciao Prolog integrates Yices, Parma Polyhedra and FTA libraries.
  • number: over 7,000 lines of Ciao Prolog in 42 modules
  • number: Rahft solves the motivating invariant example in preprocessing alone
  • number: reported comparisons favor Rahft in runtime and instances solved (details in cited papers)
  • number: uses Yices SMT, Parma Polyhedra Library and optimized FTA determinization
  • limits: The current implementation targets CLP constrained Horn clauses over linear arithmetic; arrays, maps, sets and richer theories are unsupported. Convex polyhedra can bottleneck large programs; library arity limits and interpolant generation do not scale well. Counterexample/model reconstruction in the original program is difficult after transformations and external-library use. The paper reports comparative evaluation by reference to prior studies rather than a full new benchmark table.
  • how much was read: most of it read
  • record id: rahft-horn-clause-verification-tool-2016
• DepthK (2015)
  • title: Model Checking Embedded C Software using k-Induction and Invariants (extended version)
  • what: Introduces DepthK, an automatic k-induction verifier for embedded C that combines base, forward, and inductive cases with polyhedral invariants generated by PIPS and translated into ESBMC assumptions. It transforms loops to loop-free programs, havocs loop variables, and rechecks invariant-strengthened results with BMC.
  • number: Intel Xeon E5-2670, 115 GB RAM; 15-minute CPU and 15 GB memory limits. DepthK versus ESBMC k-induction, CPAchecker variants and CBMC. On SV-COMP loops DepthK scored 140 versus ESBMC 105, CPAchecker no-inv 101, CBMC 53; 94 correct, 1 false-incorrect, 0 true-incorrect, 47 unknown/timeout. On embedded tests DepthK had 17 correct and 17 unknown/timeout; inductive-step proofs exceeded ESBMC by 25.35% (loops) and 29.41% (embedded).
  • limits: Affine/polyhedral invariants may be weak or non-convex; invariant over-approximation requires BMC rechecking. Global unwinding bound and max iterations (100) are configured; tool can return UNKNOWN on timeout, resource exhaustion, invariant-generation or implementation failures. Evaluation is limited to ANSI-C benchmarks and safe embedded programs.
  • how much was read: most of it read
  • source
  • record id: depthk-2015
• Learning Commutativity Specifications (2015)
  • what: # Whole reading: Learning Commutativity Specifications (authored by agents unless marked 🧑) This paper learns compact commutativity conditions from black-box executions. Its logical theorems characterize approximation within a declared fragment; finite-sample success and formula stabilization do not establish soundness over all executions. Read the full saved 17-page PDF, §§1–9, references 1–23, all five figures and six numbered equations. No external supplement, author implementation or experimental artifact was inspected. ## D1: contribution Gehr, Dimitrov and Vechev infer logical specifications from black-box observations. The pipeline combines type-aware sampling, sample reduction, predicate discovery and exhaustive/greedy formula search. Commutativity of library data structures is the demonstrated application. Source: Q0, Q1, S1 in quotes.json; section/page/character/LF pointers are embedded in each anchor. Exact source passage (S1, title, abstract, §1 Introduction; physical PDF page 1, printed page 307): > In this work we present a new sampling-based “black box” > inference approach for learning the behaviors of a library component. ## D2: logical assumptions A fixed finite tuple of variables ranges over a relational structure with finitely many relation symbols, no function symbols or constants, and a Boolean-closed quantifier-free fragment; formulas are in negation normal form. Relations may themselves be defined with quantifiers. These restrictions yield finitely many isolated logical types. A logical type groups tuples satisfying exactly the same formulas; it is not a programming-language or type-theory type. Source: Q0, Q4, Q5, S2, S3 in quotes.json; section/page/character/LF pointers are embedded in each anchor. Exact source passage (S3, §3 Observation 2, Equation 2; §4.1 Theorem 1; physical PDF page 6, printed page 312): > We shall focus on the setting where: (i) the structure X is relational, i.e., it > mentions no function symbols (including constants); (ii) the relation symbols > are finitely many; and (iii) L(x) is the quantifier-free fragment of X. Combined, > these conditions guarantee that there are finitely many L(x)-definable relations > in the structure X, and therefore we can leverage Observation 2. We will further > assume that formulas are in negation normal form, i.e., that all negations are > pushed in front of atomic subformulas. ## D3: proved structural result Observations 1–2 state that definable relations are disjoint unions of type preimages and that a finite definable family yields finitely many isolated types. Theorem 1 characterizes the best definable under-approximation as the union of whole type preimages contained in the target relation. This characterizes the objective relative to a chosen fragment, not what finite sampling establishes about all behavior. Source: Q4, Q5, S4 in quotes.json; section/page/character/LF pointers are embedded in each anchor. Exact source passage (S4, §3 Observation 2, Equation 2; §4.1 Theorem 1; physical PDF page 6, printed page 312): > Theorem 1. The best under-approximation h ∈ H to any relation c over X > equals the disjoint union >  > {t ⊆ c | t is a preimage of some type}. ## D4: finite-sample objective Equation 3 maximizes accepted positives subject to accepting no sampled negative. Theorem 2 accepts types observed only positively and excludes negative or ambiguous types. A type is ambiguous when both labels occur; useful positive observations may therefore be rejected. Missing types remain unconstrained by this objective. Reader inference: a sample-optimal hypothesis need not be a sound under-approximation of the true relation. Source: Q6, S5, S6, S9 in quotes.json; section/page/character/LF pointers are embedded in each anchor. Exact source passage (S6, §4.1 Definition 5/Theorem 2/Equation 3; §4.2 Equation 4; physical PDF page 7, printed page 313): > Theorem 2. A hypothesis h ∈ H is optimal with respect to (3) for a given > sample (s+, s−) if and only if for every tuple u from X with non-missing type > u ∈ h ⇐⇒ tpL(x)(u) is positive > u ∈ h ⇐⇒ tpL(x)(u) is negative or ambiguous ## D5: search and minimality Dynamic programming enumerates formulas by Equation 4 size and identifies formulas equivalent on the sample. Exhaustive enumeration alone guarantees minimum size. Interleaved greedy weighted set cover seeks a disjunction of conjunctions false on all negatives; at size i these conjunctions have size less than i, and the algorithm returns a cover with fewer than 2i (two times i) conjunctions. The greedy path explicitly does not guarantee minimality, so do not attribute a universal smallest-syntax guarantee to the combined practical algorithm. Source: Q6, Q7, S7 in quotes.json; section/page/character/LF pointers are embedded in each anchor. Exact source passage (S7, §4.2 greedy search; §4.3 predicate discovery; physical PDF page 8, printed page 314): > it with a greedy algorithm, which does not guarantee minimality, but is much > faster in practice. ## D6: predicate discovery and limits The Boolean case removes opposite literals using sample monotonicity/antitonicity. Generalization uses literal-indexed neighbor relations on logical types; admissibility is defined for samples with no missing types. For integer order, types are ordered partitions, and neighbor operations swap or merge adjacent classes. The authors explicitly warn that missing types may prune literals needed by an optimal hypothesis. Source: Q7, Q8, S8 in quotes.json; section/page/character/LF pointers are embedded in each anchor. Exact source passage (S8, §4.3 Definitions 7–8/linear-order neighbors; §5 introduction; physical PDF page 9, printed page 315): > Because of missing types, the above method > may prune literals which are required for finding the optimal hypothesis. Thus, > our pruning approach is a heuristic that relies on good samples. ## D7: sampling and oracle assumptions Sampling trades type diversity (m examples overall) against evidence per type (k); it stops drawing from an ambiguous type. Reduction preserves one representative per positive/negative type and two opposite representatives per ambiguous type. When outputs cannot be chosen, sampling controls only the input type and classifies the completed argument/return tuple after execution. The commutativity oracle needs reproducible same-state runs and supplied abstract-state equality. Source: Q9, Q10, Q11, S12 in quotes.json; section/page/character/LF pointers are embedded in each anchor. ## D8: conditional soundness Section 5.1 guarantees a best sound approximation if every type has its observed status equal to its true status. Such a sample exists because type count is finite, but obtaining it can be infeasible; the authors suggest white-box verification. The paper does not give a probability or sample-complexity bound certifying that a particular finite sample satisfies this condition. Source: Q9, S9 in quotes.json; section/page/character/LF pointers are embedded in each anchor. Exact source passage (S9, §5.1 type-aware sampling, reduction and guarantees; physical PDF page 10, printed page 316): > Guarantees. If we obtain a sample of maximal informativeness, i.e., in which > every type has its observed status equal to its true status, then we are guaranteed > to infer (the best) sound approximation. Such a sample always exists (as there are > finitely many logical types) but obtaining it is often infeasible in practice. Thus, > we can combine our black-box approach with white-box verification, e.g., [12]. ## D9: stopping and termination Section 5.3 doubles new sample blocks, reruns search on cumulative examples from scratch, caps each search by that step’s sampling time, and returns the same formula after two consecutive outcomes. Theorem 3 states required search time is o(the increasing sampling-time limit) after sample reduction because reduced sample size is bounded by type count. This is a search/termination argument; stabilization supplies no proof of semantic soundness or PAC-style error/confidence bound. Source: Q10, S10, S11, S9 in quotes.json; section/page/character/LF pointers are embedded in each anchor. Exact source passage (S10, §5 Figure 3, §5.2 interface, §5.3 stabilization/Theorem 3; physical PDF page 11, printed page 317): > If the search gives the same result two consecutive times, then we > return the discovered formula. ## D10: commutativity meaning The two calls execute in both orders from the same initial state. A positive example requires matching final abstract states and corresponding return values; failure yields two negative examples. Equal(sigma1,sigma2) is supplied at the abstract level. The learned integer/Boolean equality/order fragment has arbitrary Boolean structure. The instantiated formulas omit the state and therefore approximate state-dependent specifications. Source: Q2, Q11, S12 in quotes.json; section/page/character/LF pointers are embedded in each anchor. Exact source passage (S12, §6 commutativity/Equation 5; §7 evaluation introduction; physical PDF page 12, printed page 318): > To compare states we assume that an abstract equality check, > Equal(σ1, σ2), is provided (naturally, we reason at the abstract level as opposed > to the bit for bit concrete level). ## D11: evaluation design and aggregation The paper evaluates method pairs of 21 data types, including six union-find variants, classic containers and bit structures. Initial sample size 5000 was tuned using Set/Map and reused. Figure 4 reports eight-run averages of each structure’s maximum across method pairs, separately for each column. Times are milliseconds unless seconds are explicitly marked; the full 21-row transcription is in evaluation.json. Source: Q11, Q12, S13 in quotes.json; section/page/character/LF pointers are embedded in each anchor. Exact source passage (S13, §7 UnionFind 6/Equation 6, Figure 4 and aggregation; physical PDF page 13, printed page 319): > For every data > structure we show the averaged maximum over all method pairs. ## D12: measured results and claim boundary Figure 4 reports formula sizes 1–19 and largest disjunct sizes 1–9, predicate-discovery search speedups 1.6–43.2 times, sampling values 35 ms–2.4 s, and search values 0.06–710 ms. These ranges are reader calculations over the reported averages of maxima, not confidence ranges. The authors report best approximations in every case, but the paper supplies no independent exhaustive/proof certification for every result. No experiments were reproduced for this record. Source: Q12 in quotes.json; section/page/character/LF pointers are embedded in each anchor. ## D13: sampling comparison Figure 5 compares type-aware and random sampling for Map put/put, get/put and get/get, with tuple lengths six, five and four. Typical illustrated runs stabilize at 15000 versus 75000 samples. Authors qualify faster exploration of new types as applying to larger tuples, about six components here, and note high random-sampling stabilization variance. The sample-count comparison does not establish a universal fivefold runtime improvement. Source: Q13, S14 in quotes.json; section/page/character/LF pointers are embedded in each anchor. Exact source passage (S14, §7 Figure 5/sampling comparison; §8 related work; physical PDF page 14, printed page 320): > We observe > that: (i) type-aware sampling explored new types more quickly than pure ran- > dom sampling, but only when sampling larger tuples (about 6 components in > this particular case); and (ii) type-aware sampling stabilized the inferred for- > mula much earlier (15 000 vs. 75 000 examples). In fact, in our experiments, we > observed large variance in stabilization time when sampling purely at random. ## D14: baselines and tradeoffs The paper reports that Daikon/DIG learned crude approximations because commutativity needs rich disjunctions, while explicitly saying the proposed approach is not strictly better: Daikon scales with more relations and DIG targets polynomial invariants. Perfect-separation learners fail on ambiguous types even when a useful approximation exists. The randomized method in reference 20 was not observed terminating with five or more variables. These comparisons lack a quantitative common-baseline protocol in the paper. Source: Q13, Q14, S15, S16 in quotes.json; section/page/character/LF pointers are embedded in each anchor. Exact source passage (S15, §8 comparisons and limitations; §9 Conclusion; physical PDF page 15, printed page 321): > That said, our approach is not strictly better. Daikon scales well when the num- > ber of relations in the fragment increases, and DIG specializes in polynomial > invariants. ## D15: reproduction limits The paper does not report hardware, all implementation settings, per-type k, seeds, detailed sampling distributions, uncertainty intervals, or complete baseline versions/timeouts. Eight-run averages alone do not quantify run variance; the text qualitatively notes large random-sampling variance. Reading the supplied PDF cannot establish unreported details. Source: Q9, Q10, Q12, Q13, Q14 in quotes.json; section/page/character/LF pointers are embedded in each anchor. ## D16: printed and extraction discrepancies Rendered §5.1 prints c- using nonmembership in s- while discussing the true target relation. Rendered Equation 5 repeats m2 in the reverse sequence; nearby invocation subscripts are inconsistent. Prose in §§2/6.2 resolves intended opposite-order semantics, but no implementation defect is inferred. Raw extraction also corrupts inequality, nonmembership, union, norms and superscripts; exact quotations retain raw characters, and separate rendered transcriptions explain the mathematics. Source: Q2, Q9, Q11 in quotes.json; section/page/character/LF pointers are embedded in each anchor. ## D17: distributed verification relevance: reader inference Direct relevance is discovery of conditions under which reordering preserves abstract state and returns. For distributed verification, one could use this as a source of candidate commutativity predicates or independence conditions, then separately check the required executions and state model. The paper itself does not prove a distributed protocol, linearizability or correctness under concurrency; its commutativity observations are pairs of sequential executions. Source: Q0, Q2, Q11 in quotes.json; section/page/character/LF pointers are embedded in each anchor. ## D18: Verus/Rust and TLA+ relevance: reader inference The learned predicates could motivate candidate Verus/Rust contracts or TLA+ action-independence conditions. Translation must state the logical fragment, abstract equality, state quantification and return-value meaning; a checker/proof must establish the candidate over the intended model. The paper contains no Verus, Rust or TLA+ implementation or evaluation, and supplies no such translation. Source: Q5, Q9, Q11, Q14 in quotes.json; section/page/character/LF pointers are embedded in each anchor. ## D19: specification/proof agents and evaluation: reader inference An agent could propose predicates, diversify examples by logical type, retain ambiguous examples and produce a compact formula. This paper supports separating candidate generation, sample consistency and whole-model proof. Evaluation should report the chosen fragment, oracle/equality assumptions, ambiguity and missing-type coverage, aggregation, actual proof/checker outcomes, and failures. Stable formulas alone do not certify soundness. No LLM or proof-writing agent is evaluated here. Source: Q6, Q8, Q9, Q10, Q11, Q12 in quotes.json; section/page/character/LF pointers are embedded in each anchor. ## Concrete cases and measurements Map put returns the old value. Equation 1 says distinct keys commute, or both puts leave their values unchanged: (k1 != k2) OR ((v1=r1) AND (v2=r2)). Figure 2 has six rows: four positive and two negative. Its first two rows have the same logical type despite different concrete values. This illustrates why logical-type diversity and removal of repeated types help. Source: Q2. unite(a,b) merges the classes under the representative of a and returns whether it changed the structure. Equation 6 is [((a1=a2) OR (a1=b2) OR (a2=b1)) AND r1 AND r2] OR (a1=b1) OR (a2=b2) OR ((NOT r1) AND (NOT r2)). This is a rendered transcription, not a literal raw quotation; it includes both changes, self-unions, and two no-change calls. Source: Q12. Figure 5 uses argument/return tuples of six, five and four components for put/put, get/put and get/get. The text reports stabilization at 15000 versus 75000 examples in typical illustrated runs and qualifies faster new-type exploration as applying to larger tuples here. Random sampling has high stabilization variance. Source: Q13, S14. Theorem 2 permits a useful best under-approximation even when a positive and a negative tuple have the same logical type. Such a type must be excluded wholesale; a classifier required to accept every positive would fail. A missing negative can leave a truly ambiguous type looking positive in a finite sample. Source: Q6, Q9, Q14. All 21 reported result rows, original time suffixes, aggregation and baseline limits are preserved in evaluation.json. Equations and printed discrepancies are separated from literal extraction in rendered_math_transcriptions.json. This record performs source reading and quotation validation, not empirical reproduction or formal checking.
  • limits: Finite relational/quantifier-free fragment and logical types; supplied black-box oracle and abstract state equality; sample-optimality versus conditional true-relation soundness; missing/ambiguous types; heuristic pruning/stabilization; incomplete experiment details; D2–D16.
  • how much was read: most of it read
  • source
  • record id: learning-commutativity-specifications-2015
• PDR∀ universal invariants (2015)
  • title: Property-Directed Inference of Universal Invariants or Proving Their Absence
  • what: Extends IC3/PDR to universal first-order invariants using finite-model diagrams. On termination returns an inductive universal safety invariant, a concrete counterexample, or a proof that no such invariant exists over the chosen vocabulary. Implements the algorithm for linked structures and evaluates verification, deliberate bugs and invariant-expressibility failures. Finite-state models are generalized to existential diagrams specifying every relation/constant and distinct element, so their negations provide universal strengthening clauses. Lemma 1 shows that a diagram implies every closed existential formula true of its model. This makes diagram blocking precise relative to universal inductive invariants. Frames overapproximate bounded reachable states; recursive predecessor blocking, clause propagation and unsatisfiable-core generalization seek a fixed point. If blocking reaches initial states, bounded model checking distinguishes a genuine trace from a spurious diagram trace; Proposition 1 proves the latter excludes every universal safety invariant in the vocabulary. The shared-tail/traverseTwo example demonstrates the universal-submodel preservation obstruction: removing the shared tail from a reachable model creates a bad submodel. Implementation uses EAR reachability logic reduced to EPR, Z3 finite models and auxiliary allocation/input-membership/order predicates for rich specifications. Table 1 compares memory safety to prior human-template PDR shape analysis and also reports stronger functional verification.
  • number: 22 verified correct-program rows (11 singly-linked, 4 sorted singly-linked, 3 doubly-linked, 4 composite structures)
  • number: full verification: split 206 s, 8 frames, 1,143 Z3 calls, 36 clauses (19 universal)
  • number: full verification: sorted-merge 655 s; insertion-sort 1,934 s, 14 frames, 4,783 calls, 41 clauses (18 universal)
  • number: no universal invariant: shared-tail 3.6 s, 2 frames, 42 Z3 calls; comb 2 s, 3 frames, 52 calls
  • limits: No termination guarantee. Init, transition and Bad must be representable in the chosen first-order logic; satisfiable queries need finite models. The presentation assumes SAT/model procedures; implementation uses decidable EAR (relational ∃∀ with restricted deterministic transitive closure, no function symbols), reduced to EPR. More complex control flow is encoded via a program counter. Absence result is limited to universal inductive invariants over the fixed vocabulary, not program incorrectness or impossibility of richer proofs. Auxiliary predicates are used despite no user-supplied abstraction templates. EAR has limited ability to express list segments not pointed to by variables. Benchmarks are small list/data-structure algorithms; four bugs are deliberate. No liveness, distributed-protocol, Verus/Rust, TLA+, or LLM evaluation. Timing comparisons to [32] concern memory safety; that baseline’s functional specifications are stated to be weaker, so full-correctness columns are not directly like-for-like.
  • how much was read: most of it read
  • source
  • record id: pdr-universal-invariants-2015
• Differential radical invariants (2014)
  • title: Characterizing Algebraic Invariants by Differential Radical Invariants
  • what: Characterizes invariant algebraic varieties of polynomial vector fields using a finite chain of successive Lie derivatives of one polynomial. The resulting differential-radical invariant rule is sound and complete for checking invariance over real-closed fields, and generation reduces to maximizing the kernel dimension (equivalently minimizing rank) of a symbolic matrix. Defines the Zariski closure of an ODE orbit as the smallest algebraic overapproximation, proves its soundness and differential-ideal property, and establishes the differential radical characterization theorem: h vanishes on an orbit iff finitely many Lie derivatives vanish initially. Theorem 2 gives a decidable invariant-variety check and a sound/complete proof rule; Theorem 3 says every invariant variety is a differential-radical ideal of one polynomial. Homogenization converts generation to biaffine symbolic linear algebra; Gaussian elimination searches parameter assignments and Proposition 3 gives a sound orbit overapproximation condition. Case studies recover trigonometric identities, airplane collision invariants, and three longitudinal-aircraft energy functions.
  • number: M2,1: 35×15, 90 nonzeros, kernel dimension 3
  • number: M2,3: 126×15, 693 nonzeros, kernel dimension 5
  • number: aircraft M3,1: 495×165, 2,115 nonzeros
  • number: one-hour Mathematica run on 1.7 GHz Core i5 / 4 GB
  • limits: Systems are autonomous polynomial ODEs with explicit vector fields and unique local maximal solutions; nonautonomous polynomial time can be encoded by a clock. Zariski closure abstracts away time direction and can be uninformative when the vanishing ideal is zero (e.g., generic one-dimensional evolving fields). Generation is at least NP-hard and PSPACE under stated no-parameter assumptions; de-homogenization may fail for projective candidates. Results target algebraic equalities, not general semialgebraic safety regions; upper bounds on differential-radical order and hybrid-system use remain future work.
  • how much was read: most of it read
  • source
  • record id: differential-radical-invariants-2014
• ICE (2014)
  • title: ICE: A Robust Framework for Learning Invariants
  • what: Introduces ICE learning, in which a black-box invariant learner receives positive examples, negative counterexamples, and implication pairs generated by a white-box teacher. It formalizes honest teachers and strong convergence, then gives learners for Boolean combinations of numerical constraints and universally quantified array/list properties. Defines ICE samples (E,C,I), target descriptions, iterative rounds, honesty/progress, and strong convergence under arbitrary teacher choices. For scalar programs, the learner enumerates Boolean templates of octagonal constraints with bounded constants and solves a quantifier-free linear integer arithmetic encoding using incremental Z3; dovetailing guarantees simplest-template search and strong convergence. For quantified invariants, it lifts learning to sets of valuation words and adapts RPNI state merging to elastic quantified data automata (EQDAs), yielding polynomial work per round and strong convergence for fixed alphabets. Boogie/SMACK and a QDA teacher connect the abstractions to C and array programs.
  • number: 28 numerical benchmark rows
  • number: octagonal constraints with constants |c|≤M
  • number: EQDA runs 3–18 rounds, 8–21 states, 0.3–9.4 s
  • number: Theorem 1 scalar strong convergence; Theorem 3 EQDA strong convergence
  • limits: Scalar learning is complete only relative to the enumerated template class and bounded constants, though dovetailing eventually explores all finite templates. The teacher must soundly generate examples, counterexamples, and inductiveness implications using verification conditions. EQDA strong convergence relies on a fixed finite set of pointer and quantified variables; no polynomial-time iterative learner exists for unbounded alphabets. Array experiments use decidable array-property-fragment translations; list support is described but not evaluated because no Strand decision procedure was available. Learners synthesize invariants expressible in their concept classes and do not remove underlying theorem-proving costs.
  • how much was read: most of it read
  • source
  • record id: ice-2014
• QDA quantified invariant learning (2013)
  • title: Learning Universally Quantified Invariants of Linear Data Structures
  • what: Introduces quantified data automata (QDAs) for universally quantified properties of linear data structures and reduces active QDA learning to Moore-machine learning; elastic QDAs support decidable verification conditions. Theorem 1 establishes a unique minimal QDA for valuation-word languages; Theorem 2 gives a polynomial active learner assuming membership/equivalence teachers, with complexity also depending on longest counterexample. Theorem 3 constructs the most precise elastic over-approximation using blank-symbol closure, powerset states and formula-lattice joins. Section 6 translates EQDAs to Strand exactly and to the array property fragment by a sound one-way abstraction. The implementation uses libALF and a passive sample teacher over bounded executions, learns QDAs, elastifies and converts them to formulas, then validates adequate invariants with an SMT solver. Table 1 contains 25 invariant/postcondition rows and 3 precondition rows, including sorting, cachePage, Glib, Linux/driver routines and GNU sortlines.
  • number: 25 invariant/postcondition rows and 3 precondition rows
  • number: learned automata 4–42 states in Table 1
  • number: Tlearn 0.00–0.11s
  • number: list-partition 16395 tests, 11807 membership queries, 11.40s teacher time
  • limits: Fixed finite pointer/universal-variable sets and formula lattice; quantifier-free data theory must be decidable. Universal variables occupy distinct positions in the word encoding. General QDA emptiness is undecidable; EQDA restrictions exclude bounded-distance tests. Sample-based membership rejects unseen words and can produce a nonminimal invariant; passive runtime is polynomial in the learned automaton, not the smallest true invariant. APF translation can over-approximate semantics. Black-box inference discards program-code information and empirical adequacy still needs SMT checking.
  • how much was read: most of it read
  • record id: qda-quantified-invariant-learning-2013
• TRACER symbolic execution verifier (2012)
  • title: TRACER: A Symbolic Execution Tool for Verification
  • what: Presents TRACER, a symbolic-execution verifier for safety assertions in sequential C. It builds a finite overapproximating symbolic tree, learns weak interpolants from infeasible paths to subsume paths, and widens/refines loop invariants for unbounded loops. The paper gives the path-subsumption mechanism based on underapproximated weakest preconditions, unsatisfiable cores and quantifier elimination, then works a guarded increment example where WP reduces an exponential tree to a linear one. For loops it dynamically widens candidate invariants, detects spurious errors, extracts a WP interpolant and restarts; the Windows-driver example shows why the refinement must preserve new != old. The implementation translates CIL programs (including pointers/arrays and alias partitions) to CLP(R), supports SP/WP/CLP interpolation and optional InterProc invariants, and reports proof trees or counterexamples.
  • number: 900-second timeout
  • number: WP s3 client times 61, 115, 338, 80 seconds
  • number: WP s3 server times 33, 120, 37, 27 seconds
  • number: WP reduces symbolic states, e.g. cdaudio 2138 vs SP 4663
  • limits: Targets finite-state safety properties of sequential C and quantifier-free first-order assertions; CLP(R) reasoning is linear arithmetic over reals plus arrays, while WP currently supports only linear real arithmetic. Loop invariant generation is incomplete and may not terminate because candidates come only from propagated constraints, widening is naive and per-candidate (richer subsets would be exponential). If execution does not terminate, safety is not reported; abstraction can yield spurious errors requiring refinement.
  • how much was read: most of it read
  • record id: tracer-symbolic-execution-verifier-2012
• Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification (2012)
  • what: LLVM-based configurable framework for sequential C assertion safety. Computes safe inductive invariant or counterexample using an abstract reachability graph over loop cutpoints. Abstract post, refiner and expansion policy parameterize predicate abstraction, interpolation and combined algorithms. Explains all-inlined SSA preprocessing, explicit repair of uninitialized-variable nondeterminism before compiler optimization, loop-free path encoding delegated to SMT, inductiveness checks and exact differences among three instantiations. Combined method closes an interpolant candidate under abstract transitions, which enlarges its state set rather than merely conjoining stronger predicates.
  • limits: §§1–2: sequential C safety/assertions; formal program model uses transition relation, initial/error formulas and variables. Successful invariant I must include all initial states, be inductive and disjoint from error states. No termination/liveness/concurrency/distributed algorithm proof. §2.1: intraprocedural analysis requires all functions inlined into main and expects SSA via mem2reg. This is not interprocedural verification of unbounded recursion. Other LLVM-source languages C++,Ada,Fortran discussed as potential experimentation, not demonstrated support/semantic coverage or verified Rust frontend. §2: claims preprocessing gives semantically equivalent optimized program; relies on frontend/transforms/SMT and explicit benchmark semantics. No mechanized frontend or end-to-end framework soundness proof here. Certificate is safe inductive invariant for optimized LLVM model, not separately validated proof-carrying binary or certified compiler. §2.1/Fig.2: verification benchmarks interpret uninitialized variables nondeterministically, while LLVM undef optimization may choose values that remove branches. Ufo-specific pass inserts external nondet() initialization before optimizations to preserve intended benchmark choices. Does not establish that every C undefined behavior or memory/integer semantic issue is handled. §2.1: debug information emitted by clang maps optimized counterexamples back to C. Neither reconstructed source traces nor LLVM-source equivalence independently checked here. LLVM native optimizations/compilers are trusted rather than verified in this paper. §2.1–2.2: cutpoint graph summarizes loop-free paths; weak topological ordering schedules inner before outer loops. ARG is a DAG-like unrolling annotated by state overapproximations. SMT compactly encodes potentially exponentially many paths, not a proof of polynomial algorithm complexity or absence of solver blowup. §2.2: abstract post must overapproximate edge successors; refiner removes spurious error paths or reports counterexample; SMT checks invariant certificates. Current interface uses MathSAT5 interpolation and Z3 quantifier elimination. No certificate checker independent of these SMT results or artifact proof replay shown. §3: UD label refers to interpolation-driven exploration of program paths; its abstract post still returns true, the weakest overapproximation. Interpolant annotations are candidate invariants until inductiveness checked; failed guess expands at innermost failing loop. Do not interpret a guessed invariant as certified or UD annotations as concrete-state underapproximations. §3: OD uses Boolean/Cartesian predicate abstraction, uses interpolants to extend predicates rather than directly guessing ARG annotations, and eager expansion recomputes from initial states. Combined uses lazy failure-point expansion with predicate closure from candidate I, obtaining Ip with I⇒Ip, then further interpolation if not safe/inductive. §3: combined method trades fewer refinements against expensive abstract-post computations. Claims it can outperform both OD and UD refer to prior paper [1]; no benchmark table, timings, hardware, solved counts or empirical comparison included in this seven-page tool paper. §§1/3: novelty/first-tool claims and relative power are author assertions. No new formal algorithm theorem/proof, repository execution, scalability study, Verus/Rust/TLA+ implementation or LLM evaluation established here.
  • how much was read: most of it read
  • record id: ufo-a-framework-for-2012
• HMC: Verifying Functional Programs Using Abstract Interpreters (2011)
  • what: Hindley-Milner-Cousots reduces typed higher-order functional-program safety to first-order imperative safety through refinement constraints. Unknown predicates become relations, encoded by mutually recursive first-order functions whose input/output tuples represent those relations. Uses existing ARMC or Interproc analyses to infer safe constraints without user-supplied refinement predicates. Explains polarity of function subtyping, translation of lower-bound constraints into nondeterministic callee blocks and concrete upper bounds into main assertions, and the distinction between constraint satisfiability equivalence and one-way source safety. Higher-order indexed iterator illustrates three-variable bounds beyond octagons. Context-insensitive template merging gives an explicit safe finite-Boolean example the current frontend cannot verify.
  • limits: §2/footnote1: soundness formalization uses core μML and call-by-value small-step semantics; errors arise when primitives receive out-of-domain values. Safety means no finite reduction reaches Err, not termination or total functional correctness. Arrays have pre-specified get/set bounds contracts; assert requires true. §§2.1/2.2: relation variables range over typed base values (integers, Booleans, uninterpreted encodings for richer values); model maps each variable to an n-ary relation. Complex data structures/higher-order flow handled by refinement typing, numeric correlations by backend invariants. Formal source generator and theorem proofs omitted to reference [11]. No language/compiler/backend implementation mechanization claimed. §2.1/Theorem1: satisfiable generated constraints imply source safety. Converse not established and false for the current context-insensitive frontend. §2 p.474 prose briefly says constraints satisfiable if program safe, reversing Theorem1; follow the theorem and explicit §4 incompleteness. Unsafe/unknown backend result therefore need not be a concrete unsafe source execution. §2.2/Theorem2: equivalence is constraint satisfiability iff translated μC safety. μC has local variables, nondeterministic assignments, assumptions, assertions, choice and recursive first-order functions. This is a verification encoding, not a semantics-preserving compiler intended to reproduce original outputs/control flow. §2.2/Theorem3: overall soundness conditional on a sound μC verifier, source constraint generation and translation. Boolean Safe/Unsafe interface defines only Safe implication; an imprecise abstract interpreter may raise false alarms. No end-to-end completeness or guaranteed analysis termination. §2.1: exposition suppresses some unknown refinements and adds nonnegative list length for brevity. Do not interpret the hand-shown templates as the entire automatic generator. Function subtyping reverses the domain flow in c2/c4; ignoring contravariance changes the proof obligation. §2.2/Fig.3: printed generic get/set rules bind/return x despite pattern variable x0, and arity notation varies between number of relation fields and function arguments. Explanatory prose and Figure4 use one fewer input than relation fields and return the value coordinate. A formal implementation needs consistent names/arity; no artifact defect established. §3: prototype uses OCaml Hindley-Milner inference and Dsolve constraint infrastructure; well-formedness/scope constraints convert pending substitutions into parameters, then simplification/constant propagation/resolution. Backend ARMC CEGAR or Interproc/Polka polyhedra; avoids user qualifier lists in these examples, not external semantic contracts or type-system assumptions. §3/Table1: 14 small examples each with manually inserted buggy variant; times for backend analysis of translated program, not clearly total source translation plus verification. No hardware, LOC, repetitions/variance, memory, or numeric DNF cutoff specified. DNF denotes did-not-finish, not automatically a 900-second timeout. §3/Table1: ARMC finishes 13/14 safe and 13/14 buggy; heapsort neither. Interproc analyzes all 14 variants but false-alarms on three correct programs (heapsort,lock,sum-acm-m), so proves 11/14 safe. Buggy-case times are analysis outcomes, not a documented source-trace reconstruction or false-alarm precision study. §4: single template per monomorphic function merges call contexts and loses information even with finite Boolean values. Refined intersections plus finite-state backend could recover finite-state completeness in a different generation strategy; omitted from implementation because constraints may grow super-exponentially. Not a general complete verifier for infinite-state higher-order programs. §§1/3: “competitive” with DepCEGAR is author comparison, but this table has no DepCEGAR column, common hardware/budget protocol or significance study. Generic applicability to other source systems/mutable-state languages is a proposed constraint-level extension, not a demonstrated verified Rust/C/concurrency frontend.
  • how much was read: most of it read
  • record id: hmc-verifying-functional-programs-2011
• Splitter predicates (2011)
  • title: Simplifying Loop Invariant Generation Using Splitter Predicates
  • what: Defines splitter and phase-splitter predicates that decompose multi-phase loops into semantically equivalent sequences of single-phase loops. Weakest-precondition and SMT checks find phase transitions, allowing ordinary conjunctive invariant generators to prove assertions requiring disjunctions. A Hoare-triple theorem proves splitter equivalence; a second theorem adds conditions ensuring the branch predicate is constant in each phase. The recursive inside-out algorithm computes a weakest precondition, validates the remaining conditions with an SMT solver, splits and recursively simplifies each loop. A SAIL/Mistral prototype uses SSA and quantifier elimination. Experiments compare Interproc polyhedra and InvGen on literature and real-code benchmarks, including stronger assertion variants.
  • number: 95 OpenSSH loops inspected
  • number: first nine benchmark comparison
  • number: 6 Interproc and 4 InvGen previously failing cases repaired
  • number: 90 ms maximum splitter computation
  • limits: The formal language is integer-valued and restricts holes from occurring inside nested loops; weakest-precondition approximations for nested loops rely on an invariant generator. The method targets conditionals with a fixed number of phase transitions and can miss loops alternating behavior. SMT quantifier elimination and path constraints may be expensive; mergesort demonstrates incomparable/non-improving widening results.
  • how much was read: most of it read
  • source
  • record id: splitter-predicates-2011
• Threader: A Constraint-Based Verifier for Multi-threaded Programs. (2011)
  • what: C verification tool automatically discovers state predicates and transition predicates for monolithic, Owicki-Gries and rely-guarantee safety proofs. Iterates abstract reachability and recursion-free Horn-clause refinement, comparing the three proof methods on 15 small concurrent programs. Concrete proof rules distinguish state-based interference closure from binary environment relations; pair-specific transition abstractions constrain environment effects while preserving a thread’s locals. Horn satisfiability supplies refinement predicates; unsatisfiability identifies real counterexample evidence under the encoding. Table shows different rule strengths in practice: Owicki-Gries solves three-process QRCU, rely-guarantee uniquely solves See-Saw/Scull, and four-process QRCU defeats all three within budget.
  • limits: §2: CIL frontend accepts N functions representing N fixed parallel threads sharing variables. Recursive functions unsupported; other calls inlined. No demonstrated dynamically unbounded thread creation or parameterized proof over every N. Unbounded context switching is separate from unbounded process count. §2: constraint transition model P=(V,initial,error,rho1,…,rhoN); globals initialized and assert statements define bad states. Each thread relation changes only globals and its locals. Full relation is disjunction of thread relations, an interleaving abstraction. Paper does not supply weak-memory, detailed C pointer/heap/arithmetic semantics, frontend correctness proof or Rust ownership model. §2/Fig.2: all auxiliary state assertions Ri are stated over V, not restricted by definition to only globals plus thread-i locals. They may be non-thread-modular; predicate search can optionally be restricted to favor thread-modular proofs. Strongest solution is relative to the chosen abstraction, not an exact reachable-state computation or strongest expressible invariant of the full language. §2: abstraction begins with empty predicate sets; spurious abstract error triggers Horn query, whose solution adds predicates. No general termination/completeness bound or guarantee that finite refinement succeeds on every safe input. Referenced POPL algorithm details not reproduced here. §2 opening p.412 literally says “If no error state is unreachable then Threader reports that the program is safe.” This reverses the intended condition; subsequent rule R∧error→false and reachability discussion specify absence of reachable errors. Record follows formal safety rule and flags prose typo, not a tool defect. §2 p.415: termination capability asserted with details delegated to reference [8], then under submission. Table evaluates safety, not termination or fairness-dependent liveness. No termination proof, ranking-relation example or termination benchmark provided in this six-page paper. §3/Table1: all 15 programs safe, 18–451 C lines; fixed 900-second timeout. No unsafe-input detection/false-positive study, new bug discoveries, hardware setup, repetition/variance, memory usage or direct external-verifier timing comparison reported. Authors’ lack-of-other-tools statement is not a measured competitive study. §3: mutual exclusion assertions instrumented; See-Saw uses invariants from StInG as assertions. Automatic auxiliary-predicate discovery does not mean specifications or benchmark transformations were automatically generated. Scull is a modeled driver benchmark, not demonstrated verification of every configuration of a whole Linux driver. §3 p.416: broad prose says monolithic cannot cope “for all benchmarks”, but Table1 shows three successes. Read failure as a tendency for harder examples, not literal universal failure. Owicki-Gries inability wording for final examples describes this abstraction/refinement experiment, not a general logical incompleteness theorem. §3: no symmetry reduction, contributing to QRCU scalability limit. Claims applicability to ad-hoc synchronization and code with data races concern the abstract program analysis, not legal raceful ISO C++/Rust executions or memory safety under a weak-memory model.
  • how much was read: most of it read
  • source
  • record id: threader-a-constraint-based-2011
• Array-Based Backward Reachability SMT (2010)
  • title: Backward Reachability of Array-Based Systems by SMT Solving: Termination and Invariant Synthesis
  • what: Develops a declarative SMT-based backward-reachability framework for infinite-state array systems. First-order formulas over separate index/data theories represent states; preimages, safety and fixpoint checks are mechanized with quantifier instantiation. Model-theoretic embeddings and well-quasi-order conditions yield termination results, while a dual invariant-synthesis method is complete under corresponding hypotheses. The paper separates symbolic and semantic tracks, defines array-based transition systems and theory conditions for closure/decidability, presents a tableaux-like calculus, and proves undecidability outside restricted classes. It integrates resource-bounded invariant guessing (index and signature abstraction) with exact backward search, checking candidate invariants before pruning. mcmt experiments cover mutual exclusion, cache coherence, imperative array programs and miscellaneous protocols, comparing default and tuned settings.
  • number: Tables 1–4 report tableaux depth/nodes, deletions, Yices calls, invariants and seconds
  • number: German pfs: 31m01s default vs 30m27s best; 858,184 vs 784,168 SMT calls
  • number: Alternating bit: timeout default, 44.48s best with one invariant
  • number: Max in Array: timeout default, 0.03s best with five invariants
  • limits: Termination and completeness require theory-specific local-finiteness, quantifier-elimination/instantiation and well-quasi-order hypotheses; unrestricted safety and satisfiability are undecidable. Quantified SMT is difficult, and mcmt uses Yices plus heuristic instantiation. Invariant synthesis is theoretically complete but can have a huge finite search space; experiments are on selected translated benchmarks and old hardware, with tuned settings potentially non-global best.
  • how much was read: most of it read
  • record id: array-based-backward-reachability-smt-2010
• Directed Proof Generation for Machine Code (2010)
  • what: MCVETO combines concrete traces and symbolic overapproximations to find a target-reaching input, prove target unreachable, or fail to terminate. Builds instruction-level disassembly and nested-word automaton abstraction on demand, supports pointer/byte-memory/bit-vector effects, refines with folded traces and speculative invariants, and explicitly detects executions that violate matched return-address discipline. Explains how feasible traces can refine an overapproximation without SMT/complementation, why guessed invariants require both positive and negative branches, how whole-program nested-word abstractions share interprocedural refinement, and how unvalidated return discipline would make the analysis unsound. Gives concrete language-independent alias-precondition construction and a three-outcome soundness theorem distinguishing acceptable-execution violations from target bugs.
  • limits: §§1–2: safety goal is reachability of a designated target control location. No assumption of precomputed CFG/call graph, source types, fixed alias analysis or protected return/local memory; input is object/machine code without symbol metadata. This is neither arbitrary temporal/liveness verification nor proof of source-to-binary compiler correctness. §2: traces T underapproximate states, abstract graph G overapproximates. Symbolic execution of witnessed prefix plus frontier instruction either generates new feasible input or yields refinement. If no abstract path remains, G is proof; search can fail to terminate. No general termination/completeness guarantee. §§3/3.1: infinite call/return context graph represented finitely by nested-word automata (NWA), closed under intersection. Initial two abstract states classify PC=target versus not; PC is modeled data. Instructions decoded from current memory bytes one at a time during concrete traces, handling instruction aliasing and self-modification rather than assuming static code/data split. §3.1/Fig.5: folding groups equal-PC positions; target surrogate TS covers all unexplored non-target locations and target, with wildcard transitions, alternate unseen branch outcomes, indirect jumps/calls and unfinished traces. Halt goes distinguished rejecting Exit. Omitting these conservative exits would turn tested traces into unsound universal claims. Precise SMC extension deferred to report25. §3.1: trace generalization itself requires no SMT calls or automaton complementation. Overall DPG still calls SMT for path feasibility, refinement and symbolic alias tests; claim is not solver-free verification. §3.2: affine relations from frequently accessed inferred memory locations and strided intervals provide candidate equalities/ranges/congruences. They may miss indirect-write effects. Sound incorporation splits on φ and ¬φ, retains both, and later DPG proves unwanted branches unreachable; candidates are not trusted invariants from observed traces. §3.3: interprocedural refinement shared through whole-program automata; no assumed source local/global split or explicit procedure summaries. Ability to select frontier across procedures depends on policy; closest-target example is a strategy illustration, not dominance or guaranteed avoidance of hard procedures. Detailed automata/transducer/pushdown algorithms deferred to report25. §3.4: instruction semantics supplies symbolic store S′ from identity state; substitute into desired postcondition to compute Pre. Array update/access yields ite conditions; determine definite cases under symbolic state, record alias guard α, simplify ψ′, use α⇒ψ′ as weaker refinement. Concrete-witness variant cheaper but covers fewer states; no claim that all aliasing is statically resolved. §3.4: simplified exposition INT→INT memory/register maps; actual byte memory INT32→INT8 and four accesses per 32-bit word. Byte-precise worked derivation deferred to report25. Requires correct instruction decoder/operational semantics, solver and analyzer implementation; no mechanized verification or proof-certificate validation of MCVETO reported. §3.5: call instructions treated as call positions, ret as returns. Arbitrary machine code can violate this discipline. Auxiliary stack records intended return addresses; acceptable execution (AE) requires nonempty stack and matching processor/auxiliary return address at each ret. Violation is reported as such, not silently excluded or necessarily a target bug. §3.5/Theorem 1: AE violation output supplies actual non-AE input; bug-found supplies AE reaching target; OK implies all program executions AE and target absent during every AE, hence target unreachable. Non-returning jumps into another function not classified solely by source procedure names. This guarantee does not promise a complete target verdict for legitimate nonlocal-return/longjmp code. §3.5 proof: initial accepting PC=target∨V and new internal transition to TS for each ret preserve overapproximation of shortest malformed-return prefixes, of form NWPrefix ret. Without this modification naive matched-return filtering may incorrectly prove safety. Proof sketch rather than mechanized theorem here. §4: TSL instruction semantics and ISAL binary-to-AST definitions generate concrete/symbolic primitives; instantiated x86 and PowerPC. Experiments table is x86 only. Retargetability still depends on accurate supplied instruction semantics, decoder and runtime/environment modeling. §5/Fig.9: 29 small cases,20-minute budget,Windows XP,single core 3.0GHz Xeon,4 GB user process,Visual Studio 8.0 object files. No repetitions/variance, optimization flags, real-world binary scale, concurrency or head-to-head runtime baseline table. Examples selected for low-level complications, not representative corpus. §5/Fig.9: verisec-gxine/simp_ok row outcome says proof but CE/SE/Ref/time all “**”, whose legend means exceeded 20-minute limit. Preserve contradiction; do not count as timed successful proof or silently relabel definitive timeout. Instruction-alias example static instruction count explicitly approximate. §§5–7: large-scale sound binary verification remains future research. Claims of first SMC model checker are author assertions not independently checked. No technical-report appendices, tool execution or reproductions read/performed.
  • how much was read: most of it read
  • record id: directed-proof-generation-for-2010
• Dsolve (2010)
  • title: Dsolve: Safety Verification via Liquid Types
  • what: Introduces Dsolve, which infers Liquid refinement types for OCaml by generating subtyping constraints and solving predicate abstractions with Z3. It verifies array bounds, arithmetic safety, sorting and tree invariants with low annotation overhead and reports inferred types useful for debugging. The weighted_avg example shows higher-order foldn inference: Dsolve infers index bounds for callback f, proves equal positive array lengths, discharges an unreachable assertion and proves nonzero division. The implementation parses a typed OCaml AST, generates template subtyping constraints, and searches conjunctions of user-provided qualifiers; interfaces (.mlq) support modular checking and abstract modules with axioms/uninterpreted functions. Errors are mapped to source lines. The tool found and guided repair of a real vec balancing bug by inferring a balance-factor bound of 4 before the fix.
  • number: array-bound annotation overhead reduced from 17% LOC (DML) to under 1%
  • number: array benchmarks run 1–64 s; bitv is 426 LOC
  • number: data-structure benchmarks run 1–103 s; vec is 343 LOC
  • number: inferred original vec balance factor ≤4 exposed faulty paths and test inputs
  • limits: Inference is restricted to conjunctions of predicates from a finite, user-provided qualifier set, so failure may mean an unsafe program, missing qualifiers or an inexpressible invariant. Dsolve verifies OCaml modules and relies on Z3; whole-program checking uses driver calls unless contracts are supplied. Experiments report runtimes and annotation reductions but no error bars or soundness proof in this short tool paper; abstract modules require user-supplied axioms.
  • how much was read: most of it read
  • record id: dsolve-2010
• Daikon (2007)
  • title: The Daikon system for dynamic detection of likely invariants
  • what: Records values from runs of a program and reports candidate preconditions, postconditions and invariants that held on every observed run, after filtering out coincidences.
  • number: cited earlier studies: precision over 95%, recall over 90%
  • number: about 90% automated lemmas/tactics for three distributed-algorithm proofs (cited)
  • number: NASA CTAS codebase over one million lines had partial specs
  • limits: The properties are not guaranteed over all executions. They are not proofs of safety or liveness.
  • how much was read: most of it read
  • source; notes: The Daikon system for dynamic detection of likely invariants
  • record id: daikon-2007
• IvyBench
  • title: IvyBench: Collection of Distributed Protocol Verification Problems
  • what: IvyBench collects 54 safety-checking problems in Ivy, mypyvy and VMT formats: Paxos, TLA-derived commit examples, locks, elections, I4 cases, FOL-IC3 cases and two DistAI cases.
  • number: 54 safety checking problems: 10 Paxos, 5 TLA-derived, 14 ex, 7 I4, 16 mypyvy/FOL-IC3, 2 DistAI.
  • number: 54 problems: paxos 10, tla 5, ex 14, i4 7, mypyv 16, distai 2
  • number: README says 54 safety checking problems; six advertised groups total 54, but multisig adds four files making 58 Ivy inputs
  • number: Group sizes: distai 2, ex 14, i4 7, multisig 4, mypyv 16, paxos 10, tla 5
  • limits: The README lists benchmark membership, not pass rates or independently reproduced results.
  • how much was read: most of it read
  • source; notes: IC3PO and its shared ivybench collection
  • record id: ivybench
• I3DP (2026)
  • title: I3DP: Neuro-Symbolic Inductive Invariant Inference for Distributed Protocols
  • what: I3DP takes a TLA+ model and a safety goal. TLC screens candidate invariants (facts meant to hold in every reachable state). Apalache checks that each one stays true after every step. An LLM proposes stronger candidates. TLAPS, a proof checker, checks proofs that hold without a size bound. The notes know it only through its public artifact.
  • number: Artifact README records 29/29 passed in replay (not run by the reviewers)
  • number: artifact README records 29/29 replay passed (not rerun by notes)
  • limits: The paper’s full text was not accessible. It covers safety of the model only, not running code or liveness. It has the same authors and benchmarks as IC3Syn (2605.24619) and is apparently its successor, but this is not confirmed. So it is not an independent evaluation.
  • how much was read: parts read
  • source; notes: I3DP: Neuro-Symbolic Inductive Invariant Inference for Distributed Pro; notes: I3DP: Neuro-Symbolic Inductive Invariant Inference for Distributed Pro
  • record id: i3dp-2026
• 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
• 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
• PSyn (2025)
  • title: Guiding Likely Invariant Synthesis on Distributed Systems with LLMs
  • what: Compares LLMs generating invariants directly against symbolic synthesis, on eight Promela distributed systems checked with Spin. In PSyn, the LLM proposes predicates from counterexamples.
  • number: 8 Promela systems: Peterson, Bakery, Alternating Bit, Leader Election, UPPAAL Train/Gate, Distributed Lock Server, Producer Consumer, Smart Contract
  • limits: The target is probably invariants for monitoring, not proofs.
  • how much was read: parts read
  • record id: psyn-2025
• Scimitar (2025)
  • title: Interpretable Safety Verification of Distributed Protocols by Inductive Proof Decomposition
  • what: Scimitar breaks a proof into a graph of lemmas and transitions. This exposes where guidance is needed. The target is Raft LogMatching, on a modified model of about 600 TLA+ lines.
  • number: 21 hours, 33 total lemma nodes
  • number: grammar has 173 predicates
  • number: 33 lemma nodes
  • number: 173 grammar predicates
  • limits: The draft the notes inspected has a different title from earlier and later records, and a placeholder conference header. One property of an edited model is not a complete verification of Raft.
  • how much was read: parts read
  • source; notes: papers inspected
  • record id: scimitar-2025
• Kondo (2024)
  • title: Inductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline Distributed Protocol Proofs
  • what: Kondo derives inductive invariants for Dafny protocol proofs from the protocol’s structure. This reduces the invariants the user must write.
  • number: Paxos: 418 lines, Kondo needs 20 user invariants, 777 total proof lines, 42.9 s
  • number: IronFleet 4,581 lines of Dafny and Verdi 50,000 lines of Coq for manual proofs
  • number: Paxos row: 631 model lines; 27 invariant clauses without Kondo vs 20 synchronous; 856 proof lines without Kondo vs 557 synchronous plus 220 modified
  • number: Table 1 p. 848: 10 systems (Echo Server, Ring Leader Election, Simplified Leader Election, Two-Phase Commit, Paxos, Flexible Paxos, Distributed Lock, ShardedKV, ShardedKV-Batched, Lock Server)
  • limits: Liveness proofs are beyond its scope. Line counts are not measured human hours.
  • how much was read: parts read
  • source; notes: papers inspected
  • record id: kondo-2024
• Updria / Lambda (2024)
  • title: Invariant Checking for SMT-Based Systems with Quantifiers
  • what: Two algorithms that automatically find invariants of the form ‘for all processes i, j: …’ for protocols with an unbounded number of nodes and numeric data. One refines an abstraction step by step (Updria); the other generalizes from small instances and then checks the guess (Lambda).
  • number: benchmarks: 238 MCMT-format systems, 52 VMT/MyPyvy systems, 25 train-control systems
  • number: MCMT family: Lambda solves 214, Updria 208, MCMT 172 of 238 (Table 3)
  • number: VMT family: Lambda 29, Updria 29, Ic3po 36, MyPyvy 27 of 52
  • number: trains family: Lambda 25, Updria 24 of 25
  • limits: Finds only universally quantified invariants, so it fails where an existential quantifier is needed (7 more instances solved by Ic3po). The problem is undecidable, so both algorithms may not terminate; Lambda comes with no guarantee that its guess works. Safety only; no liveness.
  • how much was read: parts read
  • source; notes: ## Invariant Checking for SMT-based Systems with Quantifiers (2024)
  • record id: updria-lambda-2024
• Yao thesis (DistAI, DuoAI, LVR) (2024)
  • title: Automated Verification of Safety and Liveness Properties for Distributed Protocols (PhD thesis)
  • what: It shows that liveness can be reduced to a list of simpler safety properties, which invariant-inference tools often prove automatically. One task is left: synthesize a ranking function (a number that decreases toward the goal) to prove termination. It was applied to 8 protocols, including Paxos. It also covers DistAI and DuoAI.
  • number: 37 of 40 generated safety properties are always true, inductive, or get an invariant automatically; 3 found manually in a few hours each
  • number: every Z3 query to synthesize a ranking function finished in under a second
  • number: manual effort 128 and 165 lines versus IronFleet’s 2,093 and 7,869 lines of Dafny (16x and 47x less)
  • number: DuoAI covers 27 protocols and solves Paxos more than two orders of magnitude faster than any alternative
  • limits: It handles only “eventually” properties, not bounded time. Ranking functions are polynomials only. It works on protocol-level models, not code. It assumes fair scheduling, minimum packet delivery and a contention-free Paxos round. Part of the line-count gap is Dafny versus mypyvy. The notes’ author read about 20% of the 137 pages.
  • how much was read: parts read
  • source
  • record id: yao-thesis-distai-duoai-lvr-2024
• Sift (2022)
  • title: Sift: Using Refinement-guided Automation to Verify Complex Distributed Systems
  • what: Starting from a specification, an implementation model and intermediate layers, it turns each layer-to-layer obligation into a safety problem. It infers invariants with IC3PO and generates C++ with Ivy.
  • number: six cases: leader election, distributed lock, two-phase commit, sharded hash table, Raft, Multi-Paxos
  • number: manual work under five minutes for the three small cases, one person-month for Raft, three person-weeks for Multi-Paxos
  • number: Raft proof effort 1 person-month
  • number: MultiPaxos effort 3 person-weeks
  • limits: The top-level abstraction proofs for Raft and Multi-Paxos are manual or reused. Imperative optimizations may need loop invariants written by hand. It targets C++, not Rust.
  • how much was read: parts read
  • source; notes: papers inspected; notes: Sift: refinement from protocol down to executable systems
  • record id: sift-2022
• Paxos with IC3PO (2021)
  • title: Towards an Automatic Proof of Lamport’s Paxos
  • what: Uses IC3PO along a hierarchy of simpler protocols chosen by a human: Voting, SimplePaxos, ImplicitPaxos, Paxos, then Flexible Paxos and Multi-Paxos. It passes strengthening assertions (extra facts that make the proof go through) upward.
  • number: Pages 112-122
  • limits: The hierarchy of abstractions, and its link to the intended system, are separate human work.
  • how much was read: parts read
  • source; notes: papers inspected; notes: IC3PO and its shared ivybench collection
  • record id: paxos-with-ic3po-2021
• Temporal prophecy (2021)
  • title: Temporal prophecy for proving temporal properties of infinite-state systems
  • what: Adds prophecy variables (recorded predictions about future execution) to the earlier abstraction method. This lets it keep distinctions that the abstraction lost, without strengthening the contract with the environment.
  • number: four cases: ticket protocol, alternating bit, hybrid reliable broadcast, TLB shootdown
  • number: user invariant conjectures 60, 70, 58, 102
  • number: checking takes 7, 25, 25, 240 seconds
  • number: Figure 3 (model lines; conjectures; checker seconds): ticket with task queues 90; 60; 7; alternating bit 143; 70; 25; hybrid reliable broadcast 166; 58; 25; TLB shootdown 468; 102; 240 (checking time, not authoring time)
  • limits: Prophecy formulas are extracted automatically only from an invariant the user supplies. Choosing the witness is manual. No claim of completeness.
  • how much was read: parts read
  • source; notes: Ivy: dynamic abstraction and temporal prophecy; notes: additional temporal methods
  • record id: temporal-prophecy-2021
• Apalache (2019)
  • title: Apalache: temporal properties tutorial, feature table and TLA+ model checking made symbolic
  • what: Apalache is a model checker for TLA+ that works on symbols instead of listing states, using an SMT solver. It checks state, action and trace invariants, inductive invariants (a property that holds at the start and is preserved by every step) and temporal properties.
  • limits: Apalache parses ASSUME but does not pass it to the solver. It does not use THEOREM. Its bounded checks do not prove properties for unbounded runs. The authors did not read the original paper.
  • how much was read: parts read
  • source; notes: tools; notes: Model checking: what a successful run means
  • record id: apalache-2019
• Bounded quantifier instantiation (2017)
  • title: Bounded Quantifier Instantiation for Checking Inductive Invariants
  • what: This work limits how deeply quantifiers are instantiated, not the number of participants. That makes checking an inductive invariant decidable (a procedure always gives an answer).
  • number: Journal Table 1: 9 rows; conference Table 1 has 7 (no trusted-chain rows)
  • number: Bound 1 proves the invariant inductive in all correct examples
  • limits: No artifact is available. The ring case checks an invariant related to termination, not a full liveness proof.
  • how much was read: parts read
  • source; notes: Cutoff and bounded instantiation leads
  • record id: bounded-quantifier-instantiation-2017
• Proving that non-blocking algorithms don’t block (2009)
  • what: The first fully automatic tool to prove non-blocking liveness (lock-free and obstruction-free) of concurrent data structures. It uses rely-guarantee reasoning (each thread assumes what others do and promises what it does), shape analysis and a termination prover.
  • number: lock-freedom proofs found in under 10 minutes for all cases except Michael’s list, which took about 8 hours
  • number: found a linked-list deletion in Fomitchev and Yahav that is not obstruction-free
  • limits: It is not about distributed systems. The review notes read about 25% of the paper.
  • how much was read: parts read
  • source
  • record id: proving-that-non-blocking-2009
• PVerifier
  • title: PVerifier (P language verification extensions)
  • what: It checks inductive proofs of designs written in the P language. Users supply assumptions and an inductive invariant. UCLID5 and an SMT solver check that the invariant holds initially, that each step preserves it, and that it implies the desired property. A two-phase-commit tutorial shows that if the protocol accepts, every participant preferred acceptance.
  • limits: The claim holds for the supplied P design under its assumptions. The 2PC tutorial proves no theorem that the protocol completes despite crashes. An internal verification of sharded transactions with snapshot isolation is reported by the author, and its details are unreleased.
  • how much was read: parts read
  • source; notes: PVerifier
  • record id: pverifier
• ProofSaX (2026)
  • title: Synthesizing Proofs Using Proof Sharding and Exploration
  • what: ProofSAX is not an LLM. It splits a proof task into shards and searches annotations in parallel for safety proofs of distributed systems.
  • number: finds the last proof annotation in 86 of 103 proof-completion tasks, runtimes one minute to two hours
  • number: leader election fully automatic in under two minutes
  • number: ten 20-core machines
  • limits: It covers safety only. For Paxos and Raft it finds only the last annotation.
  • how much was read: only abstract or first pages read
  • source
  • record id: proofsax-2026
• Towards Quantifier-Free Interpolation in Array Languages with Unbounded Data Specifications (2026)
  • what: The paper proves quantifier-free interpolation for combinatory array logic with iterated diffs. It also proves uniform interpolation for a flat array fragment.
  • limits: It has no distributed case study and no LLM component.
  • how much was read: only abstract or first pages read
  • source
  • record id: towards-quantifier-free-interpolation-2026
• Super-V (2025)
  • title: Bolt-On Strong Consistency: Specification, Implementation, and Verification
  • what: It verifies a Raft-like replicated store built on a weak replicated store. SMT checks local, stable preconditions on updates.
  • limits: Only the abstract was read. The PDF was not obtained.
  • how much was read: only abstract or first pages read
  • source
  • record id: super-v-2025
• Bakery IC3PO (2023)
  • title: Towards an Automatic Proof of the Bakery Algorithm
  • what: It uses IC3PO to compute invariants that hold in every reachable state and are strong enough to prove the property, for two versions of the Bakery mutual-exclusion algorithm. It starts from TLA+ specifications.
  • number: Pages 21-28
  • limits: The notes did not retrieve the open PDF, the exact version names, or the proof artifacts. The paper makes no claim about liveness (that something good eventually happens).
  • how much was read: only abstract or first pages read
  • source; notes: Cutoff automation with seven concrete protocols
  • record id: bakery-ic3po-2023
• Ivy: A Multi-modal Verification Tool for Distributed Algorithms. (2020)
  • what: . Ivy is a multi-modal verification tool for correct design and implementation of distributed protocols and algorithms, supporting modular specification, implementation and proof. Ivy supports proving safety and liveness properties of parameterized and infinite-state systems via three modes: deductive verification using an SMT solver, abstraction and model checking, and manual proofs using natural deduction.
  • limits: Not read; claims unverified.
  • how much was read: only abstract or first pages read
  • source
  • record id: ivy-a-multi-modal-2020
• Threshold decomposition (2019)
  • title: Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics
  • what: Decomposes verification of threshold-based fault-tolerant distributed protocols into EPR and BAPA. An automatic inference algorithm generates threshold-intersection properties; EPR verifies protocol transition systems and BAPA checks property soundness.
  • number: Evaluates Bosco safety, Hybrid Reliable Broadcast safety/liveness, and Byzantine Fast Paxos safety
  • number: Ten repetitions per experiment on a 2.2 GHz Core i5 laptop
  • number: Aip generated all valid formulas in under one minute; minimized sets contain 3–5 formulas versus 39–79 before minimization
  • number: Verified protocols include fast-learning Byzantine consensus; threshold inference takes minutes
  • limits: The user supplies an inductive invariant and models the protocol in EPR; the method targets restricted threshold use and relies on liveness-to-safety reduction where needed.
  • how much was read: only abstract or first pages read
  • source
  • record id: threshold-decomposition-2019
• Termite (2015)
  • title: Synthesis of Ranking Functions Using Extremal Counterexamples
  • what: Presents a complete method for synthesizing lexicographic linear ranking functions supported by inductive invariants, refining constraints using extremal counterexamples. The Termite prototype is compared with termination analyzers.
  • number: Termite implementation: 3,000 lines of OCaml
  • number: Benchmark suites: PolyBench 30 (22 solved), Sorts 6 (5), TermComp 129 (119), WTC 58 (46)
  • number: Termite solved 33% more examples than Loopus, in twice the time
  • limits: The method targets termination of programs whose transition relations include disjunctions and existential conditions; benchmark comparisons include front-end and invariant-generator limitations.
  • how much was read: only abstract or first pages read
  • source
  • record id: termite-2015
• Colón-Sipma termination (2002)
  • title: Practical Methods for Proving Program Termination
  • what: Presents two algorithms that synthesize linear ranking functions from generated invariants: one based on widening and polyhedral cones, and a heuristic for structured programs with single-variable rankings.
  • number: One example’s invariant generation and termination proof took 2.5 seconds
  • number: The first method handles subtle linear combinations but is limited to few variables
  • limits: The algorithms target imperative programs and loop termination; the second method is heuristic and assumes structured programs.
  • how much was read: only abstract or first pages read
  • source
  • record id: colo-n-sipma-termination-2002
• A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems.
  • what: . Reinforcement learning has received much attention for learn- ing controllers of deterministic systems. We consider a learner-verifier framework for stochastic control systems and survey recent methods that formally guarantee a conjunction of reachability and safety properties.
  • how much was read: only abstract or first pages read
  • source
  • record id: a-learner-verifier-framework
• A Learning-Based Approach to Synthesizing Invariants for Incomplete Verification Engines
  • what: We propose a framework for synthesizing inductive invariants for incomplete verification engines, which soundly reduce logical problems in undecidable theories to decidable theories. Our framework is based on the counterexample guided inductive synthesis principle and allows verification engines to communicate non-provability information to guide invariant synthesis. We show precisely how the verification engine can compute such non-provability information and how to build effective learning algorithms when invariants are expressed as Boolean combinations of a fixed set of predicates.
  • how much was read: only abstract or first pages read
  • source
  • record id: a-learning-based-approach
• Array Abstractions from Proofs
  • what: . We present a technique for using infeasible program paths to automatically infer Range Predicates that describe properties of un- bounded array segments. First, we build proofs showing the infeasibility of the paths, using axioms that precisely encode the high-level (but in- formal) rules with which programmers reason about arrays.
  • how much was read: only abstract or first pages read
  • source
  • record id: array-abstractions-from-proofs
• ESBMC v6.0: Verifying C Programs Using k-Induction and Invariant Inference
  • what: ESBMC v6.0: Verifying C Programs Using k -Induction and Invariant Inference (Competition Contribution) Mikhail R. Gadelha1(B) , Felipe Monteiro2 , Lucas Cordeiro3 , and Denis Nicole4 1 SIDIA Instituto de Ciência e Tecnologia, Manaus, Brazil m.gadelha@samsung.com 2 Federal University of Amazonas, Manaus, Brazil felipemonteiro@ufam.edu.br 3 University of Manchester, Manchester, UK lucas.cordeiro@manchester.ac.uk 4 University of Southampton, Southampton, UK dan@ecs.soton.ac.uk Abstract. ESBMC v6.0 employs a k-induction algorithm to both fal- sify and prove safety properties in C programs.
  • how much was read: only abstract or first pages read
  • source
  • record id: esbmc-v6-0-verifying
• Full-program induction: verifying array programs sans loop invariants
  • what: Arrays are commonly used in a variety of software to store and process data in loops. Automati- cally proving safety properties of such programs that manipulate arrays is challenging. We present a novel verification technique, called full-program induction, for proving (a sub-class of) quanti- fied as well as quantifier-free properties of programs manipulating arrays of parametric size N .
  • how much was read: only abstract or first pages read
  • source
  • record id: full-program-induction-verifying
• GACAL: Conjecture-Based Verification - (Competition Contribution).
  • what: GACAL: Conjecture-based Verification (Competition Contribution) TACAS Artifact Benjamin Quiring ⋆ and Panagiotis Manolios SV-COMP 2020 Northeastern University, Boston MA, USA Accepted Abstract. GACAL verifies C programs by searching over the space of possible invariants, using traces of the input program to identify poten- tial invariants. GACAL uses the ACL2s theorem prover to verify these potential invariants, using an interface provided by ACL2s for connecting with external tools.
  • how much was read: only abstract or first pages read
  • source
  • record id: gacal-conjecture-based-verification
• Learning Assumptions for Compositional Verification of Timed Automata.
  • what: . Compositional verification, such as the technique of assume- guarantee reasoning (AGR), is to verify a property of a system from the properties of its components. It is essential to address the state explosion problem associated with model checking.
  • how much was read: only abstract or first pages read
  • source
  • record id: learning-assumptions-for-compositional
• Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants.
  • what: . Essential tasks for the verification of probabilistic programs include bounding expected outcomes and proving termination in finite expected runtime. We contribute a simple yet effective inductive synthesis approach for proving such quantitative reachability properties by generat- ing inductive invariants on source-code level.
  • how much was read: only abstract or first pages read
  • source
  • record id: probabilistic-program-verification-via
• Quantified Invariants via Syntax-Guided Synthesis
  • what: . Programs with arrays are ubiquitous. Automated reasoning about arrays necessitates discovering properties about ranges of elements at certain program points.
  • how much was read: only abstract or first pages read
  • source
  • record id: quantified-invariants-via-syntax
• Ranking LLM-Generated Loop Invariants for Program Verification
  • what: foundational AI models that have revolutionized Language Processing applications. Though LLMs Synthesizing inductive loop invariants is fun- damental to automating program verification. were originally proposed for natural languages, In this work, we observe that Large Language they have exhibited great success in formal lan- Models (such as gpt-3.5 or gpt-4) are capa- guages such as programming languages (Chen ble of synthesizing loop invariants for a class of et al., 2021).
  • limits: Abstract-level reading from openly available PDF; detailed limitations require full paper review.
  • how much was read: only abstract or first pages read
  • source
  • record id: ranking-llm-generated-loop
• Software Verification with PDR: An Implementation of the State of the Art.
  • what: . Property-directed reachability (PDR) is a SAT/SMT-based reachability algorithm that incrementally constructs inductive invariants. After it was successfully applied to hardware model checking, several adaptations to software model checking have been proposed.
  • how much was read: only abstract or first pages read
  • source
  • record id: software-verification-with-pdr
• Synthesizing Probabilistic Invariants via Doob’s Decomposition.
  • what: . When analyzing probabilistic computations, a powerful ap- proach is to first find a martingale—an expression on the program vari- ables whose expectation remains invariant—and then apply the optional stopping theorem in order to infer properties at termination time. One of the main challenges, then, is to systematically find martingales.
  • how much was read: only abstract or first pages read
  • source
  • record id: synthesizing-probabilistic-invariants-via
• Termination and non-termination specification inference.
  • what: To capture the termination and non-termination behaviors of Techniques for proving termination and non-termination of imper- each program, Le et al. [32] has recently proposed an integrated ative programs are usually considered as orthogonal mechanisms. specification logic with three temporal predicates Term M, Loop In this paper, we propose a novel mechanism that analyzes and and MayLoop, which denote, respectively, the scenarios for definite proves both program termination and non-termination at the same program termination (with a lexicographic ranking measure M made time.
  • how much was read: only abstract or first pages read
  • source
  • record id: termination-and-non-termination
• Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction.
  • what: . This paper introduces the Averroes formal verification sys- tem which exploits the power of two complementary approaches: counter- example-guided abstraction and refinement (CEGAR) of the design’s datapath and the recently-introduced IC3 and PDR approximate reach- ability algorithms. Averroes is particularly suited to the class of hardware designs consisting of wide datapaths and complex control logic, a class that covers a wide spectrum of design styles that range from general- purpose microprocessors to special-purpose embedded controllers and accelerators.
  • how much was read: only abstract or first pages read
  • source
  • record id: unbounded-scalable-verification-based
• Verification-Aided Learning of Neural Network Barrier Functions with Termination Guarantees.
  • what: Verification-Aided Learning of Neural Network Barrier Functions with Termination Guarantees Shaoru Chen1 , Lekan Molu1 , Mahyar Fazlyab2 Abstract— Barrier functions are a general framework for establishing a safety guarantee for a system. However, there is no general method for finding these functions. To address this shortcoming, recent approaches use self-supervised learning techniques to learn these functions using training data that are arXiv:2403.07308v1 [cs.LG] 12 Mar 2024 periodically gen
  • how much was read: only abstract or first pages read
  • source
  • record id: verification-aided-learning-of
• Verifying Array Manipulating Programs by Tiling
  • what: . Formally verifying properties of programs that manipulate arrays in loops is computationally challenging. In this paper, we focus on a useful class of such programs, and present a novel property-driven verification method that first infers array access patterns in loops using simple heuristics, and then uses this information to compositionally prove universally quantified assertions about arrays.
  • how much was read: only abstract or first pages read
  • source
  • record id: verifying-array-manipulating-programs
• Lemur (2024)
  • title: Lemur: Integrating Large Language Models in Automated Program Verification
  • what: Lemur uses an LLM to propose intermediate proof goals. A conventional verifier either establishes them or gives feedback.
  • number: Section 5.2: 133 benchmarks (C program plus assertion)
  • number: Section 5.3: 47 selected SV-COMP C programs
  • limits: It covers sequential C programs. It has no list of distributed protocols.
  • how much was read: reading depth not recorded
  • source; notes: Lemur: a useful architecture, with no protocol benchmark
  • record id: lemur-2024
• primal-dual Houdini (2022)
  • title: Induction Duality: Primal-Dual Search for Invariants
  • what: The paper pairs Houdini with a dual search over states. Houdini drops candidate invariants until the remaining ones hold. The method also finds counterexamples for broken protocols.
  • number: Table 2: 20 benchmarks (10 safe, 10 unsafe)
  • number: Fixed VM artifact about 5.45 GB
  • number: Pages 1-29
  • limits: The publisher PDF returned HTTP 403, so the review notes read the artifact instructions and source instead.
  • how much was read: reading depth not recorded
  • source; notes: Primal-dual Houdini: full fixed 20-task evaluation
  • record id: primal-dual-houdini-2022
• FOL-IC3 (2020)
  • title: First-Order Quantified Separators
  • what: Searches for formulas that separate good finite states from bad ones, inside an IC3 proof search. IC3 builds a proof by ruling out states that could lead to a violation.
  • number: Pinned examples/fol directory has 19 files (a manifest, not a count of successes)
  • number: Pages 703-717
  • limits: The list of 19 files is the repository’s contents. It does not claim all of them were proved.
  • how much was read: reading depth not recorded
  • source; notes: FOL-IC3 and mypyvy; notes: FOL-IC3 pinned properties
  • record id: fol-ic3-2020
• Learning dynamic polynomial proofs (2019)
  • what: DQN selects elementary polynomial inference steps, building a small set of nonnegative lemmas. A linear program combines those lemmas into an upper-bound certificate. A permutation-invariant polynomial embedding supports transfer across graph sizes. On dense random maximum-stable-set instances, reports tighter bounds with much smaller final LPs than tested static hierarchy levels. Learned search proposes steps; algebraic rules and final identities justify the certificates. Explains the distinction between a feasible stable set (existential lower bound) and a nonnegativity proof (universal upper bound). Gives strict-positivity completeness for hypercube certificates, a complete-graph dynamic degree-two derivation, and a supplementary n/l lower bound for the specified static LP. Constructs trilinear monomial-orbit features invariant to variable renaming plus max pooling over memories/equalities. Supplies dense LP-based rewards, cached action scoring, full DQN settings, a symmetry ablation and explicit rational graph certificates.
  • limits: Inference rules multiply an established nonnegative polynomial by x_i or 1−x_i and take nonnegative linear combinations. Their soundness requires x in [0,1]^n and correct initial axioms. Stable-set experiments also reduce modulo x_i^2=x_i and x_ix_j=0 for graph edges. Polynomial simplification and coefficient equality must preserve that quotient semantics. The main completeness theorem is quoted from Krivine: strictly positive polynomials on the compact hypercube have a finite nonnegative sum of x^alpha(1−x)^beta generators. The footnote restricts the completeness claim to strict positivity/refutation. It does not prove every merely nonnegative polynomial has such a certificate, nor that bounded-degree learned search is complete. Training uses random graphs with25 vertices and edge probability p in[0.5,1]. Generated memories start with2n inequality axioms and graph/Boolean equalities. Search is capped at100 additions and degree2 intermediate lemmas. Results do not establish performance on arbitrary polynomial optimization, sparse graphs, distributed programs or natural-language statements. No human proofs or optimal α(G) labels train the agent, but the dense reward depends on solving a mathematical LP after each addition. “Unsupervised” here means absence of supplied target proofs/optimum labels; it does not mean learning without an exact optimization environment. The orbit-based embedding and symmetric pooling establish architectural invariance under set enumeration and joint variable relabeling. Invariance is not injectivity or a proof of successful generalization. Fixed degree bounds the orbit feature dimension independently of sufficiently large n, while enumerating polynomials/actions still grows with n. Bounds are certified only if nonnegative coefficients and polynomial identities are checked accurately. Printed rational examples admit exact arithmetic; the paper does not provide a verified LP implementation or a systematic numerical-to-rational certificate-reconstruction/error protocol for every aggregate experiment. Supplementary theorem γ_l≥n/l concerns the precise product-generator hierarchy in Eq.10 with only Boolean and edge equalities. It is not a lower bound for every static method or for formulations strengthened by extra valid inequalities. Dynamic advantage is demonstrated against tested levels2–5 and random legal actions, not every proof search strategy. Only one training seed(0) and one NVIDIA V100 are specified. Test means cover100 random graph instances for each reported size. No intervals, multi-seed variability, end-to-end wall-clock comparison, total GPU training time or ground-truth optimality-gap table is supplied.
  • how much was read: reading depth not recorded
  • record id: learning-dynamic-polynomial-proofs-2019
• 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
• 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
• 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
• Practical Verification of Distributed Systems: Streamlining Safety Proofs Using Invariant Taxonomies, and Verifying Latency Properties Using Symbolic Latency (2025)
  • what: PhD thesis on proving distributed protocols safe by sorting the needed invariants into types, and on extending verification to end-to-end latency. Full text could not be fetched; this record rests on a search-engine summary of the library page.
  • limits: Full text blocked: the Deep Blue library (deepblue.lib.umich.edu) returned a Cloudflare ‘Just a moment’ challenge to command-line fetches, and I did not try to get around it. Nothing here comes from reading the thesis.
  • how much was read: not read; title and metadata only
  • source; notes: Practical Verification of Distributed Systems (2025)
  • record id: practical-verification-of-distributed-2025
• Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols (2023)
  • what: An interactive method in Ivy that stops SMT solvers from diverging on quantifier-heavy proofs of distributed protocols, by abstracting functions as relations and refining with counterexamples.
  • limits: Full text not read: the ACM PDF sits behind a bot check, and no open copy was found. Facts here come from the input abstract and a web-search summary.
  • how much was read: not read; title and metadata only
  • source; notes: Counterexample Driven Quantifier Instantiations (2023)
  • record id: counterexample-driven-quantifier-instantiations-2023
• Mao Michigan thesis
  • title: Automating the Verification of Distributed Systems
  • what: The lead title identifies a University of Michigan thesis on automating distributed-system verification. Deep Blue returned Cloudflare challenges for the handle and guessed bitstream and API/OAI retrievals did not expose the thesis, so its contents were not read.
  • limits: Metadata only. The repository was inaccessible in this pass; the title and repository URL are the only source facts recorded.
  • how much was read: not read; title and metadata only
  • source
  • record id: mao-michigan-thesis
• Schultz Stanford thesis
  • title: Automated and interpretable verification of distributed protocols
  • what: Crossref identifies this as William Schultz’s dissertation on automated and interpretable verification of distributed protocols. The repository landing page redirected to a 403 response during this pass, so the dissertation’s methods and cases were not read.
  • limits: Metadata only. The DOI repository response was HTTP 403, so no abstract or full text was available in this pass.
  • how much was read: not read; title and metadata only
  • source
  • record id: schultz-stanford-thesis

Last edited: 2026-10-31