docs/formal-verification.mdView on GitHub ↗

Lean-checked commerce contracts

The current source runs Lean 4.29.1 proofs for 45 policies used in production Rust paths, with 97 named properties. This is not a certificate that the entire commerce core is correct or bug-free. The cognitive-commerce review contains 414 Rust modules: one extracted policy module, 43 reviewed binding modules, one comparison driver and 369 unproved modules. Binding review is not a proof of those modules. The manifest and per-revision CI artifact are the authoritative inventory. Local compiled conformance compares 142,298 cases without mismatches; the current required negative mutation suite must also pass before landing.

The published verification report is copied from the completed merged-Core CI run 37868239729, recording source 598bbec112165fcac1847797786e2ba5c606e06f. It includes the compiled conformance result and exact source inventory. Later documentation edits do not extend its proof scope. Release acceptance and measured gaps.

Connection to the real application

HTTP / MCP / storefront
        ↓
Production Rust operations → src/verified_kernel.rs
                                      ↓ closed typed extraction
                              Commerce/Generated.lean
                                      ↓
                               Claims.lean → Lean kernel
                                      ↓
                            compiled-environment recheck
                                      ↓
                                transitive axiom audit

The application calls the Rust functions directly. There is no separate handwritten Lean implementation of their behavior. scripts/formal/extract.py accepts only bool/u64 arguments/results, literals, comparisons, Boolean operators, min and saturating_sub. It rejects unsupported syntax instead of silently approximating it. Lean Nat subtraction saturates at zero, matching u64::saturating_sub; this subset cannot overflow through addition/multiplication because those operators are excluded. Claims quantify over all natural inputs, including all representable u64 values.

The extractor is a trusted, tested translator, not a verified Rust compiler. Correct production input conversion and surrounding state handling remain part of the reviewed boundary. Finite conformance checks strengthen that connection; they do not prove the translator correct for every program.

Exactly what is proved

Production policy	Lean guarantee	Actual consumer
`discount_cap`	Discount is bounded by both requested amount and goods total; remainder plus discount conserves the total	`src/discount.rs`
`stock_admissible`	Admitted quantities are positive, within stock and conserve stock under subtraction	`src/order_checkout.rs`
`refund_admissible`	Prior/reserved plus requested refund cannot exceed captured amount; zero refunds fail	`src/payments/operations.rs`
`revision_admissible`	Admission requires an exact positive revision	`src/commerce/fulfillment.rs`
`replay_admissible`	A replay belongs to the same cart; an open cart requires the same fingerprint	`src/order_checkout.rs`
`scope_admissible`	Admission requires authentication and a known scope; explicit denial cannot inherit role defaults	`src/auth/permissions.rs`
`order_edit_admissible`	Terminal orders cannot admit operational edits	`src/commerce/order_workflow.rs`
`completion_admissible`	Completion requires payment ready, deliveries complete and a nonterminal order	`src/commerce/order_workflow.rs`
`cancellation_admissible`	Cancellation requires open deliveries and no external payment/refund constraint	`src/commerce/order_workflow.rs`
`manual_payment_admissible`	Manual payment cannot confirm an external provider; it requires a pending payment and nonterminal order	`src/commerce/fulfillment.rs`
`download_admissible`	Blocked orders grant no download; admitted downloads require payment or explicit simulated authorization	`src/assets/download.rs`
`checkout_review_admissible`	Exact revision and amount equality plus confirmed methods are required when a client supplies the review headers	`src/order_checkout.rs`
`checkout_contact_admissible`	Financial checkout requires email and billing data; simulated checkout has an explicit exception	`src/order_checkout.rs`
`receipt_admissible`	Accepted provider receipts match amount and currency and confirm the outcome	`src/payments/receipt_guard.rs`
`platform_admissible`	Operator access requires a personal identity, active grant and account	`src/platform/auth.rs`
`app_read_admissible`	Read aliases admit declared read-only, non-mutating handlers	`src/apps/surfaces.rs`
`rule_authenticated`	A guest cannot satisfy the authenticated-customer condition; both Boolean branches match exactly	`src/marketing/rule_match.rs`
`rule_boolean_comparison`	Equality, inequality and emptiness select the exact Boolean result	`src/rule_comparison.rs`
`app_flow_admissible`	Only explicitly eligible private mutation actions can be flow targets	`src/marketing/app_flows.rs`
`rule_xor_count`	XOR matches exactly one child; no matches cannot satisfy it	`src/automation_rules/evaluation.rs`
`flow_delay_admissible`	Durable delays are positive and at most thirty days	`src/marketing/pipeline.rs`
`destination_tax_admissible`	Condition, country, state, postcode and date guards must all match	`src/commerce/tax_rules.rs`
`customer_group_net`	Net basis requires a configured business group; unknown groups cannot claim it	`src/commerce/customer_groups.rs`
`app_tool_admissible`	Tool admission requires explicit enablement and current authorization	`src/apps/gateway.rs`
`app_core_reference_admissible`	Product references may be public; customer/order references require private data	`src/apps/editor_contract.rs`

| shop_request_admissible | Active shops admit requests; paused shops require an admitted read; archived shops deny ordinary operations while settlement callbacks remain available | src/platform/lifecycle.rs |

Every policy also has an exact acceptance theorem. This proves that valid inputs are accepted as well as unsafe inputs rejected; replacing a policy with false (or a discount cap with zero) fails. These are contracts on supplied facts, not proofs that database/network adapters obtain those facts correctly.

The proof statements and source inventory are the precise scope. For example, the discount cap theorem does not prove the complete tax/rounding/distribution algorithm, and stock admission does not prove transaction isolation. Authentication is supplied by the middleware; the theorem does not prove that middleware or the older aggregate read permission path. Provider receipt identity/signature checks and their parsers remain outside the pure theorem.

consent_admissible admits exactly an enabled purpose with a current, fresh, affirmative receipt; production consumers check it while holding the actual receipt/settings locks. legal_checkout_admissible admits non-strict demo mode, or current accepted documents and, when immediate consumer digital supply is requested, separate approval. Their exact Boolean equivalences cover every assignment, with mutations that remove current/fresh/affirmative/waiver checks. These statements do not prove the legal adequacy of texts, identity verification, retention, product claims, SQL isolation or email delivery. The real HTTP tests verify selected adapter behavior. See European operation.

Verification that runs on every push and pull request

The existing Verify prototype / verify job now also:

Checks generated artifacts match the production Rust policy source exactly.
Requires every Rust module to be classified and checks full-file review hashes. Schema migrations, embedded source SQL, Cargo/frontend build files, Dockerfile, proof claims, extraction/audit scripts and the verification workflow require an explicit recorded review after changes.
Builds proofs with the pinned Lean toolchain and rechecks compiled declarations using bundled leanchecker.
Audits all required theorems' transitive axioms. Only Lean's standard propext, Quot.sound and Classical.choice foundations are allowed. sorry, admit, custom axioms, native_decide and missing theorem audits fail.
Executes compiled Rust and Lean functions on 6,227 identical inputs: exhaustive Boolean assignments plus numeric boundaries/random cases, including u64::MAX. Their output types and values must match.
Requires Lean to reject 98 deliberately broken policy variants. Also rejects 14 unsupported grammar examples, three stale/unclassified/disconnected inventory cases and nine proof-shortcut/axiom/missing-audit examples.
Runs existing Rust, PHP-reference and real PostgreSQL HTTP regressions.

CI never regenerates the policy model or refreshes review hashes automatically. It uploads formal-verification-<commit> JSON evidence, including explicit entireCoreProved: false. A green check represents these checks on that commit, not a whole-system certificate. Required branch checks prevent ordinary merges before verification succeeds; changing the checks or their contracts remains a review responsibility.

Local verification and intentional changes

Requirements: existing Rust/Python toolchains plus elan. The pinned version is in proof/lean-toolchain; no Mathlib dependency is needed. Install the Lean toolchain once, then run from the repository root:

elan toolchain install leanprover/lean4:v4.29.1
python3 scripts/formal.py
python3 scripts/formal/mutations.py

When deliberately changing a policy, update its contract and actual consumer, review the generated diff and run the relevant HTTP regression. New pure critical decisions should enter this subset or use a documented stronger extraction approach; do not mark async/SQL/provider code as proved.

python3 scripts/formal.py --generate --record-review 'Explain the reviewed behavior, affected contracts and regression evidence'
python3 scripts/formal/mutations.py
cargo fmt --check
cargo clippy --locked --all-targets -- -D warnings
cargo test --locked

--record-review records changed file hashes; it cannot turn unproved code into proved code. Review the manifest diff. Do not refresh hashes to suppress a failure whose cause you have not investigated. Proof changes must not weaken an existing business guarantee merely to accept a broken implementation.

What remains open for the entire core

Database concurrency/isolation, tenant ownership in SQL, allocations and rounding, full configurable workflows and flows, network/provider behavior, extension execution, frontend code, operating system dependencies and AI model outputs are unproved. They keep their existing behavioral tests and review locks. The terminal-state integration already closed a real gap: direct HTTP payment and delivery edits now fail for completed orders and app-defined terminal states; regressions verify the persisted revision remains unchanged.

The next meaningful expansion is extracting complete integer money/tax and reservation state-transition modules, specifying their overflow bounds and proving the actual update operations. For a larger safe Rust subset, Aeneas is a possible next extraction layer; its Rust coverage and concurrency limits must be assessed against the real code. It is not installed or used by this proof pipeline. Full-system correctness requires substantially more specification and proof work, and depends on what properties have actually been specified.

For Lean's trust model and axiom limitations, see the primary documentation: proof validation and axioms.

Connected-app rule contracts

Three additional extracted policies have production consumers: rule_authenticated uses actual authenticated customer presence, app_flow_admissible admits only explicitly eligible private mutation actions, and rule_boolean_comparison selects supported equality/inequality/empty semantics. Five Lean properties state exact behavior and reject granting the logged-in branch to a guest. The original string, Unicode conversion, wildcard matching, UUID comparison input construction and the surrounding rule AST evaluation remain reviewed/tested Rust, not fully proved modules. Provider OAuth, encrypted storage, Gmail/GA4 imports, Slack delivery and private graph projection remain unproved integration code with real local HTTP/database regression coverage. No whole-core or bug-free certification is claimed.

The platform operator grant is also production-bound: personal credential, current grant and active status must all hold. The surrounding session lookup, SQL, offline bootstrap and provisioning are reviewed/tested adapters, not Lean-proved database or deployment correctness.

The app GET policy proves admission from declared metadata; it does not prove an external service is actually side-effect-free. See the full app boundary.

The automation increment additionally extracts exact XOR hit-count admission and the thirty-day durable delay bound. Three new properties and negative mutations protect those production decisions. The rule interpreter, calendar parsing and SQL/async flow runtime remain unproved; automation defines their actual test and migration boundaries.

Destination tax guard and translation apply (2026-10-05)

The production destination_tax_admissible function requires all five condition, country, state, postcode and date guards. Its exact Lean theorem accepts precisely that conjunction; all 32 Boolean assignments are compared and each individual guard bypass is rejected as a mutation. The native tax resolver consumes it. This proves the combined Boolean admission, not fact extraction, tax priority, rounding, current tax law or correctness of database configuration. Translation apply consumes the existing exact revision_admissible policy; stale product edits conflict. SQL row locks and provider output validation remain reviewed, unproved adapters with real PostgreSQL regression tests.

Channel settings, method dependency guards and image drafts (2026-10-05) add reviewed JSON/SQL/provider/MCP adapters around the existing validated checkout and revision policies. Sparse transport patching and deletion reference queries are not new extracted Lean decision policies. Provider output decoding, publication transactions, queue processing and UI behavior remain unproved; real isolated regressions and the exact source-review inventory document their scope. See settings/media.

Connected CRM and history (2026-10-05)

customer_group_net is extracted from production and consumed by commerce/customer_groups.rs. Its exactness property admits net presentation iff a group exists and explicitly selects the business basis; an unknown group cannot self-claim business presentation. Both Boolean input guards have negative mutations and exhaustive compiled Rust/Lean comparisons.

Entity snapshot triggers, actor attribution, restoration transactions, group dependency queries and frontend controls are reviewed unproved adapters. Their real HTTP/PostgreSQL and component regressions are documented in entity history. This does not certify whole-core correctness.

App assistant access policies (2026-10-05)

Two production-bound decisions add four theorems: MCP tool exposure requires both explicit enablement and current action authorization; customer/order core references must be private, while product references may be public. The real MCP ingress and manifest validator consume these functions. The async scheduler, HMAC parser, SQL receipt transactions, native renderer and provider integrations are not proved. Real disposable PostgreSQL/HTTP tests cover owned references, team scopes, MCP opt-out, webhook-to-flow effects and cold-restored cron/replay receipts.

The checkout review theorem covers the exact pure admission predicate. Header parsing, SQL/cart pricing, provider jobs and the browser remain unproved adapters. Real HTTP tests reject stale/partial/malformed reviews without orders or stock writes and preserve committed-order replay. See checkout.

The provider extension adds reservation_release_admissible: only uncaptured attempts or a provider-confirmed voided authorization may restore stock. Exact and negative properties are extracted from the live Rust consumer. Provider receipt authentication, ownership SQL and async jobs remain outside Lean.

Production boundary increment

Three further extracted decisions add seven properties: currency_scale_admissible limits decimal precision, resource_quota_admissible admits positive bounded operator limits, and payment_transition_admissible defines the monotonic ledger graph, including late capture. src/money.rs, src/platform/quotas.rs and src/payments/state.rs are their real consumers. The reviewed manifest now has 34 policies and 72 named theorems; compiled Rust/Lean comparisons and negative mutations remain required. These proofs do not cover signed integer parsing, floating-point conversion, SQL hooks/transactions, provider evidence, or the whole server. Architecture and executable checks.

Rust notification runtime

notification_retry_admissible is extracted from the actual delivery worker: only an explicit HTTP 429 rejection before attempt eight permits a provider retry. Exact and ambiguous-result properties plus mutations protect this rule. Configuration locks, SQL claims/leases, SMTP/TLS, OAuth and external provider evidence remain unproved adapters with real integration regressions; the runtime is not wholly Lean-certified.

Private app transport admission (2026-10-07)

The production app gateway consumes app_service_transport_admissible. Three named properties establish the exact decision, rejection of an unapproved private HTTP origin and rejection of URLs with unsafe components. The URL adapter compares scheme, host and port against an operator-owned allowlist; real URL cases reject lookalikes, alternate ports, credentials, queries and fragments. HTTP redirects remain disabled in the shared client. Mutation checks reject dropping the clean-URL guard or admitting every private destination.

These properties prove the extracted Boolean decision. URL parsing, DNS, hosting network isolation, HTTP/TLS execution and service authentication remain reviewed and tested adapter boundaries, not Lean proofs. See Rust services for the private hosting configuration.

Multi-currency admission (2026-10-07)

currency_context_admissible is consumed by src/currencies/model.rs: only a configured, channel-enabled currency with an admitted saved rate may be selected. Exact Boolean equivalence and stale-rate rejection brought the then-reviewed manifest to 35 policies and 74 named properties. Explicit mutations bypassing availability or freshness must fail. Rate retrieval/date parsing, rational FX, float taxation, job transactions, currency ledgers, UI and provider behavior remain outside these Lean proofs and are covered by separate unit/real integration checks. Currency architecture and verification scope.

Channel admission (2026-10-08)

channel_access_admissible is consumed by src/marketing/channel_access.rs. Four named properties cover exact admission, private-channel identity, paused-channel preview requirements and preview mutation denial. The current manifest contains 36 extracted policies and 78 properties. Core HTTP/MCP/UCP and hosted request paths share this admission adapter. One-use preview grants, cookies, membership queries, hostname resolution, proxy transport and native rendering remain unproved adapters exercised by isolated integration regressions. Channel management and security limits.

Native public asset admission (2026-10-08)

native_asset_bypass(native_asset, hosted) is called by the actual authentication middleware. Two added theorems prove exact acceptance and unconditional denial when hosted; negative mutations remove each required fact or reject all inputs. The resulting manifest has 37 policies and 80 properties. This proves the Boolean rule, not native-path classification, layer ordering, domain resolution, SQL MVCC, proxying, compression or browser behavior. Real hosted/private-asset and two-replica regressions cover those adapters, including gzip/Brotli negotiation, ranges and uncompressed credential-bearing responses. Embedded .sql and build inputs are now explicitly review-hash locked to prevent silent adapter drift.

Cognitive decision contracts (2026-10-09)

Four new extracted policies are consumed by the native cognition owners: ai_price_admissible checks the supplied corridor, margin, discount, brand and availability guards; ai_autonomy_admissible requires explicit enablement, current authority, price-only scope and both budgets; claim_render_admissible requires confirmed, public, current, valid-time exact statements; and experiment_result_admissible requires an admissible final look, enough units and a positive lower bound. Nine named properties include exact acceptance and negative cases. This proves those predicates, not price cost/tax input correctness, source entailment, signature implementation, SQL locking or statistical assumptions. Connected implementation and open audit scope.