Why Logic-First

LLMs are extremely good at producing code. What they cannot do is tell you, with certainty, what the code they produced actually does across all of its inputs. Their reasoning is statistical: they sample likely paths. A missed path is silent.

Automated reasoning answers a different kind of question. Given a formal model of a system, it can prove a property holds for every input, or hand back a concrete input where it fails. There is no sampling and no confidence score. The answer comes with either a proof object you can check independently, or a counterexample you can run.

That distinction matters most for logic where being wrong is expensive: pricing and fee schedules, order matching, access control, compliance classification, state machines with many transitions.

A worked case: a ranking function that isn't one

Some years ago Imandra analysed the order-ranking logic that a large investment bank had described to the SEC in its Form ATS filing, the document defining how its dark pool prioritises orders. Encoded faithfully into IML, the central function was order_higher_ranked (side, o1, o2, mkt).

Any ranking function has to be transitive: if a ranks above b and b ranks above c, then a must rank above c. This is not a domain-specific nicety. It is what makes sorting meaningful at all. A comparison function that violates it, handed to an ordinary sort routine, produces effectively arbitrary output while appearing to work.

Stating the property is a few lines:

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)

ImandraX did not prove it. It refuted it, and returned three concrete orders and a market state that break transitivity: a specific triple that no test suite contained and no reviewer had spotted, in logic that had already cleared a regulatory filing.

Two things are worth drawing out. First, the counterexample was computed from the logic, not retrieved from similar examples or found by random search. Second, the flaw lived in the specification, not in a line of code: the prose in the filing described a ranking that cannot exist. That is the class of problem this approach is for.

A second case: forty-four ways to price a trade

The UBS analysis asked a yes/no question and got a counterexample. The other mode is exhaustive enumeration, and it scales differently than intuition suggests.

Analysing the pricing logic for one segment of the SIX Swiss Exchange produced 44 regions. Each region is one distinct behaviour, with its own input conditions and its own exact output. One of them:

Constraints:
- (List.hd ob.buys).order_qty = (List.hd ob.sells).order_qty
- (List.hd ob.buys).order_type = Market
- (List.hd ob.sells).order_type = Market
- (List.hd (List.tl ob.buys)).order_type <> Market
- ref_price >= (List.hd (List.tl ob.buys)).order_price
- (List.hd (List.tl ob.sells)).order_type <> Market
- ref_price > (List.hd (List.tl ob.sells)).order_price
 
Invariant:
- F = Known (List.hd (List.tl ob.sells)).order_price

Reading it: List.hd ob.buys is the first order on the buy side and List.hd (List.tl ob.buys) the second, so this region covers order books where the top order on each side is a market order of matching quantity, the second order on each side is not, and the reference price sits above both. In that situation the price is the second sell order's price.

Forty-four of those, each proved, each with a concrete example input available. Enumerating them by hand is a day's careful work with a real chance of missing one. An LLM cannot produce this list at all, not because it is bad at reading code, but because the list is a mathematical consequence of the code rather than a plausible continuation of it.

Where to go next

• Region decomposition: run the analysis behind the SIX Swiss example on your own code
• Thinking formally: what makes a model easy to reason about
• Case studies: more analyses at length