From f17b42d2f8eebecd0a334fe8d811ac4a60f04ee0 Mon Sep 17 00:00:00 2001 From: Vignesh Date: Mon, 16 Feb 2026 23:52:24 -0800 Subject: [PATCH] CI: remove formal models conformance workflow (#19007) --- .github/workflows/formal-conformance.yml | 139 ----------------------- 1 file changed, 139 deletions(-) delete mode 100644 .github/workflows/formal-conformance.yml diff --git a/.github/workflows/formal-conformance.yml b/.github/workflows/formal-conformance.yml deleted file mode 100644 index 8ba6d7e56b8..00000000000 --- a/.github/workflows/formal-conformance.yml +++ /dev/null @@ -1,139 +0,0 @@ -name: Formal models (informational conformance) - -on: - pull_request: - -concurrency: - group: formal-conformance-${{ github.event.pull_request.number || github.ref_name }} - cancel-in-progress: true - -jobs: - formal_conformance: - runs-on: ubuntu-latest - timeout-minutes: 20 - permissions: - contents: read - pull-requests: write - - steps: - - name: Checkout openclaw (PR) - uses: actions/checkout@v4 - with: - path: openclaw - - - name: Checkout formal models - uses: actions/checkout@v4 - with: - repository: vignesh07/clawdbot-formal-models - ref: main - path: clawdbot-formal-models - - - name: Setup Node - uses: actions/setup-node@v4 - with: - node-version: "22" - - - name: Regenerate extracted constants from openclaw - run: | - set -euo pipefail - cd clawdbot-formal-models - export OPENCLAW_REPO_DIR="${GITHUB_WORKSPACE}/openclaw" - node scripts/extract-tool-groups.mjs - node scripts/check-tool-group-alias.mjs - - # Drift is about extracted artifacts only; compute it before model checking - # to avoid any incidental file touches affecting the result. - - name: Compute drift (generated/*) - id: drift - run: | - set -euo pipefail - cd clawdbot-formal-models - - if git diff --quiet -- generated; then - echo "drift=false" >> "$GITHUB_OUTPUT" - exit 0 - fi - - echo "drift=true" >> "$GITHUB_OUTPUT" - git diff -- generated > "${GITHUB_WORKSPACE}/formal-models-drift.diff" - - - 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 \ - queue-drain delivery-route-stability delivery-pipeline retry-termination retry-eventual-success \ - no-cross-stream multi-event-eventual-emission \ - dedupe-collision-fallback crash-restart-dedupe two-worker-dedupe openclaw-session-key-conformance \ - routing-thread-parent-channel-override routing-trirule gateway-auth-proxy-header-spoof \ - 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 \ - queue-drain delivery-route-stability-negative delivery-pipeline-negative retry-termination-negative retry-eventual-success-negative \ - no-cross-stream-negative multi-event-eventual-emission-negative \ - dedupe-collision-fallback-negative crash-restart-dedupe-negative two-worker-dedupe-negative openclaw-session-key-conformance-negative \ - routing-thread-parent-channel-override-negative routing-trirule-negative gateway-auth-proxy-header-spoof-negative - - - name: Upload drift diff artifact - if: steps.drift.outputs.drift == 'true' - uses: actions/upload-artifact@v4 - with: - name: formal-models-conformance-drift - path: formal-models-drift.diff - - - name: Comment on PR (informational) - if: steps.drift.outputs.drift == 'true' - continue-on-error: true - uses: actions/github-script@v7 - with: - script: | - const body = [ - '⚠️ **Formal models conformance drift detected**', - '', - 'The formal models extracted constants (`generated/*`) do not match this openclaw PR.', - '', - 'This check is **informational** (not blocking merges yet).', - 'See the `formal-models-conformance-drift` artifact for the diff.', - '', - 'If this change is intentional, follow up by updating the formal models repo or regenerating the extracted artifacts there.', - ].join('\n'); - - await github.rest.issues.createComment({ - owner: context.repo.owner, - repo: context.repo.repo, - issue_number: context.payload.pull_request.number, - body, - }); - - - name: Summary - run: | - if [ "${{ steps.drift.outputs.drift }}" = "true" ]; then - echo "Formal conformance drift detected (informational)." - else - echo "Formal conformance: no drift." - fi