MVP alpha.11: Close gaps for beta

.github/workflows/ci.yml

@@ -2,10 +2,15 @@ name: CI
 
 on:
   pull_request:
+  merge_group:
   push:
     branches:
       - main
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event_name }}-${{ github.event.number || github.ref }}
+  cancel-in-progress: ${{ github.event_name == 'pull_request' }}
+
 permissions:
   contents: read
 
@@ -18,8 +23,8 @@ jobs:
       matrix:
         include:
           - os: ubuntu-latest
-            label: ubuntu canonical
-            ci-target: ci
+            label: ubuntu required shared-linux perf
+            ci-target: ci-required-shared-linux
           - os: macos-latest
             label: macos portability
             ci-target: ci-portability
@@ -67,6 +72,74 @@ jobs:
             exit 1
           fi
 
+  formal-security-kernel:
+    name: Formal security kernel TLA
+    runs-on: ubuntu-latest
+    env:
+      NIX_CONFIG: |
+        substituters = https://cache.nixos.org
+        trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
+    steps:
+      - name: Checkout
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        with:
+          fetch-depth: 0
+
+      - name: Detect TLA-relevant PR changes
+        id: tla_changes
+        shell: bash
+        run: |
+          if [ "${{ github.event_name }}" != "pull_request" ]; then
+            echo "required=true" >> "$GITHUB_OUTPUT"
+            echo "mode=all" >> "$GITHUB_OUTPUT"
+            exit 0
+          fi
+
+          changed_files="$(git diff --name-only "${{ github.event.pull_request.base.sha }}" "${{ github.event.pull_request.head.sha }}")"
+          if grep -E '^(formal/tla/|tools/tlccheck/|justfile|\.github/workflows/ci\.yml)' <<< "$changed_files"; then
+            echo "required=true" >> "$GITHUB_OUTPUT"
+            echo "mode=all" >> "$GITHUB_OUTPUT"
+          elif grep -E '^(protocol/|internal/|cmd/|runner/|docs/trust-boundaries\.md|runecontext/standards/security/|runecontext/standards/global/|runecontext/changes/CHG-2026-015-[^/]+/)' <<< "$changed_files"; then
+            echo "required=true" >> "$GITHUB_OUTPUT"
+            echo "mode=core" >> "$GITHUB_OUTPUT"
+          else
+            echo "required=false" >> "$GITHUB_OUTPUT"
+            echo "mode=skip" >> "$GITHUB_OUTPUT"
+          fi
+
+      - name: Report TLA skip
+        if: github.event_name == 'pull_request' && steps.tla_changes.outputs.required != 'true'
+        run: echo "No security-kernel-relevant changes detected; TLA model check skipped for this PR diff."
+
+      - name: Install Nix
+        if: steps.tla_changes.outputs.required == 'true'
+        uses: DeterminateSystems/nix-installer-action@c5a866b6ab867e88becbed4467b93592bce69f8a # v21
+
+      - name: Cache Nix store
+        if: steps.tla_changes.outputs.required == 'true'
+        uses: DeterminateSystems/magic-nix-cache-action@565684385bcd71bad329742eefe8d12f2e765b39 # v13
+        with:
+          use-flakehub: false
+
+      - name: Run PR core TLA model check
+        if: github.event_name == 'pull_request' && steps.tla_changes.outputs.mode == 'core'
+        run: nix develop --no-write-lock-file -c just model-check-core
+
+      - name: Run full TLA model check
+        if: steps.tla_changes.outputs.mode == 'all'
+        run: nix develop --no-write-lock-file -c just model-check
+
+      - name: Verify repository unchanged after TLA check
+        if: steps.tla_changes.outputs.required == 'true'
+        run: |
+          git diff --exit-code
+          untracked="$(git ls-files --others --exclude-standard)"
+          if [ -n "$untracked" ]; then
+            echo "Untracked files found after TLA check:"
+            echo "$untracked"
+            exit 1
+          fi
+
   windows:
     name: Windows portability (Node ${{ matrix.node-version }})
     runs-on: windows-latest

.github/workflows/dco.yml

@@ -0,0 +1,52 @@
+name: DCO
+
+on:
+  pull_request:
+  merge_group:
+
+permissions:
+  contents: read
+
+jobs:
+  dco:
+    name: DCO
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        with:
+          fetch-depth: 0
+
+      - name: Validate DCO sign-offs
+        shell: bash
+        run: |
+          set -euo pipefail
+
+          if [ "${{ github.event_name }}" = "pull_request" ]; then
+            range="${{ github.event.pull_request.base.sha }}..${{ github.event.pull_request.head.sha }}"
+          else
+            range="HEAD^1..HEAD"
+          fi
+
+          commits="$(git rev-list --reverse "$range")"
+          if [ -z "$commits" ]; then
+            echo "No commits found in range $range"
+            exit 1
+          fi
+
+          missing=0
+          while IFS= read -r commit; do
+            [ -n "$commit" ] || continue
+            if ! git log -1 --format=%B "$commit" | grep -qi '^Signed-off-by: '; then
+              echo "Missing Signed-off-by trailer in commit $commit"
+              git log -1 --format='subject: %s%nauthor: %an <%ae>' "$commit"
+              missing=1
+            fi
+          done <<< "$commits"
+
+          if [ "$missing" -ne 0 ]; then
+            echo "One or more commits are missing DCO sign-off trailers."
+            exit 1
+          fi
+
+          echo "All commits in $range include DCO sign-off trailers."

CONTRIBUTING.md

@@ -60,7 +60,7 @@ The canonical local workflow uses Nix + `just`:
 - Prerequisite: Nix `>= 2.18`
 - Optional auto-entry: `direnv` + `nix-direnv`
 - Canonical command surface: `just`
-- CI runs one canonical `just ci` lane plus portability lanes (`just ci-portability`) to avoid duplicating model-check runtime cost across every matrix leg
+- CI runs fast canonical checks plus a dedicated Linux formal-security gate to avoid duplicating model-check runtime cost across every matrix leg
 
 ### Use the dev shell manually