mirror of
https://github.com/openclaw/openclaw.git
synced 2026-05-06 14:20:44 +00:00
docs: typography hygiene + 1 in-body H1 removal across 6 pages
Replaced 84 typography characters (curly quotes, apostrophes, em/en dashes, non-breaking hyphens) with ASCII equivalents per docs/CLAUDE.md heading and content hygiene rules. - docs/gateway/tools-invoke-http-api.md: 14 chars; removed the duplicate '# Tools Invoke (HTTP)' H1 (Mintlify renders title from frontmatter; the in-body H1 with parens produced a brittle anchor). - docs/tools/browser-control.md: 14 chars - docs/security/formal-verification.md: 14 chars - docs/gateway/configuration-reference.md: 14 chars - docs/concepts/agent.md: 14 chars - docs/channels/qa-channel.md: 14 chars
This commit is contained in:
@@ -1,5 +1,5 @@
|
||||
---
|
||||
summary: Machine-checked security models for OpenClaw’s highest-risk paths.
|
||||
summary: Machine-checked security models for OpenClaw's highest-risk paths.
|
||||
title: Formal verification (security models)
|
||||
read_when:
|
||||
- Reviewing formal security model guarantees or limits
|
||||
@@ -7,7 +7,7 @@ read_when:
|
||||
permalink: /security/formal-verification/
|
||||
---
|
||||
|
||||
This page tracks OpenClaw’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.
|
||||
|
||||
@@ -20,7 +20,7 @@ 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 “OpenClaw 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
|
||||
|
||||
@@ -29,7 +29,7 @@ Models are maintained in a separate repo: [vignesh07/openclaw-formal-models](htt
|
||||
## Important caveats
|
||||
|
||||
- These are **models**, not the full TypeScript implementation. Drift between model and code is possible.
|
||||
- Results are bounded by the state space explored by TLC; “green” does not imply security beyond the modeled assumptions and bounds.
|
||||
- Results are bounded by the state space explored by TLC; "green" does not imply security beyond the modeled assumptions and bounds.
|
||||
- Some claims rely on explicit environmental assumptions (e.g., correct deployment, correct configuration inputs).
|
||||
|
||||
## Reproducing results
|
||||
@@ -37,7 +37,7 @@ Models are maintained in a separate repo: [vignesh07/openclaw-formal-models](htt
|
||||
Today, results are reproduced by cloning the models repo locally and running TLC (see below). A future iteration could offer:
|
||||
|
||||
- CI-run models with public artifacts (counterexample traces, run logs)
|
||||
- a hosted “run this model” workflow for small, bounded checks
|
||||
- a hosted "run this model" workflow for small, bounded checks
|
||||
|
||||
Getting started:
|
||||
|
||||
@@ -87,7 +87,7 @@ See also: `docs/gateway-exposure-matrix.md` in the models repo.
|
||||
|
||||
### Ingress gating (mentions + control-command bypass)
|
||||
|
||||
**Claim:** in group contexts requiring mention, an unauthorized “control command” cannot bypass mention gating.
|
||||
**Claim:** in group contexts requiring mention, an unauthorized "control command" cannot bypass mention gating.
|
||||
|
||||
- Green:
|
||||
- `make ingress-gating`
|
||||
@@ -109,11 +109,11 @@ These are follow-on models that tighten fidelity around real-world failure modes
|
||||
|
||||
### Pairing store concurrency / idempotency
|
||||
|
||||
**Claim:** a pairing store should enforce `MaxPending` and idempotency even under interleavings (i.e., “check-then-write” must be atomic / locked; refresh shouldn’t create duplicates).
|
||||
**Claim:** a pairing store should enforce `MaxPending` and idempotency even under interleavings (i.e., "check-then-write" must be atomic / locked; refresh shouldn't create duplicates).
|
||||
|
||||
What it means:
|
||||
|
||||
- Under concurrent requests, you can’t exceed `MaxPending` for a channel.
|
||||
- Under concurrent requests, you can't exceed `MaxPending` for a channel.
|
||||
- Repeated requests/refreshes for the same `(channel, sender)` should not create duplicate live pending rows.
|
||||
|
||||
- Green runs:
|
||||
|
||||
Reference in New Issue
Block a user