Isabelle/HOL: Proof assistant used by Apple to verify corecrypto ML-KEM and ML-DSA
================================================================================

Isabelle/HOL is the prover Apple used with AutoCorres2, SAW and Cryptol to verify the ML-KEM and ML-DSA implementations in corecrypto (published 2026). It offers strong automation and a refinement methodology for C.

Maintainer: TU München and University of Cambridge
Website: https://isabelle.in.tum.de
Category: Proof assistants and general verifiers
Targets: C and ARM64 via AutoCorres2, Apple corecrypto
Approach: Higher-order logic with strong automation; refinement via AutoCorres2
Access: Open source (BSD)
Status: Active
Strengths: Powerful automation (sledgehammer). | AutoCorres2 for C refinement. | Industrial precedent (seL4, corecrypto).
Limits: Little ZK ecosystem presence. | Different culture and libraries from Lean/Rocq. | Refinement setups are heavyweight.
Firms using it: none listed
Sources: https://github.com/apple/corecrypto | https://isabelle.in.tum.de

Source page: https://sorryfree.com/frameworks/isabelle/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13