zeekay
5abcc6c773
Superseded: the Hanzo GitHub App pushes a webhook, so the forge tracks GitHub without a per-repo workflow. This file called git.hanzo.ai/api/v1/.../mirror-sync — a Gitea API for a system we no longer drive — and would sit inert in every repo. One mechanism, in one place, instead of ~350 copies of a cron.
clawdbot-formal-models
Machine-checkable security models for Clawdbot, primarily in TLA+ checked with TLC.
This repo is intentionally practical: it acts as a security regression suite.
- Green models should pass (no invariant violation).
- Red models are deliberately buggy variants that should fail with a counterexample trace.
Quickstart (TLA+)
Prereqs:
- Java 11+ (Java 21 recommended)
Run a specific target:
make <target>
See docs/formal-models.md for the recommended “v1 publish” run set.
Structure
tla/specs/— TLA+ specstla/models/— TLC model configs / notestools/tla/— pinned TLA+ tool jar (tla2tools.jar)bin/tlc— convenience wrapper around TLCdocs/— design notes and threat-models
Conformance
Some checks are conformance-style: they validate that the formal model matches Clawdbot’s actual implementation constants.
Currently we extract tool-group expansions and tool-name aliases from:
../clawdbot/src/agents/tool-policy.ts
Generate the extracted constants:
node scripts/extract-tool-groups.mjs
Output:
generated/tool-groups.json
Key docs
docs/formal-models.md— how to run, interpret green/red, and suggested CI approachdocs/security-claims.md— claim inventorydocs/verification-roadmap.md— roadmap for expanding fidelity/coverage
Next steps
CI
Mode A (today): CI runs TLC targets directly in this repo (no dependency on the main Clawdbot repo).
Mode B (planned): add a conformance job that checks out clawdbot/clawdbot alongside this repo and regenerates extracted constants (e.g. tool-group expansions). CI fails if the generated artifacts drift from what is committed here.
- Add CI to run TLC on PRs and upload counterexample traces as artifacts.
- Deepen fidelity: pairing-store concurrency/locking, provider-specific ingress nuances, routing identity-link semantics.