setup 是 agent-formal-verify 插件的工具准备技能，目标是把形式化验证所需的共享工具一次性装好，且与具体代码仓库无关。
用途：准备工作包括 Java、Python 3、TLC、elan、Lean、Rust 和 Kani。验证阶段会依据各仓库当前目标，从 TLA+、Lean 与 Kani 中选择工具；插件全局安装时，同一套工具可在多个仓库间复用。
主要能力与做法：技能先读取工具设置中的固定版本与环境配置，检查操作系统和已有运行时，并尽量复用已安装的前置条件与工具缓存。它确保可用的 JDK、Python 3、SHA256 工具、elan、Rust、固定版本的 Kani 与固定版本的 TLC JAR 就绪；缺失项通过用户现有包管理器或上游文档安装器安装，并遵循其安装约束。tla2tools.jar 需从 scripts/tlc-tools.sh 固定的 TLA+ 版本获取，保存到辅助脚本指定的路径；该脚本会校验 SHA256，但不自行下载。Kani 按工具设置中的版本用 Cargo 安装，然后执行 cargo kani setup；插件辅助脚本只做验证，不安装或下载。
使用方式：先确认 java -version 成功；若 java 不在 PATH，或在 macOS 上被解析为桩程序，则把 JAVA 设为可用 JDK 的 java 二进制路径，并在后续命令中使用，同时报告该设置，因为验证阶段同样需要。随后以形式化验证技能目录（本技能的兄弟目录）的绝对路径替换 <skill-dir>，依次运行：
bash <skill-dir>/scripts/setup.sh rust bash <skill-dir>/scripts/setup.sh tla bash <skill-dir>/scripts/setup.sh lean <skill-dir>/examples/lean-template
三条命令都须成功退出并输出 READY 行。Lean 模板仅提供默认版本固定，不会创建模型项目，也不会更改 elan 的全局默认。已安装的插件文件应视为只读。重复执行 setup 会复用已准备好的工具；验证时按需处理仓库特定的 Lean 版本固定。
适用场景：初次安装、缺少前置条件、需要为多仓库统一准备形式化验证工具链，以及安装后核验工具是否就绪。
限制：若没有合适的安装方法或用户未允许安装，技能只报告缺失的前置条件及其安装说明，不强行安装。就绪状态只确认工具链可用；模型正确性由矩阵运行器和 Lean 检查器负责。