Formal Verification of Security Models for OpenClaw

OpenClaw's formal security models (currently TLA+/TLC) provide a machine-verified argument that specific high-risk paths (authorization, session isolation, tool gating, and misconfiguration safety) enforce their intended policy, given clearly stated assumptions.

Note: some older links may point to the former project name.

What this is

An executable, attacker-driven security regression suite:

• Every claim includes a runnable model check across a finite state space.
• Most claims also include a negative model that produces a counterexample trace for a realistic bug category.

This is not a proof that OpenClaw is secure in every way, nor does it verify the full TypeScript implementation.

Where the models live

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

Note

That repository is currently inaccessible (GitHub returns "Repository not found" as of this writing). If it remains unavailable for you, ask in the OpenClaw maintainer channels for the current location before assuming the models were removed.

Caveats

• These are models, not the complete TypeScript code. Drift between the model and the actual code is possible.
• Results are constrained by the state space TLC explores. A green result does not imply security beyond the modeled assumptions and bounds.
• Some claims depend on explicit environment assumptions (for instance, correct deployment and valid configuration inputs).

Reproducing results

Clone the models repository and run TLC:

git clone https://github.com/vignesh07/openclaw-formal-models
cd 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 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 authentication can enable remote compromise and increases exposure. A token or 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 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 limits.

Ingress gating (mentions and control-command bypass)

Claim: in group contexts that require mention, an unauthorized control command cannot bypass 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. Check-then-write must be atomic or locked, and refresh must not create duplicates. Concretely: concurrent requests cannot exceed MaxPending for a channel, and repeated requests or 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 retains the same trace or event identity. Retries do not double-process. If provider event IDs are missing, deduplication 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