Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Specification and Verification for Climate Modeling: Formalization Leading to Impactful Tooling

Alper Altuntas, Allison H. Baker, John Baugh, Ganesh Gopalakrishnan, Stephen F. Siegel

TL;DR

Earth System Models (ESMs) are large, multi-component codes run on diverse hardware, making bitwise reproducibility-based verification impractical. The paper proposes domain-specific formal methods, including a Relational Spatio-Temporal Logic and lightweight tooling (notably CIVL-C), to specify and verify coupling, continuous-discrete interactions, and mesh handling in ESMs. A concrete case study on the KPP ocean-mixing parameterization demonstrates defect detection and automated verification, illustrating how such tooling can provide rapid, rigorous feedback beyond ad hoc testing. By outlining abstraction strategies and discussing GPU-scale considerations, the work argues for integrating formal reasoning into climate software workflows to improve reliability and efficiency on heterogeneous architectures.

Abstract

Earth System Models (ESMs) are critical for understanding past climates and projecting future scenarios. However, the complexity of these models, which include large code bases, a wide community of developers, and diverse computational platforms, poses significant challenges for software quality assurance. The increasing adoption of GPUs and heterogeneous architectures further complicates verification efforts. Traditional verification methods often rely on bitwise reproducibility, which is not always feasible, particularly under new compilers or hardware. Manual expert evaluation, on the other hand, is subjective and time-consuming. Formal methods offer a mathematically rigorous alternative, yet their application in ESM development has been limited due to the lack of climate model-specific representations and tools. Here, we advocate for the broader adoption of formal methods in climate modeling. In particular, we identify key aspects of ESMs that are well suited to formal specification and introduce abstraction approaches for a tailored framework. To demonstrate this approach, we present a case study using CIVL model checker to formally verify a bug fix in an ocean mixing parameterization scheme. Our goal is to develop accessible, domain-specific formal tools that enhance model confidence and support more efficient and reliable ESM development.

Specification and Verification for Climate Modeling: Formalization Leading to Impactful Tooling

TL;DR

Earth System Models (ESMs) are large, multi-component codes run on diverse hardware, making bitwise reproducibility-based verification impractical. The paper proposes domain-specific formal methods, including a Relational Spatio-Temporal Logic and lightweight tooling (notably CIVL-C), to specify and verify coupling, continuous-discrete interactions, and mesh handling in ESMs. A concrete case study on the KPP ocean-mixing parameterization demonstrates defect detection and automated verification, illustrating how such tooling can provide rapid, rigorous feedback beyond ad hoc testing. By outlining abstraction strategies and discussing GPU-scale considerations, the work argues for integrating formal reasoning into climate software workflows to improve reliability and efficiency on heterogeneous architectures.

Abstract

Earth System Models (ESMs) are critical for understanding past climates and projecting future scenarios. However, the complexity of these models, which include large code bases, a wide community of developers, and diverse computational platforms, poses significant challenges for software quality assurance. The increasing adoption of GPUs and heterogeneous architectures further complicates verification efforts. Traditional verification methods often rely on bitwise reproducibility, which is not always feasible, particularly under new compilers or hardware. Manual expert evaluation, on the other hand, is subjective and time-consuming. Formal methods offer a mathematically rigorous alternative, yet their application in ESM development has been limited due to the lack of climate model-specific representations and tools. Here, we advocate for the broader adoption of formal methods in climate modeling. In particular, we identify key aspects of ESMs that are well suited to formal specification and introduce abstraction approaches for a tailored framework. To demonstrate this approach, we present a case study using CIVL model checker to formally verify a bug fix in an ocean mixing parameterization scheme. Our goal is to develop accessible, domain-specific formal tools that enhance model confidence and support more efficient and reliable ESM development.
Paper Structure (17 sections, 4 figures)

This paper contains 17 sections, 4 figures.

Table of Contents

  1. Introduction
  2. Targeted Modeling Aspects
  3. Model Coupling
  4. Continuity and Discreteness
  5. Spatial Discretization
  6. Current verification and validation practices
  7. Scientific Methods
  8. Software Methods
  9. Formal Specification and Verification
  10. Towards a Relational Spatio-Temporal Logic
  11. Model Coupling and Concurrency
  12. Continuous and Instantaneous Processes
  13. Reals vs. Floating-Point Arithmetic
  14. Instantaneous events:
  15. Mesh representations
  16. ...and 2 more sections

Figures (4)

  • Figure 1: The components of the latest version of the Community Earth System Model (CESM3). Each component interacts with the rest of the system via the coupler in a hub-and-spoke structure lawrence2024cesm3.
  • Figure 2: The visualization of the Gulf Stream as simulated by the MIT General Circulation Model (MITgcm). The ocean flows are color-coded with sea surface temperature data. Adapted from menemenlis2008ecco2nasasvsgulfstream.
  • Figure 3: A tripolar grid. These are commonly used in ocean models to avoid singularities in open water by shifting the nominal pole onto land. Panel (a) illustrates the grid in index space, where the northern edge is periodically folded to create the tripolar stitch along the grid lines connecting the two red points (same geographical location) to the green point. Panel (b) displays the same grid in geographical coordinates, with the dark line between the singularity points indicating the tripolar stitch.
  • Figure 4: CIVL-C model of the KPP defect fix.