Using "better more safe programming languages" generally gets you [some greater level of] memory safety and thread safety. Developing for safety-critical embedded systems with a single thread and no dynamic memory allocation renders those benefits irrelevant. There are still concerns around type safety, but full compiler warnings and strict code review, both of which we need regardless, handle that.
We also need to be able to certify not only that our source code matches our requirements, but that our binaries match our source code. Compiling with --c99 --debug -O0 gives us a highly visible link between each line of source code that goes into the compiler and the assembly instructions that come out of the compiler. We know exactly what the computer is actually doing, not just what we think we've told it to do. The various "better" languages all get "better" via more powerful and clever (read: complex and opaque) compilers, which is a no-go in our field.
With little benefit and impermissible cost to the alternatives, and the breadth and depth and longevity of the resources and support available for it, there's no sane choice for us but C.
If the optimiser drops off some code as it thinks it has no effect, I'd guess that's possible to spot, and you'd want to know to either fix the code or remove dead code. I've not personally had to inspect compiler output but I do spend a surprising amount of time in linker map files understanding what's going on.
For really performance-oriented code you probably want to drop to SIMD first, and play with compiler optimisations second.
It's clear from the OP's question that the org is already C-centric. Language support in a safety environment is a large and complex issue. The compiler, tools, libraries are also required to be validated in context (depending on the standards environment), coding and other supporting standards have to be developed or vetted for adoption, you need a population of able reviewers, interoperation between implementations needs to be validated, etc. etc. etc.
And at the end of the day, the "safety" that another language buys you doesn't actually get you very far. A lot of folks get hung up about memory safety, or this or that language feature, when in reality the majority of safety issues in large codebases are algorithmic in nature, and no low-level language feature is going to save you from implementing the wrong design.
I don't think it's clear that the OP organisation is stuck with C. Perhaps it's the case, but I think it's also time, in 2022, to push a bit to move toward safer programming languages.
You describe an excellent set of rules and processes, perhaps too much for most projects. It sounds like it could be even better with a memory-safe programming language. Also, I doubt that most secure critical C/C++ projects proof their source code correctly in Coq or similar.
I also think many security issues are tightly related to the programming language. For example, SQL injections are because of SQL, XSS because of HTTP/HTML, and Buffer overflows because of C.
Another take away from an old old paper was that safety must be a primary design goal from the start. It's not something you can bandaid in afterwards. There is a lot of stuff out that what that didn't happen and as a result you see constant whack a mole with critical bugs.
You can justify it by difficult of bootstrapping or a lot of legacy code that is already vetted so you can reuse. But in 2022, your options are very good in this area.
I know that some people get upset when they have a question, and they don't get the answer but some suggestions. But sometimes, people are not aware of the alternatives, and it's important to remind them that perhaps a better solution exists.
If someone asks how to cut crusty bread with a butter knife safely, you can talk about the proper technic, how most people do it wrong, write a book about your industry do it better, but perhaps, someone should also mention that it's easier and better with a bread knife.