gabrielmoreira formal-methods
Formal verification tools for the academic workspace. Type-check Lean 4 proofs, verify Coq theories, and solve SMT satisfiability problems with Z3.
Process
- Check availability — Use
prover_statusto see which provers are installed - Write proof — Draft your Lean/Coq code or SMT formula
- Verify — Use
lean_check,coq_check, orz3_solveto verify - Iterate — Fix errors based on output and re-check
Tools
lean_check— Type-check Lean 4 code. Params:code(required),filenamecoq_check— Check a Coq proof. Params:code(required),filenamecoq_compile— Compile Coq to.voobject file. Params:code(required),filenamez3_solve— Solve SMT-LIB2 formula. Params:formula(required)prover_status— Check available provers and versions. No params.
Example:
{ "code": "theorem add_comm (a b : Nat) : a + b = b + a := Nat.add_comm a b" }
See canonical skill for full tool documentation and parameter details.