Anthropic・Theorem、Claudeで123のOSSライブラリの「クラッシュしない」ことを形式証明　OSS-Fuzzの239エントリポイントが対象

Anthropicの研究記事によると、証明はRocqで書かれ、静的リンクしたシングルスレッドのRISC-V Linuxバイナリという前提のもとで、64MiBまでの入力でクラッシュやサニタイザの失敗が起きないことを機械的に検証できる形で示す。証明は1件あたり平均約60万行、合計で約1億8000万行に達した。作業の過程では実際のバグも見つかり、libexpatの既知のCVEも含まれていた。Theoremは同じ仕組みをOSS Verifyとして、条件を満たすオープンソースプロジェクトに無償で提供しており、メンテナはproject.yaml、Dockerfile、build.shを含むプルリクエストを送って参加できる。