タグ: #formal-methods

한국어English日本語中文

← すべての記事

• Rust標準ライブラリ検証キャンペーンが見つけたメモリ安全性バグは0件だった

  AWSとRust Foundationが主導したverify-rust-stdキャンペーンの結果論文が、2026年のNASA Formal Methods Symposiumに掲載されました。著者たちが「ソフトウェアライブラリを対象に報告された中で最大の検証キャンペーン」と呼ぶこの取り組みは、自動生成ハーネス16,748件を作り11,970件を通過させましたが、標準ライブラリにおいて未知のメモリ安全性の脆弱性は一つも見つかりませんでした

  2026-07-16 · 47 分で読めます #formal-methods#rust#verification#memory-safety#testing

• Lean 4 & 定理証明支援系 2026 — mathlib / Rocq (旧 Coq) / Agda / Isabelle / FStar / AlphaProof / AIMO 深掘りガイド

  2026年、定理証明支援系(proof assistant)はもはや学界の秘密兵器ではない。Lean 4 は Leonardo de Moura が AWS に移って以来爆発的に成長し、mathlib は 100 万定理を超え、Terence Tao を含む一流数学者の日常の道具となった。Coq は 2024 年 3 月に Rocq へリブランドを完了し、Agda・Idris 2・Isabelle/HOL はそれぞれの位置を保つ。Mic

  2026-05-16 · 35 分で読めます #lean-4#lean#mathlib#rocq#coq