diff --git a/README.md b/README.md
index 71347925..b4953626 100644
--- a/README.md
+++ b/README.md
@@ -22,7 +22,6 @@ flowchart TB
cliRuntime["ServerRuntime
single workspace"]
cliAdapter --> cliRuntime
end
- shared["shared typed operations
admission + dispatch"]
subgraph mcpOwner["MCP lifetime"]
direction TB
mcpAdapter["lean-beam-mcp
multiplexed stdio"]
@@ -37,15 +36,14 @@ flowchart TB
cli --> cliAdapter
mcp --> mcpAdapter
- cliRuntime -. uses .-> shared
- mcpRuntime -. uses .-> shared
cliRuntime -- Beam requests --> backends
mcpRuntime -- Beam requests --> backends
```
Beam keeps the agent-facing surface small. The CLI and MCP paths share typed operations and broker
runtime code, but each owns its transport and runtime lifetime. Those runtime instances own request
-routing plus one or more Lean LSP sessions with the Beam plugin loaded.
+routing plus one or more Lean LSP sessions with the Beam plugin loaded. See the
+[architecture message paths](docs/ARCHITECTURE.md) for the complete component and lifetime flows.
Beam lets a client try Lean commands or tactics at specific positions in saved files without
changing those files. The central Beam extension is speculative execution through
diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md
new file mode 100644
index 00000000..d404471d
--- /dev/null
+++ b/docs/ARCHITECTURE.md
@@ -0,0 +1,53 @@
+# Beam Architecture
+
+Beam has two user-facing paths into the same typed Lean operations, but it does not share their
+transport or lifetime coordination. The CLI owns a project session through a foreground
+`lean-beam serve` process and a private daemon. The MCP server owns its broker runtime directly and
+multiplexes calls over JSON-RPC on standard input and output.
+
+The diagrams in this document are generated from the adjacent Graphviz sources. Update and render
+both forms together when a component or message path changes. From the repository root, run:
+
+```bash
+dot -Tsvg docs/architecture/message-paths.dot -o docs/architecture/message-paths.svg
+dot -Tsvg docs/architecture/configuration-flow.dot -o docs/architecture/configuration-flow.svg
+```
+
+## Message Paths
+
+[Open the rendered message-path diagram](architecture/message-paths.svg), or inspect its
+[Graphviz source](architecture/message-paths.dot).
+
+
+
+The CLI session descriptor selects one generation and contains its TCP endpoint and capability.
+An ordinary CLI operation reads that descriptor, verifies the daemon generation from the
+same-connection greeting, and only then sends its capability-bound request. The foreground owner
+alone creates the session and supervises normal shutdown. `status`, `stop`, and `recover` are
+explicit lifecycle paths rather than Lean operations.
+
+The MCP process does not attach to the CLI daemon. It owns an in-process `ServerRuntime`, resolves
+workspace descriptors from MCP tool arguments, and lazily owns the corresponding backend sessions.
+CLI and MCP reuse operation and runtime implementation, but each arrow in the diagram belongs to a
+separate runtime instance.
+
+## Backend Configuration Flow
+
+[Open the rendered configuration-flow diagram](architecture/configuration-flow.svg), or inspect
+its [Graphviz source](architecture/configuration-flow.dot).
+
+
+
+`DesiredConfig` is the internal wrapper-session configuration. Every configured Lean backend owns
+its command, plugin, toolchain, and bundle identity together. Temporary Rocq support is represented
+as either an optional companion to Lean or the sole backend; an empty backend set and partial Lean
+configuration cannot be constructed.
+
+The session configuration hash is a pure projection of `DesiredConfig`, not separately stored
+derived state. The established field order remains stable while the value cannot disagree with the
+root, backend set, or daemon binary from which it was computed.
+
+The option-heavy `WorkspaceBinding` remains a private descriptor and daemon-startup wire format.
+It is produced only by lowering a complete `BackendSet`. This keeps protocol compatibility at the
+edge without spreading independently optional Lean fields through configuration resolution,
+hashing, daemon startup, and MCP setup output.
diff --git a/docs/DEVELOPMENT.md b/docs/DEVELOPMENT.md
index 543b9655..ba74dfa4 100644
--- a/docs/DEVELOPMENT.md
+++ b/docs/DEVELOPMENT.md
@@ -29,6 +29,8 @@ If the question is "how do I work on the repo safely and efficiently?", start he
## Code Organization
+- [Architecture](ARCHITECTURE.md): rendered component message paths, runtime lifetimes, and wrapper
+ backend-configuration flow.
- `Beam.LSP`: Lean LSP server plugin code, including the `$/lean/runAt` request for speculative
execution at saved document positions.
- `Beam`: shared broker, CLI, and MCP layer over Lean LSP plus Beam-specific extensions.
diff --git a/docs/architecture/configuration-flow.dot b/docs/architecture/configuration-flow.dot
new file mode 100644
index 00000000..9512950a
--- /dev/null
+++ b/docs/architecture/configuration-flow.dot
@@ -0,0 +1,61 @@
+digraph BeamConfigurationFlow {
+ graph [
+ rankdir=LR,
+ bgcolor="#ffffff",
+ fontname="sans-serif",
+ fontsize=18,
+ label="Wrapper backend configuration flow",
+ labelloc=t,
+ nodesep=0.45,
+ ranksep=0.75,
+ pad=0.2
+ ];
+ node [
+ shape=box,
+ style="rounded,filled",
+ fillcolor="#f7f8fa",
+ color="#52606d",
+ fontname="sans-serif",
+ fontsize=11,
+ margin="0.16,0.10"
+ ];
+ edge [color="#52606d", fontname="sans-serif", fontsize=9];
+
+ root [label="canonical project root"];
+ required [label="required backend"];
+ resolver [label="desiredConfig", fillcolor="#e8f1fb"];
+ lean_resolve [label="resolve Lean bundle"];
+ rocq_resolve [label="resolve temporary Rocq command"];
+ lean_config [
+ label="LeanBackendConfig\ncommand + plugin\ntoolchain + bundleId",
+ fillcolor="#e8f5eb"
+ ];
+ rocq_config [label="RocqBackendConfig\ncommand", fillcolor="#e8f5eb"];
+ backend_set [
+ label="BackendSet\nnonempty and complete",
+ shape=hexagon,
+ fillcolor="#fff6db"
+ ];
+ desired [
+ label="DesiredConfig\nroot + backends + daemonBin",
+ fillcolor="#e8f1fb"
+ ];
+ hash [label="derived configuration hash\nstable ordered fields"];
+ args [label="daemon arguments"];
+ binding [label="WorkspaceBinding\nprivate wire shape"];
+ mcp_config [label="mcp-config output"];
+
+ root -> resolver;
+ required -> resolver;
+ resolver -> lean_resolve;
+ resolver -> rocq_resolve;
+ lean_resolve -> lean_config;
+ rocq_resolve -> rocq_config;
+ lean_config -> backend_set;
+ rocq_config -> backend_set;
+ backend_set -> desired;
+ desired -> hash;
+ desired -> args;
+ desired -> binding;
+ desired -> mcp_config;
+}
diff --git a/docs/architecture/configuration-flow.svg b/docs/architecture/configuration-flow.svg
new file mode 100644
index 00000000..e543edfb
--- /dev/null
+++ b/docs/architecture/configuration-flow.svg
@@ -0,0 +1,177 @@
+
+
+
+
+
diff --git a/docs/architecture/message-paths.dot b/docs/architecture/message-paths.dot
new file mode 100644
index 00000000..0d807f8b
--- /dev/null
+++ b/docs/architecture/message-paths.dot
@@ -0,0 +1,90 @@
+digraph BeamMessagePaths {
+ graph [
+ rankdir=LR,
+ bgcolor="#ffffff",
+ fontname="sans-serif",
+ fontsize=18,
+ label="Beam message paths",
+ labelloc=t,
+ nodesep=0.55,
+ ranksep=0.75,
+ pad=0.2
+ ];
+ node [
+ shape=box,
+ style="rounded,filled",
+ fillcolor="#f7f8fa",
+ color="#52606d",
+ fontname="sans-serif",
+ fontsize=11,
+ margin="0.16,0.10"
+ ];
+ edge [color="#52606d", fontname="sans-serif", fontsize=9];
+
+ subgraph cluster_callers {
+ label="Callers";
+ color="#9fb3c8";
+ style="rounded,dashed";
+ human [label="Human or agent shell"];
+ mcp_client [label="MCP client / agent"];
+ { rank=same; human; mcp_client; }
+ }
+
+ subgraph cluster_cli {
+ label="CLI-owned project session";
+ color="#3e7cb1";
+ style="rounded";
+ wrapper [label="scripts/lean-beam\nruntime discovery", fillcolor="#e8f1fb"];
+ cli [label="beam-cli\ncommands and foreground owner", fillcolor="#e8f1fb"];
+ descriptor [
+ label="private session descriptor\ngeneration + endpoint + capability",
+ shape=cylinder,
+ style="filled",
+ fillcolor="#fff6db"
+ ];
+ daemon [label="beam-daemon\nTCP transport", fillcolor="#e8f1fb"];
+ cli_runtime [label="ServerRuntime\nfrozen project workspace", fillcolor="#e8f1fb"];
+
+ wrapper -> cli [label="exec"];
+ cli -> daemon [
+ label="serve: spawn + owner pipe\nconnect + capability-bound operation\nauthenticated stop\ninterrupt: close connection"
+ ];
+ daemon -> cli [
+ label="typed ready message\nServerHello: generation identity\nprogress, diagnostics, response"
+ ];
+ cli -> descriptor [
+ label="publish / read lifecycle state\nordinary call: select session",
+ dir=both
+ ];
+ daemon -> cli_runtime;
+ }
+
+ subgraph cluster_mcp {
+ label="MCP-owned multi-workspace session";
+ color="#7a5195";
+ style="rounded";
+ mcp [label="lean-beam-mcp\nJSON-RPC stdio transport", fillcolor="#f1eafa"];
+ projection [label="MCP tool projection\nworkspace selection", fillcolor="#f1eafa"];
+ mcp_runtime [label="ServerRuntime\nlazy workspace cache", fillcolor="#f1eafa"];
+
+ mcp -> projection [label="tool call / result", dir=both];
+ projection -> mcp_runtime [label="typed operation / result", dir=both];
+ mcp -> mcp_runtime [label="cancel notification", style=dashed];
+ }
+
+ subgraph cluster_backends {
+ label="Workspace backends";
+ color="#4c956c";
+ style="rounded";
+ lean [label="Lean language server\nBeam LSP plugin", fillcolor="#e8f5eb"];
+ rocq [label="coq-lsp\ntemporary Rocq path", fillcolor="#e8f5eb"];
+ { rank=same; lean; rocq; }
+ }
+
+ human -> wrapper;
+ mcp_client -> mcp [label="JSON-RPC stdio", dir=both];
+ cli_runtime -> lean [label="LSP requests and notifications", dir=both];
+ cli_runtime -> rocq [label="goal probes", dir=both];
+ mcp_runtime -> lean [label="LSP requests and notifications", dir=both];
+ mcp_runtime -> rocq [label="goal probes", dir=both];
+}
diff --git a/docs/architecture/message-paths.svg b/docs/architecture/message-paths.svg
new file mode 100644
index 00000000..8a66b2b6
--- /dev/null
+++ b/docs/architecture/message-paths.svg
@@ -0,0 +1,227 @@
+
+
+
+
+