"Secure" sounds like a binary attribute but it's actually not. A formal proof doesn't save you from errors in the specification. At some point you need trust, the amount of trust needed is inversely proportional to the security.

Without a formal proof there is no measure of correctness at all.

Lots of passing tests mean nothing to you?

When an exploit only needs one edge case not handled right? No, lots of unit tests means nothing. Maybe less than nothing due to the false sense of security they seem to give you.

So you trust a software that has had zero testing equally to a software like sqlite that has extensive testing?

lets not go too far! tests can provide a security advantage over regressions or bugs introduced in the future. They are necessary but not sufficient to prove a particular security level.

That's like saying that the world was flat before they could prove that it is round.

No, that's like saying that we don't know what shape the world is before we could prove that it is round.

No, it's like saying it is round "if and only if" we can prove that it is round.

Which the scientifical method tells you to verify experimentally, i.e. with tests.

No, the point is: The sphere doesn't care if you can prove if it is a sphere or not, it stays a sphere. If you CAN TELL if it is (or not) is a different matter entirely, so it doesn't work that you say "if and only if it is proven" when you make claims about something having a certain property.

i.e. Just because I can't tell if you have two hands to type this doesn't mean you don't have them.

"You have two hands if and only if there's a formal proof that you have two hands"