Strict impact🔗

Every rule's findings are errors under a strict claim. An established violation makes the result FAIL; missing or unsupported evidence makes it INCOMPLETE. Neither is accepted. lake lint exits with 0 ACCEPTED, 1 VIOLATION, 2 INVALID CONFIGURATION, 3 INCOMPLETE; it exits 2 when every finding of a FAIL is RG2002. The editor shows a rule's local findings as warnings (errors under warningAsError); they are not project results, and the rule pages say which rules the editor reports.

No local exception🔗

No source option, attribute or command-line flag makes a rule pass on a claimed surface. set_option linter.regula false and regula.localFoundation never waive a rule: lake lint, the build-lint policy target and axiomGate still apply it. Where Regula's local linter reports a finding during a project build (axiomGate and the policy target keep it on by default; lake lint builds with it off, whatever the source sets linter.regula to), that finding is a build warning, so the result is INCOMPLETE under RG2003 instead of carrying the rule's finding. Switching the local linter off changes which finding is reported, never whether the result is accepted. Hiding a diagnostic does not establish the property it checks. RG5002 and RG5003 check the declarations registered with @[regula_material]; removing a registration changes the reviewed claim, not only their result.

Where rules run🔗

Project enforcement runs through lake lint (incremental), lake lint -- --fresh and lake exe axiomGate (fresh whole-project audits from empty build output), and the build-lint policy target; lake exe docFenceAudit audits documentation examples. Each rule page lists where the rule is reported. See the adoption guide.

How a finding reads🔗

The first line of every finding has the form {rule} [{impact}; {mode}; claim={claim}; {location}]: {subject}: {detail}. The finding then gives the rule's remedy and ends with the rule's page in the reference of the installed Regula version, and lake exe regula explain <ID> prints the full rule offline.

Open review obligations🔗

Every accepted result lists every review obligation below as open, whatever rules it checked (R-GRAPH only for a serialized-graph claim). A listed identifier is an open obligation, never a completed review. Each rule page names the obligations its own result leaves open, and checklist coverage the checklist rows whose review each carries.

• R-INTENT: each material proposition and its explanation match the written intent in its declaration's Intent section: quantifiers and their order, hypotheses, domains, existence or construction, conditional or open status, and limits. No proof or presence check discharges it, and the requirement owner confirms that the intent states what is needed.
• R-INVARIANT: the intended invariants (admitted values, transitions, frames, reachability and composition) are stated, and every admission, write and caller path is covered by a proof-bearing interface or theorem.
• R-LAWS: the chosen structures and instances carry the intended algebra or order, and custom definitions are justified.
• R-BOUNDARY: the enforced abstraction boundary is the intended one: module modes, exported constructors, recursors and projections, coercions, equations and actual callers.
• R-NONVACUITY: the claim is non-vacuous at the strength claimed (inhabitance, joint satisfiability or reachability); a conditional or deliberately empty claim needs no unrelated witness.
• R-DOC: material-claim registration is complete, and module documentation and docstrings are faithful to the declarations and requirements; presence or length alone is not enough.
• R-COST: a cost claim names its domain and rests on a mathematical argument or a bounded observation that preserves semantic and effect order; no timing or sample is universal evidence.
• R-QUALIFY: the checker's detection is qualified for this invocation, toolchain and capability: claim-scoped positive controls, intended-reason mutations and exact invocation evidence.
• R-GRAPH: a claimed serialized graph (freshChecker, standard §7.9) covers every selected root.

Trusted mechanisms🔗

Every accepted result also relies on these trusted mechanisms (the checker's Trusted account), which no rule verifies:

• toolchain: Lean elaborator, kernel and compiler at the snapshot's toolchain identity
• acquisition: manifest parsing, Lake loading, and source, configuration and dependency acquisition
• extraction: environment extraction, compiler and worker processes, and JSON transport
• runtime: native runtime and every execution boundary reported as trusted

Checked examples🔗

Each rule page's example was produced for the page's commit by the rule-example corpus campaign, admitted by the rule-example qualifier (whose admission relations are proved; capture and process authenticity are trusted), and checked against the commit's checker, corpus and configuration sources before the site was generated. The site build refuses stale, incomplete or partial evidence. The campaign is scoped qualification of the detectors for these inputs, not a proof that the detectors are correct for every input.

• Checked policy rejection: the violating input was completed by the checker and rejected with the findings below; the corrected input passed a completed positive check.

• Diagnostic demonstration: the violating run is INCOMPLETE by design. It shows the exact diagnostic and is not accepted negative evidence. The corrected input passed a completed positive check.