C actually has multiple formal semantics. The most recent I'm aware of is Robbert Krebbers' (almost) complete formalizatiom of C11 in the CH2O project.[1] See also his upcoming PhD thesis[2] for more details.
Arguably C doesn't: C is just what the spec says. You can try and formalise what the spec says (as, rightly, many have done), but it's hard to guarantee correctness of that formalisation.
[1] http://robbertkrebbers.nl/research/ch2o/
[2] http://robbertkrebbers.nl/thesis.html