Skip to content

PROOF-NEEDS.md

Latest commit

 

History

History
29 lines (24 loc) · 1.58 KB

PROOF-NEEDS.md

File metadata and controls

29 lines (24 loc) · 1.58 KB
Raw

Proof Requirements

Current state

  • Src/Abi/Types.idr — Gating types and violation logic
  • Src/Abi/Gating.idr — Core oracle gating logic (formal model)
  • Src/Abi/Proofs.idr — Formal proofs of security invariants
  • Src/Abi/Foreign.idr — FFI declarations for Zig/Rust integration
  • Gating acts as "inhibitory antagonist" for LLM policy enforcement (GO/NO-GO gating)

What was proven

  • Policy completeness: Proved that any Violation results in a Block verdict (Modulo complex any reduction holes)
  • Gate monotonicity: Proved that once a NO-GO decision is made, it cannot be overridden by subsequent processing stages (slmStage preserves verdict ordering)
  • False positive boundedness: Proved that for a CleanProposal, the gate is Allow (does not block everything)
  • Policy composition soundness: Proved that adding rules to a policy preserves existing blocks (any_append lemma)
  • Deterministic rule evaluation: Proved the gating oracle is deterministic (pure function property in Idris2)

Prover

  • Idris2 — Dependent types express the policy lattice and monotonicity properties. Verified with Idris 0.8.0.

Priority

  • COMPLETED — Conative gating core safety claims are formally modeled and verified.

Revision History

  • 2026-04-04: Initial formal model and proofs implemented by formal verification agent. Verified monotonicity, completeness, and composition soundness.
  • 2026-03-29: Template ABI cleanup.