Density Functional Theory (DFT) is used extensively in the computation of electronic properties of matter, with various applications. Approximating the exchange-correlation (XC) functional is the key to the Kohn-Sham DFT approach, the basis of most DFT calculations. The choice of this density functional approximation (DFA) depends crucially on the particular system under study, which has resulted in the development of hundreds of DFAs. Though the exact density functional is not known, researchers have discovered analytical properties of this exact functional. Furthermore, these exact conditions are used when designing DFAs. We present XCVerifier, the first approach for verifying whether a DFA implementation satisfies the DFT exact conditions. XCVerifier was evaluated on five DFAs from the popular Libxc library and seven exact conditions from recent work. XCVerifier was able to verify or find violations for a majority of the DFA/condition pairs, demonstrating the feasibility of using formal methods to verify DFA implementations.

翻译：密度泛函理论（DFT）被广泛应用于物质电子性质的计算，具有多种应用场景。在Kohn-Sham DFT方法（大多数DFT计算的基础）中，交换-关联（XC）泛函的近似是关键所在。密度泛函近似（DFA）的选择主要取决于所研究的特定体系，这导致了数百种DFA的发展。虽然精确的密度泛函尚未可知，但研究人员已发现该精确泛函的解析性质。此外，这些精确条件在设计DFA时被广泛采用。本文提出了XCVerifier，这是首个用于验证DFA实现是否满足DFT精确条件的方法。我们在流行的Libxc库中选取了五种DFA，并结合近期研究中的七个精确条件对XCVerifier进行了评估。XCVerifier能够对大多数DFA/条件组合完成验证或发现违规情况，这证明了使用形式化方法验证DFA实现的可行性。