One can be fundamentally mistaken about what "it says on the box" See WPA2/KRACK for example.

It becomes an infinite recursion of "how do we know the proof of the proof of the..." is what we actually want?

You mean, when you look at your code, or someone else does, they think it's ok?

I guess that's why security issues, even in massively peer reviewed code, are a thing of the past, right?

Do your best, code as safely and securely as you know how, peer review and test and fuzz...

Then when you deploy your code, treat it as vulnerable, because history days it likely is.

Treat your phone as compromised. Anything network connected as compromised.

Because history says it can be, and easily.

Monitoring is one of the most important security measures for a reason.

There does actually exist such a thing as formally proven code, which is mathematically according to spec. https://www.sel4.systems/Info/FAQ/proof.pml

I don't even see the point you are making.

Are you trying to claim that the above proof will never be invaldated?

You're really just proving mt point here. You think thongs can be secure.

what do you mean invalidated? the point of proofs is that they will be still be as true today as they will millenia into the future. pythagoras' theorem is just as true today as it was millenia ago.

Yes, that's what I'm claiming.

That's of course only a part of the story, the spec or the hardware can still be broken.

You could formally prove Unicode renderers are 100% correct. It's because they are 100% correct that they can be relied on to be exploited.

The weak spot when it comes to security is not the hardware or the software, it's the human mind.

The proof may be valid but the implementation may have a mistake, or the compiler, or the operating system, or the hardware.

Or if it dynamically loads anything that isn't formally proved.

but does the hardware? Formally proven code does not prevent you from hardware bugs like rowhammer.