MCP concurrent mutations can corrupt generated project artifacts #41

New issue

Closed

opened 2026-06-06 12:08:06 -07:00 by jwilger · 0 comments

jwilger commented

2026-06-06 12:08:06 -07:00

Owner

While converting Eddy's existing event model to EMC via the EMC MCP server, I hit a project-artifact corruption case when multiple mutating MCP tools were called concurrently.

Context

Consuming repo: /home/jwilger/projects/eddy
EMC repo: https://git.johnwilger.com/slipstream/emc
EMC was installed from the remote flake and exposed to Codex as an MCP server.

The Eddy import initially did this in one parallel batch through MCP:

init_project(name = "Eddy")
add_workflow(slug = "organization-access", ...)
parallel add_slice(...) calls for the workflow's slices
then connect_workflow(...) calls

Observed behavior

After the parallel add_slice calls, EMC reported success for several individual tool calls, but the generated workflow/index state was corrupted.

emc list slices returned only a partial/corrupt set like:

Resolve application entry
translation
record-scim-manager-relationship
show-manager-progress-visibility

emc show workflow organization-access showed the workflow digest and generated Lean/Quint containing duplicated/collapsed translation slugs and shifted fields, for example:

def workflowSlices : List String := ["resolve-application-entry","translation","translation","translation","show-manager-progress-visibility"]

def workflowStepRelationships : List (String × String) := [("resolve-application-entry", "entry"),("translation", "activate-member-from-verified-saml-claim"),("translation", "Record SCIM manager relationship"),("translation", "Translate a Stytch SCIM manager relationship removal callback into Eddy manager-report relationship facts."),("show-manager-progress-visibility", "main")]

Subsequent transition calls failed with errors like:

unknown workflow step bootstrap-root-organization-access-boundary
unknown workflow step show-stytch-b2b-access-settings

emc check then failed with artifact drift, e.g.:

Lean slice artifact drift for ActivateMemberFromVerifiedSAMLClaim.lean

I had to delete the generated EMC project artifacts (emc.toml, model/, reviews/) and reinitialize. Sequential MCP mutations did not exhibit the same corruption before the session was interrupted.

Expected behavior

Concurrent MCP mutation requests should not corrupt the EMC project.

Acceptable fixes could be any of:

serialize all mutating MCP tool calls per project root;
acquire a project-level lock around read/modify/write/regenerate operations;
make artifact updates atomic and retry-safe;
reject concurrent mutations with a clear JSON-RPC error telling the client to retry serially.

The important invariant is that successful mutating tool responses must leave the Lean/Quint artifacts and workflow/slice indexes synchronized and semantically intact.

Suggested regression coverage

Add MCP tests that issue concurrent mutating requests against the same project root, such as multiple add_slice calls for the same workflow, and assert that one of the following holds:

all requested slices exist with correct slugs, names, types, descriptions, and relationships, and emc check passes; or
overlapping writes are rejected cleanly with JSON-RPC errors and no partial/corrupt artifacts remain.

Also consider a test that runs add_slice and connect_workflow under concurrent client requests to ensure workflow transitions cannot observe a partially regenerated slice index.

Why this matters

Codex and other MCP clients can issue independent tool calls in parallel. EMC currently exposes mutating tools as normal MCP tools, so consuming projects can accidentally corrupt their authoritative Lean/Quint event model during imports or agent-driven authoring unless EMC enforces mutation serialization/atomicity itself.

While converting Eddy's existing event model to EMC via the EMC MCP server, I hit a project-artifact corruption case when multiple mutating MCP tools were called concurrently. ## Context Consuming repo: `/home/jwilger/projects/eddy` EMC repo: `https://git.johnwilger.com/slipstream/emc` EMC was installed from the remote flake and exposed to Codex as an MCP server. The Eddy import initially did this in one parallel batch through MCP: - `init_project(name = "Eddy")` - `add_workflow(slug = "organization-access", ...)` - parallel `add_slice(...)` calls for the workflow's slices - then `connect_workflow(...)` calls ## Observed behavior After the parallel `add_slice` calls, EMC reported success for several individual tool calls, but the generated workflow/index state was corrupted. `emc list slices` returned only a partial/corrupt set like: ```text Resolve application entry translation record-scim-manager-relationship show-manager-progress-visibility ``` `emc show workflow organization-access` showed the workflow digest and generated Lean/Quint containing duplicated/collapsed `translation` slugs and shifted fields, for example: ```lean def workflowSlices : List String := ["resolve-application-entry","translation","translation","translation","show-manager-progress-visibility"] def workflowStepRelationships : List (String × String) := [("resolve-application-entry", "entry"),("translation", "activate-member-from-verified-saml-claim"),("translation", "Record SCIM manager relationship"),("translation", "Translate a Stytch SCIM manager relationship removal callback into Eddy manager-report relationship facts."),("show-manager-progress-visibility", "main")] ``` Subsequent transition calls failed with errors like: ```text unknown workflow step bootstrap-root-organization-access-boundary unknown workflow step show-stytch-b2b-access-settings ``` `emc check` then failed with artifact drift, e.g.: ```text Lean slice artifact drift for ActivateMemberFromVerifiedSAMLClaim.lean ``` I had to delete the generated EMC project artifacts (`emc.toml`, `model/`, `reviews/`) and reinitialize. Sequential MCP mutations did not exhibit the same corruption before the session was interrupted. ## Expected behavior Concurrent MCP mutation requests should not corrupt the EMC project. Acceptable fixes could be any of: - serialize all mutating MCP tool calls per project root; - acquire a project-level lock around read/modify/write/regenerate operations; - make artifact updates atomic and retry-safe; - reject concurrent mutations with a clear JSON-RPC error telling the client to retry serially. The important invariant is that successful mutating tool responses must leave the Lean/Quint artifacts and workflow/slice indexes synchronized and semantically intact. ## Suggested regression coverage Add MCP tests that issue concurrent mutating requests against the same project root, such as multiple `add_slice` calls for the same workflow, and assert that one of the following holds: 1. all requested slices exist with correct slugs, names, types, descriptions, and relationships, and `emc check` passes; or 2. overlapping writes are rejected cleanly with JSON-RPC errors and no partial/corrupt artifacts remain. Also consider a test that runs `add_slice` and `connect_workflow` under concurrent client requests to ensure workflow transitions cannot observe a partially regenerated slice index. ## Why this matters Codex and other MCP clients can issue independent tool calls in parallel. EMC currently exposes mutating tools as normal MCP tools, so consuming projects can accidentally corrupt their authoritative Lean/Quint event model during imports or agent-driven authoring unless EMC enforces mutation serialization/atomicity itself.