From c83c19d9cde8dcce93c06b7ac354f2b55dcbff84 Mon Sep 17 00:00:00 2001
From: vignesh07 <vigneshnatarajan92@gmail.com>
Date: Sun, 1 Feb 2026 01:11:52 -0800
Subject: [PATCH] ci(formal): run TLC model suite (green) + negative suite
 (non-blocking)

---
 .github/workflows/formal-conformance.yml | 36 +++++++++++++++++++++++-
 1 file changed, 35 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/formal-conformance.yml b/.github/workflows/formal-conformance.yml
index 04a5db5537..7a2fa63a6f 100644
--- a/.github/workflows/formal-conformance.yml
+++ b/.github/workflows/formal-conformance.yml
@@ -6,7 +6,7 @@ on:
 jobs:
   formal_conformance:
     runs-on: ubuntu-latest
-    timeout-minutes: 10
+    timeout-minutes: 20
     permissions:
       contents: read
       pull-requests: write
@@ -36,6 +36,40 @@ jobs:
           node scripts/extract-tool-groups.mjs
           node scripts/check-tool-group-alias.mjs
 
+      - name: Model check (green suite)
+        run: |
+          set -euo pipefail
+          cd clawdbot-formal-models
+          make \
+            precedence groups elevated nodes-policy \
+            attacker approvals approvals-token nodes-pipeline \
+            gateway-exposure gateway-exposure-v2 gateway-exposure-v2-protected \
+            gateway-auth-conformance gateway-auth-tailscale gateway-auth-proxy \
+            pairing pairing-cap pairing-idempotency pairing-refresh pairing-refresh-race \
+            ingress-gating ingress-idempotency ingress-dedupe-fallback ingress-trace ingress-trace2 \
+            routing-isolation routing-precedence routing-identitylinks routing-identity-transitive routing-identity-symmetry routing-identity-channel-override \
+            routing-thread-parent discord-pluralkit \
+            ingress-retry session-key-stability session-explosion-bound config-normalization \
+            group-alias-check
+
+      - name: Model check (negative suite, expected violations)
+        continue-on-error: true
+        run: |
+          set -euo pipefail
+          cd clawdbot-formal-models
+          make -k \
+            precedence-negative groups-negative elevated-negative nodes-policy-negative \
+            attacker-negative attacker-nodes-negative attacker-nodes-allowlist-negative attacker-nodes-allowlist-negative \
+            approvals-negative approvals-token-negative nodes-pipeline-negative \
+            gateway-exposure-negative gateway-exposure-v2-negative gateway-exposure-v2-protected-negative \
+            gateway-exposure-v2-unsafe-custom gateway-exposure-v2-unsafe-tailnet gateway-exposure-v2-unsafe-auto \
+            gateway-auth-conformance-negative gateway-auth-tailscale-negative gateway-auth-proxy-negative \
+            pairing-negative pairing-cap-negative pairing-idempotency-negative pairing-refresh-negative pairing-refresh-race-negative \
+            ingress-gating-negative ingress-idempotency-negative ingress-dedupe-fallback-negative ingress-trace-negative ingress-trace2-negative \
+            routing-isolation-negative routing-precedence-negative routing-identitylinks-negative routing-identity-transitive-negative routing-identity-symmetry-negative routing-identity-channel-override-negative \
+            routing-thread-parent-negative discord-pluralkit-negative \
+            ingress-retry-negative session-key-stability-negative config-normalization-negative
+
       - name: Compute drift
         id: drift
         run: |