Write-Once, Prove-Once: A Reusable Framework for Secure Boot Verification in Rocq. - Minjie Fan 003; Qiyu Wu; Kuai Yu; Gaosong Xu; Xiaoyang Wang 006; Jiwu Shu (ICPADS, 2025)