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