NSF Research: Correctness for Scientific Computing Systems

The Correctness for Scientific Computing Systems (CS²) program is a joint initiative of the National Science Foundation (NSF) and the U.S. Department of Energy (DOE). It was established to address challenges critical to both DOE’s mission in high-performance scientific computing and NSF’s mission to advance broad scientific progress. This program emphasizes correctness in scientific computing, putting it on equal footing with performance as a core requirement for advancing computational science. The program recognizes that as computing hardware and software systems become more heterogeneous and complex, risks of incorrect outputs and flawed simulations increase, threatening the integrity of scientific discovery. Correctness in this context is defined as ensuring that scientific computing systems meet expected behavioral properties during execution, free from faulty behaviors such as numerical rounding errors, floating-point exceptions, data races, deadlocks, memory faults, and specification violations. The program also considers probabilistic or statistical definitions of correctness for applications that use randomized algorithms or uncertain data. The initiative stresses the importance of verification methods that are modular, end-to-end, and machine-checked, with correctness proofs grounded in formal logic and supported by both static and dynamic analyses. The overarching goal is to develop robust theories, methodologies, and tools to provide verified correctness across scientific applications. The CS² program requires close collaboration between researchers in two primary areas: scientific computing and formal reasoning. Scientific computing includes simulations of scientific theories, data management and analysis, and numerical libraries, while formal reasoning encompasses verification techniques, program analysis, type systems, abstract interpretation, concurrency, and mechanized theorem proving. Proposals must demonstrate expertise in both areas and include a collaboration plan showing continuous mutual engagement. Projects are expected to identify at least two critical modules from recognized high-performance applications and provide formal, machine-checked proofs of correctness for those modules. Although complete end-to-end verification of entire applications is not required, projects must outline long-term paths toward that goal. Funding for this program is jointly provided by NSF and DOE, with an anticipated total budget of $18 million over three years, divided equally between the two agencies. Approximately five awards are expected each year in fiscal years 2025, 2026, and 2027, with each award providing up to $800,000 for a duration of up to four years. DOE National Laboratories may receive up to $500,000 per year under this program. Funded projects must also budget for participation in CS² principal investigator meetings, which aim to build a new research community around verified scientific computing. Eligibility is restricted to U.S.-based organizations, including accredited institutions of higher education, independent non-profit research organizations, and DOE National Laboratories. Principal Investigators must hold a tenured, tenure-track, or full-time paid research or teaching appointment at an eligible U.S. institution, or be an employee of a DOE National Laboratory. Projects must include at least one investigator with expertise in scientific computing and one with expertise in formal methods. Individuals may participate in no more than two proposals per deadline and no more than two awards over the life of the program. Applications must be submitted through Research.gov or Grants.gov by the stated deadlines. Proposal preparation must follow the NSF Proposal and Award Policies and Procedures Guide. Specific requirements include sections on theories and methodologies, critical modules, and evaluation plans, as well as supplementary documents such as a collaboration plan, personnel list, and data management plan. DOE-affiliated proposals must include a separate budget justification for DOE review. The next deadlines are August 13, 2024, August 12, 2025, and August 11, 2026, with submissions due by 5:00 p.m. local time of the applicant’s organization. Program contacts include Dr. Anindya Banerjee (703-292-7885, cs2@nsf.gov), Dr. Damian Dechev (703-292-8910, cs2@nsf.gov), and Dr. Hal Finkel at DOE (301-903-1304, hal.finkel@science.doe.gov). Awardees will be expected to participate in annual reporting and community meetings, and to acknowledge NSF and DOE support in all project outputs. Reporting requirements include annual and final project reports to the funding agency, with information shared across NSF and DOE. Through this program, both agencies seek to ensure that future scientific computing systems are not only fast and scalable but also provably correct, thereby safeguarding the integrity of computational science across disciplines .