# CARBON Proof — bounded first slice Availability: CARBON Pro only (Claude Pro and Codex Studio Pro). Light/Lite packages do not include the command, Lean setup or proof runtime. `/proof` (MCP prompt `proof`, alias `carbon_proof`) discovers consequential code and asks a human what to verify. It is not a whole-program correctness claim. ## Runnable path The native `python-bool` backend implements finite-domain verification of a small total language: pure functions with one Boolean return expression; `and`, `or`, `not`, Boolean equality/inequality, conditionals, Boolean constants, calls to pure functions and explicit sibling-module function imports. Optional `bool` annotations are permitted. No decorators, recursion, loops, mutation, arbitrary imports, arithmetic, external services or other Python values. At most 12 Boolean arguments. Targets must be flat modules in the selected root; nested packages are unsupported. The import-resolution contract requires sibling imports to resolve to the exact fingerprinted source files, not another module installed elsewhere on `sys.path`. The generator interprets the validated AST and supplies every checked input and result. A separate sandboxed checker compiles the original validated function expressions with CPython and evaluates the approved predicate independently. PROVED requires agreement over the complete Boolean domain. This is an exhaustive finite proof under the stated CPython/OS/caller contracts, not a Lean theorem or a claim about arbitrary Python objects. We do not prove that callers pass bools. Example production module `policy.py`: ```python def allow(authenticated: bool, owner: bool) -> bool: return authenticated and owner ``` ```sh CARBON_ANALYTICS=off /path/to/carbon/bin/carbon-runtime proof discover --root /project /path/to/carbon/bin/carbon-runtime proof prepare --root /project \ --target policy.py::allow --property 'not result or authenticated' \ --description 'Authorization never succeeds for an unauthenticated caller' \ --assumption 'Callers pass actual bool values; caller validation is not proved' ``` Prepare returns a spec path and digest, without executing the target. Present both and the proposed limits to a human. After explicit approval: ```sh /path/to/carbon/bin/carbon-runtime proof run --root /project \ --spec /project/.carbon/proof/proposals/DIGEST.json --approved-digest DIGEST ``` CLI cannot prove a human approved something. The host must enforce that interaction; CI must use a separately reviewer-owned digest, not extract it from an untrusted evidence file. A changed property, assumption, budget or input requires new approval. Default proposed limits: 30 wall seconds, 20 CPU seconds, 256 MiB, 1 attempt, 0 AI tokens, 4096 proof cases and 4096 counterexample cases. Lean instead proposes 90 wall seconds, 60 CPU seconds and 1024 MiB to include fresh kernel replay of imported definitions. Those limits are shown before approval, never raised during a running attempt. Hard allowed maxima are validated in the runtime. One deterministic candidate is attempted; unused attempt allowance is never spent automatically. AI search is intentionally disabled, not silently unmetered. Generator and checker share a deadline conservatively capped at CPU seconds. Resource exhaustion produces UNPROVED, with remaining search gaps. Native isolation requires an existing macOS `sandbox-exec` or Linux `bubblewrap`. No writes, network or child processes are permitted in the macOS worker. Linux uses read-only mounts, network/PID namespaces, CPU/address-space rlimits. macOS memory is a **sampled RSS watchdog**, not an exact hard allocation cap; a process can briefly overshoot between 25ms samples. Static AST/domain/output bounds also apply. Environments requiring strict cgroup-style memory accounting should use the Docker Lean path or add a separately reviewed native container runner. Missing isolation fails closed. ## Lean model backend Local `/proof` includes a setup check by default. Run `carbon-runtime proof setup` to detect the toolchain, then `carbon-runtime proof setup --install` after approval of the download and local build. Setup downloads Lean 4.28.0 from leanprover's official GitHub release, verifies the archive SHA-256, and builds a local image with Lean and its included `leanchecker`. No account, API key or paid service is required. It supports Linux arm64/amd64 containers on a local Docker unix socket. The approximately 500 MiB download and several GiB disk use are setup costs, not part of the proof-search budget. Builds time out after 20 minutes. Start a local Docker-compatible runtime first; CARBON does not install privileged host software. Use the returned immutable image ID with `--backend lean-bool-model --lean-image sha256:DIGEST`. A preinstalled repository digest (`NAME@sha256:DIGEST`) also works. The image digest pins the toolchain, Init and checker dependencies. Resolve it before preparing the approval specification. A changed image needs new approval. Verification runs never download, install, start Docker or request credentials; missing setup produces UNPROVED with a setup instruction. Native-only verification does not require Lean. Setup does not approve or execute a proof. The trusted translator creates a closed Boolean formula with synthetic identifiers, explicit `Init.Data.Bool` and `Init.Tactics` imports (no implicit full `Init`), a fixed `by decide` proof and `#print axioms carbon_property`. No user Lean text, tactic code, dependency modules or binary proof artifacts are accepted. The candidate is regenerated and byte-compared by the independent checker; a weaker theorem or unfinished proof is rejected even if someone recomputes its hash. Two isolated builds are performed, followed by `leanchecker --fresh Proof` in the second environment. Both must report **no transitive axioms**. `sorryAx`, custom axioms, `Lean.trustCompiler` and native evaluation axioms cannot be approved here. Containers have no network, read-only root/input, unprivileged user, dropped capabilities, CPU/memory/PID limits and bounded tmpfs. Generated containers are removed even after timeout. Generator/checker errors cannot become PROVED. The theorem concerns the **Lean model only**. Finite CPython replay is additional evidence, not a machine-checked Python-to-Lean equivalence theorem. Trust remains in the approved toolchain, parser/translator, kernel/checker, operating system and the human's intended specification. Lean integration tests skip explicitly unless `CARBON_PROOF_LEAN_IMAGE` names an existing approved digest-pinned image. Reference: [Lean proof validation](https://lean-lang.org/doc/reference/latest/ValidatingProofs/). ## Failure, evidence and freshness When the property fails or the proof-case budget is insufficient, deliberate counterexample enumeration searches the same domain under its own case allowance. Failures are deduplicated by input, sorted by fewest true values then lexicographically, and independently reproduced. Minimality is global only when that full domain was searched. Multiple inputs for one property are **not** claimed as multiple bugs. Use separate approved properties/targets for distinct failures. COUNTEREXAMPLE records include an executable regression fixture: ```sh /path/to/carbon/bin/carbon-runtime proof regression --root /project \ --fixture /project/.carbon/proof/runs/RUN/regression.json ``` It exits nonzero while the property violation remains. It deliberately checks the restricted production semantics, not a fake expected-success model. Unsupported semantics and exhausted execution budgets can prevent counterexample execution; report that gap, not an invented reproducer. The approval fingerprints **every file in the selected root**, including dependency source, lockfiles, contracts, specifications, build flags/configuration files, plus the exact spec/budgets, interpreter version/binary/platform, standard-library source and extension-module hashes, and trusted verifier files. System libraries/OS remain explicit environment assumptions, not a proof of the runtime implementation. Only Git metadata, Python bytecode caches and `.carbon/proof/` evidence are excluded; none may contain verification inputs. Symlinks/external dependencies are unsupported. 1000-file/8-MiB bounds fail closed instead of silently sampling. Choose a truly self-contained verification root; do not trim away relevant dependencies to fit. Run on a hash-verified snapshot, then recheck original fingerprints after validation. Proof artifacts have separate hashes and are independently replayed, not trusted. Records under `.carbon/proof/runs/` are append-only by unique run ID and include commands, logs, exact property, limitations, hashes, bounds and replay command. Keep them private. The normal CARBON four-view HTML renderer is reused beneath the excluded proof directory, so generating a report cannot invalidate its own inputs. Every discovery, proposal, run, recheck, CI check and regression replay returns a `report.reportPath` and report URL. The dark CARBON HTML report includes what ran, the exact rule, findings, observed counterexamples, approved resource limits, recorded runtime, independent replay coverage, next actions and evidence links. It never substitutes a confidence percentage for a verification state. If the full report renderer fails, a self-contained, offline dark CARBON report is generated instead. Invalid inputs also receive a stopped-attempt report when the supplied project directory is writable. Setup-only operations return setup status, not a proof report. Report generation does not approve targets or modify evidence. ## Incremental CI Check only a reviewer-approved list, never launch unbounded repo-wide search: ```sh /trusted/carbon/bin/carbon-runtime proof ci --root /project \ --approvals /protected/approved-proof-records.json ``` The protected JSON is a list of `{ "record": "/path/evidence.json", "approvedDigest": "human-reviewed-digest" }`. Store it outside the verified project closure (or in the excluded proof directory with independently enforced CI review permissions). The trusted checker must be installed/read-only outside the proof agent's writable checkout. Ordinary local files cannot protect against an unrestricted same-user agent. A stored PROVED label is never used as CI evidence: unchanged approved records are replayed; changed inputs return STALE and fail CI. Re-prepare, re-approve and recheck affected targets. Unknown/unsupported/budget failures also fail CI. The conservative closure may invalidate unrelated edits; this favors safety over minimal rebuilds. This check says nothing about unselected properties or the rest of the program. New language-native backends must implement isolated generation, independent fixed-property validation, counterexample reproduction and complete input closure before they may emit PROVED; they cannot simply set a status field.