Customizable Route Planning, Machine-Checked🔗

This is the machine-checked companion to the CRP demo and its white paper: a Lean 4 development, built on Mathlib, that proves the mathematics Customizable Route Planning rests on — and then gives a verified implementation of the whole query, customization and overlay search included, proved to return true shortest-path distances.

Every signature and docstring on this page is pulled from the compiled development while the page is built. Nothing is transcribed: renaming a theorem breaks this page's build, so what you read cannot drift from what is proved. Every declaration rests on Lean's three standard axioms and nothing else — no sorry anywhere — and that is enforced mechanically, by an audit described at the end.

One limit, stated up front and again at the end: none of this establishes that the TypeScript running the demo is the verified program. A differential test runs both over the same city-scale graph and compares every distance; that is evidence, not proof, and the distinction is kept sharp throughout.