refactor: rename clawdbot to moltbot with legacy compat
This commit is contained in:
@@ -1,14 +1,14 @@
|
||||
---
|
||||
title: Formal Verification (Security Models)
|
||||
summary: Machine-checked security models for Clawdbot’s highest-risk paths.
|
||||
summary: Machine-checked security models for Moltbot’s highest-risk paths.
|
||||
permalink: /security/formal-verification/
|
||||
---
|
||||
|
||||
# Formal Verification (Security Models)
|
||||
|
||||
This page tracks Clawdbot’s **formal security models** (TLA+/TLC today; more as needed).
|
||||
This page tracks Moltbot’s **formal security models** (TLA+/TLC today; more as needed).
|
||||
|
||||
**Goal (north star):** provide a machine-checked argument that Clawdbot enforces its
|
||||
**Goal (north star):** provide a machine-checked argument that Moltbot enforces its
|
||||
intended security policy (authorization, session isolation, tool gating, and
|
||||
misconfiguration safety), under explicit assumptions.
|
||||
|
||||
@@ -16,11 +16,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 “Clawdbot is secure in all respects” or that the full TypeScript implementation is correct.
|
||||
**What this is not (yet):** a proof that “Moltbot 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/moltbot-formal-models](https://github.com/vignesh07/moltbot-formal-models).
|
||||
|
||||
## Important caveats
|
||||
|
||||
@@ -37,8 +37,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/moltbot-formal-models
|
||||
cd moltbot-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