Here is a Coq formalization of C11: http://robbertkrebbers.nl/research/ch2o/
It only covers a large fragment of C11, but they formalized the operational, axiomatic, and executable semantics and proved that these correspond to each other.
Yes, and there are other formalizations as well. But none of them (as far as I am aware) formalize the undefined parts in the way the featured article does. I think comparing projects with different goals and then saying "the differences must be due to the tools used" isn't solid reasoning.