writing-lean-proofs

An agent skill by trailofbits, from trailofbits/skills. Tags: code-quality, documentation, formal-verification, lean, math.

What it does

Writes and reviews structured Lean 4 proofs and designs Lean libraries following Mathlib conventions. Use when proving theorems in Lean, formalizing mathematics or specifications in Lean 4, defining new types or definitions in a Lean library, reviewing Lean proofs for readability and maintainability, refactoring long tactic proofs into lemmas, filling in sorry placeholders in a Lean development, setting up CI or linters for a Lean project, diagnosing slow proofs or maxHeartbeats timeouts, or writing custom tactics, macros, or linters.

Install

With the skills CLI, which installs into Claude Code, Codex, Cursor and other agents:

npx skills add trailofbits/skills --skill writing-lean-proofs

Or copy the skill folder into Claude Code's skills directory by hand (~/.claude/skills for every project, or .claude/skills inside one):

git clone --depth 1 https://github.com/trailofbits/skills
cp -r skills/plugins/writing-lean-proofs/skills/writing-lean-proofs ~/.claude/skills/writing-lean-proofs

Safety box score

Grade A, minimal risk: 7 of 100 risk points, rated 2026-10-21. The grade rates what the skill and its scripts can reach on the machine of whoever installs it, across eight categories from shell execution to secrets access. How the score works.

This skill is a Lean 4 proof-writing and library-design guide. It mainly affects Lean source files and project configuration, with the main risk being that it can lead an agent to execute Lean builds, edit proof code, and add metaprogramming/CI changes inside the repository.

Category levels, from 0 (none) to 3 (high)
Category	Level	Why
Code & shell execution	1 (low)	It explicitly directs the agent to run Lean tooling such as `lake build` and `lake env lean Path/To/File.lean`, and it covers writing custom tactics/macros/linters, so it can execute project code, but only in the Lean project context.
Network access	0 (none)	The files do not define any command that downloads or uploads data; the only remote references are static documentation links in markdown.
Filesystem reach	1 (low)	The skill is about creating and refactoring Lean source, proof files, and CI/lint configuration in the project, but there is no evidence of out-of-tree writes, deletions, or system-path access.
Secrets & credentials	0 (none)	Nothing in the skill asks for API keys, tokens, `.env` files, browser sessions, or other credential stores.
Privilege & persistence	0 (none)	There is no use of sudo, global installs, services, scheduled tasks, or shell/OS setting changes.
Instruction hijack surface	0 (none)	The text gives proof-style and linting guidance only; it does not instruct the agent to ignore higher-level rules, skip confirmations, or follow remote instructions.
Irreversible actions	0 (none)	The skill does not publish, deploy, message, pay, book, merge, or delete on the user's behalf; it stays within proof development and review.
Transparency	0 (none)	All shipped files are plain Markdown; there are no binaries, installers, base64 blobs, or generated-at-runtime code paths.

Before installing

Confirm you only want a Lean-proofing helper, not a general code-execution skill.
If you plan to use its CI/lint advice, check the resulting Lake/CI edits stay confined to your repo.
Skim `SKILL.md` for the `lake build` / `lake env lean` workflow so you know it will run Lean locally.
No extra script audit is needed here: the skill ships only Markdown references, not binaries or installers.

Rated 2026-10-21 by an automated review of 9 files from the skill's repository.

Source

Repository: trailofbits/skills (all skills from this repository)
Path: plugins/writing-lean-proofs/skills/writing-lean-proofs/SKILL.md
Branch: main
Collection: writing-lean-proofs
Updated: 2026-09-19

audit-prep-assistant — Prepares codebases for security review using Trail of Bits' checklist.
dimensional-analysis — Annotates codebases with dimensional analysis comments documenting units, dimensions, and decimal scaling.
mermaid-to-proverif — Translates Mermaid sequenceDiagrams describing cryptographic protocols into ProVerif formal verification models (.pv files). Use when generating a ProVerif.
spec-to-code-compliance — Check code against the documentation that specifies it - which requirements hold, which the code contradicts, which are absent.
principle-minimize-reader-load — Apply when reviewing or shaping code that's hard to trace.
stitch::extract-design-md — Extract a comprehensive design system (DESIGN.md) directly from frontend source code — React, Vue, Svelte, Angular, plain HTML/CSS.