Alloyを共通言語にして、CodexとClaudeに実装と監査をさせてみた

AIと形式手法を使って、Glyphaという小さなデジタルサイネージを作りました。

今回試したかったのは、単に「AIにコードを書かせる」ことではありません。

私は普段から、システム設計や既存コードの解析にAlloyを使っています。

そこで今回は、普段自分がやっている

「システムが守るべき性質をモデルにする」

という作業から、設計・実装・テストまでAIにやらせてみました。

CodexにAlloyから書かせる

最初に用意したのは、システムのコンセプトを書いたMarkdownだけです。

例えば、

- ServerとRendererだけで構成する
- 時計が戻っても過去のコンテンツを再生しない
- invalid contentはcurrent contentを置換しない
- Rendererの失敗はlast successful sceneを壊さない

といった、機能ではなく意味や不変条件を記述しました。

これをCodexに渡し、検討が必要な部分をAlloyでモデル化してもらいました。

作られたモデルは大きく次の4つです。

- Validation and publication
- Time and finite batches
- Rendering and failure
- Generations, restarts, and assets

Alloy Analyzerで反例を確認しながら振る舞いを決め、その後もCodexに設計・実装・テストまで任せました。

Alloyは本当に実装に使われたのか？

完成したコードは小さいのですが、妙に緻密でした。

そこで疑問が出ました。

Codexが作ったAlloyモデルは、本当に実装やテストに反映されているのか？

自分で全モデルとテストを照合する代わりに、今度は別のAIであるClaudeにリポジトリだけを渡し、

Alloyのassertとテストコードがどのように対応しているか調査してほしい

と依頼しました。

Codexとの会話内容はClaudeには渡していません。

assertをそのままテストにしていたわけではなかった

Claudeの調査で面白いことが分かりました。

CodexはAlloyのassertを、そのまま同じ形のテストへ翻訳していたわけではありませんでした。

例えばAlloyに、

コンテンツ更新時に、新旧のデータが混ざった状態が見えてはいけない

という性質があるとします。

実装ではこれを、

「新旧の世代が混ざってはいけない」
             ↓
更新途中で意図的にクラッシュさせる
             ↓
再起動する
             ↓
旧世代または新世代の完全な状態であり、
混成状態になっていないことを確認する

というテストに変換していました。

他にも、

「時間を飛び越えても最新状態へ追いつける」
    ↓
実装とは別の方法で期待値を計算
    ↓
1000回の試行で照合

や、

「更新中でも配信中の旧コンテンツを壊してはいけない」
    ↓
HTTPレスポンスを送信途中で止める
    ↓
その間に新コンテンツへ置換
    ↓
旧レスポンスを再開しても
旧世代の画像を取得できることを確認

といったテストになっていました。

つまり、

Alloyのassert → テストコード

という単純な変換ではなく、

守るべき性質 → それを壊しそうな状況 → 観測方法 → テスト

という変換が行われていました。

Claudeの監査結果をCodexへ戻す

Claudeはいくつか対応の弱い箇所も発見しました。

そこで、その監査結果をCodexへ戻しました。

CodexはClaudeの報告を再度リポジトリと照合し、記述のずれを修正しながら、証跡の弱い部分には追加テストを作成しました。

さらにその結果をClaudeへ戻して再監査しました。

最終的には、

Human Intent
     ↓
Concept
     ↓
Codex
     ↓
Alloy
     ↓
Analyzer / Counterexample
     ↓
Design / Code / Tests
     ↓
Claude Audit
     ↓
Codex Re-check
     ↓
Claude Re-audit

という流れになりました。

プロンプトより不変条件を考える

今回、人間である私が主に考えていたのは、実装方法でも詳細なプロンプトでもありませんでした。

考えていたのは、

• 何を作るのか
• 何を作らないのか
• 何が常に真であるべきなのか

ということです。

まだGlyphaという小さなシステムで一度試しただけなので、この方法が一般化できるとは考えていません。

ただ、

人間が意図と不変条件を決め、形式モデルを共通の基準として、複数のAIに生成と監査を分担させる

という開発方法は、もう少し実験してみる価値がありそうです。

Glyphaのコード、Alloyモデル、テスト、開発方法の記録はGitHubで公開しています。

詳しい経緯やClaudeによる監査については、Zenn版の記事にまとめています。