# MiFID II Transaction Reporting Classifier

## Executive Summary

### What It Does

A regulatory decision engine that determines whether a financial trade must be reported to the European Securities and Markets Authority (ESMA) under MiFID II rules.

### Why It Matters

**If this logic is broken, your firm could:**

- **Over-report**: Flooding regulators with irrelevant trades from non-EU jurisdictions, wasting compliance resources and potentially exposing confidential trading strategies
- **Under-report**: Missing mandatory disclosures, resulting in regulatory fines (up to €5M or 10% of annual turnover under MiFID II)
- **Jurisdictional overreach**: Incorrectly claiming authority over trades that fall outside EU jurisdiction, creating legal liability

### The Verification Win

**CodeLogician mathematically proved** that an OTC trade between two Non-EEA entities is **never** flagged for reporting — regardless of what instrument they trade.

This eliminates an entire class of jurisdictional bugs where the system might incorrectly report a trade between a Singapore bank and a US hedge fund simply because they were trading Airbus shares.

### Key Takeaways

| Aspect | Value |
|--------|-------|
| **Bug Found** | The original logic incorrectly flagged EEA instruments as reportable even when no EEA party was involved |
| **Counterexample** | `{Venue: OTC, Buyer: US, Seller: Singapore, Instrument: Airbus}` — was incorrectly marked REPORTABLE |
| **Invariant Proven** | Jurisdiction Safety: `OTC ∧ Non-EEA Buyer ∧ Non-EEA Seller → NOT Reportable` |

### Business Value

1. **Regulatory Confidence**: Mathematical proof that the reporting logic respects jurisdictional boundaries — defensible under regulatory scrutiny
2. **Cost Reduction**: Eliminates false positive reports that consume compliance team bandwidth
3. **Risk Mitigation**: Prevents potential fines from both over-reporting (data protection) and under-reporting (MiFID II violations)

---

*Verified with Imandra CodeLogician • MiFID II Compliant Logic*