LSE Stop Orders Verification

Overview

This case study demonstrates how CodeLogician validated a Python implementation of Stop and Stop Limit orders for the London Stock Exchange (LSE), implementing business rules from MIT201 Section 5.2. While the core MIT201 specification was correctly implemented, CodeLogician discovered a critical bug in extended functionality that bypassed regulatory requirements.

The Business Requirement

Stop orders are critical risk management tools in trading systems. According to MIT201 Section 5.2, they must follow precise election rules:

Election Rules

Buy Stop Orders:

• Elect when Last Automated Trade Price (LATP) rises to or above the stop price
• Used to protect short positions or enter long positions on upward momentum

Sell Stop Orders:

• Elect when LATP falls to or below the stop price
• Used to limit losses on long positions or enter short positions on downward momentum

Critical Safety Property

A fundamental invariant: buy and sell stop orders should never elect simultaneously, as this could indicate:

• Conflicting risk positions
• Potential for self-matching
• Unintended market impact

The System

Model Details

The trading system implementation includes:

Model Statistics:

• Language: Python
• Lines of Code: 480
• Formalization Quality: TRANSPARENT (optimal)
• Analysis Time: < 1 minute

What CodeLogician Verified

Verification Goal 1: State Validity

Property: Can the system maintain well-formed states?

Result: ✅ PROVED - The system correctly maintains valid states

Verification Goal 2: Simultaneous Election

Property: Is it possible for buy and sell stop orders to be elected at the same time?

Expected: ❌ Should be IMPOSSIBLE per MIT201 specification

Actual: ❌ REFUTED - CodeLogician found a counterexample!

The Bug

Root Cause

def maybe_elect_stop_order(latp: Optional[Price], stop_order: StopOrder) -> OrderSlot:
    # Extended functionality (NOT part of MIT201)
    if stop_order.qty > 1000:
        return elect_stop_order(stop_order)  # ⚠️ BYPASSES ALL MIT201 RULES
 
    # MIT201 compliant logic below...
    if stop_price_is_reached(latp, stop_order):
        return elect_stop_order(stop_order)
    else:
        return park_stop_order(stop_order)

This "temporary hack" for large orders:

• ❌ Bypasses LATP checks (violates Rule 2)
• ❌ Bypasses stop price checks (violates Rules 3 & 4)
• ❌ Allows simultaneous election of buy and sell orders
• ❌ Violates the published MIT201 specification

The Counterexample

CodeLogician provided a concrete scenario demonstrating the bug:

LATP: 4064
Buy Stop Order:  qty = 1,    stop_price = 2276 (small order, follows MIT201)
Sell Stop Order: qty = 1143, stop_price = 4064 (large order, triggers hack)

The Fix

Immediate Remediation

Remove the extended functionality entirely:

def maybe_elect_stop_order(latp: Optional[Price], stop_order: StopOrder) -> OrderSlot:
    # REMOVE the hack completely
 
    # Keep only MIT201-compliant logic:
    if stop_price_is_reached(latp, stop_order):
        return elect_stop_order(stop_order)
    else:
        return park_stop_order(stop_order)

Re-verification

After applying the fix:

• Verification Time: < 1 minute
• Result: ✅ Both verification goals now PROVED
• Confidence: Mathematical certainty of correctness

Value Demonstrated

Key Lessons

1. Extensions Need Verification Too

Even when core specifications are correctly implemented, custom extensions can introduce bugs. Formal verification catches these before production.

2. Counterexamples Are Invaluable

Having a concrete failing scenario makes debugging immediate and unambiguous. No guesswork required.

3. Fast Feedback Enables Confidence

Verification in under 1 minute means developers can iterate quickly and deploy with mathematical certainty.

4. Documentation Becomes Executable

The verification goals serve as executable specifications that document expected behavior and prevent regressions.

Applicability

This approach is valuable for:

✅ Trading Systems: Order handling, matching engines, risk management
✅ Financial Services: Transaction processing, compliance rules
✅ Regulated Industries: Healthcare, aerospace, automotive
✅ Critical Infrastructure: Control systems, safety mechanisms
✅ API Implementations: Protocol compliance, specification adherence

Conclusion

Formal verification with CodeLogician:

• ✅ Validated the correct MIT201 core implementation
• ✅ Discovered a bug in extended functionality
• ✅ Prevented a potential production incident
• ✅ Provided actionable remediation in under 1 minute

Bottom Line: In 30 minutes, we achieved what might take days of manual testing, with mathematical certainty rather than probabilistic confidence.

Resources

Download the Example

Related Resources

• LSE GTT Order Expiry - Related LSE verification case study
• ATRA Case Study - Algorithmic trading rules analysis
• 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: Trading Systems & Financial Markets
Result: Core Implementation ✅ | Extended Functionality ❌ | Time Saved: ~8 hours