[Submitted on 26 Sep 2026 (v1), revised 26 Sep 2026 (this version, v2), latest revision 26 Sep 2026 (v4)]
Title:Verified Terrain-Following Flight Planning in LeanExe
Abstract: A terrain-following planner must connect its discrete route choices to continuous clearance and motion bounds, and connect its implementation to that mathematical result. This report describes a LeanExe planner and Lean proofs of both connections. For every accepted nonempty terrain, the generated WebAssembly model terminates with exactly the source planner’s waypoint array and a continuously differentiable point-mass flight that satisfies the specified spatial clearance and component speed bounds, with bounded acceleration between waypoints and one-sided bounds at joins. The execution theorem assumes a valid caller heap, a borrowed input array, and sufficient allocation headroom within 64 MiB. The planner minimizes exact traversal time and then sampled altitude excess over a finite layered graph. The proof covers integer arithmetic, predecessor selection, parent reconstruction, polynomial motion, allocation, copying, and release. Inputs contain at most 64 elevations, and each interior station has 45 altitude–speed states. A rest-to-rest primitive proves feasibility for every accepted terrain. Identifying the decoded drone binary with the verified generated model remains a separate proof obligation. A self-contained account of LeanExe describes its language, artifact-verification method, and the scalar and bounded-loop compiler-correctness theorem now present on the main branch.
| Comments: | 17 pages, five plotted runs in four figures |
| Subjects: | Logic in Computer Science (cs.LO); Programming Languages (cs.PL) |
| Cite as: | marXiv:2609.00019 [cs.LO] (or marXiv:2609.00019v2 [cs.LO] for this version) |
Submission history
[v1] Sat, 26 Sep 2026 13:51:50 UTC (438 KB)
[v2] Sat, 26 Sep 2026 14:01:39 UTC (439 KB)
[v3] Sat, 26 Sep 2026 14:07:36 UTC (436 KB)
[v4] Sat, 26 Sep 2026 14:16:30 UTC (440 KB)