研究室で AI エージェントを使って研究開発を回す中で作った運用規則・検証手順・事故記録を、企業のソフトウェア開発向けに組み直した研修群です。 どれも「AI の出力を信用してよい条件を、自分で作れるエンジニア」を育てることを目的にしています。
| 段階 | 研修 | 対象・内容 |
|---|---|---|
| 1 基礎 | 「通った」を信じない AI コーディング運用 第 0 回: なぜ「通った」を信じてはいけないか | AI を使う全エンジニア向け。主張ではなく証拠を出させる指示、検証の 4 段階、変異注入、権限・フックの fail-closed 設計。定理証明器は使わない |
| 2 発展 | Lean/Rocq で AI 生成コードを検証する 第 0 回: なぜ AI 生成コードに「証明」が要るのか | 損害が出るロジックを持つチーム向け。仕様を命題で書き、AI に実装と証明を書かせ、検査器で嘘を弾く。Lean 4 主軸・Rocq 1 回 |
順に受けるのが自然ですが、発展だけの受講も可能です。いずれも受講組織の題材に合わせて組み替えられます。