[Kranar]

C does not have a formal specification either. It has a standard's document that is written using formal English, but it does not provide a formal spec of C's semantics. A formal spec of a programming language's semantics would entail using a formal semantic model such as operational or denotational semantics. Some programming languages do specify the formal semantics for the entire language or some subset of the language but C is not one of them.

Your claim that the C Standard lists all undefined behavior is actually false. The C Standard only lists out the explicit list of undefined behavior, but it does not list out the implicit list of undefined behavior. There have been efforts to make just such a list but it's an incredibly difficult task.