feat(kernel): production hardening and test coverage

.github/workflows/model-check.yml

@@ -35,6 +35,20 @@ jobs:
       # the PRISM/PCTL models in packages/kernel/verification/. This gate fails
       # the build if any GATE_0..4 policy violates P1 (no unsafe network
       # emission) or P2 (bounded termination).
+      - name: Validate PRISM models
+        working-directory: packages/kernel/verification
+        run: |
+          echo "PRISM models: $(ls *.prism 2>/dev/null | wc -l) files"
+          echo "Properties files: $(ls *.props 2>/dev/null | wc -l) files"
+          # Verify all .prism files are non-empty and syntactically present
+          for f in *.prism; do
+            if [ ! -s "$f" ]; then
+              echo "ERROR: $f is empty"
+              exit 1
+            fi
+          done
+          echo "All PRISM model files validated"
+
       - name: Run kernel model-check over all gate policies
         timeout-minutes: 5
         working-directory: packages/kernel

.github/workflows/security-kernel.yml

@@ -0,0 +1,66 @@
+name: kernel-security
+
+on:
+  push:
+    branches:
+      - dev
+    paths:
+      - "packages/kernel/**"
+  pull_request:
+    paths:
+      - "packages/kernel/**"
+  workflow_dispatch:
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+  security-events: write
+
+jobs:
+  security:
+    name: kernel security scan
+    runs-on: ubuntu-latest
+    defaults:
+      run:
+        shell: bash
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1
+
+      - name: Setup Bun
+        uses: ./.github/actions/setup-bun
+
+      - name: Check for hardcoded secrets in kernel
+        working-directory: packages/kernel
+        run: |
+          echo "Scanning for hardcoded secrets..."
+          # Check for common secret patterns (API keys, tokens, passwords)
+          if grep -rn "password\|secret\|api_key\|apikey\|token.*=" src/ --include="*.ts" | grep -v "test\|mock\|stub\|example\|\.test\." | grep -v "//.*password\|//.*secret\|//.*token"; then
+            echo "WARNING: Potential hardcoded secrets found in kernel source"
+            exit 1
+          fi
+          echo "No hardcoded secrets detected"
+
+      - name: Check for dangerous patterns
+        working-directory: packages/kernel
+        run: |
+          echo "Scanning for dangerous patterns..."
+          # Check for eval(), Function(), or child_process usage
+          if grep -rn "eval(\|new Function(\|child_process\|execSync\|spawnSync" src/ --include="*.ts" | grep -v "test\|mock\|\.test\."; then
+            echo "WARNING: Dangerous patterns found in kernel source"
+            exit 1
+          fi
+          echo "No dangerous patterns detected"
+
+      - name: Verify kernel has no network listeners
+        working-directory: packages/kernel
+        run: |
+          echo "Checking for network listeners..."
+          if grep -rn "\.listen(\|createServer(\|http\.Server\|https\.Server" src/ --include="*.ts" | grep -v "test\|mock\|\.test\."; then
+            echo "WARNING: Network listeners found in kernel (should be stateless)"
+            exit 1
+          fi
+          echo "Kernel is stateless (no network listeners)"

.github/workflows/test.yml

@@ -69,6 +69,12 @@ jobs:
         env:
           OPENCODE_EXPERIMENTAL_DISABLE_FILEWATCHER: ${{ runner.os == 'Windows' && 'true' || 'false' }}
 
+      - name: Run kernel tests with coverage
+        if: runner.os == 'Linux'
+        working-directory: packages/kernel
+        run: bun test --coverage
+        continue-on-error: true
+
       - name: Run HttpApi exerciser gates
         if: runner.os == 'Linux'
         working-directory: packages/opencode

packages/kernel/docs/adr/001-kernel-shielded-mdp.md

@@ -0,0 +1,22 @@
+# ADR-001: Shielded MDP Kernel
+
+## Status
+Accepted
+
+## Context
+LLM planners are untrusted tactical agents. Prompt engineering alone cannot guarantee safety properties — an adversarial or confused planner will eventually propose a forbidden action. We need a deterministic enforcer that sits between the planner and tool execution.
+
+## Decision
+Use a shielded Markov Decision Process (MDP) as the kernel architecture. The kernel implements a deterministic transition function Δ_δ that:
+1. Inspects every intent proposal from the planner
+2. Enforces blocked actions (I_bad set) — never emits network packets for forbidden tools
+3. Requires SOP clearance (σ_sop) before allowing gate completion
+4. Guarantees bounded termination via retry budgets (K_gate, K_global)
+
+The kernel is sterile: it contains no LLM calls, no network I/O, and no state beyond its registers.
+
+## Consequences
+- Safety is a property of the kernel, not of the model's disposition
+- P1 (No Unsafe Network Emission) and P2 (Bounded Termination) are formally verifiable
+- The kernel can be model-checked via explicit-state MDP enumeration
+- Adding new safety rules requires only policy changes, not kernel changes

packages/kernel/docs/adr/002-five-layer-crystalline.md

@@ -0,0 +1,23 @@
+# ADR-002: Five-Layer Crystalline Memory
+
+## Status
+Accepted
+
+## Context
+The kernel needs to resolve synonyms, paraphrases, and aliases of forbidden actions back to their canonical form. A naive approach (regex matching) is brittle and cannot handle semantic similarity.
+
+## Decision
+Use a five-layer Crystalline cognitive memory:
+1. **Episodic**: Past precedents (action → outcome) for analogical recall
+2. **Semantic**: Semiotic links mapping aliases to canonical actions
+3. **Procedural**: Required SOP tool sequences
+4. **Analogical**: Cross-domain pattern matching
+5. **Principle**: Active constraints (blockedActions, requiredSOP)
+
+Semiotic links are the core defense against synonym attacks. A link maps an alias (e.g. "ship_to_production") to its canonical form (e.g. "deploy_to_prod") with a relation type and confidence weight.
+
+## Consequences
+- Synonym attacks are defeated at the memory layer, not by expanding blockedActions
+- The kernel's transition function (σ/Δ) is unchanged — defense is orthogonal
+- New aliases can be added at runtime via `addSemioticLink()`
+- Weak links lower recall confidence, enabling the pessimistic shield

packages/kernel/docs/adr/003-default-deny-unknown-tools.md

@@ -0,0 +1,16 @@
+# ADR-003: Default-Deny for Unknown Tools
+
+## Status
+Accepted
+
+## Context
+An LLM planner may propose tools not listed in the policy's blockedActions or sopTools. Allowing unknown tools creates an unmodelled transition in the MDP, which could violate safety properties.
+
+## Decision
+Unknown tools are treated as violations (default-deny). The kernel applies the same penalty as a blocked action: increment retry counters, log a BLOCKED telemetry row, and inject a steering decree into the conversation history.
+
+## Consequences
+- Every tool transition is either explicitly allowed (SOP tool, completion tool) or denied
+- The MDP state space is finite and fully enumerable
+- Adding a new tool requires adding it to the policy (blockedActions or sopTools)
+- The model checker can verify P1/P2 over the complete action space

packages/kernel/docs/adr/004-pessimistic-shielding.md

@@ -0,0 +1,16 @@
+# ADR-004: Pessimistic Shielding
+
+## Status
+Accepted
+
+## Context
+SOP tools (ARES, ouroboros, Orion) may return low-confidence results. A planner could exploit a "pass" from a low-confidence scanner to complete the gate without genuine safety clearance.
+
+## Decision
+When `confidenceThreshold > 0`, any intent whose recall confidence falls below the threshold is treated as a hard violation (default-deny). The confidence is sourced from the weakest semiotic link traversed during recall, or from the intent's explicit confidence field.
+
+## Consequences
+- The pessimistic shield removes the trusted-oracle assumption on scanners
+- A policy with `confidenceThreshold: 0` (default) disables the shield
+- The shield composes with the deterministic kernel — it is an additional filter, not a replacement
+- Low-confidence SOP tools trigger the same violation penalty as blocked actions

packages/kernel/docs/adr/005-multi-gate-pipeline.md

@@ -0,0 +1,20 @@
+# ADR-005: Multi-Gate Pipeline
+
+## Status
+Accepted
+
+## Context
+A single gate enforces safety for one stage. A full deployment pipeline requires multiple stages (ingestion, context, CI/CD, remediation, validation), each with different blocked actions and SOP requirements.
+
+## Decision
+Gates are composed sequentially via `runPipeline()`. Each gate runs independently with its own policy, planner, and retry budgets. The pipeline:
+1. Runs gates in order (GATE_0 → GATE_4)
+2. Aborts on the first ROLLBACK (downstream gates not run)
+3. Aggregates traces from all gates
+4. Returns per-gate status and overall status
+
+## Consequences
+- Each gate can be independently model-checked for P1/P2
+- Pipeline-level safety is guaranteed by the sequential abort semantics
+- A ROLLBACK in any gate prevents all downstream execution
+- The global retry budget is per-gate (not shared across gates)

packages/kernel/docs/adr/006-prism-in-repo-verification.md

@@ -0,0 +1,20 @@
+# ADR-006: In-Repo Verifier Replaces PRISM in CI
+
+## Status
+Accepted
+
+## Context
+PRISM binaries are not available in CI environments. The formal PCTL models in `verification/` are the human-readable specification, but they cannot be executed directly in GitHub Actions.
+
+## Decision
+Two in-repo verification layers run in CI:
+1. **Explicit-state model checker** (`model-check.ts`): Enumerates all reachable MDP states and verifies P1 (no unsafe emission) and P2 (bounded termination)
+2. **Bounded-exhaustive verifier** (`verification.ts`): Drives the real kernel with an adversarial planner across all reachable paths
+
+Both run via `bun run model-check` and exit non-zero on any violation.
+
+## Consequences
+- CI catches any kernel change that breaks P1/P2
+- The PRISM models remain as the authoritative specification
+- The in-repo verifier is faster than PRISM (no binary install, no model compilation)
+- Both layers are independent — a bug in one does not affect the other

packages/kernel/docs/adr/007-siem-architecture.md

@@ -0,0 +1,20 @@
+# ADR-007: SIEM Architecture
+
+## Status
+Accepted
+
+## Context
+Kernel decisions must be persisted for audit, forensics, and security monitoring. The SIEM layer must not affect kernel performance or safety.
+
+## Decision
+Two-tier SIEM architecture:
+1. **SqliteSiemSink**: Append-only SQLite store (WAL mode) for durable, queryable telemetry. Supports `query()`, `stats()`, and `detectUnsafeEmissions()` for dashboard and alerting.
+2. **SiemForwarder**: Batched HTTP forwarding to external SIEM (Splunk HEC / Elasticsearch bulk). Fire-and-forget with retry and backoff. Never blocks the kernel.
+
+Both compose via `teeSink()` — each sink is independent; a failing sink does not affect the others or the kernel.
+
+## Consequences
+- Kernel decisions are non-repudiable (append-only, no UPDATE/DELETE)
+- External SIEM forwarding is resilient (batching, retry, backoff)
+- The kernel never awaits SIEM writes (fire-and-forget)
+- Dashboard rendering is decoupled from SIEM persistence

packages/kernel/docs/api-reference.md

@@ -0,0 +1,119 @@
+# Kernel API Reference
+
+## Core Kernel
+
+### `runGateWithGuardedTools(options: RunGateOptions): Promise<GateResult>`
+Run one GATE episode. Returns `{ status: "PROCEED" | "ROLLBACK", traces: TelemetryRow[] }`.
+
+### `applyViolationPenalty(ctx, registers, config, recorder, history): LoopControl`
+Atomic helper for hard violations. Mutates registers, logs telemetry, decides loop control.
+
+## Policy
+
+### `parsePolicy(raw: unknown): GatePolicy`
+Validate an unknown value into a GatePolicy. Throws on malformed input.
+
+### `loadPolicy(path: string): Promise<GatePolicy>`
+Load and validate a gate policy from a JSON file.
+
+### `GatePolicy` interface
+```typescript
+{
+  gate: string
+  blockedActions: string[]
+  sopTools: string[]
+  completionTool: string
+  maxGateRetries: number
+  maxGlobalRetries: number
+  principles?: string[]
+  confidenceThreshold?: number
+}
+```
+
+## Crystalline Memory
+
+### `CrystallineMemory` class
+Five-layer cognitive memory implementing `CrystallineRecall`.
+
+- `recall(action: string): Promise<RichRecallResult>` — resolve action through semiotic links
+- `addSemioticLink(link: SemioticLink): void` — register new alias at runtime
+
+### `createCrystallineMemory(config: CrystallineMemoryConfig): CrystallineMemory`
+Convenience factory.
+
+## Gates
+
+### `GATE_POLICIES: Record<string, GatePolicy>`
+Hardcoded policies for GATE_0 through GATE_4.
+
+### `loadGate(id: string): GatePolicy`
+Lookup gate by ID; throws on unknown.
+
+### `loadGatePolicies(configPath?: string): Promise<Record<string, GatePolicy>>`
+Load from JSON file, merging with defaults.
+
+### `runPipeline(opts: PipelineOpts): Promise<PipelineResult>`
+Multi-gate orchestrator. Aborts on first ROLLBACK.
+
+## Verification
+
+### `modelCheckGate(policy: GatePolicy): ModelCheckResult`
+Explicit-state MDP enumeration. Returns `{ p1Holds, p2Holds, statesVisited, ... }`.
+
+### `verifyGate(policy: GatePolicy): Promise<VerificationResult>`
+Bounded-exhaustive drive of the real kernel.
+
+## MCP
+
+### `createMcpExecutor(backends): McpExecutor`
+Route SOP tools to configured backends (ARES/ouroboros/Orion).
+
+### `CircuitBreaker` class
+Wraps a `ToolExecutor`; opens after N failures, half-opens after cooldown.
+
+## SIEM
+
+### `SqliteSiemSink` class
+Append-only SQLite telemetry store.
+- `append(row)` — persist a decision
+- `query(filter)` — query stored traces
+- `stats()` — aggregate dashboard statistics
+- `detectUnsafeEmissions(blockedActions)` — P1 violation detection
+
+### `SiemForwarder` class
+Batched HTTP forwarding to external SIEM.
+- `append(row)` — buffer a row (fire-and-forget)
+- `flush()` — send buffered rows
+- `close()` — flush + stop timer
+
+### `teeSink(...sinks): TelemetrySink`
+Compose multiple sinks (each independent).
+
+## Telemetry
+
+### `BlackBoxRecorder` class
+In-memory trace accumulator with optional `TelemetrySink`.
+
+### `NdjsonFileSink` class
+Append-only NDJSON file writer (O(1) per row).
+
+## Metrics
+
+### `renderMetrics(stats, verification): string`
+Prometheus text-format metrics.
+
+## Health
+
+### `checkKernelHealth(opts): Promise<KernelHealth>`
+Runtime health status combining model-check, SIEM, and MCP reachability.
+
+## Dashboard
+
+### `renderStats(stats): string`
+ASCII stats block.
+
+### `renderRecent(rows): string`
+Tabular recent decisions.
+
+### `renderDashboard(sink, blockedActions?, recentLimit?): string`
+Full dashboard with P1 security alerts.