Submission 193ee48ff712

Title:	Verified Terrain-Following Flight Planning in LeanExe
Authors:	Jamie Stephens
Subjects:	Logic in Computer Science (cs.LO); Programming Languages (cs.PL)
Replaces:	marXiv:2609.00019
Submitted:	Sat, 26 Sep 2026 09:16
PDF:	submitted PDF
Status:	accepted
Paper:	marXiv:2609.00019

Event log

Sat, 26 Sep 2026 14:16:30 UTC	submitted
Sat, 26 Sep 2026 14:16:30 UTC	review started
Sat, 26 Sep 2026 14:20:16 UTC	accepted

Review

Decision: accept

Accepted.

## Remarks

- Requirement 10, §3.3: “LeanExe uses the pinned Talos interpreter and proof libraries for WASM execution.”  Cite the Talos source and identify the pinned revision.  Reference [4] identifies the WebAssembly specification.
- Requirement 10, §3.3: “The independent core type-safety development proves preservation and progress for its own typed syntax and semantics.”  Identify the development and cite the relevant proofs.
- Requirement 12, Redundancy, §§1–2: “Relating a decoded drone binary to that model remains a separate proof obligation” and “A theorem identifying a decoded drone binary with that model remains a separate verification step” repeat the same limitation in consecutive sections.  Consolidate these scope statements.