agentmods.dev

QECLean: Instructions file for Claude Code

CLAUDE.md

QECLean CLAUDE.md is an instructions file for Claude Code from Stavan-Jain/QECLean. It costs 11,849 tokens per session, scanned C, original, Apache-2.0.

A project instruction file for QECLean, a Lean 4 and mathlib library that formally verifies parts of quantum error correction. It explains the library's relationship to a separate research repository.

In plain words
What is it for?
Use it when navigating QECLean, building the Lean library, or working on formalization branches that depend on the sibling qec-lab repository.
Why use it?
It gives agents the project layout, required reading, build command, and rules for keeping formal proofs complete and accepted.

Instructions file for Claude Code

Written for Claude Code: the file is CLAUDE.md. Also seen: mentions CLAUDE.md; mentions Claude Code.

This is Stavan-Jain/QECLean's own configuration. It tells Claude Code how to work on QECLean itself, so it is not a mod to install elsewhere. Copy it as a starting point and replace the rules that are about this project. Everything QECLean configures →

Needs its repository: it reads a path above its own folder, which exists only inside the repository. The line is diff lake-manifest.json ../../../lake-manifest.json && {.

not rated 48repo changed 4d ago C scan 11,849 tokens original Apache-2.0
View source ↗ Stavan-Jain/QECLean stavan-jain.github.io
Reuse

Borrowing it

Nothing to install: this file belongs to Stavan-Jain/QECLean. Take a copy, put it at the same path in your own repository, and replace the rules that are about this project with yours.

Copy the file
curl -O https://raw.githubusercontent.com/Stavan-Jain/QECLean/main/CLAUDE.md
Clone the repo
git clone --depth 1 https://github.com/Stavan-Jain/QECLean

Made for: Claude Code.

Wrote this? Show the measurements

A badge with what this costs and how it scanned, read live from this page, so it follows the numbers instead of freezing them. Markdown for a README, HTML for a documentation site or a project page.

agentmods badge for QECLean CLAUDE.md

README.md
[![agentmods](https://agentmods.dev/badge/instructions/stavan-jain/qeclean/claude-md/github.svg)](https://agentmods.dev/instructions/stavan-jain/qeclean/claude-md)
Your own site
<a href="https://agentmods.dev/instructions/stavan-jain/qeclean/claude-md"><img src="https://agentmods.dev/badge/instructions/stavan-jain/qeclean/claude-md/github.svg" alt="Measured on agentmods" height="20"></a>

Or the 80×15 button, for a site that already has a row of RSS and ATOM ones. Only the verdict fits; the numbers stay here.

agentmods 80×15 button for QECLean CLAUDE.md

Your own site · 80×15
<a href="https://agentmods.dev/instructions/stavan-jain/qeclean/claude-md"><img src="https://agentmods.dev/badge/instructions/stavan-jain/qeclean/claude-md.svg" alt="Reviewed on agentmods" width="80" height="20"></a>
Per session 11,849 This file is loaded in full into every session.
When invoked 11,849 The same file — it is already loaded in full.
Security scan C 1 finding. A grade says what 26 rules found in the file — not that it is safe.
Origin original No closer match found in the catalogue.
Token cost

What it costs to keep this loaded

Counted locally with the o200k_base tokenizer, which is exact for GPT models; Claude uses its own tokenizer and its counts differ. Treat this as one consistent yardstick across the catalogue rather than a bill. Prices are per million input tokens.

ModelPer sessionOnce invoked
Fable 5.1 $0.11849 $0.11849
Opus 5.5 $0.04740 $0.04740
Sonnet 5.5 $0.02370 $0.02370
Haiku 4.5 $0.01185 $0.01185

Measured 4d ago against content hash 5b797e84f201, method: parsed. Prices are Anthropic first-party input rates as of 2026-10-07, from the pricing page.

Security

Grade C, and why

QECLean CLAUDE.md scanned grade C with 1 finding against 26 rules in 11 categories — prompt injection, anti-refusal, data exfiltration, privilege escalation, supply chain, agent snooping, system-prompt leakage, SSRF and excessive agency — measured 4d ago.

A static scan of the body, not an audit. Every finding is printed with the line that produced it so you can judge whether it matters here. A mod is markdown that instructs an agent; that is exactly why what it instructs is worth reading.

Recursive force deletehighDestructive command

rm -rf with a variable or a broad path is one typo away from removing the wrong tree.

rm -rf .lake/packages
CLAUDE.md · 777 lines

How it starts

The opening of the file, as written. The whole thing — 777 lines — stays where its author put it; the contents beside it link to each section on GitHub.

CLAUDE.md — agent orientation

This is a Lean 4 / mathlib formalization of the stabilizer formalism for quantum error correction. The active math is in QEC/. Build with lake build.

Two-repo layout

This repo is the library only — polished, sorry-free Lean on main (mathlib/cslib model). The research program behind it lives in the sibling repo qec-lab (shared pre-split git history; tag archive/pre-split-20260718 marks the split point): the BB distance lab (experiments/bb_lab/), the formalization pipeline (pipeline/, catalog/, the four pipeline agent specs), the narrative docs, and the dashboard. Convention: qec-lab tooling expects this repo checked out as a sibling directory (env QECLEAN_ROOT, default ../QECLean). WIP formalization branches live here (in worktrees), can be backed up to the qec-lab remote (git push lab <branch> works thanks to shared ancestry), and merge to main only when sorry-free. Read qec-lab's CLAUDE.md before any pipeline or research work.

Where to look for what

CLAUDE.md is the small must-read on every invocation. It carries codebase-wide orientation, naming/style policy, layering rules, and build/MCP workflow. Volatile or topic-scoped knowledge lives elsewhere:

  • qec-lab: docs/lean-patterns.md — tactical patterns by code shape (CSS distance, non-CSS distance, parametric families, mechanical fixes). Reach for this when your current code matches one of its sections; add new patterns there when they're code-shape-specific rather than codebase-wide.
  • qec-lab: docs/mathlib-version-quirks.md — mathlib API drift (deprecations, renames, signature changes), grouped by version. Add new entries there when you work around a mathlib version-specific quirk.
  • blueprint/README.md — the LeanArchitect blueprint: what is generated vs. hand-written, how to add a node, how to inspect one with #show_blueprint. Read before editing QECBlueprint.lean or blueprint/. See also the "Blueprint" section below.
  • QECWidgets/README.md — the ProofWidgets-based infoview widgets (#pauli_strip, #toric_chain, #check_matrix, and the expression presenters): what each renders, how meta-level reduction drives them, and the linter rules for adding widget files. Read before editing QECWidgets/.
  • QEC/Stabilizer/Codes/BivariateBicycle/README.md — orientation for the BB family (gross d=12 proof spine, instance dirs, hypothesis-discharge map, engine-vs-analytic status, generated-file manifest). Read before any BB edit. Generated files carry GENERATED FILE — DO NOT HAND-EDIT banners: change the generator (see qec-lab's experiments/bb_lab/GENERATORS.md) and regenerate, landing both repos' changes together — never hand-edit the emitted Lean.

Read the full file on GitHub · 777 lines

Changes

What this file has done since we first saw it

Hashed on every crawl. A supply-chain change to an agent config is a question of when, not whether, so the history is kept rather than the latest state alone.

  1. 4d ago Changed · +11 tokens per session 5b797e84f201
  2. 7d ago Changed · +5 lines · +85 tokens per session 2957eebec739
  3. 20d ago Changed · +16 lines · +335 tokens per session 2d0f22c8ec2a
  4. 25d ago Changed · +15 lines · +338 tokens per session 634125c4ee05
  5. 1mo ago Changed · +5 lines · +103 tokens per session 35f4efb32347
  6. 1mo ago Changed · +1 lines · +30 tokens per session fe0d69383fd9
  7. 2mo ago Changed · +22 lines · +435 tokens per session 52bf2203a591
  8. 2mo ago Changed · +22 lines · +663 tokens per session f50a54bf2159
  9. 2mo ago Changed · +43 lines · +756 tokens per session 86a6e305d805
  10. 2mo ago First seen · 648 lines · 9,093 tokens per session scan C 280597dd0313

Subscribe to this mod's changes

QECLean CLAUDE.md is an instructions file published in the GitHub repository Stavan-Jain/QECLean (48 stars, last pushed 2d ago), licensed Apache-2.0. It adds 11,849 tokens to every session, about $0.0474 per session on Opus 5.5. A static security scan graded it C with 1 finding (recursive force delete). No closer match exists in the catalogue, so it is treated as the original; first seen 2026-08-30.

Related

QECLean CLAUDE.md compared with instructions from other repositories

QECLean CLAUDE.md next to 6 instructions from other repositories
ModTypeStarsLast pushLicenceScanTokensWorks with
QECLean CLAUDE.mdStavan-Jain/QECLeanInstructions file482d agoApache-2.0C11,849Claude Code
vscode buildNext.instructions.mdmicrosoft/vscodeInstructions file195ktodayMITA9,719GitHub Copilot
next.js AGENTS.mdvercel/next.jsInstructions file143kyesterdayMITA7,461Codex, OpenCode
vscode oss-third-party-notices.instructions.mdmicrosoft/vscodeInstructions file195ktodayMITA5,649GitHub Copilot
langchain AGENTS.mdlangchain-ai/langchainInstructions file149ktodayMITA4,680Codex, OpenCode
vscode copilot-instructions.mdmicrosoft/vscodeInstructions file195ktodayMITA3,093GitHub Copilot
vscode ai-customization.instructions.mdmicrosoft/vscodeInstructions file195ktodayMITA1,907GitHub Copilot