Rustのバグを根絶！形式手法モデルチェッカー「Kani」の実力とは？

Kaniは、Rustプログラムの堅牢性を最大限に高めるためのオープンソースの形式手法（Formal Verification）ツールです。コンパイラによるチェックを超えて、プログラム内のあらゆる実行パスを網羅的に検証し、パニックやアサーション違反などの潜在的なバグを論理的に見つけ出します。並行処理の難解なバグに悩まされている方や、クリティカルなシステムの信頼性を担保したいエンジニアにとって、最強のデバッグパートナーとなるでしょう。

彼らの古い論文はこちら: https://dl.acm.org/doi/pdf/10.1145/3510457.3513031

このチュートリアルが参考になるよ: https://model-checking.github.io/kani/kani-tutorial.html シンプルな使い方だと、ちょっとhypothesis autoを思い出すね: https://github.com/timothycrosley/hypothesis-auto/

関連ツールとして、並行処理のバグ検出に特化したRustのモデル検査ツールもあるよ: https://pure.royalholloway.ac.uk/ws/portalfiles/portal/71989788/rustmc_paper.pdf

関連情報。他にはどんなものがあるかな？ Kani Rust Verifier – a bit-precise model-checker for Rust - https://news.ycombinator.com/item?id=30786511 - 2022年3月 (コメント12件)