That was really a risk. It's no longer a risk. In any situation where the developer's interpretation of the semantics differs from the binary semantics, their tool chain will reject the compiled binary. That's the point.
The gcc git repository receives hundreds of contributions every week. Despite the heroic efforts of the open-source communities, it's still very easy to submit buggy or malicious patches (just think about the University of Minnesota scandal [1]). One of those could easily be used to target seL4, especially since it's hard to target seL4 in any other way, given all the other security guarantees. A tool that double-checks the compiler will buy the stakeholders significant peace of mind.