Formal Verification for Harness Engineering in Quantitative Finance

Machine-generated policies can be produced faster than humans can review them, while testing observes only sampled behavior. We present a Lean 4 reference architecture that separates proposal from modeled authority at a pre-trade risk boundary. A candidate becomes active only after contract-relative qualification and promotion bind acceptance to its exact bytes. The gateway derives a request from root-owned parameters, trusted snapshots, and live reservations; evaluates the decoded promoted artifact; admits only requests in the root-owned finite evidence domain; and reserves risk before modeled dispatch. For a sequential, buy-only, one-account, one-instrument, two-slot machine from exact zero genesis, we prove that every valid finite trace preserves position and limit-price-basis acquisition-commitment caps, with commitmentalso bounded by cash headroom. For each archived dispatch, the theorem furnishes artifactcausality, root-agreement, and exact-origin witnesses; a separate theorem rejects off-domain requests fail-closed. These model-internal results assume named signature, snapshot, kernel, toolchain, operating-system, and hardware trust boundaries. They establish neither concurrencynor linearizability, Lean–Rust refinement, concrete cryptographic security, external-fact truth, liveness, nor economic or regulatory correctness. Rust supplies regression evidence through pinned tests and Lean-emitted fixtures. The reproduction gate checks pinned-source replay, a frozen axiom inventory, generated theorem signatures and claim tables, and normalized-PDF agreement across two same-environment builds; ledger-prose fidelity remains human-reviewed.