An evidence ledger for a proprietary solver: claim–artefact correspondence under verification without disclosure.
K. Lekola. Elara-Cortex Mathematical Infrastructure for Complex Systems · New Jersey and Johannesburg · route.elara-cortex.com
1 · The verification principle
A proprietary method cannot ask to be trusted; it can only ask to be checked. Each published Elara-Cortex result therefore ships in one of four evidence classes, in descending order of formal strength, and no claim is published outside these classes:
| Class | Instrument | What the reader re-checks |
|---|---|---|
| Machine-checked statement | Z3 SMT solver (negation returned UNSAT); Dafny verified lemmas | The certificate and the encoded statement |
| Solution certificate | Explicit routes with recomputed cost | Feasibility and cost, from the public instance file and arithmetic |
| Measured benchmark | Public instances, published baselines, stated budgets, fixed seeds | The same run, reproduced from one command or through the public API |
| Public registry | Third-party leaderboard data (frozen and archived) | Every figure, directly on the registry |
Scope of disclosure. This ledger discloses results, protocols, budgets, baselines and certificates, everything needed to verify the claims. It does not disclose the method. That posture is standard for commercial solvers; it is strengthened here by certificates.
2 · Certified optimality
On capacitated vehicle-routing instances small enough for an exact solver, the provable global optimum was computed with the Z3 theorem prover (the certificate being UNSAT on "a cheaper feasible tour exists"). The production engine reaches that proven optimum on every such instance:
| Customers | Z3 proven optimum | Engine | Verdict |
|---|---|---|---|
| 6 | 359 | 359 | optimal |
| 7 | 355 | 355 | optimal |
| 8 | 386 | 386 | optimal |
| 9 | 381 | 381 | optimal |
| 10 | 296 | 296 | optimal |
| Match | 5 / 5 | Z3-certified |
Where optimality is provable, the engine is provably optimal. Beyond the size an exact method can certify (the problem is NP-hard), results are reported as gap-at-budget against the community's best-known solutions (Section 3).
3 · Comparative benchmark results
Full protocol, tables and solution certificates are in technical report TR-2026-01. The headline results, each carried by a certificate:
| Benchmark | Elara result | Baseline result | Outcome |
|---|---|---|---|
| CVRPLIB X-instances, 100–512 customers (9 instances) | mean gap +3.05% to best-known, ≤5 s single-threaded | Google OR-Tools (guided local search): +3.6% to +16.1%, 15–20 s (run on 6 of the 9) | Elara ahead on every instance where both were run (6 of 6); a lower best-known gap on all 9 |
| Solomon / Gehring–Homberger time windows (5 instances) | all customers served; mean distance gap +3.1%; 0.2% on C101 and C1_2_1 | under our own time-window encoding (which we do not certify as a fair head-to-head) OR-Tools returned incomplete solutions on 4 of 5 within 120 s | Elara serves all; the certified comparison is reported against best-known only |
| Provable-optimum instances (5 instances) | matches the certified optimum 5 / 5 | — | optimal, with certificate |
Every solution behind these rows is published as an explicit route list (solution_certificates.json: 123 CVRP routes, 91 VRPTW routes); re-verifying one requires only the public instance file and arithmetic.
4 · System-correctness properties
The service is engineered so that a delivered answer cannot bypass verification. Two independent guards enforce this: the engine repairs every solution to feasibility before returning, and the endpoint re-checks the result and refuses with an honest error rather than deliver an answer that fails its own certificate. The request lifecycle is modelled and verified as a state machine; the adversarial review method is documented in TR-2026-03.
| Property | Verification | Measured basis |
|---|---|---|
| Delivery implies feasibility (no bypass path) | state-machine reachability proof: removing the self-check gate makes the delivered state unreachable | moat_state_machine.json |
| Termination (no deadlock) | absorbing-chain analysis; absorption probability 1, ≈3.9 expected steps | moat_state_machine.json |
| Construction invariant | 0 infeasible outputs in 5 000 adversarial constructions | artifacts test battery |
| Certificate honesty | 0 discrepancies in 500 independent ground-truth recomputations | red-team ledger |
| Hostile-input robustness | 25/25 malformed-input classes returned typed errors, zero crashes; system-wide battery with zero server errors | fragility_battery.json |
| Adversarial review closure | every enumerated attack line closed, each closure certified independently by Z3 and by Dafny, zero disagreements | adversarial review reports (TR-2026-03) |
5 · Operational measurements
Measured through the production API on real published data (protocols in TR-2026-01 §7 and the enterprise evidence page):
| Measurement | Result |
|---|---|
| Plan a 200-stop, 10-vehicle day | 4.6 ms |
| Replan after five cancellations + three urgent insertions across five moving vehicles | ≈1.2 ms |
| Reassign 38 outstanding stops after a vehicle breakdown | ≈0.8 ms |
| Ten real airline route networks (OpenFlights): valid aircraft rotations + disruption recovery | 10 / 10 valid; recovery ≈1 s per carrier scenario |
| Live 843-station fleet feed (public GBFS): rebalancing plan + live replan | plan 3.0 s; replan ≈1 ms; re-verified for coverage, capacity and cost |
6 · Data compression and integrity
The same mathematical framework carries the data layer. Results below are measured on the stated corpus and machine; the comparison tools are run identically on the same inputs (TR-2026-02 §6):
| Measurement | Result |
|---|---|
| Lossless compression of the 162 MB log | 93% reduction (14.4× vs raw): one third smaller than gzip, 6% smaller than Brotli on this corpus; never larger than either on any tested input |
| Round-trip fidelity | byte-for-byte identical, SHA-256 verified on every file |
| Integrity-check throughput (own construction) | 30 GB/s, vs xxHash 21 GB/s and SHA-256 0.49 GB/s on the same machine |
| Route-update deltas on a road change | 80.1% transmission saved on the measured route (186 B vs 935 B), checksum-verified rebuild |
7 · The public mathematical track record
The founder's contribution to the Great Internet Mersenne Prime Search (GIMPS) is analysed in a separate paper with eight machine-checked statements over the frozen public leaderboard (the analysis · PDF). The certified forms, stated exactly, with the paper's own counterexample register of what may not be claimed, include: an archived participation-day double first place (highest success-per-attempt among visible members with a success, and the fastest 24-hour rise on the board); sixth of 309 members-with-a-success on the all-time table by attempts-per-success; contribution density at least 3.8× the board's attempt-weighted average (deep-assignment specialists run higher; see the analysis's own threats-to-validity); and a Pareto-dominance theorem certified for every non-negative weighting of the board's two goods. A standing pre-registration offer converts the analysis into a falsifiable forward experiment.
8 · The ledger: claim → artefact
| Claim | Artefact | Re-verification path |
|---|---|---|
| Optimal where provable, 5/5 | z3_exact_fair.json | Re-run the SMT encoding; compare certificates |
| Ahead of OR-Tools on every instance where both were run (CVRPLIB-X) | final_banked.json + solution_certificates.json | Recompute route costs from public instances; re-run the baseline |
| Time windows: all customers served; baseline incomplete 4/5 | ortools_vrptw_120s.json + vrptw_validated.json | Replay time windows arc-by-arc from certificates |
| Delivery-implies-feasibility; termination; no-bypass | moat_state_machine.json | Check the transition matrix and reachability argument (TR-2026-03) |
| 0/5000 construction invariant; 0 certificate lies/500 | red-team and construction batteries | Re-run the battery through the public API |
| Adversarial closure, dual-certified, 0 disagreements | adversarial review reports | Audit each attack line against its Z3/Dafny closure (TR-2026-03) |
| ms-scale replanning on live data | real_data_proofs.json, multi_airline_proofs.json | Re-run on the public OpenFlights / GBFS feeds with a free key |
| Compression and integrity results | bench_field outputs | One command re-runs the field on your own machine (TR-2026-02 §7) |
| GIMPS certified theorems T0–T7 | z3_gimps_story_receipt.json + frozen dataset | Open the public registry; re-run the Z3 scripts (available on request) |
9 · Reproduction and challenge protocol
Registered users (free 7-day key, route.elara-cortex.com/developers) can submit any capacitated or time-window routing instance to POST /v1/solve and receive a solution certificate: explicit routes, the cost, and an in-response verification block re-checking coverage, capacity and recomputed cost. The same instance can be run through OR-Tools, Gurobi, Hexaly or an in-house solver and compared like-for-like. A standing challenge is open on any metric on this ledger: hello@elara-cortex.com. Where a submitted counterexample survives verification, the ledger is corrected in public.
9.1 · Live re-verification (checkable right now, no key)
The claims in this ledger are backed by stored artefacts and are additionally re-verifiable at any
time, without an account, through the public endpoint. POST /v1/demo/solve runs the real
production engine on a small instance and returns a solution together with an in-response certificate the
caller re-checks (coverage, capacity, recomputed cost); by construction, the engine does not return
that certificate on an invalid solution. The airline operations
console exercises the same engine on live data: on each recovery it calls /v1/demo/solve
and shows the engine's measured solve time and verified certificate, alongside real aircraft
positions from a live ADS-B feed for the selected carrier. A reader who wants a receipt need not trust
a stored file; they can produce a fresh, self-verified one in their own browser.
Limitations
- The comparative set is nine CVRP and five VRPTW instances; the full suites and multi-seed dispersion are named future work in TR-2026-01 §8 and are in progress.
- Commercial solvers are not yet in the baseline; the free, open-source solver Google OR-Tools is used as the public baseline.
- Artefacts listed in Table 7 are published with the series or available on request where they embed third-party data; each report states which.
References
- de Moura, L., & Bjørner, N. (2008). Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 4963, 337–340.
- Leino, K. R. M. (2010). Dafny: An automatic program verifier for functional correctness. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-16), LNCS 6355, 348–370.
- Uchoa, E., Pecin, D., Pessoa, A., Poggi, M., Vidal, T., & Subramanian, A. (2017). New benchmark instances for the capacitated vehicle routing problem. European Journal of Operational Research, 257(3), 845–858.
- Woltman, G., & Kurowski, S. (2024). Great Internet Mersenne Prime Search (GIMPS). https://www.mersenne.org
Data, receipts & series
Series: TR-2026-01 (benchmark paper) ·
TR-2026-02 (measured performance) ·
TR-2026-03 (correctness under adversarial review) ·
TR-2026-04 (local computation in navigation) ·
TR-2026-05 (comparison against consumer map APIs) ·
GIMPS significance analysis
© 2026 Elara-Cortex Mathematical Infrastructure for Complex Systems · New Jersey · Johannesburg ·
The Elara mathematical framework is proprietary; all materials needed for verification are public;
every result is measured, never simulated.