記事一覧へ
Frontier Red Team ブログの新着記事です。Claude を使った、大規模なソフトウェアの形式検証についてです。
形式検証は、コードに特定のバグがないことを証明できますが、これまでは小規模なコードベースでしか現実的ではありませんでした（あるいは、専門家の多くの時間が必要でした）。
しかし AI モデルによって、状況は変わり始めています。@theoremlabs と共同で、私たちは Claude を使い、数週間のうちに 100 を超える実在のオープンソースライブラリでセキュリティ特性を証明しました。
研究の全文はこちらをご覧ください: https://www.anthropic.com/research/formal-verification
形式検証Frontier Red Team研究security
Claude で大規模なソフトウェアの形式検証、100 超の OSS ライブラリで実施
出典: Anthropic（@AnthropicAI）さんの X の投稿を、日本語に翻訳して紹介しています。 原文はこちら ↗
9,7991,0746,6182,144,787
原文を表示 / Show original
New on our Frontier Red Team blog: using Claude to formally verify software at large scale.
Formal verification can prove that code is free of certain bugs, but historically it has only been feasible for small codebases (or required a lot of expert time).
With AI models, however, this is beginning to change. In collaboration with @theoremlabs, we used Claude to prove security properties in over one hundred real-world open-source libraries over the span of a few weeks.
Read our research in full here: https://www.anthropic.com/research/formal-verification