🤖 database, distributed and concurrent systems that were proved

(authored by agents unless marked 🧑)

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

An Empirical Study of LLM-Generated Specifications for VeriFast (2026)
- what: # An Empirical Study of LLM-Generated Specifications for VeriFast (authored by agents unless marked 🧑) Wen Fan, Minh Tran, Sanya Dod, Xin Hu, Marilyn Rego, Danning Xie, Jenna DiVincenzo and Lin Tan, arXiv:2606.26490v1, 25 June 2026. This is an empirical study of LLM-written specifications and auxiliary proofs for C programs checked with VeriFast. It reports 855/2,727 outputs passing verification (31.4%), 91% source-behavior preservation and 92% contract preservation. The last figure combines equivalent and strengthened contracts; it is not an equivalence rate. The released verification CSVs contain 856 “yes” rows, one more than the paper. No general correctness theorem or end-to-end proof of an LLM verifier is given (Q1,Q8,Q9,T3–T6,C8). ## Reading and source scope Read all 13 PDF pages, sections I–VIII, both figures, all eight tables, displayed code/specifications and all 83 bibliography entries. All 13 individual page renders were inspected. There is no appendix, checklist, numbered theorem/proof or separately numbered algorithm. Figure 1 is a complete append-tail verification example; Figure 2 diagrams the study. References were read as bibliography entries, not recursively followed. The inventory PDF matches its recorded SHA256. Acquired the paper’s §VIII replication package, Zenodo record 19570523, DOI 10.5281/zenodo.19570523; its 17,362,580-byte ZIP matches the published MD5 8c8335ee601057daf18c27d3cf9097e3. Inventoried 14,646 ZIP members. The archive’s ISSRE26 filename does not establish a publication venue. Its metadata identifies an anonymous replication package published 14 April and updated 20 April 2026, preceding the arXiv version; correspondence to every reported run is not established. Read the root and two infrastructure readmes, all selected analyzer and generation scripts, four original append-tail inputs/ground truth, three generated append-tail FBP outputs and four generated files containing literal assume(false). The 15 released CSVs were parsed as plaintext to count labels, unique benchmark names and selected rows; modified.txt was counted, not semantically reviewed. In total 43 plaintext assets are retained, with per-asset reading boundaries. A bounded lexical scan covered the 2,727 primary full-study C outputs, without treating it as whole-output semantic reading. XLSX workbooks, remaining inputs/outputs, retrieved examples/tutorial bodies, libraries, raw checker/API logs and recursively cited papers were not read. No author code was executed/imported, verifier rerun, model/checkpoint loaded or experiment reproduced. Quotes retain exact source bytes and LF/character pointers; arithmetic and static control-flow findings are reader checks, not new experimental results. ## Task, logic and benchmark assumptions Separation logic describes ownership of disjoint heap regions. VeriFast uses symbolic execution, contracts, predicates, loop invariants, folding/unfolding statements and lemma calls to check safety and specified behavior. The paper describes Z3 as the default solver. Although background mentions VeriFast 25.11, actual experiments use 24.08.30 with default integer-overflow and heap-leakage checks. The record therefore does not transfer outcomes to another release or to Verus/Rust (Q2,Q7,Q8). The dataset has 303 functions from 60 small single-file C programs: 258 functions from 50 public examples and 45 from ten author-written programs. Selection starts with 770 repository programs, narrows to 160 single-file example/tutorial programs, then removes 46 lacking code or SL specifications, 49 duplicates or prompt-tutorial examples, ten with unresolved verification errors and five without prepared inputs. This deliberately retains known-verifiable programs, not arbitrary industrial code. Overall ground truth averages 43 source and 81 specification lines, with ranges 3–143 and 5–600. The public and new subsets average 44/91 and 34/32 lines respectively (Q3). Each function receives one mutually exclusive feature tag, prioritizing concurrency, then loops, then recursive predicates: 45 concurrent, 39 loop, 134 recursive-predicate and 85 other functions. A function tagged concurrency may also contain a loop; these are not independent feature effects. The authors’ ten new programs resemble the public set and are used for both selection and the full study. Their non-leakage is asserted, not independently established; a low overall verification rate cannot itself measure contamination (Q3,Q12). Three inputs retain executable code but differ in guidance: NL gives informal behavior, FB formal pre/postconditions, and FBP adds allocation ownership or integer constraints needed for verification. FBP is closer to a complete solution and asks a different completion task from NL. Paper Table I’s append-tail example specifies an acyclic input/output list; Figure 1’s contract tracks ownership and acyclic shape, not a value sequence, preserved prefix or insertion of exactly one value. A program satisfying only that contract has not thereby proved the full usual append operation. The retained artifact’s list nodes omit the value field and its append_tail takes only head; this is a simpler example variant, not a byte-identical implementation of Figure 1 (Q2,Q3,T1,F1,C10). ## Prompt/model selection and measured workflow Four prompt contents, Basic, chain-of-thought, sparse retrieval and dense retrieval, cross whole-program versus function input for eight choices. The first pilot uses GPT-4o and the 45 new functions’ FBP variants. Sparse retrieval with function splitting verifies 64%, versus at most 56% for alternatives, with 63 errors versus more than 67; its three logical errors and two behavior changes also influence selection. These are selection-set results, not independent held-out estimates (Q4). A second pilot chooses Claude 3.7 Sonnet, Gemini 2.5 Pro and GPT-4o from ten models: selected models verify at least 60%, have at most 73 errors and at most two behavior changes. A follow-up crosses ten models with eight prompts over the same 45 FBP functions; however, deprecated Claude 3.7 is replaced by Haiku 4.5. It therefore supplies broader prompting evidence without evaluating exactly the same model set. Sparse split and unsplit tie at median 16 verified functions; selected model families’ reported medians are 23, 22.5 and 20.5, versus at most 15 for the rest. It does not remove reuse of the selection set or isolate all input/model interactions (Q5). The full study fixes sparse retrieval with splitting and evaluates three models × three input types × 303 functions, producing 2,727 outputs. Temperature is zero, with one output per condition, not repeated sampling. Sparse retrieval uses BM25, dense retrieval TextEmbedding, and vectors reside in Qdrant. The retained prompt code retrieves ten program/library entries and five tutorial entries, caps concatenated example text at 300,000 characters and extracts C-fenced blocks. Main generation calls each model once per input, without a verifier-feedback loop. The code’s active model list is the later ten-model configuration including Haiku, not a preserved exact full-study configuration; historical correspondence needs logs (Q4–Q8,Q12,C6,C7). Reported local hardware is a Yoga 14sACH 2021, 16 AMD Ryzen 7 5800HS CPUs, 16 GiB RAM, 1 TB SSD, Ubuntu 24.04 and Python 3.12; Qdrant has 0.5 vCPU, 1 GiB RAM and 4 GiB disk. Full-study API costs per model are Gemini $233, C l a u d e$ 232 and GPT-4o 1,380 retrospective API price
- number: Cat: 106.8M tokens, 64 h, 17 prompts
- number: Clipper 26/29 functions after 81h44m; Nouns Auction 18/20 after 94h28m with certificate check timing out
- limits: It does not show transaction availability, bounded gas, eventual completion or soundness of the supplied policy. The refinement relation permits vacuity through gas exhaustion (running out of gas makes a claim hold trivially). The trusted base includes the EVM formalization, imported Lean axioms and native_decide. A human supplies the high-level spec.
- how much was read: most of it read
- source; notes: Foundational Refinement Proofs for Deployed Bytecode, at the Price of ; notes: Foundational Refinement Proofs for Deployed Bytecode, at the Price of
- record id: eqivm-2026
Fairneris (2026)
- title: A Higher-Order Separation Logic for Verifying Liveness-Preserving Refinements of Distributed Systems
- what: A logic mechanized in Rocq. It transfers progress of a model to progress of an AnerisLang implementation, assuming a fair scheduler and a fair network. The network may drop, duplicate and reorder messages. Fairness here applies to sets of messages.
- number: two-node implementation; every sequence number eventually gets a reply assuming callback termination and fairness
- number: no LOC, person-time or benchmark timing reported
- limits: It verifies code under the language’s own operational semantics, not a production Rust or OCaml executable. Humans supply the model, invariants, contracts and refinement proofs. The URL of the mechanization artifact is not given.
- how much was read: most of it read
- source; notes: A Higher-Order Separation Logic for Verifying Liveness-Preserving Refi
- record id: fairneris-2026
Federated Formal Verification (2026)
- title: Federated Formal Verification: Cross-Backend Citation, Cross-Axis Convergence, and AI-Orchestrated Proof Dispatch for Production Systems
- what: This work sends the open TLA+ proof obligations of a production Raft system to Coq, Lean, Why3, Apalache, Z3 and CBMC. Claude Code specialists handle each backend. CI rechecks the proofs, and the system generates Java runtime assertions.
- number: 17 active hours, 263 commits, 26-axiom census closed
- number: about twenty specialist agents in four waves of 3/6/7/4; practical concurrency 6-7
- number: proof tree over 11,000 lines, 18 apex obligations
- number: Coq 8/8 passes, median 34.4 s; Apalache 0/3; TLC 0/5; PRISM 1/13
- limits: A human wrote the claim that the backends are equivalent. There is no artifact URL. The paper gives no prompts, no cost, and no breakdown of human effort. The Java assertions check test states only, not refinement. The speedup compares different protocols. Apalache refuted a property that Coq cited, at bound six.
- how much was read: most of it read
- source; notes: Federated Formal Verification: Cross-Backend Citation, Cross-Axis Conv
- record id: federated-formal-verification-2026
Fewer Assumptions by Design: A Reusable Skill for LLM-Assisted Verus Verification (2026)
- what: Verifies an index-based doubly linked list in Verus by hand, then with a Claude agent. It then packages a ‘skill’ (SKILL.md, templates, and a list of pitfalls) that tells the agent how to work. The goal is to use as few assume statements (unproven hypotheses) and axiomatic lemmas as possible.
- number: by hand: 16 assumes (Exp 1), 11 assumes (Exp 2)
- number: with Claude: assume count dropped from 75 to 11; final state 45 verified, 0 errors, 11 assumes
- number: agent cost: a couple of hours of reasoning plus manual prompting by the user
- number: Table5: Codex5.2 High46assumes; Claude4.8 Max two index runs0assumes/0axioms; Claude4.6 High18assumes/1axiom; Standard/SlotMap0assumes/8axioms. Runs10–50min. Table6 rates all concrete Standard/SlotMap mutators fully opaque.
- limits: It covers one data structure only. The evaluation is a rubric scored by the authors over 6 runs with Claude 4.6/4.8. No success rate is given.
- how much was read: most of it read
- source
- record id: fewer-assumptions-by-design-2026
Formal Verification Frameworks for Cloud-Native Microservices (2026)
- what: Sketches a framework that models microservices as a graph of states and writes five properties in temporal logic (request gets a response, error leads to recovery, and so on), to be checked by a model checker. Reports detection rates against testing and monitoring.
- number: deadlock detection accuracy 96.7% vs 81.2% for log-based testing (Table 1)
- number: fault detection accuracy 95.4% vs 85.2% traditional (Table 2)
- number: verification coverage 94.6% vs 80.1%
- number: detection time 96 ms vs 130 ms
- limits: The paper names no model checker, no concrete system, no test workload, and no definition of how accuracy or coverage were measured, so the numbers cannot be interpreted. The properties are written as generic formulas, none is proved.
- how much was read: most of it read
- source; notes: ## Formal Verification Frameworks for Cloud-Native Microservices (2026
- record id: formal-verification-frameworks-for-2026
Formal Verification of Multi-Controller Systems in Cloud Management (2026)
- what: A NuXMV model of two Kubernetes-style controllers, two resources and two users. It checks convergence (eventually the requested state holds forever) and completion. Overlapping resources cause endless overwriting. Dependencies can block forever.
- number: Table 2: four settings; no overlap/dependencies all pass, others fail
- number: no runtime, effort or source size reported
- limits: A small abstract model, built by hand from incidents. The unavailability result holds only if the model lets a resource be unavailable forever.
- how much was read: most of it read
- source; notes: Formal Verification of Multi-Controller Systems in Cloud Management
- record id: formal-verification-of-multi-2026
From Verification Failures to Reusable Guidance for Coding Agents (2026)
- what: Turns diagnosed proof failures into reusable procedures (a kit) for coding agents. The agents write specifications and proofs of execution in the K framework, with Lean for leftover math. Separate agents audit the result.
- number: 164/164 final AI audit PASS verdicts after two targeted repairs and heavy human-guided resource development
- number: at the common checkpoint with the kit: 97 Pass, 67 Concerns, 0 Fail
- number: 12-pair challenge: all 12 defects detected, all 12 clean accepted (Wilson interval 75.8-100%)
- number: controlled 31-program test: GPT-5.6 Luna 15/31, 15/31, 19/31; all four intervals include zero
- limits: The target is partial functional correctness (correct if it terminates), and termination is handled separately. The trusted base includes the translation, the semantics and the solver integration. The controlled evidence does not show a clear general benefit of the kit.
- how much was read: most of it read
- source; notes: From Verification Failures to Reusable Guidance for Coding Agents; notes: From Verification Failures to Reusable Guidance for Coding Agents
- record id: from-verification-failures-to-2026
GGMS (2026)
- title: Learning Provably Correct Distributed Protocols Without Human Knowledge
- what: A transformer-guided Monte Carlo tree search learns transition tables for synchronous crash-fault protocols (atomic commit and consensus). Exhaustive model checks give it feedback.
- number: atomic commit 2/1: 100%, 15 min; 3/2: 60%, 813 min; 4/2: 70%, 754 min
- number: consensus 4/2: 90%, 717 min; 4/3: 100%, 3358 min
- number: plain MCTS / DFS baselines often 0-50%
- number: timeouts 1, 2, 4 days for 2, 3, 4 processes; ten runs per setting
- limits: Humans supply the states, decisions, correctness formulas and bounds. The setting is synchronous, crash-only, with finite process counts. Termination is bounded, not asynchronous liveness. It is not an LLM agent.
- how much was read: most of it read
- source; notes: Learning Provably Correct Distributed Protocols Without Human Knowledg; notes: Learning Provably Correct Distributed Protocols Without Human Knowledg
- record id: ggms-2026
Guidelines for Producing Concise LNT Models, Illustrated with Formal Models of the Algorand Consensus Protocol (2026)
- what: # Whole-paper read: Guidelines for Producing Concise LNT Models, Illustrated with Formal Models of the Algorand Consensus Protocol (authored by agents unless marked 🧑) Hubert Garavel. MARS2026, EPTCS443,pp43–83,doi10.4204/EPTCS.443.5;arXiv2604.05006,41pages. The paper refactors a finite LNT model of Algorand’s BBA* phase and reports equivalence/model checks. Its strongest directly measured result is model compaction with strong bisimilarity checked for two four-node configurations. It supplies a detailed transformation sequence, printed model code and property scripts. It does not establish correctness of the deployed Algorand implementation or arbitrary-size Byzantine consensus. [Q0,Q1,Q2,Q10,Q11] ## What changes, and what is preserved The original Urbino model has967LNT lines. Application-specific changes produce U0 with769lines. These changes include new observations, merged/split events, a different attacker and a fair-coin correction; the paper explicitly says many “do not preserve bisimilarity properties.” Thus equivalence of U0–U4 does not imply equivalence with the original967-line model. [Q2,Q11,Q14] Four generic transformations then produce U1–U4: extract shared modules, replace duplicated control branches with data parameters, merge common sequences, and replace mutually recursive tail calls with assignments and explicit loops. Strong bisimilarity means corresponding states can match every labelled transition in both directions. Authors report BCG_CMP checks for A4,0(four honest nodes) and A2,2(two honest/two malicious), with incremental checks after individual changes. They give structural/algebraic explanations, not a mechanized theorem covering every use of every transformation. The common-suffix choice law is explicitly qualified as failing for common prefixes. [Q3,Q4,Q5,Q6,Q7] The §2.2 table gives total/nonblank-noncomment lines: U0=769/705,U1=607/552,U2=320/282,U3=288/250,U4=250/212. U0→U4 therefore removes67.49%of total lines and69.93%of substantive lines, ratios3.076and3.325 respectively; these are reader arithmetic. The original967→250comparison also includes semantic changes. Readability and reduced maintenance effort are the author’s qualitative judgments; there is no reader study or maintenance-cost experiment. [Q3,Q11] State counts illustrate that fewer source lines need not produce fewer unminimized states. For the honest-node/malicious-node/A4,0/A2,2 LTSs, U0 has1740/3190/24230/42509states; U1 is identical; U2 has1761/3190/24599/42509;U3 has1681/3046/20665/34679;U4 has1723/3130/20905/35059. After strong-bisimulation minimization every version has558/840/12059/19486states. Identical minimized counts alone would not prove bisimilarity; the reported equivalence checks supply that evidence. No runtime or memory benchmark is given. [Q3] ## Concrete transformation cases U1 extracts duplicated node/counter code and splits data definitions into types/constants/channels. U2 merges honest, malicious and disguised behaviors using a MORALITY parameter; node IDs≤H identify honest nodes. U3 factors common suffixes/prefixes and reduces NODE’s process calls22→9. Its final branch-factorization example is acknowledged as harder to understand despite being shorter. U4 exposes an inner three-step coin loop inside an outer block-processing loop, replacing12recursive calls across node/counter code with3loops. [Q4,Q5,Q6,Q7] The loop discovery uses pairs of control location and step residue, rather than control locations alone. The initial random-bit process had combined graded-consensus abstraction with a later fair coin; separating these roles restores the nested-loop structure. The earlier probability P_H used for the later coin is corrected to0.5 among the specific changes before the equivalence-preserving sequence. The counter independently accepts propagated/self-propagated bits, increments K0/K1 and resets them after TALLY. AnnexB prints U2/U3/U4 node code and recursive/imperative counter variants, enabling direct comparison. [Q7,Q14,Q15,Q16] ## What is verified Visual checking first hides irrelevant events and minimizes by branching bisimulation, which allows matching behavior across internal steps. Four-node models have roughly12000–20000strongly minimized states,43000–69000transitions and131labels. SYNC-only slicing exposes alternating BEGIN/END barriers. The block interface exposes proposal bits0/1 and commit-proposed/commit-empty events: for H≥T the observed model allows acceptance or rejection; for H<T the illustrated attacker systematically rejects bit1 proposals. Earlier pre-v5models have visible deadlock traces. These are observations of the stated abstract models and attacker, not an arbitrary-fault resilience theorem. [Q8] Equivalence checks compare sliced systems with small hand-written expected processes: TALLY events form a cyclic four-dimensional hypercube; SELF_PROPAGATE has a more involved loop with optional per-node propagation. Hidden bit/counter values are renamed toX, so those checks establish event-pattern behavior after abstraction, not correctness of discarded values. SET_BIT slices remain difficult to inspect, motivating value-passing MCL formulas. [Q9,Q10] AnnexC reports16named property scripts checked on both U4configurations: P1deadlock absence;P2SYNC alternation;P3aTALLY counter sum≤4 andP3bhypercube;P4a/bPROPAGATE patterns;P5a/bSELF_PROPAGATE patterns;P6a/bselection P_IN/P_OUTpatterns;P7a/bP_ZERO/P_ONEpatterns;P8ablock-interface classification;P9a/b/cper-node SET_BITinitialization and step progression. The latter formulas require an eventual next bit-setting event or, in P9b, a new proposal, without intervening conflicting events. They are local sequencing checks. The conclusion leaves formulas connecting all nodes’ votes to the expected consensus decision as future work. The printed P9cdescription is grammatically incomplete, while its formula explicitly targets SET_BIT(ID,0,any). [Q17,Q18,Q19,Q20] The models have infinite loops. Absence of deadlocks does not itself prove eventual block commitment. The paper does not report probabilistic model checking or almost-sure termination; probability values occur in observable choice labels, and probabilistic verification is proposed as future work. The evaluated equivalences and MCL results should not be turned into a quantitative probability-of-failure guarantee. Larger configurations of6,8,10nodes are mentioned as explored compositionally, without this paper providing comparable property outcomes or resource measurements for them. [Q10,Q11,Q15,Q16] ## Model assumptions and limits AnnexA fixes node population, honesty and equal stake; omits money/rewards, cryptography and leader election; abstracts graded consensus by a probability; reduces step numbers modulo3; and synchronizes every voting phase with global BEGIN/ENDbarriers. Committees are independently selected possibilities ranging from0toNmembers rather than fixed sizeC. The attacker does not fork: it manipulates votes to reject selected proposed blocks. U0 replaces shared BOYCOTT synchronization with independent malicious behavior triggered by proposal bit1. Therefore the model covers one censorship-style strategy, not all Byzantine behavior or dynamic corruption. [Q12,Q13,Q14] Two documented interpretation choices are fresh committees per step rather than per round, and a persistent per-node bit across steps. Printed constants use N=4,C=3,T=2,H=2(or4),P_V=C/N,and P_H=p²(1+p−p²),p=H/N. The main process synchronizes nodes on proposals, propagation, barriers and both commit events. Reader observation: agreement at those shared commit events is constrained by the model composition; the paper’s checks do not independently establish all implementation behaviors fit that composition. Relaxing synchrony and moving from historical BBA* to deployed ABFT remain future work. [Q12,Q13,Q15,Q16,Q11] For this collection, the paper contributes a concrete workflow for simplifying distributed-system specifications while checking equivalence and targeted temporal properties. Its relevance to LLM-generated specifications is my inference: proposed cleanup should retain an explicit preservation target, and success on self-chosen event slices should not substitute for the intended protocol guarantee. The paper has no Verus, Rust, TLA+ or LLM experiment. ## Read and evidence scope Read all41pages, §§1–8,29reference entries and AnnexesA–C, including all32specific changes,9model-code subsections,16property scripts and auxiliary processes. Inspected all5figures, the full §2.2table and dense formula/code renderings; complete extracted text supplied the remaining material. No external author artifact was linked or acquired beyond the full code printed in the paper. Official arXiv and inventory PDFs are byte-identical. Publisher PDF differs in66bytes but yields identical raw extracted text; hashes and comparison saved. No author code, compiler, model checker, solver or generated LTS was executed or loaded. All reported tool results remain attributed to the author.
- limits: boundedfixedsynchronousmodel;restrictedattacker;abstractGC/crypto;equivalenceamongrefactoringsnotoriginal/deployedprotocol
- how much was read: most of it read
- source
- record id: guidelines-for-producing-concise-2026
IC3Syn (2026)
- title: Synthesizing Inductive Invariants for Distributed Protocols via IC3 and Large Language Models
- what: An IC3 controller hands an LLM (Claude Opus 4.6) concrete bad states to block. The LLM proposes TLA+ clauses. TLC and Apalache check them on small instances. TLAPS then proves the invariant for all sizes.
- number: 29 of 29 protocols solved (Table 1 p. 9); direct Claude baseline 23/29; Gemini 3 Flash inside IC3 solves 27/29
- number: MLDR (MongoDB Raft model): 4525 s, 16 clauses, proof over 3,000 lines; EPR Paxos: 1806 s, 9 clauses
- number: Default synthesis timeout 30 minutes, 2 hours for the two hardest cases
- number: Paper’s rerun of Endive solves 24 shared cases
- limits: The models and safety goals are supplied. Liveness is not evaluated. The synthesis loop works on finite instances only. The proof stage used a scaffold plus Codex automation. The model, budget and log of human intervention are not stated. Full end-to-end automation is ongoing work. No public code or proof artifact was found. The results are the authors’ own reports.
- how much was read: most of it read
- source; notes: IC3Syn: a direct 2026 LLM invariant search result; notes: IC3Syn: agent-written proofs of unbounded distributed protocol safety; notes: IC3Syn protocol inventory
- record id: ic3syn-2026
ICEPICK API model checking (2026)
- title: Systematic API Testing Through Model Checking and Executable Contracts
- what: Introduces ICEPICK, a black-box REST API testing framework that models API state in TLA+, exhaustively explores the TLC state-space graph, extracts call sequences, and checks execution with GLACIER first-order contracts. The paper specifies a two-phase pipeline: CRUD/OAS contract generation, manual semantic predicates, a conservative TLA+ abstraction, TLC state-space preprocessing, coverage-guided BFS path selection, and execution with an emulator that evaluates preconditions, postconditions and invariants. PUT updates are inserted into post/delete paths; results are classified OK, WARN, ERR or NOT_TESTED. State coverage is complete for generated paths, while transition coverage can miss parallel transitions represented by the same abstract state pair. In the evaluation, Tournaments, Petstore and Features-Service expose distinct scalability and compliance behavior; injected delete and referential-integrity faults are detected, but non-REST APIs block useful inference.
- number: 17 SSG configurations
- number: 30–99.4% SSG size reduction after preprocessing
- number: 5–21 GB models complete within about an hour
- number: 467 GB and 16 h 16 min for Tournaments size 12
- limits: The approach requires resource-oriented REST APIs, accurate schemas and HTTP status semantics; generated contracts are intentionally partial and domain invariants may require manual predicates. TLA+ models are abstractions that can diverge from implementations. TLC and path extraction face state explosion: on the reported hardware about 5–21 GB SSGs finish within an hour, while a 467 GB model takes 16 h 16 min; a 100 GB heap handled about 46K states/349K transitions. Only three systems were evaluated, and three-value configurations produced infeasible request counts.
- how much was read: most of it read
- record id: icepick-api-model-checking-2026
IDS (2026)
- title: Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems
- what: Given a specification written by an expert in Rocq/Coq, a coordinator of GPT-5.4 workers writes an implementation and a proof that Coq’s kernel checks. It can throw away a data representation and start over. Code is extracted to OCaml.
- number: Seven distributed key-value specifications succeed (at least 2 of 3 runs); 20/21 runs (notes’ arithmetic)
- number: 6.8 hours and 1229, 1 week/ $583, 2 w ee k s /$ 1580; about a month and 57 per system across 48 systems (§5.3)
- limits: Model checking plus reproduction gives concrete failures, not proofs for all executions. Its coverage of liveness is weak. The results pool several versions, and only 14 systems used the latest version.
- how much was read: most of it read
- source; notes: Specula: close the model–code loop before calling a violation a bug
- record id: specula-2026
Specy (2026)
- title: Specy: Automatically Learning Specifications for Distributed Systems from Event Traces
- what: It learns event-based formulas from traces of distributed systems (P models or logs). It builds monitors from them and checks fresh traces to reject guesses that are too strong. For six deductive-verification experiments, the learned formulas were translated by hand.
- number: all 43 goal specs recovered, 28 (65%) without help, 15 needed guidance
- number: 14 benchmarks incl. 3 industrial, 10,000 traces each
- number: about 9% of extra learned formulas fail on fresh traces, no designated goal formula does
- number: pruning speeds up by geometric mean 14.8
- limits: The only guarantee is consistency with the supplied traces. Hard properties need predicates, event choices or ghost state. The deductive results cover selected safety properties of P models. There is no refinement to production code.
- how much was read: most of it read
- source; notes: Specy: Learning Specifications for Distributed Systems from Event Trac; notes: Specy: Learning Specifications for Distributed Systems from Event Trac
- record id: specy-2026
SysMoBench (2026)
- title: SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems
- what: A benchmark of eleven concurrent and distributed systems. An AI writes a TLA+ model of each. The model is scored on syntax, execution, behavioral match to the code, and expected properties.
- number: source sizes from 175 lines (PGo dqueue) to 5,360 (ZooKeeper leader election)
- number: Etcd Raft with basic Sonnet agent: 7.69% conformance, 69.23% invariant correctness, 100% syntax
- number: liveness properties violated 41.9% vs safety 8.3% (§5, Figure 4c)
- number: each agent run five times, best output evaluated, at most three repairs
- limits: Covers only the finite executions and configurations supplied. A model can match buggy code and still fail the desired guarantee. The evaluator uses an LLM for some mappings.
- how much was read: most of it read
- source; notes: SysMoBench
- record id: sysmobench-2026
TACO threshold automata verification toolsuite (2026)
- title: TACO: A Toolsuite for the Verification of Threshold Automata
- what: Introduces Taco, a modular toolsuite for developing and verifying threshold-based distributed algorithms modeled as monotonic or extended threshold automata, with SMT, ZCS/BDD, and ACS/WSTS model checkers plus semi-decision support for reset/decrement extensions. The paper specifies TA configurations, resilience conditions, guards and updates, and ELTL_FT safety specifications, then details a preprocessor and three algorithms. SMT encodes steady paths in existential Presburger arithmetic; ZCS abstracts thresholds to finite (0,1)-counter systems and checks BDD error graphs; ACS uses WSTS fixed points. TACO accepts ByMC .ta/.eta and a TLA+ fragment, emits traces, uses safe Rust crates and interchangeable SMT/BDD backends, and reports about 97% line coverage.
- number: ~97% line coverage
- number: 19 MTA benchmark instances plus ETA sets
- number: 20-minute timeout; 2 AMD EPYC 7773x processors, 2 TB RAM
- number: safe Rust implementation
- limits: Monotonic TA permit only increasing shared variables and have decidable parameterized verification. Extended TA with decrements/resets are generally undecidable; ZCS/ACS are semi-decision procedures, and ACS does not support empty-target specifications. TACO currently supports safety ELTL_FT, not liveness.
- how much was read: most of it read
- record id: taco-threshold-automata-verification-toolsuite-2026
Timers (2026)
- title: Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings
- what: Turns a claim about time into a termination problem by adding timers that predict when formulas become true. A human supplies the model, the claim, the implicit ranking, the invariant and finite-set approximations. Z3 checks the generated conditions.
- number: 17 tasks in Table 2, e.g. Ticket: 2 s, 20 invariant conjuncts, 256 proof tokens
- number: Paxos: 101 s, 238 tokens; ABP: 4 s, 539 tokens; HRB-Correct: 135 s, 99 tokens; Dijkstra k-State: 64.8 s, 213 tokens
- number: Ivy proof sizes for six tasks: 407, 521, 860, 446, 593, 748 tokens (Ticket, Paxos, ABP, HRB-Correct, HRB-Relay, Ackermann)
- number: runtime is Z3 validation on Apple M1 Pro, Z3 4.13.3
- limits: The guarantees cover first-order transition-system models, not deployed code. Rankings and invariants are not discovered automatically. Sizes count proof tokens, not human effort.
- how much was read: most of it read
- source; notes: Verifying First-Order Temporal Properties of Infinite-State Systems vi
- record id: timers-2026
TLA+ Examples repository (2026)
- what: This repository is a corpus of TLA+ specifications and models, with CI and metadata indicating beginner examples, PlusCal variants and TLC, Apalache or TLAPS use. Its README also labels models that intentionally fail on deadlock, safety, liveness or assumptions.
- number: at commit 6a7b26a: 81 case directories, 424 modules, 233 model configurations, 73 modules with proof metadata
- limits: Repository metadata and CI status can change; this pass did not run every model.
- how much was read: most of it read
- source
- record id: tla-examples-repository-2026
TLAPS-Bench (2026)
- title: TLAPS-Bench repository
- what: TLAPS-Bench asks AI agents to prove invariants of TLA+ protocol/system specifications in a sandboxed runtime. Its current problem set includes ZooKeeper, etcd and HashiCorp Raft, MongoDB transactions and other protocols.
- number: Current problem set: 9 specs and 57 invariants
- number: Retired/next lists include Byzantine Paxos, broadcast, Paxos, 2PC, termination detection and WAL protocols.
- number: 9 specs and 56 proof targets (FLASH 15, ZooKeeper 9, etcd Raft 8, HashiCorp Raft 6, others)
- limits: The README says retired proofs are available by contact and current runs focus on a few hard tasks; no agent run was reproduced.
- how much was read: most of it read
- source
- record id: tlaps-bench-2026
Towards Composable Proofs of Cache Coherence Protocols (2026)
- what: A Lean proof of safety for the MSI cache-coherence protocol. It shows by trace refinement that the protocol behaves like atomic memory. It is composed from independently verified MI and SI subprotocols, each with local invariants.
- number: 9228 proof lines excluding whitespace/comments
- number: three person-days to translate to Bluespec hardware and test
- number: 100,000 load responses in first testbench
- number: two 64-KB L1 and one 64-KB L2
- limits: It covers safety only. The translation to hardware is manual and tested, not proved equivalent. The authors designed the decomposition and the invariants.
- how much was read: most of it read
- source; notes: Towards Composable Proofs of Cache Coherence Protocols
- record id: towards-composable-proofs-of-2026
Towards System-Oriented Formal Verification of Local-First Access Control (2026)
- what: # Whole-paper read: Towards System-Oriented Formal Verification of Local-First Access Control (authored by agents unless marked 🧑) Florian Jacob, Johanna Stuber and Hannes Hartenstein; arXiv2604.23560v1,26April2026,PaPoC2026-related manuscript,8PDFpages. The contribution is a capability-based authorization design and three deliberately restricted Verus implementations. The paper explicitly says its full §3target has not yet been met. Its results concern simplified authorization/query functions assuming a valid eventually consistent chronicle; they do not verify Matrix, Keyhive, a cryptographic hash implementation, or a deployed replication stack. [Q0,Q1,Q3,Q10,Q13] ## Threat model and intended semantics A local-first entity acts on its own replica and exchanges events asynchronously. The threat model permits any strict subset of entities to be Byzantine, f/n<1, including selective omission, equivocation and backdating. Events are assumed authenticated and integrity-protected. The underlying hash chronicle is assumed Byzantine fault-tolerant, append-only and eventually consistent; collision-resistant identifiers fix an event’s causal past. This is the input contract for the authorization layer, rather than a new proof of the replication or cryptographic layer. Eventual dissemination requires the stated chronicle/anti-entropy assumptions; it does not follow merely from having one honest participant. [Q2,Q4,Q9] The mathematical design uses four event kinds:create,grant,revoke,assign. A grant specifies subject, recipient and operation capability; a use presents the grant’s identifier; revocation references that identifier. Events combine an invocation and a downward-closed set of precursor identifiers. The printed identifier contract idealizes collision resistance as equality of identifiers iff equality of events. A valid group has one creation event, no event concurrent with creation, and valid timestamps. Logging appends an event after the current history; joining takes set union. The name query returns the latest authorized assign events, allowing multiple concurrent names. These are the intended §3semantics, not all jointly verified features. [Q5,Q6] Authorization requires a matching authorized grant in the event’s causal past, no matching authorized revocation in its past or concurrent history, and, for a revoke, a referenced grant in its past. Creation and setup precursors are authorized by definition. Extending revocations to concurrent uses prevents an attacker from bypassing a revocation by backdating a new use. It also makes authorization non-monotonic: new information can invalidate an earlier result. [Q6,Q7] The paper distinguishes authorization based only on immutable precursors (“precursive”) from authorization based on the available group including concurrent events (“discursive”). A subtle example is revocationa concurrent with useb, followed by revocationc concurrent witha but afterb: revokinga can reauthorizeb even thoughc followsb. Concurrency is not transitive. Thus a property’s dependence cannot safely be inferred just by looking at direct time order. This motivates distinguishing what may be stored/broadcast from what currently affects queries. [Q7] The three stated security invariants are:precursor-based authorization is unchanged by adding events, while current authorization can change through authorized revocations; a changed query result requires an authorized newly added event; and an invocation unauthorized now remains unauthorized when backdated. These are specifications of the intended behavior. The paper’s explanation that the full Spec.2supports them is not itself a mechanized proof of all Spec.2features. [Q8] ## What the Verus case study reports The three verified restrictions separate the difficult features. First, assign capabilities are fixed before creation and cannot later change. Second, the creator may grant assign rights after creation, but nobody may revoke. Third, assign rights are initially granted and the creator may revoke them, but new grants are not introduced afterward. The third case permits concurrent assign/revoke conflicts; it avoids mutually revoking equally privileged entities. Supporting both grants and revocations in one algorithm, post-creation delegation, query/membership capabilities, self-revocation, public joining, sparse replication and group changeover are future work. [Q10,Q11,Q12] Specification functions describe pure mathematical behavior; executable functions have contracts linking their results to it. Figure4illustrates a log contract accepting exactly the events authorized by the specification, with an explicit fresh-identifier availability precondition. It is a shortened code example with ellipses, not the complete executable implementation. Authors report total and pure queries, precursor authorization as a group type invariant, and the restricted constructions supporting current authorization/revocation safety. If correct replicas eventually hold the same chronicle, deterministic total queries give the same answer. That conditional convergence argument does not prove dissemination, bounded latency, or settlement in a perpetually changing history. [Q9,Q10,Q11] Totality has a material trust boundary. Authors report modifying vstd to add no_unwind contracts, assuming standard-library functions terminate and allocation/randomness system calls do not panic. They also add the assumption that cloning a HashSet preserves its elements, conditional on Rust std correctness. Ghost specifications and proofs impose no runtime checks according to the paper; the paper provides no throughput, memory or latency experiment demonstrating a numerical runtime saving. Its “zero runtime cost” refers to erasing verification annotations, not to a proof that the algorithms execute for free. [Q9,Q11] The evaluation is a proof-of-concept experience report. It supplies no complete table of proof obligations, solver times, source/proof line counts, hardware measurements, test-population results or comparative performance study. The artifact README says verification “should complete in a hand full of seconds”; this is an informal expected duration, not a saved timing measurement. A practical difficulty was replacing unsupported iterator combinators with for loops and proving their invariants; authors call this among the most time-consuming parts. Their claim that Verus is accessible/future-proof is an author judgment, not a measured user-study result. [Q11,Q13,S0] ## Static artifact comparison The paper-linked repository was retrieved at commit3d6bdaf63c192ada9039f4f61127744465827ed0. Its README identifies Verus release0.2026.01.23.1650a05. The Makefile invokes Verus on main.rs, which imports separate modules for the chronicle, three authorization variants, types, helpers and assumed specifications. I inspected the whole Rust source tree. The HashSetclone assumption is explicit; the only external_body in these sources wraps printing. No assume/admit proof escape appeared beyond that declared assume_specification and imported library axioms. This describes these project files, not the full trusted Verus/vstd closure. [S0,S1,S2,S3,S4,S5,S6,S7,S8,S9] The source makes further simplifications concrete. EntityID/EventID areu64, and Chronicle::find_free_id scans from0 for a locally unused identifier under an explicit availability precondition. Events contain the full predecessor set. There is no cryptographic hashing/signature verification, replica transport or join operation in these project modules. Grant/Revoke operations target an entity’s SetName authorization, without the full Spec.2grant-identifier/delegation structure. The immutable case consults setup_grants; the monotonic case permits creator grants; the non-monotonic case treats all entities as initially able to SetName and disables that right when a matching revocation appears in the relevant history. A type invariant requires all stored events to be causally authorized. name’s executable result must equal its specification’s latest concurrently authorized SetName values. These contracts support the stated restricted authorization layer; they do not implement the complete hash-chronicle data type. [S1,S3,S4,S5,S6,S7] main.rs supplies four hand-written scenarios with proof assertions: reject Dave’s unauthorized assignment and retain two concurrent names; reject an unauthorized grant and a use concurrent with its grant; accept a causally valid backdated assignment but exclude it from current name results; and observe{name1}→{name1,name2}→{name1}when a concurrent revocation arrives. I read these scenarios without executing or re-verifying them. Some chronicle clones are executable statements labelled “for verification purposes only”; the general proof-erasure statement should not be read as a measured guarantee that this entire example has no verification-related executable work. [S8] The paper’s reported no_unwind experiment cannot be reconstructed from this snapshot alone: no no_unwind annotation or modified-vstd patch occurs in the acquired project files. The Nix/Cargo metadata point to external Verus/vstd sources, which I did not inspect. Thus the paper’s conditional totality claim remains attributed to the authors; absence in the project snapshot does not establish that their separate experiment failed. The README’s expected fast verification was not reproduced. [Q9,S0,S1,S8,S9] ## Contribution and read scope This paper directly adds a verified-Rust authorization case study to the distributed-systems collection. It isolates the trust placed in replication, cryptographic identity, library specifications and resource-related behavior. Its potential use in evaluating proof-writing agents is my inference: assess the exact restricted capability policy and trusted library additions before calling a whole system verified. The paper has no TLA+ or LLM experiment. [Q9,Q10,Q11,Q13] Read all8PDFpages,37references,all4figures,both complete mathematical specification boxes and all3security-invariant formulas; inspected every page render. The final PDFpage contains all37references. Read all9Rust source files,README,Makefile,Cargo.toml,flake.nix and relevant lock metadata;15static text files acquired withSHA256/Gitblobidentities. External Verus/vstd dependencies and repository scenario images were not inspected. Official arXiv and inventory PDFs are byte-identical. No author execution, compiler, solver or prover run.
- limits: validauthenticatedeventualchronicle;3simplifiedauthorizationvariants;modifiedvstd/librarytrust;fullcombinedpolicyfuturework
- how much was read: most of it read
- source
- record id: towards-system-oriented-formal-2026
TraceFix (2026)
- title: TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples
- what: Claude Opus 4.6 turns a task description into a topology of agents, locks and channels. It writes PlusCal for each agent, runs TLC, and repairs from failures. The checked processes become runtime prompts.
- number: 48 of 48 tasks reach TLC verification; 30/48 pass first try; hard tasks 4/16 first try
- number: 29 repair attempts: 20 deadlocks, 5 timeouts, 3 syntax errors, 1 undrained channel
- number: Mean about 594 s and about 300–5000 savings uses the paper’s historical AWS3,000 in subscriptions
- number: Ten xv6 bugs and one Sail bug found; median kernel-update re-proof 35 agent-minutes
- limits: It covers safety only, not liveness. Humans steered the layering and specs heavily.
- how much was read: parts read
- source
- record id: machcsl-2026
Tulip (2026)
- title: Verifying a high-performance distributed transaction system using permissioned state machines
- what: Tulip is a distributed transaction system. It comes with a machine-checked proof that the implementation meets a spec identical to that of a local transaction system that is strictly serializable. The method combines TLA-style protocol invariants (facts that stay true in every reachable state) with separation-logic permissions.
- number: about 4,000 lines of Go, about 42,000 lines of Rocq (about 11x)
- number: 10 module types
- number: bugs caught: transactional read, lock release, TAPIR timestamp inversion
- number: 3,956 lines of Go code (abstract)
- limits: The spec does not capture liveness, and the authors did not explore whether the method applies to liveness. The PDF does not name the venue.
- how much was read: parts read
- source; notes: Verifying a high-performance distributed transaction system using perm
- record id: tulip-2026
Verified Detection and Prevention of Concurrency Anomalies in Multi-Agent Large Language Model Systems (2026)
- what: The paper writes four concurrency anomalies of shared memory between LLM agents in TLA+, checked with TLC. It verifies Rust detectors and runtimes in a Verus crate.
- number: 274 Verus obligations (zero assume, zero admit)
- number: 24 obligations for the spec-implementation chain; refinement obligations 31 (pessimistic), 18 (SSI projection)
- number: 274 Verus proof obligations
- limits: Nothing mechanical links the TLA+ and Verus parts. The TLAPS proofs only check that the texts agree, and the Verus refinements are against Verus state machines. It covers safety only, and the authors state that liveness is a gap. It has a single author and the results are self-reported. The notes read about 25% of the paper.
- how much was read: parts read
- source
- record id: verified-detection-and-prevention-2026
3SF model checking (2025)
- title: Technical Report: Exploring Automatic Model-Checking of the Ethereum specification
- what: The authors translate the Python spec of Ethereum’s 3-slot-finality (3SF) consensus protocol into TLA+ and use the Apalache model checker to test Accountable Safety: if two conflicting chains are both finalized, at least one third of validators can be shown to have broken a voting rule. They then add hand-made abstractions and re-encode the problem in SMT (CVC5) and Alloy to check larger instances.
- number: Direct translation (Spec2): checking Accountable Safety timed out after more than 40 hours (Table 1)
- number: Alloy with Kissat: Accountable Safety holds for up to 6 blocks; e.g. 5 blocks, 25 checkpoints, 12 votes in 234 s (Table 5)
- number: CVC5: verified up to 5 blocks with 5 checkpoints (1h 40m) or 3 blocks with 6 checkpoints (74h) (Table 4)
- number: A 7-block Alloy run went over 16 days without finishing
- limits: Only the finality gadget and only Accountable Safety, on small bounded instances (at most 7 checkpoints and 24 votes); every validator has stake 1. The hand-made abstractions are not proved equal to the Python spec. Appendix A (translation rules) and B (soundness proofs) were skimmed, not read closely.
- how much was read: parts read
- source; notes: ## Exploring Automatic Model-Checking of the Ethereum specification (2
- record id: 3sf-model-checking-2025
A Refinement Methodology for Distributed Programs in Rust (precursor: Refinement Proofs in Rust Using Ghost Locks) (2025)
- what: Proves that Rust distributed programs match a simpler model of what they should do (a refinement proof), using the Prusti verifier. The precursor paper also proves liveness (something good eventually happens). It writes those proofs as ghost code (code used only for proving, never run), using a direct encoding of LTL (a logic for statements about time). Cases include a simplified Memcached.
- limits: The review notes could not get the final OOPSLA PDF and read the precursor instead. The verifier is Prusti, not Verus. The review notes do not know whether the final version keeps the liveness part.
- how much was read: parts read
- source
- record id: a-refinement-methodology-for-2025
Anvil thesis (2025)
- title: Building and Verifying Cloud Infrastructure Systems with State-Centric Reasoning (PhD dissertation)
- what: The thesis proves liveness of Kubernetes controllers in Verus, using the Anvil framework. The human writes one general liveness formula, “eventually stable reconciliation”: if the desired state stops changing, the cluster eventually matches it and stays that way. The proof splits into two parts: the environment becomes stable, and the controller reaches the desired state.
- number: about two person-months to verify the ZooKeeper controller, about two person-weeks for each of the other two
- number: each controller takes around 2.5 person-months to implement and verify; proof-to-code ratio 4.5 to 7.4
- number: ZooKeeper: executable 1,134 lines, proof 8,352 (ESR 7,245), trusted 950; RabbitMQ: executable 1,598, proof 7,228, trusted 548
- number: framework: 5353 lines of reusable lemmas, 7817 lines of trusted code; 70+ temporal-rule lemmas, 60 Kubernetes-environment lemmas
- limits: The controller must be a state machine whose actions are atomic (they cannot be interrupted). The proof trusts the environment model, the shim layer, external APIs, the verifier, the compiler and the OS. After verification, testing still found one bug. It came from an incomplete spec of a trusted ZooKeeper API. About 40% of the 111 pages were read.
- how much was read: parts read
- source
- record id: anvil-thesis-2025
CapybaraKV (2025)
- title: CapybaraKV (verified-storage)
- what: CapybaraKV is a verified key-value store written in Verus. An earlier version appears in the OSDI 2025 paper PoWER Never Corrupts. It comes with a line-counting script that computes the ratio of proof lines to code lines.
- limits: The notes read only the README.
- how much was read: parts read
- source
- record id: capybarakv-2025
Clock-SI TLA+ (2025)
- title: Formal modelling and analysis of Clock-SI with TLA+
- what: A master’s thesis that models the Clock-SI protocol (snapshot isolation for a partitioned database using loosely synchronized clocks) in TLA+ in two versions, a detailed one and a simpler one, and uses the TLC model checker to test that the protocol gives Snapshot Isolation, stated with a client-centric specification.
- number: Abstract model, Snapshot Isolation check: 2 keys, 2 partitions, 2 txns 3 s; 3 txns 3 min 28 s; 3 keys, 2 partitions, 3 txns 11 h 23 min 20 s; 3 keys, 3 partitions, 3 txns timed out (Table 10)
- number: Detailed model: 3 keys, 2 partitions, 2 txns 21 min; most larger cases timed out (Table 9)
- number: Symmetry and view features cut one 2-key, 2-partition, 3-txn state-space run from 2 h 54 min to 2 min 2 s (Table 8)
- number: Machine: i7-7700HQ, 16 GB RAM; each time is the average of 3 runs; maximum runtime 12 hours
- limits: Bounded to at most 3 transactions, keys, partitions; the target of 3/3/3 was not reached. The abstract model removes the message system, so it does not cover the real messaging. Only the safety property (Snapshot Isolation) is checked; no liveness. Chapters 2-3 (background) and the model listings in 4.1-4.2 were skimmed.
- how much was read: parts read
- source; notes: ## Formal modelling and analysis of Clock-SI with TLA+ (2025)
- record id: clock-si-tla-2025
Design and Modular Verification of Distributed Transactions in MongoDB (2025)
- what: A TLA+ spec of MongoDB distributed transactions, with a modular spec of the interface. A follow-up blog generates conformance tests against WiredTiger.
- number: TLA+ spec about 571 lines plus storage spec about 332 lines
- number: 87,143 generated tests in about 40 minutes on a small finite model (2 keys, 2 transactions)
- limits: It is tested only. Code is at https://github.com/mongodb-labs/vldb25-dist-txns.
- how much was read: parts read
- record id: design-and-modular-verification-2025
Korg thesis (2025)
- title: Verification and Attack Synthesis for Network Protocols
- what: Proves properties of three network-protocol pieces with theorem provers (Karn’s RTT algorithm and TCP’s timeout rule in Ivy and ACL2s, and Go-Back-N efficiency in ACL2s), model-checks TCP, DCCP and SCTP handshakes in SPIN, then builds Korg, a tool that searches for attacker behaviour that breaks a given property.
- number: Handshake properties: TCP 4 (phi1-phi4), SCTP 10 (gamma1-gamma10), DCCP has its own set
- number: Korg asked for at most 10 attacks per property; default search depth 600,000, maximum 2,400,000
- number: TCP phi3 (peers do not get stuck) took 72 min to 223 min per attacker model; other TCP properties took seconds
- number: SCTP: one patched-vs-unpatched check; with the CVE-2021-3772 patch, Korg finds no off-path attack, which proves the patch closes it for the model
- limits: Models are small by design to avoid state-space explosion; the handshake models are not linked to the Ivy/ACL2s models. Korg handles one centralized attacker, not coordinated multi-process attackers, and is exact only for the model, not the real code. Models took long to write by hand.
- how much was read: parts read
- source; notes: ## Von Hippel thesis on protocol verification and attack synthesis (20
- record id: korg-thesis-2025
PolySemist (2025)
- title: Accelerating Protocol Synthesis and Detecting Unrealizability with Interpretation Reduction.
- what: A tool that fills in the missing guards and updates of a half-written TLA+ distributed protocol (a sketch) so the protocol meets a safety or liveness property. It loops: the TLC model checker finds a counterexample, the tool rules out every candidate that shares it, and it skips candidates that behave the same on the states seen so far.
- number: 7 benchmark protocols: 2PC, consensus, decentralized lock, lock server, sharded KV store, two reconfigurable Raft variants
- number: faster than the previous tool Scythe in 160 of 171 realizable problems; total time about 9,000 s vs 32,000 s on those both solve
- number: whole distributed-lock protocol (6 expressions over 2 actions) synthesized in 125 s; Scythe timed out at 1 hour
- number: detected ‘no protocol exists’ in 80 of 123 unrealizable problems vs 16 for Scythe (easy 46/50, medium 21/35, hard 13/38)
- limits: A human supplies the sketch (state variables, actions, hole grammars) and the property; results hold only for the chosen finite parameters (e.g. number of nodes), and the all-parameters step is left to TLAPS proofs from prior work. Termination is guaranteed only when each hole grammar has finitely many expressions up to interpretation equivalence.
- how much was read: parts read
- source; notes: ## PolySemist: protocol synthesis by sketching (2025)
- record id: polysemist-2025
Shipwright (2025)
- title: Shipwright: Proving liveness of distributed systems with Byzantine participants
- what: A Dafny framework. A node is written as event handlers and compiled to Go. A refinement proof shows that the real handlers, running over a network model that eventually stabilizes, give safety and liveness. The case study is PBFT agreeing on one log entry, with infinitely many views.
- number: Shipwright 13,357 lines (1,351 trusted); PBFT implementation 31,138 lines (266 trusted)
- number: total 1,617 trusted, 42,878 untrusted, 44,495 lines
- number: proof found three liveness bugs (bad new-view signatures, wrong certificate counting, timer started too early)
- number: implementation 1888 lines (Figure 11, PDF p.11)
- limits: It assumes partial synchrony (the network eventually stabilizes), an unverified Go runtime, and unforgeable signatures. It covers only one PBFT iteration. Reply messages to clients are not in the top-level theorem. Some refinements are unfinished. Person-time is not given.
- how much was read: parts read
- source
- record id: shipwright-2025
Vest (2025)
- title: Vest: Verified, Secure, High-Performance Parsing and Serialization for Rust
- what: Users describe a binary format, and Vest generates Rust parsers and serializers verified in Verus. It uses a reusable combinator library.
- number: about 6K library lines, verified in under ten seconds
- number: DSL compiler 5,807 Rust lines
- number: format descriptions: Bitcoin about 67 lines, TLS 1.3 about 500, WebAssembly about 600
- limits: It proves that parse and serialize are inverses, plus memory safety. It does not prove consensus or handshake security. Timing side channels are not a Verus theorem. The DSL frontend is unverified.
- how much was read: parts read
- source; notes: Vest: Verified, Secure, High-Performance Parsing and Serialization for
- record id: vest-2025
ZENITH (2025)
- title: ZENITH: Towards A Formally Verified Highly-Available Control Plane
- what: A microservice SDN (software-defined networking) controller. Its TLA+/PlusCal spec is verified to ensure that the network state eventually matches the intent. Code is generated from the spec.
- number: spec is 8.6K lines
- number: eight properties P1-P8 proved by hand in TLAPS
- number: 26 race conditions from prior SDN controller bugs (9 state inconsistencies, 7 deadlocks)
- limits: The code generator is assumed correct, as with PGo. Model checking alone does not scale across topologies. TLAPS needed history variables (extra variables recording the past). Person effort is not given.
- how much was read: parts read
- record id: zenith-2025
Fairneris (2024)
- title: Fairneris: Verifying Liveness Properties of Distributed Systems via Trace Refinement in Higher-Order Concurrent Separation Logic
- what: An AnerisLang implementation of Stenning transfer over UDP-like networking. Under fair scheduling and a fair network (nothing is delayed forever), every sequence number is eventually acknowledged. Coq checks the refinement (that the code matches the model) and most of the infrastructure.
- limits: The model’s liveness theorem is a pen-and-paper proof, not machine-checked. The review notes did not establish the venue, date or artifact.
- how much was read: parts read
- source; notes: papers and boundaries
- record id: fairneris-2024-2
Kondo (2024)
- title: Inductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline Distributed Protocol Proofs
- what: Kondo derives inductive invariants for Dafny protocol proofs from the protocol’s structure. This reduces the invariants the user must write.
- number: Paxos: 418 lines, Kondo needs 20 user invariants, 777 total proof lines, 42.9 s
- number: IronFleet 4,581 lines of Dafny and Verdi 50,000 lines of Coq for manual proofs
- number: Paxos row: 631 model lines; 27 invariant clauses without Kondo vs 20 synchronous; 856 proof lines without Kondo vs 557 synchronous plus 220 modified
- number: Table 1 p. 848: 10 systems (Echo Server, Ring Leader Election, Simplified Leader Election, Two-Phase Commit, Paxos, Flexible Paxos, Distributed Lock, ShardedKV, ShardedKV-Batched, Lock Server)
- limits: Liveness proofs are beyond its scope. Line counts are not measured human hours.
- how much was read: parts read
- source; notes: papers inspected
- record id: kondo-2024
RefinedRust (2024)
- title: RefinedRust: A Type System for High-Assurance Verification of Rust Programs
- what: A tool that checks Rust code, including unsafe code that uses raw pointers, against hand-written specs and emits a proof that the Coq proof assistant checks, so the tool itself need not be trusted. Demonstrated on a simplified Vec (growable array).
- number: Vec and RawVec APIs: 120 lines of code, 76 lines of annotations, about 1200 lines of generated Coq
- number: verification takes about 6 minutes wall time (22 minutes CPU) on an Apple M1 Max
- number: for Vec::pop: about 3,000 automatic steps, 100 side conditions, all but five solved automatically, about 20 lines of manual Coq
- number: type system formalization: about 21k lines of specification and 14k lines of proof; about 80 lines of manual Coq for Vec’s invariant
- limits: Only sequential code: no concurrency, traits, closures, recursive types or unsized types. Trusts the Rust model (Radium) and the Rust-to-Coq frontend. The Vec code is simplified from the standard library.
- how much was read: parts read
- source; notes: RefinedRust (2024)
- record id: refinedrust-2024
SandTable (2024)
- title: SandTable: Scalable Distributed System Model Checking with Specification-Level State Exploration
- what: It model-checks a TLA+ spec quickly, then replays the bug traces in the code. A conformance checker replays model traces to find places where the spec and code differ.
- number: 23 bugs, 18 new, 17 confirmed, 13 fixed
- number: Half a person day to a few person days to fix modeling errors; two person weeks adapting ZooKeeper specs
- number: 114x-2989x faster state exploration
- number: abstract: 18 new bugs, 17 confirmed, 13 fixed (the note’s sentence adds ‘out of 23 total’ garbled)
- limits: It cannot guarantee that no differences remain between the spec and the implementation.
- how much was read: parts read
- source; notes: P10. SandTable: Scalable Distributed System Model Checking with Specif
- record id: sandtable-2024
Trillium / Fairis (2024)
- title: Trillium and Fairis
- what: A program-logic framework in Coq and Iris. Fairis proves liveness of concurrent programs under fair scheduling, by refinement of a model. The Aneris instantiation proves that distributed implementations refine TLA+ models (two-phase commit, single-decree Paxos and a CRDT).
- number: about 1100 lines of proof scripts for Paxos
- limits: The step from TLA+ to the Coq model was done manually. The distributed refinements give trace safety only. Distributed liveness is in a later manuscript. The notes’ author read about 40%.
- how much was read: parts read
- source
- record id: trillium-fairis-2024
Yao thesis (DistAI, DuoAI, LVR) (2024)
- title: Automated Verification of Safety and Liveness Properties for Distributed Protocols (PhD thesis)
- what: It shows that liveness can be reduced to a list of simpler safety properties, which invariant-inference tools often prove automatically. One task is left: synthesize a ranking function (a number that decreases toward the goal) to prove termination. It was applied to 8 protocols, including Paxos. It also covers DistAI and DuoAI.
- number: 37 of 40 generated safety properties are always true, inductive, or get an invariant automatically; 3 found manually in a few hours each
- number: every Z3 query to synthesize a ranking function finished in under a second
- number: manual effort 128 and 165 lines versus IronFleet’s 2,093 and 7,869 lines of Dafny (16x and 47x less)
- number: DuoAI covers 27 protocols and solves Paxos more than two orders of magnitude faster than any alternative
- limits: It handles only “eventually” properties, not bounded time. Ranking functions are polynomials only. It works on protocol-level models, not code. It assumes fair scheduling, minimum packet delivery and a contention-free Paxos round. Part of the line-count gap is Dafny versus mypyvy. The notes’ author read about 20% of the 137 pages.
- how much was read: parts read
- source
- record id: yao-thesis-distai-duoai-lvr-2024
A Case Study on Parametric Verification of Failure Detectors (2023)
- what: The authors model the Chandra-Toueg failure detector (a protocol that guesses which machines have crashed) in TLA+, Ivy and counter automata, assuming partial synchrony (the network is unpredictable at first, then becomes well-behaved). They prove liveness (something good eventually happens) by hand, turning it into a safety proof (nothing bad happens).
- limits: The conversion from liveness to safety is done by hand. Ivy’s automatic conversion was not used.
- how much was read: parts read
- source
- record id: a-case-study-on-2023
ByMC survey (2023)
- title: Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
- what: Protocols are modeled by counting messages and participants against thresholds. This lets the tool check safety, and some liveness, for any number of participants, under conditions like n>3t (n participants, at most t faulty).
- number: Table 4: 13 asynchronous/randomized algorithms (FRB, STRB, ABA, NBACG, NBACR, CBC, CF1S, C1CS, BOSCO, Ben-Or, RABC, kSet, RS-BOSCO)
- number: Table 6: 16 synchronous cases, 14 verified; HybridQueen and kSetOmit have no successful check
- limits: People still supply the models and assumptions. Termination of randomized protocols holds only against adversaries that act in rounds. The Tendermint claim covers one round only. The synchronous checker is a separate prototype.
- how much was read: parts read
- source; notes: ByMC and threshold automata
- record id: bymc-survey-2023
IronSync (2023)
- title: Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems
- what: It connects ownership reasoning (who may access what) for thread-local code to a global transition model. Cases: a NUMA node-replication library, and SplinterCache, a concurrent page cache.
- number: 2747 lines of non-ghost implementation plus 316 of shared library, for all four concurrent examples (§7.1, PDF p.12)
- limits: It covers shared-memory systems, not networking. It does not verify liveness, termination or freedom from deadlock. It trusts the framework’s axioms and the memory model.
- how much was read: parts read
- source; notes: papers; notes: Sharding the State Machine: Automated Modular Reasoning for Complex Co
- record id: ironsync-2023
Lessons from Formally Verified Deployed Software Systems (2023)
- what: A survey of 32 formally verified deployed systems, mostly not distributed.
- number: 22 of 32 depend on unverified code elements
- number: HACL* proof-to-code ratio about 2, up to 6
- number: Vericert: about 3 person-months implementation, 15 person-months proofs
- limits: The notes’ author did not mine the full survey.
- how much was read: parts read
- source
- record id: lessons-from-formally-verified-2023
PGo (2023)
- title: Compiling distributed system models with PGo
- what: It compiles Modular PlusCal models into Go.
- number: Table 2 (MPCal SLOC; glue SLOC; effort): lock service 67; 87; 2 person-days; Raft 771; 676; 22 person-days; distributed KV 256; 383; 3 person-days; primary-backup KV 420; 270; 10 person-days; state-based CRDT 160; 185; 10 person-days
- number: monolithic RaftKV: 25 person-days, 758 model lines, 1099 glue lines
- limits: It gives no guarantee about the compiler.
- how much was read: parts read
- source; notes: P07. Compiling Distributed System Models with PGo; notes: papers
- record id: pgo-2023
Proving Refinement in a Rust Verifier (MSc thesis) (2023)
- what: A way to prove that a Rust program, checked by Prusti, refines a TLA+ model (every step of the program matches a step of the model). The model state is ghost state (proof-only state) behind a “ghost lock”. Each implementation step takes the lock to perform one model step.
- number: Paxos acceptor phases: 112 model / 132 implementation / 152 proof lines (3.5 min)
- number: lock-free hash set: 123 / 57 / 376 lines (3 min)
- limits: It covers safety only. Prusti lacks support for ghost code. The translation from TLA+ is manual and not implemented as automatic. The notes’ author read about 35%.
- how much was read: parts read
- source
- record id: proving-refinement-in-a-2023
Adore (2022)
- title: Adore: Atomic Distributed Objects with Certified Reconfiguration
- what: Adore describes a distributed protocol’s state at a high level. It tracks which parts are committed and which are not, and hides packet details. A Coq proof shows that a Raft-like protocol, SRaft, correctly implements Adore (a refinement). Adore covers several ways of changing cluster membership, chosen by parameters.
- number: about 13.8k Coq lines overall; 2.5k for SRaft-to-Adore refinement
- number: 2 weeks for CADO safety plus another 3 for reconfiguration, five person-weeks, abstract safety only (§7, PDF p.13)
- number: 13.8K lines for the full Raft development
- limits: The proof is about the protocol, not application code. It makes no claim that the system eventually makes progress or stays available.
- how much was read: parts read
- source; notes: papers; notes: Adore: Atomic Distributed Objects with Certified Reconfiguration
- record id: adore-2022
Applying Formal Verification to Microkernel IPC at Meta (2022)
- what: Meta proved two lock-free queues, used for message passing between processes in an OS under development, using Iris and Coq. The proofs cover verified pseudocode of the algorithm, not the C code.
- number: Entire IPC implementation about three thousand lines
- number: Six months with two engineers
- limits: The specs say nothing about liveness (that operations eventually finish). A queue whose operations loop forever would satisfy them.
- how much was read: parts read
- source
- record id: applying-formal-verification-to-2022
Op-based CRDTs (2022)
- title: Modular Verification of Op-Based CRDTs in Separation Logic
- what: A reliable causal broadcast library and OpLib, so that a data type can be verified without redoing the proofs about packets and threads. Twelve examples: counters, sets, registers, combinators, composed maps.
- limits: Proves convergence when replicas have received equal sets of operations. It does not prove eventual delivery, which counts as a progress property.
- how much was read: parts read
- source; notes: papers; notes: Modular Verification of Op-Based CRDTs in Separation Logic
- record id: op-based-crdts-2022
Sift (2022)
- title: Sift: Using Refinement-guided Automation to Verify Complex Distributed Systems
- what: Starting from a specification, an implementation model and intermediate layers, it turns each layer-to-layer obligation into a safety problem. It infers invariants with IC3PO and generates C++ with Ivy.
- number: six cases: leader election, distributed lock, two-phase commit, sharded hash table, Raft, Multi-Paxos
- number: manual work under five minutes for the three small cases, one person-month for Raft, three person-weeks for Multi-Paxos
- number: Raft proof effort 1 person-month
- number: MultiPaxos effort 3 person-weeks
- limits: The top-level abstraction proofs for Raft and Multi-Paxos are manual or reused. Imperative optimizations may need loop invariants written by hand. It targets C++, not Rust.
- how much was read: parts read
- source; notes: papers inspected; notes: Sift: refinement from protocol down to executable systems
- record id: sift-2022
Aneris causal memory (2021)
- title: Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic
- what: Specifies a causally consistent database (one where an effect is never seen before its cause). Servers and clients are proved separately, and a session manager adds guarantees for each client on top.
- limits: It proves the code does the right thing through separate specs for each part. It makes no promise about response time. The collection filename says 2022 but the paper says 2021.
- how much was read: parts read
- source; notes: Distributed Causal Memory: Modular Specification and Verification in H
- record id: aneris-causal-memory-2021
Civl FMCAD 2021 (2021)
- title: The Civl Verifier
- what: Describes a static verifier for concurrent programs. It proves a program in layers, where each layer is shown to match the one above. It uses checks for interference between threads, a step-merging technique called reduction, and permissions. Case studies include garbage collection, Paxos and locks.
- limits: The test suite is a repository that keeps changing. It is not a fixed protocol benchmark. Pin a commit.
- how much was read: parts read
- source; notes: Civl and inductive sequentialization; notes: S16
- record id: civl-fmcad-2021-2021
Paxos with IC3PO (2021)
- title: Towards an Automatic Proof of Lamport’s Paxos
- what: Uses IC3PO along a hierarchy of simpler protocols chosen by a human: Voting, SimplePaxos, ImplicitPaxos, Paxos, then Flexible Paxos and Multi-Paxos. It passes strengthening assertions (extra facts that make the proof go through) upward.
- number: Pages 112-122
- limits: The hierarchy of abstractions, and its link to the intended system, are separate human work.
- how much was read: parts read
- source; notes: papers inspected; notes: IC3PO and its shared ivybench collection
- record id: paxos-with-ic3po-2021
ShardStore (2021)
- title: Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3
- what: Executable reference models and checks for the S3 ShardStore storage node.
- number: Reference models about 1% of implementation code
- number: Checks and harnesses 12% of the code base
- number: Prevented 16 issues from reaching production
- number: 18% of reference model and harness code written by the engineering team
- limits: Passing the checks does not mean the code is correct.
- how much was read: parts read
- source; notes: papers; notes: Using Lightweight Formal Methods to Validate a Key-Value Storage Node
- record id: shardstore-2021
Civl refinement CAV 2020 (2020)
- title: Refinement for Structured Concurrent Programs
- what: This paper moves refinement reasoning (showing that a detailed program implements a simpler one) into structured concurrent programs. It uses yield invariants and permissions.
- limits: The paper has no fixed, complete list of protocol benchmarks.
- how much was read: parts read
- source; notes: Civl and inductive sequentialization; notes: S15
- record id: civl-refinement-cav-2020-2020
eXtreme Modelling (2020)
- title: eXtreme Modelling in Practice
- what: MongoDB compared two ways to link a model to code. One is model-based trace checking (MBTC), which checks whether logged runs fit the model. The other is model-based test-case generation (MBTCG). Trace checking of replication was impractical. For Realm Sync’s operational-transformation rules, a Go generator turned TLC states into C++ tests.
- number: Realm Sync table (§5.2): 795 TLA+ lines, 755 Go lines, 4 weeks total effort
- number: Abandoned trace checking after 10 weeks
- number: 4913 generated tests reached 100% branch coverage vs 21% handwritten and 92% AFL fuzzer
- limits: Trace checking of replication struggled with the level of abstraction, concurrency, incomplete observations, and keeping code and model in sync. The generated tests cover local merge behavior, not the whole distributed product.
- how much was read: parts read
- source; notes: P04. eXtreme Modelling in Practice
- record id: extreme-modelling-2020
Inductive sequentialization (2020)
- title: Inductive Sequentialization of Asynchronous Programs
- what: The user supplies a simpler sequential ordering of the steps of an asynchronous program, plus evidence that steps can be swapped (commute). A checked induction then shows the simplification is sound.
- number: Table 1 (7 problems): Broadcast consensus 396/108/121 LOC 1.0s; Ping-Pong 281/91/106; Producer-Consumer 225/65/93; N-Buyer 681/251/256; Chang-Roberts 377/117/135; 2PC 553/181/222; Paxos 1168/534/302, 4.2s
- number: IS applications: 2,1,1,4,2,4,1
- limits: It asserts no liveness result. The review notes found no measurement of human hours. The line counts include boilerplate.
- how much was read: parts read
- source; notes: Civl and inductive sequentialization
- record id: inductive-sequentialization-2020
Logres (2020)
- title: A Formally Verified Protocol for Log Replication with Byzantine Fault Tolerance
- what: A log replication protocol that runs in lock-step rounds (the Heard-Of model), uses signatures, and tolerates Byzantine faults. Its proof in Isabelle/HOL includes liveness.
- number: About 300 lines for the protocol model and 1000 lines for the proofs
- number: IronFleet took about 3.7 person-years (the paper’s figure)
- limits: Liveness is cheap here because the model is lock-step, with no leader and no timing. That is the notes’ inference. The proof is a counting argument, not a fairness argument.
- how much was read: parts read
- source
- record id: logres-2020
Apalache (2019)
- title: Apalache: temporal properties tutorial, feature table and TLA+ model checking made symbolic
- what: Apalache is a model checker for TLA+ that works on symbols instead of listing states, using an SMT solver. It checks state, action and trace invariants, inductive invariants (a property that holds at the start and is preserved by every step) and temporal properties.
- limits: Apalache parses ASSUME but does not pass it to the solver. It does not use THEOREM. Its bounded checks do not prove properties for unbounded runs. The authors did not read the original paper.
- how much was read: parts read
- source; notes: tools; notes: Model checking: what a successful run means
- record id: apalache-2019
HotStuff (2019)
- title: HotStuff: BFT Consensus in the Lens of Blockchain
- what: HotStuff is BFT consensus (it tolerates arbitrarily faulty replicas) with n=3f+1 replicas, a known delay bound Δ and an unknown GST. If a correct leader stays in one view long enough after GST, Basic HotStuff decides. A Pacemaker keeps replicas and leaders in step.
- limits: The argument is handwritten. The deployed Pacemaker is not machine-checked. The chained variant needs two consecutive correct leaders, and its liveness argument is omitted for brevity. Completing in a single view does not establish that this view is eventually selected (an inference).
- how much was read: parts read
- source; notes: HotStuff; notes: Consensus: where the assumptions enter the proof
- record id: hotstuff-2019
Pretend Synchrony / Goolong (2019)
- title: Pretend synchrony: synchronous verification of asynchronous distributed programs
- what: Verifies Go distributed programs by automatically rewriting them into an equivalent synchronous program (messages become assignments), then checking ordinary verification conditions with the Z3 solver. Four case studies: two-phase commit, Raft leader election, single-decree Paxos, Multi-Paxos key-value store.
- number: manual invariant annotations reduced by 6x versus Dafny
- number: check time 1.73 s total vs 1455.84 s in Dafny for the three protocols
- number: Paxos 504 lines of Go, 14 loop-invariant lines, 1.51 s; Dafny 72 invariant lines, 1141.35 s
- number: Multi-Paxos KV: 847 Go lines, 1.64 s check, 118.5 req/ms, within 1.5-3x of unverified EPaxos code
- limits: Safety only, no liveness. Needs structured loops, symmetric process ids, typed channels, pairwise communication and round non-interference; rules out Multi-Paxos stable-leader optimization, Stoppable Paxos and ring topologies such as Chord.
- how much was read: parts read
- source; notes: Pretend Synchrony (2019)
- record id: pretend-synchrony-goolong-2019
Disel (2018)
- title: Programming and Proving with Distributed Protocols
- what: Proves distributed components and their clients in Coq against protocol descriptions, and composes their contracts. A protocol can be strengthened for one client without redoing the component proofs.
- number: about 4,500 lines of framework metatheory
- number: two-phase commit core: 997 definition/spec lines and 2,113 proof lines; nine person-days
- number: trusted OCaml shim about 250 lines
- number: nine person-days for the core two-phase-commit development (§8, PDF p.24)
- limits: Safety only.
- how much was read: parts read
- source; notes: papers and boundaries; notes: Programming and Proving with Distributed Protocols
- record id: disel-2018
Tendermint (2018)
- title: The latest gossip on BFT consensus
- what: The paper presents the Tendermint algorithm. It proves that, after GST, a favorable round arises from the proposer rotation, the growing timeouts and the gossip. Then all correct participants decide.
- number: faulty voting power below one third of total
- limits: The proof is handwritten. It says nothing about verifying current Tendermint successors. The fault unit is voting power, not replica count. The page reference for lemma 7 in the inherited review was wrong for the v3 the review notes inspected.
- how much was read: parts read
- source; notes: Tendermint; notes: Consensus: where the assumptions enter the proof
- record id: tendermint-2018
Velisarios (2018)
- title: Velisarios: Byzantine Fault-Tolerant Protocols for Verified Distributed Systems
- what: It proves agreement for an executable Coq implementation of PBFT: correct replicas return the same reply for the same client and timestamp. Code is extracted to OCaml with a networking and cryptography runtime.
- number: PBFT evaluation uses desktops with 16 GB RAM and 8-core 3.40 GHz i7-6700 CPUs
- number: Single-machine simulation: 1 million requests, 27.6 microseconds average for f=1 replies
- number: Primary failure recovery took around 7 seconds
- number: Compared response times with BFT-SMaRt for f=1–3
- limits: The theorem assumes authenticated origins, correct keys, and a bound on the number of faulty nodes. Linearizability, liveness and timeliness are left for future work. The runtime and cryptographic assumptions stay in the trust boundary.
- how much was read: parts read
- source; notes: Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq; notes: Velisarios: Byzantine Fault-Tolerant Protocols for Verified Distribute
- record id: velisarios-2018
ConsL cutoff (2017)
- title: Cutoff Bounds for Consensus Algorithms
- what: It describes round-based consensus algorithms in a small language, ConsL. It proves bounds on how many processes are enough to check. It translates the algorithms to Promela/LTL for the Spin model checker.
- number: Table 2: 9 cases (Paxos, Paxos 3 rounds, Chandra-Toueg, an algorithm from Consensus Refined, 1/3-rule, coordinated uniform voting, simplified version, uniform voting variant, Ben-Or)
- number: Cutoffs: 5 processes, except 1/3-rule at 7
- number: Pages 217-237
- limits: Progress claims keep the communication assumptions. Failed processes keep receiving, but their messages are suppressed. Ben-Or termination here is not termination with probability one against arbitrary adversaries. The notes did not recover the generated model download.
- how much was read: parts read
- source; notes: Cutoff and bounded instantiation leads
- record id: consl-cutoff-2017
CertiKOS (2016)
- title: CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels
- what: CertiKOS specifies an interface and the visible events at each kernel layer. It proves that a module can stand in for its specification in the contexts it allows (this is called contextual refinement). The mC2 kernel is proved in Coq.
- number: Under 2 person-years for supporting concurrency
- number: 6500 lines of C and x86 assembly
- limits: The 2 person-years is the cost of adding concurrency support, not the cost of a whole new kernel.
- how much was read: parts read
- source; notes: S9
- record id: certikos-2016
Chapar (2016)
- title: Chapar: Certified Causally Consistent Distributed Key-Value Stores
- what: Chapar states the public causal-visibility rule separately from the store internals. The rule says that if an update is visible, its dependencies are visible. The authors prove two store algorithms and extract OCaml. They verify client examples, such as publishing a photo before a post that refers to it.
- limits: It trusts serialization and the runtime infrastructure.
- how much was read: parts read
- source; notes: papers; notes: Chapar: Certified Causally Consistent Distributed Key-Value Stores
- record id: chapar-2016
Verdi Raft (2016)
- title: Planning for Change in a Formal Verification of the Raft Consensus Protocol
- what: The authors complete the proof of Raft state-machine safety in Verdi. They manage changes across interdependent invariants by hiding definitions behind interface lemmas.
- number: 90 system invariants discovered and proved
- number: about 45000 additional lines on top of an earlier roughly 5,000-line proof
- number: 530 lines of code and 50,000 lines of proof
- number: 530 lines of code and 50,000 lines of proof (Raft development only, §5, PDF p.5)
- limits: It proves safety only. It excludes dynamic membership and log compaction.
- how much was read: parts read
- source; notes: S34
- record id: verdi-raft-2016
AWS formal methods (2015)
- title: Use of Formal Methods at Amazon Web Services (How Amazon Web Services Uses Formal Methods)
- what: AWS engineers used TLA+ and TLC to explore distributed designs and find subtle bugs, including in replication and recovery designs. It is the clearest industrial statement of the gap between model and code.
- limits: It checks designs only and does not prove the deployed code correct. The linked manuscript is dated 29 September 2014 and differs from the final publication.
- how much was read: parts read
- source; notes: P01. How Amazon Web Services Uses Formal Methods; notes: papers
- record id: aws-formal-methods-2015
Matichuk et al. (seL4 proof size study) (2015)
- what: The study compares the size of seL4 proofs with the size of the statements they prove.
- number: 15,018 lemmas, about 215,000 lines of proof
- how much was read: parts read
- record id: matichuk-et-al-sel4-2015
seL4 comprehensive (2014)
- title: Comprehensive formal verification of an OS microkernel
- what: It details seL4’s refinement from the abstract spec to the executable design and then to C. It also covers security and binary checks, assumptions and effort.
- number: About 20 person-years (py) for the correctness proof, including framework work
- limits: Binary verification and hardware assumptions are discussed in Sections 4.7-4.8. Do not carry the historical boundaries over to current versions.
- how much was read: parts read
- source; notes: S10
- record id: sel4-comprehensive-2014
Formal Verification of Distributed Algorithms: From Pseudo Code to Checked Proofs (2012)
- what: Isabelle/HOL proofs of safety and liveness for consensus algorithms. They use a transition system with explicit runs. The examples are a Rotating Coordinator, Chandra-Toueg consensus and Paxos.
- number: approximately 10k lines of Isabelle/HOL per algorithm
- limits: The work is old and manual. The review notes read about 50% of it.
- how much was read: parts read
- source
- record id: formal-verification-of-distributed-2012
Heard-Of (AFP) (2012)
- title: Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model
- what: Isabelle proofs of six consensus algorithms in the Heard-Of model. Two ways of defining runs are linked by a reduction theorem. Termination of LastVoting is proved under a “communication predicate” (a condition on which messages arrive) instead of weak or strong fairness.
- number: six consensus algorithms (OneThirdRule, Uv, LastVoting, Ute, Ate, Eigbyz)
- limits: The communication predicate is a strong assumption about the environment: a good phase in which a coordinator hears a majority and everyone hears the coordinator. The user must argue that it is realistic (the notes’ inference).
- how much was read: parts read
- source
- record id: heard-of-afp-2012
seL4 process study (2012)
- title: Large-Scale Formal Verification in Practice: A Process Perspective
- what: A study of the process of verifying seL4.
- number: Design verification consumed roughly 60-70% of time and effort
- number: Less than 14 person-years for kernel design, development and verification
- number: Integrity and authority confinement took 10 person months
- number: Maintenance about one full-time person
- how much was read: parts read
- source; notes: S35
- record id: sel4-process-study-2012
CompCert (2009)
- title: Formal verification of a realistic compiler
- what: CompCert, a verified C compiler written in Coq. Gives the classic ratio of effort for a verified system.
- number: 42000 lines of Coq, approximately 3 person-years
- number: 14% compilation algorithms, 10% semantics, 76% correctness proof
- number: each compilation pass takes 1500 to 3000 lines for spec and proof
- number: 42000 lines of Coq and approximately 3 person-years (that historical version)
- limits: Only the paragraph on effort was read.
- how much was read: parts read
- source; notes: S14
- record id: compcert-2009
Proving that non-blocking algorithms don’t block (2009)
- what: The first fully automatic tool to prove non-blocking liveness (lock-free and obstruction-free) of concurrent data structures. It uses rely-guarantee reasoning (each thread assumes what others do and promises what it does), shape analysis and a termination prover.
- number: lock-freedom proofs found in under 10 minutes for all cases except Michael’s list, which took about 8 hours
- number: found a linked-list deletion in Fomitchev and Yahav that is not obstruction-free
- limits: It is not about distributed systems. The review notes read about 25% of the paper.
- how much was read: parts read
- source
- record id: proving-that-non-blocking-2009
seL4 (2009)
- title: seL4: Formal Verification of an OS Kernel
- what: This is a proof in Isabelle that a microkernel’s implementation refines (correctly implements) its spec.
- number: 8,700 lines of C
- number: 200,000 lines of Isabelle script
- number: Abstract spec took about 4 person months
- number: Refinement statements at most 20% of effort
- limits: It is a historical baseline. The 2014 paper has the expanded stack and the effort analysis.
- how much was read: parts read
- source; notes: S11
- record id: sel4-2009
PBFT (1999)
- title: Practical Byzantine Fault Tolerance
- what: Clients eventually get replies if at most (n-1)/3 replicas are faulty and message delays do not grow faster than the timeout forever. The proof raises view timeouts, gets correct replicas into the same view, and rotates primaries until a correct one has enough time.
- limits: Read in the official HTML because the PDFs failed. The delay condition is specific to this paper. It is not the modern GST contract.
- how much was read: parts read
- source; notes: Consensus: where the assumptions enter the proof; notes: PBFT
- record id: pbft-1999
PVerifier
- title: PVerifier (P language verification extensions)
- what: It checks inductive proofs of designs written in the P language. Users supply assumptions and an inductive invariant. UCLID5 and an SMT solver check that the invariant holds initially, that each step preserves it, and that it implies the desired property. A two-phase-commit tutorial shows that if the protocol accepts, every participant preferred acceptance.
- limits: The claim holds for the supplied P design under its assumptions. The 2PC tutorial proves no theorem that the protocol completes despite crashes. An internal verification of sharded transactions with snapshot isolation is reported by the author, and its details are unreleased.
- how much was read: parts read
- source; notes: PVerifier
- record id: pverifier
tla-rs
- what: Ports the AutoMan workflow to Rust and Verus. In the RSL and Raft theorems the review notes inspected, finite behaviors of the distributed model are proved to refine an abstract spec. The Raft theorem maps behavior to an abstract behavior of the committed log.
- limits: It covers safety correspondence only, with no theorem about eventual progress. Collection helpers are marked external_body, so their contracts are not checked against their bodies. The scheduler, unsafe syscall glue, identity and TLS are outside the body proofs. Verification counts and benchmarks are the authors’ reports, which the review notes did not reproduce.
- how much was read: parts read
- source; notes: tla-rs primary source audit
- record id: tla-rs
verified-nrkernel
- what: Verified single-threaded page-table management for an OS, in Verus.
- number: 288 verified, 0 errors
- limits: It is currently single-threaded.
- how much was read: parts read
- source
- record id: verified-nrkernel
Verus state machines
- title: Verus State Machines Tutorial and Reference
- what: Shows how to model a program as a tokenized state machine. Shows how the tool checks the inductive conditions (true at the start, preserved by each step) for each initializer and transition. A counter example shows why a stronger invariant is needed.
- how much was read: parts read
- source; notes: D2
- record id: verus-state-machines
A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report (2026)
- what: The authors translate production Rust cryptographic code into Lean 4 using Charon/Aeneas or Hax. The target is formal cryptography spec libraries. AI provers (Aristotle, Aleph) then finish the proofs that are still open. They applied this to Plonky3 and RISC Zero. Lean’s small trusted core checks every proof. Aleph proved two bounds theorems that had been left as unproved placeholders (sorry).
- limits: The abstract is cut off before the results on which proof goals the AI closed.
- how much was read: only abstract or first pages read
- source
- record id: a-rust-to-lean-2026
Apalache (2026)
- title: The TLA+ Model Checker Apalache
- what: Describes Apalache, a symbolic TLA+ model checker using SMT, with bounded verification, randomized symbolic execution, and inductiveness checking. A Byzantine consensus case study shows safety and liveness-to-safety workflows and their cost.
- number: Consensus instance n=6, t=1, f=1: bound 10 took 26 min 43 s before abstraction and 1 min 24 s after
- number: Bound 15 took about 47 h; 100 symbolic simulations took about 17 min
- number: 13 lemmas took about 15 h of experienced-author work to discover
- number: 40 experiments over 10 protocols; Apalache answered 8 cases TLC could not
- limits: Inductiveness checking requires a user-provided invariant; unboundedness is only in rounds while node counts remain bounded. Clever abstractions and lemmas are human supplied.
- how much was read: only abstract or first pages read
- source
- record id: apalache-2026
CB-Ver (2026)
- title: CB-Ver: A Stable Foundation for Modular Network Control Plane Verification
- what: CB-Ver verifies that network control planes eventually become stable. The human gives a spec for each component, SMT checks them, and soundness is proved in Lean. It can also synthesize component specs using Constrained Horn Clauses.
- number: benchmarks: fat-tree and Internet2 networks with a 24 h timeout, compared with Timepiece and Minesweeper
- limits: The notes cover only the abstract and the evaluation setup.
- how much was read: only abstract or first pages read
- source
- record id: cb-ver-2026
Deterministic Execution and Margin Enforcement in Financial Transaction Systems: Empirical Evaluation with Formal Safety Verification (2026)
- what: Proposes an order-handling design for trading in which every balance change is appended to a ledger and margin is reserved explicitly, models the accounting core in TLA+, and compares it with two common designs under concurrent load.
- number: Median order latency 9.39 ms, p99 33.70 ms
- number: Optimistic locking accepted $609, 300 o f or d er s a g ain s t$ 100,000 of capital (509.3% over-commitment); the append-only ledger had zero false acceptances
- limits: Only the abstract was available (the TechRxiv PDF page returned an HTML page, not the paper); state-space size, invariant text, model effort and proof size are unknown. The abstract says the property holds ‘within the verified state space’, so it is a bounded model check, not a proof.
- how much was read: only abstract or first pages read
- source; notes: ## Deterministic margin enforcement with TLA+ (2026)
- record id: deterministic-execution-and-margin-2026
Generalized DBLog (2026)
- title: Generalized DBLog: A Verified Contract for Interleaving Copied Rows with a Change Log
- what: This is a verified contract for interleaving table copies with a change log. It covers Netflix DBLog, Debezium and Flink CDC.
- limits: The conditions are of the safety kind (nothing bad happens).
- how much was read: only abstract or first pages read
- source
- record id: generalized-dblog-2026
LLM-assisted Verification of Protocol Implementations for Logic Flaws Using TLA+ (2026)
- what: A pipeline from code to Protocol Intermediate Language to TLA+ to TLC, with feedback. The abstract reports three logic flaws, including WolfSSL 5.8.2 accepting CertificateVerify before ClientKeyExchange.
- number: 3 logic flaws confirmed by the vendor
- number: Three logic flaws identified, confirmed by the vendor (abstract)
- limits: Only the abstract was available. The human inputs, the scope of the proofs and the method are unverified.
- how much was read: only abstract or first pages read
- source; notes: Located but full text unavailable; notes: Located but full text unavailable
- record id: llm-assisted-verification-of-2026
ProofSaX (2026)
- title: Synthesizing Proofs Using Proof Sharding and Exploration
- what: ProofSAX is not an LLM. It splits a proof task into shards and searches annotations in parallel for safety proofs of distributed systems.
- number: finds the last proof annotation in 86 of 103 proof-completion tasks, runtimes one minute to two hours
- number: leader election fully automatic in under two minutes
- number: ten 20-core machines
- limits: It covers safety only. For Paxos and Raft it finds only the last annotation.
- how much was read: only abstract or first pages read
- source
- record id: proofsax-2026
Scaling Verification of Cryptographic Software with Aeneas, Rust, and Lean (2026)
- what: The paper argues that verification still has friction (it takes expertise, and proofs must be maintained as code evolves). It says tools have appeared to reduce it.
- limits: The abstract text in the notes starts mid-sentence and is cut off.
- how much was read: only abstract or first pages read
- source
- record id: scaling-verification-of-cryptographic-2026
SPECA (2026)
- title: Beyond Code Reasoning: Specification-Anchored Auditing of Multi-Implementation Distributed Protocols
- what: SPECA has an LLM read protocol specs (Ethereum consensus) and write categorized properties. It then audits each client against them. These are not proofs.
- number: 15/15 in-scope Fusaka vulnerabilities with expert augmentation, 8/15 automated
- number: About $30 per high/medium/low bug
- limits: The authors say the quality of the generated properties is the main limit.
- how much was read: only abstract or first pages read
- source; notes: specification-anchored auditing
- record id: speca-2026
SureDistrib (2026)
- title: SureDistrib: Verifying Almost-Sure Termination of Composite Asynchronous Byzantine Protocols
- what: SureDistrib is a Rocq framework with refinement and composition lemmas. It gives the first mechanized proof that an asynchronous Byzantine binary agreement algorithm terminates with probability 1. The common coin is treated as a black box.
- limits: The review notes did not extract the effort and read only the introduction and the framework overview.
- how much was read: only abstract or first pages read
- source; notes: SureDistrib: Verifying Almost-Sure Termination of Composite Asynchrono
- record id: suredistrib-2026
The Cross-Domain State Preservation Functor (2026)
- what: An Isabelle/HOL development that claims safety plus starvation-freedom with f < n/3 Byzantine nodes.
- number: 3,215 lines (search summary)
- limits: A company preprint. The theorem and the model of partial synchrony are unchecked.
- how much was read: only abstract or first pages read
- source
- record id: the-cross-domain-state-2026
DafnyMPI (2025)
- what: DafnyMPI is a Dafny library. It proves deadlock freedom, termination, and functional equivalence with sequential implementations of MPI programs. Deadlock freedom comes from preconditions on MPI calls.
- number: Three PDE solver case studies
- limits: The notes cover only the abstract.
- how much was read: only abstract or first pages read
- source
- record id: dafnympi-2025
Fortifying Integrity, Traceability, and Operational Efficacy in Blockchain-Based Examination Management Through Formal Verification with TLA+ (2025)
- what: Models an Ethereum smart contract for exam records in TLA+ (a specification language for state machines), checks it with the TLC model checker for safety and liveness, and maps the TLA+ constructs to Solidity code. Hoare logic (pre- and postconditions) is applied to key functions.
- limits: Full text not obtained (IEEE paywall, no open copy found by Unpaywall or Semantic Scholar); only the abstract was read, so properties checked, state-space size and results are unknown.
- how much was read: only abstract or first pages read
- source; notes: TLA+ for a blockchain exam-management contract (2025)
- record id: fortifying-integrity-traceability-and-2025
Gillian-Rust (2025)
- title: A Hybrid Approach to Semi-automated Rust Verification
- what: Gillian-Rust verifies safe Rust automatically and unsafe Rust semi-automatically, on the Gillian platform. It is linked with Creusot. It verifies real Rust standard library code with minor annotations.
- limits: It is a proof-of-concept tool. Only the abstract was read.
- how much was read: only abstract or first pages read
- source
- record id: gillian-rust-2025
hax / Bert13 (2025)
- title: Formal Security and Functional Verification of Cryptographic Protocol Implementations in Rust
- what: The developer annotates Rust code and picks a backend prover (F*, ProVerif or SSProve) through the hax pipeline. The authors evaluate it on Bert13, a Rust post-quantum TLS 1.3 implementation.
- limits: The full text was unavailable (HTTP 403). Only the abstract was read, so the scope, numbers and effort are unknown. The abstract makes no liveness claim.
- how much was read: only abstract or first pages read
- source; notes: Formal Security and Functional Verification of Cryptographic Protocol
- record id: hax-bert13-2025
Machine Verification of Correctness for a Concurrent Union-Find Object (2025)
- what: A machine-checked proof, written in TLA+ and checked by TLAPS, that the Jayanti-Tarjan randomized-linking union-find objects are strongly linearizable (a property that keeps concurrent behaviour correct even with randomized callers).
- number: proof spans over 16,000 lines
- number: organized into 20 theorems
- limits: Full text not obtained: the Dartmouth Digital Commons PDF link returned a bot-check page and I did not work around it. Only the landing-page abstract was read.
- how much was read: only abstract or first pages read
- source; notes: ## Karun Ram: union-find in TLA+ (abstract only)
- record id: machine-verification-of-correctness-2025
Rust guard refinement (2025)
- title: A Refinement Methodology for Distributed Programs in Rust
- what: The author’s abstract says it combines guards, locally inductive invariants and Rust ownership in a library usable with an off-the-shelf verifier. The case study is a concurrent Memcached.
- limits: The notes’ author read only the abstract. The proof boundary, the verifier and the effort are unaudited. It is not necessarily based on Verus.
- how much was read: only abstract or first pages read
- source; notes: A Refinement Methodology for Distributed Programs in Rust
- record id: rust-guard-refinement-2025
Super-V (2025)
- title: Bolt-On Strong Consistency: Specification, Implementation, and Verification
- what: It verifies a Raft-like replicated store built on a weak replicated store. SMT checks local, stable preconditions on updates.
- limits: Only the abstract was read. The PDF was not obtained.
- how much was read: only abstract or first pages read
- source
- record id: super-v-2025
TLA+ communication module (2025)
- title: A Practical TLA+ Library for Designing and Verifying Distributed Systems
- what: A TLA+ library of communication-channel primitives with selectable faults. It was used to verify atomic broadcast properties and Deferred Update Replication.
- limits: The full text is behind a subscription, so the review notes have only abstract-level claims. The checked properties, counts and effort are unverified. The repository tests are model checks with TLC, not proofs that code matches the model.
- how much was read: only abstract or first pages read
- source; notes: A Practical TLA+ Library for Designing and Verifying Distributed Syste
- record id: tla-communication-module-2025
Verified SCION router (2025)
- title: Protocols to Code: Formal Verification of a Secure Next-Generation Internet Router
- what: From the authors’ abstract: network-wide protocol and security refinements in Isabelle/HOL are soundly linked to a proof about a Go production router. The proof covers freedom from crashes, freedom from data races, and adherence to the concrete model. The code is from an independent dev team.
- limits: Only the abstract and the repo were read. Numeric effort and exactly which files were verified are unaudited.
- how much was read: only abstract or first pages read
- source; notes: Protocols to Code: Formal Verification of a Secure Next-Generation Int
- record id: verified-scion-router-2025
Cedar (2024)
- what: The AWS authorization language Cedar. It is modeled in Lean with proofs, implemented in Rust, and the Rust is tested against the model by comparing their outputs (differential testing).
- number: Search-result summary: 4 bugs found by verification, 21 more by testing (unchecked)
- limits: Not distributed.
- how much was read: only abstract or first pages read
- source
- record id: cedar-2024
Formal Verification of Digital Twins with TLA and Information Leakage Control (2024)
- what: A TLA+ model that abstracts physical and communication processes into atomic state transitions. It explicitly assumes that messages are eventually delivered correctly.
- limits: Delivery is assumed, not proved.
- how much was read: only abstract or first pages read
- source; notes: digital twins with TLA+
- record id: formal-verification-of-digital-2024
Cinnabar (2023)
- title: Synthesis of Distributed Agreement-Based Systems with Efficiently-Decidable Verification
- what: Introduces Cinnabar, a counterexample-guided synthesis tool that completes sketches of distributed agreement-based systems so they fall in efficiently decidable verification classes.
- number: Targets leader election and consensus based DAB systems
- number: Counterexample-guided sketch completion
- limits: Automated verification is undecidable outside the characterized class; synthesis starts from a designer sketch.
- how much was read: only abstract or first pages read
- source
- record id: cinnabar-2023
QuickSilver (2021)
- title: QuickSilver: Modeling and Parameterized Verification for Distributed Agreement-Based Systems
- what: Quicksilver abstracts verified agreement protocols. It applies the abstractions to application case studies, using parameterized verification (one proof covers any number of nodes).
- limits: The notes cite only the abstract. Procedure note: check that the abstractions preserve the application properties the paper claims, not only the agreement primitive.
- how much was read: only abstract or first pages read
- source
- record id: quicksilver-2021
Randomized threshold consensus (2021)
- title: Verification of randomized consensus algorithms under round-rigid adversaries
- what: Extends threshold automata for randomized consensus with unbounded asynchronous rounds; round-rigid adversaries reduce verification to one-round model checking and support almost-sure termination reasoning.
- number: Automatically verifies Ben-Or, Bracha, 2-set agreement and RS-Bosco
- number: Handles crashes and Byzantine faults
- limits: Round-rigid schedules/adversaries are the fairness abstraction; probabilistic claims are model-specific.
- how much was read: only abstract or first pages read
- source
- record id: randomized-threshold-consensus-2021
Ivy: A Multi-modal Verification Tool for Distributed Algorithms. (2020)
- what: . Ivy is a multi-modal veriﬁcation tool for correct design and implementation of distributed protocols and algorithms, supporting modular speciﬁcation, implementation and proof. Ivy supports proving safety and liveness properties of parameterized and inﬁnite-state systems via three modes: deductive veriﬁcation using an SMT solver, abstraction and model checking, and manual proofs using natural deduction.
- limits: Not read; claims unverified.
- how much was read: only abstract or first pages read
- source
- record id: ivy-a-multi-modal-2020
Making Byzantine Consensus Live (2020)
- what: A spec for a view synchronizer (the component that gets nodes into the same view) strong enough to give liveness for single-shot HotStuff, Tendermint, PBFT and SBFT. The proofs are rigorous but not machine-checked.
- limits: The review notes read the abstract only. The proofs are not mechanized.
- how much was read: only abstract or first pages read
- source
- record id: making-byzantine-consensus-live-2020
PoS Nakamoto Coq proof (2020)
- title: Formalizing Nakamoto-Style Proof of Stake
- what: Gives a Coq machine-checked proof of safety and liveness for a synchronous Proof-of-Stake Nakamoto-style blockchain using chain growth, chain quality and common-prefix properties.
- number: Safety and liveness jointly implied by three chain properties
- number: Static corrupted parties in a synchronous network
- limits: The model assumes synchrony and a static corruption set; it is a protocol model rather than deployed code.
- how much was read: only abstract or first pages read
- source
- record id: pos-nakamoto-coq-proof-2020
Global synchronization guards (2019)
- title: Parameterized Verification of Systems with Global Synchronization and Guards.
- what: Defines a parameterized-system model with global synchronization and transition guards, proves decidability conditions for reachability and investigates cutoff bounds.
- number: Reachability decidable without guards under the model
- number: Sufficient conditions yield small cutoffs
- limits: Results are decidability/cutoff theorems for the model, not an implementation verification.
- how much was read: only abstract or first pages read
- source
- record id: global-synchronization-guards-2019
Threshold decomposition (2019)
- title: Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics
- what: Decomposes verification of threshold-based fault-tolerant distributed protocols into EPR and BAPA. An automatic inference algorithm generates threshold-intersection properties; EPR verifies protocol transition systems and BAPA checks property soundness.
- number: Evaluates Bosco safety, Hybrid Reliable Broadcast safety/liveness, and Byzantine Fast Paxos safety
- number: Ten repetitions per experiment on a 2.2 GHz Core i5 laptop
- number: Aip generated all valid formulas in under one minute; minimized sets contain 3–5 formulas versus 39–79 before minimization
- number: Verified protocols include fast-learning Byzantine consensus; threshold inference takes minutes
- limits: The user supplies an inductive invariant and models the protocol in EPR; the method targets restricted threshold use and relies on liveness-to-safety reduction where needed.
- how much was read: only abstract or first pages read
- source
- record id: threshold-decomposition-2019
LiLi (2016)
- title: A Program Logic for Concurrent Objects under Fair Scheduling
- what: A program logic based on rely-guarantee reasoning (each thread assumes what others do and promises what it does). It verifies linearizability (operations appear to take effect at one instant) and progress together, under fair scheduling. Applied to ticket locks, queue locks, lock-coupling lists, optimistic lists and lazy lists.
- limits: Abstract only. No effort numbers.
- how much was read: only abstract or first pages read
- source
- record id: lili-2016
FCSL (2015)
- title: Mechanized Verification of Fine-grained Concurrent Programs
- what: Presents FCSL, a mechanized higher-order concurrent separation logic and framework for verifying fine-grained concurrent programs and data structures. The paper reports mechanized proofs across benchmark libraries and explains recurring invariant patterns.
- number: Mechanized verification covers a benchmark suite of concurrent programs and data structures
- number: Framework uses higher-order separation logic and mechanized metatheory
- limits: The focus is shared-memory concurrency and data-structure verification rather than distributed protocols; proof effort depends on user-supplied invariants and specifications.
- how much was read: only abstract or first pages read
- source
- record id: fcsl-2015
Paxos Commit (2006)
- title: Consensus on Transaction Commit
- what: Defines Two-Phase Commit and Paxos Commit, with TLA+ specifications of their safety properties, and explains when Paxos Commit makes progress despite coordinator failures.
- number: Paxos Commit uses 2F+1 coordinators and makes progress when at least F+1 work
- number: Two-Phase Commit is the F=0 special case
- limits: The paper’s formal specifications omit liveness assumptions in the appendix; progress depends on the stated failure and majority assumptions.
- how much was read: only abstract or first pages read
- source
- record id: paxos-commit-2006
A Formal Analysis of the FIDO UAF Protocol
- what: —The FIDO protocol suite aims at allowing users to tion specification (WebAuthn) [52] and Client-to-Authenticator log in to remote services with a local and trusted authenticator. Protocol (CTAP) [3]. WebAuthn supports online services to With FIDO, relying services do not need to store user-chosen use FIDO through a standardized web API, whereas CTAP secrets or their hashes, which eliminates a major attack surface supports external devices to work with browsers supporting for e-business.
- how much was read: only abstract or first pages read
- source
- record id: a-formal-analysis-of
Applying Formal Methods to Networking: Theory, Techniques, and Applications
- what: “algebraic path problem” traction from code in sections IV-A1, IV-A2, IV-A3, and (e.g., a classical example of an abstract algebraic path problem IV-A4, respectively. is shortest path routing) [74]. Routing algebra meta-language 9 1) Finite State Machines: The mathematical formalism of that has been used in the study of computability and languages finite state machine (FSM), or finite state automaton, is com- [81].
- how much was read: only abstract or first pages read
- source
- record id: applying-formal-methods-to
Architecture of the Formally-Verified Distributed Ledger System InnoChain
- what: MODELING AND ANALYSIS OF INFORMATION SYSTEMS, VOL. 27, NO. 4, 2020 journal homepage: www.mais-journal.ru THEORY OF COMPUTING Architecture of the Formally-Verified Distributed Ledger System InnoChain L.
- how much was read: only abstract or first pages read
- source
- record id: architecture-of-the-formally
Are Users More Willing to Use Formally Verified Password Managers?
- what: . Formal verification has recently been increasingly used to prove the correctness and security of many applications. It is attractive because it can prove the absence of errors with the same certainty as mathematicians proving theorems.
- how much was read: only abstract or first pages read
- source
- record id: are-users-more-willing
Automated Attacker Synthesis for Distributed Protocols
- what: . Distributed protocols should be robust to both benign malfunction (e.g. packet loss or delay) and attacks (e.g.
- how much was read: only abstract or first pages read
- source
- record id: automated-attacker-synthesis-for
Automated Parameterized Verification of CRDTs.
- what: . Maintaining multiple replicas of data is crucial to achiev- ing scalability, availability and low latency in distributed applications. Conflict-free Replicated Data Types (CRDTs) are important building blocks in this domain because they are designed to operate correctly under the myriad behaviors possible in a weakly-consistent distributed setting.
- how much was read: only abstract or first pages read
- source
- record id: automated-parameterized-verification-of
Automated Verification of RPC Stub Code.
- what: Formal verification has been successfully applied to provide strong correctness guarantees of software systems, but its application to large code bases remains an open challenge. The technique of component-based software devel- opment, traditionally employed for engineering benefit, also aids reasoning about such systems. While there exist compositional verification techniques that lever- age the separation implied by a component system architecture, they implicitly rely on the component platform correctly implementing the isolation and com- position semantics they assume.
- limits: Read from the saved open PDF; this record uses the abstract/opening section and preserves the exact extracted quote below.
- how much was read: only abstract or first pages read
- source
- record id: automated-verification-of-rpc
’Cause I’m strong enough: reasoning about consistency choices in distributed systems.
- what: use. Ideally, we would like replicated databases to provide strong Large-scale distributed systems often rely on replicated databases consistency, i.e., to behave as if a single centralised node handles that allow a programmer to request different data consistency guar- all operations. However, achieving this ideal usually requires syn- antees for different operations, and thereby control their perfor- chronisation among replicas, which slows down the database and mance.
- how much was read: only abstract or first pages read
- source
- record id: cause-i-m-strong
Code-Level Safety Verification for Automated Driving: A Case Study.
- what: . The formal safety analysis of automated driving vehicles poses unique challenges due to their dynamic operating conditions and signiﬁcant complexity. This paper presents a case study of applying for- mal safety veriﬁcation to adaptive cruise controllers.
- how much was read: only abstract or first pages read
- source
- record id: code-level-safety-verification
Continuous Formal Verification of Amazon s2n.
- what: . We describe formal verification of s2n, the open source TLS implementation used in numerous Amazon services. A key aspect of this proof infrastructure is continuous checking, to ensure that properties remain proven during the lifetime of the software.
- how much was read: only abstract or first pages read
- source
- record id: continuous-formal-verification-of
Deductive Verification of Unmodified Linux Kernel Library Functions
- what: . This paper presents results from the development and evalu- ation of a deductive verification benchmark consisting of 26 unmodified Linux kernel library functions implementing conventional memory and string operations. The formal contract of the functions was extracted from their source code and was represented in the form of preconditions and postconditions.
- how much was read: only abstract or first pages read
- source
- record id: deductive-verification-of-unmodified
DY Fuzzing: Formal Dolev-Yao Models Meet Cryptographic Protocol Fuzz Testing
- what: — Critical and widely used cryptographic protocols corresponding class of logical attacks [11]. The DY attacker have repeatedly been found to contain flaws in their design and is an active network attacker who treats exchanged messages their implementation. A prominent class of such vulnerabilities as formal terms (in a term algebra): this representation is logical attacks, e.g.
- how much was read: only abstract or first pages read
- source
- record id: dy-fuzzing-formal-dolev
Formal Reasoning About the Security of Amazon Web Services.
- what: . We report on the development and use of formal veriﬁca- tion tools within Amazon Web Services (AWS) to increase the secu- rity assurance of its cloud infrastructure and to help customers secure themselves. We also discuss some remaining challenges that could inspire future research in the community.
- how much was read: only abstract or first pages read
- source
- record id: formal-reasoning-about-the
Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System.
- what: . Formal verification and validation is a fundamental step for the certifi- cation of railways critical systems. Many railways safety standards (e.g.
- how much was read: only abstract or first pages read
- source
- record id: formal-verification-and-validation
Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System.
- what: . Vehicle-to-Vehicle (V2V) communications is a “connected vehicles” standard that will likely be mandated in the U.S. within the coming decade.
- how much was read: only abstract or first pages read
- source
- record id: formal-verification-of-a
Integrated Environment for Verifying and Running Distributed Components
- what: . This paper targets the generation of distributed applica- tions with safety guarantees. The proposed approach starts from graph- ical speciﬁcation formalisms allowing the architectural and behavioral description of component systems.
- how much was read: only abstract or first pages read
- source
- record id: integrated-environment-for-verifying
Integrating Formal Schedulability Analysis into a Verified OS Kernel.
- what: . Formal veriﬁcation of real-time systems is attractive because these systems often perform critical operations. Unlike non real-time sys- tems, latency and response time guarantees are of critical importance in this setting, as much as functional correctness.
- how much was read: only abstract or first pages read
- source
- record id: integrating-formal-schedulability-analysis
Leapfrog: certified equivalence for protocol parsers.
- what: June 13–17, 2022, San Diego, CA, USA. ACM, New York, NY, USA, We present Leapfrog, a Coq-based framework for verifying 21 pages. https://doi.org/10.1145/3519939.3523715 equivalence of network protocol parsers.
- how much was read: only abstract or first pages read
- source
- record id: leapfrog-certified-equivalence-for
Mechanising blockchain consensus
- what: the previous state of the node or the entire network (we We present the first formalisation of a blockchain-based intentionally leave out the details of what can go into distributed consensus protocol with a proof of its consis- a transaction, as they are application-specific); a node tency mechanised in an interactive proof assistant. can also (b) create and broadcast a block that contains Our development includes a reference mechanisation the encoding of a certain vector of transactions, cre- of the block forest data structure, necessary for imple- ated locally or received via messages of type (a) from menting provably correct per-node protocol logic. We other nodes.
- limits: Abstract-level reading from openly available PDF; detailed limitations require full paper review.
- how much was read: only abstract or first pages read
- source
- record id: mechanising-blockchain-consensus
Modeling and Verification of a Dual Chamber Implantable Pacemaker.
- what: . The design and implementation of software for medical de- vices is challenging due to their rapidly increasing functionality and the tight coupling of computation, control, and communication. The safety- critical nature and the lack of existing industry standards for veriﬁcation, make this an ideal domain for exploring applications of formal modeling and analysis.
- how much was read: only abstract or first pages read
- source
- record id: modeling-and-verification-of
nekton: A Linearizability Proof Checker
- what: . nekton is a new tool for checking linearizability proofs of highly complex concurrent search structures. The tool’s unique features are its paramet- ric heap abstraction based on separation logic and the flow framework, and its support for hindsight arguments about future-dependent linearization points.
- how much was read: only abstract or first pages read
- source
- record id: nekton-a-linearizability-proof
On the Industrial Uptake of Formal Methods in the Railway Domain
- what: . The railway sector has seen a large number of successful ap- plications of formal methods and tools. However, up-to-date, structured information about the industrial usage and needs related to formal tools in railways is limited.
- limits: Abstract-level reading from openly available PDF; detailed limitations require full paper review.
- how much was read: only abstract or first pages read
- source
- record id: on-the-industrial-uptake
Prove your Colorings: Formal Verification of Cache Coloring of Bao Hypervisor
- what: . Hypervisors allow sharing of computing resources between applications—possibly of various levels of criticality—that makes them increasingly relevant for modern embedded systems. In this context, memory isolation properties (including low-level cache isolation) are es- sential to guarantee.
- how much was read: only abstract or first pages read
- source
- record id: prove-your-colorings-formal
Refinement-Based Specification and Security Analysis of Separation Kernels
- what: —Assurance of information-flow security by formal methods is mandated in security certification of separation kernels. As an industrial standard for improving safety, ARINC 653 has been complied with by mainstream separation kernels. Due to the new trend of integrating safe and secure functionalities into one separation kernel, security analysis of ARINC 653 as well as a formal specification with security proofs are thus significant for the development and certification of ARINC 653 compliant Separation Kernels (ARINC SKs).
- how much was read: only abstract or first pages read
- source
- record id: refinement-based-specification-and
Semantics, Specification, and Bounded Verification of Concurrent Libraries in Replicated Systems.
- what: . Geo-replicated systems provide a number of desirable prop- erties such as globally low latency, high availability, scalability, and built- in fault tolerance. Unfortunately, programming correct applications on top of such systems has proven to be very challenging, in large part because of the weak consistency guarantees they oﬀer.
- how much was read: only abstract or first pages read
- source
- record id: semantics-specification-and-bounded
Simpler Specifications and Easier Proofs of Distributed Algorithms Using History Variables
- what: This paper studies specifications and proofs of distributed algorithms when only message history variables are used, using the Basic Paxos and Multi-Paxos algorithms for distributed consensus as precise case studies. We show that not using and main- taining other state variables yields simpler specifications that are more declarative and easier to understand. It also allows easier proofs to be developed by needing fewer invariants and facilitating proof derivations.
- limits: Abstract-level reading from openly available PDF; detailed limitations require full paper review.
- how much was read: only abstract or first pages read
- source
- record id: simpler-specifications-and-easier
The EMV Standard: Break, Fix, Verify
- what: —EMV is the international protocol standard for ca. 600,000 Euros [11]. The underlying flaw of Murdoch et smartcard payment and is used in over 9 billion cards worldwide.
- how much was read: only abstract or first pages read
- source
- record id: the-emv-standard-break
The mCRL2 Toolset for Analysing Concurrent Systems - Improvements in Expressivity and Usability.
- what: . Reasoning about the correctness of parallel and distributed systems requires automated tools. By now, the mCRL2 toolset and lan- guage have been developed over a course of more than ﬁfteen years.
- how much was read: only abstract or first pages read
- source
- record id: the-mcrl2-toolset-for
Using Flow Specifications of Parameterized Cache Coherence Protocols for Verifying Deadlock Freedom
- what: . We consider the problem of verifying deadlock freedom for symmet- ric cache coherence protocols. While there are multiple definitions of deadlock in the literature, we focus on a specific form of deadlock which is useful for the cache coherence protocol domain and consistent with the internal definition of deadlock in the Murphi model checker: we refer to this deadlock as a system- wide deadlock (s-deadlock).
- limits: Abstract-level reading from openly available PDF; detailed limitations require full paper review.
- how much was read: only abstract or first pages read
- source
- record id: using-flow-specifications-of
Verification of a lazy cache coherence protocol against a weak memory model.
- what: —In this paper we verify a modern lazy cache coher- synchronisation boundaries. In these protocols, shared lines are ence protocol, TSO-CC, against the memory consistency model self-invalidated on synchronisation boundaries and therefore arXiv:1705.08262v1 [cs.LO] 18 May 2017 it was designed for, TSO. We achieve this by first showing a no longer require a (poorly scaling) sharing vector.
- how much was read: only abstract or first pages read
- source
- record id: verification-of-a-lazy
Verification of an alternating bit protocol by means of process algebra protocol
- what: VERIFICATION OF AN ALTERNATING BIT PROTOC~. BY MEANS OF PROCESS AtGEBRA J , A , BERGSTRA, J,W, KLOP Centre for Mathematics and Cemputer Science P.O.Box 4079, 1009 AB Amsterdam, The Netherlands We verify a simple verslon o? the alternating bit protocol in the system ACP~ (Algebra of Communicating Processes with silent actions) augmented with Koomenls falr abstraction rule.
- limits: Abstract-level reading from openly available PDF; detailed limitations require full paper review.
- how much was read: only abstract or first pages read
- source
- record id: verification-of-an-alternating
Verus verified node replication
- title: Verified Node-Replication Crate
- what: The repository contains a Verus port of IronSync node-replication proofs and reports verification results and benchmark comparisons with unverified Rust and Dafny implementations.
- number: 254 verified, 0 errors (README status)
- limits: README status is self-reported and was not rerun.
- how much was read: only abstract or first pages read
- source
- record id: verus-verified-node-replication
AWS ARG decade post (2026)
- title: A decade of mathematical certainty: Reflections on the Automated Reasoning Group
- what: Lists AWS’s production verification work. Describes Kiro’s requirements checks and its enforcement of agent policies.
- limits: Does not name the verified components, the properties, the sizes, the models or the success rates.
- how much was read: reading depth not recorded
- source; notes: AWS: production proofs exist; published accounts do not attribute them
- record id: aws-arg-decade-post-2026
Isolation levels for free (2026)
- title: Verifying Isolation Levels of Database Implementations for Free Using Separation Logic
- what: The paper proves that specs written in separation logic at the implementation level imply transactional consistency models that are defined independently. This holds for all executions of the program.
- limits: It bridges the meanings of specs. It is not evidence that a new production database is verified.
- how much was read: reading depth not recorded
- source; notes: Verifying Isolation Levels of Database Implementations for Free Using
- record id: isolation-levels-for-free-2026
Nitro Isabelle post (2026)
- title: Isabelle/HOL: The proof assistant behind the Nitro Isolation Engine
- what: Background on how Isabelle/HOL is used for foundational proofs about the Nitro Isolation Engine.
- limits: The review notes found no mention of LLMs or agents in the article body.
- how much was read: reading depth not recorded
- source; notes: AWS: production proofs exist; published accounts do not attribute them
- record id: nitro-isabelle-post-2026
Quint race post (2026)
- title: It Told Me No: How Quint Helped Us Fix a Long-Standing Race Condition
- what: A Quint model of the OpenHands Runtime API rejected two proposed fixes for duplicate Kubernetes pods. The accepted fix counted terminating pods and waited for them to disappear.
- limits: It is a case report from the team itself. It leaves open whether the model is too simple to capture another race. It gives no success rate or model version.
- how much was read: reading depth not recorded
- source; notes: Quint: production case studies, not a measured proof benchmark
- record id: quint-race-post-2026
Weak isolation (Aneris) (2025)
- title: Reasoning about Weak Isolation Levels in Separation Logic
- what: The paper writes transaction specs that do not depend on the implementation, for read-uncommitted, read-committed and snapshot isolation. It proves that known bad histories are prohibited. It verifies an in-memory, single-node MVCC key-value database, accessed over RPC, in OCaml/Aneris.
- limits: It covers a single node, with no replication or crash recovery. The review did not verify the translator from source to AnerisLang or the runtime.
- how much was read: reading depth not recorded
- source; notes: Reasoning about Weak Isolation Levels in Separation Logic
- record id: weak-isolation-aneris-2025
AdoB (2024)
- title: AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects
- what: The authors use Coq to prove safety and progress of a generic consensus object. They also prove that specs written at the network level are refinements of it (they behave as a more detailed version of the object). For GenJolteon, they also prove liveness at the network level. They extract it to runnable OCaml event handlers, using a handwritten shim. For Fast Paxos, they prove only safety and refinement.
- number: abstract benign AdoB proof under one person-month
- number: GenJolteon refinement/safety eight person-months; liveness two person-months
- number: Fast Paxos safety/refinement one person-month
- number: proof lines 17,000, 2,700, 2,000 (case-study discussion, PDF p.22)
- limits: This does not verify the production Jolteon or Fast Paxos code. There is no network-level liveness proof for Fast Paxos.
- how much was read: reading depth not recorded
- source; notes: AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed
- record id: adob-2024
Fairneris (2024)
- title: Verifying Liveness Properties of Distributed Systems via Trace Refinement in Higher-Order Concurrent Separation Logic
- what: Fairneris extends Aneris/Trillium to reason about progress in distributed systems. It reasons about code for the Stenning sliding-window protocol over a formal semantics resembling UDP. The proof that the implementation matches the model is machine-checked.
- limits: The Stenning model’s liveness theorem is only a proof on paper. So the transfer of its eventual-progress result to the implementation is not fully machine-checked. No runnable OCaml extraction was established, and the final venue is unknown.
- how much was read: reading depth not recorded
- source; notes: Verifying Liveness Properties of Distributed Systems via Trace Refinem
- record id: fairneris-2024
Aneris reliable channels (2023)
- title: Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols
- what: The paper specifies the order and contents of messages over a reliable-channel abstraction built on unreliable UDP. It uses dependent protocols, which let each message’s allowed form depend on earlier messages. The authors reuse the channel for RPC and for a leader/follower key-value service.
- limits: It proves the code does the right thing under the modeled network. It does not claim that a failed peer eventually answers. No audited link from the model to the real runtime is given.
- how much was read: reading depth not recorded
- source; notes: Verifying Reliable Network Components in a Distributed Separation Logi
- record id: aneris-reliable-channels-2023
StateLib (2023)
- title: Modular Verification of State-Based CRDTs in Separation Logic
- what: A reusable verified library for merging replica states. Each CRDT proof connects its lattice and merge function to the application’s operations. Proves convergence and functional correctness of several example CRDTs.
- limits: The proof is over AnerisLang. Running on OCaml is an experiment (§4.2), not a verified compiler or runtime. No theorem about delivery or termination.
- how much was read: reading depth not recorded
- source; notes: Modular Verification of State-Based CRDTs in Separation Logic
- record id: statelib-2023
ADO (2021)
- title: Much ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent Distributed Systems
- what: The ADO interface shows chosen failure cases to the user. It does not pretend that each operation either fully succeeds or does nothing. The authors use Coq and CCAL to prove that distributed C implementations (for example Multi-Paxos), and the clients built on them, match their abstract specs. The proofs sit on top of the verified CertiKOS.
- number: multi-Paxos: 2.6K lines of C and 43.9K lines of functional correctness proofs (§6, PDF p.23)
- limits: The results say nothing about progress (that the system eventually finishes its work). One example assumes termination. That assumption is not a proof of progress.
- how much was read: reading depth not recorded
- source; notes: Much ADO about Failures: A Fault-Aware Model for Compositional Verific
- record id: ado-2021
ReSync (2020)
- title: Programming at the Edge of Synchrony
- what: ReSync lets a process receive messages bit by bit within a round. It also lets each protocol set its own policy for moving to the next round. The paper establishes a round-switch abstraction and evaluates runnable consensus implementations.
- limits: The evaluated applications are not thereby fully proved.
- how much was read: reading depth not recorded
- source; notes: Programming at the Edge of Synchrony
- record id: resync-2020
Perennial (2019)
- title: Verifying concurrent, crash-safe systems with Perennial
- what: Perennial adds reasoning about crashes and recovery to concurrent separation logic. It separates specs for ordinary calls from specs for recovery, and durable ownership from volatile ownership. Examples are a crash-safe mail system and local replicated disks.
- limits: It covers replication across local disks only, not a replication protocol over a network.
- how much was read: reading depth not recorded
- source; notes: Verifying concurrent, crash-safe systems with Perennial
- record id: perennial-2019
WormSpace (2019)
- title: WormSpace: A Modular Foundation for Simple, Verifiable Distributed Systems
- what: Wormspace has a write-once-register API. Clients can reason about immutable agreed values instead of the coordination protocol. Certified concurrent abstraction layers prove that C code refines the API, and links it to the verified CertiKOS.
- number: 6 person-months core verification (4.5 functional correctness, 1.5 ghost layer) and 5 person-weeks application/linking proofs (§6, PDF p.10)
- number: 108K verification lines
- limits: Chain-replication registers and reconfiguration are outside the verified part. There is no availability proof.
- how much was read: reading depth not recorded
- source; notes: WormSpace: A Modular Foundation for Simple, Verifiable Distributed Sys
- record id: wormspace-2019
PSync (2016)
- title: PSync: A Partially Synchronous Language for Fault-Tolerant Distributed Algorithms
- what: PSync algorithms are written in communication rounds, with stated assumptions about which rounds are good. A Scala runtime runs them. SMT checks the user’s invariants and progress conditions under lockstep round semantics (all nodes advance round by round together). A reduction connects these to partially synchronous executions.
- number: LastVoting algorithm is 89 lines (Table 2, PDF p.13)
- limits: The runtime cannot be written in PSync’s round language. So the reduction theorem does not verify every statement of the runtime.
- how much was read: reading depth not recorded
- source; notes: PSync: A Partially Synchronous Language for Fault-Tolerant Distributed
- record id: psync-2016
DistAlgo (2012)
- title: From Clarity to Efficiency for Distributed Algorithms
- what: DistAlgo lets you write queries over message history directly. It compiles them, and makes them incremental, into efficient Python.
- limits: It is a paper about a language and its optimization. It gives no machine-checked guarantee of safety or liveness.
- how much was read: reading depth not recorded
- source; notes: From Clarity to Efficiency for Distributed Algorithms
- record id: distalgo-2012
Resume Means Resume: A Machine-Checked Conformance Contract for Checkpoint, Interrupt, and Resume Semantics in Workflow Persistence Layers (2026)
- what: A machine-checked conformance contract for a framework that saves execution state. It covers how a run can be interrupted, survive a crash, and continue.
- limits: Seen only as a Google Scholar snippet. Not read.
- how much was read: not read; title and metadata only
- source
- record id: resume-means-resume-a-2026
Testing LLM-Generated Distributed Protocol Code (2026)
- what: A framework evaluates LLM-written Two-Phase Commit, Ring Election and Raft. It uses a simulator that injects message loss, delay and duplication. LLMs do well on simple protocols and code completion, struggle on complex consensus, and debug inconsistently.
- limits: Based on the schedule abstract, through a fetch-tool summary. The review notes have no full text and no numbers.
- how much was read: not read; title and metadata only
- source
- record id: testing-llm-generated-distributed-2026
Verifier-supervised fine-tuning for Rust/Verus: vericoding dataset (restricted) (2026)
- what: A Zenodo record for a training dataset of Rust/Verus verified-code tasks used to fine-tune a code model with the verifier as the supervision signal. Only the record’s metadata could be read: the files are under embargo until 2026-12-31 and the record has no listed files.
- limits: Blocked: no full text exists and the data is embargoed (‘access_right’: ‘embargoed’, embargo_date 2026-12-31) with the author listed as ‘Anonymous’ (double-blind review). Everything here comes from the record’s description and keywords; content, size, and results are unknown.
- how much was read: not read; title and metadata only
- source; notes: Verifier-supervised fine-tuning for Rust/Verus dataset (2026)
- record id: verifier-supervised-fine-tuning-2026
AWS correctness practices (2025)
- title: Systems Correctness Practices at Amazon Web Services
- what: The paper was not read. Search summaries say it covers P, model checking, fuzzing, property-based testing, fault injection and simulation, with formal specs used as test oracles (the source of expected answers).
- limits: Fetching the paper returned HTTP 403. The claims are unverified search summaries.
- how much was read: not read; title and metadata only
- source; notes: P02. Systems Correctness Practices at Amazon Web Services
- record id: aws-correctness-practices-2025
Blockchain verification monograph (2025)
- title: Security analysis and formal verification on blockchain and its applications
- what: Per its abstract, a monograph that sorts real blockchain correctness and security flaws, and surveys the models, specifications and techniques used to formally verify blockchains.
- limits: Full text not obtained: publisher PDF is behind a bot-check page (not worked around), no open copy found. Only the publisher abstract from Crossref was read, so nothing about its content beyond the abstract is recorded.
- how much was read: not read; title and metadata only
- source; notes: Security analysis and formal verification on blockchain and its applic
- record id: blockchain-verification-monograph-2025
Practical Verification of Distributed Systems: Streamlining Safety Proofs Using Invariant Taxonomies, and Verifying Latency Properties Using Symbolic Latency (2025)
- what: PhD thesis on proving distributed protocols safe by sorting the needed invariants into types, and on extending verification to end-to-end latency. Full text could not be fetched; this record rests on a search-engine summary of the library page.
- limits: Full text blocked: the Deep Blue library (deepblue.lib.umich.edu) returned a Cloudflare ‘Just a moment’ challenge to command-line fetches, and I did not try to get around it. Nothing here comes from reading the thesis.
- how much was read: not read; title and metadata only
- source; notes: Practical Verification of Distributed Systems (2025)
- record id: practical-verification-of-distributed-2025
AWS formal methods video (2024)
- title: Formal Methods for Distributed Systems
- what: AWS video metadata describes a re:Invent session introducing P for modeling and verifying complex distributed protocols and discussing formal methods in design and testing.
- limits: Only the official video page metadata was read; no transcript or slides were retrieved.
- how much was read: not read; title and metadata only
- source
- record id: aws-formal-methods-video-2024
Derecho coordination proof (2024)
- title: Verifying a C Implementation of Derecho’s Coordination Mechanism Using VST and Coq
- what: Metadata points to a VST/Coq proof of a C implementation of Derecho’s coordination mechanism.
- limits: The review notes saw metadata only and did not retrieve the exact theorem. It covers that one mechanism, not the whole Derecho system.
- how much was read: not read; title and metadata only
- source; notes: Verifying a C Implementation of Derecho’s Coordination Mechanism Using
- record id: derecho-coordination-proof-2024
Kukovec TU Wien dissertation (2024)
- title: SMT-driven techniques for verifying distributed systems
- what: The dissertation develops symbolic-transition abstractions, SMT encodings of TLA+ and type inference to verify distributed algorithms.
- number: 168 pages
- limits: Repository metadata/abstract read; linked 1.97 MB PDF not downloaded in this pass.
- how much was read: not read; title and metadata only
- source
- record id: kukovec-tu-wien-dissertation-2024
Towards Mechanised Consensus in Isabelle (2024)
- what: Verifies Bitcoin’s Proof-of-Work consensus in Isabelle/HOL. Proves the common prefix property.
- limits: Known only from a search-result summary.
- how much was read: not read; title and metadata only
- record id: towards-mechanised-consensus-in-2024
Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols (2023)
- what: An interactive method in Ivy that stops SMT solvers from diverging on quantifier-heavy proofs of distributed protocols, by abstracting functions as relations and refining with counterexamples.
- limits: Full text not read: the ACM PDF sits behind a bot check, and no open copy was found. Facts here come from the input abstract and a web-search summary.
- how much was read: not read; title and metadata only
- source; notes: Counterexample Driven Quantifier Instantiations (2023)
- record id: counterexample-driven-quantifier-instantiations-2023
Performal: Formal Verification of Latency Properties for Distributed Systems (2023)
- what: This is a search lead from OpenAlex that nobody has read. The notes give only its title, year and DOI.
- limits: The notes screened it as unreachable. The DOI PDF request returned paywall HTML, and no author copy was exposed. The notes mark it as a priority lead.
- how much was read: not read; title and metadata only
- source
- record id: performal-formal-verification-of-2023
Proving Correctness of Parallel Implementations of Transition System Specifications (2023)
- what: Listed as an unread search lead from OpenAlex. The notes give only its title, year and DOI.
- limits: Screened as unreachable: the downloaded file could not be extracted.
- how much was read: not read; title and metadata only
- source
- record id: proving-correctness-of-parallel-2023
Formal Verification of Liveness Properties in Causal Order Broadcast Systems Using Event-B (2021)
- what: An unread search lead from OpenAlex. The notes give only its title, year and DOI.
- limits: Not read. The claims are unverified.
- how much was read: not read; title and metadata only
- source
- record id: formal-verification-of-liveness-2021
Formal specification and verification of a broadcasting protocol: a refinement-based approach (2020)
- what: Listed as an unread search lead from OpenAlex. The notes give only its title, year and DOI.
- limits: Not read. Claims are unverified.
- how much was read: not read; title and metadata only
- source
- record id: formal-specification-and-verification-2020
Formal verification of a consensus algorithm in the Heard-Of model (2009)
- what: The paper proves a consensus algorithm correct in Isabelle, in the Heard-Of model. The proof is at least five times shorter than a fine-grained Paxos proof.
- number: proof at least five times shorter than a fine-grained Paxos proof in Isabelle
- limits: The review notes saw only a search summary and did not open the paper.
- how much was read: not read; title and metadata only
- record id: formal-verification-of-a-2009
Correctness of a gossip based membership protocol (2005)
- what: Citation-snowball lead; full text was not retrieved from the attempted open endpoints.
- limits: Metadata-only: attempted open endpoints returned access-denied or non-PDF HTML; the paper was not read.
- how much was read: not read; title and metadata only
- source
- record id: correctness-of-a-gossip-2005
Pang VU thesis (2004)
- title: Formal Verification of Distributed Systems
- what: The VU repository record identifies Pang’s 2004 PhD thesis on formal verification of distributed systems and provides a complete-dissertation link.
- limits: Only repository metadata was read; dissertation PDF was not downloaded.
- how much was read: not read; title and metadata only
- source
- record id: pang-vu-thesis-2004
Mao Michigan thesis
- title: Automating the Verification of Distributed Systems
- what: The lead title identifies a University of Michigan thesis on automating distributed-system verification. Deep Blue returned Cloudflare challenges for the handle and guessed bitstream and API/OAI retrievals did not expose the thesis, so its contents were not read.
- limits: Metadata only. The repository was inaccessible in this pass; the title and repository URL are the only source facts recorded.
- how much was read: not read; title and metadata only
- source
- record id: mao-michigan-thesis
Schultz Stanford thesis
- title: Automated and interpretable verification of distributed protocols
- what: Crossref identifies this as William Schultz’s dissertation on automated and interpretable verification of distributed protocols. The repository landing page redirected to a 403 response during this pass, so the dissertation’s methods and cases were not read.
- limits: Metadata only. The DOI repository response was HTTP 403, so no abstract or full text was available in this pass.
- how much was read: not read; title and metadata only
- source
- record id: schultz-stanford-thesis

Last edited: 2026-10-31

Keyboard shortcuts

Steven Hé (Sīchàng)

🤖 database, distributed and concurrent systems that were proved