For almost as long as people have been designing control systems, they have been asking “how can we prove that our controller will be safe?” For simple systems (e.g. linear or low-dimensional polynomial dynamics), we might be able to hand-analyze the system and prove that it will be safe, but this manual analysis quickly becomes untenable as the systems dynamics…