seL4 security proofs now complete on AArch64

Proofcraft has completed the formal proof that the seL4 microkernel enforces confidentiality on AArch64, the final piece of the security isolation proofs for that architecture. This means applications running on seL4 are mathematically guaranteed to be unable to access information without authorization. The milestone, supported by the UK's NCSC, completes the full security proof stack for 64-bit Arm, preventing attacks from propagating between critical and non-critical applications. The company also announced progress on MCS verification for RISC-V and a new dynamic domain scheduler API.