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 verification tools for the academic workspace. Type-check Lean 4 proofs, verify Coq theories, and solve SMT satisfiability problems with Z3.
This skill wraps locally installed formal verification provers (lean, coqc, z3) via subprocess. No Docker or external services required.
prover_status to see which provers are installedlean_check, coq_check, or z3_solve to verifyType-check Lean 4 code.
Parameters:
code (string, required): Lean 4 source codefilename (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" }
Check a Coq proof for correctness.
Parameters:
code (string, required): Coq source codefilename (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.\nProof. intros. lia. Qed." }
Compile a Coq file to a .vo object file.
Parameters:
code (string, required): Coq source codefilename (string, optional): Source filename (default: compile.v)Returns: { success, compiled, output, errors, returncode }
Solve a satisfiability problem using Z3 with SMT-LIB2 format.
Parameters:
formula (string, required): SMT-LIB2 formulaReturns: { success, result, model }
Example:
{ "formula": "(declare-const x Int)\n(assert (> x 5))\n(check-sat)\n(get-model)" }
Check which formal provers are available and their versions.
Parameters: None
Returns: { provers: { lean4: { available, version }, coq: { available, version }, z3: { available, version } } }
lean, coqc, z3)