sal: Multi-modal Verification of Replicated Data Types

Sal is a Lean 4 framework for verifying state-based CRDTs and Mergeable Replicated Data Types (MRDTs) under replication-aware (RA) linearizability. Rather than discharging every verification condition with a single backend, Sal stages automation by trustworthiness: it first attempts kernel-verified proof reconstruction, falls back to an SMT backend only when that fails, and finally hands remaining obligations to an AI-assisted interactive theorem prover — all while keeping the trusted computing base (TCB) as small as the VC allows. When a VC is in fact invalid, Sal uses Plausible (property-based testing) together with a ProofWidgets-based visualizer to turn the failure into an inspectable counterexample execution trace.

The approach builds on the F★-based Neem framework of Soundarapandian, Nagar, Rastogi, and Sivaramakrishnan (OOPSLA 2025), which reduces RA-linearizability for a data type to a fixed set of VCs over do, merge, and rc. Sal is the Lean port of that reduction plus a multi-modal tactic, counterexample pipeline, and custom decidable set/map interfaces that make grind effective on RDT goals.

What's verified

The suite currently contains 29 RDTs — 17 CRDTs and 12 MRDTs — with all 24 RA-linearizability VCs closed on every RDT the standard VC schema applies to. Two MRDTs sit outside that count for different reasons: Enable_Wins_Flag_known_broken is an intentionally-buggy demo fixture, and the tombstone-free RGA is provably outside the schema (its commutation only holds conditioned on reachable states) — it instead carries a direct, kernel-checked end-to-end theorem: RA-linearizability up to observational equivalence at every reachable configuration, under an honest-delivery assumption (see the metatheory entry below). That's 648 VCs for state convergence (27 × 24), of which the vast majority are kernel-checked (no TCB-enlarging admits) and a small residue of stage-2 Blaster-admits remain in a few files (OR_Set_MRDT, OR_Set_Efficient_MRDT, Add_Win_Priority_Queue_MRDT, Multi_Valued_Register_MRDT) — validated by Z3 via the sal tactic's SMT stage but not yet kernel-reconstructed.

Every RDT carries a *_ReadSide.lean companion (and a *_SPOT.lean of small concrete-execution tests) alongside its *_CRDT.lean / *_MRDT.lean. The Tier-C RDTs (Peritext, RGA, Add_Win_Priority_Queue, OR_Set plain and efficient, Multi_Valued_Register, LWW_Element_Set) carry substantive intent-preservation theorems matching paper claims; the Tier-A RDTs carry mechanical 30–60 line files documenting the obvious read so a reader can confirm at a glance that it is in fact obvious. Per-RDT crosswalks for the Tier-C papers:

• docs/peritext-vs-paper.md — Litt et al. CSCW 2022, Ex 1 / 2 / 3 / 5 / 7 / 8 intent-preservation.
• docs/rga-vs-paper.md — Roh et al. JPDC 2011, causal-order preservation, tombstone monotonicity, deterministic concurrent-insert tiebreak.
• docs/aw-crpq-vs-paper.md — Zhang et al. Internetware 2023, Add-wins headline + LWW innate + acquired-Σ + get_max.
• docs/or-set-vs-paper.md — Shapiro et al. INRIA RR-7506, Add-Wins on lookup with sequential-Add-then-Remove extinguishment.
• docs/mvr-vs-paper.md — Shapiro et al. INRIA RR-7506 §3.2.2, classical replace-on-write semantics with concurrent-writes-both-survive + sequential-writes-supersede.
• docs/lww-element-set-vs-paper.md — Shapiro et al. INRIA RR-7506 §3.3.4, LWW-comparison lookup with lookup_after_add_with_fresh_ts + remove_at_higher_ts_extinguishes.

The methodology — the Tier-A/B/C distinction, when read-sides are needed, the snapshot-in-op-payload pattern, and the spec-validation lesson from in_span_boundary — is documented in docs/readside-projections.md.

Everything is checked on Lean v4.28.0 against the chore-bump-lean-4.28 branch of a Blaster fork.

CRDTs (Sal/CRDTs/)

Registers & counters:

• Increment_Only_Counter
• PN_Counter
• LWW_Register
• MAX_Register
• MIN_Register
• Multi_Valued_Register — classical replace-on-write MVR via the snapshot-in-op-payload trick (Shapiro et al. INRIA RR-7506 §3.2.2). State (writes, removed); concurrent writes survive via additive merge, sequential writes overwrite via the snapshot. + read-side: is_visible_value, concurrent_writes_both_visible, sequential_write_supersedes. See docs/mvr-vs-paper.md.
• Bounded_Counter — Sypytkowski 2019 / Balegas et al. 2015. PN-counter plus a sparse per-replica-pair transfers map for quota redistribution.

Sets & maps:

• OR_Set — Shapiro et al. INRIA RR-7506. + read-side: lookup, add_wins_over_concurrent_remove, add_then_remove_extinguishes. See docs/or-set-vs-paper.md.
• Grow_Only_Set
• Grow_Only_Multiset
• LWW_Element_Set — Shapiro et al. INRIA RR-7506. Per-element latest-add-ts and latest-remove-ts maps; lookup uses strict-> comparison (remove-wins on tie). + read-side: lookup_after_add_with_fresh_ts, remove_at_higher_ts_extinguishes (independent intent theorems); lookup_def (definitional unfolding of lookup, not a behavioural guarantee — renamed from latest_write_wins, which overstated it). See docs/lww-element-set-vs-paper.md.
• LWW_Map
• MAX_Map

Sequences & structured data:

• RGA — Replicated Growable Array, the sequence CRDT underlying Automerge / Yjs, in its state-based formulation as a grow-only Map OpId (char, afterId, deleted). + read-side: visible_lt four-rule DFS-traversal predicate, causal_order_visible_lt, tombstone_monotone_under_remove, concurrent_insert_tiebreak_deterministic. See docs/rga-vs-paper.md.
• Peritext — Litt et al. CSCW 2022. Rich text = RGA + formatting marks represented as a flat set AnchorAttachment. + read-side: paper Ex 1 / 2 / 3 / 5 / 7 / 8 intent-preservation theorems (kernel-checked, mirrored on the MRDT side). See docs/peritext-vs-paper.md.
• Shopping_Cart
• Add_Win_Priority_Queue — adapted from Zhang et al. 2023. + read-side: lookup, add_wins_over_concurrent_rmv, LWW innate, MCW-collapsed-to-Σ acquired, get_max, inc_increases_acquired. See docs/aw-crpq-vs-paper.md.

MRDTs (Sal/MRDTs/)

• Increment_Only_Counter
• PN_Counter
• Multi_Valued_Register — classical MVR with the same (writes, removed) shape as the CRDT but standard three-way merge per component. + read-side (mirrors the CRDT side). See docs/mvr-vs-paper.md.
• Grow_Only_Set
• Grow_Only_Map
• OR_Set — + read-side (mirrors the CRDT side via three-way merge). See docs/or-set-vs-paper.md.
• OR_Set_Efficient — compressed variant with (rid, ts, elem) triples and per-replica deduplication. + read-side with the same headline theorems on the triple representation.
• Replicated_Growable_Array — the tombstoned MRDT RGA (Sal/MRDTs/RGA_with_tombstones/). + read-side with relational readSeq_visible and the three RGA intent theorems. See docs/rga-vs-paper.md.
• RGA_Tombstone_Free — the rehoming RGA (Sal/MRDTs/RGA_Rehoming/; formerly holding the plain name RGA/, demoted 2026-07-16): the tombstone-free, path-carrying RGA: deletes really remove (no tombstone set); each op carries its target's recorded ancestor path, and merge rehomes survivors along it. Status: its convergence capstone is sound, but its do is sequential-spec-refuted — deleting an interior node reorders survivors on a single replica (tombstone_free_violates_delete_order, and in campaign form rehoming_seq_refuted), so it does not implement the naive text buffer. Retained as the framework's generality stress test and the delete-order countermodel; the recommended sequence datatype is the embedded-chain family (RGA_Embed/EmbedRGA, seq-spec-sound and read-equal to the published RGA). Provably outside the standard 24-VC schema (commutation is reachability-conditioned, and a prefix-free variant is impossible — RGA_PrefixFree_Impossible.lean); verified instead by a direct end-to-end theorem, rga_ra_linearizable3_eq: RA-linearizability up to observational ≈ at every reachable configuration under honest delivery, via the applicability-conditioned metatheory (Sal/ConditionedMRDTs/MRDT_Instances/RGA_Rehoming/RA_Lin.lean). An eq-variant (RGA_Tombstone_Free_Eq_MRDT.lean) shows the ≈ is purely representational: a normalizing delete pins ghost payloads to the default, on normal forms the observational equivalence is structural equality, and the variant's folds are the normal forms of the original's. See Sal/MRDTs/RGA_Rehoming/doc/why-the-path-matters.pdf.
• Add_Win_Priority_Queue — adapted from Zhang et al. 2023. Drops the CRDT's tombstone set since the LCA handles Add-Wins directly, leaving set (add_ts, elem, value) × set (inc_ts, elem, amount). + read-side. See docs/aw-crpq-vs-paper.md.
• Peritext — Litt et al. CSCW 2022. RGA substrate plus set AnchorAttachment. RGA's tombstones are structurally load-bearing (later inserts reference earlier char ids), so this MRDT keeps all components grow-only and uses pointwise-union merge, mirroring RGA_MRDT. + read-side: the kernel-checked paper Ex 1 / 2 / 3 / 5 / 7 / 8 intent-preservation theorems (Sal/MRDTs/Peritext_with_tombstones/Peritext_ReadSide.lean). See docs/peritext-vs-paper.md.
• Enable_Wins_Flag — enable-wins boolean flag, per-replica map of (counter, flag).
• Enable_Wins_Flag_known_broken — intentionally buggy variant preserved as a demo fixture. Drives the Plausible counterexample demo; the bug manifests on inter_right_1op.

The sal tactic

The tactic lives in Sal/Tactic/Sal.lean and tries three strategies in order, stopping at the first one that succeeds:

1. dsimp + grind — lightweight SMT-style automation with proof reconstruction; the result is a kernel-checkable proof term. This stage is preferred because it does not enlarge the TCB. We deliberately skip aesop at this stage because its verification times on these RDT goals were prohibitive.
2. lean-blaster — encodes the goal to Z3. More powerful (especially for higher-order functions and lambdas) but sacrifices proof reconstruction, so the TCB grows to include the SMT solver. Invoked with a wall-clock timeout (default 30 s) so a stuck goal cannot hang.
3. dsimp + aesop + all_goals (try grind) — a broader proof-search fallback. Remaining goals are then typically closed interactively with tactics produced by Harmonic's Aristotle, whose outputs are kernel-checked so the TCB is still not enlarged.

Stages 1 and 3 are guarded against sorryAx in the resulting proof term: aesop's default mode can otherwise close a goal with a silent sorry placeholder. Stage 2 is intentionally not guarded, because Blaster trusts Z3's "valid" verdict via MVarId.admit — that is Blaster's TCB-enlarging mechanism.

The tactic takes a heartbeat budget (default 400 000) that caps Lean-side elaboration across all three stages, and a separate smtTimeoutSec budget (default 30 s) for the SMT stage. See the docstring in Sal.lean for how to tune them.

Minimal example (see Sal/Tactic/SalExample.lean for more):

import Sal.Tactic.Sal

example (a b : Nat) : a + b = b + a := by sal

Many post-paper CRDTs in the suite are proved with a uniform kernel-verifiable pattern — rcases over the operation family, refine ⟨?_, …, ?_⟩ to split the state's components, then simp +decide [*] and grind — and avoid Blaster entirely. A few stubborn VCs still need Blaster or an Aristotle-assisted intermediate lemma (e.g. LWW_Map_CRDT uses merge_do_lex_max); those calls stay inside the three-stage pipeline. For the full recipe of translating an op-based CRDT into Sal's state-based signature and closing the 24 VCs, see docs/porting-op-based-crdts.md.

Custom set and map interfaces

Lean's standard Set α := α → Prop is convenient for hand-written proofs but fights automation (membership is a proposition, not a Boolean). Sal introduces decidable versions where grind can compute:

abbrev set (a : Type) [DecidableEq a] := a → Bool

structure map (key : Type) [DecidableEq key] (value : Type) where
  mappings : key → value
  domain   : set key

Every lemma on these types is annotated with @[simp, grind] and (where useful) a grind_pattern, building a domain-specific rewrite database that lets grind discharge set/map goals without SMT assistance. Files live in Sal/Interfaces/.

The Boolean-predicate representation is grind-friendly only as a top-level state component. Nesting a set inside a map value — e.g. map K (set V) — forces grind to prove function equality via funext and typically defeats it. Where possible, flatten: represent map K (set V) as set (K × V). The Peritext CRDT is the clearest example in the suite: its formatting marks were originally a map (OpId × Bool) (set MarkOp), which left 5 of 24 VCs stuck; flattening to a top-level set AnchorAttachment closes all 24.

Counterexample generation and visualization

When automation fails because the implementation is actually wrong, Sal makes the failure inspectable rather than opaque:

• Plausible generates concrete counterexamples for decidable VCs. The canonical demo is the Enable-Wins Flag MRDT, which contains a known bug from prior work (the inter_right_1op VC fails); Plausible rediscovers a minimal failing execution automatically. See Sal/Counterexample_Visualization/WriterMonad_Enable_Wins_Flag.lean.
• ProofWidgets trace visualizer. A logging-style writer monad instruments do and merge to record intermediate states, and a ProofWidgets component renders the LCA, left branch, right branch, and merge result as a vertical diagram. See Sal/Counterexample_Visualization/.
• Universe tracking for functional sets. Since Sal's set type is a α → Bool predicate and may be infinite, the visualizer augments abstract sets with a concrete HashSet of elements added or removed during execution, so the state can be displayed concretely.

Steps to run

Clone this repository, then install elan (the Lean toolchain manager). elan will read lean-toolchain and install Lean v4.28.0 on first use. From the repo root, run lake exe cache get to download the prebuilt Mathlib oleans — this takes a few minutes and is required before any file will type-check in a reasonable time.

lake update is safe to run — lakefile.toml pins mathlib to v4.28.0 and pins Blaster to the chore-bump-lean-4.28 branch of kayceesrk/Lean-blaster, a fork whose upstream (input-output-hk/Lean-blaster) does not yet have a v4.28-compatible branch. Once the upstream catches up we will switch back.

Open each Lean file in VS Code to run the verification conditions interactively, or run lake lean <path-to-file.lean> from the command line. The run_files.sh script checks every .lean file under a given directory.

Interactive playgrounds

Browser demos live in demos/ (Vite + React + TypeScript, one hand-ported module per RDT). 28 of the 29 RDTs have a playground — 17 CRDTs + 11 MRDTs (the tombstone-free RGA does not have one yet).

• CRDT playgrounds spin up three replicas, let you apply local ops per replica, and merge any pair directionally (source → target, like git merge). There's also a "Merge all" button that folds every replica's state into a single join and assigns it back, so you can watch replicas snap to the same value in one click. Toggle Show concrete state to expose the lattice representation.
• MRDT playgrounds organise history like git. Every local op creates a 1-parent commit; every merge creates a 2-parent commit with the LCA computed from the DAG (BFS on ancestors). A toggleable SVG history graph shows per-replica lanes with colour-coded commits (op commits solid, merge commits dashed, HEADs ringed thicker); click any past commit to inspect its full state.
• Lattice-law invariants are property-checked with fast-check per RDT: CRDTs get idempotence / commutativity / associativity / strong convergence; MRDTs get left identity / right identity / commutativity (the MRDT merge(l,a,a) ~ a analog is NOT a law — the closed-form counter MRDT violates it by design; MRDTs only promise convergence given a coherent history DAG, which the playground supplies at runtime).

cd demos
npm install
npm run dev       # http://localhost:5173
npm run test      # 28 fast-check suites, ~1.5 s
npm run build     # TS + Vite production bundle

See demos/README.md for the CRDTSpec / MRDTSpec interfaces, file layout, and deployment. .github/workflows/demos-deploy.yml publishes to GitHub Pages on every push to main that touches demos/**.

Repository layout

• Sal/Interfaces/ — Sal's decidable set and map interfaces (Set_Extended, Map_Extended, Map_Extended_With_Lean_Set).

• Sal/Tactic/ — the sal tactic (Sal.lean) and usage examples (SalExample.lean).

• Sal/CRDTs/ — 17 state-based CRDTs in the ⟨Σ, σ₀, do, merge, rc⟩ signature.

• Sal/MRDTs/ — 12 state-based MRDTs.

• Sal/Counterexample_Visualization/ — the WriterMonad_*.lean logging-monad traces that feed the ProofWidgets visualizer.

• demos/ — Vite + React + TypeScript playgrounds, one per RDT. CRDT demos do two-way merge; MRDT demos maintain a git-style commit DAG with LCA-driven three-way merge and a toggleable history visualisation.

• runtime/ — the JS MRDT runtime (task #94): a git-like commit DAG for the browser (dependency-free ESM), replicas enforcing head-sync by construction, LCA-driven three-way merge with an explicit criss-cross gate (multiple maximal common ancestors throw, pointing at the virtual-LCA extension, task #90; routine under honest p2p: 592 gated syncs in 220 randomized trials — and the model side of #90 has since landed (virtual-lca-note.md + VirtualLCA_Spot.lean): Step3V with the ungated mergeVirtual rule (recursive antichain merge virtualLCAState, well-founded, ascending rank), the covering proposition mca_events_cover (the MCA union is exactly the head intersection, under the store invariants already carried), canonicity virtualLCAState_canonical (so the per-datatype VC surface does not move for canonicity datatypes), RA-linearizability on the widened LTS (ra_linearizable3_of_honest_reachV), and the revised GC gc_safetyV with the mcasClosure keep-set (the one-layer seed provably loses a depth-2 LCA); single-MCA picks are machine-refuted (each resurrects a deleted element, the SPOT FAIL pair); the runtime's gate remains until the JS implements virtual merges plus the closure seed. The quotient-layer mirrors have since landed as well (GoodConfig3H_V.lean: ONE H-layer fold induction sufficed — the Eq-quotient layers contain no step destructs, and the NF route is precisely the refuted noopFeasible path, deliberately not built — giving the rehoming Eq capstone over the widened LTS, rga_ra_linearizable3_eq_V, and all eleven flats through one bridge, flat_ra_linearizable3_eq_V; the route was forced by a Python probe, rehoming-vlca-probe.md, which found the hEnum shape fires at antichain unions under every enumeration order yet is rehome-correct at every firing, so noopFeasible marks a dead proof route and the mirrors go through K1/GenDisc). And the stability layer is now verified (Stability_VC.lean, design + validation in stability-vc-note.md): the SettledAt contract (the naive meet-of-heads gate is machine-refuted by the discriminating-remove countermodel, fired in the Python harness and pinned as a kernel SPOT), the StabilityVC bundle with an Aux-indexed merge congruence, and stability_simulation at {propext, Quot.sound} — compaction projects to a stuttering self-merge, so the twin DAGs stay literally identical — with reads equal at every version and RA-linearizability inherited observationally; first instance the OR-set (ORSet_stability_reads/ORSet_stability_ra: the twin-liveness-guarded drop — a static drop set is pinned unsound), and the embed re-coding cluster bridged to SettledAt up to the named AnchorsFactorBeyond residue (EmbedRGA_Stability_Bridge.lean)), and the commit GC implementing the verified keep-set: gc_safety (Metatheory/GC_Safety.lean, kernel-clean; design note runtime-gc-note.md) proves pruning to the upward closure of the pairwise head intersections preserves every run and every head read, with a machine-checked countermodel showing a widened (non-head-sync) merge genuinely needs a pruned commit, and the head-monotonicity invariant corrected to HeadDom ∨ Virgin (fresh replicas rebase at the root). Datatype ports: the embedded-chain RGA (pluggable delta code, default = the verified flipped Elias-δ instance transliterated from Lean, 8.9× smaller than unary on the growing-delta workload, code-invariance tested: identical reads under both codes across 100 randomized runs) and an OR-set; the ports are unverified transliterations pinned by Lean codeword pins, Python-extracted read fixtures (both fooling-pair worlds ride through the runtime), and a twin-run GC-safety PBT (220+120 trials, per-step read equality against un-GC'd twins). The GC line has since been completed on both sides: SettledAt is discharged, not assumed (EvidenceDischarge.lean: settledAt_of_allHeard_honest derives it from honest reachability plus the all-heads frontier, the causal-stability argument, with the frontier-maintenance lemmas axiom-free and createReplica the one breaker, i.e. exactly the open-membership gate); the commit GC is strengthened to bounded state (GC_BoundedState.lean: gc_safety_bounded via the clock-swap drops the DAG skeleton entirely so the store costs O(live keep-set), with the compaction-era lineage collision handled by the ClockCoherent payload-is-a-function-of-the-clock guard and machine-checked at its resurrection boundary); and the run-table representation is now a shipped serializer (serialize.js, reconciled bit-for-bit with the mechanized accounting), which closes the absolute-chain save-size gap: real save sizes 24 KB / 22 KB / 73 KB / 120 KB on the four traces (from 35 MB / 53 MB / 170 MB / 243 MB as-shipped JSON), on par with the smallest production save and never growing on delete. And the sync layer is now real: an Automerge-repo-style delta gossip protocol (sync.js: peers exchange head frontiers, ship only the missing commits, ingest re-computes each state and gates on the content-id so state is never trusted over the wire; measured payload ~0.28–0.38× a whole-state resync) and a certified stability GC (frontier.js: the per-replica frontier is the runtime realization of AllHeardSince's evidence commits, stableCut is their meet, and compactStable compacts only at a cut whose certificate is present — refusing otherwise, the executable form of settledAt_of_allHeard; the directed discriminating-remove test shows it refuse while a replica is unheard-from and fire soundly once heard, reads identical to a never-compacted control throughout, with the old asserted compaction diverging as the FAIL companion). 57 runtime tests.

• docs/porting-op-based-crdts.md — recipe for porting a new op-based CRDT into Sal's state-based signature.

• ROADMAP.md — open research threads (Neem soundness metatheory, op→state transfer, the tombstone-free/prefix-free RGA results) with status and entry points.

• docs/metatheory-note/joinpeel-note.pdf — a self-contained paper-style note: why the original VCs are inadequate (worked counterexamples), the set-relative repair and the Join Lemma, the new JoinPeelVCs, and the mechanization.

• Sal/ConditionedMRDTs/sal-mrdts.pdf — the consolidated paper-style note (one document, three parts, replacing the former separate metatheory, embedded-chain design, and sequential-specification notes). Part I, the MRDT (ternary-merge) metatheory: what an MRDT is and how to describe one (with the counter and the OR-set as worked examples), the corrected flat metatheory (the eight VCs with intuition, the delta contract and why no lattice contract can exist, the causal-delta equation, the LCA lemma erratum, the defeater execution, the discharged production catalogue — with TikZ execution diagrams), the conditioned metatheorem, and the factored discharge route (HonestReach × per-configuration JoinLemma3At, the mergeable queue as its flagship). Part II, the embedded-chain RGA design note: birth-chain sort keys, the entropy-coded coordinate representation and the entropy law, the insert prefix, the validation battery, the compaction theorem, the sided generalization with the Fugue/FugueMax arc, and the Eg-walker comparison. Part III, Convergence Is Not Correctness, the sequential-specification campaign: the specification gap RA-linearizability leaves open, the four tiers and their invariant taxonomy (identity hygiene → geometry → composition), the three machine-checked refutations and the two-axis do/merge separation (every placement a named kernel theorem), the composition caveat with the dead-anchor corner and the open question oq:seqwitness, and the consolidated verified matrix absorbing task #64's in-repo rows. Now 83 pages: Part I additionally carries the runtime-facing metatheory (virtual LCAs with the exact covering proposition and the machine-refuted single-MCA shortcut; commit GC with gc_safety and the keep-set; the stability VC with SettledAt, the discriminating-remove countermodel, and stability_simulation), and Part II additionally carries the closed maximal-non-interleaving arc (full adapted W-K Theorem 9 with the corrected backward exception and the Table-1 placement), the chain-price section (the sibling-splice fooling pair, the retention characterization, the 2×2), and the storage layer (re-coding, compactEliasDelta, spine fusion, the run-table representation, all four measurement tables with their accounting models, and the cross-system benchmark with the grows-on-delete churn table). Plus one consolidated open-questions list and one mechanization map.

• Sal/ConditionedMRDTs/defeater-walkthrough.pdf — a slow, self-contained walkthrough of the defeater execution for the published (pre-correction) MRDT soundness proof: the paper's induction and eight-law toolbox restated, every version's state and LCA checked, then the critical merge exhausted move by move (each of the five merge rules in both orientations, the automation catalogue, and the peel-architecture repairs), every failure anchored to a computation or a named kernel theorem (no_inter_lca_2op_rem_peel_of_defeater, crack1_witness, reunification_peel_obstruction, no_proper_back_block, killTest_no_common_U); states precisely that the theorem survives while the proof does not, and re-runs the same merge through the corrected delta-contract route in five lines. Expands sal-mrdts.pdf Part I §4.2.

• Sal/CRDTs/Metatheory/ — the Neem soundness meta-theorem for binary-merge CRDTs, corrected: machine-checked counter-models refute the paper's merge-case proof and show the 24-VC bundle insufficient (a reachable non-RA-linearizable execution under CoreVCs + full semilattice laws); the repaired chains CoreVCs + JoinPeelVCs ⇒ RA-lin and the CD ladder CoreVCs + ACI + inflation + CD ⇒ RA-lin are proved end-to-end (0 sorries), with CD proved the exact minimal residual. See its README.md and FINDINGS.md (A1–A9, drafts A10–A12).

• Sal/ConditionedMRDTs/ — the ternary (three-way merge) metatheorem over the version DAG: the LCA lemma as a reachability invariant, a validated VC set (CoreVCs3CD + FeasibleDeltaVCs3 + CDVC3), and kernel-checked end-to-end RA-linearizability for all 12 production MRDTs through one generic conditioned framework: the eleven flat datatypes (OR-Set, OR-Set-efficient, Enable-wins flag, Grow-Only Set and Map, Increment-Only and PN counters, tombstone RGA, Peritext, Multi-Valued Register, Add-Wins Priority Queue) at the identity instantiation with their VC discharges under MRDT_Instances/ (one directory per RDT), and the rehoming tombstone-free RGA — provably outside the VC schema — at full generality (MRDT_Instances/RGA_Rehoming/RA_Lin.lean): RA-linearizability up to observational ≈ at every reachable configuration, from a single honest-delivery assumption (born accuracy + applicable delivery), kernel-clean. (Demoted 2026-07-16: the convergence capstone stands, but the design is sequential-spec-refuted at the do level — rehoming_seq_refuted, MRDT_Instances/RGA_Rehoming/RGA_SeqSpec_Refuted.lean: a single-replica delete reorders survivors, so the datatype does not implement the naive text buffer — and fused Peritext, its pure instantiation, inherits the residual at the render (fused_delete_reformats_survivor: deleting a plain character re-formats an untouched survivor). It is retained as the framework's only fully general instantiation and as the delete-order countermodel; the canonical sequence RDT is the embedded-chain family below, and the canonical fused Peritext is now the embed-based Peritext_Embed/.) Beyond the production mirrors, five born-conditioned instances: the bounded (escrow) counter — convergence is flat, and the bound value ≥ 0 is a kernel-checked safety theorem at every version of every reachable configuration whose history satisfies the client applicability contract (bc_version_inv, MRDT_Instances/BoundedCounter/); and the mergeable queue of Peepul (PLDI'22 Certified Mergeable Replicated Data Types) — concurrent enqueues form a non-commuting clique, so no rc assignment exists and the flat VC engine is structurally unavailable; its Join Lemma is instead proved directly, exhibiting Peepul's three-way merge as the linearization witness at every merge, giving per-version RA-linearizability under honest delivery (queue_ra_linearizable3, MRDT_Instances/MergeableQueue/), with the dequeue applicable head-check discharging honesty (qHonest_of_applicable); and the FWW reservation register — first-writer-wins with the arbitration timestamp in the payload (a min-semilattice, the positive complement to the lww_merge_needs_timestamps kill-test), whose winner is characterized at every reachable version (fww_version_min, honesty-free) and whose claim-when-unset discipline is deliberately consumed by no theorem: "unset" is not stable under concurrent honest extension, so a merge-based register is a reservation, never a mutex; the LWW register — the max-semilattice dual, with-metadata arbitration carried in the payload so its eight VCs are pure max-algebra and its winner lww_version_max is characterized at every reachable version (honesty-free, MRDT_Instances/LWWRegister/), the resolution of the lww_merge_needs_timestamps kill-test in the LWW rather than FWW direction; and BudgetCart — a budgeted shopping cart (OR-set contents with add-wins rc, per-replica spend derived from live instances so removal refunds the adder automatically), convergent through the OR-set route (BCart_ra_linearizable3_eq) with its budget-safety theorem delivered hypothesis-gated (bcart_version_inv_gated): the ungated obligation is provably false because vis-only causal folds are enumeration-dependent under concurrent add/remove — the instance that forces Open Question 8 (rc-oriented causal witnesses). The composition kit (Sal/ConditionedMRDTs/Metatheory/Product*.lean) turns the binary heterogeneous product of conditioned MRDTs into once-only theorems — convergence (concatenation join witness), safety (one-sided causal witnesses; the two-sided form is provably impossible), and the ≈-quotient lift — and its first real consumer is composed Peritext (MRDT_Instances/Peritext_Composed/): rich text as RGA ⊗ marks (peritextComposed_ra_linearizable_up_to_eq, up to ≈_RGA × =; marks resolved at read time by the RGA's own path-climbing, render ≈-congruence kernel-checked), against a from-scratch alternative assessed structurally infeasible. The fused Peritext is the tombstone-free-and-live alternative: characters and boundary marks share one RGA (PeritextElt = char ⊕ boundary), so mark endpoints ride document order directly rather than freezing tree paths, with independent positional intent theorems (render_id_active_iff_between, render_span_before) at the cost of non-atomic mark placement (the mark-positioning trilemma — atomic / tombstone-free / live, pick two). It exists twice, deliberately: MRDT_Instances/Peritext_Rehoming/ (on the rehoming kernel, peritext_ra_linearizable_up_to_eq) inherits the rehoming delete-reorder residual at the render (fused_delete_reformats_survivor, machine-checked: deleting a plain character re-formats an untouched survivor) and is retained as the countermodel; the canonical fused Peritext is MRDT_Instances/Peritext_Embed/ (on the embed kernel, peritextEmbed_ra_linearizable3 — a pure instantiation of the now payload-generic embed instance), where the state is the document, the read is a map with no fuel or well-formedness hypotheses, and the residual is fixed as a general theorem: renderIds_del (kernel-clean on {propext, Quot.sound}) proves deleting a character leaves every other character's rendered formatting bitwise untouched, with the rehoming witness trace replayed clean in the SPOT block. On top of it, the document-order mark read model (Peritext_Embed/PeritextEmbed_MarkIntent.lean) gives the paper-faithful semantics the earlier no-leak claim got wrong: a deleted boundary anchor rehomes to the nearest surviving neighbour in reading order (gravity per startSide/endSide, growth end-side only), and doc_no_backward_leak (kernel-clean on [propext] alone) proves a rehome never migrates a span backward — the positive that replaces the retracted mark_*_no_leak, with the tree-ancestry leak machine-refuted as its companion, the Litt Ex 1-8 renderings pinned (bold expands at its end, a link does not), and the trilemma's atomicity cost stated honestly as a theorem (doc_delete_can_respan) rather than hidden. The sequential-spec campaign (MRDT_Instances/SeqSpec_Flat.lean, MergeableQueue/MergeableQueue_SeqSpec.lean, EmbedRGA/EmbedRGA_SeqSpec.lean) supplies the independent specification RA-linearizability deliberately does not: RA-lin certifies convergence to the datatype's own fold, so a single-replica do bug is invisible to it; these theorems prove, per RDT, that the fold of any single-replica history equals a straightforward sequential program, via an explicit inductive invariant. Tier 1: the eleven flat RDTs (view homomorphisms; MVR and AWPQ need genuine invariants — overwritten tags stay staked, stake tags stay nodup). Tier 2: the mergeable queue = a plain functional FIFO. Tier 3: the embed RGA = the naive insert-at-index text buffer (the geometric adjacency lemma chainBefore_snoc_iff), with the published tombstoned RGA inheriting the same buffer spec as a corollary (EmbedRGA_SeqSpec_RGA.lean, standalone target). Tier 4, completing the campaign's positive tiers: the embed-based fused Peritext = the naive marked-text editor (peritextEmbed_seq_sound, Peritext_Embed/PeritextEmbed_SeqSpec.lean) — the render is the editor's screen on every sequentially honest history, by composing the now payload-generic tier-3 buffer soundness with the shared pure render walk; the negative rows are the rehoming RGA (rehoming_seq_refuted, do-level) and, at the render, the rehoming-based fused Peritext. Superseded routes, impossibility results, and plans live under Development/.

• Shesha (Sal/ConditionedMRDTs/MRDT_Instances/Shesha/) — a tombstone-free sibling-linked replicated list (order lives in links between live nodes; delete splices and retains nothing), designed live on the whiteboard (2026-07) and named for Ananta-Shesha, "the remainder". Phase-1 verification: sequential_soundness (single-replica folds = the naive linked list; kernel-clean) and delete_preserves_survivor_order — the property the flat tombstone-free RGA provably violates — plus machine-checked litmus witnesses byte-matched to the Python reference, merge symmetry (merge_comm) proved at state equality, and the two fooling-pair impossibility theorems (I1/I2_no_merge_function: no tombstone-free merge can match the tombstoned oracle, nor the strong list spec) quantified over all merge functions. Phase-2b merge lemmas (Shesha_Forest/Skel/M0/M2.lean: a parent-chain/depth layer, the exact skeleton characterization, a placed-exactly-once accounting, and the wpar↔tree-structure bridge): Lemmas M0 and M2 fully closed, all six files sorry-free and kernel-clean — merge_WF (merge_read_nodup: every id placed at most once, via a generic DFS-count engine over splice-chain determinism), the survivor-set identity merge_ids (the merge displays exactly the merge-live ids: ⊆ by working-set + marker-freeness, ⊇ by placement + the positive marker climb + a level-graded emission chain), and the order theorem merge_extends_L/merge_L_filter (merge-surviving L-pairs keep exactly L's display order: a skeleton row is structurally the shallow-W front of its node's child forest, marker expansion turns it into the shallow-survivor front, and the collapsed DFS reads out the survivor filter of read L — the merge-time splice IS the delete splice). Phase-2c (Shesha_Evolution/Cond.lean): the honest-evolution layer is closed — branches evolved from the LCA by honest steps (fresh nonzero ids, live anchors/targets) preserve WF and the branch-structure invariant LRowsOK, so with cross-branch Lamport uniqueness as the sole global contract, every honestly-reached merge is well-formed, symmetric, displays exactly the merge-live ids, and extends the LCA order (merge_*_honest, kernel-clean). Shesha is wired into the one framework as a conditioned instance (SheshaD, timestamp-as-id) by the mergeable-queue route — with a twist the framework had never met: the queue-style plain join hook is provably FALSE for Shesha (Shesha_Join_Refuted.lean, machine-checked: canonical states are existential and, for Shesha, not unique per event set — a concurrent (ins x←a, del a) pair folds to different live sets under its two enumeration orders — so JoinLemma3At can be fed a misaligned canonical triple that makes the merge emit a node twice; the queue was immune only because its canonical states are unique). The corrected route is new generic metatheory (Metatheory/WitnessClass.lean, kernel-clean): join lemmas relative to a witness class, instantiated for Shesha at effective enumerations (SheshaEff: every insert applies — the class real executions produce, under which the live set is determined by the event set alone). The capstone shesha_ra_linearizable3 keeps its exact statement; the join hook shesha_join_at_eff is now proved (phase 2e) by a closed two-way reduction: analysis — every effective witness's fold is the delete-collapse (dropF) of its anchored forest (Shesha_EffFold.lean: delete postponement, order-free set-drop, head-insertion rows, collapse rows = fronts; Shesha_Hook_Facts.lean: Lamport clocks make causal pasts finite and enumerable, so honesty always bites — the exclusion lemmas — and witness_nf puts every join slot in normal form) — and assembly — any vis-compatible anchored forest for the union realizes its collapse as a SheshaEff-canonical state (Shesha_Witness.lean: presplice_canonical, planning the forest then deleting ascending; plan_pw discharges respects loOn structurally); the replay layers (positive op commutations, graft algebra, insert-phase realization planF) feed both halves from Shesha_Replay.lean. The last owed sorry was the merge-correctness core shesha_rows_residue (the ternary merge output is the collapse of a pre-splice anchored forest of the union) — and it is now machine-checked FALSE (Shesha_Rows_Refuted.lean, 2026-07): at an honest SCoh-aligned config (SCoh vacuous) the merge of the canonical folds of LCA=[ins 1], A=[ins 2←1, ins 4←⌂, del 1], B=[ins 3←1] is [3,4,2], splitting deleted node 1's children {2,3} around the concurrent root sibling 4; no pre-splice forest collapses to it, and [3,4,2] is not the fold of any loOn-respecting linearization of the union — so shesha_ra_linearizable3 (which typechecks from that sorry) rests on a now-known-false lemma and its statement is itself unsatisfiable at this reachable merge. The split is caused by Shesha's local-order-preserving splice over a mutable forest — not by anchor-forgetting: the RA-linearizable RGA_Tombstone_Free also forgets the anchor on delete, but it re-homes and re-sorts survivors by their global key, so its read is always a fold (⇒ RA-lin) at the price of reordering survivors (tombstone_free_violates_delete_order); Shesha instead keeps local sibling order (delete_preserves_survivor_order), so one replica is delete-order-faithful but the merge of two mutable forests is not a global fold. This is the sequence-CRDT trilemma (local-order-preserving delete ⊻ merge RA-linearizability). The dissolution is not anchor-retention but immutable stored positions (KC+Kartik Development/RGA_OrderPreserving_Reference.lean, task #63): freeze each node's ancestry path at insert, read = lex-sort by frozen position, delete = pure drop — positions never move, so delete-order holds and the read is a fold; on this trace 2,3 keep contiguous frozen paths [k₁,k₂],[k₁,k₃] while 4 is [k₄], so 4 cannot split them and [3,4,2] never arises (the trilemma reasserts only at the insert-after-already-deleted-anchor corner: the frozen path then needs the dead anchor's position — an append-only position map, i.e. a metadata tombstone, or default-to-root that loses order). The owed research decision is either the immutable-position re-encoding or a capstone restatement to Shesha's actual guarantee (convergence + licensed divergence), which the PBT harness verifies, not a proof of the current statement. Also ahead: Theorem P (causal pairwise display stability) and Theorem D (licensed divergence vs the tombstoned RGA). Design record, pen-and-paper proofs, PBT harness (~16k merges, 0 displayed-pair flips) and the verified anomaly-comparison matrix (6 implementations + yjs/automerge/loro/list-positions) under whiteboard/.

• Sal/MRDTs/RGA_Rehoming/doc/why-the-path-matters.pdf — a visual (TikZ) account of why the tombstone-free RGA needs the operation path, and why a prefix-free variant cannot be VC-verified.

• whiteboard/ — the Shesha exploration record: Excalidraw boards (design trail, fooling pair), self-contained design + proof notes, the PBT harness, the verified anomaly matrix (anomaly-matrix/anomaly_matrix_report.md), and the related-work verification. After the rose-tree Shesha's merge was machine-checked non-RA-linearizable (Shesha_Rows_Refuted), the successor sibling-edge design (sibling-edge-design.pdf) extends the tombstone-free RGA with a second immutable origin (a right sibling edge) and carried spine paths, delete = pure remove (no rehome): a brute-force model (sibling-origin-pbt.py) finds it convergent and RA-linearizable — a loOn-fold for every one of ~37,000 random merges, single- and multi-epoch, 0 anomalies — while preserving single-replica delete-order and non-interleaving. The design search then ran through the consolidated litmus suite (whiteboard/litmus/: tests L1–L25 with provenance + a randomized version-DAG PBT harness, 16 designs), the delta tree (KC's parent-relative-ranges design — refuted as strictly dead-free by two named mechanisms, then corrected by identity arbitration; delta-tree-design.pdf), and the retention question (retention-countermodel.pdf: what must be remembered about a deleted character — answer: nothing beyond the coordinates of the living, if the carve is timestamp-faithful), and its endpoint is the embedded-chain RGA (design note now Part II of Sal/ConditionedMRDTs/sal-mrdts.pdf): coordinates = birth chains under an order-preserving prefix-free delta code, ties impossible, the merge never decides an order — battery-clean (except one-sided L19, RGA's own anomaly), DAG-PBT-clean at 420 executions, lockstep read-equal with the published tombstoned RGA 120/120, and entropy-optimal (~4 bits/level sequential; IEEE 754 as carrier machine-refuted). Its Lean mechanization has landed its capstone: embed_ra_linearizable3 (Sal/ConditionedMRDTs/MRDT_Instances/EmbedRGA/) — RA-linearizability per version at every honestly reachable configuration, kernel-clean, parametric in the code (the unary code, the binary delta code, and the flipped Elias-δ code eliasDeltaCode — log δ + O(log log δ) per level, Embed_Code_EliasDelta.lean — are all proved OrderedPrefixCode instances: three encodings on one proof, the δ-flip capstone inherited with zero new content as embed_ra_linearizable3_eliasDelta), via the mergeable-queue route with the join discharged by canonicity (e_fold_canon: well-formed enumerations of one event set fold to the same state) — in nine sections where the rehoming-based tombstone-free RGA needed its 55-file conditioned chain, closing with applicable⟹honesty (eHonest_of_applicable) and the instance intent theorems (delete-order preservation as sublist stability). Beneath it, Sal/MRDTs/RGA_Embed/ carries the map-model kernel (commutations to state equality under rc = Either; coherence + chainState closures; display stability — step stability axiom-free — the chain-lex theorem, unique decodability, subtree-convexity non-interleaving, and native_decide SPOTs where the flat RGA's delete-reorder witness gets the opposite verdict). The entropy claims are calibrated on real editing traces (whiteboard/litmus/entropy_measure.py on josephg/editing-traces, endContent-verified: order metadata ≈ 1.4–1.8 bits/level; context-conditioned coding measured NOT worth mechanizing; run coalescing the real lever — whiteboard/order-coding-compression-notes.md). And the compaction theorem has landed (rga_read_eq_embed_read, EmbedRGA_ReadEquiv.lean, kernel-clean, standalone build target): on every honest event set, any enumeration of the published tombstoned RGA's visible ids in its own relational visible_lt order — proved total and asymmetric on the birth tree en route, facts the published side never had — equals the embed read, element for element; the lockstep 120/120 is this theorem's tested form, and the embedded-chain RGA is now, as a theorem, the published RGA with the tombstone set compressed into the coordinates. The coordinates themselves are now GC-able, as a theorem (EmbedRGA_Recoding.lean): an order-preserving re-coding below a stable cut, in the lazy-translation formulation (a stable-prefix map applied at rest and on ingest), commutes with the fold (eRecode_applySeq) and leaves every read identical (eRecode_reads_identical), with canonicity and the capstone's per-version witness transporting (eRecode_ra_transport), all kernel-clean; a first-class negative (eRecode_ext_global_collapse) shows the whole-history formulation trivializes (extension-commuting at every historical mint forces the re-map to a constant prefix), so lazy translation is the only nontrivial shape. Measured (embed_recode_check.py): 200 bits to 1 bit on a delete-heavy 200-chain, 500/500 randomized states including concurrent cross-cut continuations, and the deliberately order-breaking control flips reads, pinning the order hypothesis as load-bearing (design note embed-recoding-note.md; deferred there: the protocol half of choosing a common cut, and re-basing honesty so the capstone runs natively in the new epoch). The compaction stack is now verified with no remaining formal debt: the honesty-rebasing obligation (⋆) — the single residue shared by the single-epoch AnchorsFactorBeyond gap and the multi-epoch CompatChain — is discharged (EmbedRGA_HonestyRebase.lean, kernel-clean, Python-validated first with no countermodel): a re-coded configuration is honest modulo the coordinate order-embedding via the invariant I (coded anchored forest over live coordinates), which EHonest establishes once and every StablePrefixMap preserves, so compaction reads are native rather than by-transport at every epoch. The concrete compaction is verified end to end (compactEliasDelta_settled_reads, EmbedRGA_CompactEliasDelta.lean, kernel-clean): at a settled cut of a disciplined honest configuration, drop-dead-ranges plus rank-renumbering under the flipped Elias-δ code preserves every read of every beyond-cut continuation under the lazy translation, with the in-flight wrinkle pinned both ways in the SPOTs (dense renumbering under an in-flight sibling provably flips a read; the guarded pass skips the group and still compresses). The AnchorsFactorBeyond residue is discharged through the generation discipline (EmbedRGA_AnchorsFactor.lean), with a recorded countermodel showing bare honest reachability cannot supply it. The runtime ships the same algorithm plus spine fusion (compact.js, 42 tests), measured on real editing traces at 1.7×–3.2× end to end with history-independence holding three ways; the per-level attribution shows fusion removes essentially all dead levels and the remaining cost is live-tree shape (mean live depth 835–1468 levels), making live-run re-coding (task #73's isometric-fold layer) the next order-of-magnitude lever — and that lever is now verified too (RunTable.lean + EmbedRGA_RunTable.lean): the tail-attachment lemma (tail_attachment, at {propext, Quot.sound} alone), the representation iso in both directions (stateOf_tableOf losslessness + tableOf_stateOf canonicity — over label chains and liveness, deliberately not timestamps, which would be false after an epoch), the two-case contracted comparator equal to keyLt for every code (cmpTable_eq_keyLt), the walk-is-the-display theorem, tableOf_congr (the table is a function of the live-chain set, so merges rebuild identically in any delivery order), tableOf_insert_extend (typing bumps one length field: O(1) per keystroke, as a theorem), and the epoch composition runTable_epoch — the only theorem in the run-table stack carrying a settled-cut hypothesis, its absence elsewhere being the formal content of the measured no-stability-gate finding; SPOTs pin coalesce-necessity and the no-split rival's wrong display as FAIL companions. Generic simulation lemmas for split/delete/materialization remain owed (SPOT-pinned meanwhile), as does the sided run table. The successor arc is the sided embed (sided-embed-design-note.md): two-sidedness as a parameter, not a second datatype. An insert names an anchor and a side; the display rule generalizes from the prefix rule to the in-order rule, made plain lexicographic again by a marker alphabet (R band < marker < L band, the L band in the complemented code); the current datatype is the all-R fragment, exactly; and side selection (always-R gives RGA, Fugue's between-rule gives non-interleaving) is a generation policy, not a datatype choice. The Python model and full battery (litmus/embed_sided.py) validated every design-note prediction on the first run: under the Fugue policy L19 flips clean (backward runs become L-chains) with the rest of the gauntlet staying clean, the all-R fragment is lockstep-exact with the one-sided embed, and the side-bit + per-band-code carrier is faithful. The Lean port has landed both layers, kernel-clean: the sided chain-lex kernel (Sided_ChainLex.lean: the sided marker theorem sdisplay_iff_schainBefore, axiom-free totality, unique decodability sidedCoordOf_inj, the all-R fragment theorem schainBefore_liftR, and in-order-interval subtree convexity schain_subtree_convex, the Fugue intent target), and the conditioned instance with its capstone sided_embed_ra_linearizable3 (MRDT_Instances/SidedRGA/) — RA-linearizability at every honestly reachable configuration for every side assignment, sides being payload to convergence. The per-policy intent theorems have landed (SidedRGA_Intent.lean, kernel-clean): sFold_liftOp proves the always-R sided instance IS the one-sided instance fold for fold, unconditionally (a pure simulation — the sort keys coincide definitionally, so every one-sided theorem transports); and sided_fold_subtree_convex proves subtrees display as contiguous blocks in any chain-generated fold, so any run that chains — the Fugue policy's shape for forward and backward typing alike — is never interleaved by concurrent survivors, with the L19 trace replayed contiguous through the Lean fold as its SPOT. And the Fugue policy itself is now formal (SidedRGA_Fugue.lean, with the design note whiteboard/fugue-maximal-noninterleaving.md and the Python validator litmus/fugue_noninterleave_check.py): an intent-op layer (insert at position), the Fugue side rule as a generation-time function of the replica-local grow-only tree (dead nodes included), and the Weidner–Kleppmann maximal-non-interleaving Definition 4 adapted and formalized over reachable configurations. The verdict is a machine-checked separation, exactly the paper's own Fugue-vs-FugueMax gap landing on our policy: run-contiguity is proved kernel-clean (fugue_reachable_runs_no_interleave, via subtree convexity — concurrent runs never interleave, forward or backward), forward non-interleaving is stated and Python-clean over 1500 randomized states (proof needs the display-to-traversal theory, gap G2), and the FULL maximal-non-interleaving property is refuted twice on reachable traces (fugue_not_maximally_noninterleaving: the kernel's newest-first tiebreak reverses the paper's lowest-ID-first; fugue_not_maximally_noninterleaving_backward: the paper's Figure-7 execution, condition (2)) — as it must be, since W-K themselves prove plain Fugue is not maximally non-interleaving and our policy is Fugue with the RGA recency tiebreak, not FugueMax. That residue has since landed in two waves. The FugueMax tiebreak is a third policy (SidedRGA_FugueMax.lean), realized in the kernel by right-origin tags (an order-reversing fixed-width tag ahead of the R band, SidedMax_ChainLex.lean): the condition the recency tiebreak refuted becomes a positive theorem (fuguemax_same_origin_low_first), and the sided sequential-spec tier is closed (the sentinel-rooted sided_seq_sound, SidedRGA_SeqSpec.lean). The traversal theory then landed (Sided_Traversal.lean + SidedRGA_NonInterleaving.lean, design record §9 of the Fugue note, Python-clean over 12 directed cases and 1800 randomized states in litmus/traversal_check.py): FugueMax forward non-interleaving is discharged kernel-clean (fuguemax_forward_ni, via the chain-shape lemma loShape_of_inv and a first-after descent on the left-origin walk), and the backward condition is now discharged as well (SidedRGA_Backward.lean): the design phase machine-refuted the live-witness reading of the paper's Lemma-5 exception (Figure 7 plus one delete needs the tombstone itself as the witness, so the corrected statement quantifies the witness over minted records, exactly as the paper's own text does), and the mechanization discharges the corrected condition via the RBk mint-time clause bundle and a deterministic four-route witness construction, closing fuguemax_maximally_noninterleaving: the full adapted Weidner-Kleppmann Theorem 9, kernel-clean, to our knowledge the first mechanized maximal non-interleaving result. The plain Fugue policy's forward condition is discharged in W-K's own vocabulary too (fugue_forward_ni, SidedRGA_Fugue_ForwardNI.lean, kernel-clean; the link layer rebuilt as an external invariant over an untouched FugueReach, with ~85% of the FugueMax machinery transferring verbatim). The FugueMax variant also carries its own convergence capstone (fuguemax_ra_linearizable3, SidedRGA_FugueMax_RA_Lin.lean, kernel-clean: RA-linearizability at every honestly reachable configuration of the tagged datatype, parametric in the delta code, via fold canonicity m_fold_canon), with one substantive finding: unique decodability of the tagged coordinates needs tag wellformedness (TagsOK), so the FM honesty contract carries a clause the plain sided contract did not need — the right-origin tag is convergence-load-bearing, not just intent-load-bearing. The remaining sided residue is the price question alone: what the right-origin tag costs in coordinate entropy (task #89).

Paper

Pranav Ramesh, Vimala Soundarapandian, KC Sivaramakrishnan. Sal: Multi-modal Verification of Replicated Data Types.

• PDF: https://kcsrk.info/papers/sal_jan26.pdf

The paper evaluates Sal on 13 RDTs (4 CRDTs + 9 MRDTs), 312 VCs total (24 per RDT). The breakdown across the three stages (DG = dsimp + grind; LB = lean-blaster; ITP = Aristotle-assisted interactive proof):

• 215 VCs (68.9%) via DG — TCB not enlarged.
• 87 VCs (27.9%) via LB — TCB enlarged to include Z3.
• 9 VCs (3.0%) via ITP, all closed using Aristotle, whose outputs are kernel-checked — TCB not enlarged.

RDT	DG	LB	ITP
Increment-only counter MRDT	24	0	0
PN-counter MRDT	24	0	0
OR-set MRDT	3	21	0
Enable-Wins Flag MRDT	9	14	0
Efficient OR-Set MRDT	2	22	0
Grows-only set MRDT	24	0	0
Grows-only map MRDT	22	0	2
Replicated Growable Array MRDT	15	9	0
Multi-valued Register MRDT	24	0	0
Increment-only counter CRDT	24	0	0
PN-counter CRDT	16	2	6
Multi-Valued Register CRDT	24	0	0
OR-set CRDT	4	19	1

Two patterns from the paper: MRDTs generally need less SMT than CRDTs because three-way merges express causality directly, and map-based reasoning stresses current Lean automation more than set-based reasoning (the 8 remaining ITP goals are concentrated in map-heavy RDTs).

Since publication the suite has grown from 13 to 29 RDTs, and most of the added CRDTs were proved with the uniform kernel-verifiable pattern described under The sal tactic, without invoking Blaster for the majority of VCs. A refreshed DG/LB/ITP breakdown across all 29 RDTs is future work. The papoc2026 branch snapshots the repo at the paper-artifact state.

License

MIT; see LICENSE.