1. 【最重要】Kiro、Lean形式検証をハーネスに適用 — 18件の実コード上の反例を発見
原文発表：11月2日／AWS日本語版：11月3日。 Kiroのハーネスは、会話コンテキスト、長い会話の圧縮、プロンプトキャッシュのプレフィックス、セッション復元、ツール呼び出しの承認を管理します。こうした状態依存の処理は通常の単体テストでは抜けやすく、Leanによる性質検証を試しました。
なぜ重要か
モデルの推論能力とは独立した実装バグが、エージェントの振る舞いを静かに変える可能性があります。コードと仕様の両方を検証することが重要です。
技術・API・評価
| 項目 | 確認結果 |
|---|---|
| 対象 | TypeScript・Rust・Pythonのハーネス関連26関数 |
| 性質・観察 | 96件 |
| Leanで証明 | 70件 |
| 有界検査 | 2件 |
| 反証とコード再現 | 18件 |
| 部分的結果・観察 | 6件 |
| 公開API | 一般提供の検証APIは未発表 |
| 料金 | 検証システムの提供価格は未発表 |
評価上の限界： 18件の反例はコードでも再現されましたが、すべてが実害のある脆弱性を意味するわけではありません。証明した性質も、モデル化した仕様に対するもので、実装全体の無欠陥を保証しません。
要点： Kiroは11月2日、エージェントのハーネス実装をLeanでモデル化し、実コードと照合する自動検証の成果を発表した。 26関数のモデルで96件の性質・観察を調べ、70件を証明、2件を有界検査、18件を反証してコードでも再現した。 11月3日のAWS日本語記事は原文の翻訳であり、別イベントとして数えない。
一次情報： AWS Japan / Kiro公式記事