Formal verification of trading in financial markets
Pith reviewed 2026-05-24 19:45 UTC · model grok-4.3
The pith
A Coq framework formally defines fair, uniform, and individually rational trades and proves their properties for double-sided auctions.
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
Core claim
We introduce a formal framework for analyzing trades in financial markets. We formally define fair, uniform, and individual rational matchings, prove relevant results on matchings, and verify these properties for two classes of double-sided auctions. All the definitions and results presented in this paper are completely formalised in the Coq proof assistant without adding any additional axioms to it.
What carries the argument
Formal definitions in Coq of fair, uniform, and individual-rational matchings, together with proofs of their properties on matchings, used to verify two classes of double-sided auctions.
If this is right
- Results on matchings can be stated and proved inside Coq for any auction that produces such matchings.
- The two verified classes of double-sided auctions satisfy the fairness, uniformity, and individual-rationality properties by construction.
- Any future auction implementation can be checked against the same Coq definitions to obtain machine-checked compliance evidence.
- The absence of added axioms means the proofs rest only on the standard Coq logic and the paper's own definitions.
Where Pith is reading between the lines
- The same Coq library could be reused to check compliance of new auction designs before deployment.
- Regulators could adopt the formal definitions as an unambiguous reference when writing rules.
- Extending the framework to continuous double auctions or other market mechanisms would require only new definitions that reuse the existing matching lemmas.
Load-bearing premise
The formal definitions of fair, uniform, and individual rational accurately capture the regulatory guidelines that market regulators enforce on exchanges.
What would settle it
A concrete matching that satisfies the Coq definitions of fair, uniform, and individual rational yet fails to meet the corresponding regulatory guideline as stated by a market authority, or vice versa.
read the original abstract
We introduce a formal framework for analyzing trades in financial markets. An exchange is where multiple buyers and sellers participate to trade. These days, all big exchanges use computer algorithms that implement double sided auctions to match buy and sell requests and these algorithms must abide by certain regulatory guidelines. For example, market regulators enforce that a matching produced by exchanges should be \emph{fair}, \emph{uniform} and \emph{individual rational}. To verify these properties of trades, we first formally define these notions in a theorem prover and then give formal proofs of relevant results on matchings. Finally, we use this framework to verify properties of two important classes of double sided auctions. All the definitions and results presented in this paper are completely formalised in the Coq proof assistant without adding any additional axioms to it.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper introduces a formal framework in Coq for analyzing trades in financial markets via double-sided auctions. It defines the notions of fair, uniform, and individually rational matchings, proves relevant results about matchings, and verifies that two important classes of such auctions produce matchings satisfying these properties. All definitions, theorems, and verifications are claimed to be completely formalized in Coq without any additional axioms.
Significance. If the formal definitions correctly capture the intended market properties, the work supplies a machine-checked Coq development that can serve as a foundation for verifying regulatory compliance of auction algorithms. The absence of added axioms and the use of standard Coq logic are explicit strengths that allow independent checking of the proofs.
major comments (1)
- [Abstract] Abstract and introduction: the central claim that the Coq definitions of fair, uniform, and individual rational 'capture' the properties 'market regulators enforce' is not supported by any citation to specific regulatory sources (e.g., SEC Rule 610, MiFID II best-execution provisions, or exchange rulebooks) or by an explicit side-by-side mapping of the formal predicates to regulatory clauses. Without this, it is impossible to determine whether the verified properties omit key requirements such as time priority or pro-rata allocation.
Simulated Author's Rebuttal
We thank the referee for the constructive comments. We address the single major comment below and agree that the manuscript would benefit from additional references and clarification.
read point-by-point responses
-
Referee: [Abstract] Abstract and introduction: the central claim that the Coq definitions of fair, uniform, and individual rational 'capture' the properties 'market regulators enforce' is not supported by any citation to specific regulatory sources (e.g., SEC Rule 610, MiFID II best-execution provisions, or exchange rulebooks) or by an explicit side-by-side mapping of the formal predicates to regulatory clauses. Without this, it is impossible to determine whether the verified properties omit key requirements such as time priority or pro-rata allocation.
Authors: We acknowledge that the abstract and introduction state the regulatory relevance of fairness, uniformity, and individual rationality without supporting citations or an explicit mapping. The paper treats these as standard properties from market design literature rather than deriving them from specific rules. We agree this leaves open questions about coverage of aspects such as time priority. In the revision we will add citations to relevant market microstructure and auction design references that discuss these properties in regulatory contexts, and include a brief clarifying paragraph noting that our formal predicates target core matching invariants while order-book mechanisms (time priority, pro-rata) are typically enforced upstream of the matching function itself. This keeps the scope focused on the Coq formalization while addressing the referee's concern. revision: yes
Circularity Check
No circularity: formal definitions and proofs are self-contained in standard Coq without self-referential reductions or load-bearing self-citations.
full rationale
The paper defines fair/uniform/individual-rational matchings directly in Coq (§3–4) and proves preservation properties for two auction classes. These definitions are introduced as formalizations of regulatory notions, but the derivation chain consists of explicit Coq predicates and theorems proved from the standard library with no added axioms. No equations reduce by construction to fitted inputs, no uniqueness theorems are imported from the authors' prior work, and no ansatz or renaming is smuggled via self-citation. The modeling claim that the predicates capture regulatory guidelines is an external semantic assertion, not a circular step within the formal derivation itself. The work is therefore self-contained against external benchmarks (Coq kernel).
Axiom & Free-Parameter Ledger
axioms (1)
- standard math Coq proof assistant standard logic and libraries
Lean theorems connected to this paper
-
IndisputableMonolith/Cost/FunctionalEquation.leanwashburn_uniqueness_aczel unclear?
unclearRelation between the paper passage and the cited Recognition theorem.
We formally define these notions in a theorem prover and then give formal proofs of relevant results on matchings... verify properties of two important classes of double sided auctions.
-
IndisputableMonolith/Foundation/ArithmeticFromLogic.leanLogicNat.induction unclear?
unclearRelation between the paper passage and the cited Recognition theorem.
Definition 12. fair_on_bids M B:= ∀ b b’, In b B ∧ In b’ B -> b > b’ -> In b’ BM -> In b BM.
What do these tags mean?
- matches
- The paper's claim is directly supported by a theorem in the formal canon.
- supports
- The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
- extends
- The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
- uses
- The paper appears to rely on the theorem as machinery.
- contradicts
- The paper's claim conflicts with a theorem or certificate in the canon.
- unclear
- Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.