aws.amazon.com

Verus で正しさが証明できる Rust コードの開発

Rust の型システムは多くのバグを防ぎますが、コードが本当に正しいことまでは保証しません。そこで、Rust 向けのオープンソースの自動プログラム検証ツール Verus を紹介します。事前条件・事後条件による仕様記述の書き方、1 秒未満の高速なフィードバック、unsafe コードや並行コードの正しさの証明、そして Nitro Isolation Engine をはじめとする Amazon 社内やオープンソースでの活用事例まで説明します。