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.

翻译：地球系统模型对于理解过去气候和预测未来情景至关重要。然而，这些模型因其庞大的代码库、广泛的开发者社区以及多样化的计算平台而具有高度复杂性，给软件质量保证带来了重大挑战。GPU和异构架构的日益普及进一步加剧了验证工作的难度。传统的验证方法通常依赖于比特级可复现性，但这并非总是可行，尤其是在新编译器或硬件环境下。另一方面，人工专家评估则具有主观性强且耗时长的特点。形式化方法提供了一种数学上严谨的替代方案，但由于缺乏针对气候模型的特定表示方法和工具，其在ESM开发中的应用一直受限。本文主张在气候建模中更广泛地采用形式化方法。具体而言，我们识别了ESM中特别适合进行形式化规范的关键方面，并引入了为定制化框架设计的抽象方法。为展示该方法，我们通过一个案例研究，使用CIVL模型检查器对海洋混合参数化方案中的错误修复进行了形式化验证。我们的目标是开发易于使用的领域特定形式化工具，以增强模型可信度，并支持更高效、更可靠的ESM开发。