タグ: Z3

"Z3" が付いた記事と Wiki ページ

• 形式手法を Claude Code で回す — Z3 と TLA+ で仕様の穴を見つけ、反例をテストに落とす

  2026年10月9日

  Claude Code に料金計算の仕様を Z3 で、キャッシュ設計を TLA+ で形式化させ、仕様の矛盾と並行実行の競合を見つけた。形式手法とテストの違い、道具の選び方、反例を pytest に落とす手順、検査の空振りの確かめ方を実行結果つきで解説する。