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.

let mut state = FlowState::bottom();          // clean session
state.join_operation(Operation::WebFetch);     // tainted by web content
assert!(!state.flows_to(SinkClass::GitPush));  // can't push tainted data

cargo install --git https://github.com/coproduct-opensource/nucleus nucleus-claude-hook
nucleus-claude-hook --setup    # wires into your AI coding assistant
nucleus-claude-hook --smoke-test

Every tool call now flows through the permission kernel. The hook tracks data provenance and blocks dangerous combinations — like writing code derived from untrusted web content.

Full inventory: 165 Lean 4 theorems (zero sorry), 112 Kani BMC proofs, 297 Verus VCs, ~2,850 tests. Verified Claims | Formal Methods | Production Delta

Agent → MCP → tool-proxy (inside VM) → portcullis check → OS operation

┌──────────────────────────────────────────────┐
│  nucleus-cli / nucleus-audit scan            │
├──────────────────────────────────────────────┤
│  nucleus (Sandbox + Executor + AtomicBudget) │
├──────────────────────────────────────────────┤
│  portcullis (7 control planes)               │
│  Capabilities × Obligations × Paths ×        │
│  Commands × Budget × Time + DPI              │
├──────────────────────────────────────────────┤
│  nucleus-identity (SPIFFE + mTLS)            │
├──────────────────────────────────────────────┤
│  Firecracker microVM / seccomp / netns       │
└──────────────────────────────────────────────┘

Total: ~2,850 tests across the workspace (162K LOC Rust).

Documented in SECURITY_TODO.md and docs/production-delta.md. Key items:

• bash -c bypasses command-level checks. Firecracker network policy is the real defense.
• Path sandboxing is string-based. cap-std provides defense-in-depth.
• Budget enforcement is partial. Pre-execution reservation works; post-execution accounting is not.
• Formal verification covers the lattice, not the full runtime. See FORMAL_METHODS.md.
• Hook I/O boundary is unverified. JSON parsing is a trusted edge.

Protects against: prompt injection side effects, invisible Unicode injection, misconfigured permissions, network policy drift, budget exhaustion, privilege escalation via delegation, audit log tampering.

Does not protect against: compromised host/kernel, malicious human approvals, side-channel attacks, VM kernel escapes.

Versioning: v1.0 means the interface contract is stable (see STABILITY.md), not "production-secure by default." The lattice is heavily verified; the runtime is tested but not yet battle-hardened.

cargo build --workspace
cargo test --workspace
make demo              # taint → block → receipt → compartment switch

Licensed under either of Apache License, Version 2.0 or MIT license at your option.

• The Uninhabitable State — Simon Willison
• Lattice-based Access Control — Denning 1976, Sandhu 1993
• Verus: Verified Rust for Systems Code — SOSP 2025 Best Paper