Nucleus: Enforced permissions for AI agents – policy+enforcement in one stack
Nucleus prevents AI coding agents from combining untrusted input with privileged actions, and proves what was and wasn't allowed.
Two primitives — join and flows_to — enforce information flow control with four algebraic laws. Once web content enters a session, it cannot silently reach git push . That property is machine-checked , not hoped.
Every tool call flows through the permission kernel. nucleus run tracks data provenance and blocks dangerous combinations — like writing code derived from untrusted web content. The hook for AI coding assistants previously bundled here ( nucleus-claude-hook ) is now part of nucleus-code , the private orchestrator built on this runtime.
Full inventory: 165 Lean 4 theorems (zero sorry ), 112 Kani BMC proofs, 297 Verus VCs, ~2,850 tests. Verified Claims | Formal Methods | Production Delta
Status: alpha. The crate ships a per-call SPIFFE-ID derivation library, an in-process Ed25519 demo issuer, an append-mode JSONL log, and a nucleus lineage walker. The demo is not yet wired into the runtime, edges are not yet signed, and no SPIRE-backed IdentityFetcher impl exists in this repo. See crates/nucleus-lineage/README.md for the honest scope and the audit findings for what's still missing.
nucleus-lineage extends SPIFFE workload identity from the pod level down to the individual call level. Each tool invocation, LLM call, or derived artifact mints a child SPIFFE ID whose path encodes its lineage and whose suffix is a content hash: