Visual Studio 2022+C# の組み合わせだと、nullチェック忘れとかは指摘してくれるけど、それが出来るのであれば型変換してるコードでの値の範囲チェックのコードが書かれてないのも同様に検出できそうな気がするけど、オプションとしてそれを追加するの無理なんだろうか？＞＜；
そういう風に検査を追加していったら、SPARKほどの完璧さは無理でもわりと近い安全性が実現出来そうな気がするんだけど＞＜