Formal Verification Security Models for OpenClaw

OpenClaw's formal security models (currently TLA+/TLC) provide a machine-checked rationale that certain high-risk areas, namely authorization, session isolation, tool gating, and misconfiguration safety, uphold their intended policies, given explicitly stated assumptions.

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

What this is

An executable, attacker-driven security regression suite:

• Every claim comes with a runnable model-check over a finite state space.
• For many claims, a paired negative model exists that yields a counterexample trace for a realistic bug class.

This is not a guarantee that OpenClaw is secure in every way, nor does it cover the complete TypeScript implementation.

Where the models live

Models lived in a separate repository: vignesh07/openclaw-formal-models.

Note

That repository is currently inaccessible (GitHub shows "Repository not found" as of this writing). If it remains broken for you, reach out in the OpenClaw maintainer channels for the current location before concluding the models were removed.

Caveats

• These are models, not the full TypeScript implementation, so drift between model and code is possible.
• Outcomes are limited by the state space TLC explores. A green result does not imply security beyond the modeled assumptions and bounds.
• Certain claims depend on explicit environment assumptions (for instance, proper deployment and valid configuration inputs).

Reproducing results

Reproduction steps are unavailable while the previously documented models repository is not publicly reachable. Ask in the OpenClaw maintainer channels for a verified current location before trying the targets below.

No CI integration exists in this repo yet; a later iteration might 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 enable remote compromise and raises exposure; a token/password blocks unauthenticated attackers, according to 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 needs (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 honor TTL and pending-request limits.

Ingress gating (mentions and control-command bypass)

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

Routing and session-key isolation

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

v1++ models: concurrency, retries, trace correctness

Follow-on models that improve 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, meaning check-then-write must be atomic or locked, and refresh must not create duplicates. Concretely: concurrent requests cannot go beyond MaxPending for a channel, and repeated requests or refreshes for the same (channel, sender) do not produce duplicate live pending rows.

Ingress trace correlation and idempotency

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

Routing dmScope precedence and identityLinks

Claim: dmScope precedence and identity links behave deterministically: the default main scope shares one rolling session across a single owner's DMs (the personal-agent default), while any configured isolating scope (per-peer, per-channel-peer, per-account-channel-peer) keeps DM sessions strictly separated. Channel-specific dmScope overrides win over global defaults; identityLinks collapse sessions only within explicit linked groups, not across unrelated peers. Multi-user inboxes are expected to opt into an isolating scope (the runtime security audit recommends this when it detects multi-user DM traffic).

Related

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