いやもうほんとにここに書いた通りだけの事なんですけど、AIにコードから読み取れる仕様をGherkinという仕様を自然言語で書く言語でまとめさせて、書いた仕様を、実装からTLA+で書き起こしたモデルが満たすかどうかモデル検査したら、満たさないケースを、どういう経路の場合満たさないかのトレース付きで出してくれるんですよ〜。Fable並にバグを出してくれますよ。gpt5.5を使ってるのに。