The Mathematics of Formal Verification in Finance

Financial outputs depend on mathematical assumptions, finite representations, and operational state. We formalize proof-carrying finance by separating semantic certificate relations from total fail-closed checkers on versioned finite encodings, with explicit checked assumptions, environmental assumptions, and trusted computing bases. We prove three finite results. For explicitly enumerated rational one-period markets, no-arbitrage admits polynomial-size strictly positive state-price witnesses with polynomial-time exact checking and linear-programming production. For a rational static-hedge calculus, a terminating structural algorithm extracts a net portfolio, disposal slack, and unused budget and reconstructs a cut-free derivation. For an environment-parameterized typed deterministic serial reservedexecution schema with cumulative fills, cancellation, fee reserves, buffering, digest-bound replay protection, and authenticated terminal finality, we prove preservation of cash, inventory, quantity, and report-consistency invariants. The release provides Lean 4 developments and bounded Python checkers with per-artifact scope; it does not establish an end-to-end autonomous-trading system or a refinement of the Python execution model to the paper schema.