digital · infrastructure · family: the answer is in a field you’ve never heard of
noprooftherobotwillbehave
AI-enabled autonomous systems cannot be formally verified for safety
Problem statement
Cyber-physical systems are engineered systems built from, and dependent on, "the seamless integration of computation with physical processes and components." NSF's Cyber-Physical System Foundations and Connected Communities (CPS) program seeks foundational advances in all areas of such systems, "including artificial intelligence for cyber-physical systems." Its foundational research track (CPS-FR) lists among its areas of interest "AI-enabled autonomy," safe learning and adaptive systems, and "formal methods for verification and assurance of cyber-physical systems, including those that integrate AI." In other words, how to verify and assure a cyber-physical system that has AI inside it is one of the areas in which this track invites foundational research. The program page says research on such systems benefits from considering "the dynamic and unpredictable nature of physical systems," along with the continuously evolving context of user behavior and environmental conditions. The solicitation and the program page name the research area; they do not describe how far current verification methods fall short.
Why this matters
The CPS program says its aim is "reliable, resilient cyber-physical systems that enhance quality of life and community well-being," and it describes its connected-community work as "emphasizing safety, wellness, security, efficiency, dependability and resilience." The program's community-inspired track lists civil infrastructure, disaster response, transportation, manufacturing, power systems, and agriculture among its areas of particular interest. The foundational track also lists among its areas of interest "security, privacy and trustworthiness for ensuring robust operations under adversarial and failure conditions."
What’s been tried and why it hasn’t worked
The two NSF sources are funding calls, and they do not review earlier approaches or say why those approaches fell short. What they do show is how the research has been organized. Cyber-physical systems research previously had its own solicitation (NSF 24-581), which NSF 25-543 replaces; the new solicitation lists the CPS program among the programs it added to the Future CoRe set. Within that set, a different program also names verification: Software and Hardware Foundations supports "foundational research in the design, verification, operation, utilization and evaluation of computer hardware and software," while the solicitation says the CPS program supports "convergent research," and the program page lists formal methods for AI-integrated systems as one area of interest among many. The CPS-FR track says validation of research contributions "through prototyping or testing is strongly encouraged"; the sources do not say whether testing is enough to assure a system that includes AI.
What would unlock progress
The CPS-FR track lists the areas it is interested in, among them: "formal methods for verification and assurance of cyber-physical systems, including those that integrate AI"; safe learning and adaptive systems; "novel techniques for learning, planning, and optimization in uncertain, real-time environments"; and security, privacy and trustworthiness for robust operation under adversarial and failure conditions. The page says projects in this track generate "broadly applicable theories, algorithms, methods, and tools that can enable robust cyber-physical systems across multiple domains," and that validating those contributions through prototyping or testing is strongly encouraged.
Entry points for student teams
A student team could implement and compare existing neural network verification tools (e.g., Marabou, alpha-beta-CROWN, nnenum) on a small autonomous decision-making task (e.g., a simplified lane-keeping controller), benchmarking scalability limits and identifying where current tools break down. This is a feasible software engineering/formal methods project. Alternatively, a team could design a runtime monitoring system for a specific autonomous behavior (e.g., obstacle avoidance) that detects when the neural network's inputs fall outside its verified operating envelope and triggers a safe fallback controller.
Genes
Structural cousins: stuck the same way, in other fields
Sources
"Computer and Information Science and Engineering (CISE): Future Computing Research (Future CoRe)," NSF Program Solicitation NSF 25-543, CPS-FR track. (accessed 2026-02-10). Supplemented with the Cyber-Physical System Foundations and Connected Communities (CPS) program page: go to source 1 ↗ go to source 2 ↗
Working notes
Notes made while writing and checking this brief, shown as written. They use working shorthand.
- NSF 25-543 (Future CoRe), posted July 25, 2025, replaces three earlier solicitations (NSF 24-589, NSF 24-581 and NSF 25-527) and adds the CPS program to the Future CoRe programs. The CPS-FR track is the program's foundational research track; formal methods for verification and assurance of cyber-physical systems, including those that integrate AI, is one of its listed areas of interest.
- Cross-domain connection: the verification gap is structurally similar to the cascading infrastructure failure problem — both involve reasoning about complex system behavior that emerges from component interactions and resists traditional analysis.
- The "newly-created" temporal tag reflects this project's own reading that the problem follows from the recent use of AI inside cyber-physical systems; the NSF sources do not say when the problem arose.
- Related communities: the CPS program page describes its connected-community research as "inherently multidisciplinary" and lists four other NSF directorates as interdisciplinary collaborators on the CPS program: Engineering (ENG), Social, Behavioral and Economic Sciences (SBE), Geosciences (GEO), and STEM Education (EDU).
Reconciliation 2026-10-01: Fact repair after reading the whole write-up against both sources it names. Both were fetched directly from nsf.gov on 2026-10-01 and read in full: the NSF 25-543 program solicitation (https://www.nsf.gov/funding/opportunities/future-core-computer-information-science-engineering-future-computing/nsf25-543/solicitation) and the Cyber-Physical System Foundations and Connected Communities (CPS) program page (https://www.nsf.gov/funding/opportunities/cps-cyber-physical-system-foundations-connected-communities). Both are funding calls. The solicitation gives the CPS program two sentences of description; the program page gives the CPS-FR track one paragraph, which lists "formal methods for verification and assurance of cyber-physical systems, including those that integrate AI" as one area of interest among about ten. Neither source describes the state of verification methods, so most of the earlier text had no support in them and was taken out rather than re-sourced. (1) Source line: the solicitation title was given as "Future CoRe: Computer and Information Science and Engineering Future Computing Research." The solicitation gives its program title as "Computer and Information Science and Engineering (CISE): Future Computing Research (Future CoRe)"; the Source line now uses that, and gives the program page its full name. (2) Problem Statement: removed, because they are in neither source, the statements that there is "no way" to formally verify learning-enabled components; that neural networks have billions of parameters; that no accepted mathematical specification of correct behavior exists; that adversarial examples resist formal characterization; that testing cannot give guarantees because the input space is effectively infinite; and that there is a "certification deadlock" in which AI systems are "fundamentally unverifiable." The examples of self-driving vehicles, surgical robots, drones and smart grid controllers are also not in the sources and were removed. The section now gives the program page's definition of cyber-physical systems, the CPS-FR areas of interest, and the page's remark about unpredictable physical systems, and says plainly that the sources name the research area without measuring the gap. (3) Why This Matters: removed, because they are in neither source, the statements that the FAA, FDA and DoD all require verification pathways that do not exist for learning-enabled components; that autonomous vehicle crashes, medical AI misdiagnoses and drone incidents happened "precisely because of" failures in learned perception and decision-making; that no autonomous system can be deployed in safety-critical applications without assurance; and that the gap is growing and could block deployment "indefinitely." The section now gives the program's stated aims and the application areas its community-inspired track lists. (4) What's Been Tried: removed, because they are in neither source, the statements that existing tools handle only networks of "tens of neurons" and do not scale to millions or billions of parameters; that robustness certification does not compose into system-level guarantees; that simulation covers limited scenarios; that runtime monitoring gives no proactive assurance; and that separating development-time from runtime assurance yields fragmented safety arguments. The section now says the sources do not review earlier approaches, and gives what they do show: that NSF 25-543 replaces the earlier CPS solicitation NSF 24-581, that verification of hardware and software is described under a different program (Software and Hardware Foundations), and that the CPS-FR track encourages validation by prototyping or testing. (5) What Would Unlock Progress: the list of compositional verification, specification languages, continuous assurance frameworks and hybrid formal-statistical approaches is not in the sources; the section now gives the CPS-FR track's own list. (6) Source Notes: the first note said NSF 25-543 "consolidates several previous CISE programs including CPS" and that CPS-FR "specifically targets" systems with learning-enabled components. The solicitation says it replaces NSF 24-589, NSF 24-581 and NSF 25-527 and that the CPS program was added; formal methods for verification and assurance of cyber-physical systems, including those that integrate AI, is one listed area of the track, not its specific target. The note now says that. The note naming the CAV and FMCAD conferences, the AI safety community and INCOSE as working with "limited cross-pollination" is not in the sources and now gives the program page's list of collaborating NSF directorates. The note calling compositional verification "an open theoretical problem" is not in the sources and was removed. The note on the "newly-created" tag now says it is this project's reading and not a statement in the sources. Confirmed in the sources and left as written: the solicitation number NSF 25-543, the CPS-FR track name, and both links. Not checked against the two sources, because they are suggestions and not source claims: the entry points. The three tools named there (Marabou, alpha-beta-CROWN, nnenum) each have a public code repository on GitHub that opened on 2026-10-01; nothing else about them was checked. The cross-domain note comparing this problem to cascading infrastructure failure is this project's own comparison and was left as written. No title changed. The long title says formal verification of such systems cannot be done; the sources do not say that, only that verification and assurance of AI-integrated systems is an area where NSF seeks research. The title was left for an editor to decide. Genome tags untouched. A second reader went over these repairs against both sources on the same day; every removal stands, and several of the new sentences were reworded to stay closer to the page: the page says research on cyber-physical systems "benefits from considering" the unpredictable nature of physical systems (it does not say such systems are hard to reason about); security, privacy and trustworthiness is a listed area of interest and not a request; the Software and Hardware Foundations program names verification in its description, which does not show that verification belongs to that program alone; "convergent research" is the solicitation's phrase for the CPS program; "inherently multidisciplinary" is the page's description of connected-community research, not of the whole program; the four collaborating directorates are listed for the CPS program as a whole, not for its connected-community research; the first Source Note now names the listed area of interest as the page words it (formal methods for verification and assurance of cyber-physical systems, including those that integrate AI) rather than "AI-integrated systems"; and the solicitation's "Replaces" and "Added" lines are reported as two facts rather than as one causing the other.