Formal Verification for Climate Model Accuracy

ISEF Category: Mathematics

Subcategory: Other  ·  Difficulty: Advanced  ·  Setup: University Lab  ·  Time: Full Year

The Hook

A tiny rounding error can snowball into a bad climate prediction. That makes precision a math problem, not just a coding problem. In this project, you ask whether a small interval-arithmetic library can safely bound the true answer. Then you test it on a reduced climate model that is simple enough to verify, but still meaningful.

What Is It?

Formal verification means proving that code does what you claim it does. Instead of hoping your program is correct because it passed a few tests, you write a mathematical proof that covers every valid input. In this project, the code under review is a small interval-arithmetic library. Interval arithmetic stores a lower and upper bound instead of one exact number, so the real value should stay somewhere inside the interval after each calculation.

Think of it like packing a suitcase with extra room so nothing important gets left out. If you add two uncertain numbers, the result should be a new interval wide enough to contain every possible true sum. A good library keeps those bounds honest. If the bounds are too tight, the real answer can slip out. If they are too loose, the result becomes less useful for climate emulation.

The climate piece comes from a reduced 0-D energy-balance model. That kind of model tracks one average temperature for the whole planet, instead of simulating every grid cell. It is simple, but it still depends on nonlinear math and repeated numerical updates. That makes it a good test bed for checking whether your verified interval code can protect emulator precision.

Why This Is a Good Topic

This topic works well for a science fair because it has a clear yes-or-no core question, and it connects pure math to a real modeling problem. You can test whether the code’s guarantees match the behavior you expect from the equations, then measure how interval width changes as the model runs. You also get room to learn proof writing, numerical error, and model validation, which are valuable research skills. The project feels advanced, but the model can stay small enough for a student to manage with careful scope.

Research Questions

• How does the choice of interval-splitting rule affect the width of the final temperature bounds in a 0-D energy-balance model?
• What is the effect of floating-point rounding mode assumptions on the proof obligations for the interval-arithmetic library?
• Does a formally verified interval implementation produce tighter or looser bounds than a reference implementation on the same reduced climate model?
• To what extent does increasing the number of time steps widen the interval bounds in the emulator?
• Which nonlinear term in the energy-balance model contributes most to bound growth under interval arithmetic?
• How does changing the proof specification for addition and multiplication affect the number of verification steps needed in Coq?

Basic Materials

• Laptop with a modern processor and at least 16 GB RAM.
• Coq installed on your computer.
• A text editor or IDE with Coq support, such as VS Code with the Coq extension.
• A reference on interval arithmetic, such as a university lecture note or textbook chapter.
• A copy of a simple 0-D energy-balance model in plain mathematical form.
• Spreadsheet software or Python for plotting interval widths and model outputs.
• Notebook for proof notes, theorem statements, and failed attempts.

Advanced Materials

• University Linux workstation or high-end laptop.
• Coq with required libraries for real analysis or program verification.
• Optional extraction toolchain for comparing verified code with executable versions.
• Python with NumPy and Matplotlib for experiments on emulator error growth.
• Version control software such as Git for tracking proof changes.
• Access to a climate modeling mentor or faculty member for checking the model assumptions.
• Research papers on interval analysis, verified numerics, and reduced climate models.

Software & Tools

• Coq: Lets you write the formal proof that the interval library satisfies its correctness claims.
• Git: Tracks proof changes, failed lemmas, and working versions of the library.
• Python: Helps you compare interval widths, plot error growth, and organize test cases.
• Matplotlib: Plots how uncertainty changes across model steps and parameter choices.
• VS Code: Gives you a clean editor for proof scripts and model notes.

Experiment Steps

1. Define the exact correctness claim you want to prove for each interval operation.
2. Reduce the climate model to a small set of equations that still exposes rounding and bound growth.
3. Identify the assumptions your proof will need about ordering, rounding, and real-number operations.
4. Build the smallest verified interval core first, then extend it to the operations used by the model.
5. Design comparison tests that check the verified code against high-precision numerical results.
6. Measure how interval width changes as you vary model structure, time stepping, or proof assumptions.

Common Pitfalls

• Trying to verify the whole climate model at once, which usually makes the proof too large for a first project.
• Mixing up real-number math and floating-point math, which breaks the link between the proof and the code.
• Defining interval bounds too loosely, which makes the model output so wide that the result stops being useful.
• Forgetting to state assumptions about division or nonlinear functions, which leaves gaps in the proof.
• Comparing the verified code only to low-precision runs, which can hide bound errors and make the validation look better than it is.

What Makes This Competitive

A stronger project goes beyond proving a few operations correct. You can compare multiple interval strategies, measure how quickly uncertainty grows, and explain why one approach stays tighter than another. You can also test the library on more than one reduced climate equation set, then use careful error analysis to show where the proof helps most. That kind of design turns the project from a coding exercise into a real study of verified numerical reliability.

Project Variations

• Apply the same verification approach to a different reduced climate model, such as a one-box carbon cycle model.
• Compare interval arithmetic with affine arithmetic and test which one keeps tighter bounds in the same emulator.
• Focus on one nonlinear operation, such as exponentiation or division, and study how its proof affects the whole model.
• MIT OpenCourseWare: Search for courses in formal methods, programming languages, or verification to see how proof systems are structured.
• Coq Reference Manual: Look up the official documentation for syntax, tactics, and proof commands.
• Certified Programming with Dependent Types: Read selected chapters for a student-friendly path into Coq proofs.
• PubMed: Search for review articles on numerical error propagation only if you want a broader sense of how uncertainty affects scientific models.
• NASA Earth Science Division: Look for background material on climate modeling and simplified energy-balance models.

Learn More

• MIT OpenCourseWare: Search for formal methods, discrete mathematics, or programming languages courses for proof techniques and verification ideas.
• Coq Reference Manual: Use the official Coq documentation to learn tactics, theorem statements, and proof scripts.
• Certified Programming with Dependent Types: Read this book for a clear introduction to proof-based programming in Coq.
• arXiv: Search for papers on interval arithmetic, verified numerics, and machine-checked proofs.
• NASA Earth Science Division: Find background pages on energy-balance models and climate system basics.
• NOAA Climate.gov: Read accessible explanations of climate forcing, feedbacks, and simplified climate modeling.