Why Business Decisions Need Formal Verification

A pricing ruleset reaches forty rules the way most systems reach anywhere: one request at a time. A promo for new accounts. A loyalty tier bonus. A carve-out for the one enterprise account whose contract predates the current pricing model. Every rule was reviewed. Every rule was tested. The ruleset has run in production for a year without an incident.

Then a support ticket arrives. A customer on the STANDARD tier with a small cart got no discount at all, and nobody can say whether that was intended. Someone reads all forty rules in order and comes back with the answer: nothing covers that combination. It was never a bug anyone wrote — it is a hole between rules that were each individually correct.

No test failed, because no test asked. No alert fired, because nothing errored. The system did exactly what the rules said. The rules said nothing about that case.

This post is about the defects that live in that silence, why testing and simulation structurally cannot reach them, and what it takes to answer the question they cannot: not what happened, but what could happen.

What a passing test doesn't prove

A test is an example. It picks one point in the input space and asserts the output there. A hundred tests are a hundred points.

The input space of a ruleset is not a hundred points. Four facts — a tier, a cart total over the non-negative reals, a country code, an account age in days — already put the combinations past enumeration. A suite samples them where the author was thinking, because the same person wrote the rule and the test in the same hour with the same mental model. The defects live where nobody was thinking, which is precisely where nobody wrote a test.

That gap exists in ordinary code too. Rulesets make it worse for a structural reason — they grow by accumulation. Rule 37 arrives from a different person, in a different quarter, under a different deadline than rule 6, and it is reviewed against its own intent rather than against the other thirty-nine rules, because that review is combinatorial and humans do it badly. The interaction surface grows quadratically while attention stays linear.

The ruleset ends up in a state that is common and rarely noticed: every rule is correct, and the set is not.

Three things that go wrong quietly

A ruleset develops three specific defects on its own, and none announce themselves.

Unreachable rules. A rule that can never fire. In LexQ, priority is an automatic 1..N ordering inside a version, and a mutex group with EXCLUSIVE resolution lets only one member win. Put a catch-all in that group at priority 6, and rules 7 through 12 are dead code that still shows up in the console and still gets edited by someone who believes it runs. Unreachability also comes from the fact domain itself — a condition requiring tier = 'GOLD' and tier = 'SILVER' at once is unsatisfiable whatever the traffic looks like.

Conflicts. Two rules whose conditions can be true at once and whose actions disagree. Two SET_FACT actions writing the same fact. A discount rule and a BLOCK that both match. Sometimes this is deliberate and a mutex group resolves it. Sometimes nobody noticed the overlap, and the outcome falls to whichever priority was assigned first, which is to say to the order two unrelated people filed their tickets.

Gaps. A region of the input space that no rule covers. This is the one from the opening scene. It produces no error and no log line. The decision comes back with nothing applied, indistinguishable from a decision where nothing was supposed to apply.

All three are facts about the ruleset, not about the traffic. They hold whether or not a single request has ever landed in them, which is why runtime observation cannot find them.

What simulation answers, and what it doesn't

Replaying real traffic is the strongest tool most teams have. LexQ's Impact Simulation runs a new rule version against historical execution records and reports what changed: match rates, metric deltas, per-rule statistics. Decision Replay does the same for a single decision, old and new outcome side by side. Every decision carries a trace of which rule fired, on what inputs, at what version, and that trace lands in an immutable audit trail. I have written before about why seeing the impact of a rule change before it ships is the job that made me build this, and about what it takes to prove after the fact which rule produced a given outcome.

Both are the same shape of answer: they cover inputs that exist. Simulation replays traffic you already received; an audit trail explains a decision that already happened. Neither says anything about the combination nobody has sent yet.

The gap from the opening scene is invisible to all of it. If no STANDARD customer with a small cart checked out during the replay window, the simulation is silent on that region — not "no problem found" but no observation at all, reported identically. The unreachable rule is worse: simulation shows it matching zero records, which is also what a correct rule covering a rare segment looks like.

So here is the line, and I would rather draw it myself than have a reader find it. LexQ today does the first job and not the second. Impact Simulation, Decision Replay, per-rule latency profiling, versioned rules with instant rollback, decision traces, an immutable audit trail: all of that exists and runs in production right now. Formal verification of a ruleset does not exist in LexQ. There is no verifier to open. Everything below this line is a problem definition and a design direction, not a feature you can use.

What formal verification does differently

The move is to stop sampling the input space and start describing it.

A rule condition is already a logical formula. tier = 'GOLD' AND cartTotal > 5000 is a conjunction of two constraints, one over a string domain and one over a numeric one. A ruleset is a set of those formulas plus the semantics deciding which wins — priority ordering, mutex groups, the catch-all whose empty condition matches everything.

Once conditions are formulas rather than code paths, the three defects turn into satisfiability questions, and satisfiability is a problem the research community has spent forty years making tractable. An SMT solver such as Z3 takes a first-order formula and does one of two things: finds an assignment that satisfies it, or proves none exists.

• Unreachable rule. Ask whether the rule's condition, conjoined with the negation of every higher-priority condition that would preempt it, is satisfiable. UNSAT means it can never fire under any input whatsoever.
• Conflict. Ask whether two rules with contradicting actions and no mutex separation can both be satisfied at once. If SAT, the solver hands back an input that triggers both.
• Gap. Ask whether the negation of the disjunction of every condition is satisfiable. If SAT, there is an uncovered region, and the solver names a point inside it.

A green suite says the cases I checked worked. UNSAT says no such case exists — not on the sample, but across the entire input space, including inputs that will not arrive for another three years.

The name I am claiming for this is LexQ Verify. The shape I have in mind for its output looks like this:

✅ No unreachable rules
⚠️  2 potential conflicts:
   "vip-discount" ∧ "loyalty-bonus"
   → Resolved by mutex group "promo-exclusive"
❌ 1 gap:
   tier=STANDARD, cartTotal < 5000 is uncovered

That block is a sketch of an output, not a screenshot of one. I am putting the name and the shape in public with no implementation behind them, because the problem deserves a vocabulary whether or not any one vendor ever gets to it. The industry has no accepted phrase for "this ruleset is provably free of unreachable branches", and that absence is part of why the defect keeps shipping.

Why nobody has built this for business rules

Engineers with real SMT experience are rare. The skill sits in compilers and verification research, and barely overlaps with the population building rule engines.

The compiler from a rule condition DSL down to SMT formulas is academic-grade design work. Facts are typed and mixed: strings over finite domains, unbounded numerics, booleans, arrays for membership tests. Modeling those faithfully is the smaller half. The larger half is that a ruleset's semantics are not only its conditions — priority ordering, mutex resolution, and MUTATE_FACT actions that change a fact mid-evaluation all shape which rule decides. A verifier that ignores ordering proves something true about a system nobody is running.

And the count of commercial rule engines shipping formal verification of the ruleset is zero. Not few. Zero. Every engine I looked at while writing a comparison of what self-hosted and managed engines actually give you operationally stops at authoring, execution, and some form of testing.

Now the part I won't dress up. Someone has done this, first and well. Amazon's Cedar has formal verification productized for authorization, built on Lean and automated reasoning, shipped and documented. On the technique itself LexQ is a follower, and pretending otherwise would be the kind of claim this blog does not get to make.

What is unclaimed is the other domain. Cedar verifies who can access what. LexQ verifies what decision will be made.

Those are different problems, and the difference is not marketing. When I wrote that a Decision Operations Platform is not authorization, the distinction was about scope. Formalization is where it turns technical. An authorization decision is largely boolean over an entity graph: principal, action, resource, allow or deny. A business decision produces values — a discount amount, a mutated running total, a blocked transfer, a proration over mixed arithmetic. "Can this principal read this document" and "is there a cart that triggers two contradictory discounts" are different formulas over different theories. The prior art is a head start on the technique and close to none on the domain. I took that comparison apart properly in a closer look at what Cedar proves and why decision rules are the harder target.

When you don't need this, and when you don't need LexQ

Formal verification of a ruleset is not free, and the honest cases against it are short.

Your ruleset is small and still. Five rules unchanged in two years fit in one person's head. Read them. A solver adds nothing a careful afternoon doesn't.

Your rules are disjoint by construction. If the ruleset is a lookup keyed on one field with one row per value, conflicts and unreachability are impossible by shape. Proof has nothing to do.

A wrong decision is cheap. If the worst outcome of a gap is a customer paying full price and emailing support, the cost is bounded. Proof is worth buying where the wrong answer is expensive, and not much elsewhere.

Then the broader case, about LexQ rather than verification. If your rules are still if-else branches inside a service and changing one means a pull request and a deploy, unreachable branches are not your problem yet — getting the decision out of the release cycle is. And if the decisions rarely change at all, you don't need a Decision Operations Platform either. Leave it in the if-else block. Pulling it out costs more than the branch will ever cost you.

LexQ is a Decision Operations Platform for engineering teams, and today its answer to "what will this rule change do" is Impact Simulation against real traffic — an answer about the inputs you have. What a ruleset does across every input it could ever receive is a different question with a known mathematical shape, and no commercial rule engine has answered it. That is what LexQ Verify names.

→ See what runs today — start free at lexq.io