【第 2 回】AI のハルシネーションとの戦い — 29機能すべてが SUCCESSFUL で、認証バイパスが通った

形式検証でセキュリティバグを見落とした。29個の機能がすべてテストを通ったのに、認証を丸ごとスキップできるバグが検証を素通りしていた。原因は、テストそのものが業務的に意味を持たない式で書かれていたこと。「ユーザーが許可されたか拒否されたか、どちらかのはず」という常に真になる式を書いて、業務ルール「許可されたときだけ進む」は何も縛っていなかった。

形式検証の恐ろしさは、ここにある。通ったテストほど、人間の安心を作る。テストが存在することそのものが「守られている」という錯覚を生み出す。この例では、被覆率が91%という数字が出ていた。それは参照カウントで、判別力ではない。assert が存在すること自体が数えられ、そのassert が実際に何も守っていないことは、ツールには見えない。ミューテーション——実装を壊して、テストが落ちるかを見る——をするまで、穴は見つからなかった。

穴は、もっとも守るべきところに集まっていた。算術（金額・税・在庫）は自動的に強い。result == f(inputs) の形で書けば、バグを自動検知する。一方、認証・認可・締切・決済可否は真偽値を返す判定述語で、事後条件を tight に書くのが難しい。だから企業システムでもっとも守るべき制御ロジックほど、形式検証に穴が出やすい。テストツールを入れたから安全だと思う前に、ミューテーション無しの検証は「見た目の成功」でしかないことを知っておく必要がある。

中小企業でも形式検証やテスト自動化を使うときは、「テストが通った」という報告ほど疑って見る。特にセキュリティや決済など、業務的な損害が大きい箇所は、実装を意図的に壊してテストが本当に落ちるかを試す手間が必ず必要になる。ツール依存は安心を売っているに過ぎず、人間の敵対的な検証なしに「守られている」と言うことはできない。