UBS Dark Pool Verification

Financial Services Production Deployment

Formal verification of the UBS ATS dark pool matching engine — discovering a subtle transitivity violation in order ranking that could cause unpredictable matching behavior.

Overview

In 2015, Imandra was used to formally verify the order matching logic of UBS's Alternative Trading System (ATS) dark pool, based on their SEC Form ATS submission. The work won first place in the UBS Future of Finance Challenge (620 companies, 52 countries).

Dark pools are private trading venues where institutional investors execute large orders away from public exchanges. The correctness of their matching logic is critical — a bug could result in unfair order execution, regulatory violations, or financial losses.

Key Finding

Imandra discovered that the UBS ATS order ranking function violates transitivity — if order A outranks B, and B outranks C, it does not necessarily follow that A outranks C. This is a fundamental fairness violation.

The Model

The model captures the full complexity of a real dark pool: multiple order types, pegged pricing, crossing restrictions, and priority rules. The code below is a self-contained IML development you can paste into ImandraX.

Types

type order_side = BUY | SELL | SELL_SHORT
type order_peg = NEAR | MID | FAR | NO_PEG
 
type order_type =
  | MARKET
  | LIMIT
  | PEGGED
  | PEGGED_CI
  | LIMIT_CI
  | FIRM_UP_PEGGED
  | FIRM_UP_LIMIT
 
type order_attr = RESIDENT | IOC
type category = C_ONE | C_TWO | C_THREE | C_FOUR
type capacity = Principal | Agency
 
type mkt_data = {
  nbb : real;
  nbo : real;
  l_up : real;
  l_down : real;
}
 
type category_elig = {
  c_one_elig : bool;
  c_two_elig : bool;
  c_three_elig : bool;
  c_four_elig : bool;
}
 
type cross_restrict = {
  cr_self_cross : bool;
  cr_ubs_principal : bool;
  cr_round_lot_only : bool;
  cr_no_locked_nbbo : bool;
  cr_pegged_mid_point_mode : int;
  cr_enable_conditionals : bool;
  cr_min_qty : bool;
  cr_cat_elig : category_elig;
}
 
type order = {
  id : int;
  peg : order_peg;
  client_id : int;
  order_type : order_type;
  qty : int;
  min_qty : int;
  leaves_qty : int;
  price : real;
  time : int;
  src : int;
  order_attr : order_attr;
  capacity : capacity;
  category : category;
  cross_restrict : cross_restrict;
  locate_found : bool;
  expiry_time : int;
}
 
type fill_price =
  | Known of real
  | Unknown
  | TOP of real

Core Functions

let mid_point mkt = (mkt.nbb +. mkt.nbo) /. 2.0
 
let non_ci ot = not (ot = PEGGED_CI || ot = LIMIT_CI)
 
let lessAggressive (side, lim_price, far_price) =
  if lim_price <. 0.0 then far_price
  else if side = BUY then Real.min lim_price far_price
  else Real.max lim_price far_price
 
let priority_price (side, o, mkt) =
  let calc_pegged_price =
    match o.peg with
    | FAR -> lessAggressive (side, o.price,
               (if side = BUY then mkt.nbo else mkt.nbb))
    | MID -> lessAggressive (side, o.price, mid_point mkt)
    | NEAR -> lessAggressive (side, o.price,
                (if side = BUY then mkt.nbb else mkt.nbo))
    | NO_PEG -> o.price
  in
  let calc_nbbo_capped_limit =
    if side = BUY then lessAggressive (BUY, o.price, mkt.nbo)
    else lessAggressive (SELL, o.price, mkt.nbb)
  in
  match o.order_type with
  | LIMIT -> calc_nbbo_capped_limit
  | MARKET -> if side = BUY then mkt.nbo else mkt.nbb
  | PEGGED -> calc_pegged_price
  | PEGGED_CI -> calc_pegged_price
  | LIMIT_CI -> calc_nbbo_capped_limit
  | FIRM_UP_PEGGED -> calc_pegged_price
  | FIRM_UP_LIMIT -> calc_nbbo_capped_limit

The Ranking Function

This is the heart of the matching engine — determining which of two orders should be filled first:

let order_higher_ranked (side, o1, o2, mkt) =
  let p_price1 = priority_price (side, o1, mkt) in
  let p_price2 = priority_price (side, o2, mkt) in
  let wins_price =
    if side = BUY then
      (if p_price1 >. p_price2 then 1
       else if p_price1 = p_price2 then 0
       else -1)
    else
      (if p_price1 <. p_price2 then 1
       else if p_price1 = p_price2 then 0
       else -1)
  in
  let wins_time =
    if o1.time < o2.time then 1
    else if o1.time = o2.time then 0
    else -1
  in
  if wins_price = 1 then true
  else if wins_price = -1 then false
  else (
    if not (non_ci o1.order_type) && not (non_ci o2.order_type) then
      o1.leaves_qty > o2.leaves_qty
    else if wins_time = 1 then true
    else if wins_time = -1 then false
    else (
      if non_ci o1.order_type then true
      else if not (non_ci o1.order_type) && non_ci o2.order_type then false
      else o1.leaves_qty > o2.leaves_qty
    )
  )

Priority is determined by a cascade of rules:

Price priority — better-priced orders rank higher
CI handling — at equal price, conditional indication orders are ranked by quantity
Time priority — earlier orders preferred at equal price
Regular vs. CI — non-CI orders preferred when quantity and time are equal

Verification

The Property: Transitivity of Ranking

A ranking function must be transitive for fair and predictable matching. We verify:

let rank_transitivity side o1 o2 o3 mkt =
  order_higher_ranked (side, o1, o2, mkt)
  && order_higher_ranked (side, o2, o3, mkt)
  ==> order_higher_ranked (side, o1, o3, mkt)
 
verify (fun side o1 o2 o3 mkt ->
  rank_transitivity side o1 o2 o3 mkt)

The Counterexample

ImandraX finds a concrete counterexample violating transitivity:

Order	Type	Time	Leaves Qty
o1	MARKET	1	1
o2	PEGGED_CI	2	1
o3	LIMIT_CI	0	0

With market conditions NBB = 8857, NBO = 8858 (mid = 8857.5):

order_higher_ranked(BUY, o1, o2, mkt) = true (price priority)
order_higher_ranked(BUY, o2, o3, mkt) = true (quantity priority between CIs)
order_higher_ranked(BUY, o1, o3, mkt) = false (CI with time=0 beats MARKET with time=1)

The transitivity violation arises from the interaction between different order type categories — each pairwise comparison uses different ranking criteria, creating a cycle.

Adding "Pretty" Constraints

We can also verify with realistic constraints on the orders:

let pretty mkt o1 o2 o3 =
  o1.leaves_qty <= o1.qty
  && o2.leaves_qty <= o2.qty
  && o3.leaves_qty <= o3.qty
  && o1.time >= 0 && o2.time >= 0 && o3.time >= 0
  && o1.price >. 0.0 && o2.price >. 0.0 && o3.price >. 0.0
  && o1.qty > 0 && o2.qty > 0 && o3.qty > 0
  && o1.leaves_qty >= 0 && o2.leaves_qty >= 0 && o3.leaves_qty >= 0
  && mkt.l_down >. 0.0 && mkt.nbb >. mkt.l_down
  && mkt.nbo >. mkt.nbb && mkt.l_up >. mkt.nbo
 
verify (fun side o1 o2 o3 mkt ->
  pretty mkt o1 o2 o3
  ==> rank_transitivity side o1 o2 o3 mkt)
(* Still refuted — the bug persists even with realistic constraints *)

Results

The intransitivity flaw demonstrates why machine-readable, formally specified financial algorithms matter:

Without formal verification: This bug could persist in production indefinitely. No amount of random testing would reliably find it — the counterexample requires a specific combination of three order types with particular market conditions.
With ImandraX: The bug was found automatically in seconds, with a concrete, minimal counterexample that developers can immediately understand and reproduce.

Real Production System

Verified against UBS's actual SEC Form ATS submission — not a toy model.

Automated Discovery

The transitivity violation was found automatically, with a concrete counterexample produced in seconds.

Industry Recognition

Won first place in the UBS Future of Finance Challenge across 620 companies from 52 countries.

References

2017 Lecture Notes in AI — Formal verification of financial algorithms