Ferrocene released as open source

You don't need to audit all your code to certify it. Your certification is for some aspects of the final product, and your qualified compiler's job is to allow you to verify, at source level, that the parts of the software that affect the certification do what you want. Implementation defined results are absolutely OK here, because you're not certifying everything the software does, just a subset of it.

So, for example, one qualified toolchain I've used says that code after an entry point (CPU interrupt vector) but before the program invokes UB has defined behaviour; it's only code after the first invocation of UB whose behaviour can be modified by the later UB. This is fine for certification purposes; if all the certification-relevant code is audited as OK, then it doesn't matter if later code would fail the audit. It's also fine if we have to rework code to change compiler - the certification is for a final product, with known code, compiler etc, and not for an arbitrary build. And there's not necessarily a need for a tool to tell us when we leave the guarantees from the qualified compiler, since the code will be audited by someone with the guarantees in hand, who will ask questions like "where is the code that proves that this signed arithmetic cannot overflow?"

To give you a concrete example, take a car brake controller. It has braking force applied to each wheel as an input, requested total braking force as an input, movement speed of each wheel as an input, steering direction requested as an input and outputs requested braking force for each wheel. There's a mechanical linkage to the brakes separately to the brake controller, which guarantees that the applied braking force total across all wheels is at least 50% of the requested total. The controller's job is to let up the brakes on wheels whose speed is outside a physically plausible range, so that you can't lock your wheels up while trying to stop.

As a safety matter, we need to be confident that when braking force is requested, the controller asks for brakes to be applied to all wheels that are turning; we also need to be confident that if the brakes are released on a wheel, they will be reapplied as soon as the wheel resumes turning. More interestingly, if a driven wheel stops turning, we need to brake the other side of the car so that the stopped wheel restarts spinning. These are things that certification covers, and we need to convince audit that the software side of the brake controller does this.

However, the brake controller has other tasks, too; for example, if the braking force applied to a wheel is sufficiently higher than the braking force requested by the brake controller, we know that the mechanical linkage is applying braking force, too, and need to flag this as an alert. If no braking force is requested or being applied, but a wheel stops, we need to flag this as an alert. Similarly, if we ask for braking force, and the wheel doesn't slow, this is an alert. But none of this is safety-critical, so it's all outside certification.

From the point of view of code audit, as soon as I can confirm that all the safety matters are going to work given the promises the qualified compiler makes, I'm done and can put the certification on the module. If the alerts don't happen because I've got UB in the alerting code, and the compiler optimizes it out, well, so bad, so sad, just like any other C code. I may have used a qualified compiler, and I've got my shiny certification, but it only promises that the safety-relevant parts are working, and not the rest of the code.

fn main() {
    // This if statement gave an error, so I commented it out
    // if (orders_given) {
        Nuke.launch()
}