lemire 评述 AI 推动形式化验证实用化

lemire 回顾形式化验证的发展，并指出多家初创公司正尝试用 AI 证明 C 代码及其内存安全等性质。文中以 seL4 约 20 人年的验证工作量为背景，提到 Truth 与 Harmatic 等项目，同时提醒这些方案仍建立在数学模型和假设之上。