Formal verification with Lean 4, Coq, and Z3 SMT solver
---
name: formal-methods
description: Formal verification with Lean 4, Coq, and Z3 SMT solver
metadata:
openclaw:
emoji: ๐ฌ
tags: [formal-verification, lean4, coq, z3, proofs]
source: https://github.com/Prismer-AI/Prismer
homepage: https://github.com/Prismer-AI/Prismer
requires:
bins: [lean, coqc, z3]
os: [darwin, linux]
runtime: node
---
# formal-methods
Formal verification tools for the academic workspace. Type-check Lean 4 proofs, verify Coq theories, and solve SMT satisfiability problems with Z3.
## Prerequisites
This skill requires the following binaries installed locally (declared in `metadata.openclaw.requires.bins`):
| Binary | Install |
|--------|---------|
| `lean` | [Lean 4](https://leanprover.github.io/lean4/doc/setup.html) via `elan` |
| `coqc` | [Coq](https://coq.inria.fr/download) via `opam install coq` |
| `z3` | [Z3](https://github.com/Z3Prover/z3) via package manager or GitHub releases |
Use `prover_status` to check which provers are available before use. The skill gracefully handles missing binaries โ only installed provers will work.
**Source:** [github.com/Prismer-AI/Prismer](https://github.com/Prismer-AI/Prismer) (Apache-2.0)
## Description
This skill invokes locally installed formal verification provers via subprocess. No Docker, containers, or external services required.
**Execution model:** Each invocation writes source code to a temporary directory (`os.tmpdir()/formal-methods-<hash>/`), runs the prover binary with `cwd` set to that directory, captures stdout/stderr, and applies a 60-second timeout. The exact commands are:
- Lean: `lean <filepath>` โ may read Lean 4 stdlib and elan-managed toolchains from `~/.elan/`
- Coq: `coqc <filepath>` โ may read Coq stdlib and opam-managed packages from the opam switch
- Z3: `z3 <filepath>` โ self-contained, only reads the input file. Accepts declarative SMT-LIB2 format only.
**Filesystem access:** The skill itself only writes to the temp directory. However, Lean and Coq read their installed standard libraries and search paths (managed by elan/opam) as part of normal operation. The skill does not explicitly constrain `--include` paths or environment variables.
**Network access:** The skill does not make network requests. However, if Lean source contains `import` of unresolved packages, `lake` tooling could theoretically attempt a fetch โ this is a Lean runtime behavior, not initiated by the skill. To prevent this, avoid `lakefile.lean` or `lake-manifest.json` in the temp directory (which the skill does not create).
## 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
## 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 declared in `metadata.openclaw.requires.bins`: `lean`, `coqc`, `z3`
- Z3 only accepts declarative SMT-LIB2 format โ no arbitrary code execution
- Each invocation has a 60-second timeout (`execSync` with `timeout: 60000`)
- Temp files are written to `os.tmpdir()/formal-methods-<hash>/`
- Lean/Coq will read their installed standard libraries (elan/opam managed) as part of normal type-checking
- The skill itself makes no network requests; Lean imports should avoid lake-managed dependencies to prevent unintended fetches
don't have the plugin yet? install it then click "run inline in claude" again.