Formal verification (security models)

OpenClaw's formal security models (TLA+/TLC today) give a machine-checked argument that specific highest-risk paths — authorization, session isolation, tool gating, and misconfiguration safety — enforce their intended policy, under explicit stated assumptions.

Note: some older links may refer to the previous project name.

What this is

An executable, attacker-driven security regression suite:

• Each claim has a runnable model-check over a finite state space.
• Many claims have a paired negative model that produces a counterexample trace for a realistic bug class.

This is not a proof that OpenClaw is secure in all respects, and it does not verify the full TypeScript implementation.

Where the models live

Models are maintained in a separate repo: vignesh07/openclaw-formal-models.

Caveats

• These are models, not the full TypeScript implementation — drift between model and code is possible.
• Results are bounded by the state space TLC explores. Green does not imply security beyond the modeled assumptions and bounds.
• Some claims rely on explicit environment assumptions (for example, correct deployment and correct configuration inputs).

Reproducing results

Clone the models repo and run TLC:

git clone https://github.com/vignesh07/openclaw-formal-modelscd openclaw-formal-models # Java 11+ required (TLC runs on the JVM).# The repo vendors a pinned tla2tools.jar and provides bin/tlc plus Make targets. make <target>

There is no CI integration back into this repo yet; a future iteration could add CI-run models with public artifacts (counterexample traces, run logs) or a hosted "run this model" workflow for small bounded checks.

Claims and targets

Gateway exposure and open gateway misconfiguration

Claim: binding beyond loopback without auth can make remote compromise possible and increases exposure; a token/password blocks unauthenticated attackers, per the model's assumptions.

See also docs/gateway-exposure-matrix.md in the models repo.

Node exec pipeline (highest-risk capability)

Claim: exec host=node requires (a) a node command allowlist plus declared commands and (b) live approval when configured; approvals are tokenized to prevent replay, in the model.

Pairing store (DM gating)

Claim: pairing requests respect TTL and pending-request caps.

Ingress gating (mentions and control-command bypass)

Claim: in group contexts requiring mention, an unauthorized control command cannot bypass mention gating.

Routing and session-key isolation

Claim: DMs from distinct peers do not collapse into the same session unless explicitly linked or configured.

v1++ models: concurrency, retries, trace correctness

Follow-on models that tighten fidelity around real-world failure modes: non-atomic updates, retries, and message fan-out.

Pairing store concurrency and idempotency

Claim: the pairing store enforces MaxPending and idempotency even under interleavings — check-then-write must be atomic/locked, and refresh must not create duplicates. Concretely: concurrent requests cannot exceed MaxPending for a channel, and repeated requests/refreshes for the same (channel, sender) do not create duplicate live pending rows.

Ingress trace correlation and idempotency

Claim: ingestion preserves trace correlation across fan-out and is idempotent under provider retries. When one external event becomes multiple internal messages, every part keeps the same trace/event identity; retries do not double-process; if provider event IDs are missing, dedupe falls back to a safe key (for example trace ID) to avoid dropping distinct events.

Routing dmScope precedence and identityLinks

Claim: routing keeps DM sessions isolated by default and only collapses sessions when explicitly configured, via channel precedence and identity links. Channel-specific dmScope overrides win over global defaults; identityLinks collapse sessions only within explicit linked groups, not across unrelated peers.

Related

• Threat model
• Contributing to the threat model
• Incident response