The Stack Overflow Podcast
AIは「その通り」と言い、形式手法は「間違いだ」と言う
AI says you’re right, formal methods say you’re wrong
Stack Overflow Podcast で、Quint CEO の Gabriela Moreira が、TLA+ などの形式仕様言語がコードを書く前に設計上の欠陥を見つける仕組みを語った。TLA+ の上に開発者向け構文を載せた Quint の特徴、OpenHands の Kubernetes での競合状態の事例、AI 時代に仕様を誰が書き、誰が確認するのかという問題を扱う。モデルベーステストやトレース検証で、AI 生成コードを実運用のデータと突き合わせる方法も紹介された。