Multilateral Netting Engine Verification

Overview

This case study demonstrates how CodeLogician discovered TWO critical bugs in a Central Counterparty (CCP) style multilateral netting engine—the type of system that processes trillions of dollars daily in cleared derivatives markets. These bugs could have caused systemic financial failures in production.

The Business Requirement

What is Multilateral Netting?

In cleared derivatives markets, a Central Counterparty (CCP) sits between buyers and sellers, aggregating thousands of bilateral trades into net obligations for each participant.

Example:

Bilateral Trades:
- Bank A pays Bank B: $1M
- Bank B pays Bank C: $800K
- Bank C pays Bank A: $500K

Multilateral Netting Result:
- Bank A owes: $500K net
- Bank B owes: $200K net
- Bank C receives: $700K net

Critical Invariants

Zero-Sum Conservation: The sum of all net positions MUST equal exactly zero. Money cannot appear or disappear.

Σ(net_positions) = 0

Netting Efficiency: Net exposure must be less than or equal to gross exposure. Netting should reduce risk, not amplify it.

|net_exposure| ≤ |gross_exposure|

Why This Matters

• ❌ Settlement Failure: If positions don't sum to zero, funds vanish or appear from thin air
• ❌ Regulatory Breach: Violates EMIR and Dodd-Frank mathematical correctness requirements
• ❌ Cascading Default: Incorrect calculations trigger margin calls, forced liquidations, cross-market contagion

The System

Model Details

The multilateral netting engine implementation processes trades and calculates net obligations:

Model Statistics:

• Language: Python
• Lines of Code: ~200
• Formalization Quality: TRANSPARENT (optimal)
• Analysis Time: < 5 minutes

What CodeLogician Verified

The Bugs

Bug #1: Input Validation Gap

Counterexample Found by CodeLogician:

Trade(payer_id="", receiver_id="", amount=-10834.0)

Impact:

Gross Exposure: |-10834| = 10834
Net Exposure:   |10834| + |-10834| = 21668

Result: 21668 > 10834 → Netting efficiency VIOLATED!

Root Cause:

def calculate_net_obligations(trades: List[Trade]) -> Dict[str, Decimal]:
    net_positions: Dict[str, Decimal] = {}
 
    for trade in trades:
        # ⚠️ NO VALIDATION - negative amounts accepted!
        net_positions[trade.payer_id] = net_positions.get(trade.payer_id, Decimal('0')) - trade.amount
        net_positions[trade.receiver_id] = net_positions.get(trade.receiver_id, Decimal('0')) + trade.amount
 
    return net_positions

Why It Matters:

• While Python's @dataclass validation exists (__post_init__), the core algorithm is vulnerable
• An attacker or bug could inject negative trades, corrupting settlement
• CodeLogician caught this before any test code was written

Bug #2: Floating-Point Precision Failure

The Classic 0.1 + 0.1 + 0.1 Problem:

>>> float_sum = 0.0
>>> for _ in range(10):
...     float_sum += 0.1
>>> float_sum
0.9999999999999999
>>> float_sum == 1.0
False

>>> from decimal import Decimal
>>> decimal_sum = Decimal('0')
>>> for _ in range(10):
...     decimal_sum += Decimal('0.1')
>>> decimal_sum
Decimal('1.0')
>>> decimal_sum == Decimal('1.0')
True

Real-World Impact:

Consider 1000 trades averaging $1M each with IEEE 754 float precision:

Expected Zero-Sum: $0
Actual with Floats: $0.0000152587890625
Error: ~$0.015 (1.5 cents)

Sounds small? In high-frequency clearing:

• 1000 trades/second × 86400 seconds/day = 86.4 million trades/day
• Accumulated error: $1,296 per day in "phantom money"
• Over a year: $473,040 unexplained

The Fix

Solution: Migrate to Decimal

Before (Float - Buggy):

from typing import List, Dict
 
@dataclass
class Trade:
    payer_id: str
    receiver_id: str
    amount: float  # ❌ IEEE 754 precision errors
 
def calculate_net_obligations(trades: List[Trade]) -> Dict[str, float]:
    net_positions: Dict[str, float] = {}
 
    for trade in trades:
        # ❌ No validation
        net_positions[trade.payer_id] = net_positions.get(trade.payer_id, 0.0) - trade.amount
        net_positions[trade.receiver_id] = net_positions.get(trade.receiver_id, 0.0) + trade.amount
 
    return net_positions

After (Decimal - Fixed):

from decimal import Decimal
from typing import List, Dict
 
@dataclass
class Trade:
    payer_id: str
    receiver_id: str
    amount: Decimal  # ✅ Arbitrary precision
 
    def __post_init__(self):
        if self.amount < 0:
            raise ValueError(f"Negative amounts not allowed: {self.amount}")
 
def calculate_net_obligations(trades: List[Trade]) -> Dict[str, Decimal]:
    net_positions: Dict[str, Decimal] = {}
 
    for trade in trades:
        # ✅ Defense-in-depth validation
        if trade.amount < 0:
            raise ValueError(f"Negative amounts not allowed: {trade.amount}")
 
        net_positions[trade.payer_id] = net_positions.get(trade.payer_id, Decimal('0')) - trade.amount
        net_positions[trade.receiver_id] = net_positions.get(trade.receiver_id, Decimal('0')) + trade.amount
 
    return net_positions

Re-verification Results

After applying the fix:

Verification Time: < 1 minute to re-verify after fix

Value Demonstrated

Key Lessons

1. Floating-Point Arithmetic is Dangerous in Finance

Never use float for money. IEEE 754 binary representation cannot exactly represent most decimal values, leading to accumulated errors that violate conservation of funds.

2. Input Validation Must Be Defense-in-Depth

Relying solely on dataclass validation is insufficient. Core algorithms must validate their own inputs to prevent malicious or buggy data from corrupting calculations.

3. Traditional Testing Would Miss These Bugs

Unit tests typically use "normal" values. Formal verification explores the entire input space, finding edge cases like negative amounts and precision errors that humans rarely think to test.

4. Regulatory Compliance Through Proof

For CCPs subject to EMIR and Dodd-Frank, formal verification provides auditable mathematical proof of correctness—far stronger than test coverage reports.

Applicability

This approach is critical for:

✅ Financial Clearing & Settlement: CCPs, clearinghouses, payment systems
✅ Cryptocurrency Exchanges: On-chain and off-chain settlement
✅ Banking Infrastructure: Core banking, wire transfers, ACH processing
✅ Algorithmic Trading: High-frequency trading systems
✅ Risk Management: Margin calculations, collateral management

Common Thread: Systems where mathematical correctness is non-negotiable and bugs can cause systemic failures.

Conclusion

Formal verification with CodeLogician:

• ❌ Discovered 2 critical bugs (input validation, floating-point precision)
• ✅ Prevented potential systemic financial failure
• ✅ Provided mathematical proof of correctness after fix
• ✅ Enabled regulatory compliance with auditable evidence

Bottom Line: In financial infrastructure processing trillions of dollars daily, formal verification isn't optional—it's existential. CodeLogician caught production-breaking bugs before a single test was written.

Resources

Download the Example

Related Resources

• LSE GTT Order Expiry - Auction timing verification
• LSE Stop Orders - MIT201 compliance verification
• ATRA Case Study - Redundant rule detection
• All Case Studies - Explore more real-world examples
• CodeLogician Agent - Learn more about the agent

Case Study Date: November 24, 2025
Tool: CodeLogician v17
Domain: Financial Infrastructure - CCP/Clearinghouse
Result: 2 Critical Bugs Found & Fixed | Mathematical Proof Achieved | Systemic Risk Eliminated