2026年8月23日 テストカバレッジ94%でも見逃した整数オーバーフローを、symbolic executionが発見した ユニットテストは特定の入力をチェックする。symbolic executionはあらゆる可能な入力をチェックする。仕組み、コスト、始め方を解説する。 additional-strategiessymbolic-executiontestingverification
2026年8月3日 コードにランタイムエラーがないことを証明する方法（そして、なぜ諦めるかもしれない理由） 抽象解釈を使えば、実行前にランタイムエラーが発生しないことを証明できる。実際の仕組み、難しさ、そしてツールチェーンでの位置づけを解説する。 abstract-interpretationstatic-analysisruntime-errorsverification
2026年7月25日 本当に1万行を零欠陥で検証した人がいるのか？IBMはやったし、その方法論は結果より奇妙だ。 Cleanroom software engineeringは、デバッグではなくmathematical verificationによって零欠陥のインクリメントを約束した。我々はIBMの実プロジェクトデータを見て、その主張が成り立ったかを確認する。 cleanroom-correctnesszero-defectsverificationcase-study
2026年7月9日 AutoVerusは40時間の証明執筆を3回のLLM呼び出しに変える。秘訣は諦めるタイミングを知ることだ。 AutoVerusはLLMエージェントのネットワークを用いてRustコードのVerus正しさ証明を生成し、SMTソルバーのフィードバックによって駆動される生成・修復・ dischargeループにより、90%以上の証明義務を自動化する。 model-checkingautoverusrustverification
2026年7月6日 時相論理を学ばずにコードのモデル検査ができる Kaniのような境界付きモデル検査器やAlloyのような関係モデルファインダーは、通常のアサーションと制約で性質を検証できる。活性の証明を諦める代わりに、学習曲線は週ではなく時間単位で測られる。 model-checkingtemporal-logicformal-methodsverification
2026年7月5日 一行の証明も書かずに Rust コードの正しさを証明できるが、状態空間が代償となる Kani のようなモデル検査ツールを使えば、形式的証明の代わりに表明で Rust の性質を検証できる。問題は、ループの境界が小さくないときに何が起きるかだ。 model-checkingrustverificationformal-methods
2026年6月14日 テストでは2つの関数が等価であることは証明できない。では何ができるのか。 N-version programmingは実装が一致することを前提とする。テストがなぜ不十分なのか、SMT solverがいかにして等価性を実際に証明できるのか、そして「十分に良い」と「形式的に検証済み」の境界線をどこに引くべきかを見ていく。 n-version-programmingequivalence-testingformal-methodsverification
