Rustの形式検証ツールcargo kaniでは検出できない認証バイパス等の不備を、機械的に検証するための設計を解説。プログラムが検証器の保証対象外となる失敗モード（空虚、不十分、偽陽性）を整理し、再現性の高いテストを実現するためのアプローチを検討する。