formal-provers（形式证明者）

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):

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 (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:

{ "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:

{ "code": "Theorem plus_comm : forall n m : nat, n + m = m + n.\
Proof. 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:

{ "formula": "(declare-const x Int)\
(assert (> x 5))\
(check-sat)\
(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