Why Fully Automated Formal Verification of Smart Contracts Is Impossible

In a follow‑up to a previous AI article, the author asserts that just as automatic programming is unattainable, fully automatic formal verification of Ethereum‑style smart contracts is also impossible.

With the surge of blockchain interest, many attempt to apply formal verification to Solidity contracts, some even claiming to use deep learning to automatically generate Hoare Logic pre‑ and post‑conditions for correctness.

Hoare Logic is a method of program verification that requires annotating code with explicit pre‑conditions and post‑conditions; for example:

{x=0} x:=x+1 {x>0}

These annotations enable logical reasoning about program behavior, but they must be supplied by humans; the system cannot infer the intended properties on its own.

The author explains that automatically generating such annotations is akin to “mind‑reading” and therefore infeasible—deep learning cannot know what properties the programmer expects without explicit specification.

While manual Hoare annotations can be valuable and tooling may assist, ultimate correctness relies on expert‑crafted specifications and careful coding; no tool can guarantee flawless smart contracts.

Beyond verification, the piece critiques the very notion of smart contracts, arguing that scripting languages in Bitcoin and Ethereum introduce security flaws, performance issues, and unnecessary complexity, and that contractual functions belong to legal systems rather than code.

Consequently, the author believes blockchain technology is promising, but smart contracts are an overengineered distraction that should be avoided in favor of focusing on robust, simple monetary functions.

Source: http://www.yinwang.org/blog-cn/2018/02/22/smart-contract