authgate-kernel

The authorization layer between any decision and any IO. An actor presents a signed capability chain; the kernel verifies it's valid, non-expired, and traceable to a trust root — deterministically, structurally, with no LLM call inside the gate.

Rust TCB #![forbid(unsafe_code)] PolyForm Noncommercial 1.0.0 github.com/Aliipou/authgate-kernel

This isn't a mockup. The panel below runs authgate_kernel.wasm — the actual Rust TCB (engine.rs, dag.rs, wire.rs), compiled with wasm-pack, running client-side in your browser right now. Every Permit/Deny below is the real kernel's output, not a scripted response.

Live: verify a capability

Loading the compiled kernel…

Registry (claims)

Action

Architecture

flowchart TB
  REQ[Agent / planner request]
  CA[CanonicalAction
actor, resource, rights, capability_proofs, binding_hash]
  CG["CallGate.execute()"]
  L1[L1: verify binding_hash]
  L2["L2: for each capability — resource match, expiry, epoch, chain validation"]
  L3[L3: root-signed revocations]
  PERMIT[Decision::Permit]
  DENY["Decision::Deny reason"]
  AUDIT[AuditLog — SHA-256 hash-chained]

  REQ --> CA --> CG --> L1 --> L2 --> L3
  L3 -->|all invariants hold| PERMIT
  L3 -->|any invariant fails| DENY
  PERMIT --> AUDIT
  DENY --> AUDIT

Numbers that matter

This project's own README refuses to round up. Same numbers here.

Security-enforcing Rust LOC	`engine.rs` 250 LOC; full path (`engine.rs`+`dag.rs`+`call_gate.rs`) ~934 LOC
TCB Rust tests	141 passing
Python integration tests	905 passing
Kani harnesses (bounded model checking)	19 proved (bounded), CI-verified via `formal.yml`
Lean 4 theorems	Being fixed live — the CI job had no `@[default_target]` set, so it built nothing and reported green for months without checking a single file; now fixed, which surfaced real compile errors in `Scope`/`TCB`/`Temporal`/`MultiAgent` that were never actually caught. `OntologicalRoot.lean` (new) builds and proves clean.
Wire boundary attack classes	18 (WA-1…WA-18), 37 pytest assertions
Concurrent verify() stress test	1,000 calls via ThreadPoolExecutor, 200 concurrent audit appends
Python verify() latency	p50 ≈ 9.7µs (10-claim registry), 17.4µs (1,000-claim)
TLA+ / TLC	Safety model checked, CI-verified via `formal.yml` (`formal/tlc_run.log`)

What it does not do

Not this	Why
Alignment	Alignment is about values. This kernel is about typed authority.
Intent verification	The kernel does not parse or interpret natural language.
Ethics enforcement	Ethical reasoning requires semantic content — this is structural.
Side-channel defense	Timing attacks, covert channels — out of scope by design.