Comprehensive Formal Verification of Observational Correctness for the CHERIoT-Ibex Processor. - Louis-Emile Ploix; Alasdair Armstrong; Tom Melham; Ray Lin; Haolong Wang; Anastasia Courtney (CoRR, 2025)