formal-methods
Installation
SKILL.md
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 via elan |
coqc |
Coq via opam install coq |
z3 |
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 (Apache-2.0)