付録B：ツールインストールガイド

本書のツール実行は、再現性（環境差の最小化）を優先し、次の2系統で提供する。

コンテナ（推奨）：devcontainer で統一環境を用意する
ローカル：最小依存（Java/curl/unzip）で実行する

コマンドは代表例であり、配布形式や前提は変更される可能性がある。必要に応じて付録E（一次情報）も参照する。

本付録の手順により、少なくとも 1つのモデルチェック（Alloy/TLC/Apalache）と、1つのプログラム検証（Dafny）を再現できる。

対象ツール（最小セット）

Alloy 6.x（CLI実行）
TLA+ TLC（tla2tools.jar）
Apalache（TLA+ 向け、SMT ベース）
Dafny（検証器）

補足：

Quint CLI は、TLA+ 意味論に基づく型付き仕様言語をCIに載せる選択肢であり、本リポジトリでは固定版のtypecheck/testをnightlyで実行する。
Rocq/Isabelle等の定理証明器は依存が大きいため、本付録では一次情報リンク（付録E）を主とする。
Lean 4 は、本書の導線として 最小構成のみを本付録末尾に示す（Optional）。
SPIN / NuSMV / CBMC / Quint / PRISM / Tamarin / SymbiYosys / RTLola に加え、cvc5 + Carcara の証明証跡再検査もnightly laneで扱う。source buildまたはarchive検査に必要な追加前提を後述する。

Tool lane inventoryと実行保証

全toolの分類、実行版、配布物digest、artifact上限、更新手順の正本は tools/tool-manifest.json である。 pr-quick はPR差分に関連する小さい例、nightly はtool単位の独立matrix、optional/manual は明示的な workflow_dispatch だけで実行する。 documentation-only は本文で紹介するが、このリポジトリがversion、環境、実行結果を保証しないtool/serviceを表す。他toolに内蔵されたsolverを間接利用しても、solver単体の実行保証には数えない。

上の inventory ブロックにある cvc5 の nightly 分類は、cvc5-alethe-unsat-certificate という狭い pinned nightly contract を表します。「cvc5 全機能の一般保証」ではなく、cvc5 1.3.4 が生成した Alethe 証跡を Carcara 1.1.0 で独立再検査する一例だけを固定します。

RTLolaのnightly分類も、架空の3 event有限traceをoffline検査する二つの狭いcontractだけを表します。正常traceで違反0件、既知の違反traceで1件を再現するものであり、RTLola全機能、本番event収集の完全性、すべての実行の正しさを保証しません。

実行laneでは、各entryにtimeout、memory budget、seed、scope、depth、boundを明示する。 artifactはtool version、command、入力ファイル別SHA-256と集約hash、exit code、stdout/stderr、success、counterexample、unknown、timeout、resource exhaustionを区別して残す。保持期間は14日、stdout/stderrは1 entry当たり16 MiB、tool outputは1 entry当たり64 MiBを上限とする。 timeoutとstdout/stderr上限はrunnerが強制し、retained tool outputは実行後に検査する。一方、memoryMiBはCI容量計画用の申告値であり、OS/cgroupによる強制上限ではない。このためresource-exhaustedは検出可能な出力超過を表し、OOM killはtool-errorまたはrunner failureになる場合がある。

quint-counter: examples/quint/counter.qnt をQuint 0.32.0のTypeScript evaluatorでtypecheckし、seed 20260716、各test 1 sampleで実行する。別配布のRust evaluatorを暗黙downloadしない。【ツール準拠（そのまま動く）】
```
node scripts/run-example-manifest.js --id quint-counter
```
kani-abs: examples/kani/abs.rs のabs_is_nonnegative harnessをKani 0.67.0、固定Rust nightly、unwind 1で検査する。追加downloadと実行コストがあるためoptional/manualであり、PRやscheduleからは起動しない。

cache復元後もQuint binaryとPRISM archiveのSHA-256を再検証する。 PRISM 4.10.1はGPL-2.0の公式Linux x86-64 archiveを毎回再展開して絶対pathを再設定し、tool binaryはrepository、CI artifact、Pagesへ再配布しない。 Tamarin Prover 1.12.0（GPL-3.0）と対応するMaude 3.5.1（GPL-2.0-or-later）も、固定SHA-256の公式archiveから毎回再展開する。Tamarinのartifactはlemma結果と欠陥版のattack graphを保持するが、両tool binaryは再配布しない。attack graphはmodel constantを保持するため、実在する秘密情報をmodelへ含めない。 SymbiYosysはOSS CAD Suite 20260716の公式Linux x64 archiveをSHA-256検証後に毎回再展開する。archive path、重複entry、symlinkの解決先、special fileを検査し、suite versionと、SBY、Yosys、Bitwuzlaのversion/source commitをbundle内のmetadata/licenseに照合する。suite release tagのcommitは配布物digestとは別の出典provenanceとして記録する。SBYとYosysはISC、BitwuzlaはMITであり、bundle内の他componentにはそれぞれのlicenseがある。artifactには正規化結果と必要なVCDだけを保持し、suite archive、展開binary、solver modelを再配布しない。保持するのは入力hash、標準出力、期待値との比較結果だけである。 Kaniは検証済みarchiveから毎回再展開し、固定日のRust channel manifestもSHA-256を検証する。Rust component本体の整合性検査は、そのmanifestに記録されたchecksumを検証するrustupに委ねる。 RTLola CLI 0.1.2はApache-2.0のcrates.io source packageを固定SHA-256で取得し、暗黙の単一rootを含むarchive path、member数、展開size、file typeを検査して毎回再展開する。package内のCargo.lockと.cargo_vcs_info.jsonを照合し、固定Rust 1.87.0で--locked buildする。artifactには正規化判定と入力hashだけを保持し、source package、binary、未加工logを再配布しない。【ツール準拠（そのまま動く）】

node scripts/run-example-manifest.js --id kani-abs

version更新は月次に公式release/tagとasset digestを確認し、versionだけの専用PRでclean-cache実行と出力契約差分をレビューする。任意のrelease assetはDependabot/Renovateのpackage参照ではないため、自動更新されたものとして扱わない。

推奨：devcontainer（コンテナ手順）

前提：

Docker が利用可能
devcontainer を扱えるエディタ（例：VS Code + Dev Containers）

手順：

本リポジトリを devcontainer で開く（.devcontainer/ を利用）
初回起動時に tools/bootstrap.sh が実行され、ツールが tools/.cache/ に配置される
次のコマンドでサンプルを実行する

# ツール取得（再実行しても可）
bash tools/bootstrap.sh

# Alloy（SATを確認）
bash tools/alloy-check.sh --verbose examples/alloy/collection.als

# TLC（No errorを確認）
bash tools/tlc-run.sh --config examples/tla/QueueBounded.cfg examples/tla/QueueBounded.tla

# Apalache（NoErrorを確認）
bash tools/apalache-check.sh --config examples/apalache/Counter.cfg --length 10 --init Init --next Next --inv Inv examples/apalache/Counter.tla

# Dafny（0 errorsを確認）
bash tools/dafny-verify.sh examples/dafny/Abs.dfy

期待される出力（抜粋）：

Alloy：SAT（例：SAT を含む行が表示される）
TLC：Model checking completed. No error has been found.
Apalache：The outcome is: NoError および EXITCODE: OK
Dafny：finished with ... verified, 0 errors

出力（反例・ログ）は .artifacts/ 配下に保存される（CI のartifactとしてもアップロードされる）。

ローカル手順（非コンテナ）

前提（Linux/WSL）

Java 17 以上（TLC/Alloy/Apalache の実行に必要）
curl / unzip

手順は devcontainer と同じで、bash tools/bootstrap.sh で必要物を取得し、tools/*.sh を実行する。

nightly lane の追加前提（Ubuntu 24.04 x86-64）

node scripts/run-example-manifest.js --lane nightlyはSPIN 6.5.2、NuSMV 2.7.1、CBMC 6.10.0、Quint 0.32.0、PRISM 4.10.1、Tamarin Prover 1.12.0、SymbiYosys、cvc5 / Carcara、RTLolaの15 entryを実行する。最小セットとは別に、SPIN/NuSMV/Carcara/RTLolaのsource buildとSymbiYosys archiveの安全なlayout検査には次の前提が必要である。CBMCはUbuntu 24.04 x86-64用の固定deb、Quintは同platform用の固定single binary、PRISMは約41 MBの固定公式archive、Tamarinは対応するMaude 3.5.1と二つの固定公式archive、SymbiYosysは約733 MBのOSS CAD Suite 20260716 Linux x64 archiveを使うため、この手順は同環境または互換環境を対象とする。

sudo apt-get update
sudo apt-get install --yes \
  bison build-essential flex g++ gcc m4 patch pkg-config \
  python3 python3-venv xz-utils

python3 -m venv tools/.tmp/nusmv-build-tools
tools/.tmp/nusmv-build-tools/bin/pip install \
  --disable-pip-version-check \
  --require-hashes \
  --requirement tools/nusmv-build-requirements.txt

PATH="$PWD/tools/.tmp/nusmv-build-tools/bin:$PATH" \
  node scripts/run-example-manifest.js --lane nightly

取得物は commit/version と SHA-256、Meson/Ninja は requirements の package hash で固定される。macOS、Windows ネイティブ、異なる CPU architecture ではこの lane を直接再現せず、Ubuntu 24.04 x86-64 のコンテナ、WSL2、または GitHub Actions の workflow_dispatch を使う。

証明証跡の独立再検査（`cvc5` + `Carcara`）に追加で必要なもの

cvc5-alethe-unsat-certificate は、cvc5 1.3.4 の公式 release asset を取得して Alethe proof を生成し、Carcara 1.1.0 互換 commit の source archive を取得して source build した checker で検査する想定です。対象環境は Ubuntu 24.04 x86-64 または同等の Linux を推奨します。

sudo apt-get update
sudo apt-get install --yes build-essential m4

# rustup と cargo が PATH 上にあることを確認する。
# bootstrap は固定した Rust/Cargo 1.87.0 を取得して使用する。
rustup --version
cargo --version

node scripts/run-example-manifest.js --id cvc5-alethe-unsat-certificate

この lane では、cvc5 binary と Carcara build 生成物をリポジトリや Pages へ再配布しません。公式 Rust channel manifest の digest は provenance sentinel として検査し、rustup が固定versionのcomponent checksumを検査した後、導入済みrustc/Cargoのcommitとhostもmanifest値へ照合します。検証済みmanifest file自体をrustupへ渡しているわけではないため、二つの検査を同一視しません。 certificateは1 MiB、checker outputは64 KiBで制限します。保持対象は、SMT-LIB 入力、manifest の期待結果契約、生成された証明証跡、stdout/stderr、入力 hash、version metadata です。証跡検査の成功は「その encoded problem に対して checker が受理した」ことだけを保証し、自然言語要件、元仕様、エンコーダ、未モデル化仮定までは保証しません。

runtime verification（RTLola）に追加で必要なもの

rtlola-auth-before-sensitive-normalとrtlola-auth-before-sensitive-violationは、固定したRTLola CLI source packageをRust 1.87.0でbuildし、相対時刻CSVをoffline監視します。対象環境はUbuntu 24.04 x86-64または同等のLinuxです。

sudo apt-get update
sudo apt-get install --yes build-essential

rustup --version
cargo --version

node scripts/run-example-manifest.js --id rtlola-auth-before-sensitive-normal
node scripts/run-example-manifest.js --id rtlola-auth-before-sensitive-violation

bootstrapはRust channel manifest、rustc/Cargo commit、host、.crate digest、埋め込みCargo.lock、upstream commitを照合します。正常系と違反系は固定した教材traceを検査するため、本番logをこのrepositoryやCI artifactへ投入してはいけません。違反系のcounterexampleは期待結果であり、monitorが所定の違反を検出できることを回帰検査します。

PRISMだけを再実行する場合は次を使う。

node scripts/run-example-manifest.js --id prism-retry-communication

この実行はDTMCと4 propertyの数値契約を再現するだけであり、教育用成功確率0.8が実システムに妥当であることは保証しない。

Tamarinの欠陥版と修正版だけを再実行する場合は次を使う。

node scripts/run-example-manifest.js --id tamarin-replay-flawed
node scripts/run-example-manifest.js --id tamarin-replay-fixed

欠陥版のcounterexampleは期待された成功結果であり、修正版は四つの指定lemmaが同じsymbolic model設定でverifiedとなることを確認する。

SymbiYosysの欠陥版BMC、修正版proof、修正版coverだけを再実行する場合は次を使う。

node scripts/run-example-manifest.js --id sby-rtl-arbiter-flawed-bmc
node scripts/run-example-manifest.js --id sby-rtl-arbiter-fixed-prove
node scripts/run-example-manifest.js --id sby-rtl-arbiter-fixed-cover

欠陥版のcounterexampleは期待された成功結果である。proofのPASSは指定propertyとassumptionに相対的なk-induction結果であり、coverのPASSは対象状態へ至るwitnessが見つかったことを表す。

OS差分（要点）

Windows：
- WSL2での実行を推奨（ツール配布物・シェルスクリプトの前提が揃う）
- WSL側に Java を導入する（Windows側のJavaではなく）
macOS：
- timeout が標準でないため、tools/tlc-run.sh --time-limit を利用するには gtimeout 等の提供が必要（例：Homebrewで coreutils を導入）。tools/tlc-run.sh は timeout/gtimeout を自動検出する。
- tools/bootstrap.sh が取得する Dafny はLinux向け配布物のため、macOSでは公式配布物（macOS向け）か dotnet tool を利用する
Linux：
- ディストリ依存でJavaパッケージ名が異なる（例：Ubuntu/Debianは openjdk-17-jre）

TLA+ / Apalache / Quint のエディタ・CLI導線（Optional）

本リポジトリでは tools/bootstrap.sh が TLC (tla2tools.jar) と Apalache を取得し、次のラッパーでログと成果物を .artifacts/ に保存する。

# TLC: .cfg、workers、depth、seed、timeoutを明示できる
bash tools/tlc-run.sh --config examples/tla/QueueBounded.cfg --workers 1 --seed 202606 --time-limit 120 examples/tla/QueueBounded.tla

# Apalache: init/next/invariantと探索長を明示する
bash tools/apalache-check.sh --config examples/apalache/Counter.cfg --length 10 --init Init --next Next --inv Inv examples/apalache/Counter.tla

TLA+ をエディタで編集する場合は、VS Code拡張を利用しつつ、拡張、Java、tla2tools.jar、.cfg の版を PR 本文に記録する。本リポジトリのQuint契約は、公式release binaryとSHA-256をtools/tool-manifest.jsonで固定し、暗黙に追加componentを取得しないTypeScript evaluatorでtypecheckとtestを実行する。 verifyを追加する場合はApalache/TLC backend、JDK、探索境界、timeout、trace artifactを別entryとして固定する。

node scripts/run-example-manifest.js --id quint-counter

quint-counterの成功は、対象仕様の型検査と固定testが通ったことだけを表す。結果を「仕様全体の証明」とは扱わず、verifyを使う場合は対象仕様、backend、境界、seed、timeout、反例traceの保存場所を合わせて確認する。

Lean 4 環境構築（最小構成 / Optional）

Lean 4 は、本書では「定理証明を資産化し、運用可能にする」選択肢として位置づける（第9章参照）。ここでは 最短・最小構成として、起動までの導線のみを示す（詳細は一次情報を参照）。

事前に理解しておくこと（最小）

elan：Lean toolchain（Lean 本体・コンパイラ等）を管理するためのツール
Lake：Lean 4 のビルド/依存管理ツール（プロジェクト作成・ビルドに使用）
VS Code拡張：型チェック結果やゴール表示など、対話的な開発体験を提供

手順（代表例）

elan を導入する（一次情報）
VS Code + Lean 4 拡張を導入する（一次情報）
Lean 4 の最小プロジェクトを作成して起動確認する（代表例）

mkdir -p lean-sandbox && cd lean-sandbox
lake init hello
lake build

確認：

VS Code で lean-sandbox/ を開き、生成された .lean ファイルを開く
エラーが出ないこと（ツールチェーンが有効であること）を確認する

一次情報（公式/代表）：

Lean 公式: https://lean-lang.org/
Lean 4（GitHub）: https://github.com/leanprover/lean4
elan: https://github.com/leanprover/elan
VS Code Lean 4 拡張: https://github.com/leanprover/vscode-lean4

主要ツール別の導入メモ（最小導線）

個別ツールは更新頻度が高いため、本書では完全なインストール手順を固定しない。導入時は付録Eの一次情報を起点に、次の三点を PR 本文または CI 設定に残す。

公式ドキュメントまたは公式リリースへのリンク
実行したバージョン確認コマンドと結果
CI で固定した依存（バイナリ、jar、npm package、opam switch、Rust toolchain、solver、timeout、seed）

領域	ツール	導入・確認の最小方針
Alloy	Alloy 6 Analyzer	公式リリースから jar を固定し、`java -jar ...` で起動確認する。CI では jar のURL、SHAまたはバージョン、`steps`、scope を記録する。
TLA+	TLC / VS Code 拡張	`tla2tools.jar`、Java、`.cfg`、workers、seed、timeout を記録する。VS Code拡張は編集支援であり、CI ではCLI再実行を正本にする。
TLA+ 周辺	Apalache	配布zipまたはコンテナを固定し、`apalache-mc version` 相当の出力、探索長、init/next/invariant、solver設定を記録する。
TLA+ 周辺	Quint	`@informalsystems/quint` を `package.json` / lockfile で固定し、`typecheck`、`test`、`verify` を分ける。backend（Apalache/TLC）と出力traceの保存先を記録する。
定理証明	Lean 4 / Lake / mathlib	`elan` で toolchain を固定し、`lake build` を CI で再実行する。`lean-toolchain`、`lake-manifest.json`、mathlibのrevisionを証跡に含める。
定理証明	Rocq	公式リリース/パッケージ手順を使い、Rocq/Coq 互換コマンド名、opam switch、ライブラリ版を記録する。`Admitted.` や不要な公理は CI で棚卸しする。
Rust検証	Kani	`cargo kani` または公式手順で導入し、`kani --version` 相当、Rust toolchain、proof harness、unwind/探索境界を記録する。
Rust検証	Verus	公式配布またはソースビルドのrevision、`verus --version` 相当、Rust toolchain、Z3版、未証明 `assume` を記録する。
Rust検証	Creusot	公式ガイドに従い、Creusot、Why3、SMT ソルバー、Rust toolchain、loop invariant / variant、ghost codeの扱いを記録する。
Rust検証	Prusti	Prusti/Viper、Rust toolchain、事前条件・事後条件・ループ不変条件、counterexample出力を記録する。
Rust検証	Aeneas	変換対象のRust subset、Charon/LLBC、接続先（F*、Rocq、HOL4、Lean 等）、生成物のrevisionを記録する。
SMT	cvc5 / Z3	solver単体の版、呼び出し元ツール、timeout、`unknown` の扱いを記録する。solver差し替え時は結果差分をレビュー対象にする。

Cedar、Bedrock Guardrails、スマートコントラクト検証のようなクラウド/産業ツールは、CLI手順よりもサービス仕様の変化が大きい。導入メモでは、対象API、リージョン、対応言語、ポリシー/仕様の版、検証対象コミット、実行ログを中心に残す。

CI（自動実行）

GitHub Actions では .github/workflows/formal-checks.yml で、PR 向け（軽量）と夜間向け（深い探索）のジョブを提供している。ローカルで同等の実行をしたい場合は、bash examples/ci/pr-quick-check.sh を実行する。