mirror of
https://github.com/openclaw/openclaw.git
synced 2026-03-12 07:20:45 +00:00
refactor: rename to openclaw
This commit is contained in:
@@ -1,16 +1,16 @@
|
||||
---
|
||||
title: Formal Verification (Security Models)
|
||||
summary: Machine-checked security models for Moltbot’s highest-risk paths.
|
||||
summary: Machine-checked security models for OpenClaw’s highest-risk paths.
|
||||
permalink: /security/formal-verification/
|
||||
---
|
||||
|
||||
# Formal Verification (Security Models)
|
||||
|
||||
This page tracks Moltbot’s **formal security models** (TLA+/TLC today; more as needed).
|
||||
This page tracks OpenClaw’s **formal security models** (TLA+/TLC today; more as needed).
|
||||
|
||||
> Note: some older links may refer to the previous project name.
|
||||
|
||||
**Goal (north star):** provide a machine-checked argument that Moltbot enforces its
|
||||
**Goal (north star):** provide a machine-checked argument that OpenClaw enforces its
|
||||
intended security policy (authorization, session isolation, tool gating, and
|
||||
misconfiguration safety), under explicit assumptions.
|
||||
|
||||
@@ -18,11 +18,11 @@ misconfiguration safety), under explicit assumptions.
|
||||
- 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.
|
||||
|
||||
**What this is not (yet):** a proof that “Moltbot is secure in all respects” or that the full TypeScript implementation is correct.
|
||||
**What this is not (yet):** a proof that “OpenClaw is secure in all respects” or that the full TypeScript implementation is correct.
|
||||
|
||||
## Where the models live
|
||||
|
||||
Models are maintained in a separate repo: [vignesh07/clawdbot-formal-models](https://github.com/vignesh07/clawdbot-formal-models).
|
||||
Models are maintained in a separate repo: [vignesh07/openclaw-formal-models](https://github.com/vignesh07/openclaw-formal-models).
|
||||
|
||||
## Important caveats
|
||||
|
||||
@@ -39,8 +39,8 @@ Today, results are reproduced by cloning the models repo locally and running TLC
|
||||
Getting started:
|
||||
|
||||
```bash
|
||||
git clone https://github.com/vignesh07/clawdbot-formal-models
|
||||
cd clawdbot-formal-models
|
||||
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.
|
||||
|
||||
Reference in New Issue
Block a user