2026-08-20 版 / Claude Code v2.1 系で設計(他のエージェントでも成立)
現在、この研修の募集は行っていません。準備中のカリキュラムと第 0 回(無料公開)のみ掲載しています。開講時の案内をご希望の方は
下記までご連絡ください。
AI は「できたように見えたら」止まる。
検証手段を渡さなければ、人間が検証ループになる。
コーディングエージェントの「テストが通りました ✅」は、主張であって証拠ではありません。
この研修は、AI の報告を人が読んで確かめる運用から、AI にも人にも同じ検査を機械的に通させる運用へ切り替える型を、
研究室で実際に踏んだ事故と実測をもとに、手を動かして身につけます。定理証明器は使いません。
受講者が普段お使いのエージェント(Claude Code / Copilot / Cursor など)でそのまま持ち帰れます。
第 0 回を無料で読む
開講時の案内を希望する
こんな課題をお持ちの組織へ
- エージェントが「完了しました」と言ったものが、後で動いていなかったことがある
- AI が書いたテストが通るのは当然(AI が実装に合わせて書いているから)で、何を保証しているのか分からない
- 権限の確認ダイアログを押し続けるのに疲れて、「全部許可」に倒れている
- AI 導入の社内ルールを作りたいが、「気をつけて使う」以上の具体が書けない
受講後にできること
1. 主張ではなく証拠を出させる判定条件・再現手順・成果物を渡して、合否をエージェント自身に閉じさせる指示が書ける。「通った」の根拠を終了コードと成果物で確かめる
2. 検査を機械的に組み込むプロンプト → 目標 → フック → 第三者レビューの 4 段階を使い分け、fail-closed のゲート(秘密検出・ビルド・テスト)をエージェントのフックに置ける
3. 検査の検出力を測る変異注入で「わざと壊したら落ちるか」を確かめ、検出力のないテストを見抜く。走らなかった検査を「異常なし」と区別して可視化する
この研修の特徴
- 事故から作った教材。 2026-08-08、研究室で 47GB を使って OOM kill された型検査を、エージェントが 4 回続けて「通った」と報告しました。成功しても殺されても最後の 1 行が同じだったからです。この手の「見た目では区別がつかない失敗」を一覧にし、それぞれの塞ぎ方を配ります
- 道具に依存しない。 原理(証拠を出させる・fail-closed・検査の検査)はどのエージェントでも同じ。演習は受講者の環境で行い、Claude Code 固有の機能(フック・サブエージェント)はデモで示します
- インストール不要で始められる。 第 0〜3 回はシェルと普段の開発環境だけで演習できます
- 発展研修への入口。 仕様の書き方・定理証明器による検証(Lean/Rocq 研修)へそのまま接続します
カリキュラム(全 8 回・各 90 分/1 日集中版は第 0〜4 回)
| 回 | 題 | 持ち帰るもの |
| 第 0 回無料公開 | なぜ「通った」を信じてはいけないか | エージェントの停止条件。見た目では区別できない 3 つの失敗(パイプで消える終了コード・検出力のないテスト・沈黙する検査器)を手元で再現する |
| 第 1 回 | 判定条件を渡す — 強い指示の書き方 | 「書いて」ではなく「この入力でこう・実装後にテストを走らせて」。再現テストを先に書かせる。証拠(コマンド・戻り値・出力)を要求する定型文 |
| 第 2 回 | 検証を縛る 4 段階 | プロンプト内 → セッション目標 → Stop フック → 第三者レビュー。どの強さをいつ使うか。フックの無限ループ防止の上限 |
| 第 3 回 | 検査の検査 — 変異注入 | わざと壊して落ちるかを測る。検出率と誤検出を対で見る。「走っていない検査」を可視化する運用(⚠ 検査していません) |
| 第 4 回 | 権限と安全 — 人が毎回判断しない | 権限モードの使い分け。止めたいものを機械的な規則(deny)で書き、それ以外は自律させる。会話での「しないで」は消える |
| 第 5 回 | フックで fail-closed にする | コミット前の秘密検出、保存時の静的検査、ターン終了時のビルド/テスト。研究室で運用中のフック群を題材に設計する |
| 第 6 回 | 探索→計画→実装→コミット | 調査と実装を分ける。計画を飛ばしてよい条件。チェックポイントで戻せるもの・戻せないもの。worktree で並列に試す |
| 第 7 回 | 敵対的レビューと定着 | 書いた本人に採点させない。レビュー役の過剰指摘の扱い。チームの CLAUDE.md/ルールに落として運用に定着させる |
第 1 回以降の教材・演習(フックのテンプレート、変異注入スクリプト、チェックリスト)は開講時に受講組織へ提供する予定です。
実施要領(予定)
| 対象 | AI コーディング支援を業務で使っている(使い始める)ソフトウェアエンジニア/テックリード/QA/開発マネージャ。プログラミング経験は必須、特定ツールの経験は不要 |
| 人数 | 演習つきのため 1 回あたり 15 名程度まで(講義のみの概要版は人数制限なし) |
| 形式 | オンサイト/オンライン。全 8 回(各 90 分)、1 日集中(第 0〜4 回)、90 分の概要講演のいずれか |
| 環境 | 受講者の普段の開発環境とエージェント。第 5 回以降はフックが設定できるエージェント(Claude Code 等)を推奨 |
| 費用 | 未定(開講時に回数・人数・題材のカスタマイズ量により個別にお見積りします) |
| 講師 | 横山哲郎(南山大学 理工学部 教授)。プログラミング言語・プログラム変換・可逆計算。研究室の研究開発を AI エージェントで回し、その運用規則と事故記録を公開している |
よくある質問
- Q. Claude Code を使っていないのですが受講できますか?
- A. できます。証拠を出させる指示・検査の検査・fail-closed の設計は道具に依存しません。フック相当の機能がないエージェントでは、CI 側に同じゲートを置く形で扱います。
- Q. 「Lean/Rocq で AI 生成コードを検証する」との違いは?
- A. 本研修は定理証明器を使わず、テスト・ビルド・静的検査という既にある検査を「AI が誤魔化せない形」で運用する研修です。Lean/Rocq 研修はその先で、検査そのものを証明に置き換えます。順に受けるのが自然です。
- Q. 社内ルールの文書化まで支援してもらえますか?
- A. 第 7 回で、貴社の運用に合わせたルール(CLAUDE.md/チームの規約)の草案まで作ります。
現在は募集していません。開講が決まった際の案内をご希望の方は、tyokoyama [at] acm.org(横山)まで、件名に「AI コーディング運用研修」と書いてメールをお送りください。
内容へのご意見・題材のご提案も歓迎します。
第 0 回を無料で読む →