Antigravityのスラッシュコマンドとは スラッシュコマンドとは、チャットの入力欄で「/」から始まるコマンドを入力することで、Antigravityの特定の機能やワークフローを呼び出す仕組みです。

本ブログは 2026 年 8 月 31 日に公開された Amazon Science Blog “ Developing provably correct Rust code with Verus ” を翻訳したものです。 コードをその機能の数学的な仕様に照らして自動的に検査する「プログラム検証ツール (program verifier)」である Verus が、ソフトウェアプロジェクトのセキュリティ保証をどのように高めるのかを紹介します。 オープンソースや企業のソフトウェアプロジェクトの多くが Rust プログラミング言語を採用しており、 いくつかの事例 は Amazon 社内 にもあります。Rust が選ばれているのは、C 言語に匹敵するパフォーマンスと柔軟性を備えつつ、洗練された型システムによってさまざまなバグやセキュリティの脆弱性を自動的に防ぐからです。その結果、平均的なコードよりも正しく安全で、しかも高速なコードが得られます。 しかし、「より正しく安全である」ことは「実際に正しく安全である」ことと同じではありません。例えば C では、配列の範囲外アクセス (out-of-bounds access)、つまり配列に割り当てられたメモリの境界を越えたインデックス指定は、予測できない結果を招く危険な誤りです。Rust では範囲外アクセスが起きるとプログラムが停止するため、確かに安全性は高まりますが、本当に正しいプログラムであれば、そもそも範囲外アクセスは起こりません。同様に Rust は、プログラムが期待どおりの結果を計算することや、自身がアクセスできる機密情報を漏洩しないことまでは保証できません。ここで役立つのが Verus です。 配列の範囲外アクセスは、予測できない結果を招く危険な誤りです。正しいプログラムであれば、これを許しません。 Verus とは Verus は、Rust 向けのオープンソースの自動プログラム検証ツール (program verifier) です。プログラム検証ツールは、コードがどのように振る舞うべきかを記述した形式的な数学的仕様を受け取り、あらゆる入力に対してコードがその仕様に一致することを機械的に検査します。 例えば、ソート済み配列から特定の値を探すために、最適化した二分探索アルゴリズムを実装したコードがあるとします。仕様には、コードがインデックスを正常に返した場合に、配列内の対応する要素が目的の値と一致することを記述できます。検証ツールは、あらゆる入力配列と目的の値についてこの仕様が成り立つことを検査します。 一方、従来のテスト手法では、いくつかの特定の配列を試すことはできても、コーナーケースを見落とすおそれがあります (目的の値が配列の最後の要素である場合や、そもそも存在しない場合など)。プログラム検証で重要なのは、コードが仕様に一致することを示す数学的な 証明 を構築する点です。Verus のような 自動 プログラム検証ツールでは、証明構築のうち退屈で低レベルな手順の多くをツールが自動的に処理し、人間の開発者は高レベルな指示を与えます。例えば、帰納的証明の設定やループ不変条件 (loop invariant) の提示などです。以下で説明するように、最近ではこうした高レベルな手順も多くの場合 AI で自動化できます。 Amazon は Rust Foundation の創設メンバーであることを誇りに思っており、さまざまなプロジェクトで Rust を幅広く活用しています。例えば、AWS Lambda と AWS Fargate を支える Firecracker 、Amazon のサーバーレス分散 SQL データベース、そして Nitro Isolation Engine などです。Nitro Isolation Engine は、Amazon Web Services (AWS) の仮想マシン割り当てを管理するソフトウェアである Nitro Hypervisor のために、仮想マシンの分離を強制するものです。Amazon の Rust に対する熱意と、 10 年以上にわたる自動推論への取り組み を踏まえれば、Amazon が書く Rust コードにさらに強力な保証を与えるために Verus を採用するのは自然な流れです。実際に Amazon は、Nitro Isolation Engine が使用する主要なプリミティブや、Amazon 社内の複数の重要なインフラストラクチャについて、Verus を用いて正しさを証明してきました。こうしたユースケースは今後の記事で取り上げる予定です。まずは、Verus で Rust コードを検証するとはどういうことなのかを詳しく見ていきましょう。 Verus による Rust コードの検証 Verus を使うと、Rust 開発者は既存の Rust コードに対する仕様 (および証明) を Rust のソースファイルに直接追加できます。先ほどの二分探索の例を発展させて、探索関数の既存の Rust 実装に対する次の Verus 仕様 (Rust のアノテーションとして記述) を見てみましょう。 Rust のアノテーションとして記述された、探索関数の Rust 実装に対する Verus 仕様。 事前条件 (precondition) は requires キーワードで示され、関数の実行前に真でなければならない条件を記述します。この例ではコードが二分探索を実装しているため、配列がソート済みであることを要求します。 事後条件 (postcondition) は ensures キーワードで示され、関数の実行後に真でなければならない条件を記述します。この例では、関数が Some(index) を返す場合に index が配列の範囲内にあり、そのインデックスにある配列要素の値が、探していた値と一致することを示しています。 重要なのは、関数が None を返す場合には目的の値が配列内に 存在しない ことも示している点です。この 2 つ目の条件がなければ、常に None を返す実装でも仕様を満たしてしまいます。なお、通常の Rust コンパイラはこれらの Verus アノテーションを無視します。そのため、Verus のアノテーションが付いたコードは、Rust のビルドツールである Cargo を使うプロジェクトを含め、検証済みのプロジェクトでも未検証のプロジェクトでも利用できます。 この例は、Verus が採用している重要な設計上の判断も示しています。これは、他の多くの Rust 検証手法とは異なる点です。Verus では、 開発者 が Rust に似た構文を使い、自分のソースコード内に仕様と証明を記述します。証明が失敗すると、ソースレベルで表現された Rust スタイルのエラーメッセージが表示されます。このアプローチにより、証明と実際のコードの同期が保たれ、開発者は仕様や証明のためにまったく新しい言語やツールを学ぶ必要がなくなります。また、コードを書いた開発者、つまりそのコードを最もよく理解している人が、正しさを証明するプロセスにかかわることができます。 Verus は、高速で強力な自動化にも力を入れています。そのために、さまざまな ソルバー (solver) を使用して、プログラムとその仕様から生成される証明義務 (proof obligation) を解消します。実際には、開発者は通常 1 秒未満でコードと証明に関するフィードバックを得られます。これは、対話的な開発ループ (VS Code のような対話的な開発環境に表示される「赤い波線」を含む) を実現できるほどの速さです。 プロジェクト単位で見ると、Verus は数千行のコードと証明を含む複雑なプロジェクトを、従来の一部の自動プログラム検証ツールが個々の関数を検証するのに要していた時間で検証できます。この強力な自動化と高速なフィードバックループは、人間に有用なのは言うまでもなく、AI エージェントが Verus の証明を作成する際にも役立ちます。自動化が進んでいればエージェントの作業は少なくなり、証明の修正と検証をよりすばやく繰り返せるからです。 Rust の型システムは強力な安全性保証を提供しますが、開発者が高性能なコードを書くうえで足かせになる場合もあります。そのため Rust では、明示的に unsafe とラベル付けしたコードも書けます。この unsafe コードも、Rust が安全なコードに求めるすべての要件を満たす必要がありますが、コンパイラはそれらの要件を機械的に検査しなくなります。正しく実装する責任は開発者に委ねられます。しかし Verus を使えば、unsafe な Rust コードの安全性を数学的に証明でき、機械的に検査された安全性保証を取り戻せます。 同様に Rust は「恐れ知らずの並行性 (fearless concurrency)」で知られています。これは、開発者が並行コード、つまり少なくとも一部が並列に実行されるプログラムを書くときに、他のプログラミング言語では許容されてしまうさまざまな誤りを型システムが防ぐという意味です。Verus はこの基盤の上に構築されており、開発者は並行コードが安全であるだけでなく正しいことまで証明できます。 例えば、並行実行には一般に ロック が用いられます。ロックは、プロセッサスレッドが現在操作しているデータ項目への排他的アクセスを与えるものです。Verus では、開発者がロックに 不変条件 (invariant) を付与できます。つまり、ロックを取得した側はその不変条件を満たす値を得られ (例えば、その値は常に偶数である)、ロックを解放するときには、ロックで保護されている値がその不変条件を依然として満たしていることを証明しなければなりません。さらに Verus は、ロックの実装そのものが正しいことの証明もサポートします。これは、高いパフォーマンスを実現するために複雑なカスタムロック方式に依存する Nitro Isolation Engine のようなプログラムでは特に重要です。 すべてのプログラム検証ツールと同様に、Verus の保証は次の要素が正しいことに依存します。Verus 自体、プログラムの意図された振る舞いを記述した「最上位」の仕様、基盤となるランタイム (Rust 標準ライブラリなど) に関する「最下位」の仮定、そしてソースコードを実行可能なプログラムへ変換するコンパイラのツールチェーンです。今後の記事では、これらのコンポーネントの正しさに対する確信をどのように高めているかを詳しく説明します。 オープンソースエコシステムにおける Verus Verus は Amazon での利用に加えて、さまざまなオープンソースプロジェクトで興味深い性質を証明するために使われています。以下にいくつかの例を挙げます。 Vest は、バイナリデータ形式の記述を受け取り、その形式のデータを解析およびシリアル化する Rust コードを自動生成します。生成物には、正しさとセキュリティに関する Verus の証明も含まれます。 Verdict は、X.509 公開鍵暗号標準に対応した、正しさと安全性が証明された証明書検証ライブラリを提供します。ユーザーが指定した検証ポリシーもサポートします。 CapybaraKV プロジェクト は、 永続メモリログ (persistent-memory log) の正しさとクラッシュ安全性を検証します。永続メモリログは、システムがクラッシュしたり予期せず電源を失ったりしても、データを整合性のある状態で保持します。 Atmosphere マイクロカーネル は、Rust で開発され、Verus によって正しさが検証されたマイクロカーネル (最小構成のオペレーティングシステム) です。 Anvil は、クラウドコンピューティングを管理するオープンソースシステムである Kubernetes のコントローラーについて、正しさと「活性 (liveness)」を証明します。妥当な仮定の下で、コントローラーが最終的にシステムを安定した状態へ導くことを示します。 CortenMM メモリ管理システムは、スケーラブルなロックプロトコルを備えた新しいトランザクショナルインターフェイスを提供しており、その並行コードの正しさは Verus で検証されています。 Verus 自体は、各地の学術界と産業界の研究者が協力して開発を進めている、無償のオープンソースプロジェクトです。 著者について Bryan Parno Bryan Parno は Amazon Scholar であり、カーネギーメロン大学の電気・コンピュータ工学およびコンピュータサイエンスの Kavčić-Moura Professor として、Secure Foundations Lab を率いています。研究では、安全なシステムの設計手法と構築手法における長期的かつ根本的な改善に取り組み、特に形式検証されたソフトウェアに重点を置いています。暗号学的に検証可能な計算に関する研究は、IEEE Symposium on Security and Privacy で Best Paper Award と Test-of-Time Award を受賞し、検証済みシステムに関する研究では 6 件の Distinguished Paper Award を獲得しています。ACM および IEEE のシニアメンバーであり、2011 年には Forbes の「30-under-30」科学分野リストに選出され、2010 年には ACM Doctoral Dissertation Award を受賞しました。カーネギーメロン大学で博士号を取得しています。 本ブログは Security Solutions Architect の 中島 章博 が翻訳しました。

この記事は Kiro ブログの Tackling technical debt at scale with autonomous mode in Kiro Web を翻訳したものです。 ソフトウェア開発チームはどこも、保守と新機能開発のあいだの緊張関係を経験しています。一方に使った時間は、もう一方に使えなかった時間です。オープンソースのメンテナーにとってこの課題はさらに深刻で、チームは小さく、ユーザーベースは大きく、バックログは伸び続けます。 形式検証 、つまりソフトウェアの性質を証明するために数学的技法を使う領域では、ドメインの複雑さゆえにこの痛みが特に大きくなります。 AWS Automated Reasoning Group は、 Kani Rust Verifier や C Bounded Model Checker (CBMC) を含む複数のオープンソース形式検証ツールを保守、あるいは主要なコントリビューターとして開発しています。本記事で紹介する取り組みを始めた 2025 年 11 月時点で、これらのリポジトリには 916 件のオープン issue があり、コアとなる検証機能の開発を進めながらでは、チームが対応できる速度よりも速く保守タスクが積み上がっていました。 技術的負債への従来のアプローチは、開発者の時間を保守に割り当てて機能提供を遅らせるか、負債が複利で膨らむのを放置するかの二択を強います。対話型の AI コーディングアシスタントは個々のタスクを速くしてくれますが、それでもすべてのステップで開発者がループの中にいる必要があります。私たちが欲しかったのは第三の選択肢、つまり issue を読むところからプルリクエストを開くところまで保守タスクを一気通貫で引き受け、エンジニアは判断が最も価値を持つコードレビューでだけ関わる、という形です。それが Web の Kiro の autonomy モード です。保守を含む幅広いタスクをこなせるエージェンティックなソフトウェアエンジニアリングツールで、エンジニアはより価値の高い仕事に集中できます。実際にどうなったかというと、2 か月のあいだに Kiro は私たちのリポジトリ群で 87 件のオープン issue に対応するプルリクエストを提出しました。これは、それまでの 22 か月（約 2 年）でチームが対応してきた量に迫る数です。 本記事では、どのようにセットアップしたか、2 つのケーススタディの詳細、そして自分のリポジトリで Kiro を自律的に使う方法を紹介します。 Kiro の自律モードの仕組み 自律モードの Kiro は、既存のワークフローと統合しながら、専用のセキュアなクラウド開発環境の中で自律的に動作します。Kiro に作業を割り当てるのは簡単です。 app.kiro.dev でタスクを記述する、GitHub issue に kiro ラベルを付ける、あるいはコメントで /kiro とメンションする、のいずれかです。すると Kiro はリポジトリを隔離されたサンドボックスにクローンし、issue と関連コードを分析し、作業をステップに分解し、変更を実装し、テストスイート全体を実行して、プルリクエストを開きます。すべてのプルリクエストは、CI の通過とコードオーナーのレビューを含め、人間が書いたコードとまったく同じ承認要件の対象になります。Kiro はマージ権限を持たず、ブランチ保護ルールを回避することもできません。 このアプローチに最も向いているのは、受け入れ基準が明確でスコープが独立しているタスクです。依存関係の更新、再現手順がはっきりしたバグ修正、ドキュメントの改善は、いずれも良い出発点です。アーキテクチャ上の決定や横断的なリファクタリングを要するタスクは、人間に任せたほうがよいでしょう。Kiro は曖昧さに遭遇したとき、推測ではなく確認の質問を返します。Kani と CBMC のリポジトリでの運用では、マージされた Kiro 生成コードが持ち込んだリグレッションはゼロでした。 定量的なインパクト Kani リポジトリでは 2025 年 11 月初旬に Kiro の自律モードを使い始め、同月後半に CBMC へ広げました。両リポジトリを通じて、数字がその効果を示しています。 コード保守（29%） : 依存関係の更新、ツールチェーンのアップグレード、CI の改善、リファクタリング ドキュメント改善（4%） : プロジェクトドキュメントとビルド手順の更新 バグ修正（36%） : クラッシュ、誤った結果、不変条件違反などの報告済み issue の解決 機能の完成（26%） : プロトタイプ機能で文書化されていたギャップへの対応 次のグラフは CBMC リポジトリの月次プルリクエスト活動です。2025 年の大半は、このリポジトリで解決された issue は月あたり 2 件未満でした。それが 11 月には 60 件に跳ね上がりました。これらのプルリクエストの多くはまだレビューを通過中で、11 月に CBMC へ提出された 64 本の Kiro のプルリクエストのうち、2026 年 9 月時点で 16 本がマージ済み、47 本がオープンのまま、1 本は別の変更で元の issue が解決されたためクローズされています。いずれも文書化されたオープン issue に対応するものです。CBMC と Kani を合わせると、2025 年 11 月と 12 月に Kiro は 87 件のユニークな issue に対応するプルリクエストを提出しました。それ以前の 22 か月（2024 年 1 月から 2025 年 10 月）に、チームが両リポジトリで対応した issue は合計 94 件でした。 図 1: 2024 年 1 月から 2025 年 12 月までの CBMC リポジトリの月次プルリクエスト活動。2025 年の大半は月あたり 2 件未満の issue しか解決されていませんでした。Kiro を導入した 2025 年 11 月には、65 本のプルリクエストで 60 件の issue に対応するまで跳ね上がりました。 2025 年 11 月と 12 月に CBMC と Kani へ提出された 94 本のプルリクエストのうち、2026 年 9 月時点で 35 本（37%）がマージ済み、56 本（60%）がオープンでレビュー中、3 本（3%）は別の変更で元の issue が解決されたためクローズされています。マージされたもののうち、提出されたそのままマージされたものもあれば、対話的な仕上げを要したものもあります。レビューのバックログは重要なボトルネックを示しています。Kiro はチームがレビューできる速度より速くプルリクエストを生成できるのです。これらは実質的な変更でした。中央値のプルリクエストは 5 ファイル・約 110 行に触れており、最大のものは約 1,000 ファイルに及びました。1 タスクあたり集中した開発作業 2〜3 時間として、94 本のプルリクエストはおよそ 200〜280 時間の実装工数に相当します。これはレビュー時間と、最終的にマージされないかもしれないプルリクエストを除いた数字であり、また多くのタスクが機械的な更新ではなくバグ修正や機能の完成であることを踏まえると、下限として見るのが妥当です。 スループットの変化も同じくらい際立っています。Kiro 導入前の 22 か月、CBMC で解決された issue は月あたり 2 件未満でしたが、2025 年 11 月には 60 件、30 倍を超える増加でした。11 月に開かれた 65 本のプルリクエストのほぼすべて（64 本）が Kiro によるもので、このスパイクが開発者の工数の振り替えではなくエージェントによる追加キャパシティを反映していることが分かります。全体として Kiro は、チームの歴史的な issue 解決スループットのおよそ 10 倍の速度で実装作業を生み出しました。ただし実際に得られる価値は、レビューと仕上げのキャパシティに左右されます。マージされたプルリクエストは引き続きリグレッションをゼロに保っており、その裏づけとなる母数はいまやはるかに大きくなっています。運用全体（2025 年 11 月から 2026 年 9 月）で、183 本の Kiro 生成プルリクエストが 2 つのリポジトリにマージされました。初期コホートで今もオープンな 56 本は、品質上の懸念ではなく先述のレビューのボトルネックを反映したものであり、リグレッションゼロという記録はそれらがレビューを通過するにつれて改めて検証されていきます。 ケーススタディ: サブモジュール更新の自動化 Kani プロジェクトは、別系統の検証ワークフロー向けに Rust プログラムの中間表現を得るため、 charon の Git サブモジュールを保守しています。 Dependabot で自動更新している他のサブモジュールと違い、charon の更新には統合テストが必要です。翻訳レイヤーの変更が、Kani が Rust のセマンティクスを正しくモデル化できるかに影響しうるからです。手作業での更新はふつう 2〜3 時間かかり、サブモジュールの更新、コンパイルとビルド失敗の調査、上流の変更の分析、リグレッションテスト、テスト失敗の調査までを含みます。この作業に開発者の時間を繰り返し費やすのではなく、私たちはこのプロセスを Kiro に引き渡し、自律的に処理させています。 図 2: Kani の charon Git サブモジュールを更新するために Kiro の自律エージェントへ与えたタスクプロンプト。小さく、説明が明確なコミットで段階的に更新するよう指示しています。 Kani の issue #2236 は 2 年以上バックログに残っていました。 Kani は Rust 向けのオープンソース形式検証ツールで、 Firecracker や s2n-quic といった重要な AWS プロジェクトの CI で使われ、 CBMC に依存しています。ファザーが Kani コンパイラのクラッシュを明確な再現手順つきで報告していましたが、根本原因を突き止めるには大きなコンテキストスイッチが必要でした。これは放置ではなく意図的なトリアージです。ユーザーをブロックする issue や健全性を脅かす issue はすぐに修正されますが、影響を受けるユーザーがいないファザー発見のクラッシュは、優先順位づけの勝負に毎回負けます。ユーザーをブロックするバグと同じだけ高価なコンテキストスイッチを要求しながら、見返りが同じではないからです。 kiro ラベルを付けたあと、Kiro は 2 時間 22 分で修正とリグレッションテストを含む PR #4461 を提出しました。人間が費やした時間は 5 分未満です。issue が古かったため、私たちは Kiro にまずバグがまだ存在するかを確認し、すでに解決されているなら再現ケースをリグレッションテストとして追加するよう依頼しました。Kiro は計画を適応させ、そのままマージできるプルリクエストを出してきました。 Kiro はさらに PR #4445 と #4464 も作り、Kani の charon Git サブモジュールを段階的に更新しました。小さく、説明が明確なコミットにするという指示だけを与えたところ、Kiro は利用可能な更新を分析し、更新の順序を決め、コミットを生成してプルリクエストを開きました。開発者は変更をレビューし、特定のコメントには /kiro fix 、すべてのコメントには /kiro all で作業を依頼できます。段階的なコミットと明確な説明のおかげで、レビュアーは機械的な更新作業ではなく意味的な正しさに集中できます。 図 3: レビュアーがプルリクエストのコメントで /kiro fix を使い、特定のレビューフィードバックへの対応を Kiro の自律エージェントに指示しています。 ケーススタディ: Kani の内部コンパイラエラーの修正 前のセクションでは Kani issue #2236 の見出しだけを紹介しました。2 年間眠っていたものが、人間の作業 5 分未満で解決した、という話です。ここでは、その人間とエージェントの協働が実際にどう進んだのかを見ていきます。 必要だったのは issue に kiro ラベルを付けることだけでした。エージェントは作業に取りかかり、issue を分析して計画を返しました。 図 4: Kani issue #2236 の調査に向けて Kiro の自律エージェントが提案した計画。リポジトリのセットアップ、バグの再現、修正の作成という手順が並んでいます。 この issue はかなり古かったので、何らかの変更で偶然すでに修正されていた可能性も十分にありました。私たちは Kiro の計画に対して、次のガイダンスを返しました。 After having set up the repository and development environment please first make sure that the bug even still exists. Please do so by creating a regression test from the code sample provided in this issue. If the bug no longer reproduces then just create a pull request that introduces this new test (and have that pull request resolve this issue). Other than that, your plan sounds good, please go ahead. Kiro は更新したタスク計画を返し、そのうえで Kani PR #4461 としてマージしたプルリクエストを作りました。チームの誰にもコンテキストスイッチは発生していません。 うまくいかなかったこと Kiro が生成したプルリクエストの失敗パターン Kiro がどこで失敗したかを理解することは、成功と同じくらい重要でした。それが作業の割り当て方とレビューの期待値を形づくったからです。 CI を通ってしまう誤った修正。 CBMC の PR #8892 では、リグレッションテストが memcpy を呼びながら --no-library を使っていたため、問題のコードパスが一度も実行されていませんでした。修正があってもなくてもテストは通ってしまいます。私たちはこれを、対象の関数を直接実行するユニットテストに置き換えました。 教訓: CI が通ることは必要条件だが十分条件ではない。レビュアーは、テストが修正を本当に検証しているかを確かめる必要がある。 アーキテクチャ的に誤った修正。 根本原因ではなく症状に対処してしまった修正もありました。PR #8703 では 172 行の再構成がネストした量化子を壊しており、正しい修正は元の場所の 9 行でした。こうしたケースにはアーキテクチャの知識を持つレビュアーが必要です。また Kiro は、既存のユーティリティを使わずに機能を作り直してしまうこともありました。 プラットフォーム固有の失敗。 Kiro は Linux 上で開発するため、プラットフォーム依存の問題がすり抜けることがあります。PR #8894 は空の構造体（ struct S {} ）を使っており、これは GCC 拡張としては有効ですが MSVC モードでは拒否されます。修正は gcc 限定のタグを追加することでした。該当するプラットフォームガードを示す既存のテストがあったにもかかわらずです。 フォーマット違反と古くなったプルリクエスト。 ほぼすべてのプルリクエストに軽微なフォーマットの問題がありました。レビューされないままのプルリクエストはコンフリクトも溜めていきます。PR #7861 は develop から 1,614 コミット遅れており、簡単ではないリベースが必要でした。コストを複利で膨らませないために、素早いレビューが欠かせません。 対話的な仕上げでループを閉じる ここまでに挙げた限界は現実のものですが、話はそこで終わりません。そのすべてが、開発者がエディタや IDE を開くことなく解決されました。 Kiro CLI を使い、メンテナーはプルリクエストのブランチで kiro-cli chat セッションを開始し、会話を通じて修正を導きます。メンテナーが判断を与え、エージェントが実行を担います。この 2 フェーズのワークフロー（自律的な生成、その後の対話的な仕上げ）は両モードの強みを組み合わせ、合計の時間コストを、開発者が各タスクを一気通貫でこなす場合よりも十分に低く保ちます。 図 5: 2 フェーズのワークフロー。Kiro の自律エージェントは、ラベルの付いた GitHub issue をサンドボックス内で分析・実装・テストまで進め、プルリクエストを開きます。メンテナーのレビューで変更が必要になったときは、対話的な Kiro CLI セッションが調査・修正・コミットを繰り返し、プルリクエストがマージできる状態になるまで仕上げます。 2 フェーズが機能する理由。 自律エージェントはコールドスタートの問題をなくします。レビューの時点で、動くコード、通っているテスト、アプローチの明確な説明がそろっているのです。対話型の CLI は非同期のやり取りの待ち時間をなくし、数時間ではなく数分で問題を解決します。どちらのフェーズも、メンテナーが自分でコードを書くことを求めません。 定性的なインパクト。 AWS Automated Reasoning Group の Senior Manager of Applied Science、Rahul Kumar は次のように述べています。「Kiro は私たちの技術的負債への向き合い方を根本的に変えました。以前は、サブモジュールの更新は機能開発からのコンテキストスイッチを要するため、何週間もバックログに居座っていました。いまは issue に kiro とラベルを付ければ、更新・テスト・ドキュメントまでワークフロー全体を処理してくれます。11 月だけで、Kiro が生成した 15 本のプルリクエストをリグレッションゼロで Kani にマージしました。」 日常的な保守を引き受けることで、Kiro は開発者を、アーキテクチャ上の決定、複雑なアルゴリズム設計、コミュニティとの関わり、そして形式検証の研究に集中させてくれます。 自分のリポジトリで Kiro Web を使う方法 自分のオープンソースプロジェクトで試してみたい方は、 こちらの手順 に従ってください。 複雑なタスクや対話的な仕上げには、上の「対話的な仕上げでループを閉じる」で説明したとおり、プルリクエストのブランチで Kiro CLI を使い、会話を通じて作業を導いてください。 参加する Kiro Web は、 app.kiro.dev にて有料の Kiro ユーザー全員に一般提供されています。すでに Kiro をご利用中の方は、 app.kiro.dev/agent にサインインして上記の手順に進んでください。 2026 年 9 月時点で、Kiro は公開されている CBMC と Kani のリポジトリに 400 本を超えるプルリクエストを提出し、そのうち 183 本がマージされ、約 150 件のユニークな issue に対応しました。430 件以上の issue をフラグ付けしたプライベートのステージングリポジトリでは、さらに 360 本を超えるプルリクエストを生成し、レビューと段階的な上流への取り込みが進んでいます。定義の明確な issue のバックログを持つリポジトリを保守しているなら、このアプローチは数分で始められます。