🤖 database, liveness cases by how strong the evidence is

(authored by agents unless marked 🧑)

291 cases whose guarantee says something eventually happens. Agents sorted them from the text of each case record, not from the papers; a wrong label is possible. Full records are in cases.jsonl under the case id.

running code, proof accepted by a proof checker

63 cases.

Anvil FluentBit controller
- guarantee: Anvil’s FluentBit controller is proved with Verus to eventually reach and keep a fixed desired state, with Rust steps checked against the model, assuming the desired state stabilizes, faults stop and actions are fair.
- assumes: desired state stabilizes; disruptive faults eventually stop; fair actions; modeled external API behavior
- size or effort: Table 1 original Exec/Proof cells: 1208/8395; ~2.5 person-months each
- tool: Verus temporal-model proof + Rust-step/model-step conformance; written by: human
- case B:systems:7; source record anvil-2024
Anvil Kubernetes ReplicaSet, Deployment, StatefulSet and RabbitMQ controllers
- guarantee: Anvil’s Kubernetes controllers (ReplicaSet, Deployment, StatefulSet, RabbitMQ) are verified with Verus to eventually reach the desired state and stay stable despite failures and network issues.
- assumes: Controller-specific rely, guarantee and liveness-dependency conditions; SMT proof expertise
- size or effort: Three built-in and one custom controller listed; no run reproduced
- tool: Verus and Verus-TLA; Welder compositional rules; written by: human
- case C:codex_grey:11; source record anvil-2024
Anvil RabbitMQ controller
- guarantee: Verus proves that the Anvil RabbitMQ controller eventually reaches and keeps a fixed desired state, with the Rust code checked against the model, assuming the desired state stabilizes and disruptive faults eventually stop.
- assumes: desired state stabilizes; disruptive faults eventually stop; fair actions; modeled external API behavior
- size or effort: Table 1 original Exec/Proof cells: 1598/7228; ~2.5 person-months each
- tool: Verus temporal-model proof + Rust-step/model-step conformance; written by: human
- case B:systems:6; source record anvil-2024
Anvil ZooKeeper controller
- guarantee: Anvil ZooKeeper controller: fixed desired state eventually reached and retained.
- assumes: desired state stabilizes; disruptive faults eventually stop; fair actions; modeled external API behavior
- size or effort: Table 1 original Exec/Proof cells: 1134/8352; ~2.5 person-months each
- tool: Verus temporal-model proof + Rust-step/model-step conformance; written by: human
- case B:systems:5; source record anvil-2024
CLH lock (C)
- guarantee: VeriFast with ghost signals verified a CLH lock in C: acquiring terminates provided holders eventually release, using 343 annotation lines for 49 lines of code.
- assumes: Fair scheduling; every acquire creates a release obligation
- size or effort: 343 annotation lines for 49 lines of code (700%), 0.1 s
- tool: ghost signals in VeriFast; written by: human
- case C:r6:46; Ghost signals thesis, Sec 3.4 and 3.5
CRDT implementation (replicated)
- guarantee: A Coq proof in Trillium/Aneris shows a replicated CRDT implementation is correct and strongly eventually consistent, assuming fair inter-replica messages.
- assumes: fairness of inter-replica messages
- size or effort: unknown (appendix)
- tool: Coq, Trillium/Aneris; written by: human
- case A:180; source record trillium-2024
Deployment controller, including rolling update
- guarantee: Deployment controller, including rolling update: eventual stable reconciliation with ReplicaSet dependency, a conditional liveness guarantee (the row says fairness, timing and fault premises apply).
- assumes: Desired-state description eventually stabilizes; weak fairness on model actions; message drops/controller crashes eventually cease; PodMonkey disturbances eventually cease. Welder §5 PDFp11: faults eventually stop (including PodMonkey as specified below). Additional retry-on-conflict fairness: each retry loop terminates, either succeeding or returning a non-version-conflict error; §4.2 PDFp9: “RoC loop terminates”. Always-preserved request-centric rely restrictions on other controllers, with own guarantee satisfying compatible controllers; no finite delivery/computation bound required. External liveness dependency: ReplicaSet ESR (§3.3 PDFp7); §3.3 states DS equals ReplicaSet ESR. Rolling update uses Iter-ESR rather than assuming every intermediate lower-layer desired state remains fixed (§4.1). Gap: pinned per-request rely/guarantee predicates and retry fairness connection to Kubernetes execution unresolved
- tool: liveness; written by: human
- case B:liveness:6; source record welder-2026
Four-controller control plane
- guarantee: Four-controller control plane: compatible CORE guarantees compose, a conditional liveness guarantee (the row says fairness, timing and fault premises apply).
- assumes: Desired-state description eventually stabilizes; weak fairness on model actions; message drops/controller crashes eventually cease; PodMonkey disturbances eventually cease. Welder §5 PDFp11: faults eventually stop (including PodMonkey as specified below). Additional retry-on-conflict fairness: each retry loop terminates, either succeeding or returning a non-version-conflict error; §4.2 PDFp9: “RoC loop terminates”. Always-preserved request-centric rely restrictions on other controllers, with own guarantee satisfying compatible controllers; no finite delivery/computation bound required. Compose only compatible controller groups; dependency resolution requires lower-layer ESR implies upper-layer Depend (§4.4 PDFp11). Deployment/ReplicaSet and RabbitMQ/StatefulSet dependencies are resolved within their pairs, then independent pairs composed (§6). StatefulSet naming restrictions hold throughout execution. Scope: demonstrated acyclic dependencies, not arbitrary circular progress dependencies (§8). Gap: concrete pinned compatibility/dependency formulas and deployment fairness validation unresolved
- tool: liveness; written by: human
- case B:liveness:10; source record welder-2026
IronKV sharded store
- guarantee: IronKV sharded store: functional correctness; reliable-transmission packets eventually arrive under fair retransmission, a conditional liveness guarantee (the row says fairness, timing and fault premises apply).
- assumes: Each host main loop executes infinitely often; every packet sent infinitely often is eventually delivered. IronFleet §2.5 PDFp3: “each host’s main loop executes infinitely often”; §5.2 PDFp10: “any packet sent infinitely often is eventually delivered”. Guarantee concerns the reliable-transmission component, not every store request. Trusted packet integrity, I/O, Dafny/compiler/runtime/OS/hardware (§2.5). Gap: pinned implementation theorem and environmental validation unresolved
- tool: liveness; written by: human
- case B:liveness:2; source record ironfleet-2015
IronKV transmission
- guarantee: Dafny proves the IronKV implementation is a correct sharded store and that repeated transmission eventually delivers each message, assuming fair networking and hosts whose main loops run infinitely often.
- assumes: fair networking; host main loops execute infinitely often
- tool: Dafny implementation proof; written by: human
- case B:systems:2; source record ironfleet-2015
IronRSL
- guarantee: IronRSL: replicated service behaves as specified; a repeatedly submitted request eventually receives a reply.
- assumes: liveness: live quorum, eventual bounded-time networking, minimum loop frequency, sufficient memory; safety: message integrity
- tool: Dafny implementation proof; state-machine refinement; temporal proof; written by: human
- case B:systems:1; source record ironfleet-2015
IronRSL (IronFleet)
- guarantee: IronFleet proves in Dafny that if the network is eventually synchronous for a live quorum of replicas, a client that keeps submitting a request to IronRSL eventually gets a reply.
- assumes: From the artifact repo: NoZenoBehavior; ClockAmbiguityLimitedForHosts; LiveQuorum; HostExecutesPeriodically (period asp.host_period); PersistentClientSendsRequestPeriodically; NetworkSynchronousForHosts (latency_bound); NetworkDeliveryRateBoundedForHosts. Paper: link Sure; server PQ-Alw
- size or effort: proof as stated by authors: Formal (Dafny) ; paper’s verdict: ‘Weak from PQ-Alw (Cor 5.1)’: assumption stronger than needed
- tool: Dafny (IronFleet); written by: human
- case A:300; source record what-s-live-2021
IronRSL Paxos-based replicated state machine
- guarantee: IronRSL, a Paxos-based replicated state machine, is stated to have an implementation that obeys a concise safety specification and stated liveness requirements, verified with IronFleet’s Dafny framework.
- assumes: IronFleet TLA-style state-machine refinement plus implementation-level Hoare reasoning; repository README does not restate all assumptions
- size or effort: Repository release; no run reproduced in this pass
- tool: IronFleet Dafny verification; written by: human
- case C:codex_grey:9; source record ironfleet-repository
IronSHT / IronKV lease-based sharded key-value store
- guarantee: IronSHT/IronKV, a lease-based sharded key-value store, is stated to obey a concise safety specification and liveness requirements in IronFleet, and a Verus port verifies the host program without the distributed refinement layer.
- assumes: The Verus port omits the distributed TLA state-machine-to-high-level-spec refinement layer
- size or effort: Repository README; no run reproduced
- tool: IronFleet Dafny verification; Verus port verifies host program; written by: human
- case C:codex_grey:10; source record verified-ironkv
Kubernetes FluentBit controller (Anvil)
- guarantee: Anvil with Verus proves eventually stable reconciliation for the Kubernetes FluentBit controller, for all features of the reference controller.
- assumes: Same as the other controllers
- size or effort: ~2 person-weeks; average feature change under a day and 47 lines (19 proof lines); largest change 403 lines (211 proof)
- tool: Verus + Anvil; written by: human
- case A:348; Sun, PhD dissertation 2025, Sec. 4.4, 4.5.1
Kubernetes RabbitMQ controller (Anvil)
- guarantee: Verus with Anvil proves that the Kubernetes RabbitMQ controller eventually reaches a stable reconciliation for 9 state objects, and that the replica count in the data store never decreases.
- assumes: Same as ZooKeeper controller; the garbage collector eventually stops racing with the controller
- size or effort: ~2 person-weeks for ESR using the existing strategy; executable 1,598 lines, proof 7,228 lines (ESR 5,211, safety 358), trusted 548 lines; found a GC-race safety bug and a duplicate-service-name liveness bug
- tool: Verus + Anvil; written by: human
- case A:347; Sun, PhD dissertation 2025, Sec. 4.4.2, Table 4.1
Kubernetes ZooKeeper controller (Anvil)
- guarantee: Kubernetes ZooKeeper controller (Anvil, Verus): if the desired state stops changing, the cluster eventually matches it and stays matched; 1,134 executable and 8,352 proof lines.
- assumes: Trusted Kubernetes environment model; controller written as an atomic-step state machine; desired state eventually stops changing; no conflicting controllers; faults eventually stop; fairness of the API server and garbage collector
- size or effort: ~2 person-months (including developing the proof strategy); executable 1,134 lines, proof 8,352 lines (ESR 7,245), trusted 950 lines; two liveness bugs found
- tool: Verus + Anvil TLA embedding; written by: human
- case A:346; Sun, PhD dissertation 2025, Sec. 4.4.1, 4.5.1, Table 4.1
Lion async runtime (executor, reactor, timer wheel)
- guarantee: Verus proves that in the Lion async runtime a spawned task is driven to completion and a registered timer eventually wakes, under a monotonic clock and bounded-delay wake sources.
- assumes: monotonic clock; registered wake sources eventually fire within bounded polls; tasks return Ready within bounded polls; tasks keep resources registered; FIFO injection
- size or effort: 3393 exec lines vs 39648 spec/proof lines (Verus count); 126 external_body trusted items
- tool: Verus (ghost event logs, no temporal operators); written by: unclear
- case A:29; source record lion-2026
Lock-free concurrent stack with helping
- guarantee: Iris/Coq with call permissions proves every operation of a lock-free stack with helping terminates, with no scheduler assumption.
- assumes: non-blocking so no scheduler assumption
- size or effort: unknown
- tool: Iris/Coq with call permissions; written by: human
- case A:185; source record modular-termination-verification-with-2022
Memcached (simplified) and small concurrent examples
- guarantee: Prusti proves in Rust that a simplified Memcached and small concurrent examples refine an abstract guarded transition system, with safety and liveness stated as LTL in ghost code.
- assumes: not extracted
- size or effort: per-case implementation/model/proof line counts in Fig 3 of the paper
- tool: Prusti (Rust); written by: human
- case A:215; source record a-refinement-methodology-for-2025
MPI programs (three PDE solvers)
- guarantee: Three MPI PDE solvers written with DafnyMPI are verified deadlock free and terminating, and equal to the sequential implementation, given a declared communication topology.
- assumes: communication topology declared up front; preconditions on MPI_ISEND, MPI_WAIT
- size or effort: not extracted
- tool: Dafny (DafnyMPI library); written by: human
- case A:46; source record dafnympi-2025
OpLib Add-Wins Set
- guarantee: OpLib proves in Aneris/Coq that an Add-Wins Set replica state equals the data-type interpretation of its delivered causal operations, and replicas with the same delivered operations converge.
- assumes: causal broadcast library contract; serializable values; operations satisfy datatype-specific commutation conditions
- tool: Aneris/Coq modular implementation proof; written by: human
- case B:systems:32; source record op-based-crdts-2022
OpLib Last-Writer-Wins Register
- guarantee: OpLib proves in Aneris/Coq that a Last-Writer-Wins Register replica state equals the data-type interpretation of its delivered causal operations, and replicas with the same delivered operations converge.
- assumes: causal broadcast library contract; serializable values; operations satisfy datatype-specific commutation conditions
- tool: Aneris/Coq modular implementation proof; written by: human
- case B:systems:36; source record op-based-crdts-2022
PBFT agreement on a single log entry (Shipwright), executable Go from Dafny
- guarantee: Shipwright proves in Dafny (with Go extraction) that a PBFT single-log-entry implementation satisfies agreement, termination and validity with Byzantine nodes, assuming partial synchrony and unforgeable signatures.
- assumes: partial synchrony: network eventually stabilizes; unforgeable signatures; unverified Go runtime
- size or effort: Shipwright 13,357 lines (1,351 trusted); PBFT 31,138 lines (266 trusted); total 44,495 lines; person-effort not given
- tool: Dafny + Go extraction (Shipwright); written by: human
- case A:205; source record shipwright-2025
PBFT single-log-entry agreement (Go implementation)
- guarantee: Shipwright proves, for a Go implementation of PBFT single-log-entry agreement, eventual progress with malicious participants in the common case and failure scenarios, and also correctness.
- assumes: Byzantine participants; fairness details not seen
- size or effort: not seen
- tool: Shipwright (own framework, proof assistant); written by: human
- case A:196; source record shipwright-2025
PBFT state-machine replication
- guarantee: PBFT safety under at most f Byzantine replicas is machine-checked in Coq (Velisarios) and extracted to OCaml, with 27.6 us per request locally and about 7 s view-change recovery.
- assumes: At most f Byzantine replicas; authenticated messages and cryptographic assumptions
- size or effort: Machine-checked PBFT safety; 27.6 μs local million-request run; ~7 s view-change recovery
- tool: Velisarios Coq logic-of-events and extracted OCaml; written by: human
- case C:codex_snowball:28; source record velisarios-2018
Producer-consumer over a bounded FIFO of capacity 10 (C)
- guarantee: VeriFast with ghost signals verified that both threads of a capacity-10 bounded FIFO producer-consumer in C terminate despite busy-waiting, using 160 annotation lines for 37 lines of code (0.08 s); the ghost-signal rules are trusted axioms.
- assumes: Fair scheduling; ghost-signal rules added as axioms in a trusted header
- size or effort: 160 annotation lines for 37 lines of code (435%), 0.08 s
- tool: ghost signals encoded in VeriFast (call and wait permissions); written by: human
- case C:r6:45; Ghost signals thesis, Sec 3.3 and 3.5
ReplicaSet controller
- guarantee: Anvil’s ReplicaSet controller eventually reaches a stable replica count, assuming the desired state stabilizes and the controller is weakly fair.
- assumes: Desired-state description eventually stabilizes; weak fairness on model actions; message drops/controller crashes eventually cease; PodMonkey disturbances eventually cease. Welder §5 PDFp11: faults eventually stop (including PodMonkey as specified below). Additional retry-on-conflict fairness: each retry loop terminates, either succeeding or returning a non-version-conflict error; §4.2 PDFp9: “RoC loop terminates”. Always-preserved request-centric rely restrictions on other controllers, with own guarantee satisfying compatible controllers; no finite delivery/computation bound required. No external controller progress dependency in this model: §3.3 PDFp7 DS = True. PodMonkey eventually stops but must still obey applicable request rely restrictions. Gap: pinned ownership/rely predicates and retry fairness deployment validation unresolved
- tool: liveness; written by: human
- case B:liveness:7; source record welder-2026
SAT-Backtrack
- guarantee: Deterministic backtracking SAT algorithm terminates; checked in 0.3 s.
- assumes: none
- size or effort: Table 2: 0.3 s, 9, 0, 8, 157 tokens
- tool: timer reduction + implicit rankings, Z3 (mypyvy-style tool); written by: automatic tool
- case A:322; source record timers-2026
Single-producer single-consumer queue (memory-efficient)
- guarantee: A Rocq/Iris proof using Lawyer logic shows a memory-efficient single-producer single-consumer queue is wait-free (operations terminate) when there is at most one enqueuer and one dequeuer thread.
- assumes: at most 1 enqueuer and 1 dequeuer
- size or effort: unknown
- tool: Rocq + Iris, Lawyer logic; written by: human
- case A:164; Verifying Wait-Freedom for Concurrent Higher-Order Programs (ECOOP 2026), abstract
SV-Benchmarks C programs expected to terminate, verified by CPAchecker (ranking functions)
- guarantee: A verifier proved termination of SV-Benchmarks C programs (verified by CPAchecker (ranking functions)); 422 programs verified; 366 witnesses validated by at least one validator (87%), re-checked by other tools.
- assumes: Termination only (not deadlock or other non-progress); finite-state reduction for the reachability route; 900 s CPU and 15 GB per run; only programs the verifier itself solved are counted
- size or effort: 422 programs verified; 366 witnesses validated by at least one validator (87%)
- tool: CPAchecker (ranking functions) to produce the witness; validators CPAchecker-TransVer, UAutomizer-TransVer, CPAchecker-decreasing, CPAchecker-simplifying; written by: automatic tool
- case C:r8:36; Transition Invariants Revisited, Sec. 6.1 Tab. 2
SV-Benchmarks C programs expected to terminate, verified by CPAchecker via TransVer (reduction to reachability)
- guarantee: A verifier proved termination of SV-Benchmarks C programs (verified by CPAchecker via TransVer (reduction to reachability)); 200 programs verified; 192 witnesses validated by at least one validator (96%), re-checked by other tools.
- assumes: Termination only (not deadlock or other non-progress); finite-state reduction for the reachability route; 900 s CPU and 15 GB per run; only programs the verifier itself solved are counted
- size or effort: 200 programs verified; 192 witnesses validated by at least one validator (96%)
- tool: CPAchecker via TransVer (reduction to reachability) to produce the witness; validators CPAchecker-TransVer, UAutomizer-TransVer, CPAchecker-decreasing, CPAchecker-simplifying; written by: automatic tool
- case C:r8:37; Transition Invariants Revisited, Sec. 6.1 Tab. 2
SV-Benchmarks C programs expected to terminate, verified by Goblint via TransVer
- guarantee: A verifier proved termination of SV-Benchmarks C programs (verified by Goblint via TransVer); 286 programs verified; 176 witnesses validated by at least one validator (62%), re-checked by other tools.
- assumes: Termination only (not deadlock or other non-progress); finite-state reduction for the reachability route; 900 s CPU and 15 GB per run; only programs the verifier itself solved are counted; 110 witnesses failed because Goblint wrote 4394 invariants in total (about 16 per program), so validators timed out or ran out of memory
- size or effort: 286 programs verified; 176 witnesses validated by at least one validator (62%)
- tool: Goblint via TransVer to produce the witness; validators CPAchecker-TransVer, UAutomizer-TransVer, CPAchecker-decreasing, CPAchecker-simplifying; written by: automatic tool
- case C:r8:39; Transition Invariants Revisited, Sec. 6.1 Tab. 2
SV-Benchmarks C programs expected to terminate, verified by UAutomizer via TransVer
- guarantee: A verifier proved termination of SV-Benchmarks C programs (verified by UAutomizer via TransVer); 389 programs verified; 375 witnesses validated by at least one validator (96%), re-checked by other tools.
- assumes: Termination only (not deadlock or other non-progress); finite-state reduction for the reachability route; 900 s CPU and 15 GB per run; only programs the verifier itself solved are counted
- size or effort: 389 programs verified; 375 witnesses validated by at least one validator (96%)
- tool: UAutomizer via TransVer to produce the witness; validators CPAchecker-TransVer, UAutomizer-TransVer, CPAchecker-decreasing, CPAchecker-simplifying; written by: automatic tool
- case C:r8:38; Transition Invariants Revisited, Sec. 6.1 Tab. 2
SystemVerilog hardware design: 7-Segment
- guarantee: The new method solved 30 of 30 tasks of checking “something good eventually happens” properties of the SystemVerilog 7-Segment hardware design, using a learned certificate checked by the Bitwuzla SMT solver (paper’s own report).
- assumes: Hardware/reactive systems only; no arrays, strings of parametric length, procedure calls or dynamic data structures; 5 h limit per task per tool
- size or effort: 30 of 30 tasks solved by the new method (Table 1)
- tool: Neural certificate (inductive invariant + ranking function) learned with MILP solver Gurobi, checked with Bitwuzla; compared with ABC, nuXmv, rIC3 (and NMC’24 for liveness); written by: automatic tool
- case C:r7:30; Let a Neural Network Be Your Invariant, Table 1 and Appendix A
SystemVerilog hardware design: 7-Segment
- guarantee: The new method solved 9 of 15 tasks of checking combined properties such as “a until b” of the SystemVerilog 7-Segment hardware design, using a learned certificate checked by the Bitwuzla SMT solver (paper’s own report).
- assumes: Hardware/reactive systems only; no arrays, strings of parametric length, procedure calls or dynamic data structures; 5 h limit per task per tool
- size or effort: 9 of 15 tasks solved by the new method (Table 1)
- tool: Neural certificate (inductive invariant + ranking function) learned with MILP solver Gurobi, checked with Bitwuzla; compared with ABC, nuXmv, rIC3 (and NMC’24 for liveness); written by: automatic tool
- case C:r7:41; Let a Neural Network Be Your Invariant, Table 1 and Appendix A
SystemVerilog hardware design: Blink
- guarantee: The new method solved 14 of 25 tasks of checking “something good eventually happens” properties of the SystemVerilog Blink hardware design, using a learned certificate checked by the Bitwuzla SMT solver (paper’s own report).
- assumes: Hardware/reactive systems only; no arrays, strings of parametric length, procedure calls or dynamic data structures; 5 h limit per task per tool
- size or effort: 14 of 25 tasks solved by the new method (Table 1)
- tool: Neural certificate (inductive invariant + ranking function) learned with MILP solver Gurobi, checked with Bitwuzla; compared with ABC, nuXmv, rIC3 (and NMC’24 for liveness); written by: automatic tool
- case C:r7:36; Let a Neural Network Be Your Invariant, Table 1 and Appendix A
SystemVerilog hardware design: Blink
- guarantee: The new method solved 11 of 25 tasks of checking combined properties such as “a until b” of the SystemVerilog Blink hardware design, using a learned certificate checked by the Bitwuzla SMT solver (paper’s own report).
- assumes: Hardware/reactive systems only; no arrays, strings of parametric length, procedure calls or dynamic data structures; 5 h limit per task per tool
- size or effort: 11 of 25 tasks solved by the new method (Table 1)
- tool: Neural certificate (inductive invariant + ranking function) learned with MILP solver Gurobi, checked with Bitwuzla; compared with ABC, nuXmv, rIC3 (and NMC’24 for liveness); written by: automatic tool
- case C:r7:47; Let a Neural Network Be Your Invariant, Table 1 and Appendix A
SystemVerilog hardware design: Delay
- guarantee: The new method solved 32 of 32 tasks of checking “something good eventually happens” properties of the SystemVerilog Delay hardware design, using a learned certificate checked by the Bitwuzla SMT solver (paper’s own report).
- assumes: Hardware/reactive systems only; no arrays, strings of parametric length, procedure calls or dynamic data structures; 5 h limit per task per tool
- size or effort: 32 of 32 tasks solved by the new method (Table 1)
- tool: Neural certificate (inductive invariant + ranking function) learned with MILP solver Gurobi, checked with Bitwuzla; compared with ABC, nuXmv, rIC3 (and NMC’24 for liveness); written by: automatic tool
- case C:r7:34; Let a Neural Network Be Your Invariant, Table 1 and Appendix A
SystemVerilog hardware design: Delay
- guarantee: The new method solved 32 of 32 tasks of checking combined properties such as “a until b” of the SystemVerilog Delay hardware design, using a learned certificate checked by the Bitwuzla SMT solver (paper’s own report).
- assumes: Hardware/reactive systems only; no arrays, strings of parametric length, procedure calls or dynamic data structures; 5 h limit per task per tool
- size or effort: 32 of 32 tasks solved by the new method (Table 1)
- tool: Neural certificate (inductive invariant + ranking function) learned with MILP solver Gurobi, checked with Bitwuzla; compared with ABC, nuXmv, rIC3 (and NMC’24 for liveness); written by: automatic tool
- case C:r7:45; Let a Neural Network Be Your Invariant, Table 1 and Appendix A
SystemVerilog hardware design: Gray Counter
- guarantee: The new method solved 33 of 33 tasks of checking “something good eventually happens” properties of the SystemVerilog Gray Counter hardware design, using a learned certificate checked by the Bitwuzla SMT solver (paper’s own report).
- assumes: Hardware/reactive systems only; no arrays, strings of parametric length, procedure calls or dynamic data structures; 5 h limit per task per tool
- size or effort: 33 of 33 tasks solved by the new method (Table 1)
- tool: Neural certificate (inductive invariant + ranking function) learned with MILP solver Gurobi, checked with Bitwuzla; compared with ABC, nuXmv, rIC3 (and NMC’24 for liveness); written by: automatic tool
- case C:r7:35; Let a Neural Network Be Your Invariant, Table 1 and Appendix A
SystemVerilog hardware design: Gray Counter
- guarantee: The new method solved 22 of 22 tasks of checking combined properties such as “a until b” of the SystemVerilog Gray Counter hardware design, using a learned certificate checked by the Bitwuzla SMT solver (paper’s own report).
- assumes: Hardware/reactive systems only; no arrays, strings of parametric length, procedure calls or dynamic data structures; 5 h limit per task per tool
- size or effort: 22 of 22 tasks solved by the new method (Table 1)
- tool: Neural certificate (inductive invariant + ranking function) learned with MILP solver Gurobi, checked with Bitwuzla; compared with ABC, nuXmv, rIC3 (and NMC’24 for liveness); written by: automatic tool
- case C:r7:46; Let a Neural Network Be Your Invariant, Table 1 and Appendix A
SystemVerilog hardware design: i2c Stretch
- guarantee: The new method solved 20 of 20 tasks of checking “something good eventually happens” properties of the SystemVerilog i2c Stretch hardware design, using a learned certificate checked by the Bitwuzla SMT solver (paper’s own report).
- assumes: Hardware/reactive systems only; no arrays, strings of parametric length, procedure calls or dynamic data structures; 5 h limit per task per tool
- size or effort: 20 of 20 tasks solved by the new method (Table 1)
- tool: Neural certificate (inductive invariant + ranking function) learned with MILP solver Gurobi, checked with Bitwuzla; compared with ABC, nuXmv, rIC3 (and NMC’24 for liveness); written by: automatic tool
- case C:r7:29; Let a Neural Network Be Your Invariant, Table 1 and Appendix A
SystemVerilog hardware design: i2c Stretch
- guarantee: The new method solved 3 of 20 tasks of checking combined properties such as “a until b” of the SystemVerilog i2c Stretch hardware design, using a learned certificate checked by the Bitwuzla SMT solver (paper’s own report).
- assumes: Hardware/reactive systems only; no arrays, strings of parametric length, procedure calls or dynamic data structures; 5 h limit per task per tool
- size or effort: 3 of 20 tasks solved by the new method (Table 1)
- tool: Neural certificate (inductive invariant + ranking function) learned with MILP solver Gurobi, checked with Bitwuzla; compared with ABC, nuXmv, rIC3 (and NMC’24 for liveness); written by: automatic tool
- case C:r7:40; Let a Neural Network Be Your Invariant, Table 1 and Appendix A
SystemVerilog hardware design: LCD Controller
- guarantee: The new method solved 14 of 14 tasks of checking “something good eventually happens” properties of the SystemVerilog LCD Controller hardware design, using a learned certificate checked by the Bitwuzla SMT solver (paper’s own report).
- assumes: Hardware/reactive systems only; no arrays, strings of parametric length, procedure calls or dynamic data structures; 5 h limit per task per tool
- size or effort: 14 of 14 tasks solved by the new method (Table 1)
- tool: Neural certificate (inductive invariant + ranking function) learned with MILP solver Gurobi, checked with Bitwuzla; compared with ABC, nuXmv, rIC3 (and NMC’24 for liveness); written by: automatic tool
- case C:r7:27; Let a Neural Network Be Your Invariant, Table 1 and Appendix A
SystemVerilog hardware design: LCD Controller
- guarantee: The new method solved 14 of 14 tasks of checking combined properties such as “a until b” of the SystemVerilog LCD Controller hardware design, using a learned certificate checked by the Bitwuzla SMT solver (paper’s own report).
- assumes: Hardware/reactive systems only; no arrays, strings of parametric length, procedure calls or dynamic data structures; 5 h limit per task per tool
- size or effort: 14 of 14 tasks solved by the new method (Table 1)
- tool: Neural certificate (inductive invariant + ranking function) learned with MILP solver Gurobi, checked with Bitwuzla; compared with ABC, nuXmv, rIC3 (and NMC’24 for liveness); written by: automatic tool
- case C:r7:38; Let a Neural Network Be Your Invariant, Table 1 and Appendix A
SystemVerilog hardware design: Load-Store (LS)
- guarantee: The new method solved 32 of 32 tasks of checking combined properties such as “a until b” of the SystemVerilog Load-Store (LS) hardware design, using a learned certificate checked by the Bitwuzla SMT solver (paper’s own report).
- assumes: Hardware/reactive systems only; no arrays, strings of parametric length, procedure calls or dynamic data structures; 5 h limit per task per tool
- size or effort: 32 of 32 tasks solved by the new method (Table 1)
- tool: Neural certificate (inductive invariant + ranking function) learned with MILP solver Gurobi, checked with Bitwuzla; compared with ABC, nuXmv, rIC3 (and NMC’24 for liveness); written by: automatic tool
- case C:r7:37; Let a Neural Network Be Your Invariant, Table 1 and Appendix A
SystemVerilog hardware design: Pulse Width Modulation
- guarantee: The new method solved 12 of 12 tasks of checking “something good eventually happens” properties of the SystemVerilog Pulse Width Modulation hardware design, using a learned certificate checked by the Bitwuzla SMT solver (paper’s own report).
- assumes: Hardware/reactive systems only; no arrays, strings of parametric length, procedure calls or dynamic data structures; 5 h limit per task per tool
- size or effort: 12 of 12 tasks solved by the new method (Table 1)
- tool: Neural certificate (inductive invariant + ranking function) learned with MILP solver Gurobi, checked with Bitwuzla; compared with ABC, nuXmv, rIC3 (and NMC’24 for liveness); written by: automatic tool
- case C:r7:31; Let a Neural Network Be Your Invariant, Table 1 and Appendix A
SystemVerilog hardware design: Pulse Width Modulation
- guarantee: The new method solved 12 of 12 tasks of checking combined properties such as “a until b” of the SystemVerilog Pulse Width Modulation hardware design, using a learned certificate checked by the Bitwuzla SMT solver (paper’s own report).
- assumes: Hardware/reactive systems only; no arrays, strings of parametric length, procedure calls or dynamic data structures; 5 h limit per task per tool
- size or effort: 12 of 12 tasks solved by the new method (Table 1)
- tool: Neural certificate (inductive invariant + ranking function) learned with MILP solver Gurobi, checked with Bitwuzla; compared with ABC, nuXmv, rIC3 (and NMC’24 for liveness); written by: automatic tool
- case C:r7:42; Let a Neural Network Be Your Invariant, Table 1 and Appendix A
SystemVerilog hardware design: Thermocouple
- guarantee: The new method solved 17 of 17 tasks of checking “something good eventually happens” properties of the SystemVerilog Thermocouple hardware design, using a learned certificate checked by the Bitwuzla SMT solver (paper’s own report).
- assumes: Hardware/reactive systems only; no arrays, strings of parametric length, procedure calls or dynamic data structures; 5 h limit per task per tool
- size or effort: 17 of 17 tasks solved by the new method (Table 1)
- tool: Neural certificate (inductive invariant + ranking function) learned with MILP solver Gurobi, checked with Bitwuzla; compared with ABC, nuXmv, rIC3 (and NMC’24 for liveness); written by: automatic tool
- case C:r7:28; Let a Neural Network Be Your Invariant, Table 1 and Appendix A
SystemVerilog hardware design: Thermocouple
- guarantee: The new method solved 17 of 17 tasks of checking combined properties such as “a until b” of the SystemVerilog Thermocouple hardware design, using a learned certificate checked by the Bitwuzla SMT solver (paper’s own report).
- assumes: Hardware/reactive systems only; no arrays, strings of parametric length, procedure calls or dynamic data structures; 5 h limit per task per tool
- size or effort: 17 of 17 tasks solved by the new method (Table 1)
- tool: Neural certificate (inductive invariant + ranking function) learned with MILP solver Gurobi, checked with Bitwuzla; compared with ABC, nuXmv, rIC3 (and NMC’24 for liveness); written by: automatic tool
- case C:r7:39; Let a Neural Network Be Your Invariant, Table 1 and Appendix A
SystemVerilog hardware design: UART Transmitter
- guarantee: The new method solved 10 of 10 tasks of checking “something good eventually happens” properties of the SystemVerilog UART Transmitter hardware design, using a learned certificate checked by the Bitwuzla SMT solver (paper’s own report).
- assumes: Hardware/reactive systems only; no arrays, strings of parametric length, procedure calls or dynamic data structures; 5 h limit per task per tool
- size or effort: 10 of 10 tasks solved by the new method (Table 1)
- tool: Neural certificate (inductive invariant + ranking function) learned with MILP solver Gurobi, checked with Bitwuzla; compared with ABC, nuXmv, rIC3 (and NMC’24 for liveness); written by: automatic tool
- case C:r7:33; Let a Neural Network Be Your Invariant, Table 1 and Appendix A
SystemVerilog hardware design: UART Transmitter
- guarantee: The new method solved 10 of 10 tasks of checking combined properties such as “a until b” of the SystemVerilog UART Transmitter hardware design, using a learned certificate checked by the Bitwuzla SMT solver (paper’s own report).
- assumes: Hardware/reactive systems only; no arrays, strings of parametric length, procedure calls or dynamic data structures; 5 h limit per task per tool
- size or effort: 10 of 10 tasks solved by the new method (Table 1)
- tool: Neural certificate (inductive invariant + ranking function) learned with MILP solver Gurobi, checked with Bitwuzla; compared with ABC, nuXmv, rIC3 (and NMC’24 for liveness); written by: automatic tool
- case C:r7:44; Let a Neural Network Be Your Invariant, Table 1 and Appendix A
SystemVerilog hardware design: VGA Controller
- guarantee: The new method solved 10 of 10 tasks of checking “something good eventually happens” properties of the SystemVerilog VGA Controller hardware design, using a learned certificate checked by the Bitwuzla SMT solver (paper’s own report).
- assumes: Hardware/reactive systems only; no arrays, strings of parametric length, procedure calls or dynamic data structures; 5 h limit per task per tool
- size or effort: 10 of 10 tasks solved by the new method (Table 1)
- tool: Neural certificate (inductive invariant + ranking function) learned with MILP solver Gurobi, checked with Bitwuzla; compared with ABC, nuXmv, rIC3 (and NMC’24 for liveness); written by: automatic tool
- case C:r7:32; Let a Neural Network Be Your Invariant, Table 1 and Appendix A
SystemVerilog hardware design: VGA Controller
- guarantee: The new method solved 10 of 10 tasks of checking combined properties such as “a until b” of the SystemVerilog VGA Controller hardware design, using a learned certificate checked by the Bitwuzla SMT solver (paper’s own report).
- assumes: Hardware/reactive systems only; no arrays, strings of parametric length, procedure calls or dynamic data structures; 5 h limit per task per tool
- size or effort: 10 of 10 tasks solved by the new method (Table 1)
- tool: Neural certificate (inductive invariant + ranking function) learned with MILP solver Gurobi, checked with Bitwuzla; compared with ABC, nuXmv, rIC3 (and NMC’24 for liveness); written by: automatic tool
- case C:r7:43; Let a Neural Network Be Your Invariant, Table 1 and Appendix A
Treiber stack, HSY stack, DCAS stack, Michael-Scott queue (+Doherty), RDCSS, Michael’s list
- guarantee: Lock-freedom or obstruction-freedom of Treiber, HSY, DCAS stacks, Michael-Scott queue, RDCSS and Michael’s list were shown by an automatic tool; Fomitchev-Yahav delete was shown not obstruction-free.
- assumes: any thread may be stopped; isolation for obstruction-freedom
- size or effort: under 10 minutes each, Michael’s list about 8 hours
- tool: automatic tool (shape analysis + termination prover), rely-guarantee; written by: automatic tool
- case A:182; Gotsman et al., POPL 2009, s.6
Welder Deployment controller
- guarantee: Welder Deployment controller: desired state eventually reached while compatible controllers interact; interference restrictions hold.
- assumes: compatible rely/guarantee conditions; eventual stable desired state; environment fairness/fault conditions; acyclic liveness dependencies
- tool: Verus implementation/model conformance and compositional temporal proof; written by: human
- case B:systems:9; source record welder-2026
Welder four-controller composition
- guarantee: Welder shows the four verified controllers together satisfy CORE, with compatibility obligations (Deployment depends on ReplicaSet, RabbitMQ on StatefulSet).
- assumes: Deployment depends on ReplicaSet; RabbitMQ depends on StatefulSet
- tool: compatibility obligations and compositional theorem; written by: human
- case B:systems:12; source record welder-2026
Welder RabbitMQ controller
- guarantee: Welder’s RabbitMQ controller is proved with Verus to eventually reach the desired state while compatible controllers interact, and to respect interference restrictions.
- assumes: compatible rely/guarantee conditions; eventual stable desired state; environment fairness/fault conditions; acyclic liveness dependencies
- tool: Verus implementation/model conformance and compositional temporal proof; written by: human
- case B:systems:11; source record welder-2026
Welder ReplicaSet controller
- guarantee: Welder verifies in Verus that the ReplicaSet controller reaches the desired state while compatible controllers interact, under rely/guarantee conditions.
- assumes: compatible rely/guarantee conditions; eventual stable desired state; environment fairness/fault conditions; acyclic liveness dependencies
- tool: Verus implementation/model conformance and compositional temporal proof; written by: human
- case B:systems:8; source record welder-2026
Welder StatefulSet controller
- guarantee: Verus proves that the Welder StatefulSet controller eventually reaches the desired state while compatible controllers interact, and that interference restrictions hold.
- assumes: compatible rely/guarantee conditions; eventual stable desired state; environment fairness/fault conditions; acyclic liveness dependencies
- tool: Verus implementation/model conformance and compositional temporal proof; written by: human
- case B:systems:10; source record welder-2026
Yes-no with diverging thread
- guarantee: A concurrent ‘yes-no’ implementation is proved to make its specified progress even if another thread diverges.
- assumes: conditional guarantee; see cited paper and liveness note for fairness, timing and fault premises; exact case-specific premises not fully extracted
- tool: liveness; written by: human
- case B:liveness:15; source record trillium-2024
ZooKeeper controller
- guarantee: Anvil’s ZooKeeper controller eventually reaches a stable desired cluster configuration, assuming the desired state stabilizes and the controller is weakly fair.
- assumes: Stable desired-state description; weak fairness on controller/environment actions; modeled crashes and request failures eventually cease; built-in StatefulSet/DaemonSet updates eventually pause until the target updates again. Anvil §4.3.3 PDFp9: “eventually stop happening”; the competing-controller pause premise is stated in the same section. Trust TLA embedding, environment/API models, Verus/Z3, Rust compiler and OS (§4.1). Additional trusted ZooKeeper API model and response fairness: §6.1 PDFp12 “eventually receives a response” for a request sent to the deployed cluster. Gap: exact pinned ESR theorem predicates for allowed external interference and revised ZooKeeper API contract must be extracted before reuse
- tool: liveness; written by: human
- case B:liveness:3; source record anvil-2024

abstract model only, proof accepted by a proof checker

91 cases.

Ackermann (stack implementation)
- guarantee: Timer reduction and implicit rankings with Z3 prove that a stack implementation of the Ackermann function terminates.
- assumes: none; source [22] Hoenicke, Padon, Shoham
- size or effort: Table 2: 0.8 s, 5, 2, 9, 211 tokens (748 L2S)
- tool: timer reduction + implicit rankings, Z3 (mypyvy-style tool); written by: automatic tool
- case A:312; source record timers-2026
Allocator (clients, resources)
- guarantee: In a 297-line TLA+ allocator file, TLAPS proves only the Mutex safety property; the liveness properties ClientsWillReturn, ClientsWillObtain and InfOftenSatisfied are stated with no theorem found.
- assumes: WF on Return, SF on Allocate
- size or effort: 297-line file
- tool: TLA+ with TLAPS (safety only proved); written by: human
- case A:188; tlapm/examples/Allocator.tla
alternating bit
- guarantee: Alternating bit: data from the sender is eventually received despite packet loss, assuming a minimum delivery guarantee; 127 LoC.
- assumes: ‘minimum guarantee on packet delivery’; channel with packet loss
- size or effort: Table 4: 9 transitions, 127 LoC, 2 user-guidance bounds, tier 2
- tool: LVR (ranking function synthesis, mypyvy, P-FOL-IC3, Z3/CVC4); written by: automatic tool
- case A:334; Yao, Tao, Gu, Nieh, Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions (POPL 2024), Table 3-5
Alternating bit protocol
- guarantee: Ivy with a manual liveness-to-safety reduction proves the alternating bit protocol eventually transmits every array entry, a stronger property than that of Abdulla et al. 2006.
- assumes: ‘for each channel: if messages are infinitely often sent, then messages are infinitely often received’; assumes i0 reachable (finitely many indices below i0)
- size or effort: Fig. 10: 2 nesting levels; Cs=13, Ce=2, Cm=20; EPR; 6.9 s
- tool: Ivy (Z3), manual liveness-to-safety reduction + inductive invariant; written by: automatic tool
- case A:341; Padon, Hoenicke, Losa, Podelski, Sagiv, Shoham, Reducing Liveness to Safety in First-Order Logic (POPL 2018), Sec 2, Sec 7, Fig. 10
Alternating bit protocol (ABP)
- guarantee: For the alternating bit protocol under weak fairness of lossy FIFO channels with unbounded drops, all sender data is eventually received, proved with a timer reduction, implicit rankings and Z3 (4 s).
- assumes: weak fairness of lossy FIFO channels
- size or effort: Table 2: 4 s, 31 constructors, 2, 34, 539 tokens (860 L2S)
- tool: timer reduction + implicit rankings, Z3 (mypyvy-style tool); written by: automatic tool
- case A:309; source record timers-2026
Alternating bit protocol (lossy channel)
- guarantee: LVR proves that over a lossy channel the alternating bit protocol eventually delivers any data the sender sends, assuming a minimum guarantee on packet delivery.
- assumes: Minimum guarantee on packet delivery
- size or effort: 127 lines, 9 transitions; 2 bound hints, 2 tiers
- tool: LVR (mypyvy); written by: automatic tool
- case A:351; Yao, PhD thesis 2024, Sec. 4.8, Table 4.3-4.4
Asynchronous Byzantine binary agreement (HoneyBadger BA with fix), graded crusader agreement, common coin
- guarantee: Rocq (SureDistrib) proves asynchronous Byzantine binary agreement (HoneyBadger style) terminates with probability 1 against an adversarial scheduler, treating the common coin as a black box.
- assumes: asynchronous network, adversarial scheduler, common coin as black box
- size or effort: not extracted
- tool: Rocq (SureDistrib); written by: human
- case A:213; source record suredistrib-2026
Barnacle over Mysticeti, Blue Bottle, Nemo-Nemo, Orcaella (DAG consensus)
- guarantee: A Lean 4 proof (about 3,900 lines, about 2,000 AI-generated, no sorry) shows DAG consensus protocols (Barnacle over Mysticeti, Blue Bottle, Nemo-Nemo, Orcaella) have honest validators commit the same leader sequence, and after GST commit new leaders infinitely often.
- assumes: partial synchrony (GST, bound Δ); Byzantine 3f+1 or 5f+1, crash 2c+1, mixed 5f+3c+1
- size or effort: ~3,900 Lean lines: ~1,900 definitions and statements, ~2,000 AI-generated proofs, ~3,200 lines executable witnesses; no sorry
- tool: Lean 4; written by: agent
- case A:136; source record barnacle-2026
Ben-Or
- guarantee: Ben-Or consensus liveness is verified with ByMC using threshold automata and round-rigid adversaries.
- assumes: not stated in the table
- size or effort: not given in SoK; see cited paper [6] Bertrand et al., STTT 2021
- tool: ByMC; threshold automata, round-rigid adversaries; written by: human
- case A:230; Bondarev, Ziborov, Yanovich, SoK: Formal Verification of Consensus Protocols (arXiv 2608.21935), Table 1 p.7 ; cites [6] Bertrand et al., STTT 2021
Binary Counter (Example 2)
- guarantee: A binary counter starting from all 1s is proved to eventually hold all 0s with no fairness assumption, using implicit rankings and Z3.
- assumes: no fairness assumption; ♦true
- size or effort: implicit ranking structure given in Sec 6; no per-example numbers in the arXiv version text
- tool: implicit rankings + Z3 (all verified within 10 minutes); written by: automatic tool
- case A:325; source record implicit-rankings-2025
BinaryCounter
- guarantee: A binary counter in an array that changes one cell per operation is proved to terminate, using implicit rankings and Z3 (0.02 s).
- assumes: none
- size or effort: Table 2: 0.02 s, 4, 0, 0, 21 tokens
- tool: timer reduction + implicit rankings, Z3 (mypyvy-style tool); written by: automatic tool
- case A:321; source record timers-2026
Bosco, Hybrid Reliable Broadcast and Byzantine Fast Paxos
- guarantee: Safety and liveness of Bosco, Hybrid Reliable Broadcast and Byzantine Fast Paxos are verified under threshold resilience conditions using Aip and Ivy with a user-supplied inductive invariant.
- assumes: User-supplied inductive invariant; threshold intersection properties; liveness-to-safety reduction
- size or effort: 10 repetitions; Aip under one minute and 3–5 inferred formulas after minimization
- tool: EPR+BAPA decomposition with Aip and Ivy; written by: human
- case C:codex_snowball:22; source record threshold-decomposition-2019
Cascaded/blocked/bypassing queues
- guarantee: Ivy abstract models of cascaded, blocked and bypassing queues give compositional progress examples.
- assumes: conditional guarantee; see cited paper and liveness note for fairness, timing and fault premises; exact case-specific premises not fully extracted
- tool: liveness; written by: human
- case B:liveness:23; liveness Ivy abstract models; CAV2024 repository README
CascadingQueue
- guarantee: Z3 with timers and implicit rankings proves that in CascadingQueue any sent message is eventually received, if both queues are polled infinitely often.
- assumes: ‘both queues are polled infinitely often’; source [29]
- size or effort: Table 2: 1.2 s, 9, 2, 7, 175 tokens
- tool: timer reduction + implicit rankings, Z3 (mypyvy-style tool); written by: automatic tool
- case A:315; source record timers-2026
Casper (FFG)
- guarantee: Rocq proves liveness of the Casper FFG finality gadget model.
- assumes: not stated in the table ; SoK 2.2: ‘plausible liveness’: ‘from any reachable state there still exists a continuation in which checkpoints can again be finalized without violating slashing conditions, provided that more than two thirds of the stake follows the protocol’
- size or effort: not given in SoK; see cited paper [32] Palmskog et al., Verification of Casper in Coq
- tool: Rocq; finality gadget model; written by: human
- case A:251; Bondarev, Ziborov, Yanovich, SoK: Formal Verification of Consensus Protocols (arXiv 2608.21935), Table 1 p.7 ; cites [32] Palmskog et al., Verification of Casper in Coq
Chandra-Toueg consensus with failure detector diamond-S (Isabelle)
- guarantee: Chandra-Toueg consensus with diamond-S: agreement, validity and termination proved in Isabelle/HOL, ~10k LOC.
- assumes: Fairness assumptions on communication and failure detection (as in Chandra-Toueg)
- size or effort: ~10k LOC Isabelle/HOL
- tool: Isabelle/HOL; written by: human
- case A:358; Kufner, Nestmann, Rickmann, TCS 2012, Sec. 5
Chandra-Toueg failure detector (partial synchrony)
- guarantee: The Chandra-Toueg failure detector eventually becomes accurate and complete under partial synchrony (GST, bounds Delta and Phi), shown in Ivy with liveness reduced by hand to safety, and in TLA+.
- assumes: partial synchrony with GST, bounds Delta and Phi; processes send alive infinitely often; reliable communication between correct processes
- size or effort: not extracted; invariants in Table 4 of the paper
- tool: Ivy (liveness reduced by hand to safety), TLA+ (TLC/Apalache), counter automata (FAST); written by: unclear
- case A:33; source record a-case-study-on-2023
Chang–Roberts leader ring
- guarantee: Implicit rankings prove on an abstract model that Chang-Roberts leader ring eventually elects a leader.
- assumes: conditional guarantee; see cited paper and liveness note for fairness, timing and fault premises; exact case-specific premises not fully extracted
- tool: liveness; written by: automatic tool
- case B:liveness:43; liveness abstract model; Lotan–Shoham §6
Concurrent counter increment and higher-order list map
- guarantee: Rocq with Iris and the Lawyer logic proves wait-freedom, meaning every call terminates regardless of other threads, for a concurrent counter increment and higher-order list map, without fairness assumptions.
- assumes: no fairness needed (wait-freedom is claimed without a fair scheduler)
- size or effort: unknown (see artifact)
- tool: Rocq + Iris, Lawyer logic; written by: human
- case A:163; Verifying Wait-Freedom for Concurrent Higher-Order Programs (ECOOP 2026), s.1, abstract
Countdown timer (toy)
- guarantee: A countdown timer is proved in Dafny to eventually reach 0 under weak fairness.
- assumes: weak fairness encoded as a predicate over traces
- size or effort: blog
- tool: Dafny with embedded TLA operators; written by: human
- case A:39; source record dafny-2010
DAG BFT consensus: Narwhal, Bullshark, Sailfish
- guarantee: Coq/Rocq (LiDO-DAG) proves safety, liveness (every non-faulty block eventually committed) and fairness of Narwhal, Bullshark and Sailfish under partial synchrony, at model level only.
- assumes: partial synchrony; authenticated; model-level only
- size or effort: LiDO-DAG model 747 spec + 1,500 proof lines; Narwhal 2,307 spec + 9,697 proof; Bullshark 603 spec + 4,343 proof
- tool: Coq/Rocq (LiDO-DAG); written by: human
- case A:211; source record lido-dag-2025
Dekker mutual exclusion (2 processes)
- guarantee: TLAPS proves Dekker’s two-process algorithm gives mutual exclusion and never gets stuck, and that process 1 starting to enter eventually reaches the critical section (pc1=2 ~> pc1=6) under weak fairness.
- assumes: WF_vars1(pc1 # 9 /\ Next1), WF_vars2
- size or effort: 978-line file; 2 steps OMITTED (ENABLED axioms)
- tool: TLAPS; written by: human
- case A:187; tlapm/examples/Dekker/Dekker.tla
Dijkstra 3-State protocol
- guarantee: Implicit rankings with Z3 prove that Dijkstra’s 3-state protocol stabilizes and is fair.
- assumes: ranking from [26] Kessels, based on [13]
- size or effort: implicit ranking structure given in Sec 6; no per-example numbers in the arXiv version text
- tool: implicit rankings + Z3 (all verified within 10 minutes); written by: automatic tool
- case A:331; source record implicit-rankings-2025
Dijkstra 4-State protocol
- guarantee: Dijkstra 4-state stabilization is proved: a unique privilege eventually exists and every machine gets the privilege infinitely often, using implicit rankings and Z3.
- assumes: based on [11]
- size or effort: implicit ranking structure given in Sec 6; no per-example numbers in the arXiv version text
- tool: implicit rankings + Z3 (all verified within 10 minutes); written by: automatic tool
- case A:329; source record implicit-rankings-2025
Dijkstra k-state, 4-state, 3-state self-stabilizing protocols
- guarantee: Z3 with implicit rankings proves that Dijkstra’s k-state, 4-state and 3-state protocols eventually leave only one machine with a privilege.
- assumes: parameterized fairness assumptions ri; ♦true when transition relation is total
- size or effort: all examples verified in under 10 minutes
- tool: Z3 + implicit rankings (Python tool); written by: automatic tool
- case A:135; source record implicit-rankings-2025
Dijkstra k-State protocol
- guarantee: Implicit rankings with Z3 (verified within 10 minutes) prove Dijkstra’s k-state protocol eventually has a unique privilege and then every machine gets the privilege infinitely often.
- assumes: (b) assumes bot scheduled infinitely often; based on [24],[20]
- size or effort: implicit ranking structure given in Sec 6; no per-example numbers in the arXiv version text
- tool: implicit rankings + Z3 (all verified within 10 minutes); written by: automatic tool
- case A:328; source record implicit-rankings-2025
Dijkstra k-State self-stabilization
- guarantee: Timer reduction and implicit rankings with Z3 prove that Dijkstra’s k-state ring, under any scheduling, eventually reaches a state with exactly one privileged node.
- assumes: any scheduling of privileged nodes; source [28] Lotan, Shoham TACAS 2025
- size or effort: Table 2: 64.8 s, 6, 0, 3, 213 tokens
- tool: timer reduction + implicit rankings, Z3 (mypyvy-style tool); written by: automatic tool
- case A:320; source record timers-2026
First-order infinite-state transition systems (benchmarks from prior work)
- guarantee: An SMT-based method with prophecy timers and implicit ranking functions proves first-order temporal (liveness) properties of infinite-state transition systems without a fairness assumption.
- assumes: no fairness assumption needed (per summary)
- tool: SMT with implicit rankings; written by: automatic tool
- case A:201; source record timers-2026
Formalizing Nakamoto-Style Proof of Stake
- guarantee: A Coq proof shows safety and liveness of a synchronous Proof-of-Stake Nakamoto-style blockchain with a static corruption set, using chain growth, chain quality and common prefix.
- assumes: The model assumes synchrony and a static corruption set; it is a protocol model rather than deployed code.
- size or effort: Safety and liveness jointly implied by three chain properties; Static corrupted parties in a synchronous network
- tool: PoS Nakamoto Coq proof; written by: human
- case C:codex_snowball:35; source record pos-nakamoto-coq-proof-2020
Functional session type calculus
- guarantee: A session-typed functional calculus has an Agda proof of type preservation, session fidelity and relative progress.
- assumes: Linear resources; recursive session types; encoded asynchronous communication
- size or effort: Mechanized Agda development; preservation and progress by construction
- tool: Intrinsically typed Agda CEK machine; written by: human
- case C:codex_snowball:25; source record agda-session-semantics-2019
Ghosh 4-State protocol
- guarantee: Ghosh 4-State protocol stabilizes and is fair; verified within 10 minutes.
- assumes: based on [21]
- size or effort: implicit ranking structure given in Sec 6; no per-example numbers in the arXiv version text
- tool: implicit rankings + Z3 (all verified within 10 minutes); written by: automatic tool
- case A:330; source record implicit-rankings-2025
Heard-Of LastVoting (Paxos-like consensus)
- guarantee: Isabelle/HOL proves the Heard-Of LastVoting (Paxos-like) algorithm terminates, agrees and keeps integrity, if one phase has a coordinator that hears a majority.
- assumes: communication predicate: one phase with a coordinator that hears a majority and is heard by everyone
- size or effort: unknown (AFP session of 9 algorithm theories)
- tool: Isabelle/HOL; written by: human
- case A:189; Debrat and Merz, AFP Heard_Of, LastVotingProof
Hybrid reliable broadcast
- guarantee: Hybrid reliable broadcast: messages are eventually delivered, assuming minimum packet delivery; 137 lines.
- assumes: Minimum guarantee on packet delivery
- size or effort: 137 lines, 8 transitions; 2 derived-variable and 2 bound hints
- tool: LVR (mypyvy); written by: automatic tool
- case A:350; Yao, PhD thesis 2024, Sec. 4.8
hybrid reliable broadcast (HRB)
- guarantee: LVR proves in hybrid reliable broadcast that any correct node eventually accepts a message broadcast by all non-Byzantine nodes, given minimum packet delivery.
- assumes: network protocol, ‘requires some minimum guarantee on packet delivery’
- size or effort: Table 4: 8 transitions, 137 LoC
- tool: LVR (ranking function synthesis, mypyvy, P-FOL-IC3, Z3/CVC4); written by: automatic tool
- case A:333; Yao, Tao, Gu, Nieh, Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions (POPL 2024), Table 3-5
Hybrid reliable broadcast (HRB-Correct)
- guarantee: Hybrid reliable broadcast: if a message was sent to all non-faulty nodes, some obedient node eventually accepts it; checked with timer reduction and Z3 in 135 s.
- assumes: ‘non-faulty nodes that received the initial message eventually send it, and non-faulty nodes that are sent a message eventually receive it’; nodes have 4 failure modes; source [6] Berkovits et al. CAV 2019
- size or effort: Table 2: 135 s, 7, 0, 6, 99 tokens (446 L2S)
- tool: timer reduction + implicit rankings, Z3 (mypyvy-style tool); written by: automatic tool
- case A:310; source record timers-2026
Hybrid reliable broadcast (HRB-Relay)
- guarantee: Z3 with timers and implicit rankings proves that in hybrid reliable broadcast, if some obedient node accepts a message then all non-faulty nodes eventually will.
- assumes: same as HRB-Correct
- size or effort: Table 2: 56 s, 8, 0, 17, 316 tokens (593 L2S)
- tool: timer reduction + implicit rankings, Z3 (mypyvy-style tool); written by: automatic tool
- case A:311; source record timers-2026
Jolteon, pipelined
- guarantee: Coq proves safety of pipelined Jolteon and that it keeps committing.
- assumes: conditional guarantee; see cited paper and liveness note for fairness, timing and fault premises; exact case-specific premises not fully extracted
- tool: liveness; written by: human
- case B:liveness:27; source record refinement
LastVoting-PSync (Dragoi-Henzinger-Zufferey)
- guarantee: LastVoting terminates if eventually a four-round sequence occurs where the coordinator is heard by all and at least n/2 processes are heard in two rounds; formalized in PSync.
- assumes: Paper: link Sure; server PQ-Dur; Each-Learn + bound
- size or effort: proof as stated by authors: Formal (PSync) ; paper’s verdict: ‘assuming primary’
- tool: PSync (logic CL); written by: human
- case A:302; source record what-s-live-2021
Leader election on a unidirectional ring
- guarantee: In Rocq with Ticl, a leader is eventually elected on a unidirectional ring, assuming no network, process or Byzantine failures; 123 lines of definitions and 115 lines of proof.
- assumes: no network, process or Byzantine failures; ring scheduling
- size or effort: 123 lines definitions + 115 lines proof
- tool: Rocq with Ticl (interaction trees); written by: human
- case A:30; source record ticl-2025
Leader Ring (Chang-Roberts)
- guarantee: Implicit rankings with Z3 prove that Chang-Roberts leader ring eventually elects a leader.
- assumes: source [4]
- size or effort: implicit ranking structure given in Sec 6; no per-example numbers in the arXiv version text
- tool: implicit rankings + Z3 (all verified within 10 minutes); written by: automatic tool
- case A:327; source record implicit-rankings-2025
LeaderRing (Chang-Roberts)
- guarantee: LeaderRing (Chang-Roberts): under fair scheduling a leader is eventually elected; checked in 0.3 s.
- assumes: fair scheduling of all nodes; source [8] Chang, Roberts
- size or effort: Table 2: 0.3 s, 8, 1, 4, 76 tokens
- tool: timer reduction + implicit rankings, Z3 (mypyvy-style tool); written by: automatic tool
- case A:318; source record timers-2026
LexArray (Example 5)
- guarantee: A program that decrements an array cell c[i]>0 and sets c[i-1] arbitrarily is proved to terminate using an implicit ranking and Z3 (0.08 s).
- assumes: none
- size or effort: Table 2: 0.08 s, 4, 1, 2, 30 tokens
- tool: timer reduction + implicit rankings, Z3 (mypyvy-style tool); written by: automatic tool
- case A:313; source record timers-2026
Logres, BFT log replication with signatures (lock-step Heard-Of rounds)
- guarantee: In Isabelle/HOL, Logres BFT log replication always produces a new valid log for every correct node, plus Agreement and Completeness, assuming n-f >= f+1 correct nodes and reliable channels; two flaws were found in previous protocols.
- assumes: n - f >= f + 1 correct nodes (A1); reliable channels between correct nodes (A2)
- size or effort: about 300 lines model, 1000 lines proof; two flaws found in previous protocols
- tool: Isabelle/HOL, Heard-Of framework of Debrat and Merz; written by: human
- case A:166; source record logres-2020
LVR sliding window
- guarantee: LVR proves on an abstract model with a synthesized ranking that the sliding window protocol transfers reliably despite loss and reordering.
- assumes: conditional guarantee; see cited paper and liveness note for fairness, timing and fault premises; exact case-specific premises not fully extracted
- tool: liveness; written by: automatic tool
- case B:liveness:39; liveness abstract model, synthesized ranking; LVR Table 3
LVR TLB shootdown
- guarantee: LVR proves on an abstract model with a synthesized ranking that processor translations are eventually updated in TLB shootdown.
- assumes: conditional guarantee; see cited paper and liveness note for fairness, timing and fault premises; exact case-specific premises not fully extracted
- tool: liveness; written by: automatic tool
- case B:liveness:35; liveness abstract model, synthesized ranking; LVR Table 3
Message-passing programs with channels, higher-order session types (GV-style)
- guarantee: In Coq with Iris, LinearActris proves message-passing programs with channels never deadlock or leak, because linearity rules out states where all threads wait on receive; locks and semaphores are not covered.
- assumes: message passing only; no locks, semaphores or monitors
- size or effort: unknown
- tool: Coq + Iris, LinearActris; written by: human
- case A:165; source record linearactris-2024
Modified Mysticeti
- guarantee: Rocq proves safety and liveness of a modified Mysticeti with a repaired round-jumping rule.
- assumes: conditional guarantee; see cited paper and liveness note for fairness, timing and fault premises; exact case-specific premises not fully extracted
- tool: liveness; written by: human
- case B:liveness:31; liveness Rocq model proof; original deployed code only audited separately
multi-Paxos
- guarantee: LVR proves multi-Paxos nodes reach consensus on a growing log, under the usual Paxos assumptions.
- assumes: same Paxos assumptions
- size or effort: Table 4: 10 transitions, 135 LoC
- tool: LVR (ranking function synthesis, mypyvy, P-FOL-IC3, Z3/CVC4); written by: automatic tool
- case A:337; Yao, Tao, Gu, Nieh, Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions (POPL 2024), Table 3-5
Multi-Paxos
- guarantee: Ivy with a manual liveness-to-safety reduction proves every log position in Multi-Paxos is eventually agreed upon, under the same Paxos fairness assumptions.
- assumes: same Paxos fairness assumptions
- size or effort: Fig. 10: 1 level; Cs=10, Ce=13, Cm=32; EPR; 9.0 s
- tool: Ivy (Z3), manual liveness-to-safety reduction + inductive invariant; written by: human
- case A:344; Padon, Hoenicke, Losa, Podelski, Sagiv, Shoham, Reducing Liveness to Safety in First-Order Logic (POPL 2018), Sec 2, Sec 7, Fig. 10
Multi-Paxos / Stoppable Paxos
- guarantee: Multi-Paxos and Stoppable Paxos reach consensus on a growing log; 135 and 160 lines vs 7,869 manual LoC in IronFleet.
- assumes: As for Paxos
- size or effort: multi-Paxos 135 lines, stoppable Paxos 160 lines; manual effort 165 LoC vs 7,869 LoC for IronFleet’s multi-Paxos in Dafny
- tool: LVR (mypyvy); written by: automatic tool
- case A:354; Yao, PhD thesis 2024, Sec. 4.8
Mutex Ring
- guarantee: Mutex Ring: every machine that tries to enter the critical section eventually does; verified within 10 minutes.
- assumes: ♦true unless stated; source [16]
- size or effort: implicit ranking structure given in Sec 6; no per-example numbers in the arXiv version text
- tool: implicit rankings + Z3 (all verified within 10 minutes); written by: automatic tool
- case A:326; source record implicit-rankings-2025
MutexRing
- guarantee: A MutexRing token ring is verified under fair scheduling using implicit rankings and Z3 (0.5 s).
- assumes: fair scheduling; source [16]
- size or effort: Table 2: 0.5 s, 8, 0, 5, 93 tokens
- tool: timer reduction + implicit rankings, Z3 (mypyvy-style tool); written by: automatic tool
- case A:317; source record timers-2026
Nakamoto-style proof of stake
- guarantee: An Isabelle/HOL model of Nakamoto-style proof of stake is mechanized with lemmas on consensus safety and chain growth under synchrony and stake assumptions.
- assumes: protocol synchrony and stake assumptions in model
- size or effort: mechanized model and lemmas
- tool: Isabelle/HOL formalization; written by: human
- case C:codex_snowball:42; Formalizing Nakamoto-Style Proof of Stake
Network control plane routing (fat-tree, Internet2)
- guarantee: CB-Ver (SMT with a Lean-mechanized soundness proof) shows that in network routing (fat-tree, Internet2) router X eventually always has a path to destination D, assuming an unchanged environment and fair schedule.
- assumes: environment unchanged; fair schedule
- size or effort: not extracted; 24 h timeout benchmarks
- tool: SMT + Lean-mechanized soundness (CB-Ver); written by: human
- case A:208; source record cb-ver-2026
Network control planes (reachability, access control, path length)
- guarantee: CB-Ver uses SMT with a Lean soundness proof to show network control planes eventually reach stable properties (reachability, access control, path length) once the environment stops changing.
- assumes: environment stops changing
- tool: CB-Ver (SMT, Lean soundness proof); written by: human
- case A:204; source record cb-ver-2026
One-step consensus abstraction (toy)
- guarantee: In Lean 4 with Veil, a toy one-step consensus eventually chooses some value, assuming weak fairness on choose; about 30 lines.
- assumes: weak fairness on choose
- size or effort: about 30 lines, WF1 rule
- tool: Lean 4 with Veil; written by: human
- case A:38; source record veil-2025
Paxos
- guarantee: Using timer reduction and implicit rankings with Z3, Paxos is shown to eventually have a quorum agree on a value, if proposals stop after some round, a quorum responds and a value is proposed in that round.
- assumes: as in the property; source [32] Padon et al. POPL 2018
- size or effort: Table 2: 101 s, 11 constructors, 1, 20, 238 tokens (521 L2S)
- tool: timer reduction + implicit rankings, Z3 (mypyvy-style tool); written by: automatic tool
- case A:308; source record timers-2026
Paxos
- guarantee: LVR proves that Paxos eventually reaches some consensus, assuming some round r0 has no later contending round and its leader and packets behave.
- assumes: ‘there exists a round r0 which no later round contends with. The leader of round r0 carries out its duty in initializing the round and proposing a value. For any packet that belongs to round r0, if it is sent between the leader and a participant that belongs to a live quorum q0, then it will eventually be delivered.’
- size or effort: Table 4: 9 transitions, 133 LoC, 3 delta corrections
- tool: LVR (ranking function synthesis, mypyvy, P-FOL-IC3, Z3/CVC4); written by: automatic tool
- case A:336; Yao, Tao, Gu, Nieh, Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions (POPL 2024), Table 3-5
Paxos
- guarantee: Ivy with a manual liveness-to-safety reduction proves that Paxos eventually reaches a decision given a node l and a majority of nodes Q whose actions are not interfered with.
- assumes: as quoted
- size or effort: Fig. 10: 1 level; Cs=9, Ce=11, Cm=22; EPR; 8.4 s; Lamport 2006 informal proof ‘about a page’
- tool: Ivy (Z3), manual liveness-to-safety reduction + inductive invariant; written by: human
- case A:343; Padon, Hoenicke, Losa, Podelski, Sagiv, Shoham, Reducing Liveness to Safety in First-Order Logic (POPL 2018), Sec 2, Sec 7, Fig. 10
Paxos-EPR (Padon et al.)
- guarantee: Ivy proves that Paxos eventually reaches a decision given a node l and a majority of nodes Q whose actions are not interfered with.
- assumes: as quoted; paper: link Fair; server PQ-Alw
- size or effort: proof as stated by authors: Formal (Ivy) ; paper’s verdict: ‘Weak from PQ-Alw (Cor 5.1), Each-Vote insufficient (Prop 1)’: Each-Vote is too weak an assertion (Raft can satisfy it forever without reaching consensus)
- tool: Ivy; written by: human
- case A:303; source record what-s-live-2021
Paxos (single-decree)
- guarantee: LVR proves single-decree Paxos eventually reaches a consensus value, given a period of synchrony and a round r0 with no later contention.
- assumes: Period of synchrony; some round r0 that no later round contends with; packets within r0 between the leader and a live quorum eventually delivered
- size or effort: 133 lines, 9 transitions; 3 contradiction hints (e.g. cast_vote cannot fire when two proposals exist in a round); previously 25 extra relations, 143 lines and 40 invariants under Dynamic Abstraction
- tool: LVR (mypyvy); written by: automatic tool
- case A:353; Yao, PhD thesis 2024, Sec. 4.8
Raft (production Mercury platform, joint consensus, leadership transfer, compaction)
- guarantee: Five liveness properties of the Mercury production Raft with joint consensus (e.g. EventuallyConfigCommitted, EventuallyAllLogsConverge) were proved with TLAPS, Coq, Lean 4 and Apalache, removing 26 axioms in 17 active hours.
- assumes: not extracted; unbounded form depends on randomized election timeout
- size or effort: 26 axioms removed in 17 active hours of AI-agent time (author’s claim)
- tool: TLAPS + Coq + Lean 4 + Apalache, PRISM for the randomized-timeout case; written by: unclear
- case A:41; source record federated-formal-verification-2026
ReorderingQueue
- guarantee: Timer reduction and implicit rankings with Z3 prove that in a ReorderingQueue every sent message is eventually received, if each is polled infinitely often.
- assumes: ‘each is polled infinitely often’; source [29]
- size or effort: Table 2: 2.3 s, 9, 2, 11, 220 tokens
- tool: timer reduction + implicit rankings, Z3 (mypyvy-style tool); written by: automatic tool
- case A:316; source record timers-2026
SAT-CDCL
- guarantee: Z3 with timers and implicit rankings proves that SAT-CDCL terminates with SAT or UNSAT.
- assumes: none
- size or effort: Table 2: 5.3 s, 8, 0, 8, 148 tokens
- tool: timer reduction + implicit rankings, Z3 (mypyvy-style tool); written by: automatic tool
- case A:323; source record timers-2026
Scheduler queue (MeQ)
- guarantee: In Rocq with the Ticl logic, an element x in a scheduler queue (MeQ) is shown to be eventually served.
- assumes: loop invariant and ranking function = index of x in queue
- size or effort: 137 lines definitions + 362 lines proof
- tool: Rocq with Ticl; written by: human
- case A:31; source record ticl-2025
Sliding window protocol (IronKV network layer)
- guarantee: LVR proves that the sliding window protocol from IronKV’s network layer eventually delivers data despite drops and reordering, assuming a minimum guarantee on packet delivery.
- assumes: Minimum guarantee on packet delivery
- size or effort: 119 lines; manual effort 128 LoC vs 2,093 LoC in Dafny for IronFleet; 4 tiers
- tool: LVR (mypyvy), reimplementing the IronFleet Dafny spec; written by: automatic tool
- case A:355; Yao, PhD thesis 2024, Sec. 4.8.2
Spinlock, ticket lock, MCS lock clients (weak memory)
- guarantee: Clients of spinlock, ticket lock and MCS lock are proved in Coq to make progress under weak memory models (SC, TSO, RA, StrongCOH) when memory fairness and thread fairness hold.
- assumes: memory fairness in addition to thread fairness; SC, TSO, RA, StrongCOH
- size or effort: not extracted
- tool: Coq (declarative and operational memory fairness); written by: human
- case A:35; source record making-weak-memory-models-2021
Stellar SCP (row 2)
- guarantee: Stellar SCP liveness (under eventual synchrony) was shown with Ivy and Isabelle/HOL: a first-order model plus an interactive proof that the model is sound.
- assumes: not stated in the table ; SoK 2.2: ‘safety and liveness under eventual synchrony’
- size or effort: not given in SoK; see cited paper [27] Losa, Dodds, FMBC 2020
- tool: Ivy, Isabelle/HOL; FO model + interactive proof of model soundness; written by: human
- case A:272; Bondarev, Ziborov, Yanovich, SoK: Formal Verification of Consensus Protocols (arXiv 2608.21935), Table 1 p.7 ; cites [27] Losa, Dodds, FMBC 2020
stoppable Paxos
- guarantee: Stoppable Paxos, a multi-Paxos extension allowing reconfiguration, is verified for liveness; 160 LoC.
- assumes: same Paxos assumptions
- size or effort: Table 4: 11 transitions, 160 LoC
- tool: LVR (ranking function synthesis, mypyvy, P-FOL-IC3, Z3/CVC4); written by: automatic tool
- case A:338; Yao, Tao, Gu, Nieh, Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions (POPL 2024), Table 3-5
Stoppable Paxos
- guarantee: Ivy with a manual liveness-to-safety reduction proves for Stoppable Paxos that for every log position i, either a value is eventually agreed or it stops with a final log shorter than i.
- assumes: same Paxos fairness assumptions
- size or effort: Fig. 10: 1 level; Cs=14, Ce=14, Cm=34; EPR; 9.9 s; ‘first mechanically-checked liveness proof of Stoppable Paxos’; Lamport et al. 2008 informal proof about 3 pages
- tool: Ivy (Z3), manual liveness-to-safety reduction + inductive invariant; written by: automatic tool
- case A:345; Padon, Hoenicke, Losa, Podelski, Sagiv, Shoham, Reducing Liveness to Safety in First-Order Logic (POPL 2018), Sec 2, Sec 7, Fig. 10
Suzuki–Kasami distributed mutual exclusion
- guarantee: Suzuki-Kasami token-passing mutual exclusion was checked so at most one node is in the critical section, with TLA+ model checking and an Ivy inductive proof, and the paper also states a liveness goal that every requesting node eventually enters under token and fairness assumptions.
- assumes: Abstract token-passing model; Ivy uses a restrictive decidable first-order fragment and manual invariant re-expression
- size or effort: TLA+ has one mutex property plus eight supporting invariants; Ivy invariant has five conjuncts
- tool: TLA+ model checking and Ivy inductive verification; written by: human
- case C:codex_grey:1; source record yuen-capstone-2022
Synchronous multiparty session types (global types, projection)
- guarantee: A Rocq proof (about 14K lines, using Paco coinduction) shows that in typed synchronous multiparty sessions every pending send or receive is eventually matched, on fair paths with balanced global types.
- assumes: fair paths; balanced global types
- size or effort: about 14K lines Rocq
- tool: Rocq (Paco coinduction); written by: human
- case A:32; Formally Verified Liveness with Multiparty Session Types in Rocq (ITP 2026) abstract, s.5
Tendermint (row 1)
- guarantee: The SoK lists a PAT/CSP# process-algebra analysis of Tendermint liveness (the label may be a mismatch with the cited proof-of-stake paper).
- assumes: not stated in the table ; SoK cites [30] which is titled ‘Formal analysis of a proof-of-stake blockchain’; the row label ‘Tendermint’ may be a mismatch
- size or effort: not given in SoK; see cited paper [30] Maung Maung Thin et al., ICECCS 2018
- tool: PAT; CSP# process algebra; written by: human
- case A:232; Bondarev, Ziborov, Yanovich, SoK: Formal Verification of Consensus Protocols (arXiv 2608.21935), Table 1 p.7 ; cites [30] Maung Maung Thin et al., ICECCS 2018
Ticket lock
- guarantee: LVR proves that every waiting client of a ticket lock eventually enters, assuming every client is scheduled infinitely often.
- assumes: every client scheduled infinitely often; bounded critical-section steps
- tool: LVR; written by: automatic tool
- case A:155; Yao et al., LVR, POPL 2024
ticket lock
- guarantee: LVR proves for a ticket lock that any waiting client eventually enters the critical section, assuming every client is scheduled infinitely often and the critical section is left after finitely many steps.
- assumes: ‘Every client is scheduled infinitely often.’ (Eq. 2: ∀C: client. □(♢scheduled(C))); ‘Any client in the critical section can only execute a finite number of steps before leaving.’ (Eq. 3)
- size or effort: Table 4: 5 transitions, 68 LoC; Table 5 phases: static 0.02, bound 48.3, contradiction 127.5, delta 0.57 s, synthesis 0.21, validate 0.56, good-end 0.43 s, no-deadlock 117.4 (seconds unless marked)
- tool: LVR (ranking function synthesis, mypyvy, P-FOL-IC3, Z3/CVC4); written by: automatic tool
- case A:332; Yao, Tao, Gu, Nieh, Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions (POPL 2024), Table 3-5
Ticket lock
- guarantee: LVR proves in a ticket lock that any waiting client eventually enters the critical section, under fair scheduling.
- assumes: Fair scheduling; finite execution in the critical section
- size or effort: 68-line protocol, 5 transitions; hints: 1 declared and 1 derived-variable, 2 bound corrections, 0 contradictions, 0 deltas, 0 tiers (Table 4.4); invariants mostly automatic
- tool: LVR (mypyvy + Z3 + P-FOL-IC3); written by: automatic tool
- case A:349; Yao, PhD thesis 2024, Sec. 4.8, Tables 4.3-4.5
Ticket protocol
- guarantee: Ivy with a manual liveness-to-safety reduction proves every thread that requests the ticket protocol’s critical section eventually enters, if all threads are scheduled infinitely often.
- assumes: ‘all the threads are scheduled infinitely often’: ∀x: thread. □♢scheduled(x); spec = fairness implies liveness
- size or effort: Fig. 10: 1 nesting level; conjectures Cs=15, Ce=3, Cm=19; EPR; 3.7 s
- tool: Ivy (Z3), manual liveness-to-safety reduction + inductive invariant; written by: human
- case A:340; Padon, Hoenicke, Losa, Podelski, Sagiv, Shoham, Reducing Liveness to Safety in First-Order Logic (POPL 2018), Sec 2, Sec 7, Fig. 10
Ticket protocol, Paxos, alternating bit protocol, Hybrid Reliable Broadcast, ring mutex, ring leader election, Dijkstra k-state, queues
- guarantee: Z3 with prophecy timers and implicit rankings proves eventual properties such as that, given a maximal round and a responsive quorum, a Paxos quorum eventually agrees on the proposed value, and that the alternating bit protocol delivers all data.
- assumes: Paxos: maximal round, responsive quorum; ABP: weak fairness of channels; HRB: eventual send/receive by non-faulty nodes; timer reduction needs no fairness
- size or effort: user-supplied rankings and invariants; proof size in tokens vs Ivy liveness-to-safety
- tool: SMT (Z3) with prophecy timers and implicit rankings (Python tool); written by: automatic tool
- case A:207; source record timers-2026
Ticket protocol (Sec 2)
- guarantee: Z3 with timers and implicit rankings proves that in the ticket protocol, if every thread is scheduled infinitely often, every waiting thread eventually enters the critical section.
- assumes: ‘under fair scheduling, every thread that waits to enter the critical section, eventually does so’; fairness is the antecedent □♢scheduled(x) for each x
- size or effort: Table 2: 2 s, 6 constructors, 2 inductively-finite approx., 20 invariant conjuncts, 256 tokens (407 tokens for the Ivy liveness-to-safety proof)
- tool: timer reduction + implicit rankings, Z3 (mypyvy-style tool); written by: automatic tool
- case A:307; source record timers-2026
TimestampedQueue
- guarantee: TimestampedQueue: any sent message is eventually received, assuming the queue is polled infinitely often; checked in 0.5 s.
- assumes: ‘a fairness assumption that the queue is polled infinitely often’; source [29] McMillan CAV 2024
- size or effort: Table 2: 0.5 s, 6, 1, 2, 73 tokens
- tool: timer reduction + implicit rankings, Z3 (mypyvy-style tool); written by: automatic tool
- case A:314; source record timers-2026
TLA+ specs from GitHub translated to Verus
- guarantee: An LLM prover/reviewer proved in Verus, using the Anvil temporal library, safety and liveness (P ~> Q) properties of TLA+ specs from GitHub, at about $1.7 t o$ 2.1 per proof.
- assumes: fairness assumptions in the TLA+ spec; some properties need added assumptions; no refinement to code
- size or effort: 3,094 algorithmic + 492 agentic proofs; about $1.7 t o$ 2.1 per proof
- tool: Verus (Anvil temporal library) + LLM prover/reviewer; written by: agent
- case A:12; source record tla-verus-2026
TLAPS SimpleEventually (x,y,flip)
- guarantee: TLAPS proves a simple spec with fairness (WF_vars(Next)) eventually sets x to TRUE; 73-line file.
- assumes: WF_vars(Next)
- size or effort: 73-line file
- tool: TLAPS; written by: human
- case A:186; tlapm/examples/SimpleEventually.tla
TLB shootdown
- guarantee: LVR proves that after a shared-memory write each processor eventually updates its TLB correctly, assuming scheduling and lock fairness.
- assumes: ‘requires scheduling and lock fairness’
- size or effort: Table 4: 27 transitions, 361 LoC, 3 delta corrections, tier 4
- tool: LVR (ranking function synthesis, mypyvy, P-FOL-IC3, Z3/CVC4); written by: automatic tool
- case A:335; Yao, Tao, Gu, Nieh, Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions (POPL 2024), Table 3-5
TLB shootdown
- guarantee: LVR (mypyvy) proves that after a shared-memory write each processor eventually updates its TLB correctly, assuming scheduling and lock fairness.
- assumes: Scheduling and lock fairness
- size or effort: 361 lines, 27 transitions; hints include 3 contradictions and 4 tiers; one invariant found manually (took hours)
- tool: LVR (mypyvy); written by: automatic tool
- case A:352; Yao, PhD thesis 2024, Sec. 4.8, Table 4.4
TLB shootdown (Mach)
- guarantee: Mach TLB shootdown: each processor infinitely often runs the main or responder loop, so loop bodies terminate; proved in Ivy in 219 s, said to be the first mechanical liveness proof.
- assumes: ‘strong fairness assumptions for the page table lock’; spin-locks used to expose deadlock; 24 program locations; sound for unbounded processors
- size or effort: Fig. 10: 3 nesting levels; Cs=22, Ce=9, Cm=60; general FO (not EPR); 219 s; ‘first to mechanically prove its liveness’
- tool: Ivy (Z3), manual liveness-to-safety reduction + inductive invariant; written by: human
- case A:342; Padon, Hoenicke, Losa, Podelski, Sagiv, Shoham, Reducing Liveness to Safety in First-Order Logic (POPL 2018), Sec 2, Sec 7, Fig. 10
Toy Stabilization (Example 1)
- guarantee: Implicit rankings with Z3 verified within 10 minutes that in a toy stabilization ring machine bot is eventually scheduled, with no fairness assumption.
- assumes: no fairness assumption; ♦true used as fairness (totality of transition relation); ring, one privileged machine scheduled each step
- size or effort: implicit ranking structure given in Sec 6; no per-example numbers in the arXiv version text
- tool: implicit rankings + Z3 (all verified within 10 minutes); written by: automatic tool
- case A:324; source record implicit-rankings-2025
ToyStabilization
- guarantee: Z3 with timers and implicit rankings proves that in ToyStabilization any node is eventually scheduled.
- assumes: none stated; simplified Dijkstra k-state privilege movement
- size or effort: Table 2: 0.3 s, 5, 0, 3, 69 tokens
- tool: timer reduction + implicit rankings, Z3 (mypyvy-style tool); written by: automatic tool
- case A:319; source record timers-2026
Wirehead distributed double buffer (Python+MongoDB) as Rocq state machine
- guarantee: In the Rocq model of Wirehead, once a process starts a swap it is proved to eventually finish it, under weak fairness.
- assumes: Single MongoDB instance; crash-stop (no partitions, no Byzantine); each MongoDB call atomic; weak fairness for liveness; model written by hand from the Python code, link to real code not proved
- size or effort: Seven chained uses of fairness, one per swap sub-step; fully checked; Liveness.v 1,342 lines total (48 lemmas, 2 theorems)
- tool: Rocq proof assistant, written by hand; written by: human
- case C:r7:4; Doan thesis, Sec 6.1-6.2, Table 6.1
Wirehead distributed double buffer (Python+MongoDB) as Rocq state machine
- guarantee: In the Rocq model of Wirehead, if the write buffer is full and a process tries to swap, a swap is proved to eventually complete, so lock contention cannot deadlock.
- assumes: Single MongoDB instance; crash-stop (no partitions, no Byzantine); each MongoDB call atomic; weak fairness for liveness; model written by hand from the Python code, link to real code not proved
- size or effort: Case split on lock free/held; fully checked
- tool: Rocq proof assistant, written by hand; written by: human
- case C:r7:5; Doan thesis, Sec 6.1-6.2, Table 6.1
Xen vchan inter-VM channel
- guarantee: Xen vchan: data reported sent is eventually received, in a TLA+ model checked with TLC and TLAPS, assuming weak fairness on the receiver read and clean shutdown.
- assumes: weak fairness on receiver read; clean shutdown; first version vacuously true when sender blocks forever
- size or effort: blog; not extracted
- tool: TLA+ / TLC / TLAPS; written by: human
- case A:37; T. Leonard, Proving liveness with TLA (2026)
yes-no program; non-deterministic Nat; Even-Odd counter
- guarantee: Coq with Fairis proves fair termination of a yes-no program and that a nondeterministic counter visits all naturals in order.
- assumes: fair scheduling over model roles
- size or effort: unknown
- tool: Coq, Fairis; written by: human
- case A:181; source record trillium-2024

checked by a model checker on a bounded or finite instance

39 cases.

Asterinas Mutex (SysMoBench task)
- guarantee: LLMs wrote a TLA+ model of the Asterinas mutex (186 lines Rust, 219 lines TLA+), checked by TLC for mutex invariants; conformance was 100/100/66.67/66.67% across four LLMs.
- assumes: Source Rust; LLM writes the model; invariants written by benchmark authors; best of 5 runs; 3 feedback rounds
- size or effort: Basic agent: all 100% syntax and runtime; conformance 100/100/66.67/66.67%; 186 lines Rust, 219 lines TLA+
- tool: TLA+ / TLC model checker, SANY, trace validation; written by: agent
- case C:r4:7; source record sysmobench-2026
Asterinas Ringbuffer (SysMoBench task)
- guarantee: LLMs wrote a TLA+ model of the Asterinas ring buffer (615 lines Rust); only Claude ran, with 100% conformance and invariants, while GPT-5, Gemini and DeepSeek failed at runtime.
- assumes: Source Rust; LLM writes the model; invariants written by benchmark authors; best of 5 runs; 3 feedback rounds
- size or effort: Basic agent: only Claude ran (100% conformance and invariants); GPT-5, Gemini, DeepSeek failed runtime; 615 lines Rust, 123 lines TLA+
- tool: TLA+ / TLC model checker, SANY, trace validation; written by: agent
- case C:r4:9; source record sysmobench-2026
Asterinas Rwmutex (SysMoBench task)
- guarantee: LLMs wrote a TLA+ model of the Asterinas read-write mutex (395 lines Rust, 250 lines TLA+), checked by TLC for its invariants; conformance was 100/75/0/50%.
- assumes: Source Rust; LLM writes the model; invariants written by benchmark authors; best of 5 runs; 3 feedback rounds
- size or effort: Basic agent: conformance 100/75/0/50%; invariants 90/80/80/90%; 395 lines Rust, 250 lines TLA+
- tool: TLA+ / TLC model checker, SANY, trace validation; written by: agent
- case C:r4:8; source record sysmobench-2026
Asterinas Spinlock (SysMoBench task)
- guarantee: LLMs wrote a TLA+ model of the Asterinas spinlock code, checked by TLC for mutual exclusion, lock consistency, no deadlock, guard lifecycle and eventual release; conformance to the code was 100/80/80/80% across four LLMs.
- assumes: Source Rust; LLM writes the model; invariants written by benchmark authors; best of 5 runs; 3 feedback rounds
- size or effort: Basic agent: all four LLMs 100% syntax and runtime; conformance 100/80/80/80%; invariants 100/100/85.71/100% (Claude/GPT-5/Gemini/DeepSeek); 213 lines Rust, 151 lines TLA+
- tool: TLA+ / TLC model checker, SANY, trace validation; written by: agent
- case C:r4:6; source record sysmobench-2026
Azure Cosmos DB consistency levels
- guarantee: Azure Cosmos DB 4 consistency levels were specified in TLA+ with 10 liveness and 14 safety properties, checked with TLC on logs up to length 6 plus random simulation, in 2 person-months.
- assumes: bounded: logs up to length 6 plus random simulation
- size or effort: 2 person-months
- tool: TLA+; written by: human
- case A:157; Hackett et al., ICSE-SEIP 2023
Bitdefender-style endpoint decision pipeline (primary/legacy/local fallback), Promela model
- guarantee: In the Promela pipeline model, every scan eventually reaches its single terminal commit point; SPIN found zero errors over 5,659 states.
- assumes: Reliable transport; untimed deadlines; servers always correct (A1); reduced scan never flags benign (A2); 1 endpoint, 1 scan core model (also streaming and 2-endpoint models)
- size or effort: 5,659 states stored, under 1 s on the core model; zero errors; also zero errors on streaming (314,527 states) and concurrent (22,177,616 states) models
- tool: SPIN, LTL; written by: human
- case C:K:14; Aldea and Prelipcean 2026, Sec 6, Tables 2 and 4
Byzantine consensus TLA+ model
- guarantee: Apalache checks agreement safety and liveness of a Byzantine consensus TLA+ model with n=6, t=1, f=1, up to round bound 10 in 1 min 24 s after abstraction, with 13 lemmas that took about 15 h to discover.
- assumes: n=6 participants, t=1 tolerated and f=1 actual faulty participant; bounded rounds or supplied inductive invariant
- size or effort: 13 lemmas took ~15 h to discover; bound-10 check 1 min 24 s after abstraction
- tool: Apalache; written by: human
- case C:codex_snowball:14; source record apalache-2026
ChonkyBFT
- guarantee: ChonkyBFT liveness was checked with Quint and Apalache symbolic bounded model checking, per SoK Table 1.
- assumes: not stated in the table
- size or effort: not given in SoK; see cited paper [17] Franca et al., 2025
- tool: Quint, Apalache; symbolic BMC; written by: human
- case A:249; Bondarev, Ziborov, Yanovich, SoK: Formal Verification of Consensus Protocols (arXiv 2608.21935), Table 1 p.7 ; cites [17] Franca et al., 2025
Consensus algorithms, over 30 (Paxos, Multi-Paxos, EPaxos, Zab, Raft, PBFT variants, Chubby)
- guarantee: Liveness properties of over 30 consensus algorithms were compared in one formal language and TLA+; the work found EPaxos’s assumption too weak and Zab, Paxos-EPR and Chubby-Live too strong; TLC checked Paxos up to 4 proposers and 4 acceptors.
- assumes: hierarchy of assumptions (Alw-Q, PQ-Alw, Alw, Fair) and assertions
- size or effort: TLC on Paxos up to 4 proposers and 4 acceptors in a few hours
- tool: high-level specification language, TLA+/TLC; written by: human
- case A:42; source record what-s-live-2021
consensus - synthesis from sketch
- guarantee: PolySemist completes a consensus protocol sketch so that the result satisfies the given TLA+ safety/liveness property, checked by TLC on fixed small node counts.
- assumes: human-written sketch and property; fixed small node counts; consensus protocol sketch
- size or effort: easiest: all pre- or post-conditions of one action missing; hardest: all of two actions; DL fully from scratch 125 s; overall 160/171 faster than Scythe
- tool: PolySemist (CEGIS + TLC model checker); written by: automatic tool
- case C:K:34; source record polysemist-2025
Datadog Courier message queue
- guarantee: TLC checks in the Datadog Courier message queue model that, under weak fairness, eventually no messages are lost: all are processed or in the dead-letter queue.
- assumes: weak fairness WF_vars on handlers, sequencer and healthcheck actions
- size or effort: first model: 5,515,710 distinct states, no violation; adding a sequencer produced a violation trace
- tool: TLA+ / TLC; written by: human
- case A:139; Datadog blog ‘How We Use Formal Modeling…’
DCCP handshake model
- guarantee: In a SPIN model of the DCCP handshake, the RFC’s correctness properties hold, and no attacker can violate looping-behavior properties theta1 and theta3.
- assumes: Finite model
- size or effort: seconds
- tool: SPIN (LTL); written by: human
- case C:r1:5; Von Hippel thesis Sec. 4.8, 5.6
decentralized lock (DL) - synthesis from sketch
- guarantee: PolySemist completes a decentralized lock sketch so that the result satisfies the given TLA+ safety/liveness property, checked by TLC on fixed small node counts; full synthesis from scratch took 125 s.
- assumes: human-written sketch and property; fixed small node counts; simple decentralized lock
- size or effort: easiest: all pre- or post-conditions of one action missing; hardest: all of two actions; DL fully from scratch 125 s; overall 160/171 faster than Scythe
- tool: PolySemist (CEGIS + TLC model checker); written by: automatic tool
- case C:K:35; source record polysemist-2025
Etcd Raft (SysMoBench task)
- guarantee: LLMs wrote a TLA+ model of etcd Raft’s Go code checked for Raft safety and liveness invariants; only Claude reached conformance (7.69%) and invariants (69.23%) with the basic agent.
- assumes: Source Go; LLM writes the model; invariants written by benchmark authors; best of 5 runs; 3 feedback rounds
- size or effort: Basic agent: only Claude reached conformance (7.69%) and invariants (69.23%); code-translation agent: Claude 15.38% conformance, 92.31% invariants; 2,159 lines Go, 385 lines TLA+
- tool: TLA+ / TLC model checker, SANY, trace validation; written by: agent
- case C:r4:10; source record sysmobench-2026
Fizzbee example status machine (idle/working/failed/shutdown)
- guarantee: FizzBee model checking of a toy status machine checks that status always eventually returns to shutdown and to working, and that a failed state is reachable, assuming weak fairness on some actions.
- assumes: Weak fairness on Start/Finish/Fix/Restart; Shutdown and Fail not fair
- size or effort: toy model, model checked
- tool: FizzBee; written by: human
- case A:365; source record fizzbee-2024
Go-Back-N over token bucket filters
- guarantee: Go-Back-N over token bucket filters can reach perfect efficiency, with a formula for efficiency when the sender over-transmits, proved in ACL2s.
- assumes: Non-probabilistic model, no reordering
- size or effort: not stated in the sections read
- tool: ACL2s (bisimulation, invariants); written by: human
- case C:r1:3; Von Hippel thesis Sec. 3.10
Korg attacker synthesis on TCP/DCCP/SCTP handshakes
- guarantee: Korg checks whether an off-path, evil-server or on-path attacker can break each TCP, DCCP and SCTP handshake property, and outputs the attack where one exists; TCP phi3 took 72-223 min.
- assumes: Centralized single attacker; model fidelity
- size or effort: TCP phi3 72-223 min, others seconds; up to 10 attacks per property
- tool: Korg (LTL model checking via SPIN); written by: automatic tool
- case C:r1:7; Von Hippel thesis Table 5.1, 5.3
lock server (LS) - synthesis from sketch
- guarantee: PolySemist completes a lock server sketch so that the result satisfies the given TLA+ safety/liveness property, checked by TLC on fixed small node counts.
- assumes: human-written sketch and property; fixed small node counts; lock server
- size or effort: easiest: all pre- or post-conditions of one action missing; hardest: all of two actions; DL fully from scratch 125 s; overall 160/171 faster than Scythe
- tool: PolySemist (CEGIS + TLC model checker); written by: automatic tool
- case C:K:36; source record polysemist-2025
Maeslant Barrier BesW control software
- guarantee: For the Maeslant Barrier control software, 40 requirements (e.g. Open Door finishes iff at least two limit switches show open; Move Out never trims; spring set to K2 when wall slit is below 3.5 m) were checked in mCRL2 on a 5,000-line model with 4.98e14 states, each under 40 min.
- assumes: Discretised water levels; not all pump/valve fault combinations; model confidential
- size or effort: 5,000-line model, 4.98e14 states, each property under 40 min
- tool: mCRL2, modal mu-calculus; written by: human
- case C:r1:31; Maeslant paper Sec. 5-6
(paper’s own) TLA+ liveness specs
- guarantee: The paper’s own TLA+ liveness specs were model checked on single-value Paxos up to 4 proposers and 4 acceptors.
- assumes: stable duration start; leader election started at it
- size or effort: proof as stated by authors: model checking, up to 4 proposers and 4 acceptors in a few hours ; paper’s verdict: not applicable (illustration)
- tool: TLA+/TLC; written by: human
- case A:306; source record what-s-live-2021
Parameterized threshold-guarded fault-tolerant algorithms
- guarantee: ByMC checks safety and LTL liveness of threshold-guarded fault-tolerant algorithms for all parameter values by finding that no short counterexample exists, on 10 algorithms.
- assumes: Parameterized process count and fault fraction; threshold guards; LTL fragment
- size or effort: 10 prominent algorithms checked; counterexample length independent of parameters
- tool: ByMC with short-counterexample reduction; written by: automatic tool
- case C:codex_snowball:12; source record short-counterexample-ftda-2016
PGo CRDT
- guarantee: PGo CRDT was checked by TLC on a bounded instance for convergence and termination, plus compilation (10 person-days, 160 MPCal SLOC).
- assumes: paper checked configuration; compiler/glue/runtime/environment resources trusted; liveness scheduler assumptions need deployment justification
- size or effort: Table 2: 10 person-days; 160 MPCal SLOC; 185 glue Go SLOC
- tool: TLC bounded-instance model checking + compilation to Go; written by: human
- case B:systems:48; source record pgo-2023
PGo dqueue (SysMoBench task)
- guarantee: LLMs wrote a TLA+ model of the PGo-generated Go distributed queue (175 lines Go), checked for its invariants; all four LLMs got 100% runtime and invariants but 0% conformance.
- assumes: Source Go (compiler-generated); LLM writes the model; invariants written by benchmark authors; best of 5 runs; 3 feedback rounds
- size or effort: Code-translation: all four LLMs 100% runtime, 0% conformance, 100% invariants; 175 lines Go, 75 lines TLA+
- tool: TLA+ / TLC model checker, SANY, trace validation; written by: agent
- case C:r4:14; source record sysmobench-2026
PGo Lock service
- guarantee: TLC model checks the PGo lock service for mutual exclusion and liveness in the paper’s checked configuration, with the compiled code not covered by that check.
- assumes: paper checked configuration; compiler/glue/runtime/environment resources trusted; liveness scheduler assumptions need deployment justification
- size or effort: Table 2: 2 person-days; 67 MPCal SLOC; 87 glue Go SLOC
- tool: TLC bounded-instance model checking + compilation to Go; written by: human
- case B:systems:46; source record pgo-2023
PGo locksvc (SysMoBench task)
- guarantee: LLMs wrote a TLA+ model of the PGo-generated Go lock server (281 lines Go), checked for its invariants; Claude passed 83.33%, GPT-5 66.67%, DeepSeek 50%, all with 0% conformance.
- assumes: Source Go (compiler-generated); LLM writes the model; invariants written by benchmark authors; best of 5 runs; 3 feedback rounds
- size or effort: Code-translation: Claude 83.33%, GPT-5 66.67%, DeepSeek 50% invariants, 0% conformance; 281 lines Go, 93 lines TLA+
- tool: TLA+ / TLC model checker, SANY, trace validation; written by: agent
- case C:r4:15; source record sysmobench-2026
PGo raftkvs (SysMoBench task)
- guarantee: LLMs wrote a TLA+ model of the PGo-generated Go Raft key-value store (3,163 lines Go), checked for its invariants; Claude got 50% runtime, 0% conformance and 90.91% invariants.
- assumes: Source Go (compiler-generated); LLM writes the model; invariants written by benchmark authors; best of 5 runs; 3 feedback rounds
- size or effort: Code-translation: Claude 50% runtime, 0% conformance, 90.91% invariants; 3,163 lines Go, 508 lines TLA+
- tool: TLA+ / TLC model checker, SANY, trace validation; written by: agent
- case C:r4:16; source record sysmobench-2026
Raft election (mCRL2 model)
- guarantee: In an mCRL2 model of Raft election, weak liveness holds (a leader can be elected), but ‘a leader must always eventually be elected’ fails when messages are lost or nodes crash.
- assumes: message loss and crashes allowed
- tool: mCRL2; written by: human
- case A:176; source record modelling-the-raft-distributed-2024
reconfigurable Raft (RR, RR-big) - synthesis from sketch
- guarantee: PolySemist completes two reconfigurable Raft sketches (RR, RR-big) so that the result satisfies the given TLA+ safety/liveness property, checked by TLC on fixed small node counts.
- assumes: human-written sketch and property; fixed small node counts; two reconfigurable Raft sketches from prior work
- size or effort: easiest: all pre- or post-conditions of one action missing; hardest: all of two actions; DL fully from scratch 125 s; overall 160/171 faster than Scythe
- tool: PolySemist (CEGIS + TLC model checker); written by: automatic tool
- case C:K:38; source record polysemist-2025
Red Belly
- guarantee: Red Belly liveness is checked with ByMC on parametric threshold automata, assuming a round-rigid adversary.
- assumes: not stated in the table ; SoK 2.2: ‘round-rigid adversary assumption … to guarantee fair scheduling of transitions and termination’
- size or effort: not given in SoK; see cited paper [37] Tholoniat, Gramoli, 2019
- tool: ByMC; parametric threshold automata; written by: human
- case A:246; Bondarev, Ziborov, Yanovich, SoK: Formal Verification of Consensus Protocols (arXiv 2608.21935), Table 1 p.7 ; cites [37] Tholoniat, Gramoli, 2019
Redis Raft (SysMoBench task)
- guarantee: LLMs wrote a TLA+ model of Redis Raft’s C code (2,394 lines) checked for Raft invariants including linearizability; no basic-agent model ran, and the best code-translation result was Claude with 9.09% conformance and 75% invariants.
- assumes: Source C; LLM writes the model; invariants written by benchmark authors; best of 5 runs; 3 feedback rounds
- size or effort: Basic agent: no model ran; code-translation Claude 23.81% runtime, 9.09% conformance, 75% invariants; 2,394 lines C, 349 lines TLA+
- tool: TLA+ / TLC model checker, SANY, trace validation; written by: agent
- case C:r4:11; source record sysmobench-2026
SCTP handshake model
- guarantee: In a SPIN model of the SCTP handshake, ten properties hold, e.g. half-open states eventually end (gamma2) and teardown from Shutdown_Ack_Sent ends in Closed (gamma3).
- assumes: Finite model; vtag and itag compressed
- size or effort: seconds to hours per attacker check
- tool: SPIN (LTL); written by: human
- case C:r1:6; Von Hippel thesis Sec. 4.10
sharded key-value store (SKV) - synthesis from sketch
- guarantee: PolySemist completes a sharded key-value store sketch so that the result satisfies the given TLA+ safety/liveness property, checked by TLC on fixed small node counts.
- assumes: human-written sketch and property; fixed small node counts; sharded KV store
- size or effort: easiest: all pre- or post-conditions of one action missing; hardest: all of two actions; DL fully from scratch 125 s; overall 160/171 faster than Scythe
- tool: PolySemist (CEGIS + TLC model checker); written by: automatic tool
- case C:K:37; source record polysemist-2025
Stellar SCP (row 1)
- guarantee: Stellar SCP liveness is checked in UPPAAL with timed automata.
- assumes: not stated in the table ; SoK 2.2: timer abstractions
- size or effort: not given in SoK; see cited paper [42] Yoo et al., IWBOSE 2019
- tool: UPPAAL; timed automata; written by: human
- case A:270; Bondarev, Ziborov, Yanovich, SoK: Formal Verification of Consensus Protocols (arXiv 2608.21935), Table 1 p.7 ; cites [42] Yoo et al., IWBOSE 2019
TCP handshake (RFC 9293 model)
- guarantee: In a SPIN model of the TCP handshake from RFC 9293, there is no half-open connection, establishment eventually succeeds, peers never get stuck, and Syn_Received eventually leads to Established.
- assumes: No crashes modelled; small finite model
- size or effort: seconds to check
- tool: SPIN (LTL); written by: human
- case C:r1:4; Von Hippel thesis Sec. 4.6
two-phase commit (2PC) - synthesis from sketch
- guarantee: PolySemist completes a human-written two-phase commit sketch so that the result satisfies the given TLA+ safety/liveness property, checked by TLC on fixed small node counts.
- assumes: human-written sketch and property; fixed small node counts; atomic commit sketch with pre- or post-conditions removed from 1-2 actions
- size or effort: easiest: all pre- or post-conditions of one action missing; hardest: all of two actions; DL fully from scratch 125 s; overall 160/171 faster than Scythe
- tool: PolySemist (CEGIS + TLC model checker); written by: automatic tool
- case C:K:33; source record polysemist-2025
Two-thread mutex example (verus-tla export)
- guarantee: A two-thread mutex example written in Verus was exported to TLA+ and TLC checked that both threads eventually terminate under weak fairness, over 8 states (a model check, not a proof).
- assumes: weak fairness in Spec
- size or effort: 8 states checked
- tool: Verus code exported to TLA+ and checked by TLC (model check, not proof); written by: automatic tool
- case A:40; BasisResearch/verus PR #51
Verification of randomized consensus algorithms under round-rigid adversaries
- guarantee: Randomized consensus algorithms Ben-Or, Bracha, 2-set agreement and RS-Bosco are automatically verified with round-rigid adversaries, which reduce the problem to one-round model checking, including almost-sure termination.
- assumes: Round-rigid schedules/adversaries are the fairness abstraction; probabilistic claims are model-specific.
- size or effort: Automatically verifies Ben-Or, Bracha, 2-set agreement and RS-Bosco; Handles crashes and Byzantine faults
- tool: Randomized threshold consensus; written by: automatic tool
- case C:codex_snowball:38; source record randomized-threshold-consensus-2021
Xline CURP (SysMoBench task)
- guarantee: LLMs wrote a TLA+ model of Xline’s CURP replication Rust code (4,064 lines), checked for CURP invariants; with code translation Claude reached 50% and Gemini 66.67% conformance, both 100% invariants.
- assumes: Source Rust; LLM writes the model; invariants written by benchmark authors; best of 5 runs; 3 feedback rounds
- size or effort: Basic agent: none ran; code-translation Claude 50% conformance, Gemini 66.67%, both 100% invariants; 4,064 lines Rust, 100 lines TLA+
- tool: TLA+ / TLC model checker, SANY, trace validation; written by: agent
- case C:r4:12; source record sysmobench-2026
ZENITH SDN controller (microservices)
- guarantee: For the ZENITH SDN controller (8.6K-line spec), TLC and hand TLAPS proofs check that switch routing state eventually matches the intended DAG and apps eventually see consistent network state (P1-P8).
- assumes: modelled failures; switch behavior assumption; history variables used because TLAPS cannot prove some temporal properties directly
- size or effort: spec 8.6K lines
- tool: TLA+/PlusCal, TLC, TLAPS hand proof; code generated from spec; written by: human
- case A:209; source record zenith-2025

liveness bugs, failed attempts, and attacks

15 cases.

etcd/raft (Go, 16k lines; 120 lines of shim)
- guarantee: A Netrix test reproduced a known etcd/raft liveness bug: with leader 1 linked only to replica 2 and replica 5 isolated, no new leader is elected; hit in 15/100 iterations.
- assumes: Bounded liveness: success state means repeated election attempts observed; bug present with Prevote and CheckQuorum off
- size or effort: 5 filters, 3 states, 64 lines; hit in 15/100 iterations
- tool: Netrix DSL testing tool (filters + state-machine monitor, PCTCP random exploration); written by: human
- case C:r8:18; Netrix Sec. 5.3, Tab. 3
Look-aside cache loss (web app, memcached-style cache, database)
- guarantee: After a look-aside cache is lost, the database’s hidden 300 QPS capacity (versus 3,000 QPS advertised) can stop the cache from refilling and goodput from recovering; shown by informal analysis, no proof.
- assumes: 90% hit rate; app fills the cache; database 300 QPS limit
- size or effort: no proof; hidden capacity 300 QPS vs advertised 3,000 QPS
- tool: none (informal analysis); written by: human
- case C:r10:38; source record metastable-failures-2021
MongoDB RaftMongo replication (commit point)
- guarantee: For MongoDB RaftMongo replication, the aim was no committed write lost and all servers eventually learning the newest commit point, but trace checking of the C++ server failed: ‘Our traces never matched our specification’.
- size or effort: trace checking failed: ‘Our traces never matched our specification’; one month to instrument state snapshots
- tool: TLA+ / TLC with trace checking of the C++ server; written by: human
- case A:140; MongoDB blog ‘Conformance Checking at MongoDB’
Mysticeti (Sui, IOTA) DAG consensus
- guarantee: In Rocq under LiDO-DAG, Mysticeti (Sui, IOTA) was shown to commit leader vertices within bounded time; a counterexample was found with unrestricted round-jumping and fixed with a restriction.
- assumes: partial synchrony; Byzantine f of 3f+1
- size or effort: not extracted
- tool: Rocq under LiDO-DAG; written by: human
- case A:212; Mechanized Safety and Liveness Proofs for Mysticeti, Abstract and Sec 2
Paxos-Complex (Paxos Made Moderately Complex)
- guarantee: Paxos Made Moderately Complex: a client broadcasting a command eventually gets a response, but the survey says this fails because a command can be re-proposed on a new slot forever.
- assumes: ‘the clock drift of a process … is within some [bounded] factor of the rate of real time’; message time ‘is [bounded]’; authors say it weakens to fair links. Paper: link Fair; no server assumption stated
- size or effort: proof as stated by authors: none ; paper’s verdict: ‘lacking assumptions, Not Resp (Prop 6)’: Resp fails even with Alw, a command can be re-proposed on a new slot forever
- tool: paper-only (no machine proof); written by: human
- case A:298; source record what-s-live-2021
Paxos for System Builders pseudocode
- guarantee: An executable DistAlgo spec of Paxos for System Builders found liveness bugs in the original pseudocode by testing, with no proof.
- tool: DistAlgo (testing, no proof); written by: human
- case A:203; source record paxos-sb-in-distalgo-2026
Paxos for System Builders pseudocode in DistAlgo
- guarantee: An executable DistAlgo spec of the Paxos for System Builders pseudocode found omissions and liveness bugs in the pseudocode; no proof was done.
- assumes: not applicable
- size or effort: no proof
- tool: DistAlgo; written by: human
- case A:220; source record paxos-sb-in-distalgo-2026
PBFT with read-only optimization; PBFT view change; Casper FFG; early Tendermint; FaB
- guarantee: Known liveness failures in PBFT with read-only optimization, PBFT view change, Casper FFG, early Tendermint and FaB are cited, such as clients isolated forever, a new leader never catching up, and bouncing and equivocation attacks.
- assumes: partial synchrony; malicious scheduler or Byzantine processes
- size or effort: n/a
- tool: informal attacks cited in testing paper; written by: human
- case A:44; source record decouchant-kulahciogluozkan-zhou-liveness-testing-2023
Request retries after a network outage (web app + database)
- guarantee: In an idealized web app plus database with one retry after 1 s, a short network outage can leave the system overloaded even after the outage ends; worked arithmetic shows recovery needs load below 150 QPS or retries below 20 QPS.
- assumes: idealized app: one query plus one retry after 1 s; database latency jumps above 300 QPS
- size or effort: no proof; recovery needs load below 150 QPS or retries below 20 QPS
- tool: none (informal analysis, worked arithmetic); written by: human
- case C:r10:37; source record metastable-failures-2021
SystemVerilog hardware design: Load-Store (LS)
- guarantee: The new method failed on all 16 tasks of checking “something good eventually happens” properties of the SystemVerilog Load-Store (LS) hardware design, using a learned certificate checked by the Bitwuzla SMT solver (paper’s own report).
- assumes: Hardware/reactive systems only; no arrays, strings of parametric length, procedure calls or dynamic data structures; 5 h limit per task per tool
- size or effort: 0 of 16 tasks solved by the new method (Table 1)
- tool: Neural certificate (inductive invariant + ranking function) learned with MILP solver Gurobi, checked with Bitwuzla; compared with ABC, nuXmv, rIC3 (and NMC’24 for liveness); written by: automatic tool
- case C:r7:26; Let a Neural Network Be Your Invariant, Table 1 and Appendix A
Tendermint (fastsync, row 2)
- guarantee: TLC and Apalache checked Tendermint fastsync liveness, and the SoK says TLC found a counterexample.
- assumes: not stated in the table ; SoK 3.3: TLC found a counterexample violating termination; ‘For complex liveness checks, the tool timed out after 24 hours’
- size or effort: not given in SoK; see cited paper [7] Braithwaite et al., FMBC 2020
- tool: TLA+/TLC, Apalache; explicit and symbolic MC; written by: human
- case A:235; Bondarev, Ziborov, Yanovich, SoK: Formal Verification of Consensus Protocols (arXiv 2608.21935), Table 1 p.7 ; cites [7] Braithwaite et al., FMBC 2020
Tendermint v34.3 (Go, 150k lines; 600 lines of shim added)
- guarantee: A Netrix test found that a Tendermint replica that fell behind does not catch up on seeing f+1 messages from a higher round, a liveness bug; hit in 100/100 iterations.
- assumes: Bounded (timeout per iteration), so a ‘bounded liveness’ check; replica isolated for round 0
- size or effort: LaggingReplica 3 filters, 4 states, 71 lines, 100/100 iterations
- tool: Netrix DSL testing tool (filters + state-machine monitor, PCTCP random exploration); written by: human
- case C:r8:15; Netrix Sec. 1, 5.2, Tab. 3
Zab-FLE (fast leader election)
- guarantee: Zab fast leader election has no stated guarantee and was later shown to cause a liveness issue where the system gets caught in an infinite loop.
- assumes: none
- size or effort: proof as stated by authors: fix argued informally, no proof ; paper’s verdict: liveness bug found by the Zab-FLE authors; no liveness stated (not in Table 3)
- tool: paper-only (no machine proof); written by: human
- case A:295; source record what-s-live-2021
Zeebe Raft implementation (Camunda Platform 8 workflow engine), Java
- guarantee: Randomized tests of Zeebe Raft checking that, with no failures, a leader is eventually elected found issues #8324, #10180, #10202 and #10545.
- assumes: Testing, not proof: random sequences, fixed number of tries per build (@Property(tries=10)); liveness only checked after a failure-free tail; replicas single-threaded, CPU-level concurrency ignored
- size or effort: Liveness tests added while reproducing a customer bug; with the replicate property they found issues #8324, #10180, #10202, #10545
- tool: Property-based testing with jqwik; deterministic scheduler and controllable network; random operation sequences (append, snapshot and compact, receive message, execute task, tick clock, drop message, restart replica); written by: human
- case C:r7:54; Camunda blog, Properties section
ZooKeeper Fast Leader Election (SysMoBench task)
- guarantee: No LLM and agent combination produced a TLA+ model of ZooKeeper Fast Leader Election (5,360 lines Java) that passed the runtime check; the paper calls it the most challenging task.
- assumes: Source Java; LLM writes the model; invariants written by benchmark authors; best of 5 runs; 3 feedback rounds
- size or effort: No agent/LLM combination passed the runtime check; paper calls it the most challenging; 5,360 lines Java, 141 lines TLA+
- tool: TLA+ / TLC model checker, SANY, trace validation; written by: agent
- case C:r4:13; source record sysmobench-2026

everything else: paper proofs, tests, benchmark entries, unclear

83 cases.

ACT (Aguilera-Chen-Toueg, crash-recovery)
- guarantee: The Aguilera-Chen-Toueg crash-recovery protocol is argued on paper to make every good process eventually decide, if a majority of processes are good.
- assumes: ‘A majority of processes are good.’ ‘Every good process proposes a value.’ good = always up or eventually always up. Paper: link Fair; server Q-Alw; Each-Learn
- size or effort: proof as stated by authors: Systematic ; paper’s verdict: ‘All from Q-Alw single (Prop 3)’: fine (Theorem 5 of ACT proves Each-Learn)
- tool: paper-only (no machine proof); written by: human
- case A:287; source record what-s-live-2021
ASML photolithography machine software (Coco Platform)
- guarantee: ASML says its Coco Platform tooling shows photolithography machine software is free of classes of errors including starvation; the claim comes from the company and cited talks, not shown in the paper.
- assumes: Author says his own contribution is minor; claims come from the company and cited talks
- size or effort: not reported
- tool: Coco Platform (CSP-like process algebra plus optimised model checker); written by: human
- case C:r6:8; source record csp-retrospective-2024
BFTDC distributed transaction commit
- guarantee: BFTDC is claimed informally to give atomic termination and agreement for distributed commit despite Byzantine coordinator replicas (3f+1 with at most f faulty), with a 20-server prototype showing 20-30% latency overhead.
- assumes: 3f+1 coordinator replicas; at most f Byzantine replicas; WS-AT/Kandula transaction model
- size or effort: Informal correctness claims; 20-server prototype, 1000 samples per run; 20–30% end-to-end latency overhead
- tool: BFTDC protocol with Byzantine agreement and decision certificates; written by: human
- case C:codex_snowball:17; A Byzantine Fault Tolerant Distributed Commit Protocol, §§3–5
Bullshark
- guarantee: Bullshark DAG-based consensus is claimed safe and live under stated conditions.
- assumes: conditional guarantee; see cited paper and liveness note for fairness, timing and fault premises; exact case-specific premises not fully extracted
- tool: liveness; written by: human
- case B:liveness:29; source record lido-dag-2025
Chubby-Live (Paxos Made Live)
- guarantee: Paxos Made Live (Chubby) tests that the system is consistent and making progress, with no proof.
- assumes: Paper: link Sure; server Alw (eventually all servers always non-faulty); assertion Resp
- size or effort: proof as stated by authors: none (testing); Formalization ‘None’ ; paper’s verdict: ‘Weak from PQ-Alw (Cor 5.1), trivial from Alw’: too strong, makes consensus trivial
- tool: paper-only (no machine proof); written by: human
- case A:291; source record what-s-live-2021
Cogsworth Byzantine view synchronization
- guarantee: Cogsworth is a Byzantine view synchronization protocol with a protocol proof and evaluation, under Byzantine quorum and network assumptions.
- assumes: Byzantine quorum and network assumptions
- size or effort: Byzantine protocol case
- tool: protocol proof and evaluation; written by: human
- case C:codex_snowball:45; Cogsworth: Byzantine View Synchronization
Context-bounded multithreaded shared-memory program
- guarantee: Fair termination and absence of fair starvation are shown decidable for multithreaded shared-memory programs under a fixed context-switch bound per thread.
- assumes: Thread spawning; each thread can be context-switched only a fixed number of times
- size or effort: Decidability; 2EXPSPACE-complete ordinary context-bounded termination
- tool: VASS with balloons reductions; written by: human
- case C:codex_snowball:9; source record context-bounded-multithreaded-liveness-2020
Crash-stop asynchronous multiparty session processes
- guarantee: Crash-aware multiparty session types are proved to guarantee protocol conformance, deadlock freedom and liveness despite permanent process crashes.
- assumes: Crash-stop failures; optional reliability assumptions
- size or effort: Subject reduction, session fidelity, deadlock-freedom and liveness theorems
- tool: Crash-aware asynchronous MPST typing and global/local semantics; written by: human
- case C:codex_snowball:23; Crash-Stop Failures in Asynchronous Multiparty Session Types, §5
CRDT eventual consistency
- guarantee: CRDT eventual consistency holds when communication is accounted for, under additional assumptions.
- assumes: conditional guarantee; see cited paper and liveness note for fairness, timing and fault premises; exact case-specific premises not fully extracted
- tool: liveness; written by: human
- case B:liveness:17; source record trillium-2024
CT (Chandra-Toueg, eventually strong failure detector)
- guarantee: Chandra-Toueg consensus with failure detector diamond-S: every correct process eventually decides (Lemma 6.2.2), assuming fewer than half the processes faulty; paper proof.
- assumes: ‘If we assume that the maximum number of faulty processes is less than half then we can solve Consensus using ♦S’; ‘Every nonfaulty process proposes some value.’ Paper: link Fair; server Q-Alw; assertion Each-Learn
- size or effort: proof as stated by authors: Systematic (1 page); the Strong-detector algorithm has a sketch ; paper’s verdict: ‘All from Q-Alw single (Prop 3)’: fine; strongest-per-assumption
- tool: paper-only (no machine proof); written by: human
- case A:286; source record what-s-live-2021
Derecho
- guarantee: The Derecho paper claims ‘progress’ when no more than a minority of processes fail, with no proof given.
- assumes: ‘Derecho will make progress if (1) no more than a minority of the current view fails and (2) the failure detector only reports a failure if the process in question has actually failed or has become unreachable.’ Paper: link Fair; server P-Alw-Q
- size or effort: proof as stated by authors: none ; paper’s verdict: lacking assertions (progress not defined)
- tool: paper-only (no machine proof); written by: human
- case A:279; source record what-s-live-2021
Dijkstra k-, 4-, and 3-state protocols
- guarantee: Dijkstra k-, 4- and 3-state protocols eventually give a unique privilege, which then recurs.
- assumes: conditional guarantee; see cited paper and liveness note for fairness, timing and fault premises; exact case-specific premises not fully extracted
- tool: liveness; written by: human
- case B:liveness:45; liveness abstract finite-but-unbounded models; Lotan–Shoham §6
Dynamic lock-sharing systems (processes spawn processes and create locks)
- guarantee: For dynamic lock-sharing systems, properties of the run’s limit tree, including fairness and liveness, can be verified in Ptime for common small-arity, 3-priority cases, while synthesis has a complexity gap.
- assumes: finite-state or pushdown processes; shared read/write variable makes it undecidable unless the writer changes a bounded number of times
- size or effort: verification in Ptime for common small-arity, 3-priority cases; synthesis has a complexity gap
- tool: paper proofs (limit configurations, tree automata); written by: human
- case C:K:42; Mascle thesis Ch. 5 Conclusions
EPaxos
- guarantee: The EPaxos paper argues on paper that liveness holds with high probability while a majority of replicas are non-faulty, because clients and replicas time out and retry.
- assumes: Paper: link Fair; server Alw-Q (eventually always some quorum non-faulty, quorum may change); Some-Exec
- size or effort: proof as stated by authors: none ; paper’s verdict: ‘None from Alw-Q (Prop 7)’: too weak, each quorum may not stay non-faulty long enough; Prop 7: ‘No quorum-based consensus algorithm that executes in rounds can satisfy Some-Learn under Fair and Alw-Q.’
- tool: paper-only (no machine proof); written by: human
- case A:296; source record what-s-live-2021
etcd/raft (Go, 16k lines; 120 lines of shim)
- guarantee: Two Netrix variants of the etcd/raft liveness scenario check the bug appears with the Prevote/CheckQuorum options off and not with them on; both ran 100/100 iterations.
- assumes: Which variant uses which setting is not stated in the text
- size or effort: 5 filters; 100/100 iterations for both
- tool: Netrix DSL testing tool (filters + state-machine monitor, PCTCP random exploration); written by: human
- case C:r8:19; Netrix Sec. 5.3, Tab. 3
Even/odd counter
- guarantee: An even/odd counter visits every natural number under stated schedule premises.
- assumes: conditional guarantee; see cited paper and liveness note for fairness, timing and fault premises; exact case-specific premises not fully extracted
- tool: liveness; written by: unclear
- case B:liveness:16; source record trillium-2024
Eventually Consistent Counter
- guarantee: TLA-Prover lists Eventually Consistent Counter as a benchmark case: A distributed grow-only counter (G-Counter CRDT) with N nodes. Each node increments its own slot. Merge takes element-wise max. All nodes eventually agree on the total.
- tool: TLA-Prover separate suite; written by: unclear
- case B:TLA-Prover separate suite:20; source record tla-prover-2026
EVS (Extended Virtual Synchrony)
- guarantee: Extended Virtual Synchrony: if server s performs an action and a set containing s and r later faces no communication or process failures, then r eventually performs it, shown on paper only.
- assumes: link Fair; server Q-Alw; assertion Each-Exec
- size or effort: proof as stated by authors: Systematic ; paper’s verdict: ‘All from Q-Alw (Prop 4)’: fine, assumption weaker than most
- tool: paper-only (no machine proof); written by: human
- case A:277; source record what-s-live-2021
FastMCP gateway for GPU vision-training workflows (12 tools, Celery queues, CIFS mounts)
- guarantee: In the same FastMCP gateway model, every allocated GPU worker is eventually released, checked at run time on generated traces.
- assumes: Model, 12 tools and states written by hand; trace generation not described; one-step lookahead check
- size or effort: check overhead 1.2 ms (depth 2) to 31.0 ms (depth 14); 672 vs 196,608 states at depth 14; 0.0% deadlocks on 500 traces
- tool: hand-written labeled transition system with run-time LTL guard in a FastMCP gateway; no external model checker named; written by: human
- case C:r6:2; source record verified-mcp-gateway-2026
FIFO queue
- guarantee: FIFO queue: each sent item eventually received if receives recur, a conditional liveness guarantee (the row says fairness, timing and fault premises apply).
- assumes: conditional guarantee; see cited paper and liveness note for fairness, timing and fault premises; exact case-specific premises not fully extracted
- tool: liveness; written by: unclear
- case B:liveness:22; liveness Ivy abstract model; 1queuelive.ivy
FluentBit controller
- guarantee: FluentBit controller eventually reaches a stable desired configuration, assuming a stable desired-state description and weak fairness.
- assumes: Stable desired-state description; weak fairness on controller/environment actions; modeled crashes and request failures eventually cease; built-in StatefulSet/DaemonSet updates eventually pause until the target updates again. Anvil §4.3.3 PDFp9: “eventually stop happening”; the competing-controller pause premise is stated in the same section. Trust TLA embedding, environment/API models, Verus/Z3, Rust compiler and OS (§4.1). DaemonSet competing updates use the corresponding pause assumption (§4.3.3 PDFp9). Gap: pinned ESR theorem predicates for permitted desired-state inputs and external interference unresolved
- tool: liveness; written by: human
- case B:liveness:5; source record anvil-2024
Handover protocol (primary/secondary)
- guarantee: The paper states the handover protocol is usually efficient, safe and live (the secondary takes over if the primary stalls), but only the same-decision interlock is checked with FDR here; liveness is a design goal, not shown.
- assumes: Only the same-decision interlock is modelled and checked in this paper; liveness is the stated design goal, not shown here
- size or effort: not reported
- tool: CSP/FDR for the interlock; stochastic analysis in cited papers; written by: human
- case C:r6:5; source record csp-retrospective-2024
HotStuff, 2-Phase HotStuff, Sync HotStuff
- guarantee: The Twins test generator checks whether HotStuff, 2-Phase HotStuff and Sync HotStuff keep making progress under Byzantine twin replicas and partitions; 2-phase and Sync HotStuff are known to violate liveness in subtle fault scenarios.
- assumes: partial synchrony; Byzantine twin replicas and network partitions
- size or effort: testing; detects all known violations with fewer false positives than time-bounded checks
- tool: Twins test generator with temperature and lasso detection (testing); written by: automatic tool
- case A:43; source record decouchant-kulahciogluozkan-zhou-liveness-testing-2023
Imperative loop programs
- guarantee: Termination of simple imperative loops is proved by automatically generated invariants and linear ranking functions, with one example reaching sufficient invariants in 2.5 s.
- assumes: Simple Programming Language loops; linear ranking functions
- size or effort: One reported example reached sufficient invariants in 2.5 s
- tool: Invariant generation with widening and polyhedral-cone ranking synthesis; written by: automatic tool
- case C:codex_snowball:15; source record colo-n-sipma-termination-2002
Imperative loop programs
- guarantee: Termination of simple imperative loops is proved by automatically generated invariants and linear ranking functions, with one example reaching sufficient invariants in 2.5 s.
- assumes: Simple Programming Language loops; linear ranking functions
- size or effort: One reported example reached sufficient invariants in 2.5 s
- tool: Invariant generation with widening and polyhedral-cone ranking synthesis; written by: automatic tool
- case C:codex_snowball:16; source record colo-n-sipma-termination-2002
Implicit-ranking binary counter
- guarantee: The implicit-ranking binary counter guarantees specified eventual progress.
- assumes: conditional guarantee; see cited paper and liveness note for fairness, timing and fault premises; exact case-specific premises not fully extracted
- tool: liveness; written by: human
- case B:liveness:41; liveness abstract model; Lotan–Shoham §6
Implicit-ranking toy stabilization
- guarantee: An implicit-ranking toy stabilization example eventually stabilizes.
- assumes: conditional guarantee; see cited paper and liveness note for fairness, timing and fault premises; exact case-specific premises not fully extracted
- tool: liveness; written by: unclear
- case B:liveness:40; liveness abstract model; Lotan–Shoham §6
Increment/decrement counter
- guarantee: An increment/decrement counter has strong convergence under stated conditions.
- assumes: conditional guarantee; see cited paper and liveness note for fairness, timing and fault premises; exact case-specific premises not fully extracted
- tool: liveness; written by: unclear
- case B:liveness:20; liveness Isabelle executable definitions; Gomes et al. §7
IronRSL replicated service
- guarantee: IronRSL guarantees safety and that repeated client requests eventually get replies, under timing and resource assumptions and a live quorum.
- assumes: Repeated client sends to all replicas; quorum Q exists; eventually Q scheduling frequency >= F with enough memory; eventually messages between Q/client arrive within Delta; eventually each Q replica receives <= B packets per 10B/F + 1 time units; clock error <= E whenever read; no Q replica halts at an overflow-prevention limit. Bounds can be unknown to code. IronFleet §5.1.4 PDFp10: “overflow-prevention limit” is a prohibited source of halted progress. Trusted packet integrity, I/O, Dafny/compiler/runtime/OS/hardware (§2.5). Gap: pinned theorem/parameter instantiation and deployment scheduler/clock validation unresolved
- tool: liveness; written by: human
- case B:liveness:1; source record ironfleet-2015
Jolteon, unpipelined
- guarantee: Jolteon, unpipelined: safety and eventual consensus commits under partial synchrony, a conditional liveness guarantee (the row says fairness, timing and fault premises apply).
- assumes: conditional guarantee; see cited paper and liveness note for fairness, timing and fault premises; exact case-specific premises not fully extracted
- tool: liveness; written by: unclear
- case B:liveness:26; source record refinement
Linear loop programs
- guarantee: Ranking functions are synthesized for linear loop programs to prove they terminate.
- assumes: Linear loop transition relations
- size or effort: Template synthesis; no aggregate benchmark count in extracted abstract
- tool: Linear ranking templates and constraint solving; written by: automatic tool
- case C:codex_snowball:8; source record ranking-templates-2015
Lock-free CAS-retry counter (illustrative)
- guarantee: An illustrative CAS-retry counter is lock-free but not starvation-free, since a specific call may never finish even under some fair schedulers, while the fetch-and-add version is wait-free.
- assumes: fair scheduler still allows starvation
- tool: none (example used to define terms); written by: human
- case A:168; Verifying Wait-Freedom for Concurrent Higher-Order Programs (ECOOP 2026), s.1, Figure 1
LVR alternating bit
- guarantee: LVR alternating bit: sender data eventually arrives, a conditional liveness guarantee (the row says fairness, timing and fault premises apply).
- assumes: conditional guarantee; see cited paper and liveness note for fairness, timing and fault premises; exact case-specific premises not fully extracted
- tool: liveness; written by: unclear
- case B:liveness:34; liveness abstract model, synthesized ranking; LVR Table 3
LVR hybrid reliable broadcast
- guarantee: LVR hybrid reliable broadcast guarantees correct nodes eventually accept a broadcast.
- assumes: conditional guarantee; see cited paper and liveness note for fairness, timing and fault premises; exact case-specific premises not fully extracted
- tool: liveness; written by: human
- case B:liveness:33; liveness abstract model, synthesized ranking; LVR Table 3
LVR multi-Paxos
- guarantee: LVR multi-Paxos guarantees progress of the consensus log.
- assumes: conditional guarantee; see cited paper and liveness note for fairness, timing and fault premises; exact case-specific premises not fully extracted
- tool: liveness; written by: human
- case B:liveness:37; liveness abstract model, synthesized ranking; LVR Table 3
LVR Paxos
- guarantee: LVR’s Paxos: a decision is eventually reached.
- assumes: conditional guarantee; see cited paper and liveness note for fairness, timing and fault premises; exact case-specific premises not fully extracted
- tool: liveness; written by: unclear
- case B:liveness:36; liveness abstract model, synthesized ranking; LVR Table 3
LVR stoppable Paxos
- guarantee: LVR stoppable Paxos: reconfiguration-related consensus progress, a conditional liveness guarantee (the row says fairness, timing and fault premises apply).
- assumes: conditional guarantee; see cited paper and liveness note for fairness, timing and fault premises; exact case-specific premises not fully extracted
- tool: liveness; written by: unclear
- case B:liveness:38; liveness abstract model, synthesized ranking; LVR Table 3
LVR ticket lock
- guarantee: LVR’s ticket lock: a waiting client eventually enters the critical section.
- assumes: conditional guarantee; see cited paper and liveness note for fairness, timing and fault premises; exact case-specific premises not fully extracted
- tool: liveness; written by: unclear
- case B:liveness:32; liveness abstract model, synthesized ranking; LVR Table 3
Mencius
- guarantee: The Mencius paper claims “liveness” without explaining or proving it.
- assumes: ‘Since P (Mencius is P combined with certain optimizations) only relies on the eventual delivery of messages for liveness’. Paper: link Fair; no server assumption
- size or effort: proof as stated by authors: none ; paper’s verdict: lacking assumptions
- tool: paper-only (no machine proof); written by: human
- case A:293; source record what-s-live-2021
MongoDB Realm Sync operational transformation
- guarantee: For MongoDB Realm Sync operational transformation, 4913 tests generated from a TLA+ model (100% branch coverage) check that clients and server resolve conflicts the same way so all participants eventually hold identical data.
- size or effort: 4913 generated tests, 100% branch coverage
- tool: TLA+ model-based test-case generation; written by: human
- case A:141; MongoDB blog (WebFetch summary, not re-checked)
MongoDB replica-set Raft model and C++ implementation
- guarantee: MongoDB’s Raft-based replication was tested with randomized testing and trace checking against a TLA+ model, targeting that no committed write is lost and all servers eventually learn the newest commit point, without complete coverage.
- assumes: Implementation traces are sampled; mapping state back to model and completeness are difficult
- size or effort: Industry retrospective of experiments first tried in 2020; no complete coverage claim
- tool: TLA+ model, randomized testing and trace checking; written by: human
- case C:codex_grey:19; source record mongodb-conformance-blog-2025
multiparty session protocol
- guarantee: Linear Haskell session types are used to guarantee deadlock freedom of multiparty protocols through linearity and typed channels.
- assumes: linearity and typed channels
- size or effort: functional implementation case
- tool: linear Haskell session types; written by: human
- case C:codex_snowball:53; source record deadlock-free-session-types
Mutual exclusion protocols (Bar-David enhancement of deadlock-free mutex)
- guarantee: Paper proofs, checked with modal mu-calculus model checking, bound how often a process can be bypassed in Bar-David’s enhancement of deadlock-free mutual exclusion (bounded bypass, quadratic bound in atomic registers).
- assumes: atomic, safe or regular registers
- size or effort: not extracted
- tool: paper proofs, checked by modal mu-calculus model checking; written by: human
- case A:36; source record on-the-notions-of-2026
N producers and N consumers sharing a buffer of size 1
- guarantee: A written ghost-signal proof outline shows N producers and N consumers sharing a buffer of size 1 all terminate; it was not run in a tool in the text read.
- assumes: N chosen randomly at run time; proof uses N variants of each signal
- size or effort: several figures of proof outline; not run in a tool in the text read
- tool: ghost-signal logic, written proof outline (appendix); written by: human
- case C:r6:47; Ghost signals thesis, App A.5.2
Narwhal with Jolteon
- guarantee: Narwhal with Jolteon, a DAG-based consensus, is claimed safe and live under conditional fairness, timing and fault premises.
- assumes: conditional guarantee; see cited paper and liveness note for fairness, timing and fault premises; exact case-specific premises not fully extracted; Jolteon BFT requests buffered until vertex locally available, not original Narwhal-HotStuff
- tool: liveness; written by: unclear
- case B:liveness:28; source record lido-dag-2025
Non-blocking counter and stack
- guarantee: Pen-and-paper Total-TaDA proofs show a non-blocking counter and stack terminate and are lock-free, wait-free and non-impeding, given constraints on the concurrent environment.
- assumes: constraints on concurrent environment
- size or effort: unknown
- tool: Total-TaDA (pen-and-paper); written by: human
- case A:184; da Rocha Pinto et al., ESOP 2016
Paxos-Basic (Paxos Made Simple)
- guarantee: Paxos Made Simple informally argues that Paxos is live if enough of the system works properly.
- assumes: link Raw
- size or effort: proof as stated by authors: none ; paper’s verdict: no liveness stated precisely (not in Table 3)
- tool: paper-only (no machine proof); written by: human
- case A:283; source record what-s-live-2021
Paxos Commit
- guarantee: Paxos Commit is claimed to keep commit/abort decisions in agreement and make progress when at least F+1 of 2F+1 coordinators work, with no machine-checked proof size reported.
- assumes: Majority coordinator availability and stable storage
- size or effort: Protocol analysis; no machine-checked proof size reported
- tool: TLA+ specification and Paxos reasoning; written by: human
- case C:codex_snowball:6; Consensus on Transaction Commit, §4 and abstract
Paxos-Fast (Fast Paxos paper, covers basic Paxos liveness)
- guarantee: Fast Paxos paper states that a learner eventually learns a value if some proposer, coordinator and majority set stay good (nonfaulty) from some time on; paper-only, no machine proof.
- assumes: ‘An agent is defined to be nonfaulty iff it eventually performs the actions that it should, such as responding to messages. Define a set G of agents to be good iff all the agents in G are nonfaulty and, if any one agent in G repeatedly sends a message to any other agent in G, then that message is eventually received’. Paper: link Fair; server PQ-Alw (generalized to a set of quorums); assertion Some-Learn
- size or effort: proof as stated by authors: Systematic ; paper’s verdict: ‘Weak from PQ-Alw (Cor 5.1)’: fixed primary and quorum is stronger than needed
- tool: paper-only (no machine proof); written by: human
- case A:284; source record what-s-live-2021
Paxos-High (Liu-Chand-Stoller, DistAlgo)
- guarantee: Paxos-High in DistAlgo states no liveness property but was used to find liveness violations in Paxos-Complex when messages can be lost.
- assumes: none
- size or effort: proof as stated by authors: none ; paper’s verdict: no liveness stated (not in Table 3)
- tool: DistAlgo; written by: human
- case A:305; source record what-s-live-2021
Paxos-PVS (Kellomaki)
- guarantee: Kellomaki PVS Paxos has no liveness spec or proof: “Liveness is neither specified or proved.”
- assumes: none
- size or effort: proof as stated by authors: none (safety only, PVS) ; paper’s verdict: no liveness stated (not in Table 3)
- tool: paper-only (no machine proof); written by: human
- case A:289; source record what-s-live-2021
Paxos-SB (Paxos for System Builders)
- guarantee: Paxos for System Builders states on paper that if a stable majority exists and a member initiates an update, some member eventually executes it; the authors doubt any Paxos-like algorithm can meet the stronger version.
- assumes: Authors: ‘We believe that no Paxos-like algorithm will be able to meet [Strong L1]’. Paper: link Fair; server Q-Alw (Weak L1) or Alw-Q (Strong L1); Some-Exec and Each-Exec
- size or effort: proof as stated by authors: none; Formalization ‘None’ ; paper’s verdict: ‘All from Q-Alw (Prop 4)’: fine for Weak L1; but Resp fails if clients do not resend requests
- tool: paper-only (no machine proof); written by: human
- case A:292; source record what-s-live-2021
Paxos-Synod (Part-time Parliament)
- guarantee: Paxos-Synod: if a majority stay in the Chamber for T + 99 minutes with a president, every priest has a decree in the ledger; prose argument, no machine proof.
- assumes: ‘a messenger who did not leave the Chamber would always deliver a message within 4 minutes, and a priest who remained in the Chamber would always perform an action within 7 minutes’. Paper: link Sure; server PQ-Extra-Dur: some t with (no change to servers over [t,t+D1+D2]) and (some primary p nf during [t+D1,t+D1+D2]) and (some quorum q nf during [t,t+D1+D2]). Assertion Each-Learn + time bound
- size or effort: proof as stated by authors: Prose; Formalization ‘None’ ; paper’s verdict: ‘assuming primary’: assumes a primary but gives no way to elect one
- tool: paper-only (no machine proof); written by: human
- case A:282; source record what-s-live-2021
Paxos-Time (De Prisco-Lampson-Lynch)
- guarantee: The Paxos timing paper (De Prisco-Lampson-Lynch) proves on paper that in a stable execution with a majority alive the leader decides by time 21l + 8nl + 11d.
- assumes: nice = stable (no Lose/Duplicate, regular clock) and a majority alive. Paper: link Sure; server PQ-Dur; Each-Exec + time bound
- size or effort: proof as stated by authors: Systematic (IOA, informal) ; paper’s verdict: ‘assuming primary’
- tool: paper-only (no machine proof); written by: human
- case A:288; source record what-s-live-2021
Paxos-TLA (Chand-Liu-Stoller)
- guarantee: Paxos-TLA (Chand-Liu-Stoller) proves safety in TLAPS and does not discuss liveness formally.
- assumes: none
- size or effort: proof as stated by authors: none (TLAPS safety only) ; paper’s verdict: no liveness stated (not in Table 3)
- tool: TLA+/TLAPS, safety only; written by: human
- case A:301; source record what-s-live-2021
Paxos variants
- guarantee: SPIN and Isabelle/HOL are listed in the SoK for Paxos variants with a liveness property, using the Heard-Of model.
- assumes: not stated in the table ; SoK 3.3: SPIN verified LastVoting and Hybrid-1 agreement for up to 3 processes
- size or effort: not given in SoK; see cited paper [38] Tsuchiya, Schiper, DISC 2008; [11] Charron-Bost, Merz, 2009
- tool: SPIN, Isabelle/HOL; Heard-Of model; written by: human
- case A:227; Bondarev, Ziborov, Yanovich, SoK: Formal Verification of Consensus Protocols (arXiv 2608.21935), Table 1 p.7 ; cites [38] Tsuchiya, Schiper, DISC 2008; [11] Charron-Bost, Merz, 2009
Paxos-Vertical (Vertical Paxos)
- guarantee: The Vertical Paxos paper states no liveness guarantee: “A discussion of liveness is beyond the scope of this paper.”
- assumes: none
- size or effort: proof as stated by authors: none ; paper’s verdict: no liveness stated (not in Table 3)
- tool: paper-only (no machine proof); written by: human
- case A:285; source record what-s-live-2021
Paxos-VS (virtually synchronous Paxos)
- guarantee: Paxos-VS: every client request is eventually replied to, argued on paper only, assuming a correct majority per membership and eventual communication; no machine proof.
- assumes: ‘Throughout the lifetime of a membership M, a majority of servers are correct’; ‘messages may get lost, re-ordered, or duplicated’; ‘correct members can eventually communicate any message’. Paper: link Fair; server P-Alw-Q
- size or effort: proof as stated by authors: none (‘-’) ; paper’s verdict: ‘Resp from P-Alw-Q (Prop 5)’: claims Resp under weaker assumption than PQ-Alw, which makes PQ-Alw-based claims weak
- tool: paper-only (no machine proof); written by: human
- case A:278; source record what-s-live-2021
PBFT single-entry prototype
- guarantee: PBFT single-entry prototype has partial safety and liveness machinery; the end-to-end proof is incomplete, assuming eventual network stabilization.
- assumes: Eventual network stabilization; thereafter bounded message/timeout delay; eventual message/timeout delivery and clock ticks (Shipwright §3.2 PDFp5-6); cyclic leaders and increasing timeouts (§4 PDFp9). Honest nodes run verified total Dafny callbacks over trusted Go runtime; peer/address/key configuration common knowledge; adversary lacks honest private keys (§3.1 PDFp4). Quorum conditions are abstracted; exact fault-threshold/quorum instantiation not recovered here. Scope: one entry, client replies excluded; end-to-end refinements incomplete: §5 PDFp12 “We have not yet proven correct all of the trace properties required for safety and liveness of the end-to-end specification”. Not a completed liveness-task oracle
- tool: liveness; written by: human
- case B:liveness:25; source record shipwright-2025
RabbitMQ controller
- guarantee: The RabbitMQ controller is claimed to reach an eventual stable configuration and not scale down unsafely, under stable desired state, weak fairness and faults that eventually cease.
- assumes: Stable desired-state description; weak fairness on controller/environment actions; modeled crashes and request failures eventually cease; built-in StatefulSet/DaemonSet updates eventually pause until the target updates again. Anvil §4.3.3 PDFp9: “eventually stop happening”; the competing-controller pause premise is stated in the same section. Trust TLA embedding, environment/API models, Verus/Z3, Rust compiler and OS (§4.1). Safety additionally relies on replica-count validation and controller waiting for GC to remove orphan StatefulSets before updating (§6.2 PDFp13); desired descriptions alone are insufficient. Gap: pinned ESR/safety theorem predicates and allowed external interference unresolved
- tool: liveness; written by: unclear
- case B:liveness:4; source record anvil-2024
RabbitMQ with StatefulSet
- guarantee: RabbitMQ with StatefulSet composes to eventual stable reconciliation, assuming a stabilizing desired state and weak fairness.
- assumes: Desired-state description eventually stabilizes; weak fairness on model actions; message drops/controller crashes eventually cease; PodMonkey disturbances eventually cease. Welder §5 PDFp11: faults eventually stop (including PodMonkey as specified below). Additional retry-on-conflict fairness: each retry loop terminates, either succeeding or returning a non-version-conflict error; §4.2 PDFp9: “RoC loop terminates”. Always-preserved request-centric rely restrictions on other controllers, with own guarantee satisfying compatible controllers; no finite delivery/computation bound required. RabbitMQ depends on StatefulSet reconciliation; composition must discharge that dependency and prove mutual rely/guarantee compatibility (§4.4, §6). StatefulSet naming restrictions hold throughout execution: §5 PDFp11 PodMonkey always respects the StatefulSet naming scheme. Gap: pinned pairwise request predicates and deployment fairness validation unresolved
- tool: liveness; written by: human
- case B:liveness:9; source record welder-2026
Raft
- guarantee: Raft claims it keeps making progress while broadcastTime << electionTimeout << MTBF, but “progress” is not defined and no proof is given.
- assumes: timing condition broadcastTime << electionTimeout << MTBF
- size or effort: proof as stated by authors: none ; paper’s verdict: no liveness assertion stated precisely (not in Table 3); Fig. 4 shows Raft admits infinite runs where Each-Vote holds but Some-Learn never does
- tool: paper-only (no machine proof); written by: human
- case A:297; source record what-s-live-2021
Sailfish, original and optimized
- guarantee: Sailfish, original and optimized: DAG-based consensus safety/liveness, a conditional liveness guarantee (the row says fairness, timing and fault premises apply).
- assumes: conditional guarantee; see cited paper and liveness note for fairness, timing and fault premises; exact case-specific premises not fully extracted
- tool: liveness; written by: unclear
- case B:liveness:30; source record lido-dag-2025
SAT backtracking/backjumping
- guarantee: SAT backtracking/backjumping algorithms terminate.
- assumes: conditional guarantee; see cited paper and liveness note for fairness, timing and fault premises; exact case-specific premises not fully extracted
- tool: liveness; written by: unclear
- case B:liveness:44; liveness abstract models; Lotan–Shoham §6
Single-path linear loop
- guarantee: Termination of single-path linear loops is witnessed by bounded-depth multiphase-linear ranking functions, with polynomial time for rationals/reals and coNP-completeness for integers.
- assumes: Variables over rational, real, or integer domains; conjunctions of linear constraints
- size or effort: Polynomial-time for rational/real bounded depth; coNP-complete for integers
- tool: MΦRF synthesis; written by: automatic tool
- case C:codex_snowball:10; source record m-rf-2017
StatefulSet controller
- guarantee: The StatefulSet controller is claimed to reach an eventual stable managed state, assuming the desired state stabilizes, weak fairness, and drops, crashes and disturbances eventually cease.
- assumes: Desired-state description eventually stabilizes; weak fairness on model actions; message drops/controller crashes eventually cease; PodMonkey disturbances eventually cease. Welder §5 PDFp11: faults eventually stop (including PodMonkey as specified below). Additional retry-on-conflict fairness: each retry loop terminates, either succeeding or returning a non-version-conflict error; §4.2 PDFp9: “RoC loop terminates”. Always-preserved request-centric rely restrictions on other controllers, with own guarantee satisfying compatible controllers; no finite delivery/computation bound required. Stronger PodMonkey naming premise always holds, not only after faults stop: §5 PDFp11 “the PodMonkey always respects its naming scheme”. Gap: exact reserved-name/ownership predicates and retry fairness deployment validation unresolved
- tool: liveness; written by: unclear
- case B:liveness:8; source record welder-2026
Stenning reliable transfer
- guarantee: Stenning reliable transfer eventually acknowledges every sequence number under network and scheduler fairness.
- assumes: Fair scheduling plus fair network: for every message, repeated infinite sends imply eventual delivery; continuously enabled threads eventually run. Fairneris §2.1 PDFp6: “if a message is sent infinitely often (always eventually), then it is eventually delivered”; §4.1 PDFp14 uses SchedFair and NetFair for every sequence-number acknowledgment. At-Most-One-Off sender/receiver state relation is established by refinement, not an extra trusted environmental premise (§4.2). Scope: AnerisLang over modeled UDP-like primitives; §1 PDFp5 “we instead give a paper proof” for model liveness. Gap: fully mechanized model liveness, pinned artifact and production runtime connection unresolved
- tool: liveness; written by: unclear
- case B:liveness:24; source record refinement
Synchronous session calculus networks
- guarantee: A global session type system for synchronous networks is proved to guarantee lock-freedom under fairness assumptions such as justness.
- assumes: Justness or other specified fairness; flexible choice
- size or effort: Three lock-freedom notions; completeness theorem under justness
- tool: Global session types with general merge operator; written by: human
- case C:codex_snowball:24; source record justness-and-lock-freedom-2021
Termite termination benchmarks
- guarantee: Termite synthesizes lexicographic linear ranking functions for C programs, reporting PolyBench 22/30, Sorts 5/6, TermComp 119/129 and WTC 46/58 proved terminating.
- assumes: C programs translated to LLVM SSA; invariants generated by Pagai
- size or effort: PolyBench 22/30, Sorts 5/6, TermComp 119/129, WTC 46/58; 3k-line OCaml prototype
- tool: Termite; written by: automatic tool
- case C:codex_snowball:11; Synthesis of Ranking Functions, Table 1 and Sec. 9
Ticket lock (n threads, weak memory)
- guarantee: A ticket lock with n threads under weak memory (Release-Acquire, StrongCoherence) is proved on paper to be starvation free, assuming weak and memory fairness.
- assumes: weak fairness plus memory fairness; models Release-Acquire and StrongCoherence
- size or effort: paper proof; Coq development exists for the fairness definitions (Lahav et al.)
- tool: Manna-Pnueli response rules in LTL with memory fairness and ranking over weak-memory state; paper proofs; written by: human
- case A:34; source record towards-proving-liveness-on-2026
Ticket locks, queue locks, lock-coupling list, optimistic list, lazy list
- guarantee: A pen-and-paper rely-guarantee logic (LiLi) proves starvation-freedom or deadlock-freedom plus linearizability of ticket locks, queue locks, lock-coupling and optimistic lists, under fair scheduling.
- assumes: fair scheduling
- size or effort: unknown
- tool: LiLi (pen-and-paper rely-guarantee logic); written by: human
- case A:183; Liang et al., POPL 2016, abstract
Ticket mutual exclusion protocol
- guarantee: The ticket lock protocol is shown, for an unbounded number of threads, to let no two threads into the critical section together and each ticket-holder eventually enter, under fair scheduling.
- assumes: Arbitrary unbounded number of threads; fairness schedules each thread infinitely often
- size or effort: Worked theoretical case; no implementation size reported
- tool: Well-founded proof spaces and quantified predicate automata; written by: human
- case C:codex_snowball:7; source record parameterized-liveness-proof-spaces-2016
Ticket protocol
- guarantee: The ticket protocol guarantees eventual service under scheduling premises.
- assumes: conditional guarantee; see cited paper and liveness note for fairness, timing and fault premises; exact case-specific premises not fully extracted
- tool: liveness; written by: human
- case B:liveness:21; liveness Ivy abstract model; inspected ticket files
Token-based mutual exclusion as an ARDT
- guarantee: The paper states, without proof, that the token in token-based mutual exclusion eventually moves on, and notes this fails under permanent owner failure.
- assumes: At-least-once delivery; owner does not fail permanently
- size or effort: states it fails under permanent owner failure
- tool: none (stated, not proved); written by: human
- case C:r9:8; Sec 2.2, 3
Token ring
- guarantee: Token ring: requesting machine eventually enters, a conditional liveness guarantee (the row says fairness, timing and fault premises apply).
- assumes: conditional guarantee; see cited paper and liveness note for fairness, timing and fault premises; exact case-specific premises not fully extracted
- tool: liveness; written by: unclear
- case B:liveness:42; liveness abstract model; Lotan–Shoham §6
Two threads with a signal (create, fork waiter, set)
- guarantee: A 3-line ghost-signal proof outline shows a waiting loop in a two-thread signal example terminates under fair scheduling.
- assumes: Fair scheduler; signal operations thread-safe in simplest form
- size or effort: 3-line proof outline
- tool: ghost-signal separation logic (hand proof outline); written by: human
- case C:r6:44; Ghost signals thesis, Sec 3.2.1, Fig 3.3a
View synchronization for HotStuff, Tendermint, PBFT, SBFT (single-shot)
- guarantee: View synchronization for HotStuff, Tendermint and PBFT guarantees that all correct processes eventually overlap in a view with a correct leader long enough to decide, under partial synchrony and Byzantine faults, by paper proof.
- assumes: partial synchrony; Byzantine faults; bounded space despite message loss before GST
- size or effort: n/a
- tool: paper proofs (not mechanized); written by: human
- case A:45; source record making-byzantine-consensus-live-2020
VR-Revisit
- guarantee: Viewstamped Replication Revisited executes client requests provided at least f+1 non-failed replicas including the primary can communicate, argued in prose only.
- assumes: link Raw (‘are able to communicate’); server P-Alw-Q
- size or effort: proof as stated by authors: Prose ; paper’s verdict: ‘None from Raw (Prop 2)’: too weak, link assumption lets all messages be lost so no assertion can hold
- tool: paper-only (no machine proof); written by: human
- case A:281; source record what-s-live-2021
VS-ISIS (ISIS group communication)
- guarantee: The VS-ISIS paper says it omits a formal proof that its protocols are free of deadlock and livelock.
- assumes: none stated
- size or effort: proof as stated by authors: none ; paper’s verdict: no liveness stated (not in Table 3)
- tool: paper-only (no machine proof); written by: human
- case A:275; source record what-s-live-2021
Wirehead distributed double buffer (Python+MongoDB) as Rocq state machine
- guarantee: The Rocq progress proof for Wirehead (with at least one generator and fair scheduling a swap eventually happens) is complete except 2 Admitted lemmas on pigeonhole counting over unbounded process ids.
- assumes: Single MongoDB instance; crash-stop (no partitions, no Byzantine); each MongoDB call atomic; weak fairness for liveness; model written by hand from the Python code, link to real code not proved
- size or effort: Proof chain complete except 2 Admitted lemmas (pigeonhole counting over unbounded process ids); about 800 lines of auxiliary invariants in Safety.v
- tool: Rocq proof assistant, written by hand; written by: human
- case C:r7:6; Doan thesis, Sec 6.1-6.2, Table 6.1
Yes-no concurrent example
- guarantee: Yes-no concurrent example: fair termination, a conditional liveness guarantee (the row says fairness, timing and fault premises apply).
- assumes: conditional guarantee; see cited paper and liveness note for fairness, timing and fault premises; exact case-specific premises not fully extracted
- tool: liveness; written by: unclear
- case B:liveness:14; source record trillium-2024
Zab (ZooKeeper atomic broadcast)
- guarantee: Zab: a transaction proposed by leader l is eventually committed if a quorum is up, elects l, and messages are timely; paper sketch only.
- assumes: Paper: link Sure; server PQ-Alw; Each-Exec
- size or effort: proof as stated by authors: Sketch (about 2 paragraphs) ; paper’s verdict: ‘Weak from PQ-Alw (Cor 5.1)’: assumption stronger than needed (PQ-Alw is stronger than P-Alw-Q, under which Paxos-VS solves consensus)
- tool: paper-only (no machine proof); written by: human
- case A:294; source record what-s-live-2021
Zeebe Raft implementation (Camunda Platform 8 workflow engine), Java
- guarantee: Randomized tests of Zeebe Raft check that, with no failures, all records are eventually committed and replicated to all replicas, after extra failure-free steps.
- assumes: Testing, not proof: random sequences, fixed number of tries per build (@Property(tries=10)); liveness only checked after a failure-free tail; replicas single-threaded, CPU-level concurrency ignored
- size or effort: Same liveness tests; checked after extra failure-free steps (run tasks, process messages, tick heartbeat)
- tool: Property-based testing with jqwik; deterministic scheduler and controllable network; random operation sequences (append, snapshot and compact, receive message, execute task, tick clock, drop message, restart replica); written by: human
- case C:r7:55; Camunda blog, Properties section

Last edited: 2026-10-31

Keyboard shortcuts