Formal verification (of cyber-physical systems)
Concrete Problems in AI Safety — inherited
A body of prior work formally verifying safety-critical cyber-physical systems, exemplified by the complete formal verification of the federal aircraft collision avoidance system.
Testing samples a system's behavior; formal verification proves it, mathematically, for every possible input. The approach has secured real safety-critical systems, most famously the federal aircraft collision avoidance system, and the AI-safety corpus keeps it in view as a standard that other methods rarely meet.
A section on proving rather than testing opens the prose, followed by one on the rigor Asimov's fictional law never received, and that modern machine learning still lacks.
Proving a system correct rather than testing it
Formal verification is a body of techniques, including model checking and automated or interactive theorem proving, that mathematically prove a system satisfies a specification for every possible input or execution, rather than checking behavior on a finite set of sampled test cases. In the model-checking approach, a system is modeled as a finite or symbolically represented state-transition structure $M$, and a specification is written as a formula $\varphi$ in a temporal logic such as LTL or CTL, capturing properties like "a collision warning is always eventually followed by an avoidance maneuver." Verification then either exhaustively searches $M$'s reachable state space to check $M \models \varphi$, or constructs an inductive proof that no reachable state violates $\varphi$, giving a guarantee that holds for all executions rather than only the ones tested. This body of technique predates Concrete Problems and is inherited by it as a benchmark for what rigor can look like (concrete-problems, §"Cyber-Physical Systems Community:", p. 20).
The rigor Asimov's law never got, and modern ML still lacks
The paper credits the cyber-physical-systems community with "an impressive and successful effort to formally verify the entire federal aircraft collision avoidance system," alongside similar work on traffic control algorithms (concrete-problems, §"Cyber-Physical Systems Community:", p. 20). Formal verification (of cyber-physical systems) — supplies the rigor asimov lacked → Asimov's first law of robotics sets this against Asimov's first law of robotics, a fictional injunction that Weld and Etzioni once tried to formalize within classical AI planning over two decades earlier, showing what actually rigorous, machine-checked harm-avoidance looks like once a community commits to it. The comparison is double-edged: the same passage concedes that this level of rigor "has not focused much on modern machine learning systems, where formal verification is often not feasible" (concrete-problems, §"Cyber-Physical Systems Community:", p. 20), the gap Careful engineering (reward hacking remedy) gestures at but cannot close, since the continuous, high-dimensional, learned models used in modern ML resist the discrete state-space techniques formal verification was built for.