English source · 15 min

Lean-checked commerce contracts

The current source declares 63 extracted policies used in production Rust paths and 150 named properties. This is not a certificate that the entire commerce core is correct or bug-free. The reviewed inventory contains 713 Rust modules: eight extracted policy modules (including the facade), 63 reviewed binding modules, one comparison driver and 641 unproved modules. Binding review is not proof of the surrounding modules. The manifest and per-revision CI artifact are authoritative. The operational-record exclusion remains part of the generic app release policy. The original compatibility experiment and its dated evidence are retained on the separate branch; its original PHP runtime is outside this proof scope. The earlier published CI evidence below retains its own date and counts. The 23 October local and Linux CI verification compare 156,741 compiled Rust/Lean cases without mismatches and reject 183 deliberately broken policy variants. Exact local results and module audit. Local verification and the clean-checkout CI evidence are recorded separately. The later discount arithmetic repair adds one Rust regression module. It retains the same extracted policies and properties; it does not turn the allocation loop into a Lean proof. The complete required Linux CI passed before both PR #206 and the later arithmetic repair in PR #209 merged. Latest CI and public rollout.

The published verification report is copied unchanged from the successful complete Linux CI run 39953688161, recording clean source 429cdf040e3a26eaf0613cbfc0325b0a746ce08d. Its complete source tree matches PR #209 commit 467fc5fd and merged main 363181dd. The mutation results come from the same CI artifact. The reports include compiled conformance, axiom audit and exact inventory; later documentation or stylesheet edits do not extend their proof scope. Current product and public acceptance.

Connection to the real application

HTTP / MCP / storefront
        ↓
Production Rust operations → crates/kernel/src/verified_kernel.rs → seven policy domains
                                      ↓ closed typed extraction
                              Commerce/Generated.lean
                                      ↓
                       Claims/<Domain>.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 loads the exact reviewed module registration, then 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.

Domain modules and sequential guarantees

The Rust facade explicitly reexports seven small policy modules: access, agents, apps, automation, commerce, fulfillment and intelligence. The corresponding seven Lean modules independently import the extracted model. Each theorem must appear in the manifest and the stable Claims.lean entry must import every domain. The extractor rejects extra code, conditional registrations, path overrides and wildcard reexports in the facade. Each handwritten proof module is limited to 320 lines; the current largest is 240. The 61 policies that preceded this split retain identical typed expressions, argument types and results.

The 18 added properties cover two kinds of real guarantees:

• Repeated commerce decisions: two admitted reservations conserve stock; successive refunds remain within the captured amount; successive allocations remain within the budget, including after lowering its limit. The shared budget predicate is used by B2B spending and central agent token/cost allocation. Discounts remain monotone and applying the same cap twice changes nothing.
• Saved agent work: planning credentials admit only requests classified as reads or explicit planning operations. A private continuation requires an active shop, personal session, matching owner and current preview. These are the actual predicates called by agent_runs/controls.rs and agent_runs/authority.rs.

Sequential arithmetic assumes each operation observes the latest serialized state. SQL locks, route classification, authentication and the clock remain adapter facts, verified separately by native integration tests rather than proved by Lean.

Exactly what is proved

These last two properties constrain source snapshots. They do not verify tax law or authenticate a marketplace's payment assertion. The import adapter rejects negative signed amounts before calling the guards; checked addition and provider review remain tested boundaries. See marketplace integration.

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 and legal checkout additions

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:

1. Checks generated artifacts match the production Rust policy source exactly.
2. 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.
3. Builds proofs with the pinned Lean toolchain and rechecks compiled declarations using bundled leanchecker.
4. 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.
5. Executes compiled Rust and Lean functions on the per-revision population of identical inputs: exhaustive Boolean assignments plus numeric boundaries/random cases, including u64::MAX. Their output types and values must match.
6. Requires Lean to reject the registered deliberately broken policy variants. Also rejects 14 unsupported grammar examples, three stale/unclassified/disconnected inventory cases, nine proof-shortcut/axiom/missing-audit examples and ten proof/module-layout bypasses. The Cargo boundary check additionally rejects 17 dependency/owner bypasses, including aliases, optional dependencies, build scripts and targets placed in another domain's directory.
7. 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 --workspace --all-targets -- -D warnings
cargo test --locked --workspace
python3 scripts/testing/workspace_boundaries.py

--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. crates/commerce/src/money.rs, src/platform/quotas.rs and src/payments/state.rs are their real consumers. This increment brought the then-reviewed manifest to 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 manifest at this increment contained 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. That increment brought the manifest to 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.

Partial packages and carrier intent admission — 14 October 2026

The app-independent fulfillment leaf contains strict positive-subset allocation and open/nonterminal/unlabelled package intent admission. An occupied parcel admits only its identical current intent. Native reserve/release, split and dispatch checks keep unknown carrier effects fenced; an original document acknowledges that intent. Explicit boolean properties, compiled conformance and mutants exercise these pure bindings. Transaction locks, allocation-digest construction, app/provider honesty, PDF storage, OAuth, cancellation and external charges remain tested or open boundaries, never whole-system mathematical claims. Shipping workflow.

Reviewed Admin order payment admission — 14 October 2026

The final native checkout quote is checked by admin_payment_admissible before entering any external payment-provider branch. Two extracted properties establish exact acceptance and denial of external payment modes for an Admin order. The actor-private cart adapter, current compound permissions, settings/channel/customer lock order and immutable purchase bindings remain reviewed/tested Rust/SQL boundaries. They are not mathematical consequences of this Boolean policy. The real isolated HTTP regressions and browser walkthrough are described in Admin workflows.