C can be safe if you use Turing incomplete libraries that have been verified. It's the YOLO ad hock parsers that get you in trouble.

I am not sure if you are serious or not.

How does verification prevent buffer overflows? It can reduce their frequency, but you can never know you got them all. They find issues in libCURL and openSSL that have existed for years. Very few people are better than the people working on those libraries.

It is better to be safe by default then add risk only when you need it. I say this as a C++ developer, I think const should be the default state of all variables and one should have to opt out of that, and Rust did that right and C is so far from that I see no reasonable way to use plain old C safely. At least with C++ I can hide my stuff in classes and verify one thing at a time.

snakeanus

Formal verification is not the same as a security audit. With formal verification you can prove that something is bug-free.

> They find issues in libCURL and openSSL that have existed for years

Neither of them are formally verified. https://github.com/seL4/seL4 however is formally verified.