Written over many many years by experts of a field, and the end result is at most somewhat complex, nowhere near the complexity of even the monolith SPA of your favorite website.

GP said:

> meaningful complexity

Not, "the most complex". If an OS that can lock down DARPA self-flying helicopter software is not meaningful enough for you....

Less than 10 000 lines of code. But let’s say we accept it as an exception — it is most definitely not the “standard way” of writing C programs.

From GP:

> It is not possible to remove ub from the spec

did not say "it is not standard to remove ub"...

The speed of development was very low, and how many people can check the proofs?

> The speed of development was very low,

Not a part of GP's assertion

> and how many people can check the proofs?

it's not necessary, the proofs are checked using automation. I'm directly taking a shot at this assertion:

> Static analysis tooling has demonstrated that it isn’t up to the task

Just because you have a proof doesn't mean it proves the right thing.

Congratulations. You have won the argument "there is no perfectly secure system", which no one was arguing.

I've got a strong background in formal verification. I do not believe that "formally verified" means "security bug free". In fact, I personally know researchers who have had vulns found in their formally verified code more than a decade after they completed the verification.

I agree, there are lots of outrageous claims out there about "provably secure software" which seem very dubious.

What are your thoughts on SEL4, is it really a breakthrough it is made to be in success of formal verification? Is there a way for users/administrators deploying it to verify themselves authors' claims? Or is it too difficult? I am afraid the latter...

In 2004 Peter Gutmann in his thesis/book criticized the hype around effectivity of formal methods in computer security [1]. Has the situation changed?

[1] https://archive.org/details/springer_10.1007-b97264

Breakthrough? No. Good work? Yes.

I don't think there is any reasonable standard of security that demands perfection.