# Shock with Confidence: Formal Proofs of Correctness for Hyperbolic Partial Differential Equation Solvers

arXiv: https://arxiv.org/abs/2503.13877 · HTML: https://mlsanity.com/paper/2503.13877/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 18 Mar 2025.

## Built on by (most cited first, 2 of 2)

- [Report of the 2025 Workshop on Next-Generation Ecosystems for Scientific Computing: Harnessing Community, Software, and AI for Cross-Disciplinary Team Science](https://mlsanity.com/paper/2510.03413/) (2025)
- [BEACONS: Bounded-Error, Algebraically-Composable Neural Solvers for Partial Differential Equations](https://mlsanity.com/paper/2602.14853/) (2026)

## Abstract (arXiv)

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.