From e487fe2fc411548a4c211b6713477546c45bda51 Mon Sep 17 00:00:00 2001 From: vignesh07 Date: Mon, 26 Jan 2026 20:16:33 -0800 Subject: [PATCH] docs(security): improve formal verification page reproducibility --- docs/security/formal-verification.md | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/docs/security/formal-verification.md b/docs/security/formal-verification.md index b88c17eba..e2704e7b3 100644 --- a/docs/security/formal-verification.md +++ b/docs/security/formal-verification.md @@ -20,7 +20,7 @@ misconfiguration safety), under explicit assumptions. ## Where the models live -Models are maintained in a separate repo: `vignesh07/clawdbot-formal-models`. +Models are maintained in a separate repo: . ## Important caveats @@ -34,16 +34,21 @@ Today, results are reproduced by cloning the models repo locally and running TLC - CI-run models with public artifacts (counterexample traces, run logs) - a hosted “run this model” workflow for small, bounded checks -From the models repo: +Getting started: ```bash -export PATH="/opt/homebrew/opt/openjdk@21/bin:$PATH" # or any Java 11+ +git clone https://github.com/vignesh07/clawdbot-formal-models +cd clawdbot-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. + make ``` ### Gateway exposure and open gateway misconfiguration -**Claim:** binding beyond loopback without auth makes remote compromise reachable; token/password blocks unauth attackers (per the model assumptions). +**Claim:** binding beyond loopback without auth can make remote compromise possible / increases exposure; token/password blocks unauth attackers (per the model assumptions). - Green runs: - `make gateway-exposure-v2`