There are some tools aimed roughly in this direction, such as https://github.com/TrustInSoft/tis-interpreter.

A major difficulty here is that undefined behaviour is a property of a particular execution of a C program, rather than a static property of the program itself. Tools that dynamically detect UB are useful, but will not demonstrate that there are no inputs for which a program will go wrong.