OpenClaw

OpenClaw is an agent infrastructure and gateway platform aimed at developers who are building and operating AI agents across channels, tools, and models. From the documentation, it focuses heavily on security properties around authorization, session isolation, tool execution, and safe deployment configurations.

A core part of the offering is a set of formal security models written in TLA+ and checked with the TLC model checker. These models act as an executable, attacker-driven security regression suite that encodes specific claims about how OpenClaw should behave under various threat scenarios. To get started, you clone the separate openclaw-formal-models GitHub repository, ensure you have Java 11+ installed, and run make targets that invoke a vendored tla2tools.jar to explore bounded state spaces.

According to the documentation, the formal models cover concrete, high‑risk areas such as gateway exposure and misconfiguration, the nodes.run execution pipeline (including approval tokenization), pairing-store behavior for DM gating, ingress gating in group contexts, and routing/session-key isolation. Each claim has a “green” model that should pass under the intended design, and many have a paired “negative” model that demonstrates realistic failure modes via counterexample traces. This structure makes it useful both as a regression suite and as a way to reason about what can go wrong when configuration or assumptions are violated.

However, these are models, not the actual TypeScript implementation, and the docs are explicit that drift between the models and production code is possible. The checks are bounded by the explored state space, so a successful run does not prove global security—only that the modeled behavior holds under given assumptions and limits. Some claims also depend on correct deployment and configuration in the surrounding environment. There is mention of potential future CI integrations and hosted "run this model" workflows, but those are not available yet. Pricing and commercial terms for OpenClaw are not described in this documentation, so you should treat it as a technical security artifact rather than a complete product overview.