Amazon Web Services ブログ

Verus で正しさが数学的に証明できる Rust コードの開発

Rust の型システムは多くのバグを防ぎますが、コードが本当に正しいことまでは保証しません。そこで、Rust 向けのオープンソースの自動プログラム検証ツール Verus を紹介します。事前条件・事後条件による仕様記述の書き方、1 秒未満の高速なフィードバック、unsafe コードや並行コードの正しさの証明、そして Nitro Isolation Engine をはじめとする Amazon 社内やオープンソースでの活用事例まで説明します。

【開催報告】ファッション・アパレル業界向け 第一回ナレッジ共有会 〜 SMART から始まる業界共通課題への挑戦と学びの場

店舗業務支援 AI エージェント SMART を起点に、ファッション・アパレル業界 6 社 20 名が集まった第一回ナレッジ共有会の開催報告です。週報作成 15 分が 0 分に、IT 未経験の店舗出身メンバーが 2 週間で Web アプリ開発、ベテランの経験に依存していた在庫消化業務のエージェント化——SMART の合同ブートキャンプから活動を始めた 3 社が、実際に手を動かし、現場との対話を重ねて得た実践ナレッジを発表しました。作って終わりにしない AI エージェント開発のヒントが詰まった当日の模様をレポートします。

Kiro Web の自律モードで技術的負債に大規模に立ち向かう

技術的負債への従来のアプローチは、開発者の時間を保守に割り当てて機能提供を遅らせるか、負債が複利で膨らむのを放置するかの二択を強います。対話型の AI コーディングアシスタントは個々のタスクを速くしてくれますが、それでもすべてのステップで開発者がループの中にいる必要があります。私たちが欲しかったのは第三の選択肢、つまり issue を読むところからプルリクエストを開くところまで保守タスクを一気通貫で引き受け、エンジニアは判断が最も価値を持つコードレビューでだけ関わる、という形です。それが Web の Kiro の autonomy モードです。保守を含む幅広いタスクをこなせるエージェンティックなソフトウェアエンジニアリングツールで、エンジニアはより価値の高い仕事に集中できます。実際にどうなったかというと、2 か月のあいだに Kiro は私たちのリポジトリ群で 87 件のオープン issue に対応するプルリクエストを提出しました。これは、それまでの 22 か月（約 2 年）でチームが対応してきた量に迫る数です。本記事では、どのようにセットアップしたか、2 つのケーススタディの詳細、そして自分のリポジトリで Kiro を自律的に使う方法を紹介します

Kiro の GPT‑5.6 モデルが 100 万トークンのコンテキストウィンドウに対応

Kiro の IDE、CLI、Web のすべてで、GPT‑5.6 Sol、Terra、Luna が 100 万トークンのコンテキストウィンドウに対応します。これにより、コードベース全体、長文ドキュメント、長く続いたマルチターンのエージェント履歴を、チャンク分割や要約を挟まず、細部を失わないまま 1 回のリクエストで処理できるようになります。

AWS Weekly Roundup: Amazon Bedrock 上の OpenAI GPT-6 Astra、Amazon Quick デスクトップ GA、学生向け Kiro など (2026 年 9 月 14 日)

ニューヨークの 9 月中旬には、特別なエネルギーがあります。パンプキンスパイスラテがたっぷりとあり、気温も下が […]

自動推論による数学的確実性の 10 年: Automated Reasoning Group が歩んだ道

Automated Reasoning Group (ARG) の発足から 10 年の歩みを振り返ります。自動推論による形式的検証は研究プロトタイプから、Amazon Inspector、IAM Access Analyzer、Reachability Analyzer といったお客様向けサービスへと発展しました。Nitro Isolation Engine や暗号実装、認可エンジンの正しさを証明した内部の取り組み、Amazon Bedrock Guardrails の自動推論チェックによる生成 AI のハルシネーション防止、そして Amazon Bedrock AgentCore や Kiro でのエージェンティック AI への展開まで、システムを「おそらく正しい」だけでなく「正しいと証明できる」ものにする数学的確実性の価値を紹介します。

← Older posts