Skill v1.0.0
currentAutomated scan100/100version: "1.0.0" name: smt-verify description: > 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. metadata: version: "0.2.0"
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
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出力がある場合はスキップ。
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)constraintnat1→Int+(>= x 1)constraint- Record types →
declare-datatypes+ constructors/selectors seq1 of char→String+(> (str.len s) 0)constraintmap K to V→ uninterpreted sort +map_apply/map_domfunctionsset of T→(Array T Bool)characteristic function representation
POに出現する全型をSMT-LIBで宣言する。変換ルールは references/type-mapping-rules.md に従う。
2b. Generate Auxiliary Definitions
Define invariants, pre-conditions, and post-conditions referenced by the PO using define-fun:
POが参照する不変条件・事前条件・事後条件を define-fun で定義する:
(define-fun inv_TypeName ((x TypeSort)) Bool ...)(define-fun pre_funcName ((arg1 Sort1) ...) Bool ...)
Include type constraints (nat/nat1 bounds, seq1 non-empty constraints) in invariant definitions.
2c. Convert the PO Body
Convert PO expressions following references/expression-mapping-rules.md.
PO式を references/expression-mapping-rules.md に従って変換する。
Key patterns:
forall x:T &→(forall ((x T_smt)) (=> type_constraint ...))— type constraint as antecedentexists x:T &→(exists ((x T_smt)) (and type_constraint ...))— type constraint conjunctedmk_R(f1,f2):Rpattern → single variable + let-bind fieldslet x = e in body→(let ((x e_smt)) body_smt)is_(e, bool)→ usuallytrue(trivial for total functions)
2d. Negate and check-sat
SMT-LIB verification uses refutation: "if the negation is unsatisfiable (unsat), the original proposition is valid":
SMT-LIBの検証は反駁法:「否定が充足不能(unsat)なら元の命題はvalid」:
(assert (not <PO_smt>))(check-sat)
Step 3: Run Z3 Verification
Save the converted SMT-LIB file and verify with Z3:
変換したSMT-LIBファイルを保存し、Z3で検証する:
# Save to filecat > /tmp/po_N.smt2 << 'SMTEOF'<SMT-LIB content>SMTEOF# Verify with Z3z3 /tmp/po_N.smt2
Step 4: Interpret and Report Results
Interpret Z3 output and report to the user in a clear manner.
Z3の出力を解釈し、ユーザーにわかりやすく報告する。
| Z3 Output | Meaning | User Explanation (EN) | ユーザー向け説明 (JA) | |
|---|---|---|---|---|
unsat | Negation unsatisfiable → PO is valid | Proved: This property is logically derived from the spec | 証明成功: この性質は仕様から論理的に導かれます | |
sat | Negation satisfiable → counterexample exists | Counterexample found: A case violating this property exists | 反例発見: この性質を満たさないケースがあります | |
unknown | Z3 cannot decide | Undecidable: Z3 cannot automatically decide. Consider simplifying the spec | 判定不能: Z3では自動判定できません。仕様の簡略化を検討してください | |
timeout | Time limit exceeded | Timeout: Verification did not complete in time | タイムアウト: 検証が時間内に完了しません |
For sat results, have Z3 output the model (counterexample):
(check-sat)(get-model)
Explain the counterexample in natural language. Example:
Counterexample: When name = "", email = "test@example.com", age = 200, the invariantage <= 150is violated.反例: name = "", email = "test@example.com", age = 200 のとき、不変条件 age <= 150 に違反します。
Step 5: Verification Summary
Summarize all PO results:
全PO結果をまとめて報告する:
## SMT Verification Summary / SMT検証サマリー| # | Definition | PO Type | Z3 Result | Verdict ||---|------------|---------|-----------|---------|| 1 | User | invariant satisfiability | unsat | Proved / 証明成功 || 2 | findUser | map apply | unsat | Proved / 証明成功 || 3 | RegisterUser | state invariant | sat | Counterexample / 反例あり |Proved: X/NCounterexample found: Y/NUndecidable: Z/N
Conversion Priority Order
Process POs in priority order rather than all at once:
すべてのPOを一度に変換するのではなく、優先度順に処理する:
- invariant satisfiability — Simple structure, mechanical conversion / 構造が単純、変換が機械的
- state init — Concrete value equality, usually trivial / 具体値の等値性、ほぼ自明
- total function —
is_(e, bool)pattern is usually trivial / 通常自明 - subtype — Record invariant checking / レコード不変条件のチェック
- map apply — Basics of map theory / 写像理論の基礎
- func/op postcondition — Most complex, nested let expressions / 最も複雑、let式のネスト
- state invariant — Requires state transition tracking / 状態遷移の追跡が必要
- map compatible — Map operation compatibility / 写像操作の互換性
Handling Unconvertible Cases
Abandon conversion and report for these cases:
以下のケースでは変換を断念し、報告する:
- Higher-order functions: SMT-LIB is first-order logic; passing functions as values is unsupported
- Recursive function termination: Outside SMT solver scope
- Infinite set/sequence cardinality:
cardrequires approximation even for finite sets - Pattern match exhaustiveness: VDMJ's checker is more appropriate than SMT for cases expressions
高階関数、再帰関数の停止性、無限集合の基数、パターンマッチの網羅性は変換不可。
When conversion is impossible:
- Provide a natural language explanation of the PO (from verify-spec)
- Present hints for manual verification
- Propose specification simplifications
Detailed References
references/type-mapping-rules.md— Complete type conversion rulesreferences/expression-mapping-rules.md— Complete expression conversion rulesreferences/conversion-examples.md— Real PO conversion examples (verified with Z3)