Verify OpenClaw Security Models with TLA+

You know that feeling when you’re building something sensitive and you just can’t shake the “what if” scenarios? You’ve written your tests, but security is tricky. One misconfiguration or a weird race condition, and suddenly your isolation is gone.

OpenClaw handles this by using formal security models (currently TLA+ and TLC). The goal is to have a machine-checked argument that OpenClaw actually enforces its security policy—covering authorization, session isolation, tool gating, and misconfiguration safety—based on explicit assumptions.

Right now, this acts as an executable, attacker-driven security regression suite. Every claim has a runnable model-check, and many include a “negative model” that shows exactly how a realistic bug would create a security hole. It isn’t a total proof that the TypeScript code is perfect, but it’s a massive step toward verifying the logic.

Where the models live

You can find all the models in a separate repository: vignesh07/openclaw-formal-models.

Important caveats

Before you dive in, keep a few things in mind:

• These are models, not the actual TypeScript implementation. It is possible for the code and the model to drift apart.
• Results are limited by the state space TLC explores. A “green” result means it’s secure within the modeled bounds and assumptions, not necessarily in every possible universe.
• Some claims assume your environment is set up correctly (like deployment and configuration inputs).

Reproducing results

If you want to see these results for yourself, clone the repo and run TLC locally. In the future, we might offer CI-run models or a hosted workflow for quick checks.

To get started:

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` (TLA+ tools) and provides `bin/tlc` + Make targets.

make <target>

Gateway exposure and open gateway misconfiguration

Claim: If you bind beyond loopback without auth, you risk remote compromise. The model assumes that tokens or passwords successfully block unauthorized attackers.

• Green runs:
  • make gateway-exposure-v2
  • make gateway-exposure-v2-protected
• Red (expected):
  • make gateway-exposure-v2-negative

Check out docs/gateway-exposure-matrix.md in the models repo for more details.

Node exec pipeline (highest-risk capability)

Claim: Running exec host=node requires two things: a node command allowlist with declared commands, and live approval when configured. The model ensures approvals use tokens to prevent replay attacks.

• 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 must respect TTL and limits on pending requests.

• 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 where a mention is required, an unauthorized “control command” cannot skip that requirement.

• Green:
  • make ingress-gating
• Red (expected):
  • make ingress-gating-negative

Routing/session-key isolation

Claim: DMs from different peers stay in separate sessions unless you explicitly link or configure them to merge.

• Green:
  • make routing-isolation
• Red (expected):
  • make routing-isolation-negative

v1++: additional bounded models (concurrency, retries, trace correctness)

These models go deeper into real-world issues like non-atomic updates, retries, message fan-out, and interleavings.

Pairing store concurrency / idempotency

Claim: The pairing store must enforce MaxPending and stay idempotent even when requests overlap. This means “check-then-write” operations have to be atomic or locked.

What this means for you:

• Concurrent requests won’t let you exceed the MaxPending limit for a channel.

• Sending the same request or refreshing for the same (channel, sender) won’t create duplicate rows.

• Green runs:

  • make pairing-race (atomic/locked cap check)
  • make pairing-idempotency
  • make pairing-refresh
  • make pairing-refresh-race

• Red (expected):

  • make pairing-race-negative (non-atomic begin/commit cap race)
  • make pairing-idempotency-negative
  • make pairing-refresh-negative
  • make pairing-refresh-race-negative

Ingress trace correlation / idempotency

Claim: Ingestion needs to keep trace correlation consistent across fan-outs and stay idempotent when providers retry.

What this means for you:

• If one external event turns into multiple internal messages, they all share the same trace identity.

• Retries won’t cause double-processing.

• If event IDs are missing, the system uses a safe fallback key (like the trace ID) to avoid dropping unique events.

• Green:

  • make ingress-trace
  • make ingress-trace2
  • make ingress-idempotency
  • make ingress-dedupe-fallback

• Red (expected):

  • make ingress-trace-negative
  • make ingress-trace2-negative
  • make ingress-idempotency-negative
  • make ingress-dedupe-fallback-negative

Routing dmScope precedence + identityLinks

Claim: Routing must isolate DM sessions by default. Sessions only merge when you explicitly configure channel precedence or identity links.

What this means for you:

• Channel-specific dmScope settings always beat global defaults.

• identityLinks only merge sessions within the specified groups, never for unrelated peers.

• Green:

  • make routing-precedence
  • make routing-identitylinks

• Red (expected):

  • make routing-precedence-negative
  • make routing-identitylinks-negative

Need help setting up your security configuration? Try the AI Setup Assistant.

Next steps

• Explore the OpenClaw Formal Models Repository
• Read the gateway-exposure-matrix.md for deployment best practices