abstract-interpretationstatic-analysisruntime-errorsverification コードにランタイムエラーがないことを証明する方法(そして、なぜ諦めるかもしれない理由) 抽象解釈を使えば、実行前にランタイムエラーが発生しないことを証明できる。実際の仕組み、難しさ、そしてツールチェーンでの位置づけを解説する。 テストスイートは通過した。型チェッカーも緑色だ。リリースする。2時間後、本番環境で誰もテストしようとしなかったエッジケースで が発生する。… 2026年8月3日