Exchange Fee Schedule Verification

Financial ServicesFormal VerificationPython to IMLExchange Fees

Overview

Quantitative and algorithmic trading firms must know their trading fees before sending orders. Without accurate fee predictions, it's impossible to reliably forecast trading revenues—and a fraction of a basis point can be the difference between a profitable strategy and a losing one.

This case study demonstrates how CodeLogician formally verified the London Stock Exchange Trading Services Price List (January 2025), proving critical invariants and discovering hidden complexity in the fee structure.

Why This Matters

A single basis point error in fee calculation across millions of daily orders can mean revenue leakage (overestimating fees rejects profitable trades), unexpected costs (underestimating destroys margins), or regulatory risk (incorrect fee reporting violates MiFID II best execution requirements).

Background

The Restaurant Analogy

Think of the LSE fee schedule like a restaurant bill:

Restaurant	LSE Trading
Cover charge (just for sitting down)	Order entry fee — 1p for "urgent" IOC/FOK orders
Price per dish (varies by what you order)	Execution fee — varies by how much you trade
Volume discount ("10+ dishes, 10% off")	Tiered pricing — trade £3.5bn+, get cheaper rates
Loyalty card discount	LPS rebate — market makers get paid to provide liquidity
Minimum spend ("orders under £10 = £10")	Minimum charge — small trades pay a floor fee

The complexity comes from the fact that all these rules interact. That's where mistakes happen.

Fee Calculation Pipeline

graph LR A[Order] --> B[Order Entry Charge] B --> C[Rate Selection] C --> D[Fee Calculation] D --> E[Minimum Floor] E --> F[Total Cost] C --> G{Aggressive?} G -->|Yes| H[Package Rates] G -->|No| I[LPS or Tiered] style A fill:#0284c7,stroke:#0369a1,color:#fff style F fill:#16a34a,stroke:#15803d,color:#fff

The Problem

Fee schedules are notoriously difficult to model:

Opaque Specifications

Fee rules are published as PDFs with tables, prose, and footnotes—not machine-readable formats.

Complex Interactions

Tiered pricing, minimum floors, rebates, and surcharges interact in non-obvious ways.

Frequent Changes

Exchanges update fee schedules periodically; each change must be mapped to the model.

Auditability

Firms need to prove their models match the exchange specification for regulators.

The Testing Problem

The LSE fee schedule has 6+ distinct behavioral regions based on trade size, order type, and firm configuration. Traditional unit testing struggles to exhaustively cover all combinations—and can never prove correctness for ALL inputs.

The Solution

Formal Verification with CodeLogician provides mathematical proof, not just empirical testing.

The Workflow

graph TB A[Python Code] --> B[CodeLogician Formalizer] B --> C[IML Model] C --> D[Imandra Reasoning Engine] D --> E{Verification} E -->|Proved| F[✅ Invariant Holds] E -->|Refuted| G[☒ Counterexample] D --> H[Region Decomposition] H --> I[6 Behavioral Regions] style F fill:#16a34a,stroke:#15803d,color:#fff style G fill:#dc2626,stroke:#b91c1c,color:#fff style I fill:#0284c7,stroke:#0369a1,color:#fff

Python to IML

Core Fee Calculator

def get_tiered_rate(cumulative_value_gbp: Decimal) -> Decimal:
    """
    Get the standard scheme rate based on cumulative MTD value.
 
    [PDF:P4:STANDARD_TIERS]
    - First £3.5bn: 0.45bp
    - Next £5bn (to £8.5bn): 0.35bp
    - All subsequent: 0.25bp
    """
    if cumulative_value_gbp < TIER_1_THRESHOLD_GBP:
        return TIER_1_RATE_BP
    elif cumulative_value_gbp < TIER_2_THRESHOLD_GBP:
        return TIER_2_RATE_BP
    else:
        return TIER_3_RATE_BP

Every constant annotated with PDF source reference for auditability.

What CodeLogician Verified

Tiered Rate Function

3 Regions — Exactly as Expected

Region	Constraint	Rate
1	`cumulative < £3.5bn`	0.45bp
2	`£3.5bn ≤ cumulative < £8.5bn`	0.35bp
3	`cumulative ≥ £8.5bn`	0.25bp

Execution Fee Function

6 Regions Discovered — Expected 2-3!

#	Hidden	Rate	Min Dominates	Output Formula
1	✓	≥ 0	Yes	`min_charge`
2	✓	≥ 0	No	`notional × (rate + 0.25) × 0.0001`
3	✗	≥ 0	Yes	`min_charge`
4	✗	≥ 0	No	`notional × rate × 0.0001`
5	✓	< 0	N/A	`notional × (rate + 0.25) × 0.0001`
6	✗	< 0	N/A	`notional × rate × 0.0001`

Invariants Proved

Invariant 1: "Penny Jump"

An IOC or FOK order costs exactly £0.01 more than an identical DAY order.

Cost(IOC) = Cost(DAY) + £0.01

Status: ✅ PROVED for ALL inputs

Invariant 2: LPS Zero-Fee

When rate = 0.00bp and min = 0.00, execution fee is guaranteed exactly zero.

exec_fee(notional, 0.0, 0.0, false) = 0.0

Status: ✅ PROVED for ALL inputs

Edge Cases Discovered

Small Trade Penalty

Hidden Minimum Charge Boundaries

Trades below the crossover notional pay the minimum charge, resulting in an effective rate much higher than the stated bp rate.

Example: £1,000 trade at 0.45bp rate

Calculated fee: £1,000 × 0.45 × 0.0001 = £0.045

Minimum floor: £0.11

Effective rate: 11bp (24× the stated rate!)

Crossover Notional by Scheme

Scheme	Rate (bp)	Min (p)	Crossover Notional
Standard (Tier 1)	0.45	11	£2,444
Standard (Tier 2)	0.35	11	£3,143
Standard (Tier 3)	0.25	11	£4,400
Package 1	0.15	5	£3,333
Package 1 Prop	0.15	10	£6,667
Package 2	0.28	10	£3,571

Other Edge Cases

Rebate Bypass

Negative rates (LPS rebates) bypass the minimum charge logic entirely.

This is intentional—you don't apply a minimum floor to a rebate.

Hidden Order Interaction

The hidden premium (+0.25bp) is additive to the base rate before minimum floor comparison—hidden orders have a different crossover notional than visible orders.

Key Takeaways

Mathematical Proof > Unit Tests

We didn't test examples—we proved invariants hold for ALL possible combinations of inputs. 100% certainty, not 99.9%.

Hidden Complexity Exposed

Formal decomposition revealed 6 behavioral regions where we expected 2-3. This complexity is invisible if you just read the PDF.

Audit-Ready Evidence

Every fee calculation traces to a specific PDF source reference. When regulators ask "how do you know?"—we have mathematical proof.

Change Management Ready

When LSE updates their fee schedule, re-run decomposition and diff the behavioral regions to see exactly what changed structurally.

Downloads

Python Implementation IML Formal Model

LSE Trading Services Price List — Effective 01 January 2025
Formal Model Status: TRANSPARENT (fully executable, no opaque functions) — View IML Model
Verification Engine: Imandra CodeLogician

Verify your fee calculations with mathematical certainty

Use CodeLogician to ensure your trading cost models, pricing engines, and compliance calculations are provably correct.

Try CodeLogician