Papers › Shock with Confidence: Formal Proofs of Correctness for Hyperbolic Partial...
Shock with Confidence: Formal Proofs of Correctness for Hyperbolic Partial Differential Equation Solvers
Jonathan Gorard, Ammar Hakim
The archive published only this paper's code-link row. Authors, date and abstract are from arXiv's metadata (CC0), read from the Kaggle arXiv metadata snapshot of 2026-09-12 where its title matched the archive's; the title is the archive's.
First-order systems of hyperbolic partial differential equations (PDEs) occur ubiquitously throughout computational physics, commonly used in simulations of fluid turbulence, shock waves, electromagnetic interactions, and even general relativistic phenomena. Such equations are often challenging to solve numerically in the non-linear case, due to their tendency to form discontinuities even for smooth initial data, which can cause numerical algorithms to become unstable, violate conservation laws, or converge to physically incorrect solutions. In this paper, we introduce a new formal verification pipeline for such algorithms in Racket, which allows a user to construct a bespoke hyperbolic PDE solver for a specified equation system, generate low-level C code which verifiably implements that solver, and then produce formal proofs of various mathematical and physical correctness properties of the resulting implementation, including L^2 stability, flux conservation, and physical validity. We outline how these correctness proofs are generated, using a custom-built theorem-proving and automatic differentiation framework that fully respects the algebraic structure of floating-point arithmetic, and show how the resulting C code may either be used to run standalone simulations, or integrated into a larger computational multiphysics framework such as Gkeyll.
Code
Repository list and official/mentioned flags are the archive's, frozen 2025-07-28. Reachability, where shown, is from one Syntology probe window (2026-09-16 to 2026-09-18); repositories not probed show nothing. GitHub stars are not tracked.
Code Syntology ran Syntology
Not run by Syntology. Nothing on this page verifies that the listed code works.
Results from the paper archive 2025-07-28
No leaderboard rows for this paper in the archive.
Report a problem or propose a change · a person checks every report against the paper or source before anything changes; decisions are listed on /corrections