Verus：Rustコードの正当性を検証する静的解析ツール

Verusは、Rustで記述されたコードの正当性を検証するための静的解析ツールです。開発者はコードが実行すべきことを記述し、Verusは実行可能なRustコードが、コードのあらゆる実行において常に仕様を満たすことを静的に検査します。実行時チェックを追加する代わりに、Verusは強力なソルバーを使用してコードの正当性を証明します。Verusは現在、Rustのサブセットをサポートしており（拡張中です）、場合によっては、標準のRust型システムを超えて、生のポインタを操作するコードなどの正当性を静的に検査できます。Verusは現在開発中であり、機能が壊れている、または欠落している可能性があり、ドキュメントも不完全です。