Skip to main content
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.
That repository is currently unreachable (GitHub returns “Repository not found” as of this writing). If it is still broken for you, ask in the OpenClaw maintainer channels for the current location before assuming the models were removed.

​
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:
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. 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.