Formal Verification for Harness Engineering in Quantitative Finance

This repository is the source and artifact tree for the long-form paper:

Formal Verification for Harness Engineering in Quantitative Finance

The work develops a contract-relative, machine-checked reference model for finite traces of a harness that qualifies a bounded financial policy, binds the result to exact program bytes, promotes only those bytes under an explicit authority root, and mediates a modeled stateful local effect. The Rust FinGate service is a separately tested local mediator, not the executable realization of the Lean theorems. The canonical manuscript is paper/main.tex.

flowchart LR
    A[Untrusted proposer<br/>arbitrary history] -->|strategy text| G[FinCore gate<br/>verify iff contract]
    G -->|exact accepted bytes| P[Promotion<br/>receipt + one-shot capability<br/>expiry and nonce checks]
    P -->|unique active artifact| D[Derived-risk gateway<br/>strict tag-103 decode]
    S[Signed account/market snapshots<br/>sequence-advancing] --> D
    D -->|request in evidence domain<br/>else fail-closed| E[Decoded-artifact verdict<br/>proved = root reference decision]
    E -->|Allow| R[Atomic reservation<br/>filled + working within caps]
    R --> L[Signed lifecycle envelope<br/>dual promotion-generation nonces]
    L --> T[Finite-prefix traces<br/>reservation invariant holds]
    S -. signature and external-fact<br/>premises, not theorems .-> T

Loading

The evidence is intentionally layered:

1. an auxiliary generic bounded-contract lane proves exact finite checking equivalent to its completed, contract-relative semantic condition and instantiates the result for bounded Markowitz optimization; no instantiation or refinement connects this lane to the central FinCore theorem;
2. the FinCore gate and authority lane parses a total, effect-free typed expression language, checks complete static resource dimensions and root-owned finite scenarios with reified (serializable) postconditions, proves verify = true equivalence to its exact contract, and lifts it into versioned promotion authority with canonical root identity proved from an injective codec — no registry oracle;
3. the derived-risk causality lane: the live gateway decodes the exact promoted tag-103 bytes and executes that artifact's policy on every admitted order, fail-closed outside the root-owned finite evidence domain, with the decision proved equal to the root reference decision on that domain — the promoted artifact is the demonstrated decision authority, not provenance;
4. the finite-prefix composition lane: dual-authority signed envelopes bind both promotion generations (strategy and risk), replay and stale generations are rejected, and from the exact zero genesis every valid finite-prefix trace preserves the reservation invariant; and
5. an auxiliary stochastic bridge: under a reference mark, the marked value of the filled book minus its stored commitment is exactly the inventory's price drift, and instantiated with discounted geometric Brownian motion under the pinned library's equivalent martingale measure, the marked discounted value is a martingale whose expectation equals the book's discounted value at reservation time. These results are not dependencies of the central trace theorem.

The Rust FinGate mediator is a separate implemented lane. It exercises receipt, authorization, exact-byte promotion, runtime revalidation, and a local intent and order-lifecycle journal. It shares fixtures with Lean but is not proved to refine either Lean development. Keeping those boundaries explicit is part of the proposed reference foundation, not a deferred footnote.

Evidence status

Workstream	Confirmed in the repository	Scope and boundary
Generic bounded-contract Lean lane	Exact exhaustive checker equivalence; conditional binding results; bounded Markowitz Optimal or Infeasible interface, ties, the 216-input family, and the exact continuous optimum (18/41, 18/41, 5/41) with value 45/41, derived from a checked polynomial decomposition	Contract fidelity, implementation refinement, and independent formal/finance review remain outside the theorem
General FinCore gate and authority	Strict canonical S-expression parsing for a total effect-free AST; complete parseCanonical (canonical e) = some e with form-decoder and wire-text component laws; regression theorems for empty/singleton vectors and one/two-field records after repairing decoder precedence; Boolean, bounded integer, money, price, quantity, timestamp, product, option, vector, record, tagged-result, conditional, and bounded-fold forms; checked dimensional multiplication (Price x Quantity -> Money with matching instrument/width and declared positive lot factor), ill-typed dimension rejection, and overflow failure; root-owned vocabulary, finite scenarios, artifact/fuel/bit-width/scale/lot/vector/fold caps; verify_iff_contract; exact-UTF-8 receipt/capability binding; one-shot promotion; independent root rotation; no-inheritance and adaptive-proposer results	The semantic theorem is relative to the root's nonempty finite scenario list and postconditions. The codec theorem is internal to FinCore; no source-language/compiler/runtime refinement or Lean--Rust bridge is claimed
Specialized exact-byte pre-trade slice	Three compile-time artifacts and three typed requests; injective exact decoder; candidate A accepted, field-distinct candidate B accepted because it agrees on the frozen domain, and quantity mutant rejected; checked arithmetic fails closed	This closed qualification slice is an independently concrete finance instance; agreement on three requests is not global semantic equivalence
Continuous publication theorem	From the exact zero genesis, every valid continuous finite trace yields the final continuous invariant; the theorem furnishes local-effect soundness and exact producing-event factorizations for each archived dispatch, and recomputation witnesses with analogous origins for each non-reserved attempt. The audit fixture is nonvacuous: two non-reserved attempts and one guarded dispatch. Active final states therefore inherit the reservation caps.	Single-account, single-instrument, two-slot, buy-side, sequential atomic reference specification. The risk root remains unrotated with its active binding retained, although monotone clock advances are permitted, except for an optional fully-flat terminal rotation. Off-domain rejection is a separate gateway theorem. No concurrency, liveness, Rust refinement, deployment mediation, or broker-effect theorem is implied.
Pre-trade, Markowitz, and ledger finance developments	Exact bounded pre-trade decision semantics with instrument/currency/scale-indexed snapshots and operand-bounded arithmetic; proof-bearing optimization; and a stateful ledger whose events preserve an explicit currency/scale unit, conservation, replay, and settlement invariants	The three developments do not establish economic validity, regulatory compliance, currency conversion/netting, or one universal finance contract; independent finance review is future work
Rust FinGate mediator	Pinned release build; exact artifact/receipt/capability/destination binding; content-addressed activation; runtime rehash/reparse; one-shot nonce state; root-v4 account/instrument/currency/scale scope with lot, aggregate-notional, and cash caps; event-sourced New, Replace, Cancel, and lot-denominated PartialFill commitment lifecycle; exact event replay; the v5 fail-closed domain-gated live lane (live decisions come from the promoted artifact's bound evidence table, off-domain rejected without state mutation, structurally mirroring the Lean gateway's fail-closed control flow); Lean-emitted differential fixtures for the evaluator and the reservation machine; a fingate bench performance harness; 61 tests on Unix (60 on non-Unix)	No Lean--Rust refinement, broker submission, distributed linearizability, external monotonic rollback anchor, killed-process/power-loss qualification, HSM, or production-security claim; local cooperative lock and same-process race tests only; demo keys
Bounded Python/Z3 regression artifacts	Deterministic control runner and 56-test regression baseline for four finite semantic models	Executable regression evidence, distinct from the kernel proofs and from a deployment bridge
KernelFinBench materials	Execution-layer evaluator on the recorded macOS development host: sandboxed episodes (network denied), fresh pinned-toolchain kernel execution, strict axiom audit, tamper-evident sealed seed registry with a by-construction truth oracle; capability probes green there; frozen preregistration	A designed, tested benchmark awaiting its episode budget; non-macOS sandbox backends remain unqualified and fail closed; no episode run and no empirical result exists yet
Reproduction	Pinned local Lean/Rust/Python/LaTeX procedures, checked axiom inventory (554 records, three standard axioms only), and leanchecker kernel replay in the gate	Candidate-specific clean-machine results are manifest-bound post-freeze qualifications recorded under research/attestations/; they do not enlarge the paper's theorem claims

The contribution is the explicit theorem-and-system composition: the counterexample-guided separation of semantic proof from byte identity and authority, and the finance-specific policy-to-reservation boundary, under the precise assumptions recorded in the claim-contract section of research/README.md. The work composes established mechanisms -- proof-carrying code, proof-carrying authorization, reference monitoring, receipts, canonical serialization, versioned roots, replay protection, and formal finance -- and claims priority over none of them.

Repository map

• paper/ - canonical manuscript (main.tex with sections/), supplement (supplement.tex) with the generated exact-types appendix and machine claim table (generated/), generic Lean proof (proof/BoundedMarkowitz.lean), and bounded Python/Z3 artifacts (artifact/).
• theory/ - Lean authority-indexed core, exact finite pre-trade slice, general FinCore gate and authority, continuous agent-loop theorem, sequential atomic reservation/gateway specification, and the three finance developments.
• interop/pretrade-v1/ - three canonical policy artifacts and the frozen request vectors used by the finite Lean/Rust qualification slice.
• interop/pretrade-v2/ - Lean-emitted kernel-artifact and kernel-evidence fixtures with their request vectors, exercised by the Rust interoperability tests.
• interop/pretrade-v3/ - Lean-emitted reservation-machine vectors (new/replace/fill/partial-fill/cancel/replay/stale-epoch/cap-boundary), replayed against the Rust command layer in the interoperability tests.
• fingate/ - Rust promotion mediator, CLI, attack regressions, and security boundary documentation.
• research/ - program state and assurance instruments consolidated in research/README.md (claim contract, literature/novelty records, threat model, review gates, replay evidence), plus the generated claim ledger and machine-readable status files.
• kernelfinbench/ - separate evaluator and protocol-design archive; not publication-result authority.
• LICENSES/ - third-party license texts for pinned dependencies.

Private council transcripts, working peer reviews, downloaded source PDFs, provider caches, credentials, and sealed tasks are not scholarly or execution authority.

Reproduce the implemented gates

The full strict build and the per-source audit replays are executed mechanically by scripts/reproduce-foundational.sh:

flowchart TD
    S[Source tree] --> B[lake --wfail build]
    B --> R[21-source audit replay<br/>lean --trust=0 -DwarningAsError=true]
    R --> X[Axiom inventory byte-compare<br/>554 records, three standard axioms]
    X --> K[leanchecker kernel replay<br/>of every first-party module]
    K --> C[Claim ledger #check probe<br/>48 declarations]
    C --> G[Generated exact types + claim table<br/>+ markdown ledger, byte-compared]
    G --> F[Frozen fixture families v1-v3<br/>v2-v3 Lean-emitted and byte-replayed]
    F --> U[cargo fmt / clippy / 61 tests<br/>+ CLI replay]
    U --> P[Fixed-epoch PDF x2<br/>identical after trailer-ID normalization]

Loading

Specialized Lean package and audited theorems:

cd theory
lake build
lake env lean --trust=0 -DwarningAsError=true VGate.lean

The audit sources under theory/VGate/**/**Audit.lean and frozen aggregate theory/audit/all-axioms.expected.txt are the authority for theorem dependencies; their live-derived sizes and digests are recorded by the verification-manifest generator at the archival freeze. The checked-in research/release-candidate-manifest.json binds the clean source commit named in its source_base_commit; it excludes itself so the manifest-only follow-up commit does not alter the frozen set. Load-bearing results use the standard Lean/Mathlib dependencies printed in that inventory; “no custom axioms” must not be shortened to “axiom-free” when propext, Quot.sound, or Classical.choice is printed.

Rust FinGate build and tests:

cd fingate
cargo fmt --all -- --check
cargo clippy --locked --release --workspace --all-targets -- -D warnings
cargo test --locked --release --workspace
cargo build --locked --release --workspace
../scripts/replay-fingate-cli.sh

The CLI witness deterministically exercises semantic rejection, candidate repair, authorization and promotion, execution, and a New -> Replace -> PartialFill -> Cancel order lifecycle before inspecting the persisted state.

Generic bounded-paper proof and executable regressions:

cd paper
lean --trust=0 proof/BoundedMarkowitz.lean
PYTHONDONTWRITEBYTECODE=1 python3 -B -m unittest discover -s artifact -p 'test_*.py'

The reproduction script emits validated fixed-epoch PDF candidates under tmp/; it does not overwrite paper/main.pdf or paper/supplement.pdf. Canonical PDFs are promoted from those candidates only after visual review. Release remains on hold pending the remaining external gates and explicit authorization.

At archival freeze, the manifest generator records file sizes and SHA-256 hashes for the canonical manuscript, proof and implementation sources, dependency inventory, replay scripts, and publication PDFs. Independent clean-machine results are recorded in a manifest-bound post-freeze attestation; they qualify that exact candidate and are not results reported in the paper.

Assurance vocabulary

• kernel-checked: replayed by Lean under the recorded toolchain and axiom policy;
• implemented: exercised by the reference code and tests;
• attack-tested: a named frozen attack was run against fixed bytes;
• measured: observed in a frozen experiment;
• reviewed: independently approved by the relevant owner;
• specified: designed but not implemented; and
• assumed: part of the trusted computing or specification base.

No one-word verdict establishes requirement fidelity, authentic market data, economic suitability, legal compliance, external complete mediation, or production safety.

Licensing

Original code, executable specifications, schemas, scripts, and tests are Apache-2.0. Original paper text, diagrams, specifications, benchmark metadata, and task prose are CC BY 4.0. The mapping and third-party exceptions are in LICENSE; complete terms are in LICENSES/.