Towards Domain-Specific Formal Methods for Earth System Modeling @ ETAPS 2025
I had the pleasure of presenting our latest work, “Specification and Verification for Climate Modeling: Formalization Leading to Impactful Tooling”, at the Verifying Scientific Software (VSS) workshop at ETAPS 2025 in Hamilton, Ontario.
In this paper, we advocate for domain-specific formal methods in Earth system modeling (ESM), highlighting how abstractions tailored to model coupling, spatio-temporal dynamics, and numerical methods can help improve software quality and scientific reliability. Our case study demonstrates how lightweight formal verification tools like CIVL can catch subtle defects in ocean model parameterizations and validate bug fixes efficiently—providing practical benefits even in complex, HPC-scale scientific codes.
Co-authors: Allison Baker (NCAR), John Baugh (NCSU), Ganesh Gopalakrishnan (Utah), and Stephen Siegel (Delaware)