Keane Lucas, Aengus Lynch, Luna Tong, Luke Champine, Zygi Straznickas, Dino Distefano, Harshikaa Agrawal
Evyatar Ben Asher, Ava Howell, Sami Jawhar, Chris Rohlf, Nickolai Zeldovich
Nicholas Carlini, Rajashree Agrawal, Jason Gross
ほとんどのソフトウェアはバグだらけであり、AIは現在それを容易に—— 見つける および エクスプロイト。サイバー攻撃に対する従来の防御策はもはや十分ではありません。コードにバグがないことを証明する方法が必要です。形式ソフトウェア検証はこの保証を提供できる可能性がありますが、歴史的に専門家による長年の努力を必要とし、ほとんどの実世界のプロジェクトでは非現実的なものでした。以下との共同研究において 定理しかし、本研究ではこれはもはや当てはまらないことを示します。LLMは現在、大規模に形式的証明を生成できるようになり、証明されたセキュリティ保証を含む新しいソフトウェア開発ワークフローを可能にしています。Claudeを用いて、100を超える実世界のオープンソースソフトウェアライブラリにおいて、アセンブリコードレベル(RISC-V)でのセキュリティ特性を証明しました。 我々の知る限り、これはAIを活用して、アセンブリコードレベルで本番ソフトウェアに形式的検証を適用する初の大規模な取り組みです。 証明を書いている最中に、Claudeは長年見逃されてきたバグも発見しました。にもかかわらず 数兆回のテスト実行モデルの能力が向上し続けるにつれ、形式的検証が安全なソフトウェア開発に不可欠な一部になると期待しています。
はじめに
たとえ成熟し、十分にテストされたソフトウェアであってもバグを含んでおり、LLMも同様です。 ますます熟練度を増している 発見することに長けている。今日最も入念にテストされたソフトウェアの一つであり、世界中の数十億台のデバイスに展開されているLinuxカーネルは、最近 1,000件を超える脆弱性 開示されました。フロンティアモデルがますます高性能になるにつれ 一見無害なバグの連鎖 深刻な脆弱性に発展する前に、こうしたバグを実環境で悪用される前に検出し修正できる技術が必要です。
理想的には、こうした技術によって発見と修正が可能となる。 すべてのバグ、 その後、これ以上見つからないことを裏付ける証拠をいくつか示します。 形式検証 その方法の1つがこれである。形式検証では、開発者はコードを数学的モデルに変換し、それが定義された一連のセキュリティルールに常に従うことを証明しようとする。証明に失敗した場合、それはルールに違反するバグがコードに存在する可能性があることを意味し、失敗の性質からそのバグが何であるかが推測できる。このプロセスを(その都度失敗の原因を取り除いた上で)繰り返すことで、最終的には、それらのルールに違反するバグがコードには一切存在しないことの証明が得られる。
しかし、形式検証は容易ではありません。証明は元のコードの何倍もの大きさになることがあり、その作成には多大な労力と、ニッチで高度に専門化されたスキルセットが必要です。たとえば、seL4オペレーティングシステムカーネルの実装には2人年を要しましたが、 20 人年 形式的に検証するために「そのため、形式的検証は、以下のような真にミッションクリティカルなアプリケーションにおいてのみ実用的でした。」 エアバスのアビオニクスコード.
しかし、LLMはこれをはるかに容易にしています。フロンティアモデルは現在、実世界のソフトウェアの正しさの証明を完全に自律的に生成できます。これを実証するために、私たちはClaudeに、123のオープンソースライブラリにわたる有用なセキュリティ特性の証明を依頼しました。その中には、一部の実行可能アーティファクトが特定の条件下では 決して 特定の条件下でのクラッシュ。具体的には、Claudeは、64 MB 未満のすべての入力、およびモデル化されたすべての Linux オペレーティングシステム（OS）の応答とメモリレイアウトについて、特定の仮定（すなわち、プログラムが RISC-V 上で固定のメモリ予算を持つシングルスレッドの静的バイナリとして実行されるという仮定）の下で、これらのプログラムがメモリ安全性エラーを引き起こしたりアサーションに失敗したりすることなく、常に正常に終了することを証明しました。1 CPU上で、固定のメモリ予算を持つシングルスレッドの静的バイナリとして実行されるという仮定）の下で、64 MB未満のすべての入力、およびモデル化されたすべてのLinuxオペレーティングシステム（OS）の応答とメモリレイアウトに対して、これらのプログラムがメモリ安全性エラーを引き起こしたりアサーションに失敗したりすることなく、常に正常に終了することを証明しました。これは依然として すべての 可能なバグを修正するにはほど遠いものですが、以前よりもはるかに前進しており、その目的に向けたロードマップを提供するものです。
私たちは以下を公開しています これらの証明の部分集合 誰もが検証し再利用できるようにするとともに、 RISC-V と OS のセマンティクス. 定理、このプロジェクトの協力者であるところの、同様のパイプラインの実行も以下の対象について提供している その他のオープンソースプロジェクト、そして公開している Claudeスキル 開発者が自分のコードの検証を始められるよう支援するためです。
形式検証は多くの手法を含む幅広い分野です。以下では、zlib圧縮アルゴリズムのセキュリティ評価、Rustで書かれたPythonインタプリタの動作等価性の証明、重要なソフトウェアにおける長年のバグの摘出など、他のセキュリティタスクやソフトウェア開発タスクを加速するための他の形式検証手法を用いた初期の探索についても説明します。
形式検証の未来は有望です。モデルがより知的になるにつれ、証明を書くコストは低下しつつあります。さらに、より多くのコードが形式化され、セキュリティ保証を達成する手法がより標準化されるにつれて、コードベース間で証明を再利用・修正する能力がそのコストを償却してくれるでしょう。すべての開発者に、LLM を活用した形式検証を探求することをお勧めします——特に 以前あまり性能の高くないモデルで試してみたものの、うまくいかないと感じた人たちです。
この投稿の残りの部分では、私たちの形式検証の実験についてより詳しく説明します。
テストを証明に変える
ソフトウェアが正しいことを証明するには、まず「正しい」とはそもそも何を意味するのかを明示しなければなりません。正しさは次のように定義されます。 仕様 (仕様)。一部のプログラムでは、プログラムの意図された動作を正式に記述する明確な方法があります。たとえば、 PNG デコーダはバイトのシーケンスを受け取り、(続く RFC 2083) これらのバイトを対応する画像にデコードします。しかし、ほとんどのプログラムでは、そう単純ではありません。テキストエディタやウェブブラウザが「正しい」とはどういうことでしょうか。包括的で曖昧さのない仕様を入手することの難しさは、より大規模なソフトウェアの検証における重大な障害となっています。
私たちが証明しようとしたオープンソースライブラリのコードについてこの課題に対処するため、既存のコンパイル可能なテストスイートを、Linux上で任意のRISC-Vコンパイル済みバイナリを実行するとはどういうことかの一般的なモデルを用いて「このテストスイートは常にパスする」というルールをエンコードすることで、仕様へ自動変換するアプローチを取りました。歴史的に、このような仕様の証明は困難でした。それは、あらゆる入力に対して数万のアセンブリ命令のすべての可能な挙動と相互作用を包含し、それについての議論を行う証明を書くことの本質的な複雑さ(そして、その結果として証明が極めて大きくなりがちなという事実)によるものです。ここで今日のLLMが登場します。明確に定義された目標に向かって数百万行のコードを処理することは、LLMが非常に適したタスクなのです。
このプロジェクトでは、まず fuzz tests(ファジングテスト)。これらのテストでは、開発者は エントリポイント2 自分のコードに、入力を受け取る処理を組み込んでおきます。そうすれば、クラッシュを引き起こす入力はすべて、作者が関心を持つバグとなります。そして ファザー、 テストエンジンの一種であるファザーは、エントリーポイントに対して膨大な数の半ランダムおよび変異させた入力を生成し、バグの発見を試みます（図1に視覚化）。ファザーは実行時間が長いほど、より多くのバグを発見できます。しかし、これは本質的にブルートフォース（総当たり）的なプロセスであり、どれだけ多くの入力を試しても、すべての可能なコードパスを通過させる保証はありません。
ファジングテストによって表面化されたはずのすべてのバグを見つけるために、私たちはそのファジングテストを、コンパイルされたRISC-V命令上で定義された仕様に変換しました。この仕様は、そのファジングテストが 任意の 64 MB未満の入力に対してクラッシュしないことを述べています。3 Claudeがこの仕様を証明できれば、RISC-V上でのファジングテストは不要になります。そのエントリーポイントをファジングしても、バグは決して見つからないからです。
私たちはこの取り組みを、適格なオープンソースプロジェクトに継続的なファジングテストを提供するGoogleの OSS-Fuzz イニシアチブに含まれる数百のプロジェクトに対して実施しました。OSS-Fuzzには、クラッシュすること(例えばアサーションの失敗時)によって壊れたコードの特性を探す、開発者が作成した何千ものエントリーポイントが含まれています。OSS-Fuzzは、CおよびC++プログラムにAddressSanitizer4 (ASan)を自動的に組み込み、メモリが不適切にアクセスされた場合にプログラムをクラッシュさせます(これは ソフトウェアの脆弱性の主な原因です)。メモリ安全性のような広範な仕様は、ほぼすべてのソフトウェアに適用されます。
数週間の間に、 Claudeは発見したバグの修正に成功し、123の異なるOSS-Fuzzライブラリにわたる239のエントリポイントについて、64 MBまでのあらゆる入力でクラッシュが発生しないことを証明しました。 これらの証明はコンパイル済みのRISC-V命令（すなわち実行可能バイナリ）を対象としており、約180百万行のRocqで構成され、典型的な証明は約600,000行に及び、中央値18,000命令のRISC-Vバイナリに対してセキュリティ保証を提供します。これらの証明は、TheoremのRISC-V命令セマンティクスとLinuxプロセスセマンティクスを用いてRISC-Vアセンブリコードを数学的モデルに変換することで構築されています。つまり、現時点でこれらの証明は、プログラムがLinux OSを使用するRISC-V CPU上で、固定のメモリ予算を持つシングルスレッドの静的バイナリとして実行されることを前提としています。これらの証明の対象範囲を拡張することは十分に手の届く範囲であり、より多くのアセンブリアーキテクチャや他のオペレーティングシステムプロセスのためのセマンティクスを標準化することになります。参照 専門家の見解 Claudeが書いた証明について。
これは膨大な量の証明コードですが、そのうち手動でレビューが必要なものはほとんどありません。Rocq証明検証器が、証明によって仕様が正しく満たされていることを保証します。その結果、開発者が信頼する必要がある成果物は以下のみとなります:
- RISC-VおよびLinuxプロセスの形式的モデル;
- 証明された正確な定理の記述。
- Rocq証明チェッカーそのもの。5
これは、これらのライブラリにバグが一切含まれていないことを意味するものではありません。 代わりに、それは次のことを意味する。すなわち、いかなる 残りのバグは、上記の成果物の中に存在するか、あるいはClaudeによる証明の範囲外にあります. 依然としてバグを含む可能性のある信頼されたコンポーネント(Rocq、RISC-V、Linuxのセマンティクス)を強化することは決して容易ではありませんが、スケールアウトされた証明がカバーするすべてのコード行をデバッグする作業に比べれば、はるかに手に負えるタスクです。特に、このアプローチは信頼されたコンポーネントのサイズを増やすことなく、任意の数のプロジェクトを保護できる点で有用です。
我々は証明の独立した検証を歓迎し、このアプローチの改良を奨励しています。そのため、このプロジェクトのために作成した、まだ公開されていない信頼済みコンポーネント(上記)、パッチを必要としなかったファズテストに関するClaudeの完全なRocq証明、および証明できなかったその他のファズテストの仕様を公開します。
バグの発見と修正
上記で、多くのオープンソースライブラリの開発者記述テスト(ファジングテスト)を、Claude が常にパスすることを証明できる仕様に変換できることを示しました。場合によっては、見つかった残りのバグを修正した後でパスします。このため、これらの仕様を証明しようとするプロセスは、数百のバグを発見しました。
Claudeが数百のエントリーポイントを証明しようとした際に、多くのバグが見つかりました。Claudeがそのたびに人間の手を止めて待たなくて済むよう、見つけたバグをClaude自身に修正させました。つまり、コードにパッチを当て、そのパッチ適用後のコードから仕様を再生成し、その後Claudeがその新しい仕様の証明に進むという流れです。6
私たちが発見したバグの多くは、ファザーではまず見つけられないようなものでした。ファザーは小さな入力を変異させますが、 通常は1 MBに制限されているまた、通常はコードカバレッジに頼ってバグへと導かれます。あるライブラリのエントリポイントを証明している最中に、Claude は、同梱されていたデコンプレッサ（伸長器）のコピーにあるカウンタのアンダーフローを発見しました。これは範囲外への書き込みを引き起こすものでしたが、約20 MB かつ稀な特定のレイアウトを持つ入力でのみ発生するものでした。その他のバグとしては、64 MB の入力と 2 GB を超えるメモリを必要とする画像デコーダの範囲外読み取り、同じファイルへの2つのハンドルにまたがる特定の呼び出しシーケンスを必要とする別のライブラリの範囲外読み取り、そして深くネストした入力を必要とした libexpat の CVE-2026-56132 の再発見が挙げられます。Claude はまた、まったくクラッシュしないロジックバグも発見しました。たとえば、あるライブラリがメモリ安全であることを証明している際に、アプリケーションがロードできるファイルを制限する機能が常に強制されているとは限らないことに気づいたのです。
このプロジェクトの最終的な目標は、RISC-V向けにコンパイルしたファジングテストに、これ以上発見すべきクラッシュが残っていないことの証明を得ることでした。しかし、上述のようなバグは、その目標が達成されるかどうかにかかわらず、このプロセスには別のメリットがあることを示しています。つまり、このプロセスを試みただけでも、修正が必要な実際のバグが見つかるのです。
メモリ安全性以上の実証
ファズテストにこれ以上クラッシュが見つからないことを証明することは、思った以上に重要です。実際のコードのファズテストでは、エンコード・デコードのラウンドトリップ、冪等性、代数的法則、差分テスト、自己整合性、リファレンス実装との等価性といった意味のある高レベルの性質の違反を検査するのが一般的です。たとえば、LZO圧縮アルゴリズムのファズテストは、入力を圧縮してから解凍すると、結果が元の入力と同じになることを表明します。この性質が成り立たなければプログラムはクラッシュするため、テストが決してクラッシュしないことを証明することは、性質そのものを証明することと等価です。
これは、プロパティが開発者によって直接指定されていない場合にも起こりえます。たとえば、Claudeがcpp-httplibのOSS-Fuzz証明を完了するには、std::setのデストラクタにおける再帰の深すぎる呼び出しによるスタックオーバーフローの可能性を排除する必要がありました。この再帰の深さは木の最大の深さによって制限されるため、Claudeはlibc++の赤黒木の再平衡化アルゴリズムが木の深さを対数的に有界に保つよう正しく最適化されていることを（マシンコード上で！）証明しなければなりませんでした。
その他の形式検証の事例研究
形式的検証は幅広い分野です。前述のファズテストから証明への例は、機械語に証明を直接適用することで、LLMが形式的検証をより広く利用しやすくしている一例です。
また、LLMと形式検証を組み合わせた他の活用でも成功を収めています。たとえば、Claudeに次のことの形式仕様を書かせました RFC 1950, すなわち zlib 圧縮ファイルフォーマットを定義する技術文書です。次に、Linux カーネルの zlib 実装がその仕様を正しく実装していることを Claude に証明させました。上記の例と同様に、Claude はこの性質をバイナリレベルで証明しましたが、RISC-V の代わりに、Claude が生成し(徹底的にテストされた)x86 ISA の形式的意味論を用いて、x86 でコンパイルされたバイナリを直接証明しました。7 その後、同じプロセスを広く使われている他の半ダースのライブラリについても繰り返しました。その過程で、エッジケースにおけるいくつかの軽微な(悪用不可能な)バグが見つかり、現在それらを上流に報告する手続きを進めているところです。この取り組みから2つの結論を導き出しました:(1) これらの極めて入念にテストされたコードベースはすでにほぼ完全に正しいこと、そして (2) 実際に存在する現実のコードベースについてエンドツーエンドの正しさの性質を証明することが可能であること。
別の実験では、ClaudeにRustでPythonの大規模なサブセットのインタープリタを開発させ、ある学術論文に示されたCPythonのセマンティクスに準拠していることを(検証ツールであるRust用のVerusを用いて)証明するよう求めました。その後、170万件以上のランダムに生成されたPythonプログラムを実行してCPythonの動作との一致度を経験的に測定したところ、テストの99.95%でCPythonと同一の動作が確認され、残りのテストの差異は驚くほどのない既知のコーナーケースでした。
私たちは、シンプルなセキュリティ特性の形式的検証を試みることを通じて、広く使われている複数の重要なアプリケーションにも問題を発見しました。そのうちの1つでは、10年以上潜在していた未知のロジックバグを発見しました。広く使われているPDFリーダーの検証作業の中で、私たちはわずか1週間で、通常1年間で報告されるのと同数のセキュリティバグを見つけました。
参照 付録 これらの取り組みの一部に関する詳細については。
これはまだ始まりにすぎません
LLM支援による形式的検証の主要な限界のひとつは、証明の生成に数億トークンを要する可能性があることです。これらの手法をソフトウェアエコシステム全体で利用可能にすることが目標であれば、コスト効率は極めて重要です。幸い、効率が向上すると期待できる説得力のある理由があります。
新型モデルはより少ないトークンで済む
私たちは36の小さな検証タスクを作成しました 実在のOSS-Fuzzコードから。Opus 5.5 は、そのうちの半分を、Opus 5 より約 40% 少ないトークンで証明しました。長い検証タスクでモデルが訓練されるにつれ、この傾向は続くと予想されます。
証明は再利用可能です
エージェントがそれぞれ別々に作業すると、多くの労力が重複してしまうことがよくあります。証明はソフトウェアと同じように、より小さな証明から再帰的に構築されます。そして証明が小さいほど、再利用しやすくなる傾向があります。この影響を測るために、エージェントがそれぞれのターゲットの証明に取り組む際に、互いの証明をコピーできるようにしました。この共有ワークスペースへのアクセスを与えられたところ、エージェントは単独で作業した場合と比べて17%少ないトークンで済み、単独では失敗していた一部のエージェントはその後に成功さえしました。
私たちはOSS-Fuzz証明の取り組みの中で、同じ現象が大規模に起こるのを観察しました。証明の大部分は、あらゆるプログラムが含むコード(特にCランタイムとAddressSanitizerの初期化)に関係するため、まったく異なるプログラムでも大幅に重複する証明になり得ます。エージェントチームはこれを利用し、他のチームの完成した証明をコピーしてから自分たちのプログラムに適合させることで効率化しました(図6)。
このような証明の再利用性こそが、 MathlibというLeanによる形式数学の共有ライブラリが、700人以上のコントリビューターによって提出されたほぼ 300,000 700人以上の貢献者によって提出されました。新しい証明はそれぞれ、既存の研究成果の上に築かれます。私たちもOSS-Fuzzの取り組みの過程で同様の証明の集積を蓄積しており、その一部は今回のリリースに含めています(オープンソースソフトウェアにおける未修正のバグを明らかにし得る証明はリリースしていません)。
これらの初期実験から先へ進むには、最も重要な依存関係から始めて、膨大な 既存 ソフトウェアを検証するための戦略が必要です。示したように、これは汎用の仕様を用いバイナリレベルで作業することにより、コードベース全体を別の言語で書き直す必要を回避しながら、大規模に達成できます。
このアプローチは、パッケージ単位の粒度での証明の再利用も促進します。つまり、各依存関係は一度検証すればよいということです。依存関係はべき乗則に従います。共有ライブラリの小さな集合を証明するだけで、ソフトウェアの非常に大きな部分が証明可能になります。詳細については、glibc、OpenSSL、cURLなどの重要なインフラを含むNixエコシステム全体を検証するための Theoremのロードマップ glibc、OpenSSL、cURLといった重要なインフラを含む、Nixエコシステム全体を検証するためのものです。
限界
実際には、形式検証はコードのセキュリティについて、私たちが望むほど多くを証明できないことがあります。
「形式検証済み」は「バグなし」を意味しません。 Claudeは、コンパイルされたプログラムの動作が形式仕様の要件を満たすことを示す証明を書くことができます(この証明は外部の証明チェッカーによって検証されます)。しかし、証明チェッカーは、その仕様が現実と一致しているかどうかを教えてはくれません。現実と一致させるには、仕様が、検証されたプログラムが動作する現実のマシン(CPUやオペレーティングシステムを含む)に関するすべてを正しく包含しモデル化していなければなりません。検証済みコードにバグが現れるのは、仕様、あるいはマシンの想定された意味論が現実と異なるためです。幸いなことに、これは残るバグを どこ に探せばよいか、そしてまだバグを含み得るギャップを最小化するシステムをどう設計すればよいかを私たちが知っていることも意味します。以下は、これが私たちの証明に当てはまる場合の説明と、それらのギャップを閉じるための今後の作業のアイデアです。
現実のマシンが、モデルに記述されていないことを行う。 私たちの証明は、musl libcにリンクされたシングルスレッドの静的RISC-Vバイナリに関するものです。しかし、ほとんどの人はこれらのライブラリをx86やARM上で動かし、glibcに対して動的リンクします。このギャップを閉じるには、デプロイされたシステムにより近いシステムモデルが必要です。例えば、その一歩としてはx86の正確な意味論を生成することが挙げられます。
主張が、私たちが気にするすべてを網羅していない可能性がある。 私たちは、Google OSS-Fuzzの多くのファジングエントリポイントにおいて、ASanのクラッシュを含め、64 MB未満のあらゆる入力に対してクラッシュが決して発生しないことを証明しました。しかし、ASanはすべてのメモリ安全性のバグを検出するわけではなく、各ライブラリのすべてのエントリポイントを検証したわけでもありません。たとえ検証していたとしても、すべてのエントリポイントを検証してもライブラリ全体がカバーされるわけではありません(特にデッドコードがある場合)。さらに、実際のプログラムがライブラリを誤用し、 呼び出し元でメモリ破壊が起こる可能性があります。このギャップを閉じるには、各公開関数について呼び出し元が何をすべきかを仕様として定め、呼び出し元がそれを厳密に守る必要があります。
形式手法へのLLMの活用についてさらに学び、モデルが改良され続けるにつれて、これらの限界は扱いやすくなり、私たちが依存するコードのはるかに大きな割合を検証できるようになると期待しています。
結論
軌道は明らかです。歴史的に、形式検証は最も安全性が重要なコードにおける専門家が手作りする特注の保証にのみ実用的でしたが、まもなく、ほぼすべての本番ソフトウェアにとって今日のファジングと同様に実用的なものになるでしょう。静的型付け、テストフレームワーク、その他の正確性ツールと同様に、検証は「後付け」から「組み込み」へと成熟していきます。それはLLMだけでなく、言語設計や開発ワークフローの革新によっても推進されます。
LLMが自動的にコードの脆弱性をスキャンし、ますます多くの脆弱性を発見する今日の世界では、コードのセキュリティ特性を 保証 できるプロセスを使わなければなりません。LLMスケールの形式検証は、これまで達成できなかった範囲と規模でこれらの保証を確立する有望なアプローチです。私たちは、堅牢なソフトウェアが広く普及し、ソフトウェアのバグがよく理解され迅速に対処される珍しいものとなる世界を共に築くため、他の方々にも実験することを奨励します。
脚注
01RISC-Vは、x86やARMと同様のプロセッサ設計であり、ソフトウェアがコンパイルされるアセンブリ命令（チップが実行する基本コマンド）を定義するものです。
02エントリーポイントとは、コードへの正面玄関であり、その作者がテスト用に提供するものです。エントリーポイントへの入力のうちクラッシュを引き起こすものは、作者が関心を持つバグです。
03これを増やすには、パラメータを変更して仕様を再生成し、Claudeにその命題を再証明させるという、ごくわずかな人的労力しか必要としません。
04AddressSanitizerは、プログラムにチェックを追加するコンパイラツールであり、バッファオーバーフローやuse-after-freeといったメモリエラーが、実行時に発生した瞬間に検出・報告されるようにします。
05これは技術的には、Rocq証明チェッカーが依存するハードウェア、OS、OCamlコンパイラも信頼しなければならないことを意味します。
06なお、これには報酬ハッキング（reward hacking）の余地が残ることに注意してください。報酬ハッキングとは、AIモデルが、実際に意図されたことを行わずに、技術的には与えられた目標を満たす近道を見つけることです。例えるなら、内容を学ぶのではなく解答集を暗記して試験に合格する学生のようなものです。この文脈では、Claudeがプログラムを、自明に決してクラッシュしないものに書き換えることで、どんな定理でも証明可能にしてしまうおそれがありました。これを防ぐため、パッチにはペナルティを課し、どの入力を変えるかとその数がどれほど少ないかを証明した場合には加点を与えました。また、これらの失敗モードに対応するパッチを記録・監査しました。
07私たちは、ClaudeがISAの形式的意味論を——完全に自律的に——生成できるということは、別の興味深い教訓だと考えています。私たちの意味論自体が完璧だと断言はできませんが、経験的には、この意味論に沿って1ステップずつ実行することで、Linuxカーネルの上でUbuntuのユーザースペースを起動できることが分かっています。また、これらの意味論の生成により、公式リファレンスドキュメントにおける数百の誤りや、ハードウェア自体の少数のバグが特定されました。