seL4’s AArch64 Security Proof Closes a Major Gap
Proofcraft’s August 2026 milestone adds a machine-checked confidentiality proof to seL4’s AArch64 functional-correctness and integrity story. Here’s what the result proves, why processor state makes the work challenging, and where the assumptions still matter.