System 9 · The Stack
Privacy-preserving, formally verified compositional safety for multi-agent systems.
Safety is non-compositional: two individually safe agents can compose into an unsafe coalition via emergent conjunctive dependencies.
Per-agent safety checks are structurally insufficient. Spectral closes this gap.
Every system in the stack proves properties locally: CSC verifies each handoff edge, TokenGov proves each allocation round conserves budget, CCAP attests each agent's capabilities individually, Elan supervises each process in isolation.
None of them answers the critical question: is the composed system — all agents, all pipelines, all accounts, running simultaneously — safe?
This is not a gap that can be closed by making individual proofs stronger. It is a structural impossibility.
Formalises the full capability space as a directed hypergraph. Computes closure under conjunctive dependencies. Proves the closure does not intersect the forbidden set.
Agents prove their coalition is safe without revealing individual capability sets. Uses EconLib4's Crypto.ZeroKnowledge primitives — special_soundness and fiat_shamir.
When agents join, leave, or capabilities change, Spectral re-verifies safety via πdelta proofs without recomputing the full closure from scratch.
Polynomial-time partition of every capability into Safe (acquirable), Frontier (one step away), or Never (permanently forbidden). The speculum — the full snapshot.
The capability space is a directed hypergraph H = (V, E) where V is the universe of capabilities (including forbidden set F ⊆ V) and E is a set of directed hyperedges: each e = (S, t) means "possessing all capabilities in S enables acquiring capability t".
The closure Cl(A) of an initial capability set A ⊆ V is the smallest superset closed under all hyperedges. An agent or coalition with capabilities A is safe iff Cl(A) ∩ F = ∅.
| Result | Role |
|---|---|
| Non-compositionality (Thm 9.2) | Proves per-agent checks are insufficient |
| Lattice structure (Thm 9.3) | Offline preprocessing for online checking |
| coNP-completeness (Thm 9.4) | Complexity bounds for safety audit |
| Safe Audit Surface (Thm 10.2) | Core Spectral output: Safe / Frontier / Never |
| Submodularity (Thm 8.4) | Greedy (1-1/e) capability acquisition |
| Coalition Safety | Linear-time set-cover against precomputed antichain |
Coalition Safety Proof
Proves Cl(A1 ∪ ... ∪ An) ∩ F = ∅ without revealing any individual Ai. Each agent commits to its capabilities; the proof verifies against public commitments and the public forbidden set.
Incremental Update Proof
When one agent's capabilities change, proves the new composition remains safe given the previous πsafe. Avoids full recomputation — only the delta is verified.
Audit Surface Proof
Produces the Safe/Frontier/Never partition for any deployment state. The partition is public; the individual capability sets remain private. This is the speculum.
structure Speculum where
hypergraph : CapabilityHypergraph
forbidden : Finset Capability
commitments : Array (Agent × Commitment)
closure : Finset Capability
safe_region : LowerSet (Finset Capability)
antichain : Finset (Finset Capability) -- B(F), minimal unsafe boundary
audit_surface : AuditSurface
proof : SafetyProof -- π_safe
timestamp : NatThe speculum is recomputed incrementally whenever the capability state changes. Elan's supervisor consults it before any new agent composition. CCAP includes it in multi-agent execution traces.
Spectral consumes outputs from every system and provides guarantees back to all of them.
Crypto.ZeroKnowledge, Crypto.Commitment, Trust.ReputationSafety.CompositionalKey theorems to prove in EconLib4's new Safety.Compositional module.
Impossibility
∃ H F A B, safe H F A ∧ safe H F B ∧ ¬ safe H F (A ∪ B)
Constructive counterexample formalising Spera Thm 9.2
Structure
IsLowerSet (safe_region H F)
The safe region forms a lower set in the power-set lattice
Complexity
∃ alg, alg.output = audit_surface ∧ alg.complexity ≤ poly(|H| + |F|)
Safe Audit Surface is polynomial-time computable
Optimisation
Submodular (closure_gain H)
Greedy (1-1/e)-optimal capability acquisition guarantee
Soundness
verify π = true → ∃ As, all commit ∧ safe(⋃ As)
ZK coalition proof is sound: verification implies real safety
Privacy
safe As₁ ∧ safe As₂ → indistinguishable (prove As₁) (prove As₂)
ZK coalition proof reveals nothing about individual capability sets
Wave 4 adds coalition-hash-based staleness detection to the speculum lifecycle. Spectral now self-monitors whether its compositional safety snapshot is current, changed, or stale — and signals accordingly via MetaBus.
SHA-256 coalition fingerprinting computes a deterministic hash of the current coalition state. When compared against the stored coalition hash, Spectral auto-detects whether the speculum is still valid, has grown stale via TTL expiry, or the underlying coalition has changed.
Detection states:
TTL is configurable per deployment. On staleness detection, Spectral triggers incremental re-verification via πdelta rather than full recomputation.
Wave 4 introduces integration test suites covering the Spectral↔Elan and Elan↔TokenGov integration surfaces.
Tests cover freshness propagation, staleness escalation, TTL boundary conditions, and coalition-hash collision resistance.
When SpeculumFreshness detects a staleness or change condition, Spectral emits a structured event on MetaBus — the cross-system event bus — enabling downstream systems to pause coalition operations or trigger re-attestation flows.
The coalition_id identifies the affected coalition; reason carries :ttl_expired, :hash_changed, or :forced_invalidation. Elan subscribes to this event to gate new agent compositions until the speculum is refreshed.
Spectral sits between orchestration (Layer 1) and protocol (Layer 3) as a cross-cutting verification layer — the system that answers the one question no other system can.
Spera's theorem is an impossibility result. No amount of per-agent verification can guarantee compositional safety. You need a dedicated system-level verifier.
Consumes from CSC, TokenGov, Elan, CCAP, OpenCompliance, LegalLean. Provides guarantees back to all of them. The missing cross-cutting layer.
EconLib4 has special_soundness and fiat_shamir. CSC and CCAP reference ZK. But no system builds ZK proofs about composed state. Until now.
LegalEngine can tell regulators: "We have a zero-knowledge proof that the composed system remains within the safe operating envelope — without revealing proprietary details."
Phases 1–5 of the trustworthiness roadmap operationalise Spectral’s formal constructs inside the running stack. Each new module maps directly onto a core Spectral concept — forbidden-capability regions, safe closure sets, incremental forbidden-set updates, and compositional coalition safety.
CSC.CompetenceSignal creates a semantic analogue of Spectral’s forbidden-capability zone. When a SubTask’s confidence score falls below the uncertain threshold (0.40), synthesis is blocked — just as Cl(A) ∩ F ≠ ∅ blocks execution.
The capability being “forbidden” is: generating confident-sounding output with low epistemic grounding. CompetenceSignal enforces this at the vocabulary level via CertaintyVocabulary gating.
CSC.FiduciaryScope requires every deployment to declare an explicit authorised_action_set — the set of actions the stack may perform autonomously. This is the compliance analogue of Spectral’s safe region.
The pipeline cannot proceed outside this declared set, mirroring Spectral’s Cl(A) ∩ F = ∅ safety certificate. FiduciaryScope also requires licensed_entity and a liability_acceptance_hash (SHA-256), making the certificate operator-signed.
When TokenGov.NormfallAlert detects a struck norm (e.g. DOL fiduciary rule, 2026-03-18), the effective legal forbidden set F shifts — actions that were safe yesterday become unsafe today.
This is the semantic equivalent of Spectral’s incremental update proof (πdelta): the forbidden set changes, and the system must re-verify safety without recomputing from scratch. NormfallAlert tracks three norms: DOL_FIDUCIARY_RULE_2024 (struck, critical), SEC_AI_GOVERNANCE_2026 (active, high), FINRA_AGENTIC_AI_2026 (active, high).
CSC.PathwayAudit checks each SubTask against deontic obligations (FINRA 2026 + SEC 2026), proving pathway_compliance_compositional in Lean 4: if every SubTask is individually compliant, the full pathway is compliant.
This mirrors Spectral’s coalition safety question: if Cl(A1) ∩ F = ∅ and Cl(A2) ∩ F = ∅, is Cl(A1 ∪ A2) ∩ F = ∅? PathwayAudit answers the deontic analogue with a formal compositional proof — each SubTask is an “agent”, each deontic obligation is a forbidden-set element.