MiFID II Transaction Reporting Classifier

Critical Bug FoundFinancial ServicesFormal VerificationRegulatory Compliance

Overview

This case study demonstrates how CodeLogician discovered a jurisdictional bug in MiFID II transaction reporting logic that would cause improper regulatory disclosures. A regulatory decision engine that determines whether financial trades must be reported to ESMA (European Securities and Markets Authority) had a subtle flaw that formal verification caught immediately.

The Bug: Jurisdictional Overreach

Found: OTC trades between Non-EEA entities incorrectly flagged as reportable, even when no European party was involved.

Impact: Over-reporting to ESMA, wasting compliance resources and potentially exposing confidential trading strategies—plus legal liability for claiming EU jurisdiction over non-EU trades.

Detection: CodeLogician found a concrete counterexample that traditional testing would almost certainly miss.

The Business Problem

What is MiFID II?

The Markets in Financial Instruments Directive II (MiFID II) is European financial regulation requiring firms to report certain trades to ESMA. Getting this wrong has serious consequences:

❌ Over-Reporting Risk

Flooding regulators with irrelevant trades from non-EU jurisdictions
Wasting compliance team bandwidth reviewing false positives
Exposing confidential trading strategies unnecessarily
Legal liability for claiming authority over non-EU trades

⚠️ Under-Reporting Risk

Missing mandatory disclosures to ESMA
Regulatory fines up to €5M or 10% of annual turnover
Potential trading suspension or license revocation
Reputational damage and client trust issues

The Reporting Rules

Our classifier implements a priority-based decision cascade that asks four questions in order:

Priority	Question	Decision
1	Did this trade happen on a European stock exchange?	→ REPORT
2	Is this a European instrument AND at least one party European?	→ REPORT
3	Was this an OTC trade AND at least one party European?	→ REPORT
4	None of the above?	→ DON'T REPORT

The Key Insight

Just because they're trading a European stock doesn't mean Europe has jurisdiction. The parties matter too. A US hedge fund buying BMW shares from a Singapore bank over the phone has nothing to do with ESMA.

The Bug Discovery

The Original (Buggy) Logic

Priority 2: The Flaw

def is_reportable(trade: Trade) -> bool:
    # Priority 1: EEA Exchange
    if is_eea_exchange(trade.venue):
        return True
 
    # Priority 2: EEA Instrument - THE BUG
    if trade.instrument_region == Region.EEA:
        return True  # ← No counterparty check!
 
    # Priority 3: OTC with EEA Counterparty
    if trade.venue == Venue.OTC and has_eea_counterparty(trade):
        return True
 
    return False

The Problem

Priority 2 checked instrument_region == EEA without verifying that at least one counterparty was an EEA entity.

This caused jurisdictional overreach—the system would report trades that fell completely outside MiFID II scope.

The Problematic Scenario

THE TRADE:

Buyer: US Hedge Fund (New York)
Seller: Singapore Bank
Instrument: BMW shares (German company)
Venue: OTC (over the phone)

THE PROBLEM:

✗ Neither party is European
✗ Trade didn't happen in Europe
✗ ESMA has no jurisdiction here
✗ But buggy code says: "REPORT IT!"

The system incorrectly claimed EU authority over a bilateral trade between two non-EU entities.

Region Decomposition Analysis

CodeLogician decomposed the is_reportable function into 8 distinct symbolic regions, each representing a unique behavioral path through the logic:

Region	Constraints	Output	Correctness
R1	venue = LSE	REPORTABLE	✅ EEA Exchange
R2	venue = XETR	REPORTABLE	✅ EEA Exchange
R3	venue = XPAR	REPORTABLE	✅ EEA Exchange
R4	instrument = EEA ∧ venue = NYSE ∧ has_eea_counterparty	REPORTABLE	✅ ToTV nexus
R5	instrument = EEA ∧ venue = OTC ∧ has_eea_counterparty	REPORTABLE	✅ ToTV nexus
R6	venue = OTC ∧ buyer = EEA ∧ ¬EEA_instrument	REPORTABLE	✅ OTC with EEA party
R7	venue = OTC ∧ seller = EEA ∧ ¬EEA_instrument	REPORTABLE	✅ OTC with EEA party
R8	venue = NYSE ∧ ¬EEA_instrument ∧ ¬has_eea_counterparty	NOT REPORTABLE	✅ No EEA nexus

Complete Coverage Guarantee

These 8 regions provide mathematical certainty that all possible trade scenarios are covered. There are no hidden edge cases—CodeLogician has systematically explored the entire decision space.

The Verified Invariant

Jurisdiction Safety Property

Mathematical Definition:

For all trades t: (t.venue = OTC AND t.buyer_loc = NON_EEA AND t.seller_loc = NON_EEA) implies NOT is_reportable(t)

Plain English:

The Invariant

An OTC trade between two non-European entities should never be reportable to ESMA, regardless of what financial instrument they are trading.

Verification Status: ✅ PROVED by CodeLogician

Edge Cases Handled

EEA Exchange Precedence

Trades on EEA exchanges are always reportable, even if all parties are Non-EEA.

Example: Chinese firm buys US stock on London Stock Exchange → REPORTABLE

OTC with Mixed Parties

If either buyer or seller is EEA, OTC trade is reportable regardless of instrument.

Example: German bank buys Apple stock OTC from US broker → REPORTABLE

Non-EEA Venue with EEA Instrument

Trading Airbus on NYSE is only reportable if at least one party is EEA.

Fixed bug: Now correctly checks counterparty locations

The Fixed Scenario

BMW trade between US hedge fund and Singapore bank → NOT REPORTABLE

Key insight: EEA instrument alone is insufficient without EEA party involvement

Business Impact

❌ Without Formal Verification

Testing Approach:

Manual test case design: Days of work
Likely to miss jurisdictional edge cases
Bug found in production: Weeks/months later
Over-reporting hundreds of trades daily
Compliance team overwhelmed with false positives
Potential regulatory scrutiny and fines

Risk: Jurisdictional bugs create legal liability and operational burden while exposing confidential trading data.

✅ With CodeLogician

Formal Verification:

Automatic formalization: Minutes
Exhaustive verification: All scenarios covered
Bug discovery: Immediate with concrete counterexample
Fix validation: Mathematical proof of correctness
Production deployment: Zero reporting errors
Regulatory confidence: Auditable proof

Guarantee: Mathematical proof that jurisdictional boundaries are respected for ALL possible inputs.

Regulatory Context

MiFID II Compliance Requirements

🇪🇺
MiFID II Scope

✓ EEA trading venues
✓ EEA Investment Firms
✓ EEA financial instruments with EEA nexus
✓ Excludes purely non-EEA transactions

⚖️
Jurisdictional Rules

✓ ToTV nexus required
✓ Counterparty location matters
✓ Cannot claim authority over non-EU trades
✓ Data protection for non-EU entities

📋
Reporting Standards

✓ RTS 22 technical standards
✓ ESMA validation rules
✓ T+1 reporting deadline
✓ Penalties for errors

The Audit Advantage

❌ Traditional Testing

To Auditors:

"We ran 1,000 test cases covering various scenarios."

Auditor's Response:

"But what about the jurisdictional edge cases? How do you know you covered all combinations?"

✅ Formal Verification

To Auditors:

"We mathematically proved the jurisdiction safety property holds for ALL possible trades—past, present, and future."

Auditor's Response:

"That's the gold standard. Excellent evidence of compliance."

Key Results

Verification Summary

Metric	Value
Formalization Status	✅ TRANSPARENT (fully executable)
Invariants Verified	1 (Jurisdiction Safety)
Counterexamples Found	1 (in original buggy code)
Proof Status (After Fix)	✅ PROVED
Regions Decomposed	8 distinct behavioral paths
Lines of Code	342 (Python implementation)

Business Value

Regulatory Confidence

Mathematical proof that reporting logic respects jurisdictional boundaries—defensible under regulatory scrutiny.

Cost Reduction

Eliminates false positive reports that consume compliance team bandwidth. No wasted effort on non-reportable trades.

Risk Mitigation

Prevents potential fines from both over-reporting (data protection violations) and under-reporting (MiFID II non-compliance).

Operational Excellence

Zero jurisdictional errors in production. System behavior is mathematically guaranteed correct.

Resources

Download the Code

Python Implementation IML Formal Model

Documentation

Executive Summary Technical Walkthrough Plain-English Guide

Broader Applications

This verification approach applies to any regulatory or compliance logic with:

✅ Jurisdictional Rules

Geographic boundaries, entity classifications, regulatory scope determination

✅ Multi-Criteria Classification

Decision trees combining venue, party, instrument, and other attributes

✅ Priority-Based Logic

Cascade of rules where first match determines outcome

✅ Regulatory Reporting

EMIR, Dodd-Frank, MAS, ASIC, and other transaction reporting regimes

✅ Compliance Filters

Trade validation, sanctions screening, AML/KYC checks

✅ Classification Systems

Customer segmentation, risk categorization, product eligibility

Industry Examples

Capital Markets: Trade reporting (MiFID II, EMIR, Dodd-Frank), best execution analysis
Banking: Sanctions screening, AML transaction monitoring, customer due diligence
Asset Management: Regulatory classification (AIFMD, UCITS), investment restrictions
Insurance: Solvency II reporting, policyholder classification
Fintech: Regulatory perimeter determination, licensing requirements

Key Takeaways

Critical Bug Found

Jurisdictional overreach: EEA instruments were reportable even when no EEA party was involved.

Mathematical Proof

Verified that OTC trades between Non-EEA entities are NEVER reportable, regardless of instrument.

Regulatory Safety

Prevents both over-reporting (data protection, operational waste) and under-reporting (MiFID II violations).

Complete Coverage

8 behavioral regions identified—mathematical guarantee that all scenarios are covered.

Audit Evidence

Formal proofs provide defensible documentation for regulatory examinations and audits.

Production Ready

Verified Python implementation with zero jurisdictional errors in operation.

Verify your regulatory compliance logic

Use CodeLogician to ensure your reporting systems respect jurisdictional boundaries and comply with MiFID II, EMIR, and other regulatory requirements.

Try CodeLogician