# CS2: Provably Correct Implementations of Density Functional Approximations

> **NSF 01002526DB NSF RESEARCH & RELATED ACTIVIT** · University of California-Davis (CA) · $625,840

## Abstract

Density Functional Theory (DFT) is a phenomenally successful approach to finding approximate solutions to the Schrodinger equation, the fundamental equation that describes the quantum behavior of atoms and molecules. The fundamental results of Kohn, Hohenberg, and Sham showed that the ground-state energy from the Schrodinger equation is a unique functional of the electron density and subsequently reduced solving a complicated many-body problem to finding a consistent solution to a set of single-particle equations. However, the exact density functional is not known and scientists have developed hundreds of density functional approximations (DFAs). Choosing a DFA is perhaps the most important decision when performing a DFT calculation. The project's novelties are in using formal methods to ensure that the implementation of a DFA is provably correct. DFT calculations are widely used in a number of scientific and engineering fields, including solid state physics, computational chemistry, and materials science. Consequently, the project's impacts are in improving the correctness of scientific software in these application domains. 

The key insight of the project is that each DFA is a mathematical function with a known, albeit complicated, analytical form, and, hence, can be analyzed using formal-methods techniques such as Satisfiability Modulo Theory (SMT) solvers. The project will automatically verify whether a DFA implementation satisfies DFT exact conditions (known analyti

## Key facts

- **NSF award ID:** 2446223
- **Awardee organization:** University of California-Davis (CA)
- **SAM.gov UEI:** TX2DAGQPENZ5
- **PI:** Aditya V Thakur
- **Primary program:** 01002526DB NSF RESEARCH & RELATED ACTIVIT
- **All programs:** —
- **Estimated total:** $625,840
- **Funds obligated:** $625,840
- **Transaction type:** Standard Grant
- **Period:** 06/15/2025 → 05/31/2029

## Primary source

NSF Award Search: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2446223

## Citation

> US National Science Foundation, Award 2446223, CS2: Provably Correct Implementations of Density Functional Approximations. Retrieved via AI Analytics 2026-06-08 from https://api.ai-analytics.org/grant/nsf/2446223. Licensed CC0.

---

*[NSF Awards dataset](/datasets/nsf-awards) · CC0 1.0*