Verus

Rustの構文で書いた仕様を、実行時の検査を加えずに定理証明でRustのコードに対して検証するツール。

概念URI

https://comcomponent.com/knowledge/verus/

最終確認日

2026-08-01

機械可読データ

JSON-LD

この概念が関わる関係

• Rust(プログラミング言語)はVerusで確認できます。Verus は Rust の構文で書いた仕様を定理証明で検証するが、Rust のすべての機能への対応は目指していない。この記事では実行していない。 / 確度: 条件付きの関係 / 確認日: 2026-11-01 出典
• VerusはSMTソルバ(自動証明器)を利用します。Verus は自動証明器の Z3 を使って仕様を満たすことを確かめる。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典

この概念を扱う記事

• Ada と Rust の安全性の考え方の違い ── 型・オーバーフロー・所有権・データ競合・形式検証を実際に動かして比べる(言及)

一次資料

• https://verus-lang.github.io/verus/guide/

このページはサイトの知識グラフ(_data/knowledge/)から自動生成されています。誤りの指摘はお問い合わせからお願いします。