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

Jianyu Zhang, Fuyuan Zhang, Jiayi Lu +5

Formal methods (FM) are reliable but costly to apply, often requiring years of expert effort in industrial-scale projects such as seL4, especially for theorem proving. Recent advan…