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

Quick Start

cargo install --git https://github.com/coproduct-opensource/nucleus nucleus-cli
nucleus audit                       # scan agent configs (Tier 0, no runtime)
nucleus run --local "your task"     # run with enforced permissions (Tier 1)

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.

What Gets Proved

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

The Flow Algebra

Per-Call SPIFFE Provenance (preview)

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:

spiffe://<trust>/ns/<ns>/sa/<sa>                                   ← pod (root)
  /call/<uuid>/tool/<tool>                                         ← tool call
  /call/<uuid>/llm/<provider>/prompt/sha256:<hex>                  ← LLM input
  /call/<uuid>/llm/<provider>/response/sha256:<hex>                ← LLM output
  /call/<uuid>/derived/sha256:<hex>                                ← downstream artifact

Identical content → identical content-hash suffix, regardless of derivation path. The full path is a human-readable witness of the derivation chain.

Try it end-to-end (Bash → Write → mock-LLM with self-loop JWT verification — the mock LLM uses the same in-process key the issuer minted with, so this proves the JWT format, not cross-trust federation):

cargo run -p nucleus-lineage --example three_step_demo
nucleus lineage <leaf-spiffe-id> --log ./nucleus-lineage.jsonl

Output formats: --format tree (default), json, or dot (for Graphviz).

Treat the categorical framing — "per-call SPIFFE IDs lift the workload category to a bicategory; cocycle condition becomes verifiable" — as a roadmap, not as currently load-bearing. See crates/nucleus-lineage/README.md for the longer story and the explicit limitations.

How Nucleus Stops Real Exploits

Three Deployment Tiers

Architecture

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)            │
│  nucleus-lineage  (per-call SPIFFE DAG)      │
├──────────────────────────────────────────────┤
│  Firecracker microVM / seccomp / netns       │
└──────────────────────────────────────────────┘

Crates

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

Known Gaps

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.

Threat Model

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.

Development

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

License

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

References

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