EHOX CBMC Formal Verification Harness — 198 Assertions · 0 Violations · ARM Cortex-R5F

Formal verification harness for the EHOX AI governance policy engine (ARM Cortex-R5F bare-metal). Running cbmc --arch arm --unwind 32 --bounds-check --pointer-check --signed-overflow-check --unwinding-assertions ehox_cbmc_harness.c produces: 0 of 198 failed (1 iterations) VERIFICATION SUCCESSFUL with CBMC 6.9.0. Verified properties S1–S18 cover: REFUSE/ESCALATE/EXECUTE invariants, domain isolation, default deny, output range, proof counter monotonicity, hardware enforcement bypass impossibility, domain-specific constraints (Aviation, Maritime, Energy, Finance, Biotech, Nuclear, Insurance, Emergency Override). Companion papers: ORION (DOI: 10.5281/zenodo.21818826), THEMIS (DOI: 10.5281/zenodo.21819020). Live verification API: https://api.ehox.io/formal This is the reproducibility artifact for the CBMC result cited in all EHOX publications. Independent verification is possible with a standard cbmc installation (apt install cbmc).