formal-methods
Verify proofs, check theorem correctness, and solve satisfiability problems using Lean 4, Coq, and Z3 SMT solver. Use when the user asks to prove theorems, verify mathematical proofs, check logical satisfiability, or work with proof assistants.
ソース情報
- リポジトリ
- Prismer-AI/Prismer
- ソースの最終更新活動
- 2026年3月19日 07:49
- 検出された SKILL.md の言語
- 英語
- スター
- 794
- フォーク
- 38
インストール方法
デフォルトでは、最初にソースを確認する Prompt が選択されています。直接コマンドに切り替えるか、ローカルコピーをダウンロードすることもできます。
ソースファイルを確認
インストールを決める前に、SKILL.md と SkillsMP に表示されている付属ファイルをお読みください。
ファイルエクスプローラー
3 ファイルSKILL.md を表示中
SKILL.md
ソースの指示 · 読み取り専用プレビュー- name
- formal-methods
- description
- Verify proofs, check theorem correctness, and solve satisfiability problems using Lean 4, Coq, and Z3 SMT solver. Use when the user asks to prove theorems, verify mathematical proofs, check logical satisfiability, or work with proof assistants.
# formal-methods
Formal verification tools for the academic workspace. Type-check Lean 4 proofs, verify Coq theories, and solve SMT satisfiability problems with Z3.
## Description
This skill wraps locally installed formal verification provers (`lean`, `coqc`, `z3`) via subprocess. No Docker or external services required.
## Usage Examples
- "Check if this Lean 4 proof type-checks"
- "Verify my Coq induction proof"
- "Is this SMT formula satisfiable?"
- "What provers are available?"
## Process
1. **Check availability** — Use `prover_status` to see which provers are installed
2. **Write proof** — Draft your Lean/Coq code or SMT formula
3. **Verify** — Use `lean_check`, `coq_check`, or `z3_solve` to verify
4. **Iterate** — Fix errors based on output and re-check. Common patterns: "type mismatch" in Lean means type annotations need fixing; "unsat" from Z3 means no satisfying assignment exists (formula is a tautology when negated); "unknown" means Z3 couldn't determine satisfiability within limits
## Tools
### lean_check
Type-check Lean 4 code.
**Parameters:**
- `code` (string, required): Lean 4 source code
- `filename` (string, optional): Source filename (default: `check.lean`)
**Returns:** `{ success, output, errors, returncode }`
**Example:**
```json
{ "code": "theorem add_comm (a b : Nat) : a + b = b + a := Nat.add_comm a b" }
```
### coq_check
Check a Coq proof for correctness.
**Parameters:**
- `code` (string, required): Coq source code
- `filename` (string, optional): Source filename (default: `check.v`)
**Returns:** `{ success, compiled, output, errors, returncode }`
**Example:**
```json
{ "code": "Theorem plus_comm : forall n m : nat, n + m = m + n.\nProof. intros. lia. Qed." }
```
### coq_compile
Compile a Coq file to a `.vo` object file.
**Parameters:**
- `code` (string, required): Coq source code
- `filename` (string, optional): Source filename (default: `compile.v`)
**Returns:** `{ success, compiled, output, errors, returncode }`
### z3_solve
Solve a satisfiability problem using Z3 with SMT-LIB2 format.
**Parameters:**
- `formula` (string, required): SMT-LIB2 formula
**Returns:** `{ success, result, model }`
**Example:**
```json
{ "formula": "(declare-const x Int)\n(assert (> x 5))\n(check-sat)\n(get-model)" }
```
### prover_status
Check which formal provers are available and their versions.
**Parameters:** None
**Returns:** `{ provers: { lean4: { available, version }, coq: { available, version }, z3: { available, version } } }`
## Notes
- Requires provers installed locally (`lean`, `coqc`, `z3`)
- Z3 only accepts SMT-LIB2 format (declarative, no arbitrary code execution)
- Execution timeout is 60 seconds per invocation
GitHubで見る