Are you sure that wasn't about Vlad Zamfir's proof-of-stake ideas? Back then Vlad gave a bunch of talks about those being "correct by construction," and he and

Are you sure that wasn't about Vlad Zamfir's proof-of-stake ideas? Back then Vlad gave a bunch of talks about those being "correct by construction," and he and Vitalik worked closely together. I don't recall Vitalik ever claiming that arbitrary smart contracts built on top of Ethereum were provably safe. Back then nobody was applying formal proof to smart contract code, it was just regular devs slamming out Solidity scripts with minimal third-party audits. That's what the vulnerable DAO code was; there wasn't a formal proof within miles of that stuff. The hack did not target the Ethereum protocol itself. Applying formal proofs to smart contracts does make sense, since failures are expensive and the code is short. There's been gradual movement in that direction but it's been slow.