# SeamCert

> Compiles is not the same as proves. SeamCert checks whether a Lean 4 proof's formal statement says what its claim says: the specification seam that a kernel check cannot close.

- Free scan (https://seamcert.com/#scan): paste a Lean 4 statement file. A static reading of the text; nothing is compiled or executed. Marks escape hatches (`sorry`, `admit`, custom `axiom`, `native_decide`, `implemented_by`, `extern`, `unsafe`, `#exit`, skipped kernel checks), custom definitions the theorem depends on, contradictory or false hypotheses, size promises, existential constants, and generates planted wrong variants (`Mutants.lean`) that should all fail to compile.
- GitHub Actions CI & README badge (https://seamcert.com/ci): run `POST https://seamcert.com/api/ci-scan` on pull requests and embed a live statement-seam SVG badge (`/badge/<token>.svg`) in your repository's `README.md`.
- Deep Audit (https://seamcert.com/audit): a commissioned examination of one pinned commit (£349, within five working days): independent kernel replay on a disposable build machine (Lean's kernel, `leanchecker --fresh`, and `nanoda`), planted variants run, a consistency witness for the hypotheses, custom definitions read against Mathlib, and existential constants made explicit. Every finding states whether it is kernel-checked or our reading.
- Technical guides (https://seamcert.com/guides):
  - https://seamcert.com/guides/lean-4-audit-checklist
  - https://seamcert.com/guides/lean-4-vacuous-truth
  - https://seamcert.com/guides/lean-4-native-decide-soundness
  - https://seamcert.com/guides/auditing-ai-generated-lean-proofs
- Claims & public specifications ledger: sourced notes on the 2026 complexity formalizations and open-source ZK/Ethereum/hardware specifications.
  - https://seamcert.com/claims/openai-eth
  - https://seamcert.com/claims/anthropic-eth
  - https://seamcert.com/claims/rudich-rousseau-factoring
  - https://seamcert.com/claims/verified-zkevm-clean-add32
  - https://seamcert.com/claims/ethereum-ethlib-eip7951
  - https://seamcert.com/claims/verilean-sparkle-rv32-divider
- Teams (https://seamcert.com/teams): specification-seam checks and planted variants in continuous integration.
- Full text with every claim's facts, open seams, guides, and sources: https://seamcert.com/llms-full.txt