smt-verifylisted

Convert VDM-SL proof obligations (POs) to SMT-LIB and verify them with the Z3 solver. Triggered by "prove POs", "verify with SMT", "check with Z3", "auto-verify proof obligations", "prove the spec is correct", or "find counterexamples". Also responds to Japanese: 「POを証明して」「SMTで検証して」「Z3で確認して」等。 Used as the next step after PO generation with verify-spec, or for end-to-end PO generation + SMT verification.
kotaroyamame/formal-agent-contracts · ★ 1 · Data & Documents · score 62

Install: claude install-skill kotaroyamame/formal-agent-contracts

# PO → SMT-LIB Conversion and Z3 Verification Convert proof obligations (POs) generated by VDMJ into SMT-LIB format and verify them with Z3. VDMJが生成した証明責務（PO）をSMT-LIB形式に変換し、Z3で自動検証する。 ## Prerequisites ### Z3 Installation Check ```bash which z3 || pip install z3-solver --break-system-packages ``` If Z3 is not available, guide the user through installation. Z3がない場合はユーザーにインストールを案内する。 ### VDMJ Setup Locate the VDMJ JAR using the same method as the verify-spec skill. verify-specスキルと同じ方法でVDMJ JARを特定する。 ## Verification Flow ### Step 1: PO Generation Generate POs using the verify-spec procedure. Skip if PO output already exists. verify-specの手順でPOを生成する。すでにPO出力がある場合はスキップ。 ```bash java -jar <VDMJ_JAR> -vdmsl <files...> -p 2>&1 ``` ### Step 2: Convert Each PO to SMT-LIB For each generated PO, perform the following conversion steps. 各POについて以下の手順で変換する。 #### 2a. Generate Type Declarations Scan all types appearing in the PO and declare them in SMT-LIB. Follow conversion rules in `references/type-mapping-rules.md`. Key mappings: - `nat` → `Int` + `(>= x 0)` constraint - `nat1` → `Int` + `(>= x 1)` constraint - Record types → `declare-datatypes` + constructors/selectors - `seq1 of char` → `String` + `(> (str.len s) 0)` constraint - `map K to V` → uninterpreted sort + `map_apply`/`map_dom` functions - `set of T` → `(Array T Bool)` characteristic function representation POに出現する全型をSMT-LIBで宣言する。変換ルールは `references/type-mapping-rules.md` に従う。 #### 2b. Generate Auxiliary Defini