Automation for distributed protocol proofs and protocol benchmarks

(authored by agents unless marked 🧑)

Research checked on October 6, 2026. This report focuses on discovering or checking inductive invariants and on the concrete protocol sets used to evaluate that work. An inductive invariant holds initially and survives every allowed step; together with an implication to the desired property, it proves that no reachable state violates that property. Safety means a bad event never happens. Liveness means a desired event eventually happens. A finite model check is a proof only for the checked instance unless a separate argument extends it to arbitrary instances.

My synthesis: evaluate three separate tasks: translating human intent into a faithful protocol/property, finding supporting invariants, and checking the resulting proof. Most of the tools below assume the first task has already been done. An LLM can propose invariants; the checker must establish initialization, preservation, and implication for the actual model. Model reachability tests and deliberately faulty variants help detect specifications that pass because they exclude useful behavior.

How to use the benchmark inventory: protocol names identify families, not interchangeable tasks. Keep the exact file, revision, target property, supplied auxiliary invariants, and assumptions. Alternate encodings, strengthened models, and separate properties are recorded separately where the artifact does so. A tool’s shipped examples need not equal its paper’s evaluated set. Per-protocol properties below are plain-English interpretations of cited formulas unless explicitly quoted; they do not imply a liveness proof.

The web-search tool was attempted and failed with HTTP 404. Research continued using live arXiv/publisher/author pages, GitHub source archives/APIs, Zenodo, and OpenAlex searches. Relevant PDFs were downloaded only from open sources, checked for the %PDF header, and read using pdftotext. Repository inspection supplies exact manifests where paper tables omit file variants. Missing source locations or unresolved metadata are stated as gaps rather than filled by guesswork.

A few recurring terms: SMT solvers decide logical formulas, with limits for unrestricted quantified logic. IC3/PDR grows an inductive proof by blocking states that could lead to a violation. Ghost state records information needed only for a proof, such as past requests. Refinement proves that a detailed system implements a simpler specification. A cutoff is a justified finite bound sufficient for a parameterized claim; a small experiment alone does not establish one. EPR is a decidable fragment of first-order logic, usually expressed with an existential block followed by a universal block and no functions that create new terms.

Benchmark download map

These are paper evaluation sets or explicitly labeled repository manifests. The detailed sections give every model name and its property; counts should not be added because many models recur.

Classical inference tools and shared suites

These tools start from a formal transition system and a formal safety condition. Inference: they are useful proof back ends for the proposed agent pipeline; they do not themselves infer the user’s intended property from a vague description.

DistAI

DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols, Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, Suman Jana, Gabriel Ryan, OSDI 2021, pp. 405–421. Paper; PDF; download code/suite; mirror inspected.

It simulates small instances, enumerates formulas consistent with the samples, and checks/refines them with Ivy. The README states: “It takes a simulation-learning-refinement workflow.” Its suite declaration is “The 14 distributed protocols in Ivy.” Full names: async lock server (multi_lock_server), chord ring maintenance (chord), database replication (database_chain_replication), decentralized lock (decentralized_lock), distributed lock (distributed_lock), hashed sharding (shard), leader election (leader), learning switch (switch), lock server (lock_server), Paxos (paxos), permissioned blockchain (blockchain), Ricart-Agrawala (Ricart-Agrawala), simple consensus (consensus), two-phase commit (two_phase_commit). Each is downloaded under protocols/NAME/NAME.ivy; original properties follow in the manifest below.

DuoAI

DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols, Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, OSDI 2022, pp. 485–501. Paper; PDF; download code/suite.

The README says “applies top-down/bottom-up refinement” It allows formulas with both universal and existential quantifiers. Paper Table 1 (p. 497) lists 27 protocols; §7 (p. 496) reports “solving all but 1 of the 27 protocols.” Vertical Paxos runs out of memory in that experiment. This is a safety benchmark: consensus agreement is different from proving that consensus eventually happens. The complete suite is listed below, with the safety property read from each linked .ivy file.

SWISS

Finding Invariants of Distributed Systems: It’s a Small (Enough) World After All, Travis Hance, Marijn Heule, Ruben Martins, Bryan Parno, NSDI 2021, pp. 115–131. Paper; PDF. It enumerates small quantified formulas, checks them with SMT, and combines a broad search for helpful formulas with a search that finishes the proof. §5.1 (p. 123) says its sources are “the I4 benchmarks”, first-order separators benchmarks, and “six Paxos variants”.

Full Table 1 list (p. 124), including the guided run: sdl; ring-election; learning-switch-ternary; lock-server-sync; two-phase-commit; chain; chord; distributed-lock; toy-consensus-forall; consensus-forall; consensus-wo-decide; learning-switch-quad; lock-server-async; sharded-kv; ticket; toy-consensus-epr; consensus-epr; client-server-ae; client-server-db-ae; sharded-kv-no-lost-keys; hybrid-reliable-broadcast; paxos; flexible-paxos; multi-paxos; multi-paxos*; fast-paxos; stoppable-paxos; vertical-paxos. multi-paxos* repeats a protocol with human guidance: the Table 1 caption says “the user provides a correct template”. Thus there are 27 distinct protocol models and 28 rows, not 28 independent tasks. DuoAI uses the same central families, but encodings and experimental assumptions differ. The authoritative SWISS repository and inputs were subsequently located through the primal-dual Houdini artifact documentation. The README supplies run commands and per-model .config files. Related models exist in DuoAI/mypyvy/I4/Paxos made EPR, but these do not necessarily preserve the exact SWISS encoding.

I4

I4: Incremental Inference of Inductive Invariants for Verification of Distributed Protocols, Haojun Ma, Aman Goel, Jean-Baptiste Jeannin, Manos Kapritsos, Baris Kasikci, Karem A. Sakallah, SOSP 2019, pp. 370–384. Code/download; suite converted into Ivy/PYV/VMT. It finds invariants for finite instances with Averroes, generalizes them, and asks Ivy to check induction for all instance sizes. The README says “if it does not, go back to step 1 and increase the model size.” Thus finite checking is candidate generation, not the final argument for arbitrary size.

Full seven-model suite: chord_ring_maintenance (connectivity/no error), database_chain_replication (transaction ordering/atomicity), distributed_lock (exclusive lock ownership per epoch), leader_election_in_ring (unique leader), learning_switch (routing consistency), lock_server (unique client per server), two_phase_commit (consistent commit/abort). The literal source properties are linked in the ivybench manifest below.

FOL-IC3 and mypyvy

First-Order Quantified Separators, Jason R. Koenig, Oded Padon, Neil Immerman, Alex Aiken, PLDI 2020, pp. 703–717. Paper DOI; artifact; pinned implementation/download; separator dependency. The pinned README describes --logic=fol as “for quantifier alternation” and universal as “for universal only.” FOL-IC3 searches for formulas separating good and bad finite structures, within an IC3 proof search.

Pinned examples/fol has 19 files: bosco_3t_safety; client_server_ae; client_server_db_ae; consensus_epr; consensus_forall; consensus_wo_decide; firewall; hybrid_reliable_broadcast_cisa; learning_switch; lockserv; paxos_epr; raft; ring_id; ring_id_not_dead; sharded_kv; sharded_kv_no_lost_keys; ticket; toy_consensus_epr; toy_consensus_forall. This is the repository manifest, not a claim that all 19 were successfully proved. ivybench/mypyv selects 16; Bosco, Paxos, and Raft are not in that subdirectory.

The current mypyvy README calls it “A language for symbolic transition systems, inspired by Ivy.” It supports checking supplied invariants, inference via UPDR, bounded model checking, and traces. Current examples/ is larger than the pinned FOL-IC3 suite; do not report its many duplicate variants as independent protocol families.

IC3PO and its shared ivybench collection

On Symmetry and Quantification: A New Approach to Verify Distributed Protocols, Aman Goel, Karem Sakallah, NFM 2021, pp. 131–150. Paper; implementation; benchmark download. It learns a finite invariant and uses symmetry to generate quantifiers and check a size sufficient for an unbounded proof. The abstract (p. 1) says “the required prefix is automatically inferred without any search”.

Towards an Automatic Proof of Lamport’s Paxos, Aman Goel, Karem A. Sakallah, FMCAD 2021, pp. 112–122. Paper; Paxos models. It uses spatial symmetry, ordered rounds, and hierarchical strengthening. The abstract (p. 1) reports an invariant that “identically matches the human-written one”. This scope includes proof structure and auxiliary assertions; it should not be interpreted as solving raw Paxos from prose.

The ivybench README says “54 safety checking problems”. Repository observation: the six advertised groups total 54, but current multisig/ivy adds four files, making 58 physical Ivy inputs. Several are alternative encodings of the same underlying protocol. Each group below lists every Ivy filename and safety property read from its source. mypyv is the repository’s spelling.

distai (2 Ivy files)

ex (14 Ivy files)

i4 (7 Ivy files)

multisig (4 Ivy files)

mypyv (16 Ivy files)

paxos (10 Ivy files)

tla (5 Ivy files)

The preceding source links preserve the exact input files. Some contain supplied strengthening or proof certificates alongside the intended property; these must be removed or explicitly counted as human guidance when evaluating inference.

Comparability warning supported by the papers

DuoAI Table 1 (p. 497), footnote c, states that a comparison input had “3 bugs”. Footnote i states that IC3PO evaluations “manually provided clauses”. These are claims by the DuoAI authors about other tools’ evaluations. The IC3PO paper should be read alongside that criticism. Inference: evaluation must freeze exact commits and distinguish raw specifications, additional predicates, invariant templates, and strengthening assertions. Counting protocol names alone conceals different amounts of human guidance.

IC3PO paper’s actual 29-protocol experiment (distinct from the larger repository)

Table 2, §8 (pp. 12–13 of arXiv PDF) reports the following complete set: tla-consensus; tla-tcommit; i4-lock-server; ex-quorum-leader-election; pyv-toy-consensus-forall; tla-simple; ex-lockserv-automaton; tla-simpleregular; pyv-sharded-kv; pyv-lockserv; tla-twophase; i4-learning-switch; ex-simple-decentralized-lock; i4-two-phase-commit; pyv-consensus-wo-decide; pyv-consensus-forall; pyv-learning-switch; i4-chord-ring-maintenance; pyv-sharded-kv-no-lost-keys; ex-naive-consensus; pyv-client-server-ae; ex-simple-election; pyv-toy-consensus-epr; ex-toy-consensus; pyv-client-server-db-ae; pyv-hybrid-reliable-broadcast; pyv-firewall; ex-majorityset-leader-election; pyv-consensus-epr. Table 2’s row is “No. of problems solved (out of 29)”; IC3PO’s entry is 29. Experiment release is referenced by the paper (p. 16); exact release download not inspected because GitHub API rate limiting started. pyv- here corresponds to the mypyv/ group of ivybench.

DistAI complete property manifest

FOL-IC3 pinned properties

FOL artifact properties not shared by the DuoAI table: firewall restricts inbound traffic to previously contacted outsiders; Bosco asserts agreement and validity for nonfaulty nodes; Raft asserts agreement of committed values at each log index. Ring not_dead is a state invariant saying a leader exists or work remains; it is not an eventual leader-election proof. Linked formal assertions are the authority when these plain-English summaries omit details.

Ivy as the interactive verification foundation

Ivy: Safety Verification by Interactive Generalization, Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham, PLDI 2016, pp. 614–630. DOI; code. The repository description says “the human protocol designer and the automated tool interact to expose errors and prove correctness.” Ivy checks inductive invariants using SMT and helps people generalize counterexamples. Inference: an agent can replace part of that interaction, while the checker still decides whether its proposed invariant proves the formal target. The broad Ivy examples directory is an evolving collection, not the fixed 14/27/54-case suites described above.

For the no-lost-keys task, the short literal excerpt is transfer_msg or forall K. exists N. owner(N,K). The full file quantifies the first alternative existentially over node, key, and value: existence of any transfer message makes the stated target true. Inference: an evaluation should preserve this exact target instead of silently replacing it with the stronger per-key no-loss property.

Current mypyvy examples/misc/pd complete directory manifest

This is a repository observation, not a verified match to the POPL 2022 experiment subset. Download: the pd directory. Names containing unsafe are deliberately faulty variants. The suffixes forall, epr, choosable, and dnf distinguish encodings or invariant vocabularies rather than new algorithms.

cache, cache_unsafe, consensus_epr, consensus_forall, consensus_unsafe, consensus_unsafe2, fast_paxos_epr, fast_paxos_forall, fast_paxos_forall_choosable, flexible_paxos_epr, flexible_paxos_forall, flexible_paxos_forall_choosable, lockserv, lockserv_cnf, lockserv_unsafe, paxos_epr, paxos_forall, paxos_forall_choosable, paxos_forall_choosable_unsafe, paxos_forall_choosable_unsafe2, paxos_forall_choosable_unsafe_no_intersection, ring-id, ring, sharded-kv-retransmit, sharded-kv-retransmit_unsafe, sharded-kv, sharded-kv_unsafe, sharded-kv_unsafe2, stoppable_paxos_dnf_epr, stoppable_paxos_dnf_forall, stoppable_paxos_dnf_forall_choosable, stoppable_paxos_epr, stoppable_paxos_forall, stoppable_paxos_forall_choosable, tlb_safety, tlb_safety_prime, vertical_paxos_epr, vertical_paxos_forall, vertical_paxos_forall_choosable.

There are 39 physical .pyv files in that directory at the inspected checkout. Protocol families: cache coherence, consensus, lock service, ring election, sharded key-value transfer (with retransmission variants), TLB safety, and Paxos/flexible/fast/stoppable/vertical Paxos. For precise targets, each linked model marks the assertion using safety; unsafe models intentionally allow violating that target.

P-FOL-IC3: full 30-model experiment recovered

Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion, Jason R. Koenig, Oded Padon, Sharon Shoham, Alex Aiken, TACAS 2022, pp. 338–356. Open publisher PDF, implementation branch, inspected branch snapshot. The paper uses breadth-first lemma search and a restricted formula shape that permits both conjunctions and disjunctions. Section 6.1, printed p. 349: “All our examples are safe transition systems with a known human-written invariant.” Its experimental set has 30 models, not the PLDI 2020 artifact’s 19 files.

Complete Table 1, printed p. 350: lockserv; toy-consensus-forall; ring-id; sharded-kv; ticket; learning-switch; consensus-wo-decide; consensus-forall; cache; paxos-forall; flexible-paxos-forall; stoppable-paxos-forall; fast-paxos-forall; vertical-paxos-forall; firewall; sharded-kv-no-lost-keys; toy-consensus-epr; ring-id-not-dead; consensus-epr; client-server-ae; client-server-db-ae; hybrid-reliable-broadcast; paxos-epr; flexible-paxos-epr; multi-paxos-epr; stoppable-paxos-epr; fast-paxos-epr; vertical-paxos-epr; block-cache-async; bosco-3t-safety.

Properties for lock/leader/consensus/routing/firewall/client-server/sharding cases follow the narrow tables above. Paxos variants target agreement; Multi-Paxos targets agreement per instance; Stoppable Paxos also excludes decisions after a decided stop marker. ring-id-not-dead says a leader, pending message, or unsent identifier still exists; it is an invariant, not eventual election. cache requires a non-invalid, non-modified cached value to equal memory. block-cache-async contains safety obligations relating cache and synchronization states to an abstract storage model. Bosco contains honest-node agreement and validity under its fault/threshold assumptions. These last readings are from the corresponding .pyv safety declarations. Download inputs from mypyvy examples/fol and examples/pd in the branch snapshot; the exact experiment checkout versus current branch still needs confirmation.

Primal-dual Houdini: full fixed 20-task evaluation

Induction Duality: Primal-Dual Search for Invariants, Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, Alex Aiken, POPL/PACMPL 6, 2022, pp. 1–29. DOI, fixed artifact, artifact instructions, code and model snapshot. It couples a candidate-invariant elimination algorithm, Houdini, with a mathematically dual search over states. The Crossref publisher abstract calls it “primal-dual Houdini”. The publisher PDF request returned HTTP 403; the artifact instructions and source snapshot were read instead.

The artifact says its Table 2 uses “20 benchmarks (10 safe and 10 unsafe)”. The complete table-to-file mapping below is transcribed from the authors’ artifact. Unsafe variants deliberately break a protocol while preserving a safety target, so an evaluation should require a counterexample rather than a proof. The source snapshot contains all listed input filenames; its supplied invariant declarations must be distinguished from the safety target.

For exact multi-tool experiment inputs and logs, download the Zenodo VM (induction-duality-popl-2022-artifact.ova, about 5.45 GB). The instructions identify popl-2022-experiments/inputs and record mypyvy commit 5dcbb19, SWISS 348b9c4, IC3PO experiment commit 9d3a54b, and DistAI 0ec9389. This resolves the fixed experiment subset; a changing repository’s larger example inventory remains a different object.

TLA+ invariant inference, LLM proof assistance, and protocol benchmark sets

Research checked 6 October 2026 using live author sites, arXiv PDFs, USENIX PDFs, GitHub repository clones, and Crossref metadata. All principal papers below were read as PDF text. Inference: a useful evaluation separates finding an invariant, proving that supplied invariant inductive for every system size, and proving refinement to a desired external specification. These papers evaluate different stages.

Endive: TLA+ candidates, followed by an unbounded proof

Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+, William Schultz, Ian Dardik, Stavros Tripakis, FMCAD 2022. Paper, code and benchmarks, archived evaluation.

Endive samples candidate lemmas from a user-provided predicate grammar, checks them on finite instances, and greedily selects lemmas that eliminate induction counterexamples. The resulting invariant needs a TLAPS proof for an unbounded protocol. The repository cautions: “This generated inductive invariant is not necessarily a true inductive invariant” (README); its continuation attributes this to probabilistic counterexample sampling. The paper reports “an inductive invariant for 25 of the 29 protocol benchmarks” (§IV-C, p. 6). Its table contains 30 rows: the shared 29-case Ivy suite plus MLDR; two rows have no TLA+ translation, so distinguish the comparison universe from runnable TLA+ cases.

Full FMCAD 2022 comparison suite, Table I p. 5: tla-consensus; tla-tcommit; i4-lock-server; ex-quorum-leader-election; pyv-toy-consensus-forall; tla-simple; ex-lockserv-automaton; tla-simpleregular; pyv-sharded-kv; pyv-lockserv; tla-twophase; i4-learning-switch; ex-simple-decentralized-lock; i4-two-phase-commit; pyv-consensus-wo-decide; pyv-consensus-forall; pyv-learning-switch; i4-chord-ring-maintenance (n/a TLA+); pyv-sharded-kv-no-lost-keys; ex-naive-consensus; pyv-client-server-ae; ex-simple-election; pyv-toy-consensus-epr; ex-toy-consensus; pyv-client-server-db-ae; pyv-hybrid-reliable-broadcast (n/a TLA+); pyv-firewall; ex-majorityset-leader-election; pyv-consensus-epr; mldr.

The following properties are direct readings of the named TLA+ definitions, not assertions of liveness. Download benchmark source. Each row identifies source filenames; prefixes above identify historical tool origins, not separate protocol semantics.

Exact examples: Consensus.tla defines Inv == /\ TypeOK /\ Cardinality(chosen) \leq 1; lockserv.tla defines Mutex == \A x,y \in Node : (holds_lock[x] /\ holds_lock[y]) => (x = y); TwoPhase.tla describes “two RMs have not arrived at conflicting decisions.” These code quotations establish the row interpretations. The live repository also includes Peterson mutual exclusion and Paxos beyond the original evaluated suite; do not silently count them as FMCAD 2022 benchmark rows.

IC3Syn: a direct 2026 LLM invariant search result

Synthesizing Inductive Invariants for Distributed Protocols via IC3 and Large Language Models, Weining Cao, Guangyuan Wu, Yuan Yao, Hengfeng Wei, Taolue Chen, Xiaoxing Ma, arXiv preprint, 23 May 2026. Paper. No publicly downloadable implementation or proof artifact was located in the paper or GitHub repository-name search IC3Syn on 6 October 2026. This limits independent reproduction.

The IC3 controller gives an LLM concrete states to block; the LLM proposes TLA+ clauses; TLC/Apalache validate finite-instance steps; TLAPS subsequently proves the unbounded result. Table 1 p. 9 reports all 29 solved. Section 7.2 p. 11 limits the synthesis loop to finite instances. The unbounded-proof claim must be reported separately from finite discovery: §7.2 says “TLAPS proves that the discovered invariants are inductive for unbounded protocol instances.”

Full 29-case suite, Table 1 p. 9: tla-consensus; tla-tcommit; i4-lock-server; ex-quorum-leader-election; pyv-toy-consensus-forall; tla-simple; ex-lockserv-automaton; tla-simpleregular; pyv-sharded-kv; pyv-lockserv; tla-twophase; i4-learning-switch; ex-simple-decentralized-lock; i4-two-phase-commit; pyv-consensus-wo-decide; pyv-consensus-forall; pyv-learning-switch; pyv-sharded-kv-no-lost-keys; ex-naive-consensus; pyv-client-server-ae; ex-simple-election; pyv-toy-consensus-epr; ex-toy-consensus; pyv-client-server-db-ae; pyv-firewall; ex-majorityset-leader-election; pyv-consensus-epr; mldr; pyv-paxos-epr.

The shared 28 cases are the translated endive suite; the added pyv-paxos-epr comes from IC3PO and was adapted to TLA+ (§6.1). Properties follow the preceding source-property table; added Paxos requires agreement on chosen values. Baseline times and success are the paper authors’ reproductions, not our measurements. MLDR’s row is 4525 seconds and 16 clauses; added Paxos is 1806 seconds and 9 clauses. Table 1 counts clauses excluding TypeOK and including safety clauses. The paper’s Endive rerun solves 24 shared cases, unlike Endive’s original result; §7.1 acknowledges difficulty reproducing the original expert predicate pool.

The end-to-end result still needs careful wording. MLDR proof claim (§7.1 p. 11): over 3,000 proof lines, primarily completed by LLM agents with minimal human intervention; exact quote: “not a single line of proof was directly written by a human.” Its proof advancement used a scaffold and Codex automation; integration into a fully automatic pipeline is ongoing work. Inference: this is strong evidence that invariant discovery plus structured proof decomposition can make protocol verification feasible for agents, but not evidence that vague natural-language requirements were automatically turned into the right specification.

LMGPA: prove supplied invariants rather than discover them

Towards Language Model Guided TLA+ Proof Automation, Yuhao Zhou, Stavros Tripakis, arXiv December 2025/revised February 2026; TACAS 2026 DOI 10.1007/978-3-032-26204-2_32. Paper, tool and full suite, archived artifact.

An LLM decomposes difficult TLAPS obligations into smaller claims; symbolic provers verify them. The given invariant is already part of the input. Quote (§4.2 p. 11): “26 inductiveness proofs of candidate inductive invariants of distributed protocols.” Alongside these are 93 translated mathematical theorems, for 119 total. Its strongest protocol result is 50.0% with DeepSeekV3.2-Exp, versus 38.5% symbolic-only and 0.0% direct generation for that model (Table 1 p. 13). This is a different task from synthesizing a missing invariant.

Full 26 protocol files in benchmarks/distributed_ind_inv: 1_Consensus; 2_TCommit; 3_lockserver; 4_quorum_leader_election; 5_toy_consensus_forall; 6_Simple; 7_lockserv_automaton; 8_SimpleRegular; 9_sharded_kv; 10_lockserv; 11_TwoPhase; 13_simple_decentralized_lock; 14_two_phase_commit; 15_consensus_wo_decide; 16_consensus_forall; 19_sharded_kv_no_lost_keys; 20_naive_consensus; 21_client_server_ae; 22_simple_election; 23_toy_consensus_epr; 24_toy_consensus; 25_client_server_db_ae; 27_firewall; 28_majorityset_leader_election; 29_consensus_epr; 30_MongoLoglessDynamicRaft. Each is a .tla module. Properties are the same named endive properties above. This suite leaves out both learning switches, chord, and hybrid broadcast from the original comparison table.

Scimitar: distinguish the final interactive paper from an older automatic draft

Interactive Safety Verification of Distributed Protocols by Inductive Proof Decomposition, William Schultz, Edward Ashton, Heidi Howard, Stavros Tripakis, NASA Formal Methods 2026. Final author PDF, DOI, Scimitar repository.

The tool gives a user small induction failures tied to a particular lemma and action, and hides irrelevant state variables. Quote (abstract p 1): “an inductive proof graph, which is built incrementally by a human verifier.” It uses bounded TLC/Apalache counterexamples and verifies final invariants with TLAPS (§5 p. 14). The cited artifact https://github.com/will62794/nfm26-artifact was unavailable (GitHub repository not found) when checked; the live Scimitar repo remains downloadable.

Full final paper suite (Table 1 p. 15 and §5 p. 14):

Effort quote (§5.1 p. 17): “approximately 3 human weeks of effort.” This is AsyncRaft invariant development. It is not an automatic 21-hour proof. The older author draft, titled Interpretable Safety Verification of Distributed Protocols by Inductive Proof Decomposition, has an automatic synthesis evaluation for AsyncRaft LogMatching, 33 lemma nodes, 173 grammar predicates, around 21h. Its metadata contains a template conference header and must not be cited as the final NFM 2026 result.

The live Scimitar repository contains many experiments outside the final paper’s five. A machine-extracted full configuration inventory is appended below; file presence is not evidence the problem was solved.

Kondo and Basilisk: prove protocols with richer logic using structure

Inductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline Distributed Protocol Proofs, Tony Nuda Zhang, Travis Hance, Manos Kapritsos, Tej Chajed, Bryan Parno, OSDI 2024. Paper, Kondo download. Kondo generates routine network/history/ownership facts and transfers a user-written synchronous proof to asynchronous execution. The developer still provides protocol-specific invariants and synchronous proof. Full evaluated suite, Table 1 p. 848: Echo Server; Ring Leader Election; Simplified Leader Election; Two-Phase Commit; Paxos; Flexible Paxos; Distributed Lock; ShardedKV; ShardedKV-Batched; Lock Server. Guarantees appear in the Basilisk shared suite below. Human proof-size examples from Table 1: Paxos has 631 specification lines, 20 supplied invariant clauses, 557 synchronous proof lines, and 220 lines of modified asynchronous lemmas. Flexible Paxos has 633/20/554/226 in the same categories; Ring Leader Election has 183/1/56/0. These are artifact sizes, not elapsed person time.

Basilisk: Using Provenance Invariants to Automate Proofs of Undecidable Protocols, Tony Nuda Zhang, Keshav Singh, Tej Chajed, Manos Kapritsos, Bryan Parno, OSDI 2025. Paper, complete artifact, archive. Dafny-based static analysis generates invariants tying values to the protocol steps that created them. Humans prove the resulting invariant implies safety. Section 6.2 p. 11 says humans still write the safety proof. Scope quote (§6.4 p. 12): “Basilisk is designed to prove the safety of crash fault tolerant distributed protocols.” Its next sentence excludes liveness and Byzantine fault tolerance. Generated invariant search does not equal a fully automatic safety proof.

Full evaluated 16-case Basilisk suite and guarantees (Appendix B pp 16-17, download directories under basilisk/):

Verbatim property anchor (Appendix B p. 17): “Each term has at most one leader.” Table 1, p. 11, reports specification/total proof lines of 418/486 for Paxos, 418/483 for Flexible Paxos, and 447/565 for Multi-Paxos. All 16 rows have zero supplied inductive invariant clauses. Paxos-Dynamic, Raft Leader Election, and Multi-Paxos each use two human provenance hints; the remaining cases use zero. Additional monotonicity annotations and ownership labels still needed. The live repo also contains twoPhaseCommitMultiTransaction and twoPhaseCommit_paper-version; these are beyond/different variants of the evaluated sixteen.

Sift: refinement from protocol down to executable systems

Sift: Using Refinement-guided Automation to Verify Complex Distributed Systems, Haojun Ma, Hammad Ahmad, Aman Goel, Eli Goldweber, Jean-Baptiste Jeannin, Manos Kapritsos, Baris Kasikci, USENIX ATC 2022. Paper, all source and executable-system benchmarks. It divides refinement into intermediate layers that IC3PO/Ivy can prove. Users choose layers and provide hints/abstractions; this is related proof automation, not arbitrary invariant discovery from an untouched full system.

Full six-system suite, §7 p. 158/Table 1 p. 159: Leader Election (leader/), Distributed Lock (toy_lock/), Two-Phase Commit (2pc/), Sharded Hash Table (sht/), Raft (raft/), MultiPaxos (multipaxos/). Guarantees: refinement to unique leader, unique lock, consistent commit, abstract key-value map, and consensus/shared-log specifications respectively. Table 1 human effort: under 5 minutes each for Leader Election, Distributed Lock, and Two-Phase Commit; under 30 minutes for SHT; one person-month for Raft; three person-weeks for MultiPaxos. Exact quote (§7.5 p. 160): “complete the proof of Raft in one person month.” It additionally uses earlier manual spec-to-abstract-layer proofs for Raft and MultiPaxos (Table 1 labels those rows manual). Source and generated C++ are accessible via repository README commands.

Adjacent 2026 LLM result that is not a protocol benchmark

CIll: CTI-Guided Invariant Generation via LLMs for Model Checking, Yuheng Su, Tianjun Bu, Qiusong Yang, Yiwei Ci, Enyuan Tian, arXiv 2026. Paper, artifact. It uses induction counterexamples and bounded counterexamples to refine LLM-generated invariants, with IC3 and k-induction. Its full evaluated target list (Table 1 p. 14) is nerv, picorv32, serv, three RISC-V cores, not distributed protocols. Do not classify this as an Ivy/TLA+ protocol success merely because Ivy appears in related work. Inference: its verifier-guided search architecture is relevant, its benchmark population is not a replacement for distributed protocol evaluation.

Gaps and search record

Searched OpenAlex, GitHub repository API, arXiv, author publication lists, and USENIX for LLM+Ivy, LLM+TLA+, LLM+TLAPS, LLM protocol invariants, IC3Syn, Scimitar, Basilisk, Kondo, Sift, and Lemur-related work. Found direct 2026 protocol invariant synthesis in IC3Syn and supplied-invariant TLAPS proof generation in LMGPA. No independently downloadable IC3Syn proof/code artifact was located; cited NFM 2026 archive repository returned repository-not-found. No verified claim of liveness for the above invariant suites was located. Bibliography mentions Lemur, but its C-program verification population should be distinguished from protocol inference. Lemur and Veil appear in the additional workflows section.

Full live Scimitar configuration inventory (not an evaluated success list)

Repository snapshot checked 6 October 2026: f1b902dc0801cf435cb9dd6e6be495d5ed121787. Download all from benchmarks. Each row pairs exact configuration basename with the named target predicate; property wording must be read from its .tla definition, especially generic names such as Inv and Correctness. Deliberately broken grammars and protocols remain listed so the manifest is complete.

Repository manifests checked at these commits: endive 8b6f2abd1988eeb308f965813635e9871f253e2d; LMGPA c27bf4f657c10254b8df8c66ca37f1cdbbf66f1e; Basilisk 394ce1412df9c6e59efe6a00207f0f468400aa61; Sift a76729730c6698f5bd03d73f4d966048b29c9f92; Kondo 1d6c43e475cadfdf7a10bfb5137cd777ccf2138f.

Decidability, parameterized verification, and refinement

These techniques solve different parts of automation. EPR makes checking a supplied proof decidable. ByMC proves specially structured protocols for arbitrary participant counts. Civl lets a person replace complicated concurrent executions with simpler programs, and checks those replacements. My inference: evaluation should separate finding an invariant, preparing a representation in which checking works, and finding a refinement/sequentialization.

Paxos Made EPR

Paxos Made EPR: Decidable Reasoning about Distributed Protocols, Oded Padon, Giuliano Losa, Mooly Sagiv, Sharon Shoham, OOPSLA/PACMPL 1 article 108, 2017. Paper, DOI. Read PDF including sections 4–8. Abstract quote: “The steps of the transformations are also mechanically checked, ensuring the soundness of the method.” Section 8 quote: “Z3 diverged in this case for all”. The latter refers to their attempted unbounded checks of original first-order models; it does not claim Z3 fails for every possible encoding.

People supply models, invariants, and systematic transformations; the checker verifies proof obligations in effectively propositional logic (EPR). EPR is a first-order fragment whose satisfiability is decidable. This is proof checking and representation design, not autonomous invariant discovery. Full case list: Paxos, Multi-Paxos, Vertical Paxos, Fast Paxos, Flexible Paxos, Stoppable Paxos; safety/agreement (no two different chosen values, per instance where applicable). Section 8 discusses original first-order versus transformed EPR encodings. Download location verified for related reusable encodings: ivybench, whose README explicitly cites this paper as its Paxos source. The paper’s §8 footnote 7 points to http://www.cs.tau.ac.il/~odedp/paxos-made-epr.html; the HTTPS version now returns 404. SWISS supplies related six-variant input models, but a verified copy of the original complete artifact remains missing.

ByMC and threshold automata

Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker, Igor Konnov, Marijana Lazić, Ilina Stoilkovska, Josef Widder, LMCS 19(1):5, 2023. Paper/PDF, publisher, tool, all benchmark sources. Read sections 3–7 and Tables 4/6. Section 6.1 quote: “All benchmarks discussed in this paper” are available in the linked repository. Section 7.2 quote: “we use ByMC to verify its one-round safety in the parameterized case”. This limits the Tendermint claim to one round, not full multi-round consensus.

The representation counts messages and participants, and guards actions by threshold tests. It supports arbitrary participant/fault counts under resilience conditions such as n>3t. Safety and liveness use different procedures; randomized termination has a specific round-rigid adversary restriction. Models and assumptions remain human inputs.

Table 4’s complete asynchronous/randomized algorithm list:

Table 4 distinguishes six tool generations; these are the best supported properties across generations, not success by every generation. isola18 directory gives Promela/threshold-automaton versions; random19 gives randomized variants. Concrete source filename cc.ta is the conditional-consensus model; keep paper abbreviation CBC and artifact label distinct.

Table 6’s complete synchronous set follows. The property readings below come from properties declarations in the syncTA algorithm modules: consensus agreement means correct nodes do not finish with conflicting values; validity prevents a decision contradicting unanimous correct inputs. Set-agreement models instead limit the number of distinct results to k. Broadcast unforgeability prevents acceptance without an initial sender witness. The per-file resilience/fault assumptions are essential.

Successful checks combine a diameter bound with bounded model checking. The synchronous checker is a separate prototype, not integrated into ByMC (§6.4). Download all synchronous encodings from syncTA; algorithms, boundable, and counterexamples distinguish ordinary inputs, cases with theoretical bounds, and intentionally erroneous encodings. The live repository also includes corrected or additional encodings; the table above records the survey’s evaluated set. lmcs20 adds Tendermint one-round safety as tendermint-1round-safety.ta and Tendermint_1round_safety.tla.

Civl and inductive sequentialization

Official Civl site identifies two design principles: quote “Layered Refinement” and “Structured Programs”. It states “Civl decomposes proof checking into modular verification conditions that are automatically verified by a theorem prover/SMT solver.” It links distributed samples Paxos, 2PC, Chang–Roberts. This is a program/refinement benchmark complement to transition-system invariant suites.

Inductive Sequentialization of Asynchronous Programs, Bernhard Kragl, Constantin Enea, Thomas A. Henzinger, Suha Orhun Mutluergil, Shaz Qadeer, PLDI 2020. [PDF](https://civl-verifier.github.io/papers/pldi 2020.pdf), DOI, source suite. Read sections1,5. Quote section 1: “The induction argument in IS is based on a user-provided”. Quote section 5.3: “We prove that there can be at most one leader.” The latter is Chang–Roberts’s property. User supplies a simpler interleaving and commutativity evidence; checked induction makes this reduction sound.

Complete Table 1 (LOC columns include boilerplate in Civl/Boogie, not application source):

Property descriptions above follow section 5; no liveness result is asserted. Table 1 counts IS applications respectively 2,1,1,4,2,4,1. No human-hour measurement found.

Layered Concurrent Programs, Bernhard Kragl, Shaz Qadeer, CAV 2018. PDF, DOI. Section 6 quote: “around fifty smaller programs (including a ticket lock and a lock-free stack)”. Large cases: concurrent garbage collector and data-race detector. This establishes the layered program model and mechanically checked relationships between layers; the paper is not an automatic invariant synthesizer.

Refinement for Structured Concurrent Programs, Bernhard Kragl, Shaz Qadeer, Thomas A. Henzinger, CAV 2020. [PDF](https://civl-verifier.github.io/papers/cav 2020.pdf). Section 6 quote: “The open-source Civl verifier is a stable tool”. It supports proof decomposition using program structure, yield invariants and permissions. No fixed complete protocol benchmark list identified in this paper.

The Civl Verifier, Bernhard Kragl, Shaz Qadeer, FMCAD 2021. [PDF](https://civl-verifier.github.io/papers/fmcad 2021.pdf). Read section 6. Quote: “a Paxos implementation”. Gives tool overview and retained case studies, including garbage collection, Paxos and locks. Exact full test suite is a changing repository, not a fixed protocol benchmark; use a pinned commit when evaluating.

Reduction for Structured Concurrent Programs, Namratha Gangamreddypalli, Constantin Enea, Shaz Qadeer, ESOP 2026. [PDF](https://civl-verifier.github.io/papers/esop 2026.pdf), sources. Read section 8/Fig 12. Quote abstract: “these two foundational strategies can be composed arbitrarily”. Quote section 8: “approximately 50 further examples”. Full paper case set: Snapshot (linearizable snapshot;119 total LOC,82 implementation+spec,0.4s), ABD (atomic register/linearizability;389,206,1.4s), FLASH coherence (cache coherence;608,401,5s), 2PC (consistent transaction decision;146,111,1.8s). The paper combines sequential reduction of parallel calls with reduction inside procedures. My inference: these can test whether agents discover useful proof structure, beyond finding conjuncts.

Cutoff and bounded instantiation leads

Cutoff Bounds for Consensus Algorithms, Ognjen Marić, Christoph Sprenger, David Basin, CAV 2017, pp. 217–237. Open PDF, DOI. Read §§2, 5, 6 and Table 2, p. 233. ConsL describes round-based algorithms in a benign asynchronous communication abstraction; a translation produces Promela and LTL for Spin. Its bounds justify checking a small process count, rather than merely assuming small tests suffice. The abstract reports “bounds of 5 or 7”. Table 2 checks agreement and termination for every row. Section 2.1 defines termination as “Every process eventually decides on a value.” Its abstraction lets failed processes keep receiving/processing but suppresses their sent messages, so this progress claim must retain its communication assumptions.

The paper’s tool/model download pointer is http://www.infsec.ethz.ch/research/software/consl-verifier; the attempted modern HTTPS page returned 404. Gap: the original generated model download was not recovered. This termination check should not be relabeled as a proof of Ben-Or’s probability-one termination under arbitrary adversaries.

Bounded Quantifier Instantiation for Checking Inductive Invariants, Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, Sharon Shoham, TACAS 2017 pp 76–95. DOI. Metadata confirmed in EPR paper references. EPR paper section 9 describes bounding quantifier instantiation as an alternative to enforce decidable proof checking. The full journal version is LMCS 15(3):18, 2019 PDF. Read section 7.3/Table 1. Quote: “Bound 1 successfully proves the invariant inductive in all correct examples”. This bounds quantifier instantiation depth, not participant count. Table 1 complete rows: Client-server (response has matching request), List reverse (next edges reversed), Learning switch (each routing node has successor), Hole-punching firewall with ghost (external peer previously contacted internally), Hole-punching firewall ∃ time (same), Trusted chain correct, Leader-election ring correct, Trusted chain incorrect, Leader-election ring incorrect. Correct ring case checks an invariant used towards termination, not a complete liveness proof. Trusted-chain invariant concerns all nodes eventually marked trusted after pending messages disappear; the checked safety formulation requires all nodes trusted when no messages remain, plus strengthened invariants (section 6.2). The two incorrect rows test partial counterexamples and solver termination. Conference2017 Table 1 lacks the two trusted-chain rows; therefore it has 7 rows. Full code pointer in the journal bibliography is http://www.cs.tau.ac.il/research/yotam.feldman/papers/tacas17/ but currently redirects to a missing GitHub Page; original named Ivy files are provided in figure captions (client_server_ae.ivy, client_server_db_ae.ivy, ring_leader_termination.ivy). Download artifact availability remains a gap.

Search gaps

Web search tool returns HTTP404; DBLP gives a bot challenge; Semantic Scholar429; OpenAlex’s shared-IP free daily budget exhausted. Primary GitHub, arXiv PDFs and Civl site work. Unresolved: complete Message Chains artifact (the names and properties are recovered below), Bakery open PDF/artifact, original six-variant EPR artifact, historical bounded-horizon artifact URL, CAV 2017 cutoff numerical bounds/protocol list, cutoff 2022 source download. QSM-Cutoff is assessed in the next section. These are explicit gaps, not evidence that the work does not exist.

Cutoff automation with seven concrete protocols

Automating and Mechanizing Cutoff-based Verification of Distributed Protocols, Shreesha G. Bhat, Kartik Nagar, arXiv 2022 (venue unconfirmed). PDF. Read sections3–6/Table 2. Section 6 quote: “We use Z3 [12] as our backend SMT solver.” Quote section 6.1: “we cannot have two nodes where one decides to commit and the other aborts”. The latter is the2PC property. The approach proves that a small modified system simulates arbitrary instances, then verifies that small system; it synthesizes mappings and simulation obligations using static analysis. Three cases need human changes. No source repository found in paper.

Complete Table 2:

Important scope: the measured time is proving the cutoff/synthesizing simulation, not the entire end-to-end cost of model checking a finite instance. Basic store needs a precondition about prior transfers, distributed lock server needs changed stale-message behavior and a maximum-epoch mapping, and 2PC needs a third failure-simulating node. My inference: good agent evaluation should require reporting these changes and why they preserve the intended property.

Towards an Automatic Proof of the Bakery Algorithm, Aman Goel, Stephan Merz, Karem A. Sakallah, FORTE 2023 pp 21–28. DOI, author publications. Title and metadata confirmed with Crossref, author site, and the publisher abstract. The abstract says “automatically compute inductive invariants for two versions of the algorithm” using IC3PO, starting from TLA+ specifications. The target is mutual exclusion for shared-variable processes. Open PDF, names of the two exact versions, and full proof artifacts were not retrieved; no liveness claim is inferred.

Message Chains / UPVerifier: full 19-case paper set recovered

Message Chains for Distributed System Verification, Federico Mora, Ankush Desai, Elizabeth Polgreen, Sanjit A. Seshia, OOPSLA/PACMPL 7 article 300, 2023, pp. 2224–2250. Author’s open PDF, paper page, UPVerifier code, inspected revision. Read §6 and Table 1, pp. 300:19–24.

A message chain records the messages that caused a later message. Keeping that history can express causal facts directly instead of requiring people to invent ghost state for each proof. This is automatic bookkeeping for checking supplied proofs, plus specification mining from examples; it is not a general automatic invariant-discovery result. The compiler handles a P-like language. The repository README describes “Unbounded Verification of P(-like) Programs.”

Complete evaluated set: Table 1 contains the following 16 reused models. Their safety properties correspond to the shared mypyvy set, with translations detailed in §6.1. They are all checked for arbitrary system size in the model, not full production implementations.

The additional three cases are:

The paper’s model/proof sizes are literal data from §6.4. Verification times are under 2 seconds for GlobalClock and about 12 minutes for 2PC-MVCC. A property anchor in §6.4.2, p. 300:23, is “we only read the latest committed transactions”.

Download limitation: the current linked repository has examples/chain_replication.smp, client_server_ae.smp, client_server_db_ae.smp, firewall.smp, fuzz.smp, ring_id.smp, ring_id_not_dead.smp, and submit.smp, with execution data. It does not ship a full current manifest of all 19 evaluated models. The original 16 mypyvy sources are downloadable from the PLDI 2020 branch, but those are not identical UPVerifier translations. No complete fixed UPVerifier benchmark archive was located, including the industrial cases. The paper nevertheless establishes their names and guarantees.

QSM-Cutoff: a full 19-model 2025 set

QSM-Cutoff: Systematic Derivation of Quantified Cutoff Formulas for Distributed Protocols, Yun-Rong Luo, Aman Goel, Karem Sakallah, CAV 2025, pp. 263–286. Open PDF, tool, scripts and CAV logs, inputs. The PDF and repository README were read.

The method enumerates reachable finite states while exploiting symmetry, minimizes their logical description, and increases domain sizes until its saturation test succeeds. Section 7, pp. 278–280, evaluates the complete 19-case list below. The listed domain sizes are the paper’s Table 4 data, not generally applicable bounds for other encodings. The caption defines #A as strengthening assertions needed to prove safety; the paper reports safety checks using its resulting formulas. Scope distinction: identifying the strongest reachable-state characterization for every size remains a conjecture. Section 9, p. 282, calls for “a formal proof showing that the cutoff formula Rc is, in fact, a reachability invariant”. This does not erase the separately checked inductive safety proofs.

Properties are interpretations of the shared Ivy models listed elsewhere; use this fork’s exact files to reproduce the results. Ordered ballot/epoch/ticket protocols such as Paxos and Bakery are future extensions in §9, not members of this evaluated set.

Additional proof and inference workflows

Veil: proofs in Lean with automatic first-order checks

Veil: A Framework for Automated and Interactive Verification of Transition Systems, George Pîrlea, Vladimir Gladshtein, Elad Kinsbruner, Qiyuan Zhao, Ilya Sergey, CAV 2025. Paper, repository, fixed CAV artifact, source snapshot.

Veil turns a protocol and supplied invariants into proof obligations, tries SMT solvers, and permits interactive Lean proofs for the remainder. This paper evaluates checking supplied invariants, rather than discovering them. Its abstract, p. 1, says: “Veil provides an interactive verification mode”.

The evaluation contains 16 cases, including alternate encodings of the same protocol. Section 4.1, p. 8: “1704 non-empty, non-comment lines of Lean code”; “85 actions and 185 invariants”. The paper gives 100 lines per file on average These are aggregate specification/proof figures, not implementation size or invariant-discovery effort.

The complete Figure 5 list follows. Properties are my plain-English readings of the archived safety or named invariant statements in Benchmarks/Veil. This fixed snapshot matters: the current repository has different examples. All guarantees below concern safety.

RabiaMore.lean and SCPTheory.lean are support proofs, not additional Figure 5 cases. Download the archived source zip from the Zenodo record or GitHub commit. Benchmarks/Ivy supplies the corresponding Ivy comparison files.

2026 LLM case study: Ilya Sergey, “Verifying Distributed Protocols in Veil,” February 9, 2026, author’s account. The section reports that “most of the auxiliary invariants” for FloodSet were obtained with Claude Code. The prompt asks the agent to make #check_invariants succeed using verifier counterexamples. This is one documented case, not a comparative benchmark. Its guarantees are agreement and validity: every decided value originated at a node. Source.

The same account’s concluding remarks says the generated protocol definitions were “missing crucial parts, making them vacuously correct but also useless.” Inference: successful invariant discovery is insufficient evidence of faithful specification synthesis; evaluate those tasks separately.

DissProve: start at a forbidden outcome and work backward

DissProve: Automated Verification of Asynchronous Distributed Protocols with Affine Communication, Christian Fontenot, Gowtham Kaki, Bor-Yuh Evan Chang, arXiv 2026, paper. Downloaded and read the paper, including §6/Table 1, pp. 22–23. The tool takes P actor code and a forbidden state, then tries to show that no execution reaches it. “Affine” here restricts communication histories to bounded communication rounds, while allowing unbounded actors and history length; this is a restriction of the method, not a claim about every protocol.

Section 6, p. 22: “No additional user-provided specifications or invariants are needed to verify these properties”. Table 1’s complete seven-case evaluation is below; source sizes are quoted table entries, in lines of P code. The table describes consensus and mutual exclusion checks. The paragraph below it assigns consensus to One-Shot, Two-Phase Commit, and Atomic Broadcast, and mutual exclusion to the other cases.

The checked paper has no artifact URL. GitHub repository search for DissProve returned zero repositories during this review. Gap: cannot supply a verified download location for its benchmark programs; the paper itself gives the full evaluation list. These are actor implementations in P, not interchangeable with the Ivy/TLA+ encodings bearing the same names.

Lemur: a useful architecture, with no protocol benchmark

Lemur: Integrating Large Language Models in Automated Program Verification, Haoze Wu, Clark Barrett, Nina Narodytska, ICLR 2024; first arXiv version 2023. Paper, code and data. It uses an LLM to propose intermediate proof goals and a conventional verifier to establish them or provide feedback. Section 5.2, p. 8: “The benchmark set contains 133 benchmarks”, each pairing a C program with an assertion. Section 5.3 tests 47 selected SV-COMP C programs. These are sequential program benchmarks, so there is no distributed protocol list to report for Lemur. Inference: its proposal/check/feedback architecture transfers to protocol invariants; its published scores do not measure that transfer.

Evaluation recommendations and remaining gaps

My recommendations: use several tasks, because each tests a different failure mode.

1. Supply a fixed protocol and safety target, hide auxiliary invariants, and require an unbounded inductive proof. The shared Ivy/mypyvy sets provide comparable small cases. Report supplied grammars, templates, ghost predicates, abstraction steps, timeouts, solver versions, and human edits.
2. Use the primal-dual artifact’s unsafe variants alongside safe tasks. A useful agent must return a reproducible violation when the protocol is wrong. Add specification mutations and useful-state reachability checks to detect trivial or overly restrictive specifications.
3. Give a supplied invariant but omit its proof. LMGPA measures this distinct task; compare with symbolic-only proof checking, then measure the extra benefit from agent decomposition.
4. Add richer P/Dafny/Lean cases and refinement tasks from Message Chains, Basilisk, Kondo, Sift, Civl, and Veil. Count protocol-specific proof hints and abstractions as input, rather than calling every solver invocation an automatic proof.
5. Evaluate liveness separately, preserving fairness, fault, threshold, timing, and adversary assumptions. ByMC provides relevant progress tasks. Agreement or mutual exclusion alone does not establish termination, availability, or eventual election.

Remaining gaps: complete fixed UPVerifier translations/industrial models; downloadable IC3Syn proofs/code; cited Scimitar NFM 2026 archive; DissProve and cutoff2022 source archives; original six-variant EPR artifact; historical bounded-horizon archive; CAV 2017 cutoff paper’s full benchmark list and bounds; open Bakery paper and its two exact model versions; open I4 and primal-dual paper PDFs. P-FOL-IC3’s branch and paper list were found, but the exact experiment commit still needs confirmation. These are gaps in this review, not claims that artifacts never existed. Human effort is reported only where a source states it; file size alone is not effort.

Intake: 35 distinct papers found, counting the older Scimitar draft separately from its final paper; 24 new PDFs saved by this research team. CIll is an explicitly adjacent hardware paper. The final benchmark lists, rather than a sum of overlapping protocol names, are the unit of coverage. PDFs reside in one directory per paper under /hdd1/sichanghe/paper_collection; title/author/venue/year labels identify them. The requested note is this file.

Repository source links with file manifests use inspected or retrieved revisions. Versioned paper artifacts are preferred for experiment reproduction. Additional repository pins:

• VeriGu/DistAI: 3c2b90122585cf1e785e7e31fb64ccfc4982655f
• will62794/DistAI: 3c2b90122585cf1e785e7e31fb64ccfc4982655f
• VeriGu/DuoAI: ecd37c418ef56202ca332d5bca113e8e7c8c8fac
• aman-goel/ivybench: d2c9298fdd099001c71a34bc2e118db6f07d8404
• secure-foundations/SWISS: 348b9c4f9b0b2f124b50c8f420d071f4bc0789b3
• GLaDOS-Michigan/I4: 0c53ceb865487c5fda3e91fb9e379baf9840b2de
• wilcoxjay/mypyvy: cd80557ae11f5958c7c81dbecf3b24f7a3b16c1f
• will62794/endive: 8b6f2abd1988eeb308f965813635e9871f253e2d
• YUH-Z/lmgpa: c27bf4f657c10254b8df8c66ca37f1cdbbf66f1e
• GLaDOS-Michigan/Basilisk: 394ce1412df9c6e59efe6a00207f0f468400aa61
• GLaDOS-Michigan/Sift: a76729730c6698f5bd03d73f4d966048b29c9f92
• GLaDOS-Michigan/Kondo: 1d6c43e475cadfdf7a10bfb5137cd777ccf2138f
• will62794/scimitar: f1b902dc0801cf435cb9dd6e6be495d5ed121787
• istoilkovska/syncTA: 9224ef50d5ada4782d0a1d5723531ebe43149584
• QSM-Cutoff/ivybench: 34dfddd61214805b64bb9a29ab7f8a0e2d3d1bb0
• konnov/fault-tolerant-benchmarks: c9e8de463e0a6bc378d8f05270ffc7db043e79e6
• boogie-org/boogie: fcecf73a49d11ad3ab16729abd03169e5ecfd938

Last edited: 2026-10-12