Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems

# Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems
Source: [https://arxiv.org/html/2605.23109](https://arxiv.org/html/2605.23109)
Shubham Agarwal∗,1, Alexander Krentsel∗,1, Shu Liu∗,1, Mert Cemri∗,1, Audrey Cheng1, Rui Meng2, Tomas Pfister2, Chun\-Liang Li2, Sylvia Ratnasamy1, Aditya Parameswaran1, Matei Zaharia1, Ion Stoica1, Mohsen Lesani3 1UC Berkeley2Google3UC Santa Cruz

###### Abstract

AI agents increasingly excel at generating, testing, and refining code\. However, they fall short on tasks requiring formal guarantees of full coverage that testing alone cannot provide\. Distributed systems are a prime example: properties such as consistency between reads and writes must hold under every possible interleaving of events\. Mechanized formal verification can guarantee such correctness, but typically demands months to years of expert effort\. As evidence, even SOTA coding agents \(Codex with GPT\-5\.4 and Claude Code with Opus 4\.6\) succeed on only 2/7 distributed key\-value\-store specifications\. In this paper, we present the first effective approach to addressing this gap, Inductive Deductive Synthesis \(IDS\), which jointly and incrementally synthesizes implementation and proof, and learns from failed attempts to systematically try promising strategies\. Built as an agentic LLM system, IDS achieves 7/7 in about6\.86\.8hours and $106106per spec on average, roughly200×200\\timesfaster than expert effort and17%17\\%cheaper than SOTA agents\. IDS further incorporates performance feedback into the same loop, yielding implementations up to3×3\\timesfaster than published verified systems\.111Code available at[https://github\.com/skydiscover\-ai/skydiscover](https://github.com/skydiscover-ai/skydiscover)\.

$\\ast$$\\ast$footnotetext:Equal contribution\.## 1Introduction

Coding agents have made great strides at writing code for many tasks, even running tests to automatically refine their own outputAnysphere \([2025](https://arxiv.org/html/2605.23109#bib.bib99)\); Anthropic \([2025](https://arxiv.org/html/2605.23109#bib.bib100)\); Chenet al\.\([2021](https://arxiv.org/html/2605.23109#bib.bib101)\); Yanget al\.\([2024](https://arxiv.org/html/2605.23109#bib.bib36)\); Shinnet al\.\([2023](https://arxiv.org/html/2605.23109#bib.bib61)\)\. However, they fall short on tasks requiring correctnessguaranteesacross every possible behavior, rather than just the cases reached during testing\. Distributed systems are a prime example: properties such as consistency between subsequent writes and reads must hold under every possible interleaving of messages, failures, and concurrent updates, a combinatorially large space that no realistic test suite can coverLeesatapornwongsaet al\.\([2016](https://arxiv.org/html/2605.23109#bib.bib109)\)\. The consequences of incorrect behavior are severe, ranging from a replicated store that loses dataBailis and Kingsbury \([2014](https://arxiv.org/html/2605.23109#bib.bib15)\), to a file system that drops a writePillaiet al\.\([2014](https://arxiv.org/html/2605.23109#bib.bib14)\), to a confidential store that leaks a key\.

To prevent such catastrophic failures, formal verification techniques can provide exhaustive correctness guarantees\. These techniques allow a developer to \(1\) state a specification, \(2\) write an implementation, and \(3\) develop a machine\-checkable proof that the implementation satisfies the specification on every possible inputBertot and Castéran \([2004](https://arxiv.org/html/2605.23109#bib.bib102)\); de Moura and Ullrich \([2021](https://arxiv.org/html/2605.23109#bib.bib103)\); Lattuadaet al\.\([2024](https://arxiv.org/html/2605.23109#bib.bib10)\); Leino \([2010](https://arxiv.org/html/2605.23109#bib.bib104)\)\. However, adoption of formal methods over the past two decades has been limited due to the immense manual labor required: verifying real\-world systems takes months to years of expert effortKleinet al\.\([2009](https://arxiv.org/html/2605.23109#bib.bib105)\); Leroy \([2009](https://arxiv.org/html/2605.23109#bib.bib106)\); Chenet al\.\([2015](https://arxiv.org/html/2605.23109#bib.bib9)\); Hawblitzelet al\.\([2015](https://arxiv.org/html/2605.23109#bib.bib7)\); Wilcoxet al\.\([2015](https://arxiv.org/html/2605.23109#bib.bib8)\); Lesaniet al\.\([2016](https://arxiv.org/html/2605.23109#bib.bib6)\)\.

Naturally, one may ask, can we simply provide a coding agent with a specification and formal verification tooling, and ask it to build complex systems that provably satisfy that specification? Our experiments demonstrate that the answer is no\. We show in[section˜5](https://arxiv.org/html/2605.23109#S5)that Codex \(GPT\-5\.4\)Chenet al\.\([2021](https://arxiv.org/html/2605.23109#bib.bib101)\)and Claude Code \(Opus 4\.6\)Anthropic \([2025](https://arxiv.org/html/2605.23109#bib.bib100)\)fail to generate correct systems for55of77widely studied distributed key\-value\-store consistency specifications \(e\.g\., causal consistency, read\-your\-writes\)\. The failure mode we observe is a structural one: following typical human patterns, agents treat verification as a downstream check on code they have already written\. This approach \(a\) requires writing the whole proof at once, which is exceptionally difficult even for humans222Past workLesaniet al\.\([2016](https://arxiv.org/html/2605.23109#bib.bib6)\)reports 9–12 months of expert effort to write a proof for a key\-value \(KV\) store\., and \(b\) defers all correctness feedback to the end of an implementation, depriving the agent of valuable guiding signals\.

To address these challenges, we introduce*Inductive Deductive Synthesis*\(IDS\), a technique that enables agents to synthesize provably correct complex systems from a specification\.

![Refer to caption](https://arxiv.org/html/2605.23109v1/x1.png)Figure 1:Code and proof advance jointly and incrementally with IDS; the proof assistant grades each partial step\.Our key insight is to synthesize both the implementation and its proofjointly and incrementally\([fig\.˜1](https://arxiv.org/html/2605.23109#S1.F1)\), while learning from failures at each step to guide the search toward promising solutions and away from dead ends\. As detailed in[section˜3](https://arxiv.org/html/2605.23109#S3), every implementation decision \(e\.g\., adding a data structure or modifying control flow\) is paired with a corresponding proof update \(e\.g\., adding new constraints or splitting lemmas\)\.

IDS offers two benefits: \(1\) each individual joint step is considerably simpler toprove, decreasing the complexity of proof generation, and \(2\) the intermediatepartialproofs can be verified with a formal checker to assess the viability of the current design\. A negative result rules out a dead\-end implementation path before further work is wasted and serves as a counterexample to improve the design going forward\. This is akin to “chain\-of\-thought”Weiet al\.\([2022](https://arxiv.org/html/2605.23109#bib.bib118)\), except that the intermediate states are formally encoded and verified\. Beyond correctness, this iterative loop also optimizes performance: as soon as a candidate’s implementation is complete, it is benchmarked on a distributed testbed; the performance measurements then further guide the search toward efficient implementations\.

We instantiate IDS as a multi\-agent system \([section˜4](https://arxiv.org/html/2605.23109#S4)\), and we evaluate IDS on 7 distributed key\-value\-store consistency specifications: Chapar’s published causal\-consistency specLesaniet al\.\([2016](https://arxiv.org/html/2605.23109#bib.bib6)\)plus six new*IDS suite*specs we release with the system \([appendix˜I](https://arxiv.org/html/2605.23109#A9)\)\. IDS produces a complete verified implementation on all 7 in about6\.86\.8hours and $106106per spec on average, with no human intervention or fine\-tuning\. On the two specs our vanilla agent baseline completed, IDS runs1\.6×1\.6\\timesfaster and17%17\\%cheaper\. The discovered implementations match or beat hand\-written expert references on every spec and reach up to3×3\\timesthe throughput of Chapar’s published vector\-clock reference, a margin we attribute to a design\-space search broader than what manual proof allows\.

As a general prover, IDS achieves state\-of\-the\-art performance on four cross\-language verification benchmarks \(DafnyBenchLoughridgeet al\.\([2024](https://arxiv.org/html/2605.23109#bib.bib63)\), miniCodePropsLohn and Welleck \([2024](https://arxiv.org/html/2605.23109#bib.bib64)\), Verus\-BenchYanget al\.\([2025](https://arxiv.org/html/2605.23109#bib.bib31)\), CoqStoqThompsonet al\.\([2025](https://arxiv.org/html/2605.23109#bib.bib79)\)\), beating agentic baselines that share its prompt and underlying model by\+10%\+10\\%to\+51%\+51\\%\. On three further code\-and\-proof synthesis benchmarks, IDS again leads:176/189176/189on VERINAYeet al\.\([2026](https://arxiv.org/html/2605.23109#bib.bib58)\)\(prior38/18938/189\),65/7765/77on AlgoVeriZhaoet al\.\([2026](https://arxiv.org/html/2605.23109#bib.bib59)\)\(prior31/7731/77\), and a perfect62/6262/62on CloverBenchSunet al\.\([2024a](https://arxiv.org/html/2605.23109#bib.bib57)\)\.

In summary, we make the following contributions in this work:

- •Inductive Deductive Synthesis \(IDS\):the first general technique for jointly synthesizing code and machine\-checked proof under a partial\-proof oracle, with feedback from failures and performance benchmarks in the same loop\.
- •IDS\-based multi\-agent system:the first agentic system to autonomously generateverifieddistributed systems\. Solves7/77/7consistency specifications where SOTA agents \(GPT\-5\.4, Opus 4\.6\) solve only2/72/7, with up to3×3\\timesthe throughput of published verified systems\.
- •IDS suite:six new Rocq specifications for distributed key\-value\-store consistency models, released as an open benchmark for verified\-synthesis research\.

## 2Related Work

Verified code generation with an LLM has three components: \(1\) a specification of desired guarantees, \(2\) an implementation, and \(3\) a machine\-checkable proof that the implementation satisfies the specification\. Prior work falls into four threads: three each address one component \(specification generation, program generation with an evaluator, automated proof generation\), and verified synthesis attempts \(2\) and \(3\) jointly\. IDS pursues this last class on distributed\-systems specifications\.

Specification generation\.A complementary line uses LLMs to recover formal specifications from code or intentEndreset al\.\([2024](https://arxiv.org/html/2605.23109#bib.bib2)\); Wenet al\.\([2024](https://arxiv.org/html/2605.23109#bib.bib3)\); CloverSunet al\.\([2024a](https://arxiv.org/html/2605.23109#bib.bib57)\)generates formal annotations from natural language specifications, and then checks the consistency of code with the formal and natural specifications of Dafny benchmarks\. IDS takes such specifications as input rather than producing them\.

Program generation with an evaluator\.A separate strand of work treats program construction as search guided by evaluator feedback\. Coding agents get feedback from given or self\-generated testsYanget al\.\([2024](https://arxiv.org/html/2605.23109#bib.bib36)\); Shinnet al\.\([2023](https://arxiv.org/html/2605.23109#bib.bib61)\), or from communication with other specialized agentsHonget al\.\([2024](https://arxiv.org/html/2605.23109#bib.bib41)\); Qianet al\.\([2024](https://arxiv.org/html/2605.23109#bib.bib40)\); Wuet al\.\([2024](https://arxiv.org/html/2605.23109#bib.bib19)\)\. Algorithmic discovery systems use a scoring function to drive evolutionRomera\-Paredeset al\.\([2024](https://arxiv.org/html/2605.23109#bib.bib42)\); Novikovet al\.\([2025](https://arxiv.org/html/2605.23109#bib.bib45)\)or deep reinforcement learningMankowitzet al\.\([2023](https://arxiv.org/html/2605.23109#bib.bib43)\)\. IDS shares the evaluator\-guided search scheme; however, instead of tests or scores, it uses a proof assistant\. In contrast to sampled signals \(tests over traces, specific inputs, or estimated scores\), type\-checked proofs guarantee correctness on all inputs\.

Automated proof generation\.Most prior LLM\-for\-verification work fixes the implementation and specification, asking the model only for the proof\. For SMT\-backed languages such as DafnyLeino \([2010](https://arxiv.org/html/2605.23109#bib.bib104)\)and VerusLattuadaet al\.\([2024](https://arxiv.org/html/2605.23109#bib.bib10)\), recent systems synthesize the loop invariants and assertions a verifier needs, either via compiler\-feedback loopsYanget al\.\([2025](https://arxiv.org/html/2605.23109#bib.bib31)\)or targeted invariant generationMugnieret al\.\([2025](https://arxiv.org/html/2605.23109#bib.bib56)\)\. For tactic\-driven assistants such as Leande Moura and Ullrich \([2021](https://arxiv.org/html/2605.23109#bib.bib103)\)and RocqBertot and Castéran \([2004](https://arxiv.org/html/2605.23109#bib.bib102)\), prover systems have been trained on databases of prior formal proofsYang and Deng \([2019](https://arxiv.org/html/2605.23109#bib.bib52)\), natural\-language proofsWanget al\.\([2024](https://arxiv.org/html/2605.23109#bib.bib113)\), and conjectured theoremsDong and Ma \([2025](https://arxiv.org/html/2605.23109#bib.bib115)\)\. Approaches differ in scope: some generate full proofs in one passRenet al\.\([2025](https://arxiv.org/html/2605.23109#bib.bib24)\); Wanget al\.\([2025](https://arxiv.org/html/2605.23109#bib.bib75)\); Firstet al\.\([2023](https://arxiv.org/html/2605.23109#bib.bib30)\); others decompose the proof into sub\-goalsLiet al\.\([2026](https://arxiv.org/html/2605.23109#bib.bib116)\); Zhaoet al\.\([2024](https://arxiv.org/html/2605.23109#bib.bib112)\); Jianget al\.\([2023](https://arxiv.org/html/2605.23109#bib.bib21)\); tactic\-level methods iteratively predict and repair the next proof step from the current proof state and verifier feedbackHubertet al\.\([2025](https://arxiv.org/html/2605.23109#bib.bib111)\); Yanget al\.\([2023](https://arxiv.org/html/2605.23109#bib.bib32)\); Thakuret al\.\([2024](https://arxiv.org/html/2605.23109#bib.bib28)\); Ospanovet al\.\([2025](https://arxiv.org/html/2605.23109#bib.bib74)\); Ruidaet al\.\([2025](https://arxiv.org/html/2605.23109#bib.bib114)\)\. IDS differs by jointly generating the implementation and proof, and further optimizing performance\.

Verified synthesis\.The long\-standing goal of producing a program and its correctness proof from a specification alone goes back to deductive synthesisManna and Waldinger \([1980](https://arxiv.org/html/2605.23109#bib.bib86)\); Polikarpovaet al\.\([2016](https://arxiv.org/html/2605.23109#bib.bib95)\)and counterexample\-guided inductive synthesisSolar\-Lezama \([2008](https://arxiv.org/html/2605.23109#bib.bib90)\); Solar\-Lezamaet al\.\([2006](https://arxiv.org/html/2605.23109#bib.bib89)\), but the inference rules and candidate\-search space confined results to small individual functions\. The LLM era rekindles this dream\. VERINAYeet al\.\([2026](https://arxiv.org/html/2605.23109#bib.bib58)\)provides a benchmark to evaluate specification, code, and proof generation, evaluates existing tools, and underscores significant challenges for automatic provers\. Recent LLM\-driven verified\-synthesis work targets SMT\-backed languages: AlphaVerusAggarwalet al\.\([2025](https://arxiv.org/html/2605.23109#bib.bib69)\)bootstraps verified Verus code via self\-improving translation, scaling to function\-level tasks\. At the other extreme, hand\-built verified distributed systems, such as IronFleet’s Paxos\-replicated state machinesHawblitzelet al\.\([2015](https://arxiv.org/html/2605.23109#bib.bib7)\), Verdi’s RaftWilcoxet al\.\([2015](https://arxiv.org/html/2605.23109#bib.bib8)\), FSCQ’s crash\-safe file systemChenet al\.\([2015](https://arxiv.org/html/2605.23109#bib.bib9)\), Anvil’s verified Kubernetes controllersSunet al\.\([2024b](https://arxiv.org/html/2605.23109#bib.bib11)\), Chapar’s causally\-consistent KV storesLesaniet al\.\([2016](https://arxiv.org/html/2605.23109#bib.bib6)\), and Iris\-based concurrent and distributed verificationJunget al\.\([2015](https://arxiv.org/html/2605.23109#bib.bib17)\); Sharmaet al\.\([2023](https://arxiv.org/html/2605.23109#bib.bib13)\); Chajedet al\.\([2019](https://arxiv.org/html/2605.23109#bib.bib16)\)demonstrate that machine\-checkable guarantees*are*achievable at systems scale, but at months to years of expert proof effort\. IDS shows that verified synthesis need not be small\-scale or slow: it automatically generates implementations and their machine\-checkable correctness proofs for distributed key\-value stores in hours rather than months\.

## 3Background and Overview

We begin with a short introduction to formal verification\. A formally verified system has three pieces\. The*specification*is a precise mathematical statement of correctness; the*implementation*is the code that runs; and the*proof*is a machine\-checkable argument that, on every input, the implementation matches the specification\. Historically, humans wrote all three; IDS takes a human\-written spec and automatically produces both implementation and proof, using LLM agents driven by the proof assistant RocqBertot and Castéran \([2004](https://arxiv.org/html/2605.23109#bib.bib102)\)\. We show a simple example: a*counter*, a state machine with two operations \(incto increment the count andreadto return it\) starting from an initial stateinit\.

Specification

ModuleTypeCounterSpec\.

Parametert:Type\.

Parameterinit:t\.

Parameterinc:t\-\>t\.

Parameterread:t\-\>nat\.

Axiomread\_init:

readinit=0\.

Axiomread\_inc:

foralls,

read\(incs\)=

S\(reads\)\.

EndCounterSpec\.

Partial impl\. & proof

Definitiont:=listunit\.

Definitioninit:t:=nil\.

Definitioninc\(s:t\):t\.

Admitted\.

Definitionread\(s:t\):=

lengths\.

Theoremread\_init:

readinit=0\.

Proof\.reflexivity\.Qed\.

Theoremread\_inc:

foralls,

read\(incs\)=S\(reads\)\.

Admitted\.

Complete impl\. & proof

Definitiont:=listunit\.

Definitioninit:t:=nil\.

Definitioninc\(s:t\):=tt::s\.

Definitionread\(s:t\):=

lengths\.

Theoremread\_init:

readinit=0\.

Proof\.reflexivity\.Qed\.

Theoremread\_inc:

foralls,

read\(incs\)=S\(reads\)\.

Proof\.intross\.unfoldread,inc\.

simpl\.reflexivity\.Qed\.

Figure 2:Counterspecification\(left\),partialsynthesis \(center, yellow =Admitted\), andcompletesynthesis \(right, green = filled in\)\. Rocq accepts both files\.Figure[2](https://arxiv.org/html/2605.23109#S3.F2)shows the counter’sspecification\(left\), apartial synthesis\(center\), and acomplete synthesis\(right\)\. The spec states two properties, or “axioms,” aboutinit,inc, andread: reading the initial state returns zero, and reading after an increment returns one more than reading before\. In the partial synthesis,inc’s body and theread\_inctheorem are deferred viaAdmitted\(a placeholder for unfinished work\), but Rocq still accepts the file: the chosen representation \(a list whose length encodes the count\) is consistent with the work so far\. The complete synthesis fills in the deferred pieces\. The representation is a free choice; any state satisfying the axioms works, thoughnat\(natural numbers\) is more efficient\.

Rocq’s type\-checker as an oracle, including for partial work\.Rocq’s checkeracceptsa declaration/proof if and only if it satisfies its stated type/proposition, and rejects with a precise diagnostic otherwise\. There are no false positives or false negatives, in contrast to tests \(only the inputs tried\), static analysis \(over\-approximate\), or LLM\-as\-judge \(guesses\)\. The verdict also extends to*partial*code, as the center column of Figure[2](https://arxiv.org/html/2605.23109#S3.F2)illustrates: unproven obligations are stated as*deferred holes*\(Admittedlemmas or stub function bodies\), and the file still type\-checks\. \([appendix˜G](https://arxiv.org/html/2605.23109#A7)walks a longerall\_less\_thanexample through this progression\.\) IDS leverages the type\-checker as an oracle to drive a*deductive synthesis*Manna and Waldinger \([1980](https://arxiv.org/html/2605.23109#bib.bib86)\): at every step, the agent extends the partial implementation and proof, then asks Rocq whether the partial state still type\-checks\. A yes keeps the design on track; a no rules it out before further work is committed\. If progress stalls \(measured by the number of partial proofs left empty\), IDS reverts to an earlier state\.

From counter to distributed stores\.IDS applies this loop at scale\. For distributed systems, the specification grows from simple axioms to conditions over executions involving messages, clients, replicas, and failures\. For example,read\_incin a distributed setting becomes read\-your\-writes: a client that increments then reads must observe its own increments\. The implementation grows from a few\-line module to a multi\-replica protocol with larger state, multiple message types, and handlers\. For example, a replica can no longer store onenat; it must keep a vector with one entry per client, tracking the increments received from that client\. On a request carrying the client’s increment count, the replica can then tell whether it is up\-to\-date enough to serve, providing read\-your\-writes\. The proof grows from simple tactics to an inductive simulation argument \(an induction linking implementation and spec states\) with dozens of helper lemmas\.

Such implementations span a large, subtle design space with widely varying performance, explored by decades of research\.[section˜4](https://arxiv.org/html/2605.23109#S4)describes the agent that drives this process,[appendix˜I](https://arxiv.org/html/2605.23109#A9)gives the full specifications, and[section˜5](https://arxiv.org/html/2605.23109#S5)reports results\.

## 4IDS Agentic Architecture

![Refer to caption](https://arxiv.org/html/2605.23109v1/x2.png)Figure 3:IDS’ agentic architecture; code and proof advance jointly throughout\. A coordinator runs parallel1Deductive Synthesis Agents \(DSAs\); each step is graded by2Rocq’s type\-checker, completed implementations are3benchmarked, and closed proofs are4audited for non\-vacuity\. On failure, the5Inductive Synthesis Agent \(ISA\) intervenes:A*proposer*adds helper lemmas on tactical stalls;B*reloader*respawns a DSA with a fresh design on strategic dead\-ends\.Overview\.We now describe how we realize IDS as an agentic architecture \([fig\.˜3](https://arxiv.org/html/2605.23109#S4.F3)\)\. Given a system interface and property specifications, the framework orchestrates multiple LLM agents guided by verification and performance feedback to generate an efficient, mechanically\-checked implementation\. This architecture relies on a powerful synergy: deductive synthesis constructs the code and proof under a given strategy, while inductive synthesis discovers better strategies from failed attempts\.

Inspired by deductive synthesisManna and Waldinger \([1980](https://arxiv.org/html/2605.23109#bib.bib86),[1979](https://arxiv.org/html/2605.23109#bib.bib87)\), IDS introduces Deductive Synthesis Agents \(DSAs,1\) to incrementally synthesize implementations from specifications\. Guided by a strategy, a DSA recursively decomposes a component and its specification into sub\-components using placeholders\. The DSA constructs proofs assuming these sub\-components are correct, repeating this process down to trivial elements\. The Rocq type\-checker \(2\) continuously verifies both complete and partial proofs throughout this decomposition\.

While this deductive approach succeeds when guided by a sound search strategy \(e\.g\., a high\-level design or proof approach in the prompt\), a DSA can stall under a dead\-end strategy\. Inspired by inductive synthesisSolar\-Lezamaet al\.\([2006](https://arxiv.org/html/2605.23109#bib.bib89)\); Solar\-Lezama \([2008](https://arxiv.org/html/2605.23109#bib.bib90)\); Clarkeet al\.\([2000](https://arxiv.org/html/2605.23109#bib.bib117)\), IDS introduces an Inductive Synthesis Agent \(ISA,5\) that learns from failed strategies to propose more promising ones\. The ISA receives feedback when a DSA stalls or yields poor performance\. It then intervenes in two roles: a*proposer*for tactical, local adjustments \(A\), and a*reloader*for strategic, global shifts to entirely new designs \(B\)\.

Coordinator\.The coordinator launches and orchestrates the DSAs and the ISA, maintaining overall system state and managing a parallel pool of workers\. While DSAs can report localized errors, they cannot detect strategic dead\-ends on their own\. The coordinator monitors progress to identify stagnating agents, recording failed strategies and invoking the ISA to propose new ones before respawning the DSA\.

To ensure the synthesized system is not only correct but also performant, the coordinator benchmarks each candidate eagerly, even before its proof completes\. It extracts the implementation to executable code and runs the benchmark harness \(3,[section˜5\.1](https://arxiv.org/html/2605.23109#S5.SS1)\)\. The measurements are fed back to the ISA so that its future strategies guide the DSA toward more efficient implementations\. Once a proof closes \(i\.e\., the proof completes with no remainingAdmittedplaceholders\), the coordinator audits the result to ensure it is fully verified, non\-trivial, and implements the expected interface \(4\)\. Finally, it returns the most efficient verified solution found within the time budget\.

DSA: Deductive Synthesis Agent\.Off\-the\-shelf LLMs, pretrained on a large corpus of programs and proofs, are well\-equipped to guide synthesis search, as we empirically demonstrate in[section˜5\.2](https://arxiv.org/html/2605.23109#S5.SS2)\. To harness this capability, we design the DSA as a generic LLM coding agent operating under strict constraints: implementations must be well\-typed before proving, specifications cannot be altered, final outputs must contain no unproven assumptions, and system state must remain bounded\.

At each node of the search tree, the agent can take the following actions to advance the synthesis: \(1\) define partial implementations, \(2\) close open proof branches, or \(3\) decompose complex lemmas into simpler helper lemmas\. After each step, the implementation and proof are passed to Rocq’s type\-checker\. If there are no errors, the state is saved, building a search tree of well\-typed partial implementations and proofs\. If errors occur, the agent can take the following actions: \(1\) repair the failed step by attempting a different approach, or \(2\) revert to an earlier node in the search tree\.

ISA: Inductive Synthesis Agent\.The DSA cannot reliably step back and pivot a failing strategy on its own\. The ISA fills this gap as a stateless LLM agent that reasons over a strategy summary and proposes new approaches across two decision horizons:

- •Proposer \(tactical\)\.Triggered when the strategy is promising but the DSA is stuck on a specific proof\. The proposer offers finer\-grained assistance, suggesting helper lemmas and structural decompositions from a holistic view of the proof state\.
- •Reloader \(strategic\)\.Triggered when the strategy is a dead\-end or slow\. Rather than allowing the DSA to endlessly apply small fixes, the reloader intervenes by respawning the DSA with an entirely new high\-level design\.

## 5Evaluation

We evaluate IDS on 7 Rocq specifications of distributed key\-value\-store consistency: Chapar’s published causal\-consistency specLesaniet al\.\([2016](https://arxiv.org/html/2605.23109#bib.bib6)\)and 6 new*IDS suite*specs co\-developed with a formal\-verification and distributed\-systems expert \([appendix˜I](https://arxiv.org/html/2605.23109#A9)\)\. We extract synthesized implementations from Gallina to OCaml and benchmark them on a 5\-VM Google Cloud cluster under a distributed runtime against hand\-written expert references\. For synthesis, we compare against SOTA coding agents, Codex \(GPT\-5\.4\)Chenet al\.\([2021](https://arxiv.org/html/2605.23109#bib.bib101)\)and Claude Code \(Opus 4\.6\)Anthropic \([2025](https://arxiv.org/html/2605.23109#bib.bib100)\), under the same prompt and budget\. We answer three questions in the following subsections:

- •Q1\. Does IDS handle hard specifications?IDS succeeds on all77in about6\.86\.8hours and $106106per spec on average \(max1111h, $155155\), versus22of77each for Codex and Claude Code under the same prompt and budget \([section˜5\.2](https://arxiv.org/html/2605.23109#S5.SS2)\)\.
- •Q2\. Are the synthesized implementations performant?They match or beat every expert\-implemented reference:3×3\\timesthroughput on Chapar’s vector\-clock reference,1\.4×1\.4\\timeson IDS suite CC and monotonic reads, comparable on read\-your\-writes \(within20%20\\%\), and sustained throughput on MW and RYW\+MW where the reference times out \([section˜5\.3](https://arxiv.org/html/2605.23109#S5.SS3)\)\.
- •Q3\. Which of IDS’ design decisions drive these results?The joint code\-and\-proof co\-design, the ISA’s proposer and reloader roles, the audit step, the Rocq feedback to the DSA, and the performance feedback to the ISA each contribute consequentially\. The DSA alone also sets a new state\-of\-the\-art on four public proof benchmarks across four languages \([section˜5\.4](https://arxiv.org/html/2605.23109#S5.SS4)\)\.

### 5\.1Experimental Setup

Specifications\.Each specification is a high\-level reference implementation of a key\-value store; its state type and operations define the consistency notion\. IDS takes a specification and produces a refining implementation paired with a machine\-checked proof of correctness on every input\.

ChaparLesaniet al\.\([2016](https://arxiv.org/html/2605.23109#bib.bib6)\)provides a published causal\-consistency specification \(CC\)\. The other six form the*IDS suite*benchmark dataset that we release alongside the system \([appendix˜I](https://arxiv.org/html/2605.23109#A9)\): read\-your\-writes \(RYW\), monotonic writes \(MW\), monotonic reads \(MR\), their composition \(RYW\+MW\), and two causal\-consistency variants: IDS suite CC and LCC \(*labeled*causal consistency, where each client subscribes to a set of topic labels and sees causality enforced only on those labels\)\. The IDS suite spans the space of session consistency guarantees\. To the best of our knowledge, no prior benchmark provides verified Rocq artifacts across this range\. Difficulty grows in three tiers: simple \(RYW, MW\), specs whose proofs need many cases \(MR, RYW\+MW\), and specs that also manage explicit dependency sets \(CC, LCC\)\. A side\-by\-side summary of all seven specifications appears in[appendix˜A](https://arxiv.org/html/2605.23109#A1)\.

Harness and metrics\.Verified Rocq implementations are extracted to OCaml \(via Rocq’s built\-in extraction, an automatic compilation pass from Gallina to OCaml\) and run under a distributed runtime on a 5\-VM Google Cloud cluster\. Each run executes44parallel workers×\\times1,0001\{,\}000random operations; we sweep across put rates, and run a separate scaling sweep at put rate=50%=50\\%overN∈\{1,000,2,000,5,000,20,000\}N\\in\\\{1\{,\}000,2\{,\}000,5\{,\}000,20\{,\}000\\\}\.[appendix˜D](https://arxiv.org/html/2605.23109#A4)covers the cluster topology and toolchain\. Every method runs under the same per\-spec wall\-clock and dollar budget\. Runs that exhaust either budget are considered failed runs\. Each cell aggregates three independent runs, and we report pass rate \(successes out of three\), time\-to\-finish, dollar cost, throughput, p99 latency, peak memory, and ops\-per\-worker scaling, all as medians\.

Baselines\.The synthesis baselines are Codex \(GPT\-5\.4\)Chenet al\.\([2021](https://arxiv.org/html/2605.23109#bib.bib101)\)and Claude Code \(Opus 4\.6\)Anthropic \([2025](https://arxiv.org/html/2605.23109#bib.bib100)\)\. Both run under the same prompt and budget as IDS’ DSA, so the comparison isolates the agentic architecture\. Codex is also IDS’ primary backend\. For performance comparisons, the references are the hand\-written expert implementations: Chapar’s two published references \(vector\-clock and list\-based\)Lesaniet al\.\([2016](https://arxiv.org/html/2605.23109#bib.bib6)\), and the expert\-written reference released alongside each IDS suite specification, except LCC, a custom spec with no expert reference\. For the cross\-language evaluation, we adopt four public verification benchmarks \(DafnyBench, Verus\-Bench, miniCodeProps, CoqStoq\) across the languages Dafny, Verus, Lean, and Rocq\. We compare against the strongest published prior tool for each benchmark\.[appendix˜E](https://arxiv.org/html/2605.23109#A5)covers three more \(VERINA, AlgoVeri, CloverBench\)\. These cross\-language benchmarks target function\- and algorithm\-level tasks, smaller and simpler in scope than the real\-world distributed systems above\.

Table 1:IDS succeeds onall seven specifications\(≥2/3\\geq\\,2/3runs\) versus only2 of 7 eachfor Codex and Claude Code, while usingless total wall\-clock and fewer total dollars; on every spec where any method succeeds, IDS is alsofaster and cheaper\.pass rate==\# successes out of33\(green:≥2/3\\geq\\,2/3; red:<2/3<\\,2/3\);hours==median wall\-clock until a successful run \(RocqQedaccepted, audit step passed, extracted OCaml runs on the harness\);cost==median dollars per run\. All methods share the same model, verifier, pass criterion, and per\-spec budget; relative std across runs is≤7%\\leq 7\\%\.CodexClaude CodeIDSSpecificationPass rate↑\\uparrowHours↓\\downarrowCost \($\)↓\\downarrowPass rate↑\\uparrowHours↓\\downarrowCost \($\)↓\\downarrowPass rate↑\\uparrowHours↓\\downarrowCost \($\)↓\\downarrow*Chapar*Causal Consistency0/3121600/3111653/310148*IDS suite*Read\-Your\-Writes3/34603/33703/3252Monotonic Reads0/3121300/3101403/37102Monotonic Writes2/35653/34703/3358RYW \+ MW0/391251/361103/3593Causal Consistency0/3121600/3111702/311155LCC0/3131800/3111603/310136Total across specs2/767$8802/756$8857/748$744
### 5\.2Synthesis correctness

IDS returns verified implementations for all seven specifications, a3\.5×3\.5\\timespass rate over the22out of77that each of Codex and Claude Code reach under the same prompt and budget\. Even on the two specs \(RYW and MW\) where both baselines succeed, IDS is1\.6×1\.6\\timesfaster and17%17\\%cheaper \(Table[1](https://arxiv.org/html/2605.23109#S5.T1)\)\. IDS succeeds by storing the data in a way that lets the proof split into smaller, manageable cases \(e\.g\., one entry per key on Chapar CC, or one entry per \(key, client\) pair on monotonic reads\); the baselines keep the spec’s default layout, never backtrack, and stall on the same hard cases\. We also evaluate two LLM\-only baselines that ask Codex for an implementation only \(the standard coding\-agent task\), with best\-of\-N=100N\{=\}100generation, on44properties \(RYW, MW, MR, CC\)\.*Setting 1 \(spec\-given\):*Codex receives the formal Rocq specification\.*Setting 2 \(vibe coding\):*Codex receives only a natural\-language paragraph of the property\. We then check each selected implementation two ways: an adversarial multi\-client trace flags implementations that violate the spec on a single execution, and a refinement proof against the spec catches the rest\. Spec\-given Codex passes both checks on1/41/4properties; vibe coding on0/40/4\([appendix˜C](https://arxiv.org/html/2605.23109#A3)\)\. Even given the formal spec and100100candidates per property, the LLM alone cannot produce implementations that are guaranteed correct on every input\.

Chapar causal consistency\.IDS closes Chapar’s published causal\-consistency proof, originally a major hand\-written verificationLesaniet al\.\([2016](https://arxiv.org/html/2605.23109#bib.bib6)\), in1010hours and $148 \(roughly200×200\\timesfaster than the cited 9–12 months of expert effort\), while both agent baselines fail to finish within1\.2×1\.2\\timesour wall\-clock and cost\. IDS succeeded by changing how the data was stored\. Its first attempt kept each replica’s state as one big object, so proving correctness required reasoning about every key and message together, and the proof got stuck\. IDS backtracked, gave each key its own small table, and the proof then split into one easy case per key\. The full trajectory and the per\-family lemma counts are given in[appendix˜B](https://arxiv.org/html/2605.23109#A2)\.

IDS suite specifications\.IDS handles the four harder IDS suite specifications \(monotonic reads, RYW\+MW, LCC, and IDS suite CC\) in55to1111hours per spec, with33\-of\-33pass rates on the first three and22\-of\-33on IDS suite CC\. In comparison, Codex never succeeds, and Claude Code succeeds only once, on RYW\+MW\. The same Chapar pattern recurs: the first design gets stuck on the spec’s default layout, then IDS backtracks and rebuilds the data so the proof splits into smaller cases, for instance one entry per \(key, client\) on monotonic reads, or one case per message on the two CC variants\. Per\-specification details are reported in[appendix˜B](https://arxiv.org/html/2605.23109#A2)\.

![Refer to caption](https://arxiv.org/html/2605.23109v1/x3.png)Figure 4:Throughput, p99 latency, and peak memory vs\. put rate, and throughput vs\. ops\-per\-workerNN, for IDS suite CC and monotonic reads\. Solid==IDS; dashed==reference \(function\-as\-map for both\)\. The per\-spec breakdown for all seven specifications appears in[section˜D\.1](https://arxiv.org/html/2605.23109#A4.SS1)\.
### 5\.3Runtime performance

IDS’ synthesized implementations match or beat every prior reference:3×3\\timesthroughput on Chapar’s vector\-clock reference,1\.4×1\.4\\timeson IDS suite CC and monotonic reads, comparable on read\-your\-writes \(within20%20\\%\), and152152k and139139k ops/s on MW and RYW\+MW where the reference times out at every put rate \([section˜D\.1](https://arxiv.org/html/2605.23109#A4.SS1)\)\. We compare on throughput, p99 latency, peak memory, and ops\-per\-worker scaling\. Figure[4](https://arxiv.org/html/2605.23109#S5.F4)shows IDS suite CC and monotonic reads vs\. the references, and the full per\-spec breakdown is in[section˜D\.1](https://arxiv.org/html/2605.23109#A4.SS1)\. The gap follows from one mechanism: IDS’ data\-store representations are bounded, while the references’ grow with workload size\. These representations emerged from the joint code\+proof loop: the proof obligation drove the agent to them \([section˜5\.2](https://arxiv.org/html/2605.23109#S5.SS2)\)\. The performance feedback from the benchmark harness then steers the agent toward the fastest among multiple verifying candidates \([section˜5\.4](https://arxiv.org/html/2605.23109#S5.SS4)\)\.

IDS suite CC\.Both implementations enforce causality with one timestamp per client; the data store differs\. The reference’s function\-from\-key\-to\-value extracts to OCaml as a chain that grows per put \(every get walks it\), while IDS uses a balanced\-tree map where a lookup costs at most the tree depth\. IDS reaches up to1\.4×1\.4\\timespeak throughput at low put rate where gets dominate, with p99 latency up to1\.7×1\.7\\timeslower\. The gap narrows at high put rate as broadcast becomes the bottleneck; tail latency tracks the same effect, rising with put rate on both implementations as broadcast queue waits grow\. Peak memory is comparable at11k ops per worker, since the vector\-clock state is bounded by client count rather than put rate; larger workloads would push it upward\. On ops\-per\-worker scaling, the reference’s throughput collapses by more than half from11k to2020k ops per worker while IDS loses only about a quarter\.

Other IDS suite specifications\.Unlike CC, these specs only need per\-client guarantees, so they do not pay CC’s per\-write cross\-client coordination cost; their tail latency stays flat across put rate \(Figure[4](https://arxiv.org/html/2605.23109#S5.F4), MR\)\. On the other IDS suite specs, IDS ranges from comparable on read\-your\-writes \(chain stays short\) to a gap large enough that the reference times out at every put rate on the monotonic\-write specs \(MW, RYW\+MW\)\. The four with prior references \(RYW, MW, MR, RYW\+MW\) share the closure\-chain mechanism: the reference’s function\-from\-key\-to\-value extracts as a chain that grows per put; IDS replaces it with a flat list or balanced tree, and the speedup tracks how often the chain is walked\. On the monotonic reads benchmark, a get in the reference walks every operation, so IDS outperforms it by1\.4×1\.4\\times\.

### 5\.4Ablations and Generalization

The joint step\-wise discovery of code and proof is the key design decision behind IDS\. We ablate this joint design itself \(−\-J\), the ISA’s proposer \(−\-P\) and reloader \(−\-R\), the coordinator’s audit step \(−\-A\), and the Rocq feedback to the DSA \(−\-VF\) across the seven key\-value store specs and VERINA’s189189Lean tasks \(Table[2](https://arxiv.org/html/2605.23109#S5.T2)\)\. We also evaluate the DSA alone and IDS’ prover component decoupled from the rest of the system on four cross\-language proof benchmarks \(DafnyBench, miniCodeProps, Verus\-Bench, CoqStoq\), where it sets a new state\-of\-the\-art on each\.

Architecture ablations\.Without joint discovery, only RYW succeeds in a majority of runs: Chapar CC, RYW\+MW, IDS suite CC, and LCC drop to0out of33, and VERINA falls to85%85\\%\(−8%\-8\\%from full IDS’93%93\\%\)\. This is because a fixed implementation limits the proof phase\. On Chapar CC,−\-J commits to the global per\-replica state closest to the spec\. Full IDS reloads to per\-key entries when the proof stalls\. The audit step catches trivial solutions that pass Rocq’s type\-checker: on IDS suite CC, an agent without auditing once shipped aput\-guardreturningfalseunconditionally, with the theorem being trivially satisfied\. On the other hand, cells under−\-A count only audited successful runs\. Ablations of the proposer and reloader each drop pass rate on the four hardest specs \(Chapar CC, MR, IDS suite CC, LCC\), taking VERINA to79%79\\%\(−14%\-14\\%\) under−\-P and to88%88\\%\(−5%\-5\\%\) under−\-R\. The Rocq feedback to the DSA is the most consequential single component: replacing the structured Rocq diagnostic \(goal, hypotheses, tactic backtrace\) with only an accept/reject drops every spec to at most11of33successful runs and VERINA to58%58\\%\(−35%\-35\\%\)\.

Performance\-feedback ablation\.Without performance feedback \(−\-PF\), the agent commits to the first implementation and proof that passes the type\-checker and misses the course\-corrections seen in[section˜5\.3](https://arxiv.org/html/2605.23109#S5.SS3)\. As[fig\.˜5](https://arxiv.org/html/2605.23109#S5.F5)shows, full IDS is on average1\.42×1\.42\\timesfaster than−\-PF across the six specs with reference baselines \(Chapar CC, RYW, MW, RYW\+MW, MR, IDS suite CC\)\.

DSA as a general prover\.The DSA’s effectiveness is not specific to IDS’ synthesis loop or to Rocq: applied alone to public verification benchmarks across four languages, it sets a new state\-of\-the\-art on each \(Figure[6](https://arxiv.org/html/2605.23109#S5.F6), Table[7](https://arxiv.org/html/2605.23109#A5.T7)\)\. It saturates miniCodeProps \(100100of100100\) and Verus\-Bench \(149149of150150\), and beats prior SOTA by3636to69%69\\%on DafnyBench and CoqStoq\. IDS’ agentic architecture brings further gain: full IDS adds\+10%\+10\\%on DafnyBench,\+20%\+20\\%on miniCodeProps, and\+51%\+51\\%on CoqStoq over Codex under the same prompt, while a baseline\-model swap \(Codex→\\toClaude under the same prompt, no IDS architecture\) gains at most6%6\\%on any of these four benchmarks\. IDS also reaches state\-of\-the\-art on all three code\-and\-proof benchmarks:176/189176/189on VERINA \(prior SOTA3838\),65/7765/77on AlgoVeri \(2×2\\timesprior SOTA3131\), and a full62/6262/62on CloverBench \(Table[7](https://arxiv.org/html/2605.23109#A5.T7); detail in[appendix˜E](https://arxiv.org/html/2605.23109#A5)\)\.

Table 2:Component ablations: \# successes from33runs \(189189tasks for VERINA\)\.
![Refer to caption](https://arxiv.org/html/2605.23109v1/x4.png)
Figure 5:Performance\-feedback ablation atput=60%\\textit\{put\}=60\\%: IDS \(solid\) vs\. no\-feedback \(hatched\)\.![Refer to caption](https://arxiv.org/html/2605.23109v1/x5.png)
Figure 6:Cross\-language success rate \(%\) on 4 verification benchmarks; labels are \# of successes\.

## 6Discussion and Conclusion

#### IDS is language\- and problem\-agnostic\.

IDS as a technique depends on neither the verification backend nor the problem domain\. The backend need only support \(i\) mechanical checking of partial proofs, \(ii\) a programmatic interface an LLM agent can drive, and \(iii\) executable extraction of verified implementations for performance feedback; Leande Moura and Ullrich \([2021](https://arxiv.org/html/2605.23109#bib.bib103)\)and VerusLattuadaet al\.\([2024](https://arxiv.org/html/2605.23109#bib.bib10)\)both qualify, and we expect IDS to transfer to either without structural changes\. The problem domain need only admit a machine\-checkable formal specification and a way to benchmark candidate implementations\. We chose Rocq for the maturity of its ecosystem, and we chose distributed key\-value stores because the literature already provided a complete formal specification for one consistency model; following its structure, we contribute six additional specifications covering other consistency properties \([appendix˜I](https://arxiv.org/html/2605.23109#A9)\)\.

#### Limitations\.

Our work has three main limitations\. First, IDS requires a formal Rocq specification as input; writing complete formal specifications for distributed systems requires substantial expert effort, a challenge we return to below\. Second, the seven specifications we evaluate cover correctness\-critical behavior but not the full operational envelope of a production KV store; they do not define interfaces for scaling out \(adding or removing nodes at runtime\), reconfiguration, fault recovery, or informal but practically necessary behavior such as logging and observability endpoints\. Given a richer specification that captures these aspects, we see no reason IDS would not apply unchanged, but evaluating this is left to future work\. Third, our empirical evaluation covers the distributed key\-value store problem only, leaving validation on other domains \(e\.g\., OS protocols, cryptographic primitives\) to future work\.[appendix˜H](https://arxiv.org/html/2605.23109#A8)discusses additional limitations and broader impacts\.

#### The specification bottleneck\.

While IDS automates the synthesis of verified implementations, writing the formal specification itself remains the largest open problem: accurately capturing a system’s intended behavior in a machine\-checkable form is hard, and any correctness guarantee is only as strong as the specification it is checked against\. We envision two directions for closing this gap\. First,*adversarial specification synthesis*, in which an LLM agent collaborates with a human stakeholder in natural language, iteratively probing intent and surfacing ambiguities until a formal specification emerges\. Second,*specification extraction from existing systems*, in which an agent recovers the correctness properties of a deployed implementation while leaving the design space open, so that IDS can synthesize alternative implementations that satisfy the same properties with better performance\. We are actively pursuing both directions, which we plan to report on in future work\.

#### Conclusion\.

Verified systems construction has traditionally required months to years of expert effort\. IDS condenses this timeline to mere hours by replacing human labor with compute\. By providing an LLM coding agent with fast and exact correctness feedback without false positives, IDS transforms the joint code\-and\-proof construction into an automated search problem\. This shifts vibe coding to verified coding by using LLMs to directly build type\-safe systems that are machine\-checked against a formal specification, effectively eliminating silent bugs and unverified assumptions\. Crucially, this methodology generalizes to any domain with a machine\-checkable correctness oracle, including OS kernels, compilers, cryptographic protocols, and hardware\. Ultimately, IDS shows that verified software generation is transitioning from a human\-labor bottleneck to a compute\-driven approach, paving the way for the broad adoption of verified system synthesis\.

## Acknowledgments

This research is supported by NSF \(IFML\) CCF\-2019844 and gifts from Accenture, AMD, Anyscale, Broadcom Inc\., Google, IBM, Intel, Intesa Sanpaolo, Lambda, Mibura Inc\., Samsung SDS, and SAP\. We also thank our Sky Lab and NetSys colleagues at UC Berkeley for fruitful discussions that shaped this paper\.

## References

- \[1\]\(2025\)AlphaVerus: bootstrapping formally verified code generation through self\-improving translation and treefinement\.ICML\.Note:arXiv:2412\.06176Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p5.1)\.
- \[2\]M\. Ahamad, G\. Neiger, J\. E\. Burns, P\. Kohli, and P\. W\. Hutto\(1995\)Causal memory: definitions, implementation, and programming\.Distributed Computing9\(1\)\.Cited by:[Figure 25](https://arxiv.org/html/2605.23109#A9.F25),[Figure 25](https://arxiv.org/html/2605.23109#A9.F25.3.2)\.
- \[3\]Anthropic\(2025\)Claude Code: anthropic’s agentic coding system\.Note:[https://www\.anthropic\.com/product/claude\-code](https://www.anthropic.com/product/claude-code)Cited by:[§1](https://arxiv.org/html/2605.23109#S1.p1.1),[§1](https://arxiv.org/html/2605.23109#S1.p3.2),[§5\.1](https://arxiv.org/html/2605.23109#S5.SS1.p4.1),[§5](https://arxiv.org/html/2605.23109#S5.p1.1)\.
- \[4\]Anysphere\(2025\)Cursor: the AI code editor\.Note:[https://cursor\.com](https://cursor.com/)Cited by:[§1](https://arxiv.org/html/2605.23109#S1.p1.1)\.
- \[5\]P\. Bailis and K\. Kingsbury\(2014\-09\)The network is reliable\.Commun\. ACM57\(9\),pp\. 48–55\.External Links:ISSN 0001\-0782,[Link](https://doi.org/10.1145/2643130),[Document](https://dx.doi.org/10.1145/2643130)Cited by:[§1](https://arxiv.org/html/2605.23109#S1.p1.1)\.
- \[6\]D\. Banerjee, O\. Bouissou, and S\. Zetzsche\(2026\)DafnyPro: llm\-assisted automated verification for Dafny programs\.Note:POPL Dafny Workshop; arXiv:2601\.05385Cited by:[1st item](https://arxiv.org/html/2605.23109#A5.I1.i1.p1.1)\.
- \[7\]Y\. Bertot and P\. Castéran\(2004\)Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions\.Texts in Theoretical Computer Science,Springer\.External Links:[Document](https://dx.doi.org/10.1007/978-3-662-07964-5)Cited by:[§1](https://arxiv.org/html/2605.23109#S1.p2.1),[§2](https://arxiv.org/html/2605.23109#S2.p4.1),[§3](https://arxiv.org/html/2605.23109#S3.p1.1)\.
- \[8\]T\. Chajed, J\. Tassarotti, M\. F\. Kaashoek, and N\. Zeldovich\(2019\)Verifying concurrent, crash\-safe systems with perennial\.InProceedings of the 27th ACM Symposium on Operating Systems Principles,SOSP ’19,New York, NY, USA,pp\. 243–258\.External Links:ISBN 9781450368735,[Link](https://doi.org/10.1145/3341301.3359632),[Document](https://dx.doi.org/10.1145/3341301.3359632)Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p5.1)\.
- \[9\]H\. Chen, D\. Ziegler, T\. Chajed, A\. Chlipala, M\. F\. Kaashoek, and N\. Zeldovich\(2015\)Using crash hoare logic for certifying the FSCQ file system\.InProceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015, Monterey, CA, USA, October 4\-7, 2015,E\. L\. Miller and S\. Hand \(Eds\.\),pp\. 18–37\.External Links:[Link](https://doi.org/10.1145/2815400.2815402),[Document](https://dx.doi.org/10.1145/2815400.2815402)Cited by:[§1](https://arxiv.org/html/2605.23109#S1.p2.1),[§2](https://arxiv.org/html/2605.23109#S2.p5.1)\.
- \[10\]M\. Chen, J\. Tworek, H\. Jun, Q\. Yuan, H\. P\. d\. O\. Pinto, J\. Kaplan, H\. Edwards, Y\. Burda, N\. Joseph, G\. Brockman, A\. Ray, R\. Puri, G\. Krueger, M\. Petrov, H\. Khlaaf, G\. Sastry, P\. Mishkin, B\. Chan, S\. Gray, N\. Ryder, M\. Pavlov, A\. Power, L\. Kaiser, M\. Bavarian, C\. Winter, P\. Tillet, F\. P\. Such, D\. Cummings, M\. Plappert, F\. Chantzis, E\. Barnes, A\. Herbert\-Voss, W\. H\. Guss, A\. Nichol, A\. Paino, N\. Tezak, J\. Tang, I\. Babuschkin, S\. Balaji, S\. Jain, W\. Saunders, C\. Hesse, A\. N\. Carr, J\. Leike, J\. Achiam, V\. Misra, E\. Morikawa, A\. Radford, M\. Knight, M\. Brundage, M\. Murati, K\. Mayer, P\. Welinder, B\. McGrew, D\. Amodei, S\. McCandlish, I\. Sutskever, and W\. Zaremba\(2021\)Evaluating large language models trained on code\.Note:arXiv:2107\.03374External Links:[Link](https://arxiv.org/abs/2107.03374)Cited by:[§1](https://arxiv.org/html/2605.23109#S1.p1.1),[§1](https://arxiv.org/html/2605.23109#S1.p3.2),[§5\.1](https://arxiv.org/html/2605.23109#S5.SS1.p4.1),[§5](https://arxiv.org/html/2605.23109#S5.p1.1)\.
- \[11\]E\. Clarke, O\. Grumberg, S\. Jha, Y\. Lu, and H\. Veith\(2000\)Counterexample\-guided abstraction refinement\.InInternational Conference on Computer Aided Verification,pp\. 154–169\.Cited by:[§4](https://arxiv.org/html/2605.23109#S4.p3.3)\.
- \[12\]L\. de Moura and S\. Ullrich\(2021\)The Lean 4 theorem prover and programming language\.InAutomated Deduction — CADE 28 — 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings,A\. Platzer and G\. Sutcliffe \(Eds\.\),Lecture Notes in Computer Science, Vol\.12699,pp\. 625–635\.External Links:[Document](https://dx.doi.org/10.1007/978-3-030-79876-5%5F37)Cited by:[§1](https://arxiv.org/html/2605.23109#S1.p2.1),[§2](https://arxiv.org/html/2605.23109#S2.p4.1),[§6](https://arxiv.org/html/2605.23109#S6.SS0.SSS0.Px1.p1.1)\.
- \[13\]K\. Dong and T\. Ma\(2025\)STP: self\-play llm theorem provers with iterative conjecturing and proving\.InInternational Conference on Machine Learning,pp\. 14114–14136\.Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p4.1)\.
- \[14\]M\. Endres, S\. Fakhoury, S\. Chakraborty, and S\. K\. Lahiri\(2024\)Can large language models transform natural language intent into formal method postconditions?\.InProc\. ACM Softw\. Eng\. \(FSE\),Note:arXiv:2310\.01831Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p2.1)\.
- \[15\]E\. First, M\. N\. Rabe, T\. Ringer, and Y\. Brun\(2023\)Baldur: whole\-proof generation and repair with large language models\.InProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering,ESEC/FSE 2023,New York, NY, USA,pp\. 1229–1241\.External Links:ISBN 9798400703270,[Link](https://doi.org/10.1145/3611643.3616243),[Document](https://dx.doi.org/10.1145/3611643.3616243)Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p4.1)\.
- \[16\]C\. Hawblitzel, J\. Howell, M\. Kapritsos, J\. R\. Lorch, B\. Parno, M\. L\. Roberts, S\. T\. V\. Setty, and B\. Zill\(2015\)IronFleet: proving practical distributed systems correct\.InProceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015, Monterey, CA, USA, October 4\-7, 2015,External Links:[Document](https://dx.doi.org/10.1145/2815400.2815428)Cited by:[§1](https://arxiv.org/html/2605.23109#S1.p2.1),[§2](https://arxiv.org/html/2605.23109#S2.p5.1)\.
- \[17\]S\. Hong, M\. Zhuge, J\. Chen, X\. Zheng, Y\. Cheng, C\. Zhang, J\. Wang, Z\. Wang, S\. K\. S\. Yau, Z\. Lin, L\. Zhou, C\. Ran, L\. Xiao, C\. Wu, and J\. Schmidhuber\(2024\)MetaGPT: meta programming for a multi\-agent collaborative framework\.InICLR,Note:arXiv:2308\.00352Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p3.1)\.
- \[18\]T\. Hubert, R\. Mehta, L\. Sartran, M\. Z\. Horváth, G\. Žužić, E\. Wieser, A\. Huang, J\. Schrittwieser, Y\. Schroecker, H\. Masoom,et al\.\(2025\)Olympiad\-level formal mathematical reasoning with reinforcement learning\.Nature,pp\. 1–3\.Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p4.1)\.
- \[19\]A\. Q\. Jiang, S\. Welleck, J\. P\. Zhou, W\. Li, J\. Liu, M\. Jamnik, T\. Lacroix, Y\. Wu, and G\. Lample\(2023\)Draft, sketch, and prove: guiding formal theorem provers with informal proofs\.InICLR,Note:arXiv:2210\.12283Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p4.1)\.
- \[20\]R\. Jung, D\. Swasey, F\. Sieczkowski, K\. Svendsen, A\. Turon, L\. Birkedal, and D\. Dreyer\(2015\)Iris: monoids and invariants as an orthogonal basis for concurrent reasoning\.InProceedings of the 42nd Annual ACM SIGPLAN\-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15\-17, 2015,S\. K\. Rajamani and D\. Walker \(Eds\.\),pp\. 637–650\.External Links:[Document](https://dx.doi.org/10.1145/2676726.2676980)Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p5.1)\.
- \[21\]G\. Klein, K\. Elphinstone, G\. Heiser, J\. Andronick, D\. A\. Cock, P\. Derrin, D\. Elkaduwe, K\. Engelhardt, R\. Kolanski, M\. Norrish, T\. Sewell, H\. Tuch, and S\. Winwood\(2009\)seL4: formal verification of an OS kernel\.InProceedings of the 22nd ACM Symposium on Operating Systems Principles, SOSP 2009, Big Sky, Montana, USA, October 11–14, 2009,pp\. 207–220\.External Links:[Document](https://dx.doi.org/10.1145/1629575.1629596)Cited by:[§1](https://arxiv.org/html/2605.23109#S1.p2.1)\.
- \[22\]A\. Lattuada, T\. Hance, J\. Bosamiya, M\. Brun, C\. Cho, H\. LeBlanc, P\. Srinivasan, R\. Achermann, T\. Chajed, C\. Hawblitzel, J\. Howell, J\. R\. Lorch, O\. Padon, and B\. Parno\(2024\)Verus: A practical foundation for systems verification\.InProceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles, SOSP 2024, Austin, TX, USA, November 4\-6, 2024,E\. Witchel, C\. J\. Rossbach, A\. C\. Arpaci\-Dusseau, and K\. Keeton \(Eds\.\),pp\. 438–454\.External Links:[Document](https://dx.doi.org/10.1145/3694715.3695952)Cited by:[§1](https://arxiv.org/html/2605.23109#S1.p2.1),[§2](https://arxiv.org/html/2605.23109#S2.p4.1),[§6](https://arxiv.org/html/2605.23109#S6.SS0.SSS0.Px1.p1.1)\.
- \[23\]T\. Leesatapornwongsa, J\. F\. Lukman, S\. Lu, and H\. S\. Gunawi\(2016\)TaxDC: a taxonomy of non\-deterministic concurrency bugs in datacenter distributed systems\.InProceedings of the 21st International Conference on Architectural Support for Programming Languages and Operating Systems \(ASPLOS\),pp\. 517–530\.Cited by:[§1](https://arxiv.org/html/2605.23109#S1.p1.1)\.
- \[24\]K\. R\. M\. Leino\(2010\)Dafny: an automatic program verifier for functional correctness\.InLogic for Programming, Artificial Intelligence, and Reasoning — 16th International Conference, LPAR\-16, Dakar, Senegal, April 25–May 1, 2010, Revised Selected Papers,E\. M\. Clarke and A\. Voronkov \(Eds\.\),Lecture Notes in Computer Science, Vol\.6355,pp\. 348–370\.External Links:[Document](https://dx.doi.org/10.1007/978-3-642-17511-4%5F20)Cited by:[§1](https://arxiv.org/html/2605.23109#S1.p2.1),[§2](https://arxiv.org/html/2605.23109#S2.p4.1)\.
- \[25\]X\. Leroy\(2009\)Formal verification of a realistic compiler\.Communications of the ACM52\(7\),pp\. 107–115\.External Links:[Document](https://dx.doi.org/10.1145/1538788.1538814)Cited by:[§1](https://arxiv.org/html/2605.23109#S1.p2.1)\.
- \[26\]M\. Lesani, C\. J\. Bell, and A\. Chlipala\(2016\)Chapar: certified causally consistent distributed key\-value stores\.InProceedings of the 43rd Annual ACM SIGPLAN\-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St\. Petersburg, FL, USA, January 20 \- 22, 2016,R\. Bodík and R\. Majumdar \(Eds\.\),pp\. 357–370\.External Links:[Link](https://doi.org/10.1145/2837614.2837622),[Document](https://dx.doi.org/10.1145/2837614.2837622)Cited by:[Appendix A](https://arxiv.org/html/2605.23109#A1.p1.1),[§I\.6](https://arxiv.org/html/2605.23109#A9.SS6.p1.1),[Table 8](https://arxiv.org/html/2605.23109#A9.T8.1.8.6.3.1.1),[Appendix I](https://arxiv.org/html/2605.23109#A9.p1.1),[§1](https://arxiv.org/html/2605.23109#S1.p2.1),[§1](https://arxiv.org/html/2605.23109#S1.p7.5),[§2](https://arxiv.org/html/2605.23109#S2.p5.1),[§5\.1](https://arxiv.org/html/2605.23109#S5.SS1.p2.1),[§5\.1](https://arxiv.org/html/2605.23109#S5.SS1.p4.1),[§5\.2](https://arxiv.org/html/2605.23109#S5.SS2.p2.3),[§5](https://arxiv.org/html/2605.23109#S5.p1.1),[footnote 2](https://arxiv.org/html/2605.23109#footnote2)\.
- \[27\]Z\. Li, Z\. Yang, H\. Zhao, A\. Zhao, S\. Tang, K\. Yang, A\. Gupta, Z\. Su, C\. Jin,et al\.\(2026\)Goedel\-code\-prover: hierarchical proof search for open state\-of\-the\-art code verification\.arXiv preprint arXiv:2603\.19329\.Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p4.1)\.
- \[28\]W\. Lloyd, M\. J\. Freedman, M\. Kaminsky, and D\. G\. Andersen\(2013\)Stronger semantics for low\-latency geo\-replicated storage\.InProc\. NSDI,Cited by:[Figure 26](https://arxiv.org/html/2605.23109#A9.F26),[Figure 26](https://arxiv.org/html/2605.23109#A9.F26.3.2)\.
- \[29\]E\. Lohn and S\. Welleck\(2024\)miniCodeProps: a minimal benchmark for proving code properties\.Note:arXiv:2406\.11915Cited by:[§E\.1](https://arxiv.org/html/2605.23109#A5.SS1.SSS0.Px1.p1.1),[Table 6](https://arxiv.org/html/2605.23109#A5.T6.7.4.2.1),[§1](https://arxiv.org/html/2605.23109#S1.p8.7)\.
- \[30\]C\. Loughridge, Q\. Sun, S\. Ahrenbach, F\. Cassano, C\. Sun, Y\. Sheng, A\. Mudide, M\. R\. H\. Misu, N\. Amin, and M\. Tegmark\(2024\)DafnyBench: a benchmark for formal software verification\.Note:arXiv:2406\.08467Cited by:[§E\.1](https://arxiv.org/html/2605.23109#A5.SS1.SSS0.Px1.p1.1),[Table 6](https://arxiv.org/html/2605.23109#A5.T6.7.3.1.1),[§1](https://arxiv.org/html/2605.23109#S1.p8.7)\.
- \[31\]D\. J\. Mankowitz, A\. Michi, A\. Zhernov, M\. Gelmi, M\. Selvi, C\. Paduraru, E\. Leurent, S\. Iqbal, J\. Lespiau, A\. Ahern, T\. Köppe, K\. Millikin, S\. Gaffney, S\. Elster, J\. Broshear, C\. Gamble, K\. Milan, R\. Tung, M\. Hwang, A\. T\. Cemgil, M\. Barekatain, Y\. Li, A\. Mandhane, T\. Hubert, J\. Schrittwieser, D\. Hassabis, P\. Kohli, M\. A\. Riedmiller, O\. Vinyals, and D\. Silver\(2023\)Faster sorting algorithms discovered using deep reinforcement learning\.Nature618\(7964\),pp\. 257–263\.External Links:[Document](https://dx.doi.org/10.1038/s41586-023-06004-9)Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p3.1)\.
- \[32\]Z\. Manna and R\. Waldinger\(1979\)Synthesis: dreams→\\toprograms\.IEEE Transactions on Software EngineeringSE\-5\(4\),pp\. 294–328\.Cited by:[§4](https://arxiv.org/html/2605.23109#S4.p2.2)\.
- \[33\]Z\. Manna and R\. Waldinger\(1980\)A deductive approach to program synthesis\.ACM Transactions on Programming Languages and Systems2\(1\),pp\. 90–121\.External Links:[Document](https://dx.doi.org/10.1145/357084.357090)Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p5.1),[§3](https://arxiv.org/html/2605.23109#S3.p3.1),[§4](https://arxiv.org/html/2605.23109#S4.p2.2)\.
- \[34\]E\. Mugnier, E\. A\. Gonzalez, R\. Jhala, N\. Polikarpova, and Y\. Zhou\(2025\)Laurel: unblocking automated verification with large language models\.PACMPL \(OOPSLA\)\.Note:arXiv:2405\.16792Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p4.1)\.
- \[35\]A\. Novikov, N\. Vũ, M\. Eisenberger, E\. Dupont, P\. Huang, A\. Z\. Wagner, S\. Shirobokov, B\. Kozlovskii, F\. J\. R\. Ruiz, A\. Mehrabian, M\. P\. Kumar, A\. See, S\. Chaudhuri, G\. Holland, A\. Davies, S\. Nowozin, P\. Kohli, and M\. Balog\(2025\)AlphaEvolve: a coding agent for scientific and algorithmic discovery\.Note:arXiv:2506\.13131Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p3.1)\.
- \[36\]A\. Ospanov, F\. Farnia, and R\. Yousefzadeh\(2025\)APOLLO: automated LLM and Lean collaboration for advanced formal reasoning\.Note:arXiv:2505\.05758Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p4.1)\.
- \[37\]T\. S\. Pillai, V\. Chidambaram, R\. Alagappan, S\. Al\-Kiswany, A\. C\. Arpaci\-Dusseau, and R\. H\. Arpaci\-Dusseau\(2014\)All file systems are not created equal: on the complexity of crafting crash\-consistent applications\.InProceedings of the 11th USENIX Conference on Operating Systems Design and Implementation,OSDI’14,USA,pp\. 433–448\.External Links:ISBN 9781931971164Cited by:[§1](https://arxiv.org/html/2605.23109#S1.p1.1)\.
- \[38\]N\. Polikarpova, I\. Kuraj, and A\. Solar\-Lezama\(2016\)Program synthesis from polymorphic refinement types\.InProceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13\-17, 2016,pp\. 522–538\.External Links:[Document](https://dx.doi.org/10.1145/2908080.2908093)Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p5.1)\.
- \[39\]C\. Qian, W\. Liu, H\. Liu, N\. Chen, Y\. Dang, J\. Li, C\. Yang, W\. Chen, Y\. Su, X\. Cong, J\. Xu, D\. Li, Z\. Liu, and M\. Sun\(2024\)ChatDev: communicative agents for software development\.InACL,Note:arXiv:2307\.07924Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p3.1)\.
- \[40\]Z\. Z\. Ren, Z\. Shao, J\. Song, H\. Xin, H\. Wang, W\. Zhao, L\. Zhang, Z\. Fu, Q\. Zhu, D\. Yang, Z\. F\. Wu, Z\. Gou, S\. Ma, H\. Tang, Y\. Liu, W\. Gao, D\. Guo, and C\. Ruan\(2025\)DeepSeek\-Prover\-V2: advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition\.Note:arXiv:2504\.21801Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p4.1)\.
- \[41\]B\. Romera\-Paredes, M\. Barekatain, A\. Novikov, M\. Balog, M\. P\. Kumar, E\. Dupont, F\. J\. R\. Ruiz, J\. S\. Ellenberg, P\. Wang, O\. Fawzi, P\. Kohli, and A\. Fawzi\(2024\)Mathematical discoveries from program search with large language models\.Nature625\(7995\),pp\. 468–475\.External Links:[Document](https://dx.doi.org/10.1038/s41586-023-06924-6)Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p3.1)\.
- \[42\]W\. Ruida, R\. Pan, Y\. Li, J\. Zhang, Y\. Jia, S\. Diao, R\. Pi, J\. Hu, and T\. Zhang\(2025\)MA\-lot: model\-collaboration lean\-based long chain\-of\-thought reasoning enhances formal theorem proving\.InForty\-second International Conference on Machine Learning,Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p4.1)\.
- \[43\]U\. Sharma, R\. Jung, J\. Tassarotti, M\. F\. Kaashoek, and N\. Zeldovich\(2023\)Grove: a separation\-logic library for verifying distributed systems\.InProceedings of the 29th Symposium on Operating Systems Principles, SOSP 2023, Koblenz, Germany, October 23\-26, 2023,J\. Flinn, M\. I\. Seltzer, P\. Druschel, A\. Kaufmann, and J\. Mace \(Eds\.\),pp\. 113–129\.External Links:[Document](https://dx.doi.org/10.1145/3600006.3613172)Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p5.1)\.
- \[44\]N\. Shinn, F\. Cassano, E\. Berman, A\. Gopinath, K\. Narasimhan, and S\. Yao\(2023\)Reflexion: language agents with verbal reinforcement learning\.InNeurIPS,Note:arXiv:2303\.11366Cited by:[§1](https://arxiv.org/html/2605.23109#S1.p1.1),[§2](https://arxiv.org/html/2605.23109#S2.p3.1)\.
- \[45\]A\. Solar\-Lezama, L\. Tancau, R\. Bodík, S\. A\. Seshia, and V\. A\. Saraswat\(2006\)Combinatorial sketching for finite programs\.InProceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2006, San Jose, CA, USA, October 21\-25, 2006,J\. P\. Shen and M\. Martonosi \(Eds\.\),pp\. 404–415\.External Links:[Document](https://dx.doi.org/10.1145/1168857.1168907)Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p5.1),[§4](https://arxiv.org/html/2605.23109#S4.p3.3)\.
- \[46\]A\. Solar\-Lezama\(2008\)Program synthesis by sketching\.Ph\.D\. Thesis,UC Berkeley\.Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p5.1),[§4](https://arxiv.org/html/2605.23109#S4.p3.3)\.
- \[47\]C\. Sun, Y\. Sheng, O\. Padon, and C\. Barrett\(2024\)Clover: closed\-loop verifiable code generation\.InSAIV,Note:arXiv:2310\.17807Cited by:[3rd item](https://arxiv.org/html/2605.23109#A5.I2.i3.p1.3),[Table 6](https://arxiv.org/html/2605.23109#A5.T6.7.7.5.1),[§1](https://arxiv.org/html/2605.23109#S1.p8.7),[§2](https://arxiv.org/html/2605.23109#S2.p2.1)\.
- \[48\]X\. Sun, W\. Ma, J\. T\. Gu, Z\. Ma, T\. Chajed, J\. Howell, A\. Lattuada, O\. Padon, L\. Suresh, A\. Szekeres, and T\. Xu\(2024\)Anvil: verifying liveness of cluster management controllers\.In18th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2024, Santa Clara, CA, USA, July 10\-12, 2024,A\. Gavrilovska and D\. B\. Terry \(Eds\.\),pp\. 649–666\.External Links:[Link](https://www.usenix.org/conference/osdi24/presentation/sun-xudong)Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p5.1)\.
- \[49\]A\. Thakur, G\. Tsoukalas, Y\. Wen, J\. Xin, and S\. Chaudhuri\(2024\)An in\-context learning agent for formal theorem\-proving\.InCOLM,Note:arXiv:2310\.04353Cited by:[2nd item](https://arxiv.org/html/2605.23109#A5.I1.i2.p1.1),[§2](https://arxiv.org/html/2605.23109#S2.p4.1)\.
- \[50\]K\. Thompson, N\. Saavedra, P\. Carrott, K\. Fisher, A\. Sanchez\-Stern, Y\. Brun, J\. F\. Ferreira, S\. Lerner, and E\. First\(2025\)Rango: adaptive retrieval\-augmented proving for automated software verification\.InICSE,Note:arXiv:2412\.14063\. Introduces the CoqStoq benchmark\.Cited by:[4th item](https://arxiv.org/html/2605.23109#A5.I1.i4.p1.1),[§E\.1](https://arxiv.org/html/2605.23109#A5.SS1.SSS0.Px1.p1.1),[Table 6](https://arxiv.org/html/2605.23109#A5.T6.7.6.4.1),[§1](https://arxiv.org/html/2605.23109#S1.p8.7)\.
- \[51\]H\. Wang, M\. Unsal, X\. Lin, M\. Baksys, J\. Liu, M\. Dos Santos, F\. Sung, M\. Vinyes, Z\. Ying, Z\. Zhu, J\. Lu, H\. de Saxcé, B\. Bailey, C\. Song, C\. Xiao, D\. Zhang, E\. Zhang, F\. Pu, H\. Zhu, J\. Liu, J\. Bayer, J\. Michel, L\. Yu, L\. Dreyfus\-Schmidt, L\. Tunstall, L\. Pagani, M\. Machado, P\. Bourigault, R\. Wang, S\. Polu, T\. Barroyer, W\. Li, Y\. Niu, Y\. Fleureau, Y\. Hu, Z\. Yu, Z\. Wang, Z\. Yang, Z\. Liu, and J\. Li\(2025\)Kimina\-Prover preview: towards large formal reasoning models with reinforcement learning\.Note:arXiv:2504\.11354Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p4.1)\.
- \[52\]R\. Wang, J\. Zhang, Y\. Jia, R\. Pan, S\. Diao, R\. Pi, and T\. Zhang\(2024\)TheoremLlama: transforming general\-purpose llms into lean4 experts\.In2024 Conference on Empirical Methods in Natural Language Processing, EMNLP 2024,pp\. 11953–11974\.Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p4.1)\.
- \[53\]J\. Wei, X\. Wang, D\. Schuurmans, M\. Bosma, E\. H\. Chi, Q\. Le, and D\. Zhou\(2022\)Chain of thought prompting elicits reasoning in large language models\.CoRRabs/2201\.11903\.External Links:[Link](https://arxiv.org/abs/2201.11903),2201\.11903Cited by:[§1](https://arxiv.org/html/2605.23109#S1.p6.1)\.
- \[54\]C\. Wen, J\. Cao, J\. Su, Z\. Xu, S\. Qin, M\. He, H\. Li, S\. Cheung, and C\. Tian\(2024\)Enchanting program specification synthesis by large language models using static analysis and program verification\.Note:arXiv:2404\.00762Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p2.1)\.
- \[55\]J\. R\. Wilcox, D\. Woos, P\. Panchekha, Z\. Tatlock, X\. Wang, M\. D\. Ernst, and T\. E\. Anderson\(2015\)Verdi: a framework for implementing and formally verifying distributed systems\.InProceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15\-17, 2015,D\. Grove and S\. M\. Blackburn \(Eds\.\),pp\. 357–368\.External Links:[Link](https://doi.org/10.1145/2737924.2737958),[Document](https://dx.doi.org/10.1145/2737924.2737958)Cited by:[§1](https://arxiv.org/html/2605.23109#S1.p2.1),[§2](https://arxiv.org/html/2605.23109#S2.p5.1)\.
- \[56\]Q\. Wu, G\. Bansal, J\. Zhang, Y\. Wu, B\. Li, E\. Zhu, L\. Jiang, X\. Zhang, S\. Zhang, J\. Liu,et al\.\(2024\)Autogen: enabling next\-gen llm applications via multi\-agent conversations\.InFirst conference on language modeling,Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p3.1)\.
- \[57\]C\. Yang, X\. Li, M\. R\. H\. Misu, J\. Yao, W\. Cui, Y\. Gong, C\. Hawblitzel, S\. Lahiri, J\. R\. Lorch, S\. Lu, F\. Yang, Z\. Zhou, and S\. Lu\(2025\)AutoVerus: automated proof generation for Rust code\.InOOPSLA,Note:arXiv:2409\.13082Cited by:[3rd item](https://arxiv.org/html/2605.23109#A5.I1.i3.p1.1),[§E\.1](https://arxiv.org/html/2605.23109#A5.SS1.SSS0.Px1.p1.1),[Table 6](https://arxiv.org/html/2605.23109#A5.T6.7.5.3.1),[§1](https://arxiv.org/html/2605.23109#S1.p8.7),[§2](https://arxiv.org/html/2605.23109#S2.p4.1)\.
- \[58\]J\. Yang, C\. E\. Jimenez, A\. Wettig, K\. Lieret, S\. Yao, K\. Narasimhan, and O\. Press\(2024\)SWE\-agent: agent\-computer interfaces enable automated software engineering\.InNeurIPS,Note:arXiv:2405\.15793Cited by:[§1](https://arxiv.org/html/2605.23109#S1.p1.1),[§2](https://arxiv.org/html/2605.23109#S2.p3.1)\.
- \[59\]K\. Yang and J\. Deng\(2019\)Learning to prove theorems via interacting with proof assistants\.InICML,Note:arXiv:1905\.09381Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p4.1)\.
- \[60\]K\. Yang, A\. M\. Swope, A\. Gu, R\. Chalamala, P\. Song, S\. Yu, S\. Godil, R\. Prenger, and A\. Anandkumar\(2023\)LeanDojo: theorem proving with retrieval\-augmented language models\.InNeurIPS,Note:arXiv:2306\.15626Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p4.1)\.
- \[61\]Z\. Ye, Z\. Yan, J\. He, T\. Kasriel, K\. Yang, and D\. Song\(2026\)VERINA: benchmarking verifiable code generation\.InInternational Conference on Learning Representations \(ICLR\),Note:arXiv:2505\.23135Cited by:[1st item](https://arxiv.org/html/2605.23109#A5.I2.i1.p1.2),[Table 6](https://arxiv.org/html/2605.23109#A5.T6.7.8.6.1),[§1](https://arxiv.org/html/2605.23109#S1.p8.7),[§2](https://arxiv.org/html/2605.23109#S2.p5.1)\.
- \[62\]H\. Zhao, Z\. Yang, J\. Li, D\. He, Z\. Li, C\. Jin, V\. V\. Veeravalli, A\. Gupta, and S\. Arora\(2026\)AlgoVeri: an aligned benchmark for verified code generation on classical algorithms\.arXiv preprint arXiv:2602\.09464\.Cited by:[2nd item](https://arxiv.org/html/2605.23109#A5.I2.i2.p1.2),[§1](https://arxiv.org/html/2605.23109#S1.p8.7)\.
- \[63\]X\. Zhao, L\. Zheng, H\. Bo, C\. Hu, U\. Thakker, and L\. Kong\(2024\)Subgoalxl: subgoal\-based expert learning for theorem proving\.arXiv preprint arXiv:2408\.11172\.Cited by:[§2](https://arxiv.org/html/2605.23109#S2.p4.1)\.

## Appendix ASpecifications and the IDS Suite Dataset

Of the seven specifications evaluated in[section˜5](https://arxiv.org/html/2605.23109#S5), one is Chapar’s published causal\-consistency specLesaniet al\.\([2016](https://arxiv.org/html/2605.23109#bib.bib6)\)and the other six are IDS suite specs we wrote with a formal\-verification and distributed\-systems expert \(1,0181\{,\}018lines of Rocq across five spec files; RYW\+MW is the joint composition of RYW and MW with no separate spec;[table˜3](https://arxiv.org/html/2605.23109#A1.T3)\)\. Formal definitions are in[appendix˜I](https://arxiv.org/html/2605.23109#A9), which also gives two reference implementations of IDS suite CC \(vector\-clock and dependency\-map variants\) and the Lloyd\-Freedman protocol \(the COPS causal\-consistency protocol\) as a systems\-scale reference\.

Table 3:The seven specifications\. Chapar CC is a published spec; the six IDS suite specs are expert\-written for this paper\.*Property*summarises the consistency guarantee;*LoC*is lines of Rocq for the spec definition\.#### Common shape\.

Every spec is a RocqModule Typewith the same seven method signatures \(getReq,getGuard,get,getRes,putReq,putGuard,put\), aStatetype, anUpdatetype, and an operational semantics on client\-replica configurations\. IDS consumes this shape directly\.

#### Generality\.

IDS is not tuned to any individual spec: the same agent, prompts, and tools handle every spec we evaluate\. Any specification matching theModule Typeshape above is a candidate target for the same loop\.

## Appendix BSynthesis Results: Per\-Spec Artifacts

All seven artifacts pass Rocq’s kernel with noAdmitted,Axiom,Hypothesis, orParameter\. The three CC specs \(Chapar CC:3,0373\{,\}037lines /7979lemmas; IDS suite CC:3,8073\{,\}807/121121; LCC:3,9243\{,\}924/128128\) are44–6×6\\timeslarger than the four session specs because their proofs span all replicas, not just sender and receiver\.

Table 4:Per\-spec implementation choice and proof artifact size\. Lemmas==Qedcount; lines viawc \-l\.#### Implementation rationale\.

Chapar CC\.The7979lemmas split:1111per\-method refinement \(one perget/put/update/guard/init\),1111reachable\-state invariants,77causality preservation,3939clock and per\-key store algebra, and1111execution\-model helpers\.

Session guarantees \(RYW, MW, MR, RYW\+MW\)\.All four share the same assoc\-list skeleton; each parameterizes the per\-entry payload to its consistency property: RYW carries \(val, client, ts\) to detect own writes, MW extends to \(val, client→\\tots\) to enforce writer order, MR uses one entry per \(key, client\) updated in place, RYW\+MW combines both\. The proof technique is shared too: each session uses heavy case\-analysis viaNat\.eq\_decon key and client equality \(8080–100100splits per spec\), varying only in which payload field the splits land on\. Each Get scans only the distinct keys touched, not the full Put history\. MR is the hardest session spec because its Put proof splits into four sub\-cases \(same vs different key, same vs different client\), each closed by case\-analysis onNat\.eq\_dec\.

IDS suite CC\.A vector clock, a per\-key vector\-clock map, and a balanced\-tree store; the balanced tree keeps Get logarithmic in distinct keys rather than linear in prior Puts\. Of the121121lemmas:88are the step\-by\-step simulation,3232are refinement\-relation invariants for the state components \(cell, replica, snapshot\) and their preservation under updates,1919are vector\-clock algebra; the remaining6262are update, lookup, owner, and dependency\-tracking algebra\. Get’s proof closes by applying the relation that ties the implementation’s vector clocks plus per\-client owner lists \(per\-key tracking of which client most recently wrote each entry\) to the spec’s dependency sets\.

LCC\.A vector clock, a per\-key vector\-clock map, and a balanced\-tree store, with dependency entries tagged with a label \(a44\-tuple of client, timestamp, key, label\) and projections at Get filtered by the requesting client’s interest mask\. The proof closes by step\-by\-step simulation; the simulation relation ties the implementation’s label\-tagged vector\-clock representation to the spec’s label\-filtered dependency sets\. Of the128128lemmas:66are the step\-by\-step simulation,2525are refinement\-relation invariants and extensions for state components \(cells, replicas, snapshots, key\-snapshots\),1919are vector\-clock algebra; the remaining7878are update, lookup, owner, and dependency\-tracking algebra\.

#### Synthesis trajectories\.

The artifacts above are not the first design IDS attempted\. In each case, the proof stalled on a goal that resisted splitting under the spec’s natural state representation; the ISA’s reloader abandoned the branch, and the proposer pivoted to a representation under which the goal decomposed\.

Chapar CC\.The hardest case in any causal\-consistency proof shows that whenever a replica delivers a remote message, it has already observed every update the message transitively depends on\. IDS’ first attempt kept the global state representation closest to the spec, under which the delivery lemma had to range over every in\-flight message at every replica together, and the DSA could not split it\. After the search stalled, the reloader abandoned that branch and the proposer revised the design to a per\-key store with per\-entry sender, sender\-clock, and dependency vector\. The proposer then split the delivery invariant into three sub\-lemma classes \(per\-message, per\-store\-entry, per\-replica\-clock\), each closing under the new representation\. The representation was chosen by what split the proof, not by performance; the per\-put performance win reported in[section˜5\.3](https://arxiv.org/html/2605.23109#S5.SS3)is a consequence\.

Monotonic reads\.Both agent baselines, and IDS’ first attempt, stalled on the function\-from\-key\-to\-value representation\. After the reloader abandoned that branch, the agent revised the design to a flat list of per\-\(key, client\) entries updated in place, after which the put proof split into four sub\-cases on key and client equality\.

IDS suite CC and LCC\.The winning move is to break the simulation goal into per\-message and per\-store\-entry sub\-lemmas, each closing against the per\-key store and label\-tagged dependency entries respectively\. The baselines try the combined goal in one shot and time out within the budget\.

## Appendix CImplementing Distributed\-KV Specifications with Coding Agents \(No Proof\)

#### Setup\.

We test Codex \(gpt\-5\.4\) on four KV\-store consistency properties \(RYW, MW, MR, and CC\)\. For each property, Codex generates 100 candidate implementations under two prompt conditions, then picks its single best candidate\. That selected implementation is the agent’s output for that \(property, condition\)\.

*Setting \(1\) Spec\-Given\.*Codex receives the formal Rocq specification and the module\-type signature\.

*Setting \(2\) NL\-Only \(“vibe coding”\)\.*Codex receives only a one\-paragraph natural\-language description of the property \(reproduced verbatim below\) and the module\-type signature\.

Each of the 100 generation sessions runs independently and can compile, edit, and test its own code\. The selector pass is also Codex, with the same compile and test access\. The selected implementation must use bounded state, cannot copy any reference implementation, and cannot useAdmitted,Axiom,Hypothesis, orParameter\(so the agent cannot stub out unfilled work\)\. The agent does not write any refinement proof\.

We evaluate the selected implementation in two stages\.*Stage 1 \(test\)\.*We run the implementation on an adversarial multi\-client scenario; if it accepts an operation the abstract specification rejects on this scenario, Stage 1 fails\.*Stage 2 \(proof\)\.*If Stage 1 passes, IDS attempts the refinement proof against the abstract specification\. If IDS cannot close the proof within budget, Stage 2 fails\. We split into two stages because proof attempts are much more expensive than scenario testing\. If Stage 1 fails, Stage 2 fails too: an implementation that breaks the spec on a single trace cannot be proven correct on every trace\.

#### Property statements \(LLM\-visible in Setting 2\)\.

RYW \(Read\-Your\-Writes\)\.Each client must observe its own previous writes\. If a client writes a value to a key and later reads that key in the same session, the read must return the client’s value or a more recent one\.

MW \(Monotonic Writes\)\.Writes by the same client are applied at every replica in the order the client issued them\.

MR \(Monotonic Reads\)\.Successive reads by the same client observe non\-decreasing replica states: once a client has seen a value, later reads must not appear older\.

CC \(Causal Consistency\)\.If operationAAcausally precedes operationBB\(eitherAAcomes beforeBBin the same client’s session, orBBreads a value written byAA\), every client that seesBBmust also have seenAA\.

Table 5:Outcome of best\-of\-N=100N\{=\}100implementation\-only synthesis with Codex\.1= passed,0= failed\. Stage 1: the selected implementation runs through a fixed adversarial multi\-client scenario without violating the abstract specification on that scenario\. Stage 2: IDS builds a refinement proof of the implementation against the abstract specification within budget\. Cost is thegpt\-5\.4token cost for the 100 generations plus the selection pass\.
#### Result and takeaway\.

Best\-of\-N=100N=100produces a verified implementation on 1 of 4 properties when given the formal specification \(Setting 1, RYW\), and on 0 of 4 from natural language alone \(Setting 2\)\. The two simpler session properties \(RYW and MW\) consistently pass the scenario test in both settings, but only RYW with the formal spec also passes the refinement proof\. The harder properties \(MR and CC\) fail even the scenario test in both settings: the textbook patterns Codex selects \(vector\-clock dominance, last\-write\-wins\) do not implement the per\-key or causal\-order behavior these specs demand\. Two failure modes appear: \(a\) implementations that fail on a single adversarial trace, and \(b\) implementations that pass the trace but cannot be proven correct on every reachable state\. IDS avoids both by integrating the refinement proof into synthesis rather than running it as a post\-hoc check; in the main evaluation it closes the proof on all 7 specifications\.

## Appendix DAdditional Performance Results and Throughput Breakdown

IDS’ gains over the reference implementations all share one mechanism: IDS’ state representations bound per\-op cost by the spec, while the references’ per\-op cost grows with workload size\.[section˜D\.1](https://arxiv.org/html/2605.23109#A4.SS1)measures this on all five IDS suite specs with cluster\-runnable implementations \(RYW, MR, MW, RYW\+MW, IDS suite CC\), shows Chapar CC at the top of the figure for comparison, and adds an illustrative LCC row \(labeled causal consistency: each client subscribes to a set of topic labels and only sees causality enforced on those\)\. Across the IDS suite, throughput tracks consistency strength \(RYW\>\>MW\>\>RYW\+MW\>\>MR\>\>LCC\>\>IDS suite CC at put=50%=50\\%\) because stricter specs require more checking work per operation\. Chapar CC and IDS suite CC are both causal\-consistency variants but their reference implementations are designed differently \(Chapar’s reads one position out of a flat list of per\-write dependencies, while IDS suite’s compares an entire per\-client clock vector and atomically updates the writer’s slot on every Put\), so the two CC rows show different per\-op work at the same correctness level\.[sections˜D\.2](https://arxiv.org/html/2605.23109#A4.SS2)and[D\.3](https://arxiv.org/html/2605.23109#A4.SS3)decompose the gap on Chapar CC and Monotonic Reads\.

#### Setup details \(extending[section˜5\.1](https://arxiv.org/html/2605.23109#S5.SS1)\)\.

Cluster zone:us\-central1\-f\. Each VM is ane2\-standard\-2\(2 vCPU, 8 GB RAM\) on Debian 12\. Toolchain: OCaml 4\.13\.1 \(dune 3\.10\) and Rocq 8\.18\.0\. Throughput is the sum across theNW=4\\text\{NW\}=4workers ofN/twN/t\_\{w\}, wheretwt\_\{w\}is each worker’s wall\-clock time andNNis its ops count, taking the median over three runs per cell; the put\-rate sweep usesN=1000N=1000\(4,000 cluster ops total per run\) and the scaling sweep variesN∈\{1,000,2,000,5,000,20,000\}N\\in\\\{1\{,\}000,2\{,\}000,5\{,\}000,20\{,\}000\\\}\. Per\-operation latency is bracketed inside the runtime aroundput\_method/get\_methodand merged across workers; p99 is the 99th percentile of the pooled per\-op latency distribution\. Peak memory is the worker maximum ofMaximum resident set sizefrom/usr/bin/time \-v, taking the median over three runs\. Workload parameters:key\_range=50\\texttt\{key\\\_range\}=50,val\_range=100,000\\texttt\{val\\\_range\}=100\{,\}000, fixed seed4242\. The cluster uses a Chapar\-style UDP runtime \(runtime\_doctex\.ml\) adapted to the seven\-method doctexAlgDefinterface; we patched a socket bug for OCaml 4\.13 / Debian 12\.

### D\.1Per\-protocol curves: all five IDS suite specs

#### Result\.

Read\-then\-write specs cause the reference to exceed our180180s wall\-clock cap at every put rate measured: in[fig\.˜9](https://arxiv.org/html/2605.23109#A4.F9)the reference’s MW and RYW\+MW rows show red×\\timesat every cell, with no measurable throughput\. IDS runs cleanly throughout:152152kops/s on MW and139139kops/s on RYW\+MW at put=60%=60\\%\. The mechanism is a closure chain: the reference stores per\-replica state as a function from key to value \(a function\-as\-map\); after extraction to OCaml, each priorPutadds a nested closure that aGetmust unwrap\. The read\-then\-write check re\-evaluates this chain on everyPut; combined with UDP packet reordering and the protocol’s no\-retry compare\-and\-swap, throughput collapses to zero\. RYW has no read\-then\-write check, so its reference is competitive with IDS across the put\-rate sweep: within roughly20%20\\%in either direction depending on workload mix, with IDS winning at low put rate \(pct=20=20\) and the reference faster at high put rate \(pct=60=60–7070\)\. The reversal is a per\-Put cost trade: IDS’ assoc\-list rewrites its spine on everyPut\(O​\(K\)O\(K\)cell allocations,KK= unique keys touched\), while the reference’s function\-as\-map prepends a single closure layer perPut\(O​\(1\)O\(1\)heap cell\)\. At low put rate the assoc\-list’sO​\(K\)O\(K\)Getlookup beats the reference’s closure\-chain walk; at high put rate the per\-Putallocation cost dominates\. MR shows the same chain\-walk cost onGet\(per\-layer slope quantified in[section˜D\.3](https://arxiv.org/html/2605.23109#A4.SS3)\); IDS suite CC follows the same mechanism with IDS’ balanced\-tree store keeping Get logarithmic in distinct keys\. Memory: IDS’ assoc\-list pays0\.10\.1–1\.01\.0MB more on RYW \(per\-entry overhead\) and runs in the same55–66MB envelope as the reference on the other specs where the reference completes; on MW and RYW\+MW the reference produces no memory measurement \(it never completes a run\)\. All memory traces are atN=1,000N=1\{,\}000ops/worker; IDS suite CC’s vector\-clock state isO​\(\#clients\)O\(\\text\{\\\#clients\}\), so its trace is flat across the put\-rate sweep at this workload size\. At substantially largerNNor more clients, the message\-bus and per\-cell deps would push memory upward\. The rightmost column \(throughput vsNNat put=50%=50\\%\) confirms the mechanism on every spec: the reference’s throughput drops asNNgrows because each newPutextends the chain, while IDS’ assoc\-list and balanced\-tree structures keep throughput approximately flat\. Across the put\-rate sweep, both implementations’ throughput falls and p99 latency rises as put\-rate increases because eachPutis broadcast to every replica, so more writes mean more in\-flight messages and longer per\-op queue waits\.

#### Course correction on MW\.

Without performance feedback, IDS ships the first verifying design: a balanced\-tree store\. With performance feedback, the agent runs both candidates in its microbench harness and converges on the assoc\-list, which the cluster benchmark harness confirms at152152k ops/s at put=60%=60\\%\([fig\.˜9](https://arxiv.org/html/2605.23109#A4.F9)\)\. Performance feedback changes the search policy, not the correctness criterion; both candidates are verified IDS suite refinements\.

### D\.2Throughput breakdown: Chapar CC

![Refer to caption](https://arxiv.org/html/2605.23109v1/x6.png)Figure 7:Per\-component decomposition of Chapar’s two published baselines \(vector\-clock, list\-based\) and IDS’ Chapar implementation \(per\-key store entries, used here as internal pivot\)\. Bar height equals4/\(published cluster throughput\)4/\\text\{\(published cluster throughput\)\}inμ\\mus per worker op\. Each bar splits into local Get cost, the per\-key\-entries Put baseline \(same for all\), per\-algorithm extra wire bytes, and a per\-algorithm residualγ\\gamma\. Segments sum to the published value at every cell by construction\.#### Setup\.

We attribute each algorithm’s per\-op time to four pieces: its Get cost \(varies by algorithm\), a shared Put baseline \(per\-key entries:58\.4​μ58\.4\\,\\mus, the smallest of the three\), a wire\-bytes term proportional to extra bytes per Put \(β=18​μ\\beta=18\\,\\mus per byte, fit from vector\-clock vs per\-key entries\), and a CPU residualγ\\gammathat captures whatever the wire\-bytes term does not explain\. Marshaled bytes per Put on the cluster:44\.8144\.81\(vector\-clock\),41\.0541\.05\(list\-based\),39\.6239\.62\(per\-key entries\)\.

#### Result\.

Vector\-clock loses on wire bytes; list\-based loses on CPU\.Vector\-clockships\+5\.2\+5\.2bytes per Put over per\-key entries, mapping to\+47​μ\+47\\,\\mus of per\-op work at put=50%=50\\%; the residualγ\\gammais−1\.75​μ\-1\.75\\,\\mus, well below the bytes term\. Almost the entire gap is wire bytes\.List\-basedships only\+1\.4\+1\.4extra bytes per Put on average, yetγ=\+21\.6​μ\\gamma=\+21\.6\\,\\mus at put=50%=50\\%\. The list\-based replica stores the full history of delivered messages; receivers walk this list on every delivery \(causality check\), andGetwalks it again to find the most\-recent value for the requested key\. Vector\-clock and per\-key entries do constant\-time element\-wise lookups\.

### D\.3Throughput breakdown: Monotonic Reads

![Refer to caption](https://arxiv.org/html/2605.23109v1/x7.png)Figure 8:Getlatency vs\. closure depth \(number ofPuts preceding eachGetin the same worker trace\) for the three Monotonic Reads implementations at three put rates\. The IDS suite reference’sGetlatency grows linearly with depth \(slope0\.21​μ0\.21\\,\\mus per closure layer at put=20%=20\\%,R2=0\.95R^\{2\}=0\.95\)\. IDS’ assoc\-list slope is an order of magnitude smaller; the balanced\-tree variant’s slope is within statistical noise at every put rate\.#### Setup\.

Three MR implementations on the same runtime and identical wire format \(92\.8392\.83B perPuton average\): the IDS suite reference \(function\-as\-map\), IDS \(assoc\-list\), and a balanced\-tree alternative\. Throughput differences are CPU\-side\. The balanced tree is a control: it tests whether IDS’ win comes from the assoc\-list specifically or from any structure that does not walk a closure chain onGet\.

#### Where the cost lands\.

The reference pays onGet; the refinements pay onPut\. At put=50%=50\\%:

RegressingGetlatency against closure depth \(number ofPuts preceding aGetin the same worker trace\) confirms the reference’s chain walk: slope0\.21​μ0\.21\\,\\mus/layer at put=20%=20\\%\(R2=0\.95R^\{2\}=0\.95,[fig\.˜8](https://arxiv.org/html/2605.23109#A4.F8)\)\. Both refinements stay flat across every put rate measured \(\|slope\|<0\.025​μ\|\\text\{slope\}\|<0\.025\\,\\mus/layer\): bounded data structure, no chain to walk\. The balanced tree’s extra Put cost comes from rebalance\.

#### N\-scaling at put=50%=50\\%\.

The reference’s throughput drops as ops\-per\-workerNNgrows; IDS stays nearly flat:

AtN=1,000N=1\{,\}000IDS is1\.20×1\.20\\timesfaster; atN=20,000N=20\{,\}000the gap widens to1\.40×1\.40\\times\. Throughput drop fromN=1,000N=1\{,\}000toN=20,000N=20\{,\}000: reference1\.35×1\.35\\times, IDS1\.16×1\.16\\times\. The reference’s per\-Getclosure walk grows linearly with priorPuts, so its per\-op cost rises withNN; the assoc\-list’s lookup is bounded by the number of distinct keys in the workload \(50 here\), so its per\-op cost isNN\-independent and only message\-bus pressure causes the mild decline\.

![Refer to caption](https://arxiv.org/html/2605.23109v1/x8.png)Figure 9:Per\-protocol performance\. Top row is Chapar CC \(Chapar paper protocol\) shown for comparison; the next five rows are the IDS suite specs \(RYW, MR, MW, RYW\+MW, IDS suite CC\); the bottom LCC row is a single\-line illustrative trajectory of labeled causal consistency\. Columns: throughput \(kops/s\), p99 latency \(μ\\mus\), memory peak \(MB\), and throughput vs ops\-per\-workerNNat put=50%=50\\%\. Per\-protocolyy\-axes are dedicated so each row’s range is visible\. Solid==IDS; dashed==reference \(function\-as\-map\)\. Red×\\timesmarks runs that hit the180180s wall\-clock cap; on MW and RYW\+MW the reference times out at every put rate \(the reference’s read\-then\-write check on a function\-as\-map is the cause; see below\)\.

## Appendix EResults on Proof, Annotation, and Code\-and\-Proof Benchmarks

IDS beats every prior method on the four proof and annotation benchmarks, and reaches𝟏𝟕𝟔/𝟏𝟖𝟗\\mathbf\{176/189\}on VERINA against prior SOTA3838and agentic baselines Codex136136, Claude Code149149\([table˜7](https://arxiv.org/html/2605.23109#A5.T7)\)\.

Table 6:What each cross\-language benchmark gives the model and what the model must produce\. ✓ = given as input; ✗ = the model must generate it\. “Spec” covers preconditions and postconditions \(or the theorem statement, where applicable\)\. For DafnyBench the implementation body is given; only Dafny verification*hints*\(loop invariants, assertions, decreases clauses\) are stripped\. miniCodeProps and CoqStoq give the spec as a Lean / Coq theorem statement\.Table 7:Pass counts on verification benchmarks\. Bold==best per column\. The first four are proof\-only \(impl and spec given\); on these, IDS reduces to its DSA component since the ISA has no design space to search\. The last three are concurrent code\-and\-proof tasks\. Per\-benchmark slices, prior\-SOTA references, and CloverBench note in[appendix˜E](https://arxiv.org/html/2605.23109#A5)\.### E\.1Proof and annotation benchmarks

#### Setup\.

The model receives a complete task specification \(signature, preconditions, postconditions, and code where applicable\) and must produce verifier\-acceptable output: proof annotations on DafnyBenchLoughridgeet al\.\([2024](https://arxiv.org/html/2605.23109#bib.bib63)\)and Verus\-BenchYanget al\.\([2025](https://arxiv.org/html/2605.23109#bib.bib31)\), or a complete proof on miniCodePropsLohn and Welleck \([2024](https://arxiv.org/html/2605.23109#bib.bib64)\)and CoqStoqThompsonet al\.\([2025](https://arxiv.org/html/2605.23109#bib.bib79)\)\(modality in[table˜6](https://arxiv.org/html/2605.23109#A5.T6)\)\. For each benchmark we use the slice the prior SOTA method published its number on:

- •DafnyBench:100100hardest tasks; prior SOTA is DafnyProBanerjeeet al\.\([2026](https://arxiv.org/html/2605.23109#bib.bib65)\)\(from the DafnyBench paper\)\.
- •miniCodeProps:100100tasks from the sorting split; prior SOTA is COPRAThakuret al\.\([2024](https://arxiv.org/html/2605.23109#bib.bib28)\)\.
- •Verus\-Bench: full150150tasks; prior SOTA is AutoVerusYanget al\.\([2025](https://arxiv.org/html/2605.23109#bib.bib31)\)\.
- •CoqStoq:100100hardest tasks; prior SOTA is RangoThompsonet al\.\([2025](https://arxiv.org/html/2605.23109#bib.bib79)\)\.

#### Result\.

IDS reaches88/10088/100on DafnyBench,100/100100/100on miniCodeProps,149/150149/150on Verus\-Bench, and97/10097/100on CoqStoq \([table˜7](https://arxiv.org/html/2605.23109#A5.T7)\), beating the strongest prior on all four\. The largest absolute gap is on CoqStoq \(\+69\+69over Rango\); IDS hits a perfect100/100100/100on miniCodeProps, and on Verus\-Bench all three LLM methods are within1%1\\%of saturation \(IDS149149, Codex148148, Claude Code148148of150150\)\. Failures reflect per\-task budget caps and proofs requiring tactics or library\-specific lemmas the agent did not discover within budget \([section˜F\.1](https://arxiv.org/html/2605.23109#A6.SS1)\)\.

### E\.2Code\-and\-proof benchmarks

#### Setup\.

A second, recent line of benchmarks evaluates joint code\-and\-proof synthesis on single\-function algorithmic tasks \(sorting, search, list manipulation, basic arithmetic like factorial/gcd/Fibonacci\): the model receives a natural\-language description, signature, and spec, and produces both the code and a proof of correctness\. These tasks are strictly simpler than the distributed\-system specs of[section˜5\.2](https://arxiv.org/html/2605.23109#S5.SS2): no concurrency, no replication, no multi\-step operational semantics\.

- •VERINAYeet al\.\([2026](https://arxiv.org/html/2605.23109#bib.bib58)\):189189Lean tasks; prior SOTA is iterative refinement with Lean compiler feedback \(6464rounds\), reported in the VERINA paper\.
- •AlgoVeriZhaoet al\.\([2026](https://arxiv.org/html/2605.23109#bib.bib59)\):7777problems, each expressed in Dafny, Verus, and Lean; prior SOTA31/7731/77\(Gemini\-3 Flash, Dafny track, reported in the AlgoVeri paper\)\.
- •CloverBenchSunet al\.\([2024a](https://arxiv.org/html/2605.23109#bib.bib57)\):6262Dafny tasks\. We omit a Prior\-SOTA cell because Clover \(the only prior published method\) evaluates a different task: its consistency\-checker filters pre\-existing correct triples \(an87%87\\%acceptance rate, with13%13\\%false negatives where it rejects a known\-correct triple\)\. Our column reports end\-to\-end synthesis: given the spec, the model generates code and annotations, and the Dafny verifier accepts\.

#### Result\.

IDS reaches𝟏𝟕𝟔/𝟏𝟖𝟗\\mathbf\{176/189\}on VERINA, well above prior SOTA3838and agentic baselines Codex136136, Claude Code149149;𝟔𝟓/𝟕𝟕\\mathbf\{65/77\}on AlgoVeri’s Dafny track,2×2\\timesthe published Gemini\-3 Flash baseline of31/7731/77; and all three LLM methods saturate at62/6262/62on CloverBench\.

## Appendix FIDS Architecture Details

This appendix expands on the components introduced in[section˜4](https://arxiv.org/html/2605.23109#S4)and ablated in[section˜5\.4](https://arxiv.org/html/2605.23109#S5.SS4)\. The architecture instantiates the two\-level CEGIS\-style refinement of[section˜4](https://arxiv.org/html/2605.23109#S4)\. The inner loop is the DSA \([section˜F\.2](https://arxiv.org/html/2605.23109#A6.SS2)\): forward moves*Define*,*Prove*,*Decompose*extend the partial \(code, proof\) candidate, and the structured Rocq diagnostic from a failed step \([section˜F\.6](https://arxiv.org/html/2605.23109#A6.SS6)\) is a concrete witness that the candidate cannot close as written, used by the agent to choose*Repair*or*Revert*\. The outer loop is the ISA: a DSA’s stalled proof attempts and bench failures \([section˜F\.7](https://arxiv.org/html/2605.23109#A6.SS7)\) drive the proposer \([section˜F\.4](https://arxiv.org/html/2605.23109#A6.SS4)\) on tactical stalls and the reloader \([section˜F\.5](https://arxiv.org/html/2605.23109#A6.SS5)\) on strategic dead\-ends\. The audit step \([section˜F\.3](https://arxiv.org/html/2605.23109#A6.SS3)\) is orthogonal to refinement: it is a deterministic safety gate, not a counterexample signal\.

### F\.1Proof methodology

Each spec is a RocqModule Typecarrying aStatetype, anUpdatetype, seven method signatures \(getReq,getGuard,get,getRes,putReq,putGuard,put\), and an operational semantics on client–replica configurations\. The implementation IDS produces is anAlgDefmodule providing the same seven methods at concrete state types, plus aRefinementmodule proving forward simulation: every step the implementation can take corresponds to a step the abstract spec can take, on related states\. From theRefinementwe obtain aTraceInclusiontheorem: every observable trace of the implementation is also a trace of the abstract spec\.

The tactic vocabulary is standard Rocq:inversion,destruct,subst,rewrite,apply,econstructor; eauto,simpl,lia,congruence, with case\-analysis onNat\.eq\_decfor equality decisions on identifiers and timestamps\. Nofirstorder/intuitionshortcuts; noAdmitted, noAxiom, noHypothesis, noParameter\. Closure is verified by Rocq’s kernel\.

### F\.2DSA: deductive synthesis

The DSA is a Codex \(or Claude Code\) session per workspace performing the deductive\-synthesis loop of[fig\.˜3](https://arxiv.org/html/2605.23109#S4.F3)\. At each search\-tree node the agent moves forward with one of three primitives:

- •*Define*: declare or extend a state/message type or function body, withadmitplaceholders for parts not yet filled in \(e\.g\. adding aCellrecord to the per\-key store withcell\_depsstubbed\)\.
- •*Prove*: close an open proof obligation by replacingAdmittedwith a tactic sequence ending inQed, or extend an existing tactic block\.
- •*Decompose*: state a helper lemma asAdmittedand use it to advance the proof of an existing lemma; the helper is discharged in a later iteration\.

After each forward stepmakeruns and Rocq’s type\-checker is the only oracle\. On error, the agent backtracks with one of two primitives:

- •*Repair*: re\-attempt the failed step with a different tactic \(e\.g\.inductioninstead ofdestruct;liainstead ofomega\)\.
- •*Revert*: rewind to an earlier search\-tree node and choose a different forward primitive \(typically when the same compile error recurs three or more times\)\.

The agent’s initial brief is read fromCLAUDE\.mdin the workspace and instantiates the four briefings of[fig\.˜3](https://arxiv.org/html/2605.23109#S4.F3)\(methodology, auditability, design, tactical playbook\)\. The brief shown below is for the Rocq setting \(our IDS suite specs and Chapar CC, plus CoqStoq and miniCodeProps\); for cross\-language benchmarks we swap the verifier and surface tools to match the target language: Dafny \(DafnyBench, AlgoVeri\-Dafny, CloverBench\), Verus \(Verus\-Bench\), and Lean 4 \(VERINA\), with success criterion adapted accordingly \(e\.g\.dafny verifyaccepts,lake buildsucceeds,verusreports zero errors\)\.

Role: Deductive Synthesis Agent\.Given a specification, incrementally produce an implementation and a machine\-checked proof that it satisfies the specification\. The type\-checker is the only oracle and accepts a partial state \(with deferred holes\) as a valid intermediate\.Schema\.Synthesis is a finite sequence of well\-typed steps; the file must type\-check \(possibly with deferred holes\) after every step\. Take one forward move:•*Define*\(refinement\): introduce or extend aDefinition,Record,Inductive,Fixpoint, orModule; bodies may containadmitor invokeAdmittedlemmas\.•*Prove*\(closure\): replace anAdmittedlemma with a tactic sequence ending inQed, or extend an existing partial proof\.•*Decompose*\(lemma introduction\): state a helper lemma asAdmitted, use it to advance the current proof, and discharge it later\. This is the deferred\-hole device of deductive synthesis\.On error, backtrack:*Repair*\(different tactic on the same goal, e\.g\.inductioninstead ofdestruct,liainstead ofomega\) or*Revert*\(rewind to an earlier state and try a different forward move; trigger when the same error recurs three or more times\)\.Invariants\.\(I1\) The file type\-checks after every step\. \(I2\) EveryAdmittedis a deferred hole, not a permanent assumption: allAdmittedmust be closed before reporting*done*\. \(I3\) The specification is fixed\. \(I4\) NoAxiom,Hypothesis,Parameter, or unguarded recursion\.Design\.State types should be concrete \(records, bounded lists, indexed nats\), not function types whoseoverridebuilds closure chains under repeated update\. State must not grow unboundedly with the number of operations: traces, logs, and accumulated dependency lists belong in the proof context, not the runtime state\.Termination\.Report*done*when \(a\) the file type\-checks with zeroAdmittedand zeroadmit, and \(b\) the audit step passes \(no vacuous proofs; no specification edits; non\-trivial method bodies\)\. The coordinator additionally extracts the implementation and runs the benchmark harness; if extraction or execution fails, the run reverts\.Tactical playbook\.•Build simple to complex: prove small structural facts first, then combine\.•When stuck on a subgoal, read it carefully; the goal often names the missing helper\.•Useadmit\(lowercase\) to skip subgoals temporarily; the final file must have zeroAdmittedand zeroadmit\.

[appendix˜G](https://arxiv.org/html/2605.23109#A7)walks through an end\-to\-end illustration of this schema on a small target \(all\_less\_than\): each of the five synthesis steps is annotated with its move \(*Define*,*Prove*,*Decompose*\), with every intermediate listing type\-checking under the kernel\.

### F\.3Audit step

The audit step is a deterministic Python script that gates closure with kernel\-level verdicts \(no model outputs\)\. It encapsulates the cheating patterns we have observed during runs\.

Static checks\.

- •Admittedcount is zero\.
- •After stripping comments,Axiom,Hypothesis, andParametercounts are zero\.
- •make clean && makeexits zero\.

Vacuous\-proof patterns\.The script also matches the closed file against four patterns:

- •Aputthat returns a fixed constant the spec accepts on every input\.
- •An always\-truegetGuardthat admits any read\.
- •A forward\-simulation theorem stated over an empty domain so that it holds vacuously\.
- •A state\-only stub whoseUpdatedrops the payload and returns the initial state on every operation\.

A candidate that fails any check is sent to the ISA; only candidates passing all checks count as audit\-clean closures\.

### F\.4Proposer \(ISA tactical role\)

After the coordinator counts no progress across1010consecutive polls, the proposer fires as a one\-shot LLM session\. It receives the work file, everyAdmittedlemma’s surrounding1717\-line context, and the most recentmakeerror with44lines of trailing context when present, and writes its output toGUIDANCE\.mdin the workspace\.

Role\.You are an expert Rocq proof advisor\. Read the work file and focus on the proof goals and error context below\. Do NOT edit the\.vfile\.For each Admitted proof, follow this checklist:1\.Read the lemma statement\.What does it claim? What are the hypotheses? What is the conclusion type?2\.Identify the proof structure needed:forall x, P x→\\tointros x; inductive type \(list, trace, nat\)→\\toinductionon it; step/transition→\\todestructon the step type, then case analysis; simulation→\\toinvariant \+ induction on trace length; two functions equal→\\tofunctional\_extensionality\.3\.Identify missing helper lemmas\.For each subgoal you cannot close directly, state the EXACT helper \(name, signature, informal meaning\)\. Suggest: prove it separately;Admitit in the main proof; close it\.4\.If the proof is\>30\>30lines, decompose:by cases \(X\_case\_C1,X\_case\_C2, … for each constructor\); by subgoal \(ifA∧BA\\wedge B, proveAAandBBseparately\); extract common patterns repeating33\+ times\.5\.Suggest specific tactic sequences,not vague directions\.For compile errors,diagnose using a decision tree \(e\.g\.,*“Cannot unify X with Y”*→\\totype mismatch, useCheck expr\.;*“Tactic failure”*→\\totryliainstead ofomega;*“No matching clauses”*→\\toincomplete pattern match\)\.Output\.WriteGUIDANCE\.mdwith one section per Admitted proof or error: \(a\) the diagnosis, \(b\) the exact tactic sequence to try, \(c\) any helper\-lemma signatures\.

On Chapar, the proposer chose three sub\-lemma classes \(per\-message, per\-store\-entry, per\-replica\-clock\) by recognising that the global delivery invariant decomposes cleanly along these axes, none of which Rocq’s automation closes alone\.

### F\.5Reloader \(ISA strategic role\)

The reloader escalates every2020polling cycles when no progress is detected: Level11at stall cycle2020, Level22at4040, Level33at6060, and so on\. Each level is a one\-shot LLM session readingDESIGN\_LOG\.md,STATUS\.md, and every prior level’s output, and writesMETA\_GUIDANCE\_L\{N\}\.md\. The strategist consumes the output to rewrite its plan and spawn a fresh worker on the new design\.

Role\.You are a level\-NNformal verification architect\. ReadDESIGN\_LOG\.md,STATUS\.md, and every priorMETA\_GUIDANCE\_L\{1\.\.N\-1\}\.md: the history of all approaches tried and why each failed\.Synthesize a NEW approach that avoids ALL recorded failures\.Think across these dimensions:1\.Data representation\.Concrete types for state and messages: records, bounded lists, nats, not functions\.2\.Abstraction function\.How concrete state maps to abstract state\. This is the KEY creative choice; if previous attempts failed on the simulation proof, the abstraction was wrong\.3\.Invariant\.What property holds at every reachable state\. The invariant must be \(a\) true initially, \(b\) preserved by every step, \(c\) strong enough to prove the final theorem\.4\.Proof decomposition\.Which helper lemmas are needed, stated explicitly with signatures\.5\.Minimum information\.For each function that takes a collection, could the caller pass a smaller collection and still get a correct result? The most precise design passes only what is needed per call\.Output\.WriteMETA\_GUIDANCE\_L\{N\}\.mdas a CONCRETE blueprint a worker can directly implement: exactRecordtypes, method signatures, abstraction function, invariant, and lemma decomposition\. Do NOT write vague advice; do NOT spawn workers\.

On Chapar, the reloader chose a per\-key store entry recording sender, sender clock, and dependency vector; alternative layouts \(e\.g\. a single global per\-replica state\) leave the delivery lemma unprovable from local information\.

### F\.6Rocq feedback

Eachmakeinvocation captures stdout/stderr; on non\-zero exit, the coordinator extracts everyError:line plus22lines of preceding context and44lines of trailing context as a single error block\. The block is included verbatim in the worker’s next prompt alongside the proof goal, the local hypothesis context, and the tactic backtrace where applicable\. No normalisation or summarisation is applied: the structured Rocq diagnostic carries the localisation signal\. Replacing this stream with a binary accept/reject collapses the search \([section˜5\.4](https://arxiv.org/html/2605.23109#S5.SS4)reports≤1/3\\leq 1/3closure on every Rocq spec under−\-VF\)\.

### F\.7Performance feedback

When a worker reaches a verifier\-clean state with a design hash distinct from prior runs, the coordinator invokes the benchmark harness asynchronously\. The harness extracts the implementation to OCaml, deploys it on the cluster \([appendix˜D](https://arxiv.org/html/2605.23109#A4)\), and writes results toPERF\_RESULTS\.mdin the workspace\. Throughput targets are calibrated per\-spec from the published reference; implementations whose throughput falls below the target are flagged and trigger the reloader on the next escalation\.

## Appendix GSynthesis Progression:all\_less\_than

This appendix walks through one full progression of IDS’ deductive\-synthesis loop on a small target\. Step 0 and the Final State are complete Rocq files that compile; the listings for intermediate Steps 1–5 show only the parts that change from the previous step, with not\-yet\-filled bodies stubbed asParameter\. The progression on real distributed\-system specs follows the same pattern at much larger scale \([section˜5\.2](https://arxiv.org/html/2605.23109#S5.SS2)\); the small target keeps each listing short enough to read end\-to\-end\.

The five synthesis steps below are an instance of the deductive\-synthesis schema of[section˜F\.2](https://arxiv.org/html/2605.23109#A6.SS2)\. Step 1 is a*Decompose*\(split the goal into aniland aconshelper lemma\)\. Step 2 combines*Define*\(fill thenilbody\) with*Prove*\(close thenilhelper\)\. Step 3 is another*Decompose*\(split theconshelper on the head\)\. Step 4 is*Define*\(the recursive call\)\. Step 5 combines*Define*\(fill theelsebranch\) with*Prove*\(close theelsehelper\)\. The file type\-checks at every step \(Invariant I1\);Admittedplaceholders carry the deferred holes forward and are all discharged by the Final state\.

The target isall\_less\_than : list nat \-\> nat \-\> bool, returningtrueiff every element of the input list is strictly less than the boundn\. The correctness statement is the iff\-equivalence withForall:

> all\_less\_than l n = true⇔\\LeftrightarrowForall \(fun x =\> x < n\) l\.

### G\.1Step 0: bare specification

The implementation is aParameter; the correctness lemma isAdmitted\. The file type\-checks but proves nothing\.

1RequireImportCoq\.Lists\.List\.

2

3Parameterall\_less\_than:listnat\-\>nat\-\>bool\.

4

5Lemmaall\_less\_than\_correct:forall\(l:listnat\)\(n:nat\),

6all\_less\_thanln=true<\-\>Forall\(funx=\>x<n\)l\.

7Proof\.

8Admitted\.

Listing 1:Step 0: spec only\.
### G\.2Step 1: case\-split on the input list

The agent commits to recursing onl\. The implementation becomes aDefinitionwith amatchonnil/cons; the branch bodies are stubbed asParameters\. The correctness lemma is split into a\_nilhelper and a\_conshelper, bothAdmitted; the main lemma now closes byinductiononl, applying each helper at its leaf\.

1Parameternil\_body:bool\.

2Parametercons\_body:nat\-\>listnat\-\>bool\.

3

4Definitionall\_less\_than\(l:listnat\)\(n:nat\):bool:=

5matchlwith

6\|nil=\>nil\_body

7\|x::xs=\>cons\_bodyxxs

8end\.

9

10Lemmaall\_less\_than\_correct\_nil:forall\(n:nat\),

11all\_less\_thanniln=true<\-\>Forall\(funx=\>x<n\)nil\.

12Proof\.Admitted\.

13

14Lemmaall\_less\_than\_correct\_cons:

15forall\(x:nat\)\(xs:listnat\)\(n:nat\),

16all\_less\_than\(x::xs\)n=true<\-\>Forall\(funx=\>x<n\)\(x::xs\)\.

17Proof\.Admitted\.

18

19Lemmaall\_less\_than\_correct:forall\(l:listnat\)\(n:nat\),

20all\_less\_thanln=true<\-\>Forall\(funx=\>x<n\)l\.

21Proof\.

22introsln\.inductionlas\[\|xxsIH\]\.

23\-applyall\_less\_than\_correct\_nil\.

24\-applyall\_less\_than\_correct\_cons\.

25Qed\.

### G\.3Step 2: fill thenilbranch and close thenilhelper

The agent fillsnil\_bodywithtrue\(replacing theParameter\) and proves\_nil: both sides of the iff are vacuously satisfied \(true = true;Forall \_ nilholds by the empty constructor\)\. Theconsbody is still aParameter\.

1Definitionall\_less\_than\(l:listnat\)\(n:nat\):bool:=

2matchlwith

3\|nil=\>true

4\|x::xs=\>cons\_bodyxxs

5end\.

6

7Lemmaall\_less\_than\_correct\_nil:forall\(n:nat\),

8all\_less\_thanniln=true<\-\>Forall\(funx=\>x<n\)nil\.

9Proof\.intros\.simpl\.split;intros;constructor\.Qed\.

### G\.4Step 3: introduce theifbranch and split theconshelper

The agent commits to comparingxagainstnviax <? n, leaving both branches asParameterstubs\. The\_conshelper is split into a\_thensub\-helper \(underx < n\) and an\_elsesub\-helper \(under¬\\neg\(x < n\)\), and\_consnow proves itself by case\-splitting onNat\.ltb\_specand applying the appropriate sub\-helper\.

1Parameterthen\_bodyelse\_body:nat\-\>listnat\-\>nat\-\>bool\.

2

3Definitionall\_less\_than\(l:listnat\)\(n:nat\):bool:=

4matchlwith

5\|nil=\>true

6\|x::xs=\>ifx<?nthenthen\_bodyxxsnelseelse\_bodyxxsn

7end\.

8

9Lemmaall\_less\_than\_correct\_cons\_then:

10forall\(x:nat\)\(xs:listnat\)\(n:nat\),

11x<n\-\>\(all\_less\_thanxsn=true<\-\>Forall\(funx=\>x<n\)xs\)\-\>

12\(all\_less\_than\(x::xs\)n=true<\-\>Forall\(funx=\>x<n\)\(x::xs\)\)\.

13Proof\.Admitted\.

14

15Lemmaall\_less\_than\_correct\_cons\_else:

16forall\(x:nat\)\(xs:listnat\)\(n:nat\),

17~\(x<n\)\-\>\(all\_less\_thanxsn=true<\-\>Forall\(funx=\>x<n\)xs\)\-\>

18\(all\_less\_than\(x::xs\)n=true<\-\>Forall\(funx=\>x<n\)\(x::xs\)\)\.

19Proof\.Admitted\.

20

21Lemmaall\_less\_than\_correct\_cons:

22forall\(x:nat\)\(xs:listnat\)\(n:nat\),

23all\_less\_thanxsn=true<\-\>Forall\(funx=\>x<n\)xs\-\>

24all\_less\_than\(x::xs\)n=true<\-\>Forall\(funx=\>x<n\)\(x::xs\)\.

25Proof\.

26intros\.destruct\(Nat\.ltb\_specxn\)as\[Hlt\|Hge\]\.

27\-applyall\_less\_than\_correct\_cons\_then;assumption\.

28\-applyall\_less\_than\_correct\_cons\_else;\[applyNat\.le\_ngt;assumption\|assumption\]\.

29Qed\.

### G\.5Step 4: fill thethenbranch with the recursive call

The agent fillsthen\_bodywithall\_less\_than xs n: the implementation now actually recurses, soDefinitionis promoted toFixpoint\. The\_thenhelper proves cleanly: underx < n, applyingNat\.ltb\_ltrewrites theif\-condition totrue, andForallonx :: xsreduces tox < non the head plusForallonxs, both available\.

1Fixpointall\_less\_than\(l:listnat\)\(n:nat\):bool:=

2matchlwith

3\|nil=\>true

4\|x::xs=\>ifx<?nthenall\_less\_thanxsnelseelse\_bodyxxsn

5end\.

6

7Lemmaall\_less\_than\_correct\_cons\_then:

8forall\(x:nat\)\(xs:listnat\)\(n:nat\),

9x<n\-\>\(all\_less\_thanxsn=true<\-\>Forall\(funx=\>x<n\)xs\)\-\>

10\(all\_less\_than\(x::xs\)n=true<\-\>Forall\(funx=\>x<n\)\(x::xs\)\)\.

11Proof\.

12introsxxsnHltH\_ind\.simpl\.

13applyNat\.ltb\_ltinHlt\.rewriteHlt\.

14split;intros\.

15\-constructor;\[applyNat\.ltb\_lt;assumption\|tauto\]\.

16\-inversionH\.tauto\.

17Qed\.

### G\.6Step 5: fill theelsebranch and close theelsehelper

The agent’s first attempt is to recurse:else\_body := all\_less\_than xs n\(“skip the out\-of\-bound element, keep checking”\)\. The implementation type\-checks, but the\_elseobligation does not: under¬\(x<n\)\\neg\(x<n\)the goal becomesall\_less\_than xs n = true⇔\\LeftrightarrowForall \(fun y =\> y < n\) \(x :: xs\), which fails onxs = nil,x = 5,n = 3\(LHS istrue; RHS demands5 < 3\)\. Rocq rejects the proof\. The agent backtracks and replaces theelsebody withfalse: the function now returns false on any out\-of\-bound element, the\_elsehelper closes \(LHS becomesfalse = true, closed bydiscriminate; RHS givesx < nfrom inversion ofForall, contradicting¬\(x<n\)\\neg\(x<n\)\)\.

1\(\*Attempt1:else\_body:=all\_less\_thanxsn\(rejected:ifffails\)\*\)

2\(\*Attempt2:else\_body:=false\(accepted\)\*\)

3

4Lemmaall\_less\_than\_correct\_cons\_else:

5forall\(x:nat\)\(xs:listnat\)\(n:nat\),

6~\(x<n\)\-\>\(all\_less\_thanxsn=true<\-\>Forall\(funx=\>x<n\)xs\)\-\>

7\(all\_less\_than\(x::xs\)n=true<\-\>Forall\(funx=\>x<n\)\(x::xs\)\)\.

8Proof\.

9introsxxsnHge\_\.simpl\.

10applyNat\.le\_ngtinHge\.applyNat\.ltb\_geinHge\.rewriteHge\.

11split\.

12\-discriminate\.

13\-introsHF\.inversionHF;subst\.

14applyNat\.ltb\_ltinH1\.congruence\.

15Qed\.

### G\.7Final state

After five steps everyParameterstub andAdmittedplaceholder is closed\. Rocq’s kernel accepts the file, verifyingall\_less\_than\_correcton every input\.

1RequireImportCoq\.Lists\.List\.

2RequireImportCoq\.Arith\.PeanoNat\.

3

4Fixpointall\_less\_than\(l:listnat\)\(n:nat\):bool:=

5matchlwith

6\|nil=\>true

7\|x::xs=\>ifx<?nthenall\_less\_thanxsnelsefalse

8end\.

9

10Lemmaall\_less\_than\_correct\_nil:forall\(n:nat\),

11all\_less\_thanniln=true<\-\>Forall\(funx=\>x<n\)nil\.

12Proof\.intros\.simpl\.split;intros;constructor\.Qed\.

13

14Lemmaall\_less\_than\_correct\_cons\_then:

15forall\(x:nat\)\(xs:listnat\)\(n:nat\),

16x<n\-\>\(all\_less\_thanxsn=true<\-\>Forall\(funx=\>x<n\)xs\)\-\>

17\(all\_less\_than\(x::xs\)n=true<\-\>Forall\(funx=\>x<n\)\(x::xs\)\)\.

18Proof\.

19introsxxsnHltH\_ind\.simpl\.

20applyNat\.ltb\_ltinHlt\.rewriteHlt\.

21split;intros\.

22\-constructor;\[applyNat\.ltb\_lt;assumption\|tauto\]\.

23\-inversionH\.tauto\.

24Qed\.

25

26Lemmaall\_less\_than\_correct\_cons\_else:

27forall\(x:nat\)\(xs:listnat\)\(n:nat\),

28~\(x<n\)\-\>\(all\_less\_thanxsn=true<\-\>Forall\(funx=\>x<n\)xs\)\-\>

29\(all\_less\_than\(x::xs\)n=true<\-\>Forall\(funx=\>x<n\)\(x::xs\)\)\.

30Proof\.

31introsxxsnHge\_\.simpl\.

32applyNat\.le\_ngtinHge\.applyNat\.ltb\_geinHge\.rewriteHge\.

33split\.

34\-discriminate\.

35\-introsHF\.inversionHF;subst\.

36applyNat\.ltb\_ltinH1\.congruence\.

37Qed\.

38

39Lemmaall\_less\_than\_correct\_cons:

40forall\(x:nat\)\(xs:listnat\)\(n:nat\),

41all\_less\_thanxsn=true<\-\>Forall\(funx=\>x<n\)xs\-\>

42all\_less\_than\(x::xs\)n=true<\-\>Forall\(funx=\>x<n\)\(x::xs\)\.

43Proof\.

44intros\.destruct\(Nat\.ltb\_specxn\)as\[Hlt\|Hge\]\.

45\-applyall\_less\_than\_correct\_cons\_then;assumption\.

46\-applyall\_less\_than\_correct\_cons\_else;\[applyNat\.le\_ngt;assumption\|assumption\]\.

47Qed\.

48

49Lemmaall\_less\_than\_correct:forall\(l:listnat\)\(n:nat\),

50all\_less\_thanln=true<\-\>Forall\(funx=\>x<n\)l\.

51Proof\.

52introsln\.inductionlas\[\|xxsIH\]\.

53\-applyall\_less\_than\_correct\_nil\.

54\-applyall\_less\_than\_correct\_cons\.assumption\.

55Qed\.

Listing 2:Step 5 \(final\): implementation and proof, fully verified\.The progression on real distributed\-system specs follows the same pattern at much larger scale: dozens of helper lemmas, hundreds of lines of implementation, and tactics that range over inductive simulation arguments rather than single\-step rewrites\.[section˜4](https://arxiv.org/html/2605.23109#S4)describes how IDS drives this process; the case\-study trajectory in[section˜5](https://arxiv.org/html/2605.23109#S5)shows it on the causal\-consistency specification\.

## Appendix HLimitations, Broader Impacts, and Ethics

The main paper presents IDS’ design and evaluation; this appendix addresses the limitations of the work, the broader impacts of verified\-synthesis tooling, and ethical considerations\.

#### Limitations\.

IDS requires a formal RocqModule Typeas input; we do not synthesize specifications from natural language\. Compute cost is22–1111hours and $52–$155 per closed spec, substantially below the months\-to\-years of expert proof effort it replaces but still meaningful\. We evaluate on distributed key\-value\-store consistency; generality to other verified\-synthesis domains \(compilers, OS kernels, cryptographic protocols\) is conjectured, not measured\.

#### Broader impacts\.

Distributed systems are common in production software \(databases, message queues, cloud services\), but formal verification of these systems has remained out of reach for most production code because hand\-written proofs take person\-years of expert effort\. IDS reduces that effort to hours of compute, putting verified distributed software within reach of production teams\. Kernel\-checked proofs make IDS’ outputs safer than unverified LLM\-generated code: the verifier rules out silent bugs against the specification\. As with all formal verification, mis\-specification remains a residual risk\.

#### Ethics\.

The work involves no human subjects and no scraped data; the verified outputs introduce no dual\-use risks beyond those already present in unverified LLM code generation\.

## Appendix IIDS Suite

IDS suite is the benchmark dataset of six distributed key\-value\-store specifications we release alongside the system; together with Chapar’s published causal\-consistency specLesaniet al\.\([2016](https://arxiv.org/html/2605.23109#bib.bib6)\), they form the seven specifications evaluated in[section˜5](https://arxiv.org/html/2605.23109#S5)\. Each specification fixes \(i\) the abstract spec state and operations the application sees, \(ii\) the concrete replica state and operations the implementation runs, and \(iii\) the consistency property the implementation must satisfy\. This appendix gives the formal definition of every spec, plus the reference implementations we benchmark in[section˜5](https://arxiv.org/html/2605.23109#S5)\. The framework setup below introduces the notation: client programs \([fig\.˜10](https://arxiv.org/html/2605.23109#A9.F10)\), the seven\-methodAlgDefinterface \([fig\.˜11](https://arxiv.org/html/2605.23109#A9.F11)\), the configuration syntax \([fig\.˜12](https://arxiv.org/html/2605.23109#A9.F12)\), the concurrent operational semantics \([fig\.˜13](https://arxiv.org/html/2605.23109#A9.F13)\), the refinement hierarchy \([fig\.˜14](https://arxiv.org/html/2605.23109#A9.F14)\), and a relaxed baseline spec \([fig\.˜15](https://arxiv.org/html/2605.23109#A9.F15)\)\.

#### Summary\.

[Table˜8](https://arxiv.org/html/2605.23109#A9.T8)lists the six IDS suite specifications plus Chapar’s published CC\. Each is then introduced in plain English and immediately followed by its formal definition and reference implementation\.

Table 8:The six IDS suite specifications, plus Chapar’s published CC for reference\.k:KKeyv:V⊇KValuex:VVariableiUnique Identifierss:S::=𝑝𝑢𝑡i​\(k,v\);sStatement\|x←𝑔𝑒𝑡i​\(k\);s\|𝑠𝑘𝑖𝑝\|Extended Syntax for Internal Statements\|⊘x←𝑔𝑒𝑡i\(k\);sBlocked Getc:CClientsa:A=C↦SApplication\\displaystyle\\begin\{array\}\[\]\{rcl@\{\\qquad\}l\}k&:&K&\\mbox\{Key\}\\\\ v&:&V\\supseteq K&\\mbox\{Value\}\\\\ x&:&V&\\mbox\{Variable\}\\\\ i&&\\penalty 50\\qquad&\\mbox\{Unique Identifiers\}\\\\ s:S&::=&\\mathit\{put\}^\{i\}\(\{k\},\{v\}\);\\ s&\\mbox\{Statement\}\\\\ &\|&x\\leftarrow\\mathit\{get\}^\{i\}\(\{k\}\);\\ s&\\\\ &\|&\\mathit\{skip\}&\\\\ &\|&&\\mbox\{Extended Syntax for Internal Statements\}\\\\ &\|&\\oslash\\,x\\leftarrow\\mathit\{get\}^\{i\}\(\{k\}\);\\ s&\\mbox\{Blocked Get\}\\\\ c&:&C&\\mbox\{Clients\}\\\\ a&:&A=C\\mapsto S&\\mbox\{Application\}\\end\{array\}

Figure 10:Client Programs𝕀=\(𝖢𝖲𝗍𝖺𝗍𝖾,𝖼\-𝗂𝗇𝗂𝗍,𝖱𝖲𝗍𝖺𝗍𝖾,𝗋\-𝗂𝗇𝗂𝗍,Implementation𝗀𝖾𝗍​\-​𝗋𝖾𝗊,𝗀𝖾𝗍​\-​𝗀𝗎𝖺𝗋𝖽,𝗀𝖾𝗍,𝗀𝖾𝗍​\-​𝗋𝖾𝗌,𝗉𝗎𝗍\-𝗋𝖾𝗊,𝗉𝗎𝗍\-𝗀𝗎𝖺𝗋𝖽,𝗉𝗎𝗍\)CClients𝖢𝖲𝗍𝖺𝗍𝖾:𝖳𝗒𝗉𝖾Client State𝖼​\-​𝗂𝗇𝗂𝗍:C→𝖢𝖲𝗍𝖺𝗍𝖾Client Initial StateRReplicas𝖱𝖲𝗍𝖺𝗍𝖾:𝖳𝗒𝗉𝖾Replica State𝗋​\-​𝗂𝗇𝗂𝗍:R→V→𝖱𝖲𝗍𝖺𝗍𝖾Replica Initial State𝖦𝖾𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽,𝖦𝖾𝗍​\-​𝗋𝖾𝗌​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽:𝖳𝗒𝗉𝖾Get Payload Types𝗀𝖾𝗍​\-​𝗋𝖾𝗊:\(K\)​\(C,𝖢𝖲𝗍𝖺𝗍𝖾\)→\(𝖦𝖾𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽,𝖢𝖲𝗍𝖺𝗍𝖾\)Get Request \(at client\)𝗀𝖾𝗍​\-​𝗀𝗎𝖺𝗋𝖽:\(K\)​\(𝖦𝖾𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽\)​\(C,R,𝖱𝖲𝗍𝖺𝗍𝖾\)→𝖡𝗈𝗈𝗅Get Guard \(at replica\)𝗀𝖾𝗍:\(K\)​\(𝖦𝖾𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽\)​\(C,R,𝖱𝖲𝗍𝖺𝗍𝖾\)→\(V×𝖦𝖾𝗍​\-​𝗋𝖾𝗌​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽,𝖱𝖲𝗍𝖺𝗍𝖾\)Get \(at replica\)𝗀𝖾𝗍​\-​𝗋𝖾𝗌:\(K,V\)​\(𝖦𝖾𝗍​\-​𝗋𝖾𝗌​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽\)​\(C,𝖢𝖲𝗍𝖺𝗍𝖾\)→𝖢𝖲𝗍𝖺𝗍𝖾Get Response \(at client\)𝖯𝗎𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽:𝖳𝗒𝗉𝖾Put Payload Type𝗉𝗎𝗍​\-​𝗋𝖾𝗊:\(K,V\)​\(C,𝖢𝖲𝗍𝖺𝗍𝖾\)→\(𝖯𝗎𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽×𝖢𝖲𝗍𝖺𝗍𝖾\)Put Request \(at client\)𝗉𝗎𝗍​\-​𝗀𝗎𝖺𝗋𝖽:\(K,V\)​\(𝖯𝗎𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽\)​\(C,R,𝖱𝖲𝗍𝖺𝗍𝖾\)→𝖡𝗈𝗈𝗅Put Guard \(at replica\)𝗉𝗎𝗍:\(K,V\)​\(𝖯𝗎𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽\)​\(C,R,𝖱𝖲𝗍𝖺𝗍𝖾\)→𝖱𝖲𝗍𝖺𝗍𝖾Put \(at replica\)\\displaystyle\\begin\{array\}\[\]\{lr\}\\mathbb\{I\}=\(\\mathsf\{CState\},\\mathsf\{c\\text\{\-\}init\},\\mathsf\{RState\},\\mathsf\{r\\text\{\-\}init\},&\\text\{\\small Implementation\}\\\\ \\phantom\{\\mathbb\{I\}=\(\}\\mathsf\{get\\text\{\-\}req\},\\mathsf\{get\\text\{\-\}guard\},\\mathsf\{get\},\\mathsf\{get\\text\{\-\}res\},\\\\ \\phantom\{\\mathbb\{I\}=\(\}\\mathsf\{put\\text\{\-\}req\},\\mathsf\{put\\text\{\-\}guard\},\\mathsf\{put\}\)\\penalty 50\\qquad\\\\ C&\\text\{\\small Clients\}\\\\ \\mathsf\{CState\}:\\mathsf\{Type\}&\\text\{\\small Client State\}\\\\ \\mathsf\{c\\text\{\-\}init\}:C\\rightarrow\\mathsf\{CState\}&\\text\{\\small Client Initial State\}\\\\ R&\\text\{\\small Replicas\}\\\\ \\mathsf\{RState\}:\\mathsf\{Type\}&\\text\{\\small Replica State\}\\\\ \\mathsf\{r\\text\{\-\}init\}:R\\rightarrow V\\rightarrow\\mathsf\{RState\}&\\text\{\\small Replica Initial State\}\\\\ \\mathsf\{Get\\text\{\-\}req\\text\{\-\}payload\},\\mathsf\{Get\\text\{\-\}res\\text\{\-\}payload\}:\\mathsf\{Type\}&\\text\{\\small Get Payload Types\}\\\\ \\mathsf\{get\\text\{\-\}req\}:\(K\)\(C,\\mathsf\{CState\}\)\\rightarrow\(\\mathsf\{Get\\text\{\-\}req\\text\{\-\}payload\},\\mathsf\{CState\}\)&\\text\{\\small Get Request \(at client\)\}\\\\ \\mathsf\{get\\text\{\-\}guard\}:\(K\)\(\\mathsf\{Get\\text\{\-\}req\\text\{\-\}payload\}\)\(C,R,\\mathsf\{RState\}\)\\rightarrow\\mathsf\{Bool\}&\\text\{\\small Get Guard \(at replica\)\}\\\\ \\mathsf\{get\}:\(K\)\(\\mathsf\{Get\\text\{\-\}req\\text\{\-\}payload\}\)\(C,R,\\mathsf\{RState\}\)\\rightarrow\(V\\times\\mathsf\{Get\\text\{\-\}res\\text\{\-\}payload\},\\mathsf\{RState\}\)&\\text\{\\small Get \(at replica\)\}\\\\ \\mathsf\{get\\text\{\-\}res\}:\(K,V\)\(\\mathsf\{Get\\text\{\-\}res\\text\{\-\}payload\}\)\(C,\\mathsf\{CState\}\)\\rightarrow\\mathsf\{CState\}&\\text\{\\small Get Response \(at client\)\}\\\\ \\mathsf\{Put\\text\{\-\}req\\text\{\-\}payload\}:\\mathsf\{Type\}&\\text\{\\small Put Payload Type\}\\\\ \\mathsf\{put\\text\{\-\}req\}:\(K,V\)\(C,\\mathsf\{CState\}\)\\rightarrow\(\\mathsf\{Put\\text\{\-\}req\\text\{\-\}payload\}\\times\\mathsf\{CState\}\)&\\text\{\\small Put Request \(at client\)\}\\\\ \\mathsf\{put\\text\{\-\}guard\}:\(K,V\)\(\\mathsf\{Put\\text\{\-\}req\\text\{\-\}payload\}\)\(C,R,\\mathsf\{RState\}\)\\rightarrow\\mathsf\{Bool\}&\\text\{\\small Put Guard \(at replica\)\}\\\\ \\mathsf\{put\}:\(K,V\)\(\\mathsf\{Put\\text\{\-\}req\\text\{\-\}payload\}\)\(C,R,\\mathsf\{RState\}\)\\rightarrow\\mathsf\{RState\}&\\text\{\\small Put \(at replica\)\}\\end\{array\}

Figure 11:Key\-Value Store Implementation Interface𝕀=\(𝖢𝖲𝗍𝖺𝗍𝖾,𝖼\-𝗂𝗇𝗂𝗍,𝖱𝖲𝗍𝖺𝗍𝖾,𝗋\-𝗂𝗇𝗂𝗍,Implementation𝗀𝖾𝗍​\-​𝗋𝖾𝗊,𝗀𝖾𝗍​\-​𝗀𝗎𝖺𝗋𝖽,𝗀𝖾𝗍,𝗀𝖾𝗍​\-​𝗋𝖾𝗌,𝗉𝗎𝗍\-𝗋𝖾𝗊,𝗉𝗎𝗍\-𝗀𝗎𝖺𝗋𝖽,𝗉𝗎𝗍\)W:𝒲≔⟨𝒞,ℛ,𝒩⟩Worldc:CClientsσ:𝖢𝖲𝗍𝖺𝗍𝖾Client State𝒞:C↦⟨𝖢𝖲𝗍𝖺𝗍𝖾,S⟩Client Programsr:RReplicasς:𝖱𝖲𝗍𝖺𝗍𝖾Replica Stateℛ:R↦𝖱𝖲𝗍𝖺𝗍𝖾Replica States𝒩:ℙ​𝕄​\(M\)NetworkM:C×R×𝐺𝑒𝑡​\-​𝑟𝑒𝑞​\(I,K,𝖦𝖾𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽\)Message\|R×C×𝐺𝑒𝑡​\-​𝑟𝑒𝑠​\(I,K,V,𝖦𝖾𝗍​\-​𝗋𝖾𝗌​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽\)\|C×R×𝑃𝑢𝑡​\-​𝑟𝑒𝑞​\(K,V,𝖯𝗎𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽\)l::=c⊳𝑔𝑒𝑡i​\(k\)Label\|r⊳𝑔𝑒𝑡i​\(k\):v\|c⊳𝑔𝑒𝑡i​\(k\):v\|c⊳𝑝𝑢𝑡​\(k,v\)\|r⊳𝑝𝑢𝑡​\(k,v\)h::=l​̵⃰History𝖾𝗑𝗍​\(h\)::=h\|\{c⊳𝑔𝑒𝑡i​\(k\):v,c⊳𝑝𝑢𝑡​\(k,v\)\}External History\\begin\{array\}\[\]\{rcl@\{\\qquad\}l\}\\mathbb\{I\}&=&\(\\mathsf\{CState\},\\mathsf\{c\\text\{\-\}init\},\\mathsf\{RState\},\\mathsf\{r\\text\{\-\}init\},&\\text\{\\small Implementation\}\\\\ &&\\phantom\{\(\}\\mathsf\{get\\text\{\-\}req\},\\mathsf\{get\\text\{\-\}guard\},\\mathsf\{get\},\\mathsf\{get\\text\{\-\}res\},\\\\ &&\\phantom\{\(\}\\mathsf\{put\\text\{\-\}req\},\\mathsf\{put\\text\{\-\}guard\},\\mathsf\{put\}\)\\\\ W:\\mathcal\{W\}&\\coloneqq&\\langle\\mathcal\{C\},\\mathcal\{R\},\\mathcal\{N\}\\rangle&\\mbox\{World\}\\\\ c&:&C&\\mbox\{Clients\}\\\\ \\sigma&:&\\mathsf\{CState\}&\\mbox\{Client State\}\\\\ \\mathcal\{C\}&:&C\\mapsto\\langle\\mathsf\{CState\},S\\rangle&\\mbox\{Client Programs\}\\\\ r&:&R&\\mbox\{Replicas\}\\\\ \\varsigma&:&\\mathsf\{RState\}&\\mbox\{Replica State\}\\\\ \\mathcal\{R\}&:&R\\mapsto\\mathsf\{RState\}&\\mbox\{Replica States\}\\\\ \\mathcal\{N\}&:&\\mathbb\{PM\}\(M\)&\\mbox\{Network\}\\\\ M&:&C\\times R\\times\\mathit\{Get\\text\{\-\}req\}\(I,K,\\mathsf\{Get\\text\{\-\}req\\text\{\-\}payload\}\)&\\mbox\{Message\}\\\\ &\|&R\\times C\\times\\mathit\{Get\\text\{\-\}res\}\(I,K,V,\\mathsf\{Get\\text\{\-\}res\\text\{\-\}payload\}\)\\\\ &\|&C\\times R\\times\\mathit\{Put\\text\{\-\}req\}\(K,V,\\mathsf\{Put\\text\{\-\}req\\text\{\-\}payload\}\)\\\\ l&::=&c\\triangleright\\mathit\{get\}^\{i\}\(\{k\}\)&\\mbox\{Label\}\\\\ &\|&r\\triangleright\\mathit\{get\}^\{i\}\(\{k\}\):v\\\\ &\|&c\\triangleright\\mathit\{get\}^\{i\}\(\{k\}\):v\\\\ &\|&c\\triangleright\\mathit\{put\}\(\{k\},\{v\}\)\\\\ &\|&r\\triangleright\\mathit\{put\}\(\{k\},\{v\}\)&\\\\ h&::=&l ⃰&\\mbox\{History\}\\\\ \\mathsf\{ext\}\(h\)&::=&h\\ \|\\ \\\{c\\triangleright\\mathit\{get\}^\{i\}\(\{k\}\):v,\\ c\\triangleright\\mathit\{put\}\(\{k\},\{v\}\)\\\}&\\mbox\{External History\}\\end\{array\}∘:𝖴𝗇𝗂𝗍ℙ​𝕄​\(S\)≜The multiset powerset of the setSW0​\(a\)𝕀≜⟨\[c↦⟨𝖼​\-​𝗂𝗇𝗂𝗍​\(c\),a​\(c\)⟩¯c∈C\],\[r↦𝗋​\-​𝗂𝗇𝗂𝗍​\(r,v0\)¯r∈R\],∅⟩v0≜The initial value\\begin\{array\}\[\]\{rcl\}\\circ&:&\\mathsf\{Unit\}\\\\ \\mathbb\{PM\}\(S\)&\\triangleq&\\mbox\{The multiset powerset of the set $S$\}\\\\ W\_\{0\}\(a\)\_\{\\mathbb\{I\}\}&\\triangleq&\\langle\[\\overline\{c\\mapsto\\langle\\mathsf\{c\\text\{\-\}init\}\(c\),a\(c\)\\rangle\}\_\{c\\in C\}\],\[\\overline\{r\\mapsto\\mathsf\{r\\text\{\-\}init\}\(r,v\_\{0\}\)\}\_\{r\\in R\}\],\\emptyset\\rangle\\\\ v\_\{0\}&\\triangleq&\\mbox\{The initial value\}\\end\{array\}

Figure 12:The State of the Key\-value Store Operational SemanticsGet\-Req≠cc0↝⁢get\-req\(k\)\(c,σ\)⁢̵⃰⟨p,σ′⟩⊳c⁢geti\(k\)→I\(C\[↦c⟨←σ,x⁢geti\(k\);s⟩\],R,N\)\(C\[↦c⟨σ′,⊘x←geti\(k\);s⟩\],R,N∪\{¯⟨c,r,⁢Get\-req\(i,k,p\)⟩∈rR\}\)\\displaystyle\\displaystyle\{\\hbox\{\\hskip 62\.32059pt\\vbox\{\\hbox\{\\thinspace\\hbox\{\\hbox\{$\\displaystyle\\displaystyle\{c\\neq c\_\{0\}\}$\}\}\}\\vbox\{\\hbox\{\\thinspace\\hbox\{\\hbox\{$\\displaystyle\\displaystyle\{\\mathsf\{get\\text\{\-\}req\}\(k\)\(c,\\sigma\)\\rightsquigarrow ⃰\\langle p,\\sigma^\{\\prime\}\\rangle\}$\}\}\}\\vbox\{\}\}\}\}\\over\\hbox\{\\hskip 137\.7117pt\\vbox\{\\vbox\{\}\\hbox\{\\thinspace\\hbox\{\\hbox\{$\\displaystyle\\displaystyle\{\{\\begin\{array\}\[\]\{l\}\(\\mathcal\{C\}\[c\\mapsto\\langle\\sigma,x\\leftarrow\\mathit\{get\}^\{i\}\(\{k\}\);s\\rangle\],\\\\ \\phantom\{\(\}\\mathcal\{R\},\\\\ \\phantom\{\(\}\\mathcal\{N\}\)\\end\{array\}\}\\xrightarrow\{c\\ \\triangleright\\ \\mathit\{get\}^\{i\}\(\{k\}\)\}\_\{\\mathbb\{I\}\}\{\\begin\{array\}\[\]\{l\}\(\\mathcal\{C\}\[c\\mapsto\\langle\\sigma^\{\\prime\},\\oslash\\,x\\leftarrow\\mathit\{get\}^\{i\}\(\{k\}\);s\\rangle\],\\\\ \\phantom\{\(\}\\mathcal\{R\},\\\\ \\phantom\{\(\}\\mathcal\{N\}\\cup\\\{\\overline\{\\langle c,r,\\mathit\{Get\\text\{\-\}req\}\(i,k,p\)\\rangle\}\_\{r\\in R\}\\\}\)\\end\{array\}\}\}$\}\}\}\}\}\}Get↝⁢get\-guard\(k\)\(p\)\(c,r,ς\)⁢̵⃰true↝⁢get\(k\)\(p\)\(c,r,ς\)⁢̵⃰⟨v,p′,ς′⟩:⊳r⁢geti\(k\)v→I\(C,⁢R\[↦rς\],N∪\{⟨c,r,⁢Get\-req\(i,k,p\)⟩\}\)\(C,⁢R\[↦rς′\],N∪\{⟨r,c,⁢Get\-res\(i,k,v,p′\)⟩\}\)\\displaystyle\\displaystyle\{\\hbox\{\\hskip 72\.5793pt\\vbox\{\\hbox\{\\thinspace\\hbox\{\\hbox\{$\\displaystyle\\displaystyle\{\\mathsf\{get\\text\{\-\}guard\}\(k\)\(p\)\(c,r,\\varsigma\)\\rightsquigarrow ⃰\\mathsf\{true\}\}$\}\}\}\\vbox\{\\hbox\{\\thinspace\\hbox\{\\hbox\{$\\displaystyle\\displaystyle\{\\mathsf\{get\}\(k\)\(p\)\(c,r,\\varsigma\)\\rightsquigarrow ⃰\\langle v,p^\{\\prime\},\\varsigma^\{\\prime\}\\rangle\}$\}\}\}\\vbox\{\}\}\}\}\\over\\hbox\{\\hskip 157\.26622pt\\vbox\{\\vbox\{\}\\hbox\{\\thinspace\\hbox\{\\hbox\{$\\displaystyle\\displaystyle\{\{\\begin\{array\}\[\]\{l\}\(\\mathcal\{C\},\\\\ \\phantom\{\(\}\\mathcal\{R\}\[r\\mapsto\\varsigma\],\\\\ \\phantom\{\(\}\\mathcal\{N\}\\cup\\\{\\langle c,r,\\mathit\{Get\\text\{\-\}req\}\(i,k,p\)\\rangle\\\}\)\\end\{array\}\}\\xrightarrow\{r\\ \\triangleright\\ \\mathit\{get\}^\{i\}\(\{k\}\):v\}\_\{\\mathbb\{I\}\}\{\\begin\{array\}\[\]\{l\}\(\\mathcal\{C\},\\\\ \\phantom\{\(\}\\mathcal\{R\}\[r\\mapsto\\varsigma^\{\\prime\}\],\\\\ \\phantom\{\(\}\\mathcal\{N\}\\cup\\\{\\langle r,c,\\mathit\{Get\\text\{\-\}res\}\(i,k,v,p^\{\\prime\}\)\\rangle\\\}\)\\end\{array\}\}\}$\}\}\}\}\}\}Get\-Res↝⁢get\-res\(k,v\)\(p\)\(c,σ\)⁢̵⃰σ′:⊳c⁢geti\(k\)v→I\(C\[↦c⟨σ,⊘x←geti\(k\);s⟩\],R,N∪\{⟨r,c,⁢Get\-res\(i,k,v,p\)⟩\}\)\(C\[↦c⟨σ′,⁢s\[/vx\]⟩\],R,N\)\\displaystyle\\displaystyle\{\\hbox\{\\hskip 64\.25691pt\\vbox\{\\hbox\{\\thinspace\\hbox\{\\hbox\{$\\displaystyle\\displaystyle\{\\mathsf\{get\\text\{\-\}res\}\(k,v\)\(p\)\(c,\\sigma\)\\rightsquigarrow ⃰\\sigma^\{\\prime\}\}$\}\}\}\\vbox\{\}\}\}\\over\\hbox\{\\hskip 135\.58083pt\\vbox\{\\vbox\{\}\\hbox\{\\thinspace\\hbox\{\\hbox\{$\\displaystyle\\displaystyle\{\{\\begin\{array\}\[\]\{l\}\(\\mathcal\{C\}\[c\\mapsto\\langle\\sigma,\\oslash\\,x\\leftarrow\\mathit\{get\}^\{i\}\(\{k\}\);s\\rangle\],\\\\ \\phantom\{\(\}\\mathcal\{R\},\\\\ \\phantom\{\(\}\\mathcal\{N\}\\cup\\\{\\langle r,c,\\mathit\{Get\\text\{\-\}res\}\(i,k,v,p\)\\rangle\\\}\)\\end\{array\}\}\\xrightarrow\{c\\ \\triangleright\\ \\mathit\{get\}^\{i\}\(\{k\}\):v\}\_\{\\mathbb\{I\}\}\{\\begin\{array\}\[\]\{l\}\(\\mathcal\{C\}\[c\\mapsto\\langle\\sigma^\{\\prime\},s\[v/x\]\\rangle\],\\\\ \\phantom\{\(\}\\mathcal\{R\},\\\\ \\phantom\{\(\}\\mathcal\{N\}\)\\end\{array\}\}\}$\}\}\}\}\}\}Put\-Req≠cc0↝⁢put\-req\(k,v\)\(c,σ\)⁢̵⃰⟨p,σ′⟩⊳c⁢put\(k,v\)→I\(C\[↦c\(σ,⁢put\(k,v\);s\)\],R,N\)\(C\[↦c\(σ′,s\)\],R,N∪\{¯⟨c,r,⁢Put\-req\(k,v,p\)⟩∈rR\}\)\\displaystyle\\displaystyle\{\\hbox\{\\hskip 67\.59024pt\\vbox\{\\hbox\{\\thinspace\\hbox\{\\hbox\{$\\displaystyle\\displaystyle\{c\\neq c\_\{0\}\}$\}\}\}\\vbox\{\\hbox\{\\thinspace\\hbox\{\\hbox\{$\\displaystyle\\displaystyle\{\\mathsf\{put\\text\{\-\}req\}\(k,v\)\(c,\\sigma\)\\rightsquigarrow ⃰\\langle p,\\sigma^\{\\prime\}\\rangle\}$\}\}\}\\vbox\{\}\}\}\}\\over\\hbox\{\\hskip 107\.163pt\\vbox\{\\vbox\{\}\\hbox\{\\thinspace\\hbox\{\\hbox\{$\\displaystyle\\displaystyle\{\{\\begin\{array\}\[\]\{l\}\(\\mathcal\{C\}\[c\\mapsto\(\\sigma,\\mathit\{put\}\(\{k\},\{v\}\);s\)\],\\\\ \\phantom\{\(\}\\mathcal\{R\},\\\\ \\phantom\{\(\}\\mathcal\{N\}\)\\end\{array\}\}\\xrightarrow\{c\\ \\triangleright\\ \\mathit\{put\}\(\{k\},\{v\}\)\}\_\{\\mathbb\{I\}\}\{\\begin\{array\}\[\]\{l\}\(\\mathcal\{C\}\[c\\mapsto\(\\sigma^\{\\prime\},s\)\],\\\\ \\phantom\{\(\}\\mathcal\{R\},\\\\ \\phantom\{\(\}\\mathcal\{N\}\\cup\\\{\\overline\{\\langle c,r,\\mathit\{Put\\text\{\-\}req\}\(k,v,p\)\\rangle\}\_\{r\\in R\}\\\}\)\\end\{array\}\}\}$\}\}\}\}\}\}Put↝⁢put\-guard\(k,v\)\(p\)\(c,r,ς\)⁢̵⃰true↝⁢put\(k,v\)\(p\)\(c,r,ς\)⁢̵⃰ς′⊳r⁢put\(k,v\)→I\(C,⁢R\[↦rς\],N∪\{⟨c,r,⁢Put\-req\(k,v,p\)⟩\}\)\(C,⁢R\[↦rς′\],N\)\\displaystyle\\displaystyle\{\\hbox\{\\hskip 77\.84895pt\\vbox\{\\hbox\{\\thinspace\\hbox\{\\hbox\{$\\displaystyle\\displaystyle\{\\mathsf\{put\\text\{\-\}guard\}\(k,v\)\(p\)\(c,r,\\varsigma\)\\rightsquigarrow ⃰\\mathsf\{true\}\}$\}\}\}\\vbox\{\\hbox\{\\thinspace\\hbox\{\\hbox\{$\\displaystyle\\displaystyle\{\\mathsf\{put\}\(k,v\)\(p\)\(c,r,\\varsigma\)\\rightsquigarrow ⃰\\varsigma^\{\\prime\}\}$\}\}\}\\vbox\{\}\}\}\}\\over\\hbox\{\\hskip 110\.43665pt\\vbox\{\\vbox\{\}\\hbox\{\\thinspace\\hbox\{\\hbox\{$\\displaystyle\\displaystyle\{\{\\begin\{array\}\[\]\{l\}\(\\mathcal\{C\},\\\\ \\phantom\{\(\}\\mathcal\{R\}\[r\\mapsto\\varsigma\],\\\\ \\phantom\{\(\}\\mathcal\{N\}\\cup\\\{\\langle c,r,\\mathit\{Put\\text\{\-\}req\}\(k,v,p\)\\rangle\\\}\)\\end\{array\}\}\\xrightarrow\{r\\ \\triangleright\\ \\mathit\{put\}\(\{k\},\{v\}\)\}\_\{\\mathbb\{I\}\}\{\\begin\{array\}\[\]\{l\}\(\\mathcal\{C\},\\\\ \\phantom\{\(\}\\mathcal\{R\}\[r\\mapsto\\varsigma^\{\\prime\}\],\\\\ \\phantom\{\(\}\\mathcal\{N\}\)\\end\{array\}\}\}$\}\}\}\}\}\}

Figure 13:Key\-value Store Operational Semantics→𝕀\\rightarrow\_\{\\mathbb\{I\}\}for the implementation𝕀=\\mathbb\{I\}=\(𝖢𝖲𝗍𝖺𝗍𝖾,\(\\mathsf\{CState\},𝖼​\-​𝗂𝗇𝗂𝗍,\\mathsf\{c\\text\{\-\}init\},𝖱𝖲𝗍𝖺𝗍𝖾,\\mathsf\{RState\},𝗋​\-​𝗂𝗇𝗂𝗍,\\mathsf\{r\\text\{\-\}init\},𝗀𝖾𝗍​\-​𝗋𝖾𝗊,\\mathsf\{get\\text\{\-\}req\},𝗀𝖾𝗍​\-​𝗀𝗎𝖺𝗋𝖽,\\mathsf\{get\\text\{\-\}guard\},𝗀𝖾𝗍,\\mathsf\{get\},𝗀𝖾𝗍​\-​𝗋𝖾𝗌,\\mathsf\{get\\text\{\-\}res\},𝗉𝗎𝗍​\-​𝗋𝖾𝗊,\\mathsf\{put\\text\{\-\}req\},𝗉𝗎𝗍​\-​𝗀𝗎𝖺𝗋𝖽,\\mathsf\{put\\text\{\-\}guard\},𝗉𝗎𝗍\)\\mathsf\{put\}\)\.The𝑔𝑒𝑡\\mathit\{get\}operations are synchronous\. Therefore, the semantics implicitly preserves the order of𝑔𝑒𝑡\\mathit\{get\}s and succeeding𝑔𝑒𝑡\\mathit\{get\}s and𝑝𝑢𝑡\\mathit\{put\}s\.

###### Definition 1\(Trace Inclusion\)\.

An implementation𝕀2\\mathbb\{I\}\_\{2\}trace\-includes another𝕀1\\mathbb\{I\}\_\{1\}, written𝕀2⊑𝕀1\\mathbb\{I\}\_\{2\}\\sqsubseteq\\mathbb\{I\}\_\{1\}, if for allW2W\_\{2\}, andh2h\_\{2\}, ifW0​\(a\)𝕀2→h2𝕀2̵⃰​W2W\_\{0\}\(a\)\_\{\\mathbb\{I\}\_\{2\}\}\\xrightarrow\{h\_\{2\}\}\_\{\\mathbb\{I\}\_\{2\}\} ⃰W\_\{2\}, then there existsh1h\_\{1\}andW1W\_\{1\}such thatW0​\(a\)𝕀1→h1𝕀1̵⃰​W1W\_\{0\}\(a\)\_\{\\mathbb\{I\}\_\{1\}\}\\xrightarrow\{h\_\{1\}\}\_\{\\mathbb\{I\}\_\{1\}\} ⃰W\_\{1\}and𝖾𝗑𝗍​\(h1\)=𝖾𝗑𝗍​\(h2\)\\mathsf\{ext\}\(h\_\{1\}\)=\\mathsf\{ext\}\(h\_\{2\}\)\.

###### Definition 2\(Convergence\)\.

An implementation𝕀\\mathbb\{I\}is convergent if for allℛ\\mathcal\{R\}, ifW0​\(a\)𝕀→𝕀̵⃰​⟨\_,ℛ,∅⟩W\_\{0\}\(a\)\_\{\\mathbb\{I\}\}\\xrightarrow\{\}\_\{\\mathbb\{I\}\} ⃰\\langle\\\_,\\mathcal\{R\},\\emptyset\\rangle, then for allkk,pp,cc,r1r\_\{1\},r2r\_\{2\}andvv, if𝗀𝖾𝗍​\-​𝗀𝗎𝖺𝗋𝖽​\(k\)​\(p\)​\(c,r1,ℛ​\[r1\]\)↝̵⃰​𝗍𝗋𝗎𝖾\\mathsf\{get\\text\{\-\}guard\}\(k\)\(p\)\(c,r\_\{1\},\\mathcal\{R\}\[r\_\{1\}\]\)\\rightsquigarrow ⃰\\mathsf\{true\}and𝗀𝖾𝗍​\(k\)​\(p\)​\(c,r1,ℛ​\[r1\]\)↝̵⃰​⟨v,\_,\_⟩\\mathsf\{get\}\(k\)\(p\)\(c,r\_\{1\},\\mathcal\{R\}\[r\_\{1\}\]\)\\rightsquigarrow ⃰\\langle v,\\\_,\\\_\\ranglethen𝗀𝖾𝗍​\-​𝗀𝗎𝖺𝗋𝖽​\(k\)​\(p\)​\(c,r2,ℛ​\[r2\]\)↝̵⃰​𝗍𝗋𝗎𝖾\\mathsf\{get\\text\{\-\}guard\}\(k\)\(p\)\(c,r\_\{2\},\\mathcal\{R\}\[r\_\{2\}\]\)\\rightsquigarrow ⃰\\mathsf\{true\}and𝗀𝖾𝗍​\(k\)​\(p\)​\(c,r2,ℛ​\[r2\]\)↝̵⃰​⟨v,\_,\_⟩\\mathsf\{get\}\(k\)\(p\)\(c,r\_\{2\},\\mathcal\{R\}\[r\_\{2\}\]\)\\rightsquigarrow ⃰\\langle v,\\\_,\\\_\\rangle\.

𝐈𝐶𝐶1\\mathbf\{I\}\_\{\\mathit\{CC\}\_\{1\}\}𝐈𝐶𝐶2\\mathbf\{I\}\_\{\\mathit\{CC\}\_\{2\}\}𝐈𝑅𝑌𝑊​\-​𝑀𝑊\\mathbf\{I\}\_\{\\mathit\{RYW\}\\text\{\-\}\\mathit\{MW\}\}𝐈𝐶𝐶∗\\mathbf\{I\}\_\{\\mathit\{CC\}\}^\{\*\}𝐈𝑅𝑌𝑊\\mathbf\{I\}\_\{\\mathit\{RYW\}\}𝐈𝑀𝑊\\mathbf\{I\}\_\{\\mathit\{MW\}\}𝐈𝑀𝑅\\mathbf\{I\}\_\{\\mathit\{MR\}\}𝐈𝐿𝐶𝐶∗\\mathbf\{I\}\_\{\\mathit\{LCC\}\}^\{\*\}𝐈𝑅𝑌𝑊∗\\mathbf\{I\}\_\{\\mathit\{RYW\}\}^\{\*\}𝐈𝑀𝑊∗\\mathbf\{I\}\_\{\\mathit\{MW\}\}^\{\*\}𝐈𝑀𝑅∗\\mathbf\{I\}\_\{\\mathit\{MR\}\}^\{\*\}𝐈Rel\\mathbf\{I\}\_\{\\mathrm\{Rel\}\}

Figure 14:Refinement Hierarchy𝕀𝑅𝑒𝑙​\(Relaxed Specification\)𝖢𝖲𝗍𝖺𝗍𝖾≔𝖴𝗇𝗂𝗍Client State𝖼​\-​𝗂𝗇𝗂𝗍​\(c\)≔⊥Client Initial State𝖱𝖲𝗍𝖺𝗍𝖾≔K↦VReplica State𝗋​\-​𝗂𝗇𝗂𝗍​\(r,v0\)≔\[k↦v0¯\]Replica Initial State𝖦𝖾𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔𝖦𝖾𝗍​\-​𝗋𝖾𝗌​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔𝖴𝗇𝗂𝗍Get payload types𝗀𝖾𝗍​\-​𝗋𝖾𝗊​\(\_\)​\(\_,σ\)≔At client:Get Request𝗋𝖾𝗍​⟨∘,p⟩No payload𝗀𝖾𝗍​\-​𝗀𝗎𝖺𝗋𝖽​\(\_\)​\(\_\)​\(\_,\_,\_\)≔At replica:Get Guard𝗋𝖾𝗍​𝗍𝗋𝗎𝖾𝗀𝖾𝗍​\(k\)​\(\_\)​\(\_,\_,ς\)≔At replica:Get𝗅𝖾𝗍​⟨v,\_⟩←ς​\(k\)𝗋𝖾𝗍​⟨v,∘,ς⟩No payload𝗀𝖾𝗍​\-​𝗋𝖾𝗌​\(\_,\_\)​\(\_\)​\(\_,σ\)≔At client:Get Response𝗋𝖾𝗍​σ𝖯𝗎𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔𝖴𝗇𝗂𝗍Put payload types𝗉𝗎𝗍​\-​𝗋𝖾𝗊​\(k,\_\)​\(\_,σ\)≔At client:Put Request𝗋𝖾𝗍​⟨∘,σ⟩No payload𝗉𝗎𝗍​\-​𝗀𝗎𝖺𝗋𝖽​\(\_,\_\)​\(\_\)​\(\_,\_,\_\)≔At replica:Put Guard𝗋𝖾𝗍​𝗍𝗋𝗎𝖾𝗉𝗎𝗍​\(k,v\)​\(\_\)​\(\_,\_,ς\)≔At replica:Put𝗋𝖾𝗍​ς​\[k↦v\]\\displaystyle\\begin\{array\}\[\]\{\|lr\|\}\\hline\\cr\\mathbb\{I\}\_\{\\mathit\{Rel\}\}\\ \(\\textsc\{Relaxed Specification\}\)&\\\\ \\hline\\cr\\mathsf\{CState\}\\coloneqq\\mathsf\{Unit\}&\\textbf\{\\small Client State\}\\\\ \\mathsf\{c\\text\{\-\}init\}\(c\)\\coloneqq\\bot&\\textbf\{\\small Client Initial State\}\\\\ \\mathsf\{RState\}\\coloneqq K\\mapsto V&\\textbf\{\\small Replica State\}\\\\ \\mathsf\{r\\text\{\-\}init\}\(r,v\_\{0\}\)\\coloneqq\[\\overline\{k\\mapsto v\_\{0\}\}\]&\\textbf\{\\small Replica Initial State\}\\\\ &\\\\ \\mathsf\{Get\\text\{\-\}req\\text\{\-\}payload\}\\coloneqq\\mathsf\{Get\\text\{\-\}res\\text\{\-\}payload\}\\coloneqq\\mathsf\{Unit\}&\\text\{\\small Get payload types\}\\\\ \\mathsf\{get\\text\{\-\}req\}\\ \(\\\_\)\(\\\_,\\sigma\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Get Request\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle\\circ,p\\rangle&\\text\{\\small No payload\}\\\\ \\mathsf\{get\\text\{\-\}guard\}\\ \(\\\_\)\(\\\_\)\(\\\_,\\\_,\\\_\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Get Guard\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\mathsf\{true\}&\\text\{\\small\}\\\\ \\mathsf\{get\}\\ \(k\)\(\\\_\)\(\\\_,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Get\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle v,\\\_\\rangle\\leftarrow\\varsigma\(k\)&\\text\{\\small\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle v,\\circ,\\varsigma\\rangle&\\text\{\\small No payload\}\\\\ \\mathsf\{get\\text\{\-\}res\}\\ \(\\\_,\\\_\)\(\\\_\)\(\\\_,\\sigma\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Get Response\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\sigma&\\text\{\\small\}\\\\ &\\\\ \\mathsf\{Put\\text\{\-\}req\\text\{\-\}payload\}\\coloneqq\\mathsf\{Unit\}&\\text\{\\small Put payload types\}\\\\ \\mathsf\{put\\text\{\-\}req\}\\ \(k,\\\_\)\(\\\_,\\sigma\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Put Request\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle\\circ,\\sigma\\rangle&\\text\{\\small No payload\}\\\\ \\mathsf\{put\\text\{\-\}guard\}\\ \(\\\_,\\\_\)\(\\\_\)\(\\\_,\\\_,\\\_\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Put Guard\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\mathsf\{true\}&\\text\{\\small\}\\\\ \\mathsf\{put\}\\ \(k,v\)\(\\\_\)\(\\\_,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Put\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\varsigma\[k\\mapsto v\]&\\\\ \\hline\\cr\\end\{array\}

Figure 15:Relaxed Specification
### I\.1Read\-Your\-Writes \(RYW\)

A client’s read sees its own most recent write\. The session tracks every put the client has issued; the get\-guard requires the responding replica to have applied every put in that set \([fig\.˜16](https://arxiv.org/html/2605.23109#A9.F16)\)\. The reference implementation stores per\-replica state as a function from key to timestamp \([fig\.˜17](https://arxiv.org/html/2605.23109#A9.F17)\)\.

𝕀𝑅𝑌𝑊​̵⃰​\(Read Your Writes Specification\)T≔𝖭𝖺𝗍Timestamp𝖢𝖲𝗍𝖺𝗍𝖾≔Client State𝖲𝖾𝗍​\[K×T\]Session puts\. \(Tuniquely identifies puts in a client\.\)𝖼​\-​𝗂𝗇𝗂𝗍​\(c\)≔Client Initial State∅No initial puts𝖱𝖲𝗍𝖺𝗍𝖾≔Replica StateK↦\(V×C×T×Map from each keykto its valuev, its origin⟨c,t⟩,𝖲𝖾𝗍\[T\]\)and timestamps of puts onkbefore it\.𝗋​\-​𝗂𝗇𝗂𝗍​\(r,v0\)≔Replica Initial State\[k↦⟨v0,c0,0,∅⟩¯\]𝖦𝖾𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔𝖲𝖾𝗍​\[T\]Get payload types𝖦𝖾𝗍​\-​𝗋𝖾𝗌​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔𝖴𝗇𝗂𝗍𝗀𝖾𝗍​\-​𝗋𝖾𝗊​\(k\)​\(\_,p\)≔At client:Get Request𝗋𝖾𝗍​⟨p\|k,p⟩Session past puts as request payload, State unchanged𝗀𝖾𝗍​\-​𝗀𝗎𝖺𝗋𝖽​\(k\)​\(p\)​\(c,\_,ς\)≔At replica:Get Guard𝗅𝖾𝗍​⟨\_,c′,t′,p′⟩←ς​\(k\)𝗋𝖾𝗍​c=c′⇒p⊆p′∪\{t′\}If stored value is from requesting client, his puts not missed\.𝗀𝖾𝗍​\(k\)​\(\_\)​\(\_,\_,ς\)≔At replica:Get𝗅𝖾𝗍​⟨v,\_,\_,\_⟩←ς​\(k\)𝗋𝖾𝗍​⟨v,∘,ς⟩No payload𝗀𝖾𝗍​\-​𝗋𝖾𝗌​\(\_,\_\)​\(\_\)​\(\_,p\)≔At client:Get Response𝗋𝖾𝗍​pState unchanged\.𝖯𝗎𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔T×𝖲𝖾𝗍​\[T\]Put payload types𝗉𝗎𝗍​\-​𝗋𝖾𝗊​\(k,\_\)​\(𝑠𝑒𝑙𝑓,p\)≔At client:Put Request𝗅𝖾𝗍​t←\|p\|\+1Current put timestamp𝗅𝖾𝗍​p′←p∪\{⟨t,k⟩\}The put is added to session puts\.𝗋𝖾𝗍​⟨⟨t,p\|k⟩,p′⟩Session puts are sent as request payload\.𝗉𝗎𝗍​\-​𝗀𝗎𝖺𝗋𝖽​\(\_,\_\)​\(\_\)​\(\_,\_,\_\)≔At replica:Put Guard𝗋𝖾𝗍​𝗍𝗋𝗎𝖾𝗉𝗎𝗍​\(k,v\)​\(⟨t,p⟩\)​\(c,\_,ς\)≔At replica:Put𝗋𝖾𝗍​ς​\[k↦⟨v,c,t,p⟩\]p\|k≔\{t\|⟨t,k⟩∈p\}\\displaystyle\\begin\{array\}\[\]\{\|lr\|\}\\hline\\cr\\mathbb\{I\}\_\{\\mathit\{RYW\}\} ⃰\\ \(\\textsc\{Read Your Writes Specification\}\)&\\\\ \\hline\\cr T\\coloneqq\\mathsf\{Nat\}&\\text\{\\small Timestamp\}\\\\ \\mathsf\{CState\}\\coloneqq&\\textbf\{\\small Client State\}\\\\ \\phantom\{X\}\\mathsf\{Set\}\[K\\times T\]&\\text\{\\small Session puts\. \($T$ uniquely identifies puts in a client\.\)\}\\\\ \\mathsf\{c\\text\{\-\}init\}\(c\)\\coloneqq&\\textbf\{\\small Client Initial State\}\\\\ \\phantom\{X\}\\emptyset&\\text\{\\small No initial puts\}\\\\ \\mathsf\{RState\}\\coloneqq&\\textbf\{\\small Replica State\}\\\\ \\phantom\{X\}K\\mapsto\(V\\times C\\times T\\,\\times&\\text\{\\small Map from each key $k$ to its value $v$, its origin $\\langle c,t\\rangle$,\}\\\\ \\phantom\{X\}\\phantom\{K\\mapsto\(\}\\mathsf\{Set\}\[T\]\)&\\text\{\\small and timestamps of puts on $k$ before it\.\}\\\\ \\mathsf\{r\\text\{\-\}init\}\(r,v\_\{0\}\)\\coloneqq&\\textbf\{\\small Replica Initial State\}\\\\ \\phantom\{X\}\[\\overline\{k\\mapsto\\langle v\_\{0\},c\_\{0\},0,\\emptyset\\rangle\}\]&\\text\{\\small\}\\\\ &\\\\ \\mathsf\{Get\\text\{\-\}req\\text\{\-\}payload\}\\coloneqq\\mathsf\{Set\}\[T\]&\\text\{\\small Get payload types\}\\\\ \\mathsf\{Get\\text\{\-\}res\\text\{\-\}payload\}\\coloneqq\\mathsf\{Unit\}&\\\\ \\mathsf\{get\\text\{\-\}req\}\\ \(k\)\(\\\_,p\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Get Request\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle p\|\_\{k\},p\\rangle&\\text\{\\small Session past puts as request payload, State unchanged\}\\\\ \\mathsf\{get\\text\{\-\}guard\}\\ \(k\)\(p\)\(c,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Get Guard\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle\\\_,c^\{\\prime\},t^\{\\prime\},p^\{\\prime\}\\rangle\\leftarrow\\varsigma\(k\)&\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ c=c^\{\\prime\}\\Rightarrow p\\subseteq p^\{\\prime\}\\cup\\\{t^\{\\prime\}\\\}&\\text\{\\small If stored value is from requesting client, his puts not missed\.\}\\\\ \\mathsf\{get\}\\ \(k\)\(\\\_\)\(\\\_,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Get\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle v,\\\_,\\\_,\\\_\\rangle\\leftarrow\\varsigma\(k\)&\\text\{\\small\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle v,\\circ,\\varsigma\\rangle&\\text\{\\small No payload\}\\\\ \\mathsf\{get\\text\{\-\}res\}\\ \(\\\_,\\\_\)\(\\\_\)\(\\\_,p\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Get Response\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ p&\\text\{\\small State unchanged\.\}\\\\ &\\\\ \\mathsf\{Put\\text\{\-\}req\\text\{\-\}payload\}\\coloneqq T\\times\\mathsf\{Set\}\[T\]&\\text\{\\small Put payload types\}\\\\ \\mathsf\{put\\text\{\-\}req\}\\ \(k,\\\_\)\(\\mathit\{self\},p\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Put Request\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ t\\leftarrow\|p\|\+1&\\text\{\\small Current put timestamp\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ p^\{\\prime\}\\leftarrow p\\cup\\\{\\langle t,k\\rangle\\\}&\\text\{\\small The put is added to session puts\.\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle\\langle t,p\|\_\{k\}\\rangle,p^\{\\prime\}\\rangle&\\text\{\\small Session puts are sent as request payload\.\}\\\\ \\mathsf\{put\\text\{\-\}guard\}\\ \(\\\_,\\\_\)\(\\\_\)\(\\\_,\\\_,\\\_\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Put Guard\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\mathsf\{true\}&\\text\{\\small\}\\\\ \\mathsf\{put\}\\ \(k,v\)\(\\langle t,p\\rangle\)\(c,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Put\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\varsigma\[k\\mapsto\\langle v,c,t,p\\rangle\]&\\\\ &\\\\ p\|\_\{k\}\\coloneqq\\\{t\\ \|\\ \\langle t,k\\rangle\\in p\\\}&\\\\ \\hline\\cr\\end\{array\}Figure 16:Read Your Writes Specification𝕀𝑅𝑌𝑊​\(Read Your Writes Implementation\)T≔𝖭𝖺𝗍Timestamp𝖢𝖲𝗍𝖺𝗍𝖾≔Client StateK↦TLatest put for each key\. \(Tuniquely identifies puts in a client\.\)𝖼​\-​𝗂𝗇𝗂𝗍​\(c\)≔Client Initial State\[k↦0¯\]No initial puts𝖱𝖲𝗍𝖺𝗍𝖾≔Replica StateK↦\(V×C×T\)Map from each keykto its valuev, and its origin⟨c,t⟩𝗋​\-​𝗂𝗇𝗂𝗍​\(r,v0\)≔Replica Initial State\[k↦⟨v0,c0,0⟩¯\]𝖦𝖾𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔TGet payload types𝖦𝖾𝗍​\-​𝗋𝖾𝗌​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔𝖴𝗇𝗂𝗍𝗀𝖾𝗍​\-​𝗋𝖾𝗊​\(k\)​\(\_,p\)≔At client:Get Request𝗋𝖾𝗍​⟨p​\(k\),p⟩Timestamp of latest put as request payload, State unchanged𝗀𝖾𝗍​\-​𝗀𝗎𝖺𝗋𝖽​\(k\)​\(t\)​\(c,\_,ς\)≔At replica:Get Guard𝗅𝖾𝗍​⟨\_,c′,t′⟩←ς​\(k\)𝗋𝖾𝗍​c=c′⇒t=t′If stored value is from requesting client, his puts not missed\.𝗀𝖾𝗍​\(k\)​\(\_\)​\(\_,\_,ς\)≔At replica:Get𝗅𝖾𝗍​⟨v,\_,\_⟩←ς​\(k\)𝗋𝖾𝗍​⟨v,∘,ς⟩No payload𝗀𝖾𝗍​\-​𝗋𝖾𝗌​\(\_,\_\)​\(\_\)​\(\_,p\)≔At client:Get Response𝗋𝖾𝗍​pState unchanged\.𝖯𝗎𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔TPut payload types𝗉𝗎𝗍​\-​𝗋𝖾𝗊​\(k,\_\)​\(𝑠𝑒𝑙𝑓,p\)≔At client:Put Request𝗅𝖾𝗍​t←p​\(k\)\+1Current put timestamp𝗅𝖾𝗍​p′←p​\[k↦t\]The put timestamp is stored as the latest for the key\.𝗋𝖾𝗍​⟨t,p′⟩Latest put timestamp sent as request payload\.𝗉𝗎𝗍​\-​𝗀𝗎𝖺𝗋𝖽​\(\_,\_\)​\(\_\)​\(\_,\_,\_\)≔At replica:Put Guard𝗋𝖾𝗍​𝗍𝗋𝗎𝖾𝗉𝗎𝗍​\(k,v\)​\(t\)​\(c,\_,ς\)≔At replica:Put𝗋𝖾𝗍​ς​\[k↦⟨v,c,t⟩\]\\displaystyle\\begin\{array\}\[\]\{\|lr\|\}\\hline\\cr\\mathbb\{I\}\_\{\\mathit\{RYW\}\}\\ \(\\textsc\{Read Your Writes Implementation\}\)&\\\\ \\hline\\cr T\\coloneqq\\mathsf\{Nat\}&\\text\{\\small Timestamp\}\\\\ \\mathsf\{CState\}\\coloneqq&\\textbf\{\\small Client State\}\\\\ \\phantom\{X\}K\\mapsto T&\\text\{\\small Latest put for each key\. \($T$ uniquely identifies puts in a client\.\)\}\\\\ \\mathsf\{c\\text\{\-\}init\}\(c\)\\coloneqq&\\textbf\{\\small Client Initial State\}\\\\ \\phantom\{X\}\[\\overline\{k\\mapsto 0\}\]&\\text\{\\small No initial puts\}\\\\ \\mathsf\{RState\}\\coloneqq&\\textbf\{\\small Replica State\}\\\\ \\phantom\{X\}K\\mapsto\(V\\times C\\times T\)&\\text\{\\small Map from each key $k$ to its value $v$, and its origin $\\langle c,t\\rangle$\}\\\\ \\mathsf\{r\\text\{\-\}init\}\(r,v\_\{0\}\)\\coloneqq&\\textbf\{\\small Replica Initial State\}\\\\ \\phantom\{X\}\[\\overline\{k\\mapsto\\langle v\_\{0\},c\_\{0\},0\\rangle\}\]&\\text\{\\small\}\\\\ &\\\\ \\mathsf\{Get\\text\{\-\}req\\text\{\-\}payload\}\\coloneqq T&\\text\{\\small Get payload types\}\\\\ \\mathsf\{Get\\text\{\-\}res\\text\{\-\}payload\}\\coloneqq\\mathsf\{Unit\}&\\\\ \\mathsf\{get\\text\{\-\}req\}\\ \(k\)\(\\\_,p\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Get Request\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle p\(k\),p\\rangle&\\text\{\\small Timestamp of latest put as request payload, State unchanged\}\\\\ \\mathsf\{get\\text\{\-\}guard\}\\ \(k\)\(t\)\(c,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Get Guard\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle\\\_,c^\{\\prime\},t^\{\\prime\}\\rangle\\leftarrow\\varsigma\(k\)&\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ c=c^\{\\prime\}\\Rightarrow t=t^\{\\prime\}&\\text\{\\small If stored value is from requesting client, his puts not missed\.\}\\\\ \\mathsf\{get\}\\ \(k\)\(\\\_\)\(\\\_,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Get\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle v,\\\_,\\\_\\rangle\\leftarrow\\varsigma\(k\)&\\text\{\\small\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle v,\\circ,\\varsigma\\rangle&\\text\{\\small No payload\}\\\\ \\mathsf\{get\\text\{\-\}res\}\\ \(\\\_,\\\_\)\(\\\_\)\(\\\_,p\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Get Response\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ p&\\text\{\\small State unchanged\.\}\\\\ &\\\\ \\mathsf\{Put\\text\{\-\}req\\text\{\-\}payload\}\\coloneqq T&\\text\{\\small Put payload types\}\\\\ \\mathsf\{put\\text\{\-\}req\}\\ \(k,\\\_\)\(\\mathit\{self\},p\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Put Request\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ t\\leftarrow p\(k\)\+1&\\text\{\\small Current put timestamp\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ p^\{\\prime\}\\leftarrow p\[k\\mapsto t\]&\\text\{\\small The put timestamp is stored as the latest for the key\.\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle t,p^\{\\prime\}\\rangle&\\text\{\\small Latest put timestamp sent as request payload\.\}\\\\ \\mathsf\{put\\text\{\-\}guard\}\\ \(\\\_,\\\_\)\(\\\_\)\(\\\_,\\\_,\\\_\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Put Guard\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\mathsf\{true\}&\\text\{\\small\}\\\\ \\mathsf\{put\}\\ \(k,v\)\(t\)\(c,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Put\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\varsigma\[k\\mapsto\\langle v,c,t\\rangle\]&\\\\ \\hline\\cr\\end\{array\}Figure 17:Read Your Writes Implementation
### I\.2Monotonic Reads \(MR\)

A client’s reads respect the order of writes the client has previously observed\. The session keeps the set of writes seen so far; subsequent reads must return values applied no earlier than every write in that set \([fig\.˜18](https://arxiv.org/html/2605.23109#A9.F18)\)\. The reference implementation stores per\-replica state as a function from key to \(value, client, timestamp\); the get\-guard checks every entry against the client’s session set on every read \([fig\.˜19](https://arxiv.org/html/2605.23109#A9.F19)\)\.

𝕀𝑀𝑅​̵⃰​\(Monotonic Reads Specification\)T≔𝖭𝖺𝗍Timestamp𝖢𝖲𝗍𝖺𝗍𝖾≔Client State𝖲𝖾𝗍\[T×K\]×Session puts\. \(C×Tuniquely identifies puts\.\)𝖲𝖾𝗍​\[C×T×K\]Session dependencies\.𝖼​\-​𝗂𝗇𝗂𝗍​\(c\)≔Client Initial State∅No initial dependencies𝖱𝖲𝗍𝖺𝗍𝖾≔Replica StateK↦\(V×C×T×Map from each keyKto its valueV, its originC×T𝖲𝖾𝗍\[T×K\]\)and puts before it𝗋​\-​𝗂𝗇𝗂𝗍​\(r,v0\)≔Replica Initial State\[k↦⟨v0,c0,0,∅⟩¯\]𝖦𝖾𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔𝖲𝖾𝗍​\[C×T\]Get payload types𝖦𝖾𝗍​\-​𝗋𝖾𝗌​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔C×T𝗀𝖾𝗍​\-​𝗋𝖾𝗊​\(k\)​\(\_,⟨p,d⟩\)≔At client:Get Request𝗋𝖾𝗍​⟨d\|k,⟨p,d⟩⟩Session deps forksent as payload, State unchanged𝗀𝖾𝗍​\-​𝗀𝗎𝖺𝗋𝖽​\(k\)​\(d\)​\(c,\_,ς\)≔At replica:Get Guard𝗅𝖾𝗍​⟨\_,c′,t′,d′⟩←ς​\(k\)𝗋𝖾𝗍​d\|c′⊆d′\|k∪\{t′\}Stored put fromc′doesn’t miss observed puts fromc′\.𝗀𝖾𝗍​\(k\)​\(\_\)​\(\_,\_,ς\)≔𝗅𝖾𝗍​⟨v,c,t,d⟩←ς​\(k\)𝗋𝖾𝗍​⟨v,⟨c,t⟩,ς⟩The stored put returned as a dependency\.𝗀𝖾𝗍​\-​𝗋𝖾𝗌​\(k,\_\)​\(⟨c,t⟩\)​\(\_,⟨p,d⟩\)≔At client:Get Response𝗋𝖾𝗍​⟨p,d∪\{⟨c,t,k⟩\}⟩Returned dependency added to session dependencies\.𝖯𝗎𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔T×𝖲𝖾𝗍​\[T×K\]Put payload types𝗉𝗎𝗍​\-​𝗋𝖾𝗊​\(k,\_\)​\(\_,⟨p,d⟩\)≔At client:Put Request𝗅𝖾𝗍​t←\|p\|\+1Current put timestamp𝗅𝖾𝗍​p′←p∪\{⟨t,k⟩\}The put is added to session puts\.𝗋𝖾𝗍​⟨⟨t,p⟩,⟨p′,d⟩⟩Session puts are sent as request payload\.𝗉𝗎𝗍​\-​𝗀𝗎𝖺𝗋𝖽​\(\_,\_\)​\(\_\)​\(\_,\_,\_\)≔At replica:Put Guard𝗋𝖾𝗍​𝗍𝗋𝗎𝖾𝗉𝗎𝗍​\(k,v\)​\(⟨t,p⟩\)​\(c,\_,ς\)≔At replica:Put𝗋𝖾𝗍​ς​\[k↦⟨v,c,t,p⟩\]d\|k≔\{⟨c,t⟩\|⟨c,t,k⟩∈d\}d\|k≔\{t\|⟨t,k⟩∈d\}d\|c≔\{t\|⟨c,t⟩∈d\}\\displaystyle\\begin\{array\}\[\]\{\|lr\|\}\\hline\\cr\\mathbb\{I\}\_\{\\mathit\{MR\}\} ⃰\\ \(\\textsc\{Monotonic Reads Specification\}\)&\\\\ \\hline\\cr T\\coloneqq\\mathsf\{Nat\}&\\text\{\\small Timestamp\}\\\\ \\mathsf\{CState\}\\coloneqq&\\textbf\{\\small Client State\}\\\\ \\phantom\{X\}\\mathsf\{Set\}\[T\\times K\]\\,\\times&\\text\{\\small Session puts\. \($C\\times T$ uniquely identifies puts\.\)\}\\\\ \\phantom\{X\}\\mathsf\{Set\}\[C\\times T\\times K\]&\\text\{\\small Session dependencies\.\}\\\\ \\mathsf\{c\\text\{\-\}init\}\(c\)\\coloneqq&\\textbf\{\\small Client Initial State\}\\\\ \\phantom\{X\}\\emptyset&\\text\{\\small No initial dependencies\}\\\\ \\mathsf\{RState\}\\coloneqq&\\textbf\{\\small Replica State\}\\\\ \\phantom\{X\}K\\mapsto\(V\\times C\\times T\\,\\times&\\text\{\\small Map from each key $K$ to its value $V$, its origin $C\\times T$\}\\\\ \\phantom\{X\}\\phantom\{K\\mapsto\(\}\\mathsf\{Set\}\[T\\times K\]\)&\\text\{\\small and puts before it\}\\\\ \\mathsf\{r\\text\{\-\}init\}\(r,v\_\{0\}\)\\coloneqq&\\textbf\{\\small Replica Initial State\}\\\\ \\phantom\{X\}\[\\overline\{k\\mapsto\\langle v\_\{0\},c\_\{0\},0,\\emptyset\\rangle\}\]&\\text\{\\small\}\\\\ &\\\\ \\mathsf\{Get\\text\{\-\}req\\text\{\-\}payload\}\\coloneqq\\mathsf\{Set\}\[C\\times T\]&\\text\{\\small Get payload types\}\\\\ \\mathsf\{Get\\text\{\-\}res\\text\{\-\}payload\}\\coloneqq C\\times T&\\text\{\\small\}\\\\ \\mathsf\{get\\text\{\-\}req\}\\ \(k\)\(\\\_,\\langle p,d\\rangle\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Get Request\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle d\|\_\{k\},\\langle p,d\\rangle\\rangle&\\text\{\\small Session deps for $k$ sent as payload, State unchanged\}\\\\ \\mathsf\{get\\text\{\-\}guard\}\\ \(k\)\(d\)\(c,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Get Guard\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle\\\_,c^\{\\prime\},t^\{\\prime\},d^\{\\prime\}\\rangle\\leftarrow\\varsigma\(k\)&\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ d\|\_\{c^\{\\prime\}\}\\subseteq d^\{\\prime\}\|\_\{k\}\\cup\\\{t^\{\\prime\}\\\}&\\text\{\\small Stored put from $c^\{\\prime\}$ doesn't miss observed puts from $c^\{\\prime\}$\.\}\\\\ \\mathsf\{get\}\\ \(k\)\(\\\_\)\(\\\_,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle v,c,t,d\\rangle\\leftarrow\\varsigma\(k\)&\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle v,\\langle c,t\\rangle,\\varsigma\\rangle&\\text\{\\small The stored put returned as a dependency\.\}\\\\ \\mathsf\{get\\text\{\-\}res\}\\ \(k,\\\_\)\(\\langle c,t\\rangle\)\(\\\_,\\langle p,d\\rangle\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Get Response\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle p,d\\cup\\\{\\langle c,t,k\\rangle\\\}\\rangle&\\text\{\\small Returned dependency added to session dependencies\.\}\\\\ &\\\\ \\mathsf\{Put\\text\{\-\}req\\text\{\-\}payload\}\\coloneqq T\\times\\mathsf\{Set\}\[T\\times K\]&\\text\{\\small Put payload types\}\\\\ \\mathsf\{put\\text\{\-\}req\}\\ \(k,\\\_\)\(\\\_,\\langle p,d\\rangle\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Put Request\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ t\\leftarrow\|p\|\+1&\\text\{\\small Current put timestamp\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ p^\{\\prime\}\\leftarrow p\\cup\\\{\\langle t,k\\rangle\\\}&\\text\{\\small The put is added to session puts\.\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle\\langle t,p\\rangle,\\langle p^\{\\prime\},d\\rangle\\rangle&\\text\{\\small Session puts are sent as request payload\.\}\\\\ \\mathsf\{put\\text\{\-\}guard\}\\ \(\\\_,\\\_\)\(\\\_\)\(\\\_,\\\_,\\\_\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Put Guard\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\mathsf\{true\}&\\text\{\\small\}\\\\ \\mathsf\{put\}\\ \(k,v\)\(\\langle t,p\\rangle\)\(c,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Put\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\varsigma\[k\\mapsto\\langle v,c,t,p\\rangle\]&\\\\ &\\\\ d\|\_\{k\}\\coloneqq\\\{\\langle c,t\\rangle\\ \|\\ \\langle c,t,k\\rangle\\in d\\\}&\\\\ d\|\_\{k\}\\coloneqq\\\{t\\ \|\\ \\langle t,k\\rangle\\in d\\\}&\\\\ d\|\_\{c\}\\coloneqq\\\{t\\ \|\\ \\langle c,t\\rangle\\in d\\\}&\\\\ \\hline\\cr\\end\{array\}Figure 18:Monotonic Reads Specification𝕀𝑀𝑅​\(Monotonic Reads Implementation\)T≔𝖭𝖺𝗍Timestamp𝖢𝖲𝗍𝖺𝗍𝖾≔Client StateT×Session latest put timestampK↦C↦TLargest timestamp read for the key from the client\.𝖼​\-​𝗂𝗇𝗂𝗍​\(c\)≔Client Initial State⟨∅,∅⟩No initial puts and dependencies𝖱𝖲𝗍𝖺𝗍𝖾≔Replica StateK↦\(V×C×T\)Map from each keyKto its valueV, its originC×T𝗋​\-​𝗂𝗇𝗂𝗍​\(r,v0\)≔Replica Initial State\[k↦⟨v0,c0,0⟩¯\]𝖦𝖾𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔𝖲𝖾𝗍​\[C×T\]Get payload types𝖦𝖾𝗍​\-​𝗋𝖾𝗌​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔C×T𝗀𝖾𝗍​\-​𝗋𝖾𝗊​\(k\)​\(\_,⟨t,d⟩\)≔At client:Get Request𝗋𝖾𝗍​⟨d​\(k\),⟨t,d⟩⟩Session deps forksent as payload, State unchanged𝗀𝖾𝗍​\-​𝗀𝗎𝖺𝗋𝖽​\(k\)​\(d\)​\(c,\_,ς\)≔At replica:Get Guard𝗅𝖾𝗍​⟨\_,c′,t′⟩←ς​\(k\)𝗋𝖾𝗍​d​\(c′\)≤t′Stored put fromc′doesn’t miss observed puts fromc′\.𝗀𝖾𝗍​\(k\)​\(\_\)​\(\_,\_,ς\)≔𝗅𝖾𝗍​⟨v,c,t⟩←ς​\(k\)𝗋𝖾𝗍​⟨v,⟨c,t⟩,ς⟩The stored put returned as a dependency\.𝗀𝖾𝗍​\-​𝗋𝖾𝗌​\(k,\_\)​\(⟨c,t⟩\)​\(\_,⟨t,d⟩\)≔At client:Get Response𝗋𝖾𝗍​⟨t,d​\[⟨k,c⟩↦t\]⟩Returned dependency advances session dependencies\.𝖯𝗎𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔TPut payload types𝗉𝗎𝗍​\-​𝗋𝖾𝗊​\(k,\_\)​\(\_,⟨t,d⟩\)≔At client:Put Request𝗅𝖾𝗍​t′←t\+1Current put timestamp𝗋𝖾𝗍​⟨t′,⟨t′,d⟩⟩𝗉𝗎𝗍​\-​𝗀𝗎𝖺𝗋𝖽​\(\_,\_\)​\(\_\)​\(\_,\_,\_\)≔At replica:Put Guard𝗋𝖾𝗍​𝗍𝗋𝗎𝖾𝗉𝗎𝗍​\(k,v\)​\(t\)​\(c,\_,ς\)≔At replica:Put𝗋𝖾𝗍​ς​\[k↦⟨v,c,t⟩\]\\displaystyle\\begin\{array\}\[\]\{\|lr\|\}\\hline\\cr\\mathbb\{I\}\_\{\\mathit\{MR\}\}\\ \(\\textsc\{Monotonic Reads Implementation\}\)&\\\\ \\hline\\cr T\\coloneqq\\mathsf\{Nat\}&\\text\{\\small Timestamp\}\\\\ \\mathsf\{CState\}\\coloneqq&\\textbf\{\\small Client State\}\\\\ \\phantom\{X\}T\\ \\times&\\text\{\\small Session latest put timestamp\}\\\\ \\phantom\{X\}K\\mapsto C\\mapsto T&\\text\{\\small Largest timestamp read for the key from the client\.\}\\\\ \\mathsf\{c\\text\{\-\}init\}\(c\)\\coloneqq&\\textbf\{\\small Client Initial State\}\\\\ \\phantom\{X\}\\langle\\emptyset,\\emptyset\\rangle&\\text\{\\small No initial puts and dependencies\}\\\\ \\mathsf\{RState\}\\coloneqq&\\textbf\{\\small Replica State\}\\\\ \\phantom\{X\}K\\mapsto\(V\\times C\\times T\)&\\text\{\\small Map from each key $K$ to its value $V$, its origin $C\\times T$\}\\\\ \\mathsf\{r\\text\{\-\}init\}\(r,v\_\{0\}\)\\coloneqq&\\textbf\{\\small Replica Initial State\}\\\\ \\phantom\{X\}\[\\overline\{k\\mapsto\\langle v\_\{0\},c\_\{0\},0\\rangle\}\]&\\text\{\\small\}\\\\ &\\\\ \\mathsf\{Get\\text\{\-\}req\\text\{\-\}payload\}\\coloneqq\\mathsf\{Set\}\[C\\times T\]&\\text\{\\small Get payload types\}\\\\ \\mathsf\{Get\\text\{\-\}res\\text\{\-\}payload\}\\coloneqq C\\times T&\\text\{\\small\}\\\\ \\mathsf\{get\\text\{\-\}req\}\\ \(k\)\(\\\_,\\langle t,d\\rangle\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Get Request\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle d\(k\),\\langle t,d\\rangle\\rangle&\\text\{\\small Session deps for $k$ sent as payload, State unchanged\}\\\\ \\mathsf\{get\\text\{\-\}guard\}\\ \(k\)\(d\)\(c,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Get Guard\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle\\\_,c^\{\\prime\},t^\{\\prime\}\\rangle\\leftarrow\\varsigma\(k\)&\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ d\(c^\{\\prime\}\)\\leq t^\{\\prime\}&\\text\{\\small Stored put from $c^\{\\prime\}$ doesn't miss observed puts from $c^\{\\prime\}$\.\}\\\\ \\mathsf\{get\}\\ \(k\)\(\\\_\)\(\\\_,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle v,c,t\\rangle\\leftarrow\\varsigma\(k\)&\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle v,\\langle c,t\\rangle,\\varsigma\\rangle&\\text\{\\small The stored put returned as a dependency\.\}\\\\ \\mathsf\{get\\text\{\-\}res\}\\ \(k,\\\_\)\(\\langle c,t\\rangle\)\(\\\_,\\langle t,d\\rangle\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Get Response\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle t,d\[\\langle k,c\\rangle\\mapsto t\]\\rangle&\\text\{\\small Returned dependency advances session dependencies\.\}\\\\ &\\\\ \\mathsf\{Put\\text\{\-\}req\\text\{\-\}payload\}\\coloneqq T&\\text\{\\small Put payload types\}\\\\ \\mathsf\{put\\text\{\-\}req\}\\ \(k,\\\_\)\(\\\_,\\langle t,d\\rangle\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Put Request\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ t^\{\\prime\}\\leftarrow t\+1&\\text\{\\small Current put timestamp\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle t^\{\\prime\},\\langle t^\{\\prime\},d\\rangle\\rangle&\\text\{\\small\}\\\\ \\mathsf\{put\\text\{\-\}guard\}\\ \(\\\_,\\\_\)\(\\\_\)\(\\\_,\\\_,\\\_\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Put Guard\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\mathsf\{true\}&\\text\{\\small\}\\\\ \\mathsf\{put\}\\ \(k,v\)\(t\)\(c,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Put\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\varsigma\[k\\mapsto\\langle v,c,t\\rangle\]&\\\\ \\hline\\cr\\end\{array\}Figure 19:Monotonic Reads Implementation
### I\.3Monotonic Writes \(MW\)

A single client’s writes are observed in order at every replica that observes them\. Each replica records, per writing client, the latest applied timestamp; the put\-guard rejects any out\-of\-order delivery \([fig\.˜20](https://arxiv.org/html/2605.23109#A9.F20)\)\. The reference implementation prepends the timestamp of each new write to a per\-key list with no de\-duplication, so receivers can re\-check ordering on every delivery \([fig\.˜21](https://arxiv.org/html/2605.23109#A9.F21)\)\.

𝕀𝑀𝑊​̵⃰​\(Monotonic Writes Specification\)T≔𝖭𝖺𝗍Timestamp𝖢𝖲𝗍𝖺𝗍𝖾≔Client State𝖲𝖾𝗍​\[T×K\]Session puts\. \(C×Tuniquely identifies puts\.\)𝖼​\-​𝗂𝗇𝗂𝗍​\(c\)≔Client Initial State∅No initial dependencies𝖱𝖲𝗍𝖺𝗍𝖾≔Replica StateK↦\(V×𝖲𝖾𝗍​\[C×T\]\)Map from each keyKto its valueV, and puts already applied\.𝗋​\-​𝗂𝗇𝗂𝗍​\(r,v0\)≔Replica Initial State\[k↦⟨v0,∅⟩¯\]𝖦𝖾𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔𝖦𝖾𝗍​\-​𝗋𝖾𝗌​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔𝖴𝗇𝗂𝗍Get payload types𝗀𝖾𝗍​\-​𝗋𝖾𝗊​\(\_\)​\(\_,p\)≔At client:Get Request𝗋𝖾𝗍​⟨∘,p⟩Session past puts as request payload, State unchanged𝗀𝖾𝗍​\-​𝗀𝗎𝖺𝗋𝖽​\(\_\)​\(\_\)​\(\_,\_,\_\)≔At replica:Get Guard𝗋𝖾𝗍​𝗍𝗋𝗎𝖾𝗀𝖾𝗍​\(k\)​\(\_\)​\(\_,\_,ς\)≔At replica:Get𝗅𝖾𝗍​⟨v,\_⟩←ς​\(k\)𝗋𝖾𝗍​⟨v,∘,ς⟩No payload𝗀𝖾𝗍​\-​𝗋𝖾𝗌​\(\_,\_\)​\(\_\)​\(\_,p\)≔At client:Get Response𝗋𝖾𝗍​pState unchanged\.𝖯𝗎𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔T×𝖲𝖾𝗍​\[T\]Put payload types𝗉𝗎𝗍​\-​𝗋𝖾𝗊​\(k,\_\)​\(\_,p\)≔At client:Put Request𝗅𝖾𝗍​t←\|p\|\+1Current put timestamp𝗅𝖾𝗍​p′←p∪\{⟨t,k⟩\}The put is added to session puts\.𝗋𝖾𝗍​⟨⟨t,p\|k⟩,p′⟩Session puts for the key are sent as request payload\.𝗉𝗎𝗍​\-​𝗀𝗎𝖺𝗋𝖽​\(k,\_\)​\(⟨t,p⟩\)​\(c,\_,ς\)≔At replica:Put Guard𝗅𝖾𝗍​⟨\_,p′⟩←ς​\(k\)𝗋𝖾𝗍​p⊆p′\|cPrevious puts of session already applied\.𝗉𝗎𝗍​\(k,v\)​\(⟨t,\_⟩\)​\(c,\_,ς\)≔At replica:Put𝗅𝖾𝗍​⟨\_,p′⟩←ς​\(k\)𝗋𝖾𝗍ς\[k↦⟨v,p′∪\{⟨c,t⟩\}\]p\|k≔\{t\|⟨t,k⟩∈p\}p\|c≔\{t\|⟨c,t⟩∈p\}\\displaystyle\\begin\{array\}\[\]\{\|lr\|\}\\hline\\cr\\mathbb\{I\}\_\{\\mathit\{MW\}\} ⃰\\ \(\\textsc\{Monotonic Writes Specification\}\)&\\\\ \\hline\\cr T\\coloneqq\\mathsf\{Nat\}&\\text\{\\small Timestamp\}\\\\ \\mathsf\{CState\}\\coloneqq&\\textbf\{\\small Client State\}\\\\ \\phantom\{X\}\\mathsf\{Set\}\[T\\times K\]&\\text\{\\small Session puts\. \($C\\times T$ uniquely identifies puts\.\)\}\\\\ \\mathsf\{c\\text\{\-\}init\}\(c\)\\coloneqq&\\textbf\{\\small Client Initial State\}\\\\ \\phantom\{X\}\\emptyset&\\text\{\\small No initial dependencies\}\\\\ \\mathsf\{RState\}\\coloneqq&\\textbf\{\\small Replica State\}\\\\ \\phantom\{X\}K\\mapsto\(V\\times\\mathsf\{Set\}\[C\\times T\]\)&\\text\{\\small Map from each key $K$ to its value $V$, and puts already applied\.\}\\\\ \\mathsf\{r\\text\{\-\}init\}\(r,v\_\{0\}\)\\coloneqq&\\textbf\{\\small Replica Initial State\}\\\\ \\phantom\{X\}\[\\overline\{k\\mapsto\\langle v\_\{0\},\\emptyset\\rangle\}\]&\\text\{\\small\}\\\\ &\\\\ \\mathsf\{Get\\text\{\-\}req\\text\{\-\}payload\}\\coloneqq\\mathsf\{Get\\text\{\-\}res\\text\{\-\}payload\}\\coloneqq\\mathsf\{Unit\}&\\text\{\\small Get payload types\}\\\\ \\mathsf\{get\\text\{\-\}req\}\\ \(\\\_\)\(\\\_,p\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Get Request\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle\\circ,p\\rangle&\\text\{\\small Session past puts as request payload, State unchanged\}\\\\ \\mathsf\{get\\text\{\-\}guard\}\\ \(\\\_\)\(\\\_\)\(\\\_,\\\_,\\\_\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Get Guard\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\mathsf\{true\}&\\text\{\\small\}\\\\ \\mathsf\{get\}\\ \(k\)\(\\\_\)\(\\\_,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Get\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle v,\\\_\\rangle\\leftarrow\\varsigma\(k\)&\\text\{\\small\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle v,\\circ,\\varsigma\\rangle&\\text\{\\small No payload\}\\\\ \\mathsf\{get\\text\{\-\}res\}\\ \(\\\_,\\\_\)\(\\\_\)\(\\\_,p\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Get Response\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ p&\\text\{\\small State unchanged\.\}\\\\ &\\\\ \\mathsf\{Put\\text\{\-\}req\\text\{\-\}payload\}\\coloneqq T\\times\\mathsf\{Set\}\[T\]&\\text\{\\small Put payload types\}\\\\ \\mathsf\{put\\text\{\-\}req\}\\ \(k,\\\_\)\(\\\_,p\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Put Request\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ t\\leftarrow\|p\|\+1&\\text\{\\small Current put timestamp\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ p^\{\\prime\}\\leftarrow p\\cup\\\{\\langle t,k\\rangle\\\}&\\text\{\\small The put is added to session puts\.\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle\\langle t,p\|\_\{k\}\\rangle,p^\{\\prime\}\\rangle&\\text\{\\small Session puts for the key are sent as request payload\.\}\\\\ \\mathsf\{put\\text\{\-\}guard\}\\ \(k,\\\_\)\(\\langle t,p\\rangle\)\(c,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Put Guard\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle\\\_,p^\{\\prime\}\\rangle\\leftarrow\\varsigma\(k\)&\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ p\\subseteq p^\{\\prime\}\|\_\{c\}&\\text\{\\small Previous puts of session already applied\.\}\\\\ \\mathsf\{put\}\\ \(k,v\)\(\\langle t,\\\_\\rangle\)\(c,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Put\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle\\\_,p^\{\\prime\}\\rangle\\leftarrow\\varsigma\(k\)&\\text\{\\small\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\varsigma\[k\\mapsto\\langle v,p^\{\\prime\}\\cup\\\{\\langle c,t\\rangle\\\}\]&\\\\ &\\\\ p\|\_\{k\}\\coloneqq\\\{t\\ \|\\ \\langle t,k\\rangle\\in p\\\}&\\\\ p\|\_\{c\}\\coloneqq\\\{t\\ \|\\ \\langle c,t\\rangle\\in p\\\}&\\\\ \\hline\\cr\\end\{array\}Figure 20:Monotonic Writes Specification𝕀𝑀𝑊​\(Monotonic Writes Implementation\)T≔𝖭𝖺𝗍Timestamp𝖢𝖲𝗍𝖺𝗍𝖾≔Client StateK↦TLatest timestamp of puts for the key\.𝖼​\-​𝗂𝗇𝗂𝗍​\(c\)≔Client Initial Statek↦0¯No initial puts𝖱𝖲𝗍𝖺𝗍𝖾≔Replica StateK↦\(V×Map from each keyKto its valueV, andC↦T\)latest puts applied from sessions\.𝗋​\-​𝗂𝗇𝗂𝗍​\(r,v0\)≔Replica Initial State\[k↦⟨v0,c↦0¯⟩¯\]𝖦𝖾𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔𝖦𝖾𝗍​\-​𝗋𝖾𝗌​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔𝖴𝗇𝗂𝗍Get payload types𝗀𝖾𝗍​\-​𝗋𝖾𝗊​\(\_\)​\(\_,σ\)≔At client:Get Request𝗋𝖾𝗍​⟨∘,σ⟩Session past puts as request payload, State unchanged𝗀𝖾𝗍​\-​𝗀𝗎𝖺𝗋𝖽​\(\_\)​\(\_\)​\(\_,\_,\_\)≔At replica:Get Guard𝗋𝖾𝗍​𝗍𝗋𝗎𝖾𝗀𝖾𝗍​\(k\)​\(\_\)​\(\_,\_,ς\)≔At replica:Get𝗅𝖾𝗍​⟨v,\_⟩←ς​\(k\)𝗋𝖾𝗍​⟨v,∘,ς⟩No payload𝗀𝖾𝗍​\-​𝗋𝖾𝗌​\(\_,\_\)​\(\_\)​\(\_,σ\)≔At client:Get Response𝗋𝖾𝗍​σState unchanged\.𝖯𝗎𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔TPut payload types𝗉𝗎𝗍​\-​𝗋𝖾𝗊​\(k,\_\)​\(\_,p\)≔At client:Put Requestt←p​\(k\)𝗅𝖾𝗍​p′←p​\[k↦t\+1\]The timestamp of the latest put for key is advanced\.𝗋𝖾𝗍​⟨t,p′⟩Latest put timestamp for the key is sent as request payload\.𝗉𝗎𝗍​\-​𝗀𝗎𝖺𝗋𝖽​\(k,\_\)​\(t\)​\(c,\_,ς\)≔At replica:Put Guard𝗅𝖾𝗍​⟨\_,p′⟩←ς​\(k\)𝗋𝖾𝗍​p′​\(c\)=tPrevious puts of session already applied\.𝗉𝗎𝗍​\(k,v\)​\(t\)​\(c,\_,ς\)≔At replica:Put𝗅𝖾𝗍​⟨\_,p′⟩←ς​\(k\)𝗋𝖾𝗍​ς​\[k↦⟨v,p′​\[c↦t\+1\]⟩\]\\displaystyle\\begin\{array\}\[\]\{\|lr\|\}\\hline\\cr\\mathbb\{I\}\_\{\\mathit\{MW\}\}\\ \(\\textsc\{Monotonic Writes Implementation\}\)&\\\\ \\hline\\cr T\\coloneqq\\mathsf\{Nat\}&\\text\{\\small Timestamp\}\\\\ \\mathsf\{CState\}\\coloneqq&\\textbf\{\\small Client State\}\\\\ \\phantom\{X\}K\\mapsto T&\\text\{\\small Latest timestamp of puts for the key\.\}\\\\ \\mathsf\{c\\text\{\-\}init\}\(c\)\\coloneqq&\\textbf\{\\small Client Initial State\}\\\\ \\phantom\{X\}\\overline\{k\\mapsto 0\}&\\text\{\\small No initial puts\}\\\\ \\mathsf\{RState\}\\coloneqq&\\textbf\{\\small Replica State\}\\\\ \\phantom\{X\}K\\mapsto\(V\\ \\times&\\text\{\\small Map from each key $K$ to its value $V$, and\}\\\\ \\phantom\{X\}\\phantom\{K\\mapsto\(\}C\\mapsto T\)&\\text\{\\small latest puts applied from sessions\.\}\\\\ \\mathsf\{r\\text\{\-\}init\}\(r,v\_\{0\}\)\\coloneqq&\\textbf\{\\small Replica Initial State\}\\\\ \\phantom\{X\}\[\\overline\{k\\mapsto\\langle v\_\{0\},\\overline\{c\\mapsto 0\}\\rangle\}\]&\\text\{\\small\}\\\\ &\\\\ \\mathsf\{Get\\text\{\-\}req\\text\{\-\}payload\}\\coloneqq\\mathsf\{Get\\text\{\-\}res\\text\{\-\}payload\}\\coloneqq\\mathsf\{Unit\}&\\text\{\\small Get payload types\}\\\\ \\mathsf\{get\\text\{\-\}req\}\\ \(\\\_\)\(\\\_,\\sigma\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Get Request\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle\\circ,\\sigma\\rangle&\\text\{\\small Session past puts as request payload, State unchanged\}\\\\ \\mathsf\{get\\text\{\-\}guard\}\\ \(\\\_\)\(\\\_\)\(\\\_,\\\_,\\\_\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Get Guard\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\mathsf\{true\}&\\text\{\\small\}\\\\ \\mathsf\{get\}\\ \(k\)\(\\\_\)\(\\\_,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Get\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle v,\\\_\\rangle\\leftarrow\\varsigma\(k\)&\\text\{\\small\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle v,\\circ,\\varsigma\\rangle&\\text\{\\small No payload\}\\\\ \\mathsf\{get\\text\{\-\}res\}\\ \(\\\_,\\\_\)\(\\\_\)\(\\\_,\\sigma\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Get Response\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\sigma&\\text\{\\small State unchanged\.\}\\\\ &\\\\ \\mathsf\{Put\\text\{\-\}req\\text\{\-\}payload\}\\coloneqq T&\\text\{\\small Put payload types\}\\\\ \\mathsf\{put\\text\{\-\}req\}\\ \(k,\\\_\)\(\\\_,p\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Put Request\}\\\\ \\phantom\{X\}t\\leftarrow p\(k\)&\\text\{\\small\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ p^\{\\prime\}\\leftarrow p\[k\\mapsto t\+1\]&\\text\{\\small The timestamp of the latest put for key is advanced\.\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle t,p^\{\\prime\}\\rangle&\\text\{\\small Latest put timestamp for the key is sent as request payload\.\}\\\\ \\mathsf\{put\\text\{\-\}guard\}\\ \(k,\\\_\)\(t\)\(c,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Put Guard\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle\\\_,p^\{\\prime\}\\rangle\\leftarrow\\varsigma\(k\)&\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ p^\{\\prime\}\(c\)=t&\\text\{\\small Previous puts of session already applied\.\}\\\\ \\mathsf\{put\}\\ \(k,v\)\(t\)\(c,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Put\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle\\\_,p^\{\\prime\}\\rangle\\leftarrow\\varsigma\(k\)&\\text\{\\small\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\varsigma\[k\\mapsto\\langle v,p^\{\\prime\}\[c\\mapsto t\+1\]\\rangle\]&\\text\{\\small\}\\\\ \\hline\\cr\\end\{array\}Figure 21:Monotonic Writes Implementation
### I\.4Read\-Your\-Writes\+\+Monotonic Writes \(RYW\+MW\)

Composition of Read\-Your\-Writes and Monotonic Writes\. RYW\+MW is the conjunction of RYW and MW rather than an independent property; an implementation satisfies it iff it refines both, so correctness is the joint refinement obligation\. The reference combines RYW’s read\-side check with MW’s compare\-and\-swap on every put \([fig\.˜22](https://arxiv.org/html/2605.23109#A9.F22)\)\.

𝕀𝑅𝑌𝑊​\-​𝑀𝑊​\(Read Your Writes and Monotonic Writes Implementation\)T≔𝖭𝖺𝗍Timestamp𝖢𝖲𝗍𝖺𝗍𝖾≔Client StateK↦TLatest timestamp of puts for the key\.𝖼​\-​𝗂𝗇𝗂𝗍​\(c\)≔Client Initial Statek↦0¯No initial puts𝖱𝖲𝗍𝖺𝗍𝖾≔Replica StateK↦\(V×C×Map from each keyKto its valueV, and its originating sessionsC,C↦T\)latest puts applied from sessions𝗋​\-​𝗂𝗇𝗂𝗍​\(r,v0\)≔Replica Initial State\[k↦⟨v0,0,c↦0¯⟩¯\]𝖦𝖾𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔TGet payload types𝖦𝖾𝗍​\-​𝗋𝖾𝗌​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔𝖴𝗇𝗂𝗍𝗀𝖾𝗍​\-​𝗋𝖾𝗊​\(k\)​\(\_,p\)≔At client:Get Request𝗋𝖾𝗍​⟨p​\(k\),p⟩Timestamp of latest put as request payload, State unchanged𝗀𝖾𝗍​\-​𝗀𝗎𝖺𝗋𝖽​\(k\)​\(t\)​\(c,\_,ς\)≔At replica:Get Guard𝗅𝖾𝗍​⟨\_,c′,p′⟩←ς​\(k\)𝗋𝖾𝗍​c=c′⇒p′​\(c′\)=tIf stored value is from requesting client, his puts not missed\.𝗀𝖾𝗍​\(k\)​\(\_\)​\(\_,\_,ς\)≔At replica:Get𝗅𝖾𝗍​⟨v,\_,\_⟩←ς​\(k\)𝗋𝖾𝗍​⟨v,∘,ς⟩No payload𝗀𝖾𝗍​\-​𝗋𝖾𝗌​\(\_,\_\)​\(\_\)​\(\_,p\)≔At client:Get Response𝗋𝖾𝗍​pState unchanged\.𝖯𝗎𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔TPut payload types𝗉𝗎𝗍​\-​𝗋𝖾𝗊​\(k,\_\)​\(\_,p\)≔At client:Put Requestt←p​\(k\)𝗅𝖾𝗍​p′←p​\[k↦t\+1\]The timestamp of the latest put for key is advanced\.𝗋𝖾𝗍​⟨t,p′⟩Latest put timestamp for the key is sent as request payload\.𝗉𝗎𝗍​\-​𝗀𝗎𝖺𝗋𝖽​\(k,\_\)​\(t\)​\(c,\_,ς\)≔At replica:Put Guard𝗅𝖾𝗍​⟨\_,\_,p′⟩←ς​\(k\)𝗋𝖾𝗍​p′​\(c\)=tPrevious puts of session already applied\.𝗉𝗎𝗍​\(k,v\)​\(t\)​\(c,\_,ς\)≔At replica:Put𝗅𝖾𝗍​⟨\_,p′⟩←ς​\(k\)𝗋𝖾𝗍​ς​\[k↦⟨v,c,p′​\[c↦t\+1\]⟩\]\\displaystyle\\begin\{array\}\[\]\{\|lr\|\}\\hline\\cr\\vrule\\lx@intercol\\mathbb\{I\}\_\{\\mathit\{RYW\}\\text\{\-\}\\mathit\{MW\}\}\\ \(\\textsc\{Read Your Writes and Monotonic Writes Implementation\}\)\\hfil\\lx@intercol\\vrule\\lx@intercol\\\\ \\hline\\cr T\\coloneqq\\mathsf\{Nat\}&\\text\{\\small Timestamp\}\\\\ \\mathsf\{CState\}\\coloneqq&\\textbf\{\\small Client State\}\\\\ \\phantom\{X\}K\\mapsto T&\\text\{\\small Latest timestamp of puts for the key\.\}\\\\ \\mathsf\{c\\text\{\-\}init\}\(c\)\\coloneqq&\\textbf\{\\small Client Initial State\}\\\\ \\phantom\{X\}\\overline\{k\\mapsto 0\}&\\text\{\\small No initial puts\}\\\\ \\mathsf\{RState\}\\coloneqq&\\textbf\{\\small Replica State\}\\\\ \\phantom\{X\}K\\mapsto\(V\\times C\\ \\times&\\text\{\\small Map from each key $K$ to its value $V$, and its originating sessions $C$,\}\\\\ \\phantom\{X\}\\phantom\{K\\mapsto\(\}C\\mapsto T\)&\\text\{\\small latest puts applied from sessions\}\\\\ \\mathsf\{r\\text\{\-\}init\}\(r,v\_\{0\}\)\\coloneqq&\\textbf\{\\small Replica Initial State\}\\\\ \\phantom\{X\}\[\\overline\{k\\mapsto\\langle v\_\{0\},0,\\overline\{c\\mapsto 0\}\\rangle\}\]&\\text\{\\small\}\\\\ &\\\\ \\mathsf\{Get\\text\{\-\}req\\text\{\-\}payload\}\\coloneqq T&\\text\{\\small Get payload types\}\\\\ \\mathsf\{Get\\text\{\-\}res\\text\{\-\}payload\}\\coloneqq\\mathsf\{Unit\}&\\\\ \\mathsf\{get\\text\{\-\}req\}\\ \(k\)\(\\\_,p\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Get Request\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle p\(k\),p\\rangle&\\text\{\\small Timestamp of latest put as request payload, State unchanged\}\\\\ \\mathsf\{get\\text\{\-\}guard\}\\ \(k\)\(t\)\(c,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Get Guard\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle\\\_,c^\{\\prime\},p^\{\\prime\}\\rangle\\leftarrow\\varsigma\(k\)&\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ c=c^\{\\prime\}\\Rightarrow p^\{\\prime\}\(c^\{\\prime\}\)=t&\\text\{\\small If stored value is from requesting client, his puts not missed\.\}\\\\ \\mathsf\{get\}\\ \(k\)\(\\\_\)\(\\\_,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Get\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle v,\\\_,\\\_\\rangle\\leftarrow\\varsigma\(k\)&\\text\{\\small\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle v,\\circ,\\varsigma\\rangle&\\text\{\\small No payload\}\\\\ \\mathsf\{get\\text\{\-\}res\}\\ \(\\\_,\\\_\)\(\\\_\)\(\\\_,p\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Get Response\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ p&\\text\{\\small State unchanged\.\}\\\\ &\\\\ \\mathsf\{Put\\text\{\-\}req\\text\{\-\}payload\}\\coloneqq T&\\text\{\\small Put payload types\}\\\\ \\mathsf\{put\\text\{\-\}req\}\\ \(k,\\\_\)\(\\\_,p\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Put Request\}\\\\ \\phantom\{X\}t\\leftarrow p\(k\)&\\text\{\\small\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ p^\{\\prime\}\\leftarrow p\[k\\mapsto t\+1\]&\\text\{\\small The timestamp of the latest put for key is advanced\.\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle t,p^\{\\prime\}\\rangle&\\text\{\\small Latest put timestamp for the key is sent as request payload\.\}\\\\ \\mathsf\{put\\text\{\-\}guard\}\\ \(k,\\\_\)\(t\)\(c,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Put Guard\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle\\\_,\\\_,p^\{\\prime\}\\rangle\\leftarrow\\varsigma\(k\)&\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ p^\{\\prime\}\(c\)=t&\\text\{\\small Previous puts of session already applied\.\}\\\\ \\mathsf\{put\}\\ \(k,v\)\(t\)\(c,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Put\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle\\\_,p^\{\\prime\}\\rangle\\leftarrow\\varsigma\(k\)&\\text\{\\small\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\varsigma\[k\\mapsto\\langle v,c,p^\{\\prime\}\[c\\mapsto t\+1\]\\rangle\]&\\text\{\\small\}\\\\ \\hline\\cr\\end\{array\}Figure 22:Read Your Writes and Monotonic Writes Implementation
### I\.5Causal Consistency \(CC\) and Labeled Causal Consistency \(LCC\)

Causal Consistency \(CC\)\.Cross\-client causal consistency: every read returns a value whose causal predecessors have all been observed at the responding replica\. Dependencies are tracked as explicit sets in the spec state \([fig\.˜23](https://arxiv.org/html/2605.23109#A9.F23)\), which the implementation must bridge to its concrete representation \(typically a per\-client vector clock plus a compare\-and\-swap on the writer’s own slot during put\)\. Two reference implementations are given: a per\-client vector\-clock store \([fig\.˜25](https://arxiv.org/html/2605.23109#A9.F25)\) and a Lloyd–Freedman\-style protocol \([fig\.˜26](https://arxiv.org/html/2605.23109#A9.F26)\)\.

Labeled Causal Consistency \(LCC\)\.Causal consistency parameterised by per\-message topic labels and per\-client interest masks\. Every put is tagged with a label, and every client declares which labels it cares about; the get\-guard requires the responding replica to have observed every dependency whose label is in the requesting client’s mask \([fig\.˜24](https://arxiv.org/html/2605.23109#A9.F24)\)\. To our knowledge this is the first Rocq formalisation of LCC and the first verified implementation\.

𝕀𝐶𝐶​̵⃰​\(Causal Consistency Spec\)T≔𝖭𝖺𝗍Timestamp𝖢𝖲𝗍𝖺𝗍𝖾≔Client State⟨𝖲𝖾𝗍\[C×T×K\],Session dependencies from puts\.𝖲𝖾𝗍\[𝖲𝖾𝗍\[C×T×K\]\]⟩Session dependencies from gets\(C×Tuniquely identifies puts\.\)𝖼​\-​𝗂𝗇𝗂𝗍​\(c\)≔Client Initial State⟨∅,∅⟩No initial dependencies𝖱𝖲𝗍𝖺𝗍𝖾≔Replica StateK↦\(V×C×T×Map from each keyKto its valueV, its originC×T,𝖲𝖾𝗍\[C×T×K\]\)and set of dependencies𝗋​\-​𝗂𝗇𝗂𝗍​\(r,v0\)≔Replica Initial State\[k↦⟨v0,c0,0,∅⟩¯\]Empty initial dependencies𝖦𝖾𝗍\-𝗋𝖾𝗊\-𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔⟨𝖲𝖾𝗍\[C×T×K\],Get payload types𝖲𝖾𝗍\[𝖲𝖾𝗍\[C×T×K\]\]⟩𝖦𝖾𝗍​\-​𝗋𝖾𝗌​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔𝖲𝖾𝗍​\[C×T×K\]𝗀𝖾𝗍​\-​𝗋𝖾𝗊​\(k\)​\(\_,⟨p,G⟩\)≔At client:Get Request𝗋𝖾𝗍​⟨⟨p\|k,G\|k⟩,⟨p,G⟩⟩Session deps sent as request payload, State unchanged𝗀𝖾𝗍​\-​𝗀𝗎𝖺𝗋𝖽​\(k\)​\(⟨p,G⟩\)​\(c,\_,ς\)≔At replica:Get Guard𝗅𝖾𝗍​⟨\_,c′,t′,d′⟩←ς​\(k\)𝗋𝖾𝗍𝖿𝗈𝗋𝖺𝗅𝗅\(λd\.¬\(d′\|k∪\{⟨c′,t′,k⟩\}⊂d\)\)G∧Stored value isn’t behind any previously read value\.c=c′⇒p⊆d′\|k∪\{⟨c′,t′,k⟩\}Read your writes\.𝗀𝖾𝗍​\(k\)​\(\_\)​\(\_,\_,ς\)≔At replica:Get𝗅𝖾𝗍​⟨v,c,t,d⟩←ς​\(k\)𝗅𝖾𝗍​d′←𝗂𝖿​\(c≠c0\)​d∪\{⟨c,t,k⟩\}​𝖾𝗅𝗌𝖾​∅The dependencies returned to the session𝗋𝖾𝗍​⟨v,d′,ς⟩are the entry and its dependencies𝗀𝖾𝗍​\-​𝗋𝖾𝗌​\(\_,\_\)​\(d′\)​\(\_,⟨p,G⟩\)≔At client:Get Response𝗋𝖾𝗍​⟨p,G∪\{d′\}⟩Received dependencies added to session dependencies\.𝖯𝗎𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔T×𝖲𝖾𝗍​\[C×T×K\]Put payload types𝗉𝗎𝗍​\-​𝗋𝖾𝗊​\(k,\_\)​\(𝑠𝑒𝑙𝑓,⟨p,G⟩\)≔At client:Put Request𝗅𝖾𝗍​t←\|p\|\+1Current put timestamp𝗅𝖾𝗍​p′←p∪\{⟨𝑠𝑒𝑙𝑓,t,k⟩\}The put is added to session dependencies\.𝗋𝖾𝗍​⟨⟨t,p∪\(⋃G\)⟩,⟨p′,G⟩⟩Session dependencies are sent as request payload\.𝗉𝗎𝗍​\-​𝗀𝗎𝖺𝗋𝖽​\(k,\_\)​\(⟨t,\_⟩\)​\(c,\_,ς\)≔At replica:Put Guard𝗅𝖾𝗍​⟨\_,\_,\_,d′⟩←ς​\(k\)𝗋𝖾𝗍​⟨c,t,k⟩∉d′The new put is not causally before the current stored put\.𝗉𝗎𝗍​\(k,v\)​\(⟨t,d⟩\)​\(c,\_,ς\)≔At replica:Put𝗋𝖾𝗍​ς​\[k↦⟨v,c,t,d⟩\]d\|k≔\{⟨c,t,k⟩\|⟨c,t,k′⟩∈d∧k=k′\}D\|k≔\{d\|k\|d∈D\}\\displaystyle\\begin\{array\}\[\]\{\|lr\|\}\\hline\\cr\\mathbb\{I\}\_\{\\mathit\{CC\}\} ⃰\\ \(\\textsc\{Causal Consistency Spec\}\)&\\\\ \\hline\\cr T\\coloneqq\\mathsf\{Nat\}&\\text\{\\small Timestamp\}\\\\ \\mathsf\{CState\}\\coloneqq&\\textbf\{\\small Client State\}\\\\ \\phantom\{X\}\\langle\\mathsf\{Set\}\[C\\times T\\times K\],&\\text\{\\small Session dependencies from puts\.\}\\\\ \\phantom\{X\}\\phantom\{\\langle\}\\mathsf\{Set\}\[\\mathsf\{Set\}\[C\\times T\\times K\]\]\\rangle&\\text\{\\small Session dependencies from gets\}\\\\ \\phantom\{X\}&\\text\{\\small\($C\\times T$ uniquely identifies puts\.\)\}\\\\ \\mathsf\{c\\text\{\-\}init\}\(c\)\\coloneqq&\\textbf\{\\small Client Initial State\}\\\\ \\phantom\{X\}\\langle\\emptyset,\\emptyset\\rangle&\\text\{\\small No initial dependencies\}\\\\ \\mathsf\{RState\}\\coloneqq&\\textbf\{\\small Replica State\}\\\\ \\phantom\{X\}K\\mapsto\(V\\times C\\times T\\,\\times&\\text\{\\small Map from each key $K$ to its value $V$, its origin $C\\times T$,\}\\\\ \\phantom\{X\}\\phantom\{K\\mapsto\(\}\\mathsf\{Set\}\[C\\times T\\times K\]\)&\\text\{\\small and set of dependencies\}\\\\ \\mathsf\{r\\text\{\-\}init\}\(r,v\_\{0\}\)\\coloneqq&\\textbf\{\\small Replica Initial State\}\\\\ \\phantom\{X\}\[\\overline\{k\\mapsto\\langle v\_\{0\},c\_\{0\},0,\\emptyset\\rangle\}\]&\\text\{\\small Empty initial dependencies\}\\\\ &\\\\ \\mathsf\{Get\\text\{\-\}req\\text\{\-\}payload\}\\coloneqq\\langle\\mathsf\{Set\}\[C\\times T\\times K\],&\\text\{\\small Get payload types\}\\\\ \\phantom\{\\mathsf\{Get\\text\{\-\}req\\text\{\-\}payload\}\\coloneqq\\langle\}\\mathsf\{Set\}\[\\mathsf\{Set\}\[C\\times T\\times K\]\]\\rangle&\\text\{\\small\}\\\\ \\mathsf\{Get\\text\{\-\}res\\text\{\-\}payload\}\\coloneqq\\mathsf\{Set\}\[C\\times T\\times K\]&\\\\ \\mathsf\{get\\text\{\-\}req\}\\ \(k\)\(\\\_,\\langle p,G\\rangle\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Get Request\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle\\langle p\|\_\{k\},G\|\_\{k\}\\rangle,\\langle p,G\\rangle\\rangle&\\text\{\\small Session deps sent as request payload, State unchanged\}\\\\ \\mathsf\{get\\text\{\-\}guard\}\\ \(k\)\(\\langle p,G\\rangle\)\(c,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Get Guard\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle\\\_,c^\{\\prime\},t^\{\\prime\},d^\{\\prime\}\\rangle\\leftarrow\\varsigma\(k\)&\\text\{\\small\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\mathsf\{forall\}\\ \(\\lambda d\.\\ \\neg\(d^\{\\prime\}\|\_\{k\}\\cup\\\{\\langle c^\{\\prime\},t^\{\\prime\},k\\rangle\\\}\\subset d\)\)\\ G\\ \\wedge&\\text\{\\small Stored value isn't behind any previously read value\.\}\\\\ \\phantom\{X\}\\phantom\{\\mathsf\{ret\}\\ \}c=c^\{\\prime\}\\Rightarrow p\\subseteq d^\{\\prime\}\|\_\{k\}\\cup\\\{\\langle c^\{\\prime\},t^\{\\prime\},k\\rangle\\\}&\\text\{\\small Read your writes\.\}\\\\ \\mathsf\{get\}\\ \(k\)\(\\\_\)\(\\\_,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Get\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle v,c,t,d\\rangle\\leftarrow\\varsigma\(k\)&\\\\ \\phantom\{X\}\\mathsf\{let\}\\ d^\{\\prime\}\\leftarrow\\mathsf\{if\}\\ \(c\\neq c\_\{0\}\)\\ d\\cup\\\{\\langle c,t,k\\rangle\\\}\\ \\mathsf\{else\}\\ \\emptyset&\\text\{\\small The dependencies returned to the session\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle v,d^\{\\prime\},\\varsigma\\rangle&\\text\{\\small are the entry and its dependencies\}\\\\ \\mathsf\{get\\text\{\-\}res\}\\ \(\\\_,\\\_\)\(d^\{\\prime\}\)\(\\\_,\\langle p,G\\rangle\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Get Response\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle p,G\\cup\\\{d^\{\\prime\}\\\}\\rangle&\\text\{\\small Received dependencies added to session dependencies\.\}\\\\ &\\\\ \\mathsf\{Put\\text\{\-\}req\\text\{\-\}payload\}\\coloneqq T\\times\\mathsf\{Set\}\[C\\times T\\times K\]&\\text\{\\small Put payload types\}\\\\ \\mathsf\{put\\text\{\-\}req\}\\ \(k,\\\_\)\(\\mathit\{self\},\\langle p,G\\rangle\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Put Request\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ t\\leftarrow\|p\|\+1&\\text\{\\small Current put timestamp\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ p^\{\\prime\}\\leftarrow p\\cup\\\{\\langle\\mathit\{self\},t,k\\rangle\\\}&\\text\{\\small The put is added to session dependencies\.\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle\\langle t,p\\cup\(\\bigcup\\,G\)\\rangle,\\langle p^\{\\prime\},G\\rangle\\rangle&\\text\{\\small Session dependencies are sent as request payload\.\}\\\\ \\mathsf\{put\\text\{\-\}guard\}\\ \(k,\\\_\)\(\\langle t,\\\_\\rangle\)\(c,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Put Guard\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle\\\_,\\\_,\\\_,d^\{\\prime\}\\rangle\\leftarrow\\varsigma\(k\)&\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle c,t,k\\rangle\\not\\in d^\{\\prime\}&\\text\{\\small The new put is not causally before the current stored put\.\}\\\\ \\mathsf\{put\}\\ \(k,v\)\(\\langle t,d\\rangle\)\(c,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Put\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\varsigma\[k\\mapsto\\langle v,c,t,d\\rangle\]&\\\\ &\\\\ d\|\_\{k\}\\coloneqq\\\{\\langle c,t,k\\rangle\\ \|\\ \\langle c,t,k^\{\\prime\}\\rangle\\in d\\wedge k=k^\{\\prime\}\\\}&\\\\ D\|\_\{k\}\\coloneqq\\\{d\|\_\{k\}\\ \|\\ d\\in D\\\}&\\\\ \\hline\\cr\\end\{array\}Figure 23:Causal Consistency Spec𝕀𝐿𝐶𝐶​̵⃰​\(Labeled Causal Consistency Spec\)LLabel type𝑙𝑎𝑏𝑒𝑙:V→LMaps each value to its label𝑐𝑙𝑖𝑒𝑛𝑡​\-​𝑙𝑎𝑏𝑒𝑙𝑠:C→𝖲𝖾𝗍​\[L\]Maps each client to its set of relevant labelsT≔𝖭𝖺𝗍Timestamp𝖢𝖲𝗍𝖺𝗍𝖾≔Client State⟨𝖲𝖾𝗍\[C×T×K×L\],Session dependencies from puts \(with labels\)𝖲𝖾𝗍\[𝖲𝖾𝗍\[C×T×K×L\]\]⟩Session dependencies from gets \(with labels\)𝖼​\-​𝗂𝗇𝗂𝗍​\(c\)≔Client Initial State⟨∅,∅⟩No initial dependencies𝖱𝖲𝗍𝖺𝗍𝖾≔Replica StateK↦\(V×C×T×Map from each keyKto its valueV, its originC×T,𝖲𝖾𝗍\[C×T×K×L\]\)and set of label\-annotated dependencies𝗋​\-​𝗂𝗇𝗂𝗍​\(r,v0\)≔Replica Initial State\[k↦⟨v0,c0,0,∅⟩¯\]Empty initial dependencies𝖦𝖾𝗍\-𝗋𝖾𝗊\-𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔⟨𝖲𝖾𝗍\[C×T×K×L\]Get payload types𝖲𝖾𝗍​\[𝖲𝖾𝗍​\[C×T×K×L\]\]𝖦𝖾𝗍​\-​𝗋𝖾𝗌​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔𝖲𝖾𝗍​\[C×T×K×L\]𝗀𝖾𝗍​\-​𝗋𝖾𝗊​\(k\)​\(𝑠𝑒𝑙𝑓,⟨p,G⟩\)≔At client:Get Request𝗅𝖾𝗍​L←𝑐𝑙𝑖𝑒𝑛𝑡​\-​𝑙𝑎𝑏𝑒𝑙𝑠​\(𝑠𝑒𝑙𝑓\)𝗋𝖾𝗍​⟨⟨p\|k\|L,G\|k\|L⟩,⟨p,G⟩⟩Label\-filtered deps sent as payload; state unchanged\.𝗀𝖾𝗍​\-​𝗀𝗎𝖺𝗋𝖽​\(k\)​\(⟨p,G⟩\)​\(c,\_,ς\)≔At replica:Get Guard𝗅𝖾𝗍​⟨v′,c′,t′,d′⟩←ς​\(k\)𝗅𝖾𝗍​L←𝑐𝑙𝑖𝑒𝑛𝑡​\-​𝑙𝑎𝑏𝑒𝑙𝑠​\(c\)𝗋𝖾𝗍𝖿𝗈𝗋𝖺𝗅𝗅\(λd\.Stored value not behind any previously¬\(\(d′\|k∪\{⟨c′,t′,k,𝑙𝑎𝑏𝑒𝑙\(v′\)⟩\}\)\|L⊂d\)\)Gread value, for client’s labels\.∧c=c′⇒p⊆d′\|k∪\{⟨c′,t′,k,𝑙𝑎𝑏𝑒𝑙​\(v′\)⟩\}Read your writes\.𝗀𝖾𝗍​\(k\)​\(\_\)​\(\_,\_,ς\)≔At replica:Get𝗅𝖾𝗍​⟨v,c,t,d⟩←ς​\(k\)𝗅𝖾𝗍​d′←𝗂𝖿​\(c≠c0\)​d∪\{⟨c,t,k,𝑙𝑎𝑏𝑒𝑙​\(v\)⟩\}​𝖾𝗅𝗌𝖾​∅Label of stored value included in returned dependency\.𝗋𝖾𝗍​⟨v,d′,ς⟩𝗀𝖾𝗍​\-​𝗋𝖾𝗌​\(\_,\_\)​\(d′\)​\(\_,⟨p,G⟩\)≔At client:Get Response𝗋𝖾𝗍​⟨p,G∪\{d′\}⟩Received dependencies added to session\.𝖯𝗎𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔T×𝖲𝖾𝗍​\[C×T×K×L\]Put payload types𝗉𝗎𝗍​\-​𝗋𝖾𝗊​\(k,v\)​\(𝑠𝑒𝑙𝑓,⟨p,G⟩\)≔At client:Put Request𝗅𝖾𝗍​t←\|p\|\+1Current put timestamp𝗅𝖾𝗍​p′←p∪\{⟨𝑠𝑒𝑙𝑓,t,k,𝑙𝑎𝑏𝑒𝑙​\(v\)⟩\}Put with its label added to session dependencies\.𝗋𝖾𝗍​⟨⟨t,p∪\(⋃G\)⟩,⟨p′,G⟩⟩All session dependencies sent as request payload\.𝗉𝗎𝗍​\-​𝗀𝗎𝖺𝗋𝖽​\(k,v\)​\(⟨t,\_⟩\)​\(c,\_,ς\)≔At replica:Put Guard𝗅𝖾𝗍​⟨\_,\_,\_,d′⟩←ς​\(k\)𝗋𝖾𝗍​⟨c,t,k,𝑙𝑎𝑏𝑒𝑙​\(v\)⟩∉d′The new put has not already been applied\.𝗉𝗎𝗍​\(k,v\)​\(⟨t,d⟩\)​\(c,\_,ς\)≔At replica:Put𝗋𝖾𝗍​ς​\[k↦⟨v,c,t,d⟩\]d\|k≔\{⟨c,t,k,l⟩\|⟨c,t,k′,l⟩∈d∧k=k′\}D\|k≔\{d\|k\|d∈D\}d\|L≔\{⟨c,t,k,l⟩\|⟨c,t,k,l⟩∈d∧l∈L\}Filter dependencies to the label setLD\|L≔\{d\|L\|d∈D\}\\displaystyle\\begin\{array\}\[\]\{\|lr\|\}\\hline\\cr\\mathbb\{I\}\_\{\\mathit\{LCC\}\} ⃰\\ \(\\textsc\{Labeled Causal Consistency Spec\}\)&\\\\ \\hline\\cr L&\\text\{\\small Label type\}\\\\ \\mathit\{label\}:V\\rightarrow L&\\text\{\\small Maps each value to its label\}\\\\ \\mathit\{client\\text\{\-\}labels\}:C\\rightarrow\\mathsf\{Set\}\[L\]&\\text\{\\small Maps each client to its set of relevant labels\}\\\\ T\\coloneqq\\mathsf\{Nat\}&\\text\{\\small Timestamp\}\\\\ \\mathsf\{CState\}\\coloneqq&\\textbf\{\\small Client State\}\\\\ \\phantom\{X\}\\langle\\mathsf\{Set\}\[C\\times T\\times K\\times L\],&\\text\{\\small Session dependencies from puts \(with labels\)\}\\\\ \\phantom\{X\}\\phantom\{\\langle\}\\mathsf\{Set\}\[\\mathsf\{Set\}\[C\\times T\\times K\\times L\]\]\\rangle&\\text\{\\small Session dependencies from gets \(with labels\)\}\\\\ \\mathsf\{c\\text\{\-\}init\}\(c\)\\coloneqq&\\textbf\{\\small Client Initial State\}\\\\ \\phantom\{X\}\\langle\\emptyset,\\emptyset\\rangle&\\text\{\\small No initial dependencies\}\\\\ \\mathsf\{RState\}\\coloneqq&\\textbf\{\\small Replica State\}\\\\ \\phantom\{X\}K\\mapsto\(V\\times C\\times T\\,\\times&\\text\{\\small Map from each key $K$ to its value $V$, its origin $C\\times T$,\}\\\\ \\phantom\{X\}\\phantom\{K\\mapsto\(\}\\mathsf\{Set\}\[C\\times T\\times K\\times L\]\)&\\text\{\\small and set of label\-annotated dependencies\}\\\\ \\mathsf\{r\\text\{\-\}init\}\(r,v\_\{0\}\)\\coloneqq&\\textbf\{\\small Replica Initial State\}\\\\ \\phantom\{X\}\[\\overline\{k\\mapsto\\langle v\_\{0\},c\_\{0\},0,\\emptyset\\rangle\}\]&\\text\{\\small Empty initial dependencies\}\\\\ &\\\\ \\mathsf\{Get\\text\{\-\}req\\text\{\-\}payload\}\\coloneqq\\langle\\mathsf\{Set\}\[C\\times T\\times K\\times L\]&\\text\{\\small Get payload types\}\\\\ \\phantom\{\\mathsf\{Get\\text\{\-\}req\\text\{\-\}payload\}\\coloneqq\\langle\}\\mathsf\{Set\}\[\\mathsf\{Set\}\[C\\times T\\times K\\times L\]\]&\\\\ \\mathsf\{Get\\text\{\-\}res\\text\{\-\}payload\}\\coloneqq\\mathsf\{Set\}\[C\\times T\\times K\\times L\]&\\\\ \\mathsf\{get\\text\{\-\}req\}\\ \(k\)\(\\mathit\{self\},\\langle p,G\\rangle\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Get Request\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ L\\leftarrow\\mathit\{client\\text\{\-\}labels\}\(\\mathit\{self\}\)&\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle\\langle p\|\_\{k\}\|\_\{L\},G\|\_\{k\}\|\_\{L\}\\rangle,\\langle p,G\\rangle\\rangle&\\text\{\\small Label\-filtered deps sent as payload; state unchanged\.\}\\\\ \\mathsf\{get\\text\{\-\}guard\}\\ \(k\)\(\\langle p,G\\rangle\)\(c,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Get Guard\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle v^\{\\prime\},c^\{\\prime\},t^\{\\prime\},d^\{\\prime\}\\rangle\\leftarrow\\varsigma\(k\)&\\\\ \\phantom\{X\}\\mathsf\{let\}\\ L\\leftarrow\\mathit\{client\\text\{\-\}labels\}\(c\)&\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\mathsf\{forall\}\\ \(\\lambda d\.&\\text\{\\small Stored value not behind any previously\}\\\\ \\phantom\{X\}\\ \\ \\ \\ \\neg\(\(d^\{\\prime\}\|\_\{k\}\\cup\\\{\\langle c^\{\\prime\},t^\{\\prime\},k,\\mathit\{label\}\(v^\{\\prime\}\)\\rangle\\\}\)\|\_\{L\}\\subset d\)\)\\ G&\\text\{\\small read value, for client's labels\.\}\\\\ \\phantom\{X\}\\wedge\\ c=c^\{\\prime\}\\Rightarrow p\\subseteq d^\{\\prime\}\|\_\{k\}\\cup\\\{\\langle c^\{\\prime\},t^\{\\prime\},k,\\mathit\{label\}\(v^\{\\prime\}\)\\rangle\\\}&\\text\{\\small Read your writes\.\}\\\\ \\mathsf\{get\}\\ \(k\)\(\\\_\)\(\\\_,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Get\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle v,c,t,d\\rangle\\leftarrow\\varsigma\(k\)&\\\\ \\phantom\{X\}\\mathsf\{let\}\\ d^\{\\prime\}\\leftarrow\\mathsf\{if\}\\ \(c\\neq c\_\{0\}\)\\ d\\cup\\\{\\langle c,t,k,\\mathit\{label\}\(v\)\\rangle\\\}\\ \\mathsf\{else\}\\ \\emptyset&\\text\{\\small Label of stored value included in returned dependency\.\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle v,d^\{\\prime\},\\varsigma\\rangle&\\text\{\\small\}\\\\ \\mathsf\{get\\text\{\-\}res\}\\ \(\\\_,\\\_\)\(d^\{\\prime\}\)\(\\\_,\\langle p,G\\rangle\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Get Response\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle p,G\\cup\\\{d^\{\\prime\}\\\}\\rangle&\\text\{\\small Received dependencies added to session\.\}\\\\ &\\\\ \\mathsf\{Put\\text\{\-\}req\\text\{\-\}payload\}\\coloneqq T\\times\\mathsf\{Set\}\[C\\times T\\times K\\times L\]&\\text\{\\small Put payload types\}\\\\ \\mathsf\{put\\text\{\-\}req\}\\ \(k,v\)\(\\mathit\{self\},\\langle p,G\\rangle\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Put Request\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ t\\leftarrow\|p\|\+1&\\text\{\\small Current put timestamp\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ p^\{\\prime\}\\leftarrow p\\cup\\\{\\langle\\mathit\{self\},t,k,\\mathit\{label\}\(v\)\\rangle\\\}&\\text\{\\small Put with its label added to session dependencies\.\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle\\langle t,p\\cup\(\\bigcup\\,G\)\\rangle,\\langle p^\{\\prime\},G\\rangle\\rangle&\\text\{\\small All session dependencies sent as request payload\.\}\\\\ \\mathsf\{put\\text\{\-\}guard\}\\ \(k,v\)\(\\langle t,\\\_\\rangle\)\(c,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Put Guard\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle\\\_,\\\_,\\\_,d^\{\\prime\}\\rangle\\leftarrow\\varsigma\(k\)&\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle c,t,k,\\mathit\{label\}\(v\)\\rangle\\not\\in d^\{\\prime\}&\\text\{\\small The new put has not already been applied\.\}\\\\ \\mathsf\{put\}\\ \(k,v\)\(\\langle t,d\\rangle\)\(c,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Put\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\varsigma\[k\\mapsto\\langle v,c,t,d\\rangle\]&\\\\ &\\\\ d\|\_\{k\}\\coloneqq\\\{\\langle c,t,k,l\\rangle\\ \|\\ \\langle c,t,k^\{\\prime\},l\\rangle\\in d\\wedge k=k^\{\\prime\}\\\}&\\\\ D\|\_\{k\}\\coloneqq\\\{d\|\_\{k\}\\ \|\\ d\\in D\\\}&\\\\ d\|\_\{L\}\\coloneqq\\\{\\langle c,t,k,l\\rangle\\ \|\\ \\langle c,t,k,l\\rangle\\in d\\wedge l\\in L\\\}&\\text\{\\small Filter dependencies to the label set $L$\}\\\\ D\|\_\{L\}\\coloneqq\\\{d\|\_\{L\}\\ \|\\ d\\in D\\\}&\\\\ \\hline\\cr\\end\{array\}Figure 24:Labeled Causal Consistency Spec\. Causal consistency — but per topic\. Every put is tagged with a label \(think: Kafka topic, Slack channel, pub/sub subject\)\. Every client declares which labels it cares about\. Causal delivery for a client is enforced only for labels the client is interested in\.𝕀𝐶𝐶1​\(Causal Consistency Implementation 1\)T≔𝖭𝖺𝗍Timestamp𝖢𝖲𝗍𝖺𝗍𝖾≔Client StateC↦TSession vector\-clock𝖼​\-​𝗂𝗇𝗂𝗍​\(c\)≔Client Initial State\[c↦0¯\]No initial dependencies𝖱𝖲𝗍𝖺𝗍𝖾≔Replica State⟨K↦V,StoreC↦T⟩Received vector\-clock \(one for all keys\)𝗋​\-​𝗂𝗇𝗂𝗍​\(r,v0\)≔Replica Initial State⟨\[k↦v0¯\],\[c↦0¯\]⟩Empty initial dependencies𝖦𝖾𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔C↦TGet payload types𝖦𝖾𝗍​\-​𝗋𝖾𝗌​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔C↦T𝗀𝖾𝗍​\-​𝗋𝖾𝗊​\(\_\)​\(\_,d\)≔At client:Get Request𝗋𝖾𝗍​⟨d,d⟩Session vector\-clock \(1\) sent as request payload \(2\) remains unchanged𝗀𝖾𝗍​\-​𝗀𝗎𝖺𝗋𝖽​\(k\)​\(d\)​\(\_,\_,ς\)≔At replica:Get Guard𝗅𝖾𝗍​⟨\_,r⟩←ς𝗋𝖾𝗍​r≥dPointwise comparison of vector clocks\. Store is ahead of session𝗀𝖾𝗍​\(k\)​\(\_\)​\(\_,\_,ς\)≔At replica:Get𝗅𝖾𝗍​⟨s,r⟩←ς𝗅𝖾𝗍​v←s​\(k\)𝗋𝖾𝗍​⟨v,r,ς⟩𝗀𝖾𝗍​\-​𝗋𝖾𝗌​\(\_,\_\)​\(r\)​\(\_,d\)≔At client:Get Response𝗋𝖾𝗍​𝗆𝖺𝗑​\(d,r\)Pointwise max of vector\-clocks𝖯𝗎𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔C↦TPut payload types𝗉𝗎𝗍​\-​𝗋𝖾𝗊​\(\_,\_\)​\(𝑠𝑒𝑙𝑓,d\)≔At client:Put Request𝗅𝖾𝗍​d′←d​\[𝑠𝑒𝑙𝑓↦d​\(𝑠𝑒𝑙𝑓\)\+1\]Session dependencies advanced\.𝗋𝖾𝗍​⟨d,d′⟩Session vector\-clock is sent as request payload\.𝗉𝗎𝗍​\-​𝗀𝗎𝖺𝗋𝖽​\(\_,\_\)​\(d\)​\(c,\_,ς\)≔At replica:Put Guard𝗅𝖾𝗍​⟨\_,r⟩←ς𝗋𝖾𝗍​r≥d∧r​\(c\)=d​\(c\)Store satisfies the dependencies\. The new put advances the store\.𝗉𝗎𝗍​\(k,v\)​\(d\)​\(c,\_,ς\)≔At replica:Put𝗅𝖾𝗍​⟨s,r⟩←ς𝗅𝖾𝗍​r′←r​\[c↦d​\(c\)\+1\]Received advanceds′←s​\[k↦v\]𝗋𝖾𝗍​⟨s′,r′⟩\\displaystyle\\begin\{array\}\[\]\{\|lr\|\}\\hline\\cr\\vrule\\lx@intercol\\mathbb\{I\}\_\{\\mathit\{CC\}\_\{1\}\}\\ \(\\textsc\{Causal Consistency Implementation 1\}\)\\hfil\\lx@intercol\\vrule\\lx@intercol\\\\ \\hline\\cr T\\coloneqq\\mathsf\{Nat\}&\\text\{\\small Timestamp\}\\\\ \\mathsf\{CState\}\\coloneqq&\\textbf\{\\small Client State\}\\\\ \\phantom\{X\}C\\mapsto T&\\text\{\\small Session vector\-clock\}\\\\ \\mathsf\{c\\text\{\-\}init\}\(c\)\\coloneqq&\\textbf\{\\small Client Initial State\}\\\\ \\phantom\{X\}\[\\overline\{c\\mapsto 0\}\]&\\text\{\\small No initial dependencies\}\\\\ \\mathsf\{RState\}\\coloneqq&\\textbf\{\\small Replica State\}\\\\ \\phantom\{X\}\\langle K\\mapsto V,&\\text\{\\small Store\}\\\\ \\phantom\{X\}\\phantom\{\\langle\}C\\mapsto T\\rangle&\\text\{\\small Received vector\-clock \(one for all keys\)\}\\\\ \\mathsf\{r\\text\{\-\}init\}\(r,v\_\{0\}\)\\coloneqq&\\textbf\{\\small Replica Initial State\}\\\\ \\phantom\{X\}\\langle\[\\overline\{k\\mapsto v\_\{0\}\}\],\[\\overline\{c\\mapsto 0\}\]\\rangle&\\text\{\\small Empty initial dependencies\}\\\\ &\\\\ \\mathsf\{Get\\text\{\-\}req\\text\{\-\}payload\}\\coloneqq C\\mapsto T&\\text\{\\small Get payload types\}\\\\ \\mathsf\{Get\\text\{\-\}res\\text\{\-\}payload\}\\coloneqq C\\mapsto T&\\\\ \\mathsf\{get\\text\{\-\}req\}\\ \(\\\_\)\(\\\_,d\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Get Request\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle d,d\\rangle&\\text\{\\small Session vector\-clock \(1\) sent as request payload \(2\) remains unchanged\}\\\\ \\mathsf\{get\\text\{\-\}guard\}\\ \(k\)\(d\)\(\\\_,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Get Guard\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle\\\_,r\\rangle\\leftarrow\\varsigma&\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ r\\geq d&\\text\{\\small Pointwise comparison of vector clocks\. Store is ahead of session\}\\\\ \\mathsf\{get\}\\ \(k\)\(\\\_\)\(\\\_,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Get\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle s,r\\rangle\\leftarrow\\varsigma&\\\\ \\phantom\{X\}\\mathsf\{let\}\\ v\\leftarrow s\(k\)&\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle v,r,\\varsigma\\rangle&\\text\{\\small\}\\\\ \\mathsf\{get\\text\{\-\}res\}\\ \(\\\_,\\\_\)\(r\)\(\\\_,d\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Get Response\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\mathsf\{max\}\(d,r\)&\\text\{\\small Pointwise max of vector\-clocks\}\\\\ &\\\\ \\mathsf\{Put\\text\{\-\}req\\text\{\-\}payload\}\\coloneqq C\\mapsto T&\\text\{\\small Put payload types\}\\\\ \\mathsf\{put\\text\{\-\}req\}\\ \(\\\_,\\\_\)\(\\mathit\{self\},d\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Put Request\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ d^\{\\prime\}\\leftarrow d\[\\mathit\{self\}\\mapsto d\(\\mathit\{self\}\)\+1\]&\\text\{\\small Session dependencies advanced\.\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle d,d^\{\\prime\}\\rangle&\\text\{\\small Session vector\-clock is sent as request payload\.\}\\\\ \\mathsf\{put\\text\{\-\}guard\}\\ \(\\\_,\\\_\)\(d\)\(c,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Put Guard\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle\\\_,r\\rangle\\leftarrow\\varsigma&\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ r\\geq d\\,\\wedge\\,r\(c\)=d\(c\)&\\text\{\\small Store satisfies the dependencies\. The new put advances the store\.\}\\\\ \\mathsf\{put\}\\ \(k,v\)\(d\)\(c,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Put\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle s,r\\rangle\\leftarrow\\varsigma&\\\\ \\phantom\{X\}\\mathsf\{let\}\\ r^\{\\prime\}\\leftarrow r\[c\\mapsto d\(c\)\+1\]&\\text\{\\small Received advanced\}\\\\ \\phantom\{X\}s^\{\\prime\}\\leftarrow s\[k\\mapsto v\]&\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle s^\{\\prime\},r^\{\\prime\}\\rangle&\\\\ \\hline\\cr\\end\{array\}
Figure 25:Causal Consistency Implementation 1 \(Inspired byAhamadet al\.\([1995](https://arxiv.org/html/2605.23109#bib.bib127)\)\)\.𝕀𝐶𝐶2​\(Causal Consistency Implementation 2\)T≔𝖭𝖺𝗍Timestamp𝖢𝖲𝗍𝖺𝗍𝖾≔Client StateT×𝖫𝗂𝗌𝗍​\[C×T\]Put timestamp, and Session dependencies𝖼​\-​𝗂𝗇𝗂𝗍​\(c\)≔Client Initial State⟨0,∅⟩Timestamp zero\. No initial dependencies\.𝖱𝖲𝗍𝖺𝗍𝖾≔Replica State⟨K↦C×T×V,Store \(C×Tuniquely identifies puts\.\)C↦T⟩Received vector\-clock𝗋​\-​𝗂𝗇𝗂𝗍​\(r,v0\)≔Replica Initial State⟨\[k↦⟨c0,0,v0⟩¯\],\[c↦0¯\]⟩Nothing initially received𝖦𝖾𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔𝖫𝗂𝗌𝗍​\[C×T\]Get payload types𝖦𝖾𝗍​\-​𝗋𝖾𝗌​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔C×T𝗀𝖾𝗍​\-​𝗋𝖾𝗊​\(\_\)​\(\_,σ\)≔At client:Get Request𝗅𝖾𝗍​⟨\_,d⟩←σ𝗋𝖾𝗍​⟨d,σ⟩Session dependencies sent as request payload𝗀𝖾𝗍​\-​𝗀𝗎𝖺𝗋𝖽​\(\_\)​\(d\)​\(\_,\_,ς\)≔At replica:Get Guard𝗅𝖾𝗍​⟨\_,r⟩←ς𝗋𝖾𝗍𝖿𝗈𝗋𝖺𝗅𝗅\(λ\(c,t\)\.r\(c\)≥t\)dStore satisfies the dependencies𝗀𝖾𝗍​\(k\)​\(\_\)​\(\_,\_,ς\)≔At replica:Get𝗅𝖾𝗍​⟨s,\_⟩←ς𝗅𝖾𝗍​⟨c,t,v⟩←ς​\(k\)𝗋𝖾𝗍​⟨v,⟨c,t⟩,ς⟩𝗀𝖾𝗍​\-​𝗋𝖾𝗌​\(\_,\_\)​\(⟨c,t⟩\)​\(\_,σ\)≔At client:Get Response𝗅𝖾𝗍​⟨t′,d⟩←σ𝗅𝖾𝗍d′←d::⟨c,t⟩𝗋𝖾𝗍​⟨t′,d′⟩𝖯𝗎𝗍​\-​𝗋𝖾𝗊​\-​𝗉𝖺𝗒𝗅𝗈𝖺𝖽≔𝖫𝗂𝗌𝗍​\[C×T\]Put payload types𝗉𝗎𝗍​\-​𝗋𝖾𝗊​\(\_,\_\)​\(c,σ\)≔At client:Put Request𝗅𝖾𝗍​⟨t,d⟩←σ𝗅𝖾𝗍​t′←t\+1𝗅𝖾𝗍​d′←\[⟨c,t′⟩\]𝗋𝖾𝗍​⟨d,⟨t′,d′⟩⟩Session dependencies sent as request payload\.𝗉𝗎𝗍​\-​𝗀𝗎𝖺𝗋𝖽​\(\_,\_\)​\(d\)​\(c,\_,ς\)≔At replica:Put Guard𝗅𝖾𝗍​⟨\_,r⟩←ς𝗋𝖾𝗍𝖿𝗈𝗋𝖺𝗅𝗅\(λ\(c,t\)\.r\(c\)≥t\)dStore satisfies the dependencies𝗅𝗈𝗈𝗄𝗎𝗉​\(c,d,0\)=r​\(c\)The new put advances the store𝗉𝗎𝗍​\(k,v\)​\(\_\)​\(c,\_,ς\)≔At replica:Put𝗅𝖾𝗍​⟨s,r⟩←ς𝗅𝖾𝗍​t←r​\(c\)\+1Current put timestamp𝗅𝖾𝗍​r′←r​\[c↦t\]s′←s​\[k↦⟨c,t,v⟩\]𝗋𝖾𝗍​⟨s′,r′⟩\\displaystyle\\begin\{array\}\[\]\{\|lr\|\}\\hline\\cr\\vrule\\lx@intercol\\mathbb\{I\}\_\{\\mathit\{CC\}\_\{2\}\}\\ \(\\textsc\{Causal Consistency Implementation 2\}\)\\hfil\\lx@intercol\\vrule\\lx@intercol\\\\ \\hline\\cr T\\coloneqq\\mathsf\{Nat\}&\\text\{\\small Timestamp\}\\\\ \\mathsf\{CState\}\\coloneqq&\\textbf\{\\small Client State\}\\\\ \\phantom\{X\}T\\times\\mathsf\{List\}\[C\\times T\]&\\text\{\\small Put timestamp, and Session dependencies\}\\\\ \\mathsf\{c\\text\{\-\}init\}\(c\)\\coloneqq&\\textbf\{\\small Client Initial State\}\\\\ \\phantom\{X\}\\langle 0,\\emptyset\\rangle&\\text\{\\small Timestamp zero\. No initial dependencies\.\}\\\\ \\mathsf\{RState\}\\coloneqq&\\textbf\{\\small Replica State\}\\\\ \\phantom\{X\}\\langle K\\mapsto C\\times T\\times V,&\\text\{\\small Store \($C\\times T$ uniquely identifies puts\.\)\}\\\\ \\phantom\{X\}\\phantom\{\\langle\}C\\mapsto T\\rangle&\\text\{\\small Received vector\-clock\}\\\\ \\mathsf\{r\\text\{\-\}init\}\(r,v\_\{0\}\)\\coloneqq&\\textbf\{\\small Replica Initial State\}\\\\ \\phantom\{X\}\\langle\[\\overline\{k\\mapsto\\langle c\_\{0\},0,v\_\{0\}\\rangle\}\],\[\\overline\{c\\mapsto 0\}\]\\rangle&\\text\{\\small Nothing initially received\}\\\\ &\\\\ \\mathsf\{Get\\text\{\-\}req\\text\{\-\}payload\}\\coloneqq\\mathsf\{List\}\[C\\times T\]&\\text\{\\small Get payload types\}\\\\ \\mathsf\{Get\\text\{\-\}res\\text\{\-\}payload\}\\coloneqq C\\times T&\\\\ \\mathsf\{get\\text\{\-\}req\}\\ \(\\\_\)\(\\\_,\\sigma\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Get Request\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle\\\_,d\\rangle\\leftarrow\\sigma&\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle d,\\sigma\\rangle&\\text\{\\small Session dependencies sent as request payload\}\\\\ \\mathsf\{get\\text\{\-\}guard\}\\ \(\\\_\)\(d\)\(\\\_,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Get Guard\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle\\\_,r\\rangle\\leftarrow\\varsigma&\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\mathsf\{forall\}\\ \(\\lambda\(c,t\)\.\\ r\(c\)\\geq t\)\\ d&\\text\{\\small Store satisfies the dependencies\}\\\\ \\mathsf\{get\}\\ \(k\)\(\\\_\)\(\\\_,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Get\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle s,\\\_\\rangle\\leftarrow\\varsigma&\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle c,t,v\\rangle\\leftarrow\\varsigma\(k\)&\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle v,\\langle c,t\\rangle,\\varsigma\\rangle&\\text\{\\small\}\\\\ \\mathsf\{get\\text\{\-\}res\}\\ \(\\\_,\\\_\)\(\\langle c,t\\rangle\)\(\\\_,\\sigma\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Get Response\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle t^\{\\prime\},d\\rangle\\leftarrow\\sigma&\\text\{\\small\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ d^\{\\prime\}\\leftarrow d::\\langle c,t\\rangle&\\text\{\\small\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle t^\{\\prime\},d^\{\\prime\}\\rangle&\\text\{\\small\}\\\\ &\\\\ \\mathsf\{Put\\text\{\-\}req\\text\{\-\}payload\}\\coloneqq\\mathsf\{List\}\[C\\times T\]&\\text\{\\small Put payload types\}\\\\ \\mathsf\{put\\text\{\-\}req\}\\ \(\\\_,\\\_\)\(c,\\sigma\)\\coloneqq&\\text\{\\small At client: \}\\textbf\{\\small Put Request\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle t,d\\rangle\\leftarrow\\sigma&\\text\{\\small\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ t^\{\\prime\}\\leftarrow t\+1&\\text\{\\small\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ d^\{\\prime\}\\leftarrow\[\\langle c,t^\{\\prime\}\\rangle\]&\\text\{\\small\}\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle d,\\langle t^\{\\prime\},d^\{\\prime\}\\rangle\\rangle&\\text\{\\small Session dependencies sent as request payload\.\}\\\\ \\mathsf\{put\\text\{\-\}guard\}\\ \(\\\_,\\\_\)\(d\)\(c,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Put Guard\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle\\\_,r\\rangle\\leftarrow\\varsigma&\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\mathsf\{forall\}\\ \(\\lambda\(c,t\)\.\\ r\(c\)\\geq t\)\\ d&\\text\{\\small Store satisfies the dependencies\}\\\\ \\phantom\{X\}\\phantom\{\\mathsf\{ret\}\\ \}\\mathsf\{lookup\}\\ \(c,d,0\)=r\(c\)&\\text\{\\small The new put advances the store\}\\\\ \\mathsf\{put\}\\ \(k,v\)\(\\\_\)\(c,\\\_,\\varsigma\)\\coloneqq&\\text\{\\small At replica: \}\\textbf\{\\small Put\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ \\langle s,r\\rangle\\leftarrow\\varsigma&\\text\{\\small\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ t\\leftarrow r\(c\)\+1&\\text\{\\small Current put timestamp\}\\\\ \\phantom\{X\}\\mathsf\{let\}\\ r^\{\\prime\}\\leftarrow r\[c\\mapsto t\]&\\text\{\\small\}\\\\ \\phantom\{X\}s^\{\\prime\}\\leftarrow s\[k\\mapsto\\langle c,t,v\\rangle\]&\\\\ \\phantom\{X\}\\mathsf\{ret\}\\ \\langle s^\{\\prime\},r^\{\\prime\}\\rangle&\\\\ \\hline\\cr\\end\{array\}Figure 26:Causal Consistency Implementation 2 \(Inspired byLloydet al\.\([2013](https://arxiv.org/html/2605.23109#bib.bib135)\)\)\.
### I\.6Chapar Causal Consistency

For Chapar CC we use Chapar’s published causal\-consistency specificationLesaniet al\.\([2016](https://arxiv.org/html/2605.23109#bib.bib6)\); we refer the reader to the original paper for its formal definition\. Per\-operation cost comparison appears in[appendix˜D](https://arxiv.org/html/2605.23109#A4)\.