mirror of
https://github.com/trailofbits/skills.git
synced 2026-09-14 14:28:48 +08:00
Fredrik Dahlgren
7b9bd5f950
* Add writing-lean-proofs plugin Structured Lean 4 proof writing and library design following Mathlib conventions: sorry-skeleton workflows, API-first definitions, lemma extraction, and an anti-pattern catalog mapped to the linters that enforce each rule. Includes a review-flow eval suite (evals/): five Lean fixtures derived from a real formal-verification project with known planted flaws and known non-flaws, natural review prompts, per-case rubrics, and a runner comparing a baseline arm against a skill arm with an LLM judge plus a deterministic no-rewrite check. The grader ships a self-test that asserts a known-bad review fails every criterion. Smoke-tested: the baseline arm reproduces the folk-advice mistake the skill corrects (calling redundant `show` lines noise); the skill arm passes 5/5. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Address Claude review findings - Validate the grader's "id" field before writing grades.json, so a malformed grader response fails with a clear error instead of a KeyError in the summary. - Restore title-case "When to Use"/"When NOT to Use" headings: the validator's required-section check matches them case-sensitively. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Address github-actions review findings Eval harness: - checksum_tree fails when it finds zero .lean files, so the no-rewrite check can no longer pass vacuously - both arms run with --setting-sources project, so a user-level install of this skill cannot contaminate the baseline arm - a failed case is recorded and the run continues; the runner exits non-zero after printing the summary - critical steps in run_case return explicitly (errexit is suppressed when the function runs in an if-context) - self-test prints its artifact dir; the on-failure leak is intentional - case 04: dropped the trailing omega so the squeezed simp only in carry_le_one is genuinely terminal (the direction test was inverted) - case 05: overall-verdict retyped from must-flag to overall, with the grader prompt told to judge such criteria solely by pass-when text - fixture overlap removed: Felt.lean's unscored unfold replaced by a bound-free lemma; Bounds.lean's unscored Fact instance replaced by the NeZero instance ZMod.val_lt actually needs Skill content (claims verified against Mathlib docs and the ImProver paper): - lake build alone does not catch sorries (they are warnings); step 4 now includes an explicit grep gate - style linters are enabled in Mathlib's own build but off by default downstream; the opt-in is now spelled out. The show, nameCheck, and setOption linters do exist, so those attributions stand. - ImProver's 100% is on the paper's accuracy metric and holds by construction (fallback to unchanged input); now stated as such - isCompact_union does not exist in Mathlib; example is isCompact_iUnion - library-design.md now distinguishes rfl-proved API lemmas (correct) from downstream proofs needing rfl (the smell) - plugin README Contents paths fixed to be relative to the skill dir Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Address second-round github-actions review findings Eval harness: - case 05 gains an engagement criterion: the review must name specific declarations from the file, so an empty "looks fine" can no longer score 5/5 by omission - the grader self-test is now two-sided: the canned bad review must fail every criterion (catches a permissive judge) and a new canned good review must pass every criterion (catches an over-strict judge) - case 01 scores the native_decide in the Fact instance; it was the most severe flaw in the fixture and previously unscored - checksum_tree excludes .claude/ so both arms fingerprint the same file set - runtime check on the isolation guard: a baseline transcript that mentions writing-lean-proofs fails the case as contaminated - results stamp includes the PID so same-second runs cannot collide - case 04: mod_add_carry_mul uses non-terminal simp [carry] (a bare simp risked "no progress"/goal-closing errors that would invalidate the criterion); rubric wording updated Skill content: - the sorry check had inverted exit status for CI use (grep exits 1 on no match); now ! grep, with the comment/docstring false-positive caveat and #print axioms alternative spelled out - anti-patterns.md documents native_decide (trust-base widening, caught by #print axioms, kernel/certificate alternatives) - llm-techniques.md sibling links demoted to plain-text mentions: AGENTS.md prohibits reference chains (file1 -> file2), which the earlier link conversion had introduced Verified: two-sided self-test passes (bad 0/7, good 7/7); live case 05 run scores baseline 2/6 vs skill 6/6 with no-rewrite passing in both arms and no contamination false-positive. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * feat: add linting, performance, and tactics references to Lean skill * Make the eval harness's own checks able to fail Five review findings, all cases of a check that reports rather than gates. - no-rewrite gates the exit status. It was written, printed, and otherwise ignored: CASE_FAILURES only counted reviewer/grader *errors*, so a reviewer that started applying its own fixes under --permission-mode acceptEdits would rewrite every fixture, print no-rewrite:fail on every line, and still exit 0 — CI would read the run as green. - Add the skill arm's mirror of the baseline contamination backstop. cp -R succeeding proves the skill is on disk, not that the CLI discovered it. If project-skill discovery under --setting-sources project ever changes, the skill arm would run bare and both arms would score alike — which is indistinguishable from the true negative "the skill provides no uplift", the one conclusion this suite exists to measure. One canary call per run asks the CLI what it can see. - Guarantee the scratch tree is removed. run_case's body moved into run_case_body so the single rm -rf covers every early return; six paths (fixture copy, skill copy, both checksums, the reviewer call, the contamination check) previously leaked a fixture copy — plus a full skill copy on the skill arm — per case. - Run the offline half of --self-test before the CLI preflight, so the schema, isolation-fixture and rubric checks work with no `claude` on PATH and no authentication — which is where you would want them, e.g. a CI shell-test suite. - Count rubric criteria with the same pattern the Python capture uses. The shell count accepted `- id: foo bar`, which the capture drops, so a malformed line surfaced later as a confusing id-mismatch diff. Also anchor linting.md's warnings-as-errors CI snippet against vacuity: Lake caches per-module artifacts and linter warnings are emitted only on recompile, so on a restored cache build.log is empty, the grep matches nothing, and the gate reports clean over live warnings and sorries — the exact failure the same file preaches against. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: kz-tob <kara.zaffarano@trailofbits.com> Co-authored-by: Marc Ilunga <marc.ilunga@trailofbits.com>
writing-lean-proofs
Structured Lean 4 proof writing and library design following Mathlib conventions — for proofs and libraries that humans and LLMs can review, repair, and extend.
What it does
Guides Claude (and Codex, via marketplace compatibility) through a design-top-down, prove-bottom-up workflow:
- Design definitions and their API first — total functions with junk values, bundled morphisms/subobjects, simp-normal forms, API lemmas in the same file before first use.
- Build a sorry skeleton — state the theorem and its lemmas as
compiling
sorrystubs (spec-driven development, as practiced by the Liquid Tensor Experiment, PFR, and FLT projects), then thehave/suffices/calcskeleton inside each proof. - Fill goals one at a time — focusing dots, honest
showlines, calc chains, simp discipline. - Verify mechanically — compile and lint; never eyeball-check style.
Plus: the extraction ladder (when a have graduates to a lemma), Mathlib
naming so lemma names are guessable, an anti-pattern catalog mapped to the
linters that catch each one, and evidence-based techniques specific to
LLM-written proofs (goal-state annotation, typed-have skeletons,
verification in the loop).
Why these rules
Every principle is sourced from Mathlib's style/review/naming guides, the Mathlib maintenance papers, retrospectives of large formalizations (perfectoid spaces, LTE, PFR, FLT), Mathematics in Lean, Theorem Proving in Lean 4, and the ImProver paper (ICLR 2025) for LLM-specific techniques. The claims were verified against the primary sources; commonly overstated rules (e.g. turning Mathlib's general one-tactic-per-line recommendation into an absolute requirement) are qualified in the anti-patterns reference.
Contents
All paths below are relative to skills/writing-lean-proofs/:
SKILL.md— workflow, extraction ladder, quick-reference rulesreferences/library-design.md— definitions, APIs, abstraction boundaries, project decompositionreferences/proof-style.md— tactic proof structurereferences/naming-conventions.md— Mathlib namingreferences/anti-patterns.md— anti-patterns → rationale → enforcing linterreferences/llm-techniques.md— LLM-specific drafting techniquesreferences/linting.md— axiom audits, library versus self-contained CI linter profiles, and project-specific lintersreferences/performance.md— proof and reduction-cost diagnosisreferences/tactics.md— safe, bounded, traceable tactic metaprogramming
Evals
evals/ contains a review-flow eval suite: Lean fixtures (derived from a
real formal-verification project) with known planted flaws and known
non-flaws, natural review prompts, per-case rubrics, and a runner that
compares a baseline arm against a skill arm using an LLM judge. See
evals/README.md; evals/run.sh --self-test verifies the
grader still detects a known-bad review.
When not to use
Lean-as-programming-language work without proofs, other proof assistants (Coq/Isabelle/Agda), Lean 3 codebases, or projects with a conflicting house style (defer to their CONTRIBUTING).