Audited, Battle-tested and Formally-Verified Smart Contracts, like Safe Multi-Sig Wallet, are the Most Secure, Reliable and Unstoppable Automation We Have Today

So this is something I recently realized recently when looking at the Ledger + Hardware wallet security discussion.

When we look at other wallets such as Trezor etc., even if they have open-source, audited and battle tested Software+firmware and bug bounty programs, some "minor" problems always remain. You never know, how many bugs are still there.

And don't forget. This is firmware code written in C. C is the language where you can have root privilege escalation vulnerabilities hidden in plain sight in a Linux utility for 12 years, because it's really hard to reason about guarantees in the state explosion. Firmware code is hard. C is hard. It's easy to write, but hard to get write safely. That's why languages such as Rust were developed to mitigate many of it's problems.

Ideally, such software is formally verified. This means, that a semi-automatic theorem prover is used to prove, that the program/assembly satisfies certain properties. E.g. you could prove, that "the seed phrase cannot be extracted with malicious firmware invocations". However, formal verification of firmware and C code is hard or next to impossible. The state explosion is so strong that it's really hard to get anything done there. Not to mention, that our tx logic isn't as simple in Ethereum as it is in Bitcoin for instance.

And I'll not even start with what you can do, if you actually have physical access to the device and start doing stuff like forced reboots, laser bit-flipping etc. (State actors have many possibilities here, but I digress.)

Yes, in practice, mostly this won't matter. But we don't know, how many things are discovered in the future. And you don't want to put such a small seed phrase in a physical device as the single point of failure to your entire crypto funds. And CEOs of crypto companies have been regularly threatened to give their hardware wallets + Pin.

Seems problematic right? And this is the best case among hardware and software wallets.

Now, let's look at smart contract multi-signature wallets - where https://safe.global is the gold standard in ethereum.

These smart contracts have many benefits over the above hardware wallets.

First of all, there is no hardware, that can be manipulated to extract the keys. It's all running on the thousands of ethereum nodes - and a bug in the EVM that can be exploited in all existing client implementations is very very unlikely. At least, it's much less likely than a bug in Trezor firmware, where there is a single firmware implementation made by a single company. Since the EVM is abstract, it's actually more secure than the hardware-based execution. Obviously, this is also one of the reasons why ethereum was created in the first place.

Second, formal-verfication of smart contract is practical and guarantees a lot. Battle-tested, open-source, audited code with big bounties is great. But if you have a proper formal verification where things like "only when n signers signs a tx, then it can be executed with the Safe Wallet funds" can be proven, you actually have very high guarantees and they actually mean a LOT. These proofs are much better than audits and testing, because you can virtually eliminate all code bugs there. Yes, technically you could have bugs in the theorems proving software, but that can be eliminated sufficiently and isn't only limited to their usage in smart contracts. With this, it's safe to say, that such smart contracts with formal verification are actually secure. (Safe has formal verification for their 2019 implementation. They're doing another formal verification for their new code currently in 2023.)

With all this background, I'd like to argue for the statement in the title: Battle-tested, audited and most importantly Formally-Verified Smart Contracts are the most secure, reliable and unstoppable Automation we have.

How many other decentralised execution environments do you know, which have Formally-Verified contracts running on multiple implementations?

Yes, you need to do the homework properly. If you prove meaningless properties, then it doesn't help much. But if done properly, I think smart contracts are multiple magnitudes more reliable than all other hardware/software based execution environments. Some people point to smart contract bugs, or misses in the audits. But I argue, that formal verification can eliminate them (and has on many occasions), and problems like theorem prover bugs are much much rarer than all the undiscovered bugs in all the individually written wallet implementations (Trezor, Metamask,etc.).

And this is before considering the "multi-sig" aspect of smart contract wallets.

What do you all think? Do you agree or disagree? And why?

Edit: I realise, that the security aspect is similar to L2s inheriting from L1 Vs. creating Sidechains. A smart contract with proper formal verification inherits the security of the compiler and the theorem prover. It can't be less secure than these - and if we assume that they are correct, then the contract is also provably correct. However, custom implementations like hardware wallets and software wallets don't inherit their security from anything and have to create their own security. But that's harder, because they work in a more complex situation (assembly) compared to the EVM (abstract).

Disclaimer: I don't own any Safe Governance tokens. Just a normal Safe Wallet user.