luminpulse-ai/formal-methods
skills/formal-methods/SKILL.md
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.
$ install --global
skillsauthnpx skillsauth add luminpulse-ai/prismer formal-methodsInstall this skill globally with one command. Works with Claude Code, Cursor, and Windsurf.
Security Scan Results
3 of 9 scanners reported clean
Some scanners were skipped, did not run, or reported a non-clean status. Review each row below.
3
Scanners Passed
9
Scanners in report
Clean
TrivyContainer and dependency vulnerability scanner
95%
Clean
SemgrepStatic code analysis for vulnerabilities
95%
Clean
mcp-scan (Snyk)Model Context Protocol security validation
95%
Skipped
Snyk (dep)Open source security scanning
50%
Skipped
Socket.devSupply chain security analysis
50%
Skipped
VirusTotalMulti-engine malware detection
50%
Skipped
CrowdStrikeAdvanced threat intelligence
50%
Skipped
OSV-ScannerOpen Source Vulnerability database check
50%
Skipped
OWASP Dep-Check
50%
Last scanned: Apr 24, 2026, 4:09 PM55.6s3 files scanned
SKILL.md
- name:
- formal-methods
- description:
- 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-methods
Formal verification tools for the academic workspace. Type-check Lean 4 proofs, verify Coq theories, and solve SMT satisfiability problems with Z3.
Description
This skill wraps locally installed formal verification provers (lean, coqc, z3) via subprocess. No Docker or external services required.
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
- 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. Common patterns: "type mismatch" in Lean means type annotations need fixing; "unsat" from Z3 means no satisfying assignment exists (formula is a tautology when negated); "unknown" means Z3 couldn't determine satisfiability within limits
Tools
lean_check
Type-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" }
coq_check
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." }
coq_compile
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 }
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)\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 installed locally (
lean,coqc,z3) - Z3 only accepts SMT-LIB2 format (declarative, no arbitrary code execution)
- Execution timeout is 60 seconds per invocation
Related Skills
luminpulse-ai/latex-compiler
development
VerifiedTrustedCommunity
Compile LaTeX documents to PDF using pdflatex, xelatex, or lualatex with template support. Use when the user asks to compile .tex files, build a LaTeX document, generate PDF from LaTeX, or typeset an academic paper.
823SKILL.mdUpdated Apr 24, 2026
luminpulse-ai/hf-papers
data-ai
VerifiedTrustedCommunity
Browse trending papers, search by keyword, and get paper details from Hugging Face Papers. Use when the user wants to find ML research, asks about recent AI papers, trending models, or mentions Hugging Face Papers.
823SKILL.mdUpdated Apr 24, 2026
luminpulse-ai/arxiv-reader
research
VerifiedTrustedCommunity
Read and analyze arXiv papers by fetching LaTeX source, listing sections, or extracting abstracts. Use when the user mentions arXiv, research papers, preprints, paper IDs like 2301.xxxxx, or wants to read academic publications.
823SKILL.mdUpdated Apr 24, 2026
luminpulse-ai/peer-review
documentation
VerifiedTrustedCommunity
Conduct thorough academic peer reviews with structured feedback using load_pdf and arxiv_to_prompt. Use when the user asks to review a paper, provide manuscript feedback, critique research, or write a referee report.
823SKILL.mdUpdated Apr 24, 2026