MVP alpha.11: Performance baselines and verification gates v0

.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

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
 

README.md

@@ -1,15 +1,15 @@
 # RuneCode — Security-first AI coding: isolated execution, signed, auditable
 
 [![CI](https://github.com/runecode-ai/runecode/actions/workflows/ci.yml/badge.svg)](https://github.com/runecode-ai/runecode/actions/workflows/ci.yml)
-[![Status: alpha.9 in progress](https://img.shields.io/badge/status-alpha.9%20in%20progress-orange)](runecontext/project/roadmap.md)
+[![Status: alpha.11 in progress](https://img.shields.io/badge/status-alpha.11%20in%20progress-orange)](runecontext/project/roadmap.md)
 [![License: Apache-2.0](https://img.shields.io/badge/License-Apache%202.0-blue.svg)](LICENSE)
 
 RuneCode is a security-first agentic automation platform for software engineering.
 It treats isolation and cryptographic provenance as co-equal pillars: work runs in tightly scoped isolates with deny-by-default capabilities, explicit artifact-based data movement, and a tamper-evident audit trail.
 
 ## Status
 
-The latest published release is `v0.1.0-alpha.7`, and the repository mainline already includes `v0.1.0-alpha.9` work in progress.
+The latest published release is `v0.1.0-alpha.7`, and the repository mainline already includes `v0.1.0-alpha.11` work in progress.
 RuneCode remains pre-production: the signed, tag-driven release pipeline exists, but the shipped Go binaries are still scaffold-heavy and not feature-complete.
 
 ## Why RuneCode
@@ -173,7 +173,8 @@ This quick path verifies signed checksums and the signed archive before install.
 - Signed runtime-image and runtime-toolchain identity contracts, typed verifier-authority state, trusted admission into a launcher-private verified runtime cache, and fail-closed launch from verified local assets rather than mutable host paths or ad hoc launch-time synthesis
 - Durable launcher runtime evidence persistence and broker-derived authoritative runtime projection for `backend_kind`, `isolation_assurance_level`, `provisioning_posture`, lifecycle, terminal state, and runtime attestation support or verification posture from persisted evidence rather than transient launcher state, with supported `attested` posture only earned after secure-session validation, post-handshake runtime evidence collection, and trusted verification
 - Broker-owned runtime audit emission for `runtime_launch_admission`, `runtime_launch_denied`, `isolate_session_started`, and `isolate_session_bound`, with reference-heavy payloads bound to persisted launcher evidence digests and later attestation linkage added from persisted post-handshake evidence rather than optimistic launch-time fields
-- Checked-in bounded TLA+ security-kernel artifacts plus deterministic TLC model-checking wired into `just model-check` and `just ci`
+- Checked-in bounded TLA+ security-kernel artifacts plus deterministic TLC model-checking wired into `just model-check`, `just model-check-core`, and `just ci`
+- Reviewed machine-consumed performance contracts under `tools/perfcontracts/`, deterministic performance fixtures and harnesses for TUI, broker, runner or workflow, gateway or dependency or audit or protocol surfaces, and a required shared-Linux CI gate that currently enforces only the checked-in `required_shared_linux` subset while launcher, attestation, and external-anchor surfaces remain informational or `contract_pending_dependency`
 
 Still incremental / not implemented end-to-end yet:
 - Secure-storage posture projection and broader provider auth modes remain incremental, but direct-credential provider setup and execution now exist for OpenAI-compatible and Anthropic-compatible endpoints on the shared provider substrate
@@ -240,8 +241,12 @@ Common commands:
 just fmt
 just lint
 just model-check
+just model-check-core
+just model-check-replay
 just test
+just ci-fast
 just ci
+just ci-required-shared-linux
 ```
 
 Useful protocol-specific checks:
@@ -254,12 +259,14 @@ cd runner && npm test
 cd runner && npm run boundary-check
 ```
 
-These checks are also covered by `just ci`.
+These checks are covered by `just ci`, while the required shared-Linux performance-contract subset runs in the dedicated `just ci-required-shared-linux` lane rather than every local `just ci` run.
 
 Formal model checking entrypoint:
 
 ```sh
 just model-check
+just model-check-core
+just model-check-replay
 ```
 
 Optional: enable automatic dev-shell entry with `direnv` + `nix-direnv`:

cmd/runecode-tui/local_rpc_integration_linux_test.go

@@ -37,10 +37,7 @@ func TestTUIRoutesUseRealLocalRPCBrokerContracts(t *testing.T) {
 
 func startTUILocalRPCServer(t *testing.T) (*brokerapi.LocalIPCListener, *brokerapi.Service, string, <-chan error) {
 	t.Helper()
-	runtimeDir := filepath.Join(t.TempDir(), "runtime")
-	if err := os.MkdirAll(runtimeDir, 0o700); err != nil {
-		t.Fatalf("MkdirAll returned error: %v", err)
-	}
+	runtimeDir := shortTUILocalRPCRuntimeDir(t)
 	service, ledgerRoot := newTUILocalRPCService(t)
 	listener, err := brokerapi.ListenLocalIPC(brokerapi.LocalIPCConfig{RuntimeDir: runtimeDir, SocketName: "broker.sock"})
 	if err != nil {
@@ -54,6 +51,16 @@ func startTUILocalRPCServer(t *testing.T) (*brokerapi.LocalIPCListener, *brokera
 	return listener, service, ledgerRoot, errCh
 }
 
+func shortTUILocalRPCRuntimeDir(t *testing.T) string {
+	t.Helper()
+	runtimeDir, err := os.MkdirTemp("", "rc-tui-rpc-")
+	if err != nil {
+		t.Fatalf("MkdirTemp returned error: %v", err)
+	}
+	t.Cleanup(func() { _ = os.RemoveAll(runtimeDir) })
+	return runtimeDir
+}
+
 func configureTUILocalRPCClient(t *testing.T, runtimeDir string) {
 	t.Helper()
 	origConfigProvider := localIPCConfigProvider

cmd/runecode-tui/shell_watch_test.go

@@ -1,13 +1,60 @@
 package main
 
 import (
+	"context"
 	"errors"
 	"testing"
 	"time"
 
 	"github.com/runecode-ai/runecode/internal/brokerapi"
 )
 
+type watchPollRequestRecorder struct {
+	*fakeBrokerClient
+	run      brokerapi.RunWatchRequest
+	approval brokerapi.ApprovalWatchRequest
+	session  brokerapi.SessionWatchRequest
+}
+
+func (r *watchPollRequestRecorder) RunWatch(ctx context.Context, req brokerapi.RunWatchRequest) ([]brokerapi.RunWatchEvent, error) {
+	r.run = req
+	return r.fakeBrokerClient.RunWatch(ctx, req)
+}
+
+func (r *watchPollRequestRecorder) ApprovalWatch(ctx context.Context, req brokerapi.ApprovalWatchRequest) ([]brokerapi.ApprovalWatchEvent, error) {
+	r.approval = req
+	return r.fakeBrokerClient.ApprovalWatch(ctx, req)
+}
+
+func (r *watchPollRequestRecorder) SessionWatch(ctx context.Context, req brokerapi.SessionWatchRequest) ([]brokerapi.SessionWatchEvent, error) {
+	r.session = req
+	return r.fakeBrokerClient.SessionWatch(ctx, req)
+}
+
+func TestShellWatchPollRequestsSnapshotOnlyStreams(t *testing.T) {
+	m := newShellModel()
+	recorder := &watchPollRequestRecorder{fakeBrokerClient: &fakeBrokerClient{}}
+	m.client = recorder
+
+	msg, ok := m.loadWatchPollCmd()().(shellWatchTransportLoadedMsg)
+	if !ok {
+		t.Fatalf("loadWatchPollCmd message = %T, want shellWatchTransportLoadedMsg", msg)
+	}
+	assertWatchPollSnapshotOnly(t, recorder.run.IncludeSnapshot, recorder.run.Follow, "run")
+	assertWatchPollSnapshotOnly(t, recorder.approval.IncludeSnapshot, recorder.approval.Follow, "approval")
+	assertWatchPollSnapshotOnly(t, recorder.session.IncludeSnapshot, recorder.session.Follow, "session")
+}
+
+func assertWatchPollSnapshotOnly(t *testing.T, includeSnapshot, follow bool, family string) {
+	t.Helper()
+	if !includeSnapshot {
+		t.Fatalf("%s watch poll IncludeSnapshot = false, want true", family)
+	}
+	if follow {
+		t.Fatalf("%s watch poll Follow = true, want false", family)
+	}
+}
+
 func TestShellWatchManagerFamilySpecificFailureProjectsDegradedHealth(t *testing.T) {
 	manager := newShellWatchManager()
 	now := time.Date(2026, 4, 16, 12, 0, 0, 0, time.UTC)

cmd/runecode-tui/shell_watch_transport.go

@@ -67,9 +67,9 @@ func (m shellModel) loadWatchPollCmd() tea.Cmd {
 		ctx, cancel := withLoadTimeout()
 		defer cancel()
 
-		runEvents, runErr := m.client.RunWatch(ctx, brokerapi.RunWatchRequest{StreamID: newRequestID("shell-run-watch-stream"), IncludeSnapshot: true, Follow: true})
-		approvalEvents, approvalErr := m.client.ApprovalWatch(ctx, brokerapi.ApprovalWatchRequest{StreamID: newRequestID("shell-approval-watch-stream"), IncludeSnapshot: true, Follow: true})
-		sessionEvents, sessionErr := m.client.SessionWatch(ctx, brokerapi.SessionWatchRequest{StreamID: newRequestID("shell-session-watch-stream"), IncludeSnapshot: true, Follow: true})
+		runEvents, runErr := m.client.RunWatch(ctx, brokerapi.RunWatchRequest{StreamID: newRequestID("shell-run-watch-stream"), IncludeSnapshot: true})
+		approvalEvents, approvalErr := m.client.ApprovalWatch(ctx, brokerapi.ApprovalWatchRequest{StreamID: newRequestID("shell-approval-watch-stream"), IncludeSnapshot: true})
+		sessionEvents, sessionErr := m.client.SessionWatch(ctx, brokerapi.SessionWatchRequest{StreamID: newRequestID("shell-session-watch-stream"), IncludeSnapshot: true})
 
 		return shellWatchTransportLoadedMsg{
 			Run:        shellWatchRunTransportResult{Events: runEvents, Err: runErr},

formal/tla/security-kernel/README.md

@@ -51,3 +51,9 @@ TLC wiring is owned by the CI/tooling lane. When TLC tooling is available, run w
 - configs:
   - `formal/tla/security-kernel/SecurityKernelV0.core.cfg`
   - `formal/tla/security-kernel/SecurityKernelV0.replay.cfg`
+
+Convenience recipes:
+
+- `just model-check-core` runs the faster core PR gate.
+- `just model-check-replay` runs the broader replay model.
+- `just model-check` runs both and is included in full local `just ci` parity.

go.mod

@@ -20,6 +20,7 @@ require (
 	github.com/charmbracelet/x/ansi v0.10.1 // indirect
 	github.com/charmbracelet/x/cellbuf v0.0.13-0.20250311204145-2c3ea96c31dd // indirect
 	github.com/charmbracelet/x/term v0.2.1 // indirect
+	github.com/creack/pty v1.1.24 // indirect
 	github.com/erikgeiser/coninput v0.0.0-20211004153227-1c3628e74d0f // indirect
 	github.com/lucasb-eyer/go-colorful v1.2.0 // indirect
 	github.com/mattn/go-isatty v0.0.20 // indirect

go.sum

@@ -22,6 +22,8 @@ github.com/charmbracelet/x/exp/golden v0.0.0-20241011142426-46044092ad91 h1:payR
 github.com/charmbracelet/x/exp/golden v0.0.0-20241011142426-46044092ad91/go.mod h1:wDlXFlCrmJ8J+swcL/MnGUuYnqgQdW9rhSD61oNMb6U=
 github.com/charmbracelet/x/term v0.2.1 h1:AQeHeLZ1OqSXhrAWpYUtZyX1T3zVxfpZuEQMIQaGIAQ=
 github.com/charmbracelet/x/term v0.2.1/go.mod h1:oQ4enTYFV7QN4m0i9mzHrViD7TQKvNEEkHUMCmsxdUg=
+github.com/creack/pty v1.1.24 h1:bJrF4RRfyJnbTJqzRLHzcGaZK1NeM5kTC9jGgovnR1s=
+github.com/creack/pty v1.1.24/go.mod h1:08sCNb52WyoAwi2QDyzUCTgcvVFhUzewun7wtTfvcwE=
 github.com/dlclark/regexp2 v1.11.0 h1:G/nrcoOa7ZXlpoa/91N3X7mM3r8eIlMBBJZvsz/mxKI=
 github.com/dlclark/regexp2 v1.11.0/go.mod h1:DHkYz0B9wPfa6wondMfaivmHpzrQ3v9q8cnmRbL6yW8=
 github.com/erikgeiser/coninput v0.0.0-20211004153227-1c3628e74d0f h1:Y/CXytFA4m6baUTXGLOoWe4PQhGxaX0KpnayAqC48p4=

internal/brokerapi/local_api_llm_execution.go

@@ -139,9 +139,10 @@ func (s *Service) executeProviderRequest(ctx context.Context, execCtx llmExecuti
 	}
 	req, errResp := s.buildProviderHTTPRequest(ctx, execCtx, body, started)
 	if errResp != nil {
-		return "", int64(len(body)), started, time.Now().UTC(), errResp
+		return "", int64(len(body)), started, normalizeExecutionCompletedAt(started, time.Now().UTC()), errResp
 	}
 	respBody, completed, errResp := s.doProviderHTTPRequest(execCtx, req)
+	completed = normalizeExecutionCompletedAt(started, completed)
 	if errResp != nil {
 		return "", int64(len(body)), started, completed, errResp
 	}
@@ -152,6 +153,13 @@ func (s *Service) executeProviderRequest(ctx context.Context, execCtx llmExecuti
 	return text, int64(len(body)), started, completed, nil
 }
 
+func normalizeExecutionCompletedAt(started, completed time.Time) time.Time {
+	if completed.After(started) {
+		return completed
+	}
+	return started.Add(time.Millisecond)
+}
+
 func (s *Service) prepareProviderRequestBody(requestID string, translated map[string]any) ([]byte, time.Time, *ErrorResponse) {
 	body, err := json.Marshal(translated)
 	if err != nil {

internal/brokerapi/local_rpc_client_linux_test.go

@@ -148,7 +148,7 @@ func assertLocalRPCSocketPath(t *testing.T, runtimeDir string) {
 
 func setupLocalRPCRunListRoundTrip(t *testing.T, service *Service) (string, *LocalRPCClient, chan error) {
 	t.Helper()
-	runtimeDir := filepath.Join(t.TempDir(), "runtime")
+	runtimeDir := shortLocalRPCRuntimeDir(t)
 	listener, err := ListenLocalIPC(LocalIPCConfig{RuntimeDir: runtimeDir, SocketName: "broker.sock"})
 	if err != nil {
 		t.Fatalf("ListenLocalIPC returned error: %v", err)
@@ -172,7 +172,7 @@ func setupLocalRPCRunListRoundTrip(t *testing.T, service *Service) (string, *Loc
 
 func setupLocalRPCSessionListRoundTrip(t *testing.T, service *Service) (string, *LocalRPCClient, chan error) {
 	t.Helper()
-	runtimeDir := filepath.Join(t.TempDir(), "runtime")
+	runtimeDir := shortLocalRPCRuntimeDir(t)
 	listener, err := ListenLocalIPC(LocalIPCConfig{RuntimeDir: runtimeDir, SocketName: "broker.sock"})
 	if err != nil {
 		t.Fatalf("ListenLocalIPC returned error: %v", err)
@@ -196,7 +196,7 @@ func setupLocalRPCSessionListRoundTrip(t *testing.T, service *Service) (string,
 
 func setupLocalRPCSessionSendMessageRoundTrip(t *testing.T, service *Service) (string, *LocalRPCClient, chan error) {
 	t.Helper()
-	runtimeDir := filepath.Join(t.TempDir(), "runtime")
+	runtimeDir := shortLocalRPCRuntimeDir(t)
 	listener, err := ListenLocalIPC(LocalIPCConfig{RuntimeDir: runtimeDir, SocketName: "broker.sock"})
 	if err != nil {
 		t.Fatalf("ListenLocalIPC returned error: %v", err)
@@ -220,7 +220,7 @@ func setupLocalRPCSessionSendMessageRoundTrip(t *testing.T, service *Service) (s
 
 func setupLocalRPCSessionExecutionTriggerRoundTrip(t *testing.T, service *Service) (string, *LocalRPCClient, chan error) {
 	t.Helper()
-	runtimeDir := filepath.Join(t.TempDir(), "runtime")
+	runtimeDir := shortLocalRPCRuntimeDir(t)
 	listener, err := ListenLocalIPC(LocalIPCConfig{RuntimeDir: runtimeDir, SocketName: "broker.sock"})
 	if err != nil {
 		t.Fatalf("ListenLocalIPC returned error: %v", err)
@@ -427,7 +427,7 @@ func TestValidateRawMessageLimitsRejectsLargePayload(t *testing.T) {
 }
 
 func TestLocalRPCClientInvokeRespectsContextDeadline(t *testing.T) {
-	runtimeDir := filepath.Join(t.TempDir(), "runtime")
+	runtimeDir := shortLocalRPCRuntimeDir(t)
 	listener, err := ListenLocalIPC(LocalIPCConfig{RuntimeDir: runtimeDir, SocketName: "broker.sock"})
 	if err != nil {
 		t.Fatalf("ListenLocalIPC returned error: %v", err)
@@ -457,3 +457,13 @@ func TestLocalRPCClientInvokeRespectsContextDeadline(t *testing.T) {
 		t.Fatalf("error code = %q, want request_cancelled", errResp.Error.Code)
 	}
 }
+
+func shortLocalRPCRuntimeDir(t *testing.T) string {
+	t.Helper()
+	runtimeDir, err := os.MkdirTemp("", "rc-rpc-")
+	if err != nil {
+		t.Fatalf("MkdirTemp returned error: %v", err)
+	}
+	t.Cleanup(func() { _ = os.RemoveAll(runtimeDir) })
+	return runtimeDir
+}