2026年7月6日 時相論理を学ばずにコードのモデル検査ができる Kaniのような境界付きモデル検査器やAlloyのような関係モデルファインダーは、通常のアサーションと制約で性質を検証できる。活性の証明を諦める代わりに、学習曲線は週ではなく時間単位で測られる。 model-checkingtemporal-logicformal-methodsverification
2026年7月5日 一行の証明も書かずに Rust コードの正しさを証明できるが、状態空間が代償となる Kani のようなモデル検査ツールを使えば、形式的証明の代わりに表明で Rust の性質を検証できる。問題は、ループの境界が小さくないときに何が起きるかだ。 model-checkingrustverificationformal-methods
2026年6月15日 Differential Testingは形式的証明なしで機能するが、Common-Mode Failureが落とし穴だ Differential testingを使えば、正解を知らなくてもバグを見つけられる。問題は、相関した誤りが合意に見えることだ。盲点を見つける方法は以下の通り。 n-version-programmingdifferential-testingformal-methodstrust
2026年6月14日 テストでは2つの関数が等価であることは証明できない。では何ができるのか。 N-version programmingは実装が一致することを前提とする。テストがなぜ不十分なのか、SMT solverがいかにして等価性を実際に証明できるのか、そして「十分に良い」と「形式的に検証済み」の境界線をどこに引くべきかを見ていく。 n-version-programmingequivalence-testingformal-methodsverification
