ORION: Formally Verified Hardware-Enforced AI Policy Governance — Architecture, Proof System, and Empirical Validation on AMD Kria KV260
Elisabeth Steurer, Gerhard Hirschmann · Zenodo (CERN European Organization for Nuclear Research) · 2026
We present ORION — a hardware-enforced AI policy governance system deployed on the AMD Kria KV260 (XCZU5EV SoC) and formally verified through 36 Z3 SMT theorems and 149 CBMC assertions. The system enforces a deterministic, three-valued gate function G: D × A → {EXECUTE, ESCALATE, REFUSE} on a physically isolated ARM Cortex-R5F core at 533 MHz in Lockstep mode. Empirical latency: median 3.051 µs (hardware core L1), 47.4 µs end-to-end (L3). 36 structural impossibility theorems proven including REFUSE-irrevocability, HITL-Liveness, Goguen-Meseguer Non-Interference, Emergency-set completeness, Lyapunov stability, and Ψ-Canonicalization. EU AI Act Art.14, STANAG 4774/4778, MiFID II Art.25, IDD Art.20. TRL 7, live API at api.paradoxonai.at.