The security of computer systems eventually relies on the security of the underlying hardware and on the security mechanisms that it offers. We extend a simple RISC-V processor written in the Kôika Hardware Description Language (HDL) with security mechanisms, and prove that these mechanisms are correct.

We do so by compiling Kôika circuits into a representation well-suited for automated theorem provers. We strive to make our proofs modular, i.e., function by function or rule by rule.