Kiro が自身のハーネスの性質を Lean で証明する

ツイート

私たちのチームは Kiro のコンテキスト管理を担当しています。モデルを取り巻くハーネスは、何をどれだけコンテキストウィンドウに入れるかを決め、長い会話を圧縮し、プロンプトキャッシュが効くように各リクエストの先頭を安定させ、セッションを復元できるように保存します。その周りには、ツール呼び出しとその承認、ストリーミングの応答、サブエージェント、バックグラウンドタスクといった、ハーネスのほかの基本機能があります。このコードのバグはテストで見つけにくいものです。バグが出るかどうかは、モデルが選ぶ入力、並行するイベントの…