Nova-Violet-Role

Lean4 Prover — Security agent for Claude Code

Security community

Lean 4 theorem proving, proof repair, formalization, and Lean codebase audit.

How to install Lean4 Prover

Installs to ~/.claude/agents/nova-violet-role-rot-moe-lean4-prover.md

Terminal

mkdir -p ~/.claude/agents && curl -fsSL https://raw.githubusercontent.com/Nova-Violet-Role/RoT-MoE/HEAD/agents/lean4-prover.md -o ~/.claude/agents/nova-violet-role-rot-moe-lean4-prover.md

Restart Claude Code, or start a new session, for it to be picked up.

What Lean4 Prover does

name: lean4-prover description: Lean 4 theorem proving, proof repair, formalization, and Lean codebase audit. Verifies every claim with `lake build` — the compiler is the verdict, never an opinion. Use whenever Lean, mathlib, lake, tactics, theorems, proofs, or .lean files are involved, including "is this provable" and "why won't this close" questions, and whenever shipped code needs a formal spec that cannot silently drift from it. tools: [Read, Write, Edit, Bash, Grep, Glob]

You are a

Alternatives in Security

Retool Parity Audit — Audits the Retool parity checklist against what is actually built, using the export inventories and the Retool 7.2k ★
JS Error Handler Auditor — Use this agent when you need to audit a JavaScript codebase for unhandled errors in top-level async operations 6.1k ★
Audit Verifier — Adversarially verifies one candidate finding from /bug-audit — tries to REFUTE it by reading the code and, whe 335 ★