Rustの安全性を数学的に証明するVerus、Amazonが基盤インフラで採用
Developing provably correct Rust code with Verus
Rustは型システムで多くのバグを防ぐが、「実際に正しい」ことまでは保証しない。VerusはRust向けのオープンソース自動プログラム検証器で、数学的な仕様に対してコードを全入力について機械的に検証する。開発者はRustに似た構文で事前条件・事後条件を注釈として書き、1秒未満の高速なフィードバックを得られるほか、AIによる証明生成の支援も可能だ。unsafeブロックや独自ロック方式の並行コードも検証でき、AWSのNitro Isolation Engineなどで安全性の保証を再確立している。
「より正しく安全」は「実際に正しく安全」とは違う。
HNでの議論
36- 63
これが面白いと思ったなら、似たような目標やスコープを持つ関連プロジェクトについても聞いてみると興味深いかもしれません：Miri[0]、Kani[1]、Creusot[2]です。Verus、Kani、Creusotの間にはかなりの重複があるようですが、私はどれも使ったことがないので、それらを区別しようとするのは控えておきます。
[0]https://github.com/rust-lang/miri
- sourdecor
Verusはまさに私が探していたもののようです！以前HNでAllConcur[0]を見つけて、Goに移植したいと思ったのですが、TLA+とCを使っていて、TLA+をCにコンパイルできない限り実装を信頼できるのか理解するのが非常に混乱しました。
GeminiとVerusをTLA+と比較について話していて、TLA+は通常（例えば）「分散合意プロトコルが論理的に健全であることを証明する」ために使われると言っていましたが、Verusも同じことができるかと尋ねたら、できると言いました。つまり、VerusはコンパイルしてRustと統合できるのに対し、TLA+はより設計図の開発に使われ、それが実装者の頭の中で実装を導くのです。
素晴らしいですね！
- nottorp
新しく改良されたUbuntuのcoreutilsのバグに役立つのでしょうか？
- Meneth
「上記のコードのバグに注意してください。私はそれが正しいことを証明しただけで、試してはいません。」 - Donald Knuth。
- lukeify
私の大学の教授の一人が開発したWhileyを思い出させます。