Agent Coherence MCP Server

agent-coherence

agent-coherence stops one agent from silently clobbering another's work on a shared plan.md, store key, or memory.json — a vendor-neutral MESI + optimistic-concurrency coordinator for agent state on a single host, with the safety invariants machine-checked in TLA+.

Two agents share an artifact — a plan.md, a store key, a memory.json. One reads it and works; meanwhile a peer commits a newer version; the first writes back anyway. Last write wins, the peer's work is silently gone, nothing errors, and every downstream decision builds on the wrong version.

Why it goes unnoticed. An agent system keeps two records of what happened: the one your infrastructure can verify — which version each agent held, what actually committed, what was refused — and the one the model narrates, "task complete", "the plan is updated". They agree until an agent acts on a version that moved underneath it, and the narrated record is the one you read. That is why a lost update looks like a clean run and gets debugged as a model problem. agent-coherence is the verified record for the state your agents share. (It does not verify what an agent did in the outside world — a sent email, a fired webhook — that stays your outbox and idempotency layer's job.) agent-coherence turns that silent clobber into a loud, typed refusal: MESI-style ownership and invalidation over shared artifacts, optimistic commit-CAS for concurrent writers, and a read-generation fence for crash-reclaimed ones — a stale write is denied or returned as a retryable conflict, never silently applied. Same library, same protocol, across LangGraph, CrewAI, AutoGen, the OpenAI Agents SDK, plain files shared across processes (CoherentVolume), any MCP client (the stale-write-guard-fs server, via the mcp extra), and any custom orchestrator. Same behavior regardless of which model provider (Anthropic, OpenAI, Google, Mistral, open-source) the agents talk to.

mcp-name: io.github.cohexa-ai/stale-write-guard-fs

# Requires Python 3.11+
pip install "agent-coherence[langgraph]"        # LangGraph drop-in
pip install "agent-coherence[crewai]"           # CrewAI adapter
pip install "agent-coherence[openai-agents]"    # OpenAI Agents SDK adapter (experimental)
pip install "agent-coherence[diagnose]"         # ccs-diagnose CLI
pip install "agent-coherence[mcp]"              # stale-write-guard-fs MCP server
pip install "agent-coherence[conformance]"      # substrate conformance corpus (for foreign implementations)
pip install "agent-coherence[all]"              # everything

# Before
from langgraph.store.memory import InMemoryStore
store = InMemoryStore()

# After — one import change, no node code changes
from ccs.adapters import CCSStore
store = CCSStore(strategy="lazy")

store.get(), store.put(), store.search() keep working unchanged. CCSStore adds read-side coherence: a peer's commit invalidates your cached view, so your next read is a fresh miss. It does not deny a stale write-back — put is not version-CAS; for write-side lost-update prevention, route writes through CoherentVolume or write_cas (below).

The one-import swap assumes your store namespaces carry the agent identity in namespace[0] — a (user_id, "memories") shape would merge users onto one shared artifact. See the namespace convention.

# Plain files shared across processes / sessions — no framework required
from ccs.adapters.coherent_volume import CoherentVolume

vol = CoherentVolume(workspace_root, managed=("plans/**",))
plan = vol.read("plans/plan.md")           # tracked read — your view is registered
vol.write("plans/plan.md", revised_plan)   # stale view? denied fail-closed → vol.reacquire() and re-derive

agent-coherence-replay — invariant-replay for any CoherenceAdapterCore-mediated agent system. LangGraph capture verified in v1 via CCSStore.record_to(path); CrewAI / AutoGen wired through the same seam but unverified — file an issue if it breaks.

What it guarantees

Each row is a safety invariant model-checked with TLA+/TLC. make tla-check runs all nine specs. CI runs them as three parallel jobs on every pull request that changes a TLA+ input (the specs and their configs, the Makefile, the workflows, and the scripts that decide and judge the run), and on every run outside a pull request. Every spec carries a documented mutant that must fail — the invariants are load-bearing, not decorative.

The table is also machine-checked against the test suite: the packaged claim ladder (ccs.testing.claim_ladder) pins every claim-phrase above to the tests that would fail without it — resolved at collection time and two-way drift-guarded by tests/conformance/test_claim_ladder.py, so a claim cannot outlive its proof (and a cross-host rung cannot appear without one).

Scope, honestly: the guarantees hold for writers that go through the coordinator, under a single coordinator (one host). Both registries hold one lock across every check-and-act sequence — the durable SQLite registry and the in-memory one carry the same concurrency contract, so an embedder may drive either from several threads. Concurrent same-key writers on one host are covered, with one open gap (#248): a plain write() made after a peer's write_cas_at has committed but before the peer's bytes reach disk is lost when the writing volume holds no live view of the file — it never read it, it read it only inside that window (the coordinator refuses such a read, even where read() hands back the old bytes under the default on_stale_read="allow"), or a write_cas / write_cas_at it ran ended in ViewWedged. Both calls report success, disk keeps the peer's bytes while the coordinator records the lost write as the newest version, and every write_cas / write_cas_at on the file raises ViewWedged until a plain write() replaces it. A volume that read the file before the peer committed is refused instead. Cross-host fencing is on the roadmap, demand-gated — if you need it, open an issue. Edits that bypass the coordinator entirely (a human in an editor, a formatter, a regenerating script) are caught at the read()/write() boundary by content-hash checks — the foreign-edit guards below, enforced by tests rather than TLA+; the batch CAS path has a narrower boundary, spelled out in Atomic multi-file publish. Specs, the invariant ↔ implementation map, and the mutant recipes live in formal/tla/.

Correctness is the wedge; the token savings come with it. Writes publish ~12-token invalidation signals instead of rebroadcasting full artifacts, so read-heavy fleets stop re-paying for state they already hold:

Measured on real LangGraph graphs; see docs/reproduce.md and the user guide.

Those are the spatial savings (more agents sharing one artifact). The temporal dimension — a single agent whose source drifts between its turns — has its own pre-registered benchmark, TC-1 (#116): a reproducible savings-regime map of how many re-fetches coherence-gating avoids as the change-rate rises. The metric is re-fetches-avoided — a proxy, a regime map, not a token/dollar invoice. Reproduce with python tools/run_cost_sweep.py; the locked verdict + numbers (PASS at n=50, crossover r≈0.31) live in benchmarks/cost_preregistration.md. Shipped in v0.9.3.

RAG & shared agent memory

RAG corpora and agent memory are shared mutable state, so the stale-read→write lost update lands there too — and a consistent store doesn't save you: the staleness is in the agent's cached view of a record, not the store. Two agents read a record at v1; one writes v2; the other, still on its v1, writes an edit computed from v1 and clobbers v2. agent-coherence keeps the readers current — CCSStore is a drop-in for langgraph.store (composing with Mem0, Letta, LlamaIndex, a vector store, or a plain file underneath whatever you already use; it stores no vectors and does no ranking), so a peer's commit invalidates the stale cached view (read-side coherence). Preventing the stale write-back itself is the write side — route those writes through CoherentVolume or write_cas.

• Runnable, deterministic demo (offline, no keys): python -m examples.coherent_volume.main reproduces the documented lost update, then prevents it.
• Honest scope: writes that go through the coordinator are caught. Auto-watching an unmanaged external source that changes with no coordinator write (a hand-edited file, an out-of-band re-index) is the source-watcher case — on the roadmap, demand-gated, not shipped today.
• Positioning + FAQ: agent-coherence.dev/rag.

---

• 📖 User guide — installation, namespace convention, strategies, observability, telemetry, examples, full API reference
• 🔎 RAG & shared memory — coherence for retrieval corpora and agent memory stores, with the runnable lost-update demo
• 🗂️ Coherent workspace — CoherentVolume, the data-plane appliance for plain files shared across processes
• 🧱 BYO substrate — CoherentRow / CoherentObject, the same coherence over a Postgres row or an S3 object you already run
• ⏪ Workspace versioning & restore — WorkspaceVersioner, checkpoint a mixed file + S3 workspace, name who may restore it, and bring it back with per-member honesty
• 🛡️ Foreign-edit guards — catch out-of-band edits (a human, a formatter, a script) at the read/write boundary, and count the ones in between offline (foreign-write detection)
• 🔌 MCP server — stale-write-guard-fs, the same guarantee for any MCP client, no Python integration required
• 🚦 Effect-ordering gate — gate(), fire an agent's effect only on the input state — value and grant — it decided from; the same verdict over MCP (swg_gate) and over HTTP (POST /hooks/effect-fence)
• 📸 Multi-artifact snapshot sessions — read several artifacts as one consistent cut; no torn reads
• 📦 Atomic multi-file publish — atomic_publish, land a set of files all-or-nothing; never a torn pair
• 🤝 Targeted grant handoff — hand a file to one named session; the giver's later write is refused as handed_off until the version moves, the successor declines, or the giver withdraws. From Claude Code, CoherentVolume, MCP or HTTP; served by the Python coordinator only
• 🧮 Formal verification — the TLA+ specs, invariant ↔ implementation map, mutant recipes
• 🩺 ccs-diagnose CLI — find divergent reads in your existing LangGraph graph without changing any code
• 📊 Conflict-outcome counters — count how often each typed refusal actually fired, read offline from a closed state.db
• 🧩 Claude Code plugin — cross-session coherence for the prose rules (CLAUDE.md, plan.md) parallel Claude Code sessions share
• 🔍 Why coherence matters — the gap across LangGraph, CrewAI, AutoGen, and Claude Agent SDK
• 🧭 The MESI-derived approach — how the protocol maps each documented gap to a shipped surface, with boundaries
• 🪪 Caller principal — once a writer claims one, a request naming its session without it cannot release its grants or commit under its name; clients that never claim keep working
• 🔐 Security & supply chain — kill switches, hash-pinned install, attestation verification, threat model
• 📜 Changelog — version history
• 📄 Paper on arXiv (2603.15183) — formal protocol, TLA+ verification, simulation results

How it works

Each shared artifact is cached locally per agent and reads serve from the local cache when that copy is fresh. Writes commit to a coordinator, which sends lightweight invalidation signals (~12 tokens) to peers so the next read fetches the new version instead of rebroadcasting the full artifact. Consistency is single-writer-multiple-reader per artifact with bounded staleness — peers re-fetch on next read.

Two write disciplines share the same guarantee. Pessimistic: acquire EXCLUSIVE, commit; a writer whose view went stale is denied and must reacquire(). Optimistic: write_cas — read, compute, commit-CAS; the loser of a race gets a typed conflict and bounded retry. Crash recovery composes with both: reclaiming a stalled grant bumps the artifact's ownership epoch, so a reclaimed writer that completes later is rejected at commit even when the version is unchanged (the read-generation fence). On the read side, a snapshot session pins a consistent cut across several artifacts, so a multi-artifact read never sees a torn mix of versions.

Five synchronization strategies ship out of the box: lazy (default), eager, lease (TTL-based), access_count, and broadcast. Pick the one that matches your workload's read/write ratio and how aggressively cached reads should refresh.

Architecture

• Protocol (ccs.core, ccs.strategies) — coherence state machine and synchronization strategies; no framework dependencies.
• Coordinator (ccs.coordinator) — authority service tracking directory state, publishing invalidations, arbitrating commit-CAS, and reclaiming stale grants (crash recovery + read-generation fence).
• Adapters (ccs.adapters) — framework integrations for LangGraph, CrewAI, and AutoGen (~100 lines each), plus an experimental OpenAI Agents SDK adapter (Session-cache coherence + RunHooks).
• Coherent workspace (ccs.adapters.coherent_volume) — the data-plane appliance: an out-of-process coordinator client that brings the same guarantee to plain files on disk, no framework required. See Coherent workspace.
• MCP server (ccs.mcp) — the stale-write-guard-fs stdio server that exposes the coherent-workspace guarantee to any Model Context Protocol client over ten swg_* tools. See MCP server.
• Simulation (ccs.simulation) — deterministic tick-driven engine for scenario benchmarks with failure injection.
• Event bus (ccs.bus) — the transport for invalidation signals; in-memory / in-process today (InMemoryEventBus). Networked transports (Redis, Kafka, NATS, gRPC) for a multi-host deployment are on the roadmap, demand-gated.

Protocol safety properties — single-writer, monotonic versioning, the crash-recovery sweep invariants, the OCC no-lost-update, the reclamation fence's no-stale-apply, the effect gate's no-stale-admit, version retention's no-collected-read, the snapshot session's no-read-skew-within-cut, and workspace restore's no-partial-restore-registered — are model-checked with TLA+/TLC. CI runs all nine specs, split across three parallel jobs, on every pull request that changes a TLA+ input (the specs and their configs, the Makefile, the workflows, and the scripts that decide and judge the run) and on every run outside a pull request.

Coherent workspace: the data plane for shared files

The framework adapters wrap a store. CoherentVolume is the other half — the data-plane appliance, the building block that makes a shared workspace coherent for plain files on disk, with no framework in the loop. Architecturally it's an out-of-process coordinator client, not an in-process wrapper: it writes the policy, spawns (or attaches to) a local coordinator over SQLite-WAL, and routes reads and writes through it. Your content stays on the real filesystem; the coordinator holds only MESI state, a content hash, and a version per managed file. Point a sibling volume in another process at the same workspace and it attaches to the same coordinator, so a single-host fleet shares one coherent view. Every volume in that fleet must declare the same managed globs: an attaching volume adds nothing to a running coordinator's policy, so at attach each volume checks the globs it declared against the coordinator's strict, tracked and ignored sets and refuses, naming them, if any is not enforced. A mixed-globs fleet is unsupported; it fails closed rather than quietly.

from ccs.adapters.coherent_volume import CoherentVolume

vol = CoherentVolume(workspace_root, managed=("plans/**", "memory/**"))
data = vol.read("plans/plan.md")              # bytes — registers a SHARED view
vol.write("plans/plan.md", revise(data))      # stale view? denied fail-closed
data = vol.reacquire("plans/plan.md")         # recover: clear the stale view + mandatory fresh read

The explicit read / write / reacquire / write_cas API is the supported primitive (write_cas(path, make_content) is the optimistic counterpart for same-key contention — the loser gets a typed conflict, never a silent drop). For code you'd rather not rewrite, an opt-in, demo-grade open() shim routes managed-path opens through the volume so existing open() / pathlib calls get coherence unchanged:

from ccs.adapters.coherent_volume import coherent_workspace

with coherent_workspace(workspace_root, managed=("plans/**",)):
    text = open("plans/plan.md").read()       # registers a SHARED view
    open("plans/plan.md", "w").write(edit)    # stale view? raises out of close()

Scope, honestly. Plain write() prevents the sequential stale-read→write lost update for a single-host fleet sharing one workspace (A reads v1, B reads v1, A commits v2, B's stale write is denied → B re-reads); concurrent same-key racers go through write_cas — one winner, the loser gets a typed conflict and re-derives, never a silent drop. Edits that bypass the volume entirely are caught at the boundary by the foreign-edit guards. It does not catch an agent that re-reads fresh bytes and then writes a buffer computed from older ones. The open() shim is convenience, not the contract: it covers open()/pathlib text+binary read/write, but not raw os.open, subprocess redirection, mmap, or append/update modes — those delegate to the original open() unchanged. Run it yourself: python -m examples.coherent_volume.main (offline, deterministic, no keys), or read the positioning + FAQ.

Foreign-edit guards: writes that bypass the coordinator

Coordination covers writers that opt in — but real workspaces also get edited from outside: a human fixes a file in an editor, a formatter rewrites it, a CI script regenerates it. Without a guard, the next agent write silently buries that edit, and the next agent read silently builds on bytes the coordinator never saw. CoherentVolume guards both boundaries with a content-hash check:

• Write boundary — on by default. Before writing, the volume checks whether the managed file's on-disk bytes changed out-of-band since it last read or wrote them. If they did, the write raises StaleView instead of clobbering the foreign edit — recover with reacquire() (fresh read → re-derive → re-write). Opt out with CoherentVolume(on_stale_write="allow") to restore last-writer-wins.

• Read boundary — opt-in. With CoherentVolume(on_stale_read="raise"), re-reading a managed file whose bytes changed out-of-band raises StaleView instead of returning bytes your other state wasn't computed from; in strict mode the coordinator enforces the same check server-side. A volume never denies its own just-written bytes — the benign commit→disk-write lag window is recognized and suppressed. on_stale_read governs read() only. Whatever it says, the versioned reads — read_with_version(), read_with_version_generation() and the MCP swg_read — refuse a managed file whose bytes are not the coordinator's content at the version it reports, outside that same window after the volume's own commit: they raise StaleView (swg_read answers a stale_view deny with no version) rather than hand out a version a compare-and-swap would then be checked against.

vol = CoherentVolume(workspace_root, managed=("plans/**",), on_stale_read="raise")
# a formatter rewrites plans/plan.md out-of-band …
vol.write("plans/plan.md", revised)   # StaleView — the foreign edit survives
fresh = vol.reacquire("plans/plan.md")  # recover: fresh read, re-derive, re-write

Scope, honestly. These are content-hash checks at the volume's read/write boundary — best-effort point-in-time detection, not filesystem interception. A write that never goes through the volume is caught at the next volume read/write of that file, not blocked as it happens; watching unmanaged external sources is on the roadmap, demand-gated. What happens before that next read or write is now observable: the Python coordinator's sweep asks git which coordinated files changed on disk and records each change it cannot account for as foreign — counted, never denied — and ccs.diagnose.foreign_writes.read_foreign_write_report reads the tally back offline from a closed state.db (foreign-write detection). It watches only files git tracks, and only when the coordinator's root is the top of its git work tree (#241). These guards are enforced by tests, not TLA+ — the model-checked invariants cover the protocol state machine, not disk bytes. They cover read()/write() (and the MCP tools that wrap them); the CAS paths check versions instead — write_cas/write_cas_at still fail closed on a foreign edit (the content-checked comparand read wedges rather than clobbering), but a multi-file atomic_publish does not check disk content at all — see its scope note.

MCP server: stale-write-guard-fs

The same guarantee for agents that speak Model Context Protocol — Claude Code, Cursor, or a custom runtime — with no Python integration at all. stale-write-guard-fs is a stdio MCP server that wraps CoherentVolume and exposes coordinated file access as ten tools:

pip install "agent-coherence[mcp]"

{
  "mcpServers": {
    "stale-write-guard-fs": {
      "command": "stale-write-guard-fs",
      "env": { "SWG_ROOT": "/path/to/shared/workspace" }
    }
  }
}

The server binds one workspace per session (SWG_ROOT, defaulting to its working directory; the whole workspace is guarded unless SWG_MANAGED — a comma-separated glob list — narrows it), rejects path traversal and any access to the coordinator's own state directory, and fails closed on IO errors. Denials come back as typed, machine-readable payloads — an agent can parse recover: reacquire and self-heal instead of retrying blindly. Run the red→green demo: python -m examples.mcp_stale_write_guard.main (offline, deterministic, no keys).

Scope, honestly. Same contract as the volume it wraps: single-host, managed paths, cooperative — it guards agents that route file access through the tools; it cannot see edits made around them (those are caught at the next tool call on that file by the foreign-edit guards).

Effect-ordering gate

Agents don't only overwrite files — they fire effects (a deploy, a PR, a shell command) computed from inputs they read earlier. If the input moved in between, the effect fires on stale state. gate() narrows that window: it captures the input's (version, ownership generation) pair at decision time, re-reads the pair at the effect boundary, and fires only if both are unchanged at that re-read — otherwise it holds the effect before it runs. The two comparands catch different failures: the version catches a peer that changed the input; the generation catches a coordinator sweep that reclaimed the grant the input was read under while the bytes never moved — a stalled agent whose lease lapsed mid-decision would otherwise fire its effect on revoked authority, with the version check none the wiser. One revocation moves neither comparand: a peer's pessimistic write-acquire takes the holder's grant with no commit behind it yet (version unmoved) and no epoch bump (that trigger is deliberately outside the bump set). The gate closes that leg by also requiring the re-read itself to be served under a standing grant — a preempted holder's re-read comes back stale, and the effect holds. That re-read is a verification read the coordinator does not re-grant, so the hold is level-triggered: a bare retry holds again until the caller reacquires. This third leg is enforced by tests (the claim ladder pins it), not TLA+ — the model-checked NoStaleAdmit covers the comparand pair.

from ccs.adapters import CoherentVolume, gate

vol = CoherentVolume(workspace_root, managed=("deploy/**",))

# fires run_deploy(plan) only if deploy/config.txt is unchanged since decide() read it;
# else raises StaleView before the deploy runs — reacquire() and re-decide.
gate(vol, "deploy/config.txt", decide=plan_deploy, effect=run_deploy)

It's plain Python, so the same call drops into a LangGraph node, a CrewAI task, or a raw script unchanged.

Three surfaces, one rule. gate() is the Python spelling of the fence. swg_gate is the MCP one, and POST /hooks/effect-fence answers the identical verdict to any client that speaks neither — same question, same classification, same hold reasons. Those reasons are a wire vocabulary, published with each one's establisher and its own recovery in the effect-fence contract. One leg is not the same everywhere: only the HTTP route can report content_claim_absent, the case where the coordinator records no content claim for the artifact at all — the Python and MCP surfaces read a hash comparison rather than the coordinator's own record, so "the claim matches" and "there is no claim" reach them as one value.

Scope, honestly. The gate orders effects, it does not roll them back: it fires pre-effect and never undoes one, so for an escaping effect there's a residual re-read→fire window it narrows but can't close. It's single-host and cooperative — the agent opts in. Both comparands are fail-closed: an unconfirmed version (degraded read) or an unconfirmed generation (a strict-mode deny, or a coordinator that reports no generation, such as one older than v0.14.0) HOLDs rather than firing. For a pure write effect, use vol.write_cas_at(path, expected_version, content) directly, which is the atomic, no-window path. Gating several mutually-consistent inputs at once is a snapshot-session operation on the coordinator, not this single-input wrapper. Run it: python -m examples.effect_gate.main (offline, deterministic, no keys), or add --baseline to see the stale fire it catches; python -m examples.gate_effect_ordering.main adds the reclaimed-lease act (version unchanged, authority revoked, deploy held).

Multi-artifact snapshot sessions

gate() protects one input. But an agent that reads several artifacts one by one — a plan, a config, a memory file — can see a torn combination: plan.md from before a peer's commit and config.json from after it. Every individual read was current; the set never coexisted (read-skew). A snapshot session closes that window: it pins a consistent cut of the artifacts you name, captured at a single point, and serves every session read from that cut while peers keep writing.

Against a running coordinator (the same one CoherentVolume spawns), over HTTP:

POST /session/begin      {session_id, read_set: ["plans/plan.md", "config/app.json"]}
                         → {session_token, cut: {path: version}, …}
POST /session/read       {session_id, session_token, path}
                         → the artifact at its PINNED version — never a newer one
POST /session/commit     {session_id, session_token, path, content}
                         → wins only if no peer moved the artifact since the cut
POST /session/heartbeat  {session_id, session_token} — keep the session's lease alive

Or in-process: CoordinatorService.begin_session(read_set=…, owner=…) → session_read(…) / session_commit(…). The cut is an inspectable {artifact: version} map, not an opaque handle — you can read exactly which versions your session is pinned to.

Fail-closed by construction: reading an artifact that was not in the pinned read-set is refused with a typed rejection — never silently served from live state. Sessions have a bounded lifetime backed by a heartbeat lease: a session whose heartbeat lapses, or that is lost to a coordinator restart, is invalidated — later reads get a typed "session invalidated" rejection telling the agent to re-establish, never a quiet fall-through to whatever is current. Model-checked: NoReadSkewWithinCut and PinAlwaysRetained (formal/tla/Snapshot.tla).

Scope, honestly. This prevents read-skew — torn reads across artifacts. It does not add write-skew prevention: commits validate per-artifact against the pinned base through the same optimistic CAS as write_cas, so two sessions that read one cut and write different artifacts can still interleave. Single coordinator, single host. When the coordinator retains version bodies it serves the pinned bytes directly; otherwise it returns the pinned version and content hash as a typed signal and the caller fetches the bytes from its own data plane.

Atomic multi-file publish

write_cas_at lands one file if it hasn't moved. But an agent often edits a set of files that must stay consistent — a plan and its manifest, a config split across files — and must land them together or not at all, never a torn pair where one file references another that already changed. atomic_publish is that all-or-nothing batch:

from ccs.adapters import CoherentVolume

vol = CoherentVolume(workspace_root, managed=("proj/**",))

# lands BOTH files iff each is still at the version the agent read; otherwise the
# WHOLE publish is held (StaleView / CasVersionConflict) with NO file written.
versions = vol.atomic_publish([
    ("proj/plan.md",     plan_version,     new_plan_bytes),
    ("proj/manifest.md", manifest_version, new_manifest_bytes),
])   # -> {"proj/plan.md": 2, "proj/manifest.md": 3}

Either every member's version advances or none does, and a moved member holds the whole batch — a torn commit is never a reachable state, formally specified as the NoPartialPublish invariant in formal/tla/AtomicPublish.tla. AtomicPublish.tla is specified and semantically validated but is not in the CI sweep — it is held out pending a bounded encoding that converges within the CI time budget, so NoPartialPublish is not among the nine invariants model-checked on every push. A single-file publish takes the direct CAS path; a multi-file publish opens a snapshot session so the versions it checks are captured at one point (no member read across a peer commit). Run it: python -m examples.atomic_publish.main (offline, deterministic, no keys), or add --baseline to see the file-by-file torn pair it prevents.

Documentation truncated — see the full README on GitHub.