Comment by afdbcreid

Well, I'm not an expert in formal verifications, but there are such libraries, I listed few of them above, you can go and check them. So it is possible.

C doesn't have the shared xor mutable rule - with strict aliasing or without.