Towards Real-World Industrial-Scale Verification: LLM-Driven Theorem Proving on seL4

Worthy read: https://microkerneldude.org/2025/04/27/benchmarking-crimes-meet-formal-verification/

Gernot was still skeptical about LLM based proof discharge, but its good to see it benchmarked on some theorems of sizable complexitiy yet realworld application.