NotesNotes要点

• First machine-checked proof for Linux x86 glibc binary end-to-end execution.
• Formal verification reduces trusted base, covering compiler/language diversity.
• Lean-based x86 execution model and proof framework developed.
• AI-assisted proofs with human expert guidance for reusability.
• Edge-case glibc bugs discovered and reported during verification.
• Modular design significantly lowers proof costs for new binaries.

• 首次实现Linux x86 glibc二进制端到端机器验证证明
• 通过形式化验证减少信任基础，覆盖编译器和语言多样性
• 使用Lean语言构建x86执行模型及证明框架
• AI辅助证明生成，人类专家指导确保可重用性
• 验证过程发现glibc边界情况bug并报告
• 模块化设计使不同二进制证明成本显著降低

• Linux x86 glibcバイナリのエンドツーエンド機械検証証明を初めて実現
• 形式化検証により信頼ベースを縮小し、コンパイラや言語の多様性をカバー
• Lean言語を用いてx86実行モデルと証明フレームワークを構築
• AI支援による証明生成、人間の専門家が再利用性を確保
• 検証過程でglibcのエッジケースバグを発見し報告
• モジュール設計により、新規バイナリの証明コストを大幅に削減