From 286b3caf2feab9e73a7b8913d2493d144da4990e Mon Sep 17 00:00:00 2001
From: vignesh07 <vigneshnatarajan92@gmail.com>
Date: Mon, 26 Jan 2026 19:54:21 -0800
Subject: [PATCH] docs(security): add formal verification page (draft)

---
 docs/security/formal-verification.md | 92 ++++++++++++++++++++++++++++
 1 file changed, 92 insertions(+)
 create mode 100644 docs/security/formal-verification.md

diff --git a/docs/security/formal-verification.md b/docs/security/formal-verification.md
new file mode 100644
index 000000000..6a12a2e78
--- /dev/null
+++ b/docs/security/formal-verification.md
@@ -0,0 +1,92 @@
+---
+title: Formal Verification (Security Models)
+summary: Machine-checked security models for Clawdbot’s highest-risk paths.
+status: draft
+---
+
+# Formal Verification (Security Models)
+
+This page tracks Clawdbot’s **formal security models** (TLA+/TLC today; more as needed).
+
+**Goal (north star):** provide a machine-checked argument that Clawdbot enforces its
+intended security policy (authorization, session isolation, tool gating, and
+misconfiguration safety), under explicit assumptions.
+
+**What this is (today):** an executable, attacker-driven **security regression suite**:
+- Each claim has a runnable model-check.
+- Most claims have a paired **negative model** that produces a counterexample trace for a realistic bug class.
+
+**What this is not (yet):** a proof that “Clawdbot is secure in all respects” or that the full TypeScript implementation is correct.
+
+## Where the models live
+
+Models are maintained in a separate repo: `vignesh07/clawdbot-formal-models`.
+
+## Reproducing results
+
+From the models repo:
+
+```bash
+export PATH="/opt/homebrew/opt/openjdk@21/bin:$PATH"  # or any Java 11+
+make <target>
+```
+
+### Gateway exposure / open gateway misconfig
+
+**Claim:** binding beyond loopback without auth makes remote compromise reachable; token/password blocks unauth attackers.
+
+- Green runs:
+  - `make gateway-exposure-v2`
+  - `make gateway-exposure-v2-protected`
+- Red (expected):
+  - `make gateway-exposure-v2-negative`
+
+See also: `docs/gateway-exposure-matrix.md` in the models repo.
+
+### Nodes.run pipeline (highest-risk capability)
+
+**Claim:** `nodes.run` requires (a) node command allowlist + declared commands and (b) live approval when configured; approvals are tokenized to prevent replay.
+
+- Green runs:
+  - `make nodes-pipeline`
+  - `make approvals-token`
+- Red (expected):
+  - `make nodes-pipeline-negative`
+  - `make approvals-token-negative`
+
+### Pairing store (DM gating)
+
+**Claim:** pairing requests respect TTL and pending-request caps.
+
+- Green runs:
+  - `make pairing`
+  - `make pairing-cap`
+- Red (expected):
+  - `make pairing-negative`
+  - `make pairing-cap-negative`
+
+### Ingress gating (mentions + control-command bypass)
+
+**Claim:** in group contexts requiring mention, an unauthorized “control command” cannot bypass mention gating.
+
+- Green:
+  - `make ingress-gating`
+- Red (expected):
+  - `make ingress-gating-negative`
+
+### Routing/session-key isolation
+
+**Claim:** DMs from distinct peers do not collapse into the same session unless explicitly linked/configured.
+
+- Green:
+  - `make routing-isolation`
+- Red (expected):
+  - `make routing-isolation-negative`
+
+## Roadmap
+
+Next models to deepen fidelity:
+- Pairing store concurrency/locking/idempotency
+- Provider-specific ingress preflight modeling
+- Routing identity-links + dmScope variants + binding precedence
+- Gateway auth conformance (proxy/tailscale specifics)