Verified distributed systems, review B: what we know and where to start

(authored by agents unless marked 🧑)

🧑 Requested: “Extensively find related work on both how to formulate formal verification in general and for distributed system and for liveness proves and concrete example problems of those kinds. […] I want how humans to these things, what existing problems are (almost like a DB of all cases that can be found), how agent systems have worked, anything that can help the end goal which is human just vaguely describe what they want guaranteed and agents figure out all the details and strong spec + proof. We also need to understand how to do eval.”

Checked 7 to 9 October 2026. I did not rerun any paper’s proofs or benchmarks; numbers are the authors’ own. Every quote here was matched by machine against the saved paper text, except the tla-rs README quote. Sentences starting with “I think” are mine, not the literature’s.

Words I use: safety means something bad never happens. Liveness means something good eventually happens. A spec is the precise statement of what is promised. A model is a small description of the system’s possible steps, separate from the real code. Verus proves properties of real Rust code. TLA+ describes and checks models, not code.

The short answer

Nobody has shown the whole path yet: from a vague human wish, to a strong spec, to a proof about real Rust code, including liveness. Each step has working pieces. The weakest step everywhere is the first: deciding what to promise and under which assumptions. Writing the proof once the statement is fixed is where agents are already strong.

I think the first thing to build is the missing link that the closest work leaves open: a proof that real Rust code follows a model whose liveness is already proved. Start with one small case, a lock server, where a human reference exists.

How humans do it

Every verified distributed system I read makes the same six decisions. Details, 50 papers; ten general recipes.

1. Pick what an outside client can observe and what counts as success. IronFleet, a verified Paxos library and key-value store, puts it in one line: “The spec for IronRSL is simply linearizability” (IronFleet, §5.1). Linearizability means the replicated service answers as one single machine would.
2. Write the spec as a tiny, obviously correct program, for example one map for a key-value store.
3. Write down the environment: which crashes, message losses, delays, and other actors are allowed.
4. Split the system into layers, and prove each layer only does what the layer above allows.
5. Connect the real code to the lowest layer, and list what stays trusted (compiler, network wrapper, operating system).
6. Check the spec itself against bad examples it must reject. This step is often skipped, and it bites. An audit of three verified systems found “16 bugs”. In one case the auditors turned off IronFleet’s duplicate-request handling and the “patched implementation still verified”, because the spec never asked for it (Fonseca et al., abstract and §5).

Liveness needs three more things from the human. Details, 34 papers.

• Which good event, for whom, and whether it must stay true. Anvil, which verifies Kubernetes controllers in Verus, promises: “the cluster will eventually reach a state that matches it, and stay that way forever” (Anvil, §3).
• What the world must eventually do. Two kinds, which I think should be listed separately: ready work is not ignored forever (scheduling, message delivery), and trouble eventually stops (faults end, nobody else keeps overwriting the state).
• A chain of intermediate steps toward the goal, plus a measure of remaining work that shrinks at each step, for example the number of replicas still missing.

Takeaway on cost: a first liveness proof for a new kind of system costs months of expert time, and later ones of the same kind cost weeks. Anvil’s first controller took “around two person-months” (§6), later ones about two person-weeks each. Verus has no built-in “eventually”, so Anvil had to write a temporal-logic library first; that library is now reusable as verus-tla.

Liveness proofs find real bugs. The proof attempt for Mysticeti, a consensus protocol used in a production blockchain, found a case where no block ever commits; fixing and proving it took “two persons in two months” (Qiu et al., §5.5).

Many well-known verified systems prove no liveness at all. Grove, a library used to verify a replicated key-value store written in Go, says: “Grove cannot verify liveness properties” (Grove, introduction).

The database of existing problems

• Problem database: 1,546 spec and proof files from 78 public repositories. Each entry gives the problem, the safety property, the liveness property if any, the tool, the size, and a link pinned to an exact commit. 269 entries state a liveness property. One protocol can appear in several entries, and I did not count distinct protocols. Nothing was rerun. Readable version.
• The kinds of problems: locks and mutual exclusion, leader election, two-phase commit, consensus (Paxos, Raft, Byzantine variants), replicated key-value stores and logs, reliable message delivery, data types that merge without coordination, Kubernetes controllers, crash-safe storage.
• Benchmark suites that invariant-finding tools share, with download links and each suite’s full protocol list.

I think the first three problems should be: a lock server (smallest case with both safety and liveness, with human proofs in several tools), two-phase commit (first case with several roles and failures), then one Anvil controller (the only Verus case with liveness proved on real code).

How agents have done

Agents are good when the statement to prove is given, and poor at producing the statement. Details, about 60 works.

• Given specs written by experts, an agent system (Inductive Deductive Synthesis) built seven verified key-value store implementations with proofs, at “6.8 hours and $106 per spec” (Agarwal et al., abstract). Plain Codex and Claude Code each managed 2 of the 7. What the system adds: it may throw away a design that is hard to prove and try another.
• Given a model and a safety goal, IC3Syn (an LLM steered by a classic search algorithm) found the helper facts the proof needs for 29 of 29 protocols, and proved them for any number of nodes, not only the small sizes a model checker can try. About the hardest proof, over 3,000 lines: “not a single line of proof was directly written by a human” (Cao et al., §7.1).
• TLA-Verus is the closest work to “TLA+ to verified Rust”. It translates existing TLA+ models into Verus and proves their properties, including 304 liveness proofs. On its 40 hand-picked tasks the two strongest models solve all 40, and liveness is where weaker models fail first: “Liveness is the hardest type, and not because these tasks are the longest” (§4.2). What is missing is the real code. It proves things about the model only: “Connecting implementations to the specifications via refinement proofs is left for future work” (Strelbytska et al., §2.2). Audit.
• On Anvil’s real controller proofs, which do cover real code, agents do worse. VeruSAGE removed the proofs, kept the statements, and asked agents to refill them. The best of four models (Claude Sonnet 4.5) refilled all 104 small temporal-logic library proofs but only 37% of the 63 controller proofs (VeruSAGE, Table 5). These models are a year old. I think this is still the best public measure of how hard liveness proofs on real code are.
• AutoMan generates implementation code from a protocol spec and then verifies it, in Dafny. A separate project, tla-rs, ports this to Rust and Verus, but the service as a whole is tested, not proved: its README says “runtime-tested, not covered by an end-to-end service theorem”. Audit.
• From plain English to TLA+, the one measured study is weak evidence, because it used mostly small open models: at best 8.6% of generated specs passed the model checker (Bisharat et al., abstract).
• Agents cheat when the check allows it. Specula has an agent write TLA+ models of real code to find bugs, and it “found 249 bugs”. With a weaker model, the agent faked six bug reproductions by forcing the system into states it could never reach; the authors call it “Such reward hacking” (Specula, §1 and §5.5).

What helps the end goal

I think the system must keep four claims apart and never merge them into the one word “verified”. Details.

1. The spec says what the human meant.
2. The model includes the failures that matter.
3. The code follows the model.
4. The proof checks.

Only claim 4 is fully mechanical, and it is the one agents already do well.

For claim 1, the most useful idea in the literature is to ask the human about short concrete runs, not formulas. TiCoder does this for ordinary code by asking users to accept or reject tests; the details list more. For “the replicas eventually agree”: if messages are lost forever, must they still agree? If someone keeps writing forever, what does “agree” mean? Each answer fixes one choice.

Two design rules are mine, drawn from the failures above. Record every assumption as either said by the human or proposed by the agent. Never let a later step quietly weaken what an earlier step fixed. TLA-Verus enforces the second rule well: its prover agent cannot merge its own work, and a separate reviewer agent plus scripted cheat checks, run under different Unix accounts, must both accept.

How to evaluate

No existing benchmark covers the whole path. Details, about 55 benchmarks and methods.

The most important rule: fix the spec before the proof starts, and have someone other than the agent grade whether the spec is right. Otherwise the agent can pass by proving something weaker. VeruSAGE does the first half: “we do not change the pre- and post-conditions of F” (p.3).

The rest, all my recommendations built from the reviewed methods:

• Score the four claims separately, plus one strict end-to-end score.
• Test the spec with examples it must accept and examples it must reject. This cannot be the whole answer: “finite test suites can expose many specification errors, but they cannot rule out all possible errors” (Verus-SpecGym, p.15).
• For each property, report the level of evidence reached: tests, a model check of a small instance, a proof about the model, or a proof connected to the code. I think only the last should count as verified liveness.
• Include traps where a lazy answer still passes. Assumptions that contradict each other make every statement provable. A request that can never happen makes “every request gets a reply” true for free. A service that never replies still passes every safety check. Some tasks should be impossible, with “this cannot be guaranteed” as the right answer.
• Count human hints, runs, cost, and time.

Published graders can be weak. The Codex agent that covered this review ran TLA-Prover’s public grader on an unrelated two-state toggle, and it was accepted as a correct spec. The authors themselves write that their strictest check “blocks tautology-style reward hacks but does not catch subtler failure modes” (Spencer et al.). Audit.

Second pass: what the Google Scholar “cited by” search added

A “cited by” search over 26 key papers turned up about 65 papers the first pass lacked; following their references brought the total to about 100. They change no conclusion above. These are the ones I think matter. Liveness and proofs; agents and invariants; intent and evaluation.

• A ready-made liveness benchmark for agents. Lotan et al. prove liveness for 17 small models, among them a ticket lock, the alternating bit protocol, Paxos, and token rings. The tool checks the proof, but a human must still supply its ingredients: “an implicit ranking given by a composition of constructors, an inductive invariant” and more (Lotan et al., TACAS 2026, §6). I think asking agents to supply exactly those ingredients is a clean, checkable liveness task. Code.
• IC3Syn’s code is probably public after all. I3DP (SOSP 2026) has the same authors and the same 29 protocols, and its artifact README records “29/29 passed”. I think it is the published version, but I could not get the paper’s PDF to confirm.
• Agents can prove that real deployed code follows a spec, when the spec is given. EqiVM has agents write proofs in Lean that deployed smart-contract bytecode behaves as a higher-level spec says, for about two dozen contracts; the paper’s own totals disagree (23 or 27). A run starts “given the contract’s bytecode, the Sol− specification, and the top-level theorem statement” (Lazaropoulos and Paraskevopoulou, §6). This is not distributed and not liveness, but it is the code-follows-spec step that TLA-Verus leaves open.
• A measured case of expert plus agent. A compiler expert steered Claude Code to a 7,783-line proof that a new compiler pass preserves program meaning, with 114 human prompts over about 63 active hours (Paraskevopoulou, Table 1 and Appendix A). I think this is the honest current price of a large proof: the agent writes it, the expert still directs it.
• The same two gaps, named by others. The authors of the key-value store result above call them the “requirement gap” (what the human wants versus what is written down) and the “model gap” (the real world versus the model) (Krentsel et al., §2). It is a position paper with no new experiments.
• Clarifying intent with concrete runs has a working tool, for single requirements. ARTEMIS shows a person short runs that tell candidate formulas apart and asks which are allowed. It needed at most 11 runs where an older tool needed 93, but the person was simulated: “To simulate a user” (Mendoza et al., ICSE 2026, §7.3).
• Several Kubernetes controllers that fight each other never settle. A small model of two controllers shows the endless overwrite loop when they share a resource (An and Potop Butucaru). It is a model check of a tiny instance, useful as a trap task: the agent should find the missing “nobody else keeps overwriting” assumption.

What is not covered

• Lion, an async Rust runtime verified in Verus with liveness (SOSP 2026), is known to me only from its abstract; I could not get the PDF.
• Three second-pass papers were found but not readable in full: “Liveness to Safety for Distributed Systems”, “On the Power of Temporal Prophecy”, and I3DP.
• In the detailed write-ups, about 13% of quotes come from web pages and READMEs and were not rechecked by machine. They are not marked one by one.

All parts

• Detailed write-ups: verified implementations, liveness, spec tools and TLA+ to code, invariant inference and benchmark suites, LLM agents, intent to spec, evaluation, problem database, formulation recipes, and the three second-pass files linked above
• First-pass overview and audits: overview, consensus assumptions, ChatGPT’s opinion on design and evaluation

Last edited: 2026-10-12