Scientific computing sits at the heart of discovery across domains, from climate science and quantum chemistry to materials science and astrophysics. Yet, as our simulations grow more complex and our hardware more heterogeneous, the correctness of scientific software has become both more critical and more elusive. In this talk, I will explore how formal methods—ranging from lightweight static analysis to full mechanized proofs—can help us design, reason about, and verify scientific software with greater rigor and confidence.
Drawing from my recent research, I will discuss challenges and opportunities in applying formal verification techniques to numerical libraries that are foundational to scientific computing. I’ll share how formal methods can reveal subtle correctness issues such as instability, excessive numerical rounding, and violations of high-level mathematical specifications. I’ll also discuss what it means to make correctness a design-time concern, from developing verification infrastructure to defining meaningful formal specifications in the presence of approximation and uncertainty.
Ultimately, my aim is to spark a conversation about how we as a community can elevate correctness as a first-class concern in the scientific software stack, alongside performance and scalability. By bridging formal methods with scientific computing, we move toward a future where our simulations are not just fast, but also trustworthy.