SCC Kernel Fortress

A system that cannot prove the legality of its next step has no right to take it.

Stateful AI systems can erase execution lineage, mutate protected memory, bypass halt conditions, and accept states without machine-checkable justification — and still produce output that passes every output-layer evaluation. These are transition-validity failures. They are invisible to logs, prompts, and post-hoc audits.

SCC Kernel Fortress makes transition legality a pre-acceptance predicate. Before a candidate next state enters the accepted trajectory, it must pass a deterministic checker. If the proof-obligation bundle is absent, malformed, or fails any of the implemented constitutional obligations, the transition is rejected — not logged, not warned about, rejected.

Formal Verification AI Safety Lean 4 Rust Agentic Systems EU AI Act Runtime Compliance

How it works

The checker is a pure Rust function — no wall-clock time, no randomness, no network calls, no mutable globals:

pub fn accepts(
    po: &POBundle, prev: &SCCState, next: &SCCState,
    event: &CanonicalEvent, audit_event: &AuditEvent,
    env: &ExecutionEnv,
) -> Result<(), CheckerError>

Every legal transition must carry a proof-obligation bundle — eight Boolean fields attesting to domain validity, invariant satisfaction, governance bounds, risk law, audit chain continuity, protected-coordinate isolation, and refinement classification. A transition with any false field, or no bundle at all, is rejected before state acceptance.

Constitutional obligation	What it enforces	Lean 4 theorem
ProtectedIsolation	Safety-critical coordinates cannot change in ordinary execution	`accepted_preserves_protected`
HaltAbsorbing	Halt is an absorbing state — cannot exit without authorized recovery	`check_accept_sound` ∘ `HaltAbsorbing`
RiskToHalt	Risk ≥ threshold forces failure mode 3	`RiskToHalt` conjunct of `GateProp`
LineageContinues	Execution history must extend — no erasure, no gaps	`LineageContinues` conjunct of `GateProp`
Required(b)	All eight proof-obligation fields must be true	`Required` conjunct of `GateProp`

14 named rejection gates

Each failure class has a committed JSON fixture, an expected first-failure gate, and a canon article mapping. A checker that accepts a negative fixture, or rejects at the wrong gate, fails the release gate.

audit_event_hash_bad checker_version_mismatch descriptor_mismatch_audit event_hash_bad halt_absorption_violation invalid_simplex lineage_erasure missing_required_field next_hash_bad prev_hash_bad protected_mutation risk_threshold_without_halt schema_mismatch wrong_step_mode

Lean 4 formal bridge

formal/lean/SCC/KernelFortress/GateSoundness.lean proves Bool-to-Prop soundness for the implemented v1 subset: if GateBool env b prev next = true then GateProp env b prev next holds. The gate property is made decidable via instDecidableGateProp, derived automatically by infer_instance.

PipelineWitness.lean formalizes the seven-stage witness bridge. A Coq proof fragment covers required-bundle reflection and quorum-intersection arithmetic.

No sorry, no admit, no unledgered axioms. Enforced by tools/validate_formal_artifacts.py in CI.

Non-claim The formal bridge covers the implemented v1 subset. It does not prove compiler correctness, operating-system correctness, SHA-256 security, full SCC canon mechanization, or that the Rust implementation faithfully corresponds to the Lean model. These limits are in the published TCB ledger.

Verify in 5 minutes

Clone
```
git clone https://github.com/IceMasterT/SCC-Formal_Constitution.git
cd SCC-Formal_Constitution
bash scripts/verify_in_5_minutes.sh
```
Runs vector validation (17 fixtures), forbidden-import scan, and the TypeScript reference suite (22 tests) without Rust or Lean.
Docker
```
docker build -t scc-kernel-fortress .
docker run --rm scc-kernel-fortress
```
Full release gate — Rust tests, TypeScript tests, formal static scan, vector validation — in a reproducible container.
Full
```
make test
```
Requires Rust 1.78+, Node 22+. Runs all suites including proptest invariants, memory-lineage compression, numerical stability, and federation quorum tests.

Paper

SCC Kernel Fortress: Executable Evaluation Gates for Runtime Compliance in Agentic Systems
Ian Farquharson — NeurIPS 2026 Datasets & Benchmarks track

The paper presents the evaluation protocol, canon-to-executable mapping, case study of representative agent-loop failures, baseline comparison against monitoring mechanisms that do not enforce pre-acceptance rejection, evidence tiers for reproducing the artifact claim, and the full threat-model and non-claim boundaries.

arxiv preprint PDF (GitHub)

Contact & collaboration

I'm looking for: researchers who want to use the negative corpus as a benchmark or extend the Lean mechanization; engineers integrating compliance gates into agentic CI pipelines; AI safety organizations interested in the formal bridge as safety-case infrastructure; and independent checker implementations in any language.

Ian Farquharson
tech@mysms.promo · GitHub