[NathanCollins]

Thanks for clarifying "white-box testing".

Some comments:

* the operations in the mathematical spec are mostly well defined, but e.g. division by zero is not defined. However, the verification handles this by checking that all operations are well-defined on all possible inputs.

* yes, identifying the "edge cases" is not something you can do easily, and hard to make formal. In some sense, the fact the non-edge-case inputs are treated in a uniform way is probably what allows the verification to succeed at all.

* a short summary of the answer you already found in the third blog post: what we actually verify is the LLVM assembly that Clang produces when compiling the C program. Much of the potentially undefined behavior in a C program is translated away by the compiler on the way to LLVM assembly. For any potential undefined behavior that remains in the LLVM assembly, the verification checks that it cannot happen at runtime.