Every double charge, every reconciliation break, every "impossible" balance ends the same way: engineers sort a million events by timestamp and argue about one millisecond. Orderproof replaces the argument with a verdict — SAFE, VIOLATED, or an honest AMBIGUOUS — and hands you the smallest set of events that forces it.
Each scenario is a real structure: services, clocks, message ids, a declared skew bound. Nothing is hard-coded — the verdict on the right is computed in this request by searching admissible orderings.
The question finance actually asks — "did we take money we were not owed?" — is a question about orderings. Databases of spans cannot answer it, because they treat timestamps as truth.
A trace with n concurrent events has exponentially many orders consistent with causality. Orderproof searches the space, not a sample, and keeps the two facts that matter: is there a safe order, and is there any order that breaks.
Dashboards force a binary. Real logs often cannot decide: the message id was dropped, the clock bound was a guess. Saying AMBIGUOUS, then telling you exactly what to instrument, is worth more than a confident wrong number.
A VIOLATED verdict comes with a deletion-minimized core: the smallest subset of events that still forces the failure. That is the difference between "somewhere in 1M events" and a three-line incident report you can hand to an auditor.
This is arithmetic and search. No LLM, no scoring, no "AI-powered" anything. That is deliberate: a verdict that cannot be audited is not a verdict.
Program order within a service, plus send/receive pairs on message ids. This yields a happens-before DAG that stays correct while the wall clocks are wrong.
Each clock reading c is only known to lie in [c−B, c+B]. If the latest possible time of A is before the earliest possible time of B, then A precedes B in every admissible order.
Every prefix of an admissible order is a downset of the DAG. The balance at a downset is fixed — independent of the order taken to reach it. So the whole question collapses to reachability over downsets.
If no negative downset is reachable: SAFE. If no safe path exists: VIOLATED. Otherwise AMBIGUOUS. For violations, delete events greedily while the violation persists.
Exact search is bounded at 24 events and 400k downsets per request; beyond that the engine samples orders and marks the answer approximate. The demo traces are all exact.
Send the events you already emit. Get a verdict, a witness, and the wall-clock counterfactual for the incident review.
# ask the engine curl -s https://orderproof.toyou.gr/api/audit \ -H 'content-type: application/json' \ -d '{ "initial": 0, "skew": 250, "events": [ {"id":"led-1","svc":"ledger","type":"credit", "clock":1009,"seq":0,"delta":120}, {"id":"led-2","svc":"ledger","type":"debit", "clock":1002,"seq":1,"delta":-120} ] }'
// what comes back { "verdict": "SAFE", "reason": "Every admissible ordering keeps the balance at or above 0...", "wallClock": { "verdict": "VIOLATED", "minBalance": -120 }, "stats": { "states": 3, "ms": 0.6 } }
A product that hides its assumptions is selling confidence, not truth. These are the three that matter.
Without send/receive pairs there is no partial order, and the honest answer collapses to AMBIGUOUS. Instrumenting those ids is the actual adoption work — the engine is the easy part.
Exact downset search is exponential in the worst case. Incident-sized windows are fast; "audit every event forever" is not, and the engine says so instead of pretending.
Every verdict is relative to a declared bound B. Set B to zero and you get confident nonsense. The engine detects when B is provably too small and refuses the trace rather than lying.