Kani

モデル検査でRustのプログラムを解析し、未定義動作・パニック・算術オーバーフロー・アサーションなどを検査するオープンソースの検証ツール。

概念URI

https://comcomponent.com/knowledge/kani/

別名・表記

Kani Rust Verifier

最終確認日

2026-08-01

機械可読データ

JSON-LD

この概念が関わる関係

• Rust(プログラミング言語)はKaniで確認できます。Kani はモデル検査で Rust のプログラムの未定義動作・パニック・算術オーバーフロー・アサーションを検査する。この記事では実行していない。 / 確度: 条件付きの関係 / 確認日: 2026-11-01 出典
• 整数オーバーフローはKaniで確認できます。Kani は算術オーバーフローを検査の対象に含む。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典

この概念を扱う記事

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

一次資料

• https://model-checking.github.io/kani/

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