Multi-tool protection semantics

The original state-machine observations and source line references below come from commit 466be4a5d423ad763c7325263f1d014311c95879 and commands run on 2026-08-22, answering the four questions in roadmap section 15.4. The status rendering described here was rechecked on 2026-09-08 using the published Linux x86-64 artifact from source commit af3324bdf121b048d310629b18405986f8e01dca, SHA-256 93d1dfa722f05127025f2c087949f9356c6292f737e37e9a8b94948e10242f8b, as pinned in the install guide at the captured revision, for one tool, several tools, two configured servers, and repeated protect invocations; it supersedes that commit’s braced rendering. It does not propose implementation work or decide the boxpol question.

That 2026-09-08 recheck used SHA-256 93d1dfa722f05127025f2c087949f9356c6292f737e37e9a8b94948e10242f8b, the published v0.3.0 artifact, before multi-server protection shipped. Current behavior differs from question 2’s answer below: a later release added multiple-server protection — multiple servers can be protected in the same project at once, and activation outside the project lock lets them run simultaneously (see the current release notes, docs/assurance/RELEASE-NOTES-v0.4.0.md, PR #304 “Protect multiple servers and admit the recovery help line” and PR #312 “Activate outside the project lock so simultaneous servers both start”; see also Several servers in one project for the current operating guidance). State now lives per server at projects/<id>/servers/<encoded-server-name>/state.json; the single project-level state.json this page’s observations were captured against predates multi-server support and is kept readable for compatibility. The per-server answers in questions 1, 3, and 4 (a server’s declared tool set is atomic: fixed at protect time, breaks as a whole if a member vanishes, and is cleared as a whole by unprotect) remain accurate for that one server; only the “a project has one protected route” claim in question 2 is superseded and is retained there as a dated historical record, not current guidance.

1. Additive or declared as a set?

Answer. Protection is declared as the complete set for one server; a later seal protect refuses while that server is protected instead of adding tools.

Evidence. spine/protection.cjs:651-662 deduplicates the requested list and refuses already_protected for every existing state except UNPROTECTED; :691-712 writes that complete list as guardTools in one project state.

Observation. Run with a test MCP server advertising db.execute_sql, db.drop_table, and db.read:

seal protect db db.execute_sql
seal protect db db.drop_table

Sealed MCP route db: PENDING RESTART (/home/you/.local/share/seal/projects/a055aba8ce9cbe0bd8bbe684f394297b/state.json)

Gated through this route:
  db.execute_sql

Not controlled:
  Bash and subprocesses outside this MCP route
  direct resource access outside this MCP route
  other clients
  other MCP servers not routed through this Seal wrapper
  other uncontrolled routes can also exist
exit 0
seal: REFUSE already_protected: project is already PENDING RESTART
exit 1

This test server advertises the full tool name db.execute_sql. The indented line prints that declared name alone; it does not prepend the server name db.

2. What does seal status show per tool?

Answer. For a protected route, seal status shows one shared server state and, under Gated through this route:, each guarded tool’s declared name alone on its own two-space-indented line, whether one tool or several were declared. The tools on one server share that server’s one state and one lease. A second protect for the same server refuses; neither invocation adds to the guarded set.

Historical (dated 2026-09-08 against the v0.3.0 artifact, superseded — see the note above). At that commit, a project admitted only one protected route: with two configured servers, a second seal protect for the other server refused, and status listed that server under Not controlled. A later release lifted that limit: protecting one server no longer blocks protecting a different server in the same project; see the current-behavior note above and Several servers in one project.

Evidence. In that captured release, bin/seal obtains one protection view, prints the route state followed by the indented guarded names, and prints the one view.lease; spine/protection.cjs:12-19 defines the six shared state values.

Observation. After protecting three advertised tools:

seal status

Sealed MCP route db: PENDING RESTART (/home/you/.local/share/seal/projects/a055aba8ce9cbe0bd8bbe684f394297b/state.json)

Gated through this route:
  db.execute_sql
  db.drop_table
  db.read

Not controlled:
  Bash and subprocesses outside this MCP route
  direct resource access outside this MCP route
  other clients
  other MCP servers not routed through this Seal wrapper
  other uncontrolled routes can also exist
exit 0

There is one PENDING RESTART value for the set, not three per-tool rows.

3. What happens when one of three tools vanishes at activation?

Answer. The whole server protection becomes BROKEN; Seal does not activate the two remaining guarded tools as a partial set.

Evidence. spine/protection.cjs:794-818 re-runs tools/list, collects every guarded name that vanished, calls markBroken, and refuses activation; :766-769 writes BROKEN into the single shared state and clears its lease.

Observation. db.drop_table was removed from the server’s advertised list after a successful three-tool protect and before starting the proxy:

seal __proxy --protect-state <state>

seal __proxy: protected_tool_vanished: protected tool "db.drop_table" vanished before activation; observed tools: db.execute_sql, db.read
exit 1

Stored-state readback:

BROKEN

4. Does unprotecting one tool touch the others’ leases?

Answer. There is no per-tool unprotect or per-tool lease: seal unprotect SERVER removes the entire declared set and clears the server’s one shared lease.

Evidence. bin/seal:326-332 accepts the server name and reports protection outside Seal; spine/protection.cjs:730-749 checks the one state.lease, removes the server override, writes UNPROTECTED, and sets that lease to null.

Observation. A three-tool wrapper was activated and allowed to exit, leaving one dead shared generation, before server-level unprotect:

state=ACTIVE guardTools=["db.execute_sql","db.drop_table","db.read"] sharedLeaseGeneration=1

seal unprotect db

Sealed MCP route db: - outside Seal (/home/you/.local/share/seal/projects/a055aba8ce9cbe0bd8bbe684f394297b/state.json)

Gated through this route:
  none

Not controlled:
  Bash and subprocesses outside this MCP route
  direct resource access outside this MCP route
  other clients
  other MCP servers not routed through this Seal wrapper
  other uncontrolled routes can also exist
exit 0

Stored-state readback after the command:

state=UNPROTECTED guardTools=["db.execute_sql","db.drop_table","db.read"] sharedLease=null

The historical names remain in the record, but none remains protected because the only state is UNPROTECTED and the only lease is null.

State-space count

The shipped multi-tool state machine admits six semantic state classes: UNPROTECTED, PENDING RESTART, ACTIVE, STALE, DRIFTED, and BROKEN. This is the count at the abstraction used by STATES in spine/protection.cjs:12-19. Concrete tool-name sets are unbounded, so counting each possible set of strings as a different configuration would not produce a finite product-state count.

The four answers keep the semantic count at six rather than multiplying it per tool: protection replaces no member independently, status exposes one shared value, one vanished member breaks the whole set, and unprotect clears the whole set and its shared lease. STALE is a status view of an ACTIVE record whose lease is dead (spine/protection.cjs:629-639), but it is a distinct value the shipped status state machine admits and displays.

Multi-tool coverage

All six state classes are exercised with a guarded set containing more than one distinct tool. Four tests use the same declaration of three distinct tools and observe the guarded set after the state transition.

State class	Multi-tool coverage	Existing test
UNPROTECTED	Yes	UNPROTECTED guards none of a former three-tool declaration and clears its shared lease in test/multi-tool-semantics-doc.test.cjs.
PENDING RESTART	Yes	three protected tools round-trip through stored state (lines 159-169).
ACTIVE	Yes	a named tool list gives both tools separate asks (lines 92-128); starting its proxy activates the shared lease before the calls.
STALE	Yes	STALE exposes one complete three-tool guard set for a dead shared lease in test/multi-tool-semantics-doc.test.cjs.
DRIFTED	Yes	DRIFTED guards the complete three-tool declaration after server configuration changes in test/multi-tool-semantics-doc.test.cjs.
BROKEN	Yes	BROKEN guards the complete three-tool declaration after one member vanishes in test/multi-tool-semantics-doc.test.cjs.

The tests for STALE, DRIFTED, and BROKEN assert that the observed guarded names equal the declared three-tool set. The UNPROTECTED test first observes that complete set after a real wrapper activation, then unprotects the server and asserts through the product view that no declared member remains guarded. A later protect test also observes the stored guarded set after replacement is refused. The shared set-comparison helper has its own known-incomplete input check, and the post-unprotect set assertion has a one-member-still-guarded check.

Verdict on “The state machine is TESTED”

The state machine is TESTED across all six shared multi-tool state classes. This badge reports behavioral test observations. The four added state tests use three distinct tools, and physical tamper runs showed each targeted test failing with the omitted tool named when its state exposed only two guarded members.

Document/code disagreements

• docs/guide/choosing-what-to-protect.md:3-5,35-42 says Seal protects exactly one tool and that the gate holds one name. The code accepts TOOL [TOOL...] and stores a nonempty list (bin/seal:290-317 and spine/protection.cjs:651-712).
• README.md:7-9, docs/guide/README.md:3,94, and docs/README.md:74-75 describe one protected tool. That is narrower than the shipped named-set behavior.
• docs/guide/what-is-protected-right-now.md:21-29 documents the protection route followed by each guarded tool name on its own indented line, which matches the shipped multi-tool status format.
• Roadmap section 17.10, lines 11418-11425, says disappearance after protect is open. Current spine/protection.cjs:794-818 implements the activation-time re-check and whole-server BROKEN result. The troubleshooting guide at docs/guide/when-something-looks-wrong.md:349-354 agrees with the current code, although it describes the guarded tool in the singular.
• Roadmap section 17.10 labels the status behavior “per tool.” Its braces example matched bin/seal at v0.2.0-rc.3; it no longer matches the shipped code, which prints one route heading and one indented tool name per line. The code supplies one shared state and one shared lease, not independent per-tool status values.

UNVERIFIED

The protection state machine has no machine-checked model in the seal-host Lean kernel. The coverage verdict is based on the shipped CLI and product spine test paths; no external Claude Code acceptance claim is made here.

Previous: Receipt operations. Up: Reference. Next: Receipt operations vector set v1.