You'll potentially have less of a chance for contracts to be exploited (at least compared to what we have now).
That said, you can't protect against infrastructure exploits as easily, mathematically flawless program or not.
My former professor (RIP) oversaw the formal verification of the F-16 computer software and it still had significant bugs in the end where the specification itself was incomplete or in error. And that was a multi-year, team-scale effort. No one is doing that for smart contracts.
TLS 1.3 has been formally proven (not an implementation, but the standard itself). To the extent the mathematicians correctly explained what the TLS 1.3 RFC says, and correctly told the machine what TLS 1.3 is supposed to do, the machine proof says this protocol does what we intended.
That work assumes a bunch of components are black boxes, they must work. If we ever lose confidence that they work, we've got to throw those out. So for example SHA-256, AES GCM, X25519, the proof doesn't say "We prove these work" it says "Assuming you're right that these do what they're designed to do the rest of your proof holds"
Anyway, one of the assumptions in that proof is a surprise to a human implementing TLS 1.3, it isn't explicitly mentioned in the TLS 1.3 document as written. And so the result is, if you didn't obey that assumption, the proof doesn't hold and sure enough you're vulnerable to an attack.
The assumption is for Pre-shared Keys (e.g. IoT devices A and B don't want to bother with certificates, so they just use pre-agreed random keys) each device pairing has its own PSK.
A person looking at the design figures hey, got two devices Alice and Bob, I can just have a single key K known to both devices, and everything is secure. But that's wrong - and the TLS 1.3 proof doesn't say this will work. Here's what bad guys can do, it's called the Selfie Attack:
Alice sends a message to Bob, maybe "Did you feed the cat?" and it's encrypted with key K. Normally Bob receives the message, maybe answers "Yes I fed the cat" also encrypted with key K and all is well.
But now Mallory is on a network able to intercept and re-route messages. Alice sends to Bob, "Did you feed the cat?" encrypted with key K. Mallory can't read or tamper with this message, it's encrypted with key K and TLS 1.3 works as designed, but Mallory just re-directs the message back to Alice, "Did you feed the cat?". The message is encrypted with key K, Alice assumes Bob sent it, and replies "No, I didn't feed the cat" also encrypted with key K, which Mallory re-directs again back to Alice, who now mistakenly believes that Bob has told her he hasn't fed the cat.
There are obviously a bunch of things you could do to fix this. First of all you could just have more PSKs. If Alice's message to Bob is always encrypted using the Alice->Bob shared key, when Alice actually receives it instead she knows something is wrong immediately. Or you could just prefix each message with To/From information, like an old-fashioned email and that works too so long as you check it.
But the important observation is that this is an assumption in a proof that nobody really surfaced until it was too late. If researchers had told the proof system "No, the PSKs can be the same" the proof fails. Or if they'd carefully explained to the TLS Working Group, "We had to spell out that the PSKs must be different" then today RFC 8446 would likely explain that you need to do that or you've got a security problem. But neither happened and this attack slipped between the cracks.
1. a non-verified approach can have many problems in the (informal) specification + implementation errors
2. the verified approach is likely to have less specification errors (because the specification had to be formally written out and matched against an implementation) and implementation errors with respect to the specification will be almost impossible (minus faults in the compiler, OS and hardware).
There's a huge jump in security guarantees between 1 and 2.
I'm saying you should define a ceiling for your smart contract so in case of a bug, no transactions over that ceiling go forward.
So if you have a stupid bug that causes you to transfer 1BTC instead of 0.001BTC you don't lose all your money.
The key is that the contracts need to be minimal and analyzable, so its ~100 lines of code you can manually analyze. Documented separately all the edge cases, or ideally removed through good design so they simply don't exist. A bunch of problems I've seen in the real world of crypto are annoying edge cases that you can fix with an if statement, or ideally change the design to remove them completely. It's actually a surprisingly hard space because you're trying to make terse, complete and secure code.
In normal web/systems programming you have layers of security; internal services, external services, firewalls, access controls, vpns, security by obscurity, etc etc etc. In crypto you have none of that. Everything is 100% public, the code probably should be published, or else it is trivially decompiled. If there is a problem someone will find it if there is value in finding it.
> In normal web/systems programming you have layers of security; In crypto you have none of that.
Yes, that's what I mean. Why not?
> The key is that the contracts need to be minimal and analyzable
Agree, but even short contracts might have bugs. Betting on "self-paying bug bounts" is not a good bet.
What I'm proposing is that every smart contract double-checks its expected results
You can make powerful systems with simple correct independent components. You can not make complex secure monolithic systems. It gets even worse when you look at contracts with delegation.
The problem with most "smart" contracts is they have abstractions, delegation and scope creep.