Key Highlights
- Vitalik Buterin advocated “vibe-coding” for critical software development.
- Buterin referenced Verified-zkEVM ArkLib and zkSecurity’s research as examples.
- He argued that AI makes secure coding difficult but still achievable with verification tools.
Ethereum co-founder Vitalik Buterin has expressed support for using “vibe-coding” for critical software components, mainly within the Lean theorem prover.
In a post on X on Monday, Buterin described the approach as a practical way to make more secure as well as verifiable code for significant projects. He highlighted two examples: the Verified-zkEVM ArkLib project on GitHub and a blog post from zkSecurity titled “The Final Form of Software Development.”
He said formal verification tools such as Lean allow developers to focus on high-level intent (“vibes”) while the system ensures mathematical correctness.
What is “vibe-coding”
Vibe coding is a way of developing software wherein coders express the “vibe” or general intention behind the code without specifying each and every detail; this can be done by natural language or using artificial intelligence.
The code is then formally verified through Lean theorem prover and other means that mathematically ensure its correctness. This allows developers to quickly generate code while also ensuring that the code works correctly. It has been recently promoted by Vitalik Buterin for use in blockchain technology.
Buterin highlights Lean through examples
In one given example, Buterin related the Lean theorem to Merkle trees. The theorem says that generating valid proofs for two different values at the same position in a Merkle tree is only possible by breaking the underlying hash function.
He also mentioned that reviewers no longer need to inspect low-level implementation details; they just need to verify the statement of the theorem and confirm that Lean has checked it.
One benefit of Lean discussed by the co-founder was the ability to use it to specify not only proofs and specifications but also executable code, including command-line applications. This feature diminishes the dependency on conventional programming languages and compilers, which themselves come with certain levels of trust.
Buterin opposed two common narratives in software development. He detailed the idea that “software is all going to become probabilistic now” due to AI as “cope,” and the suggestion that AI bug-finding needs embracing closed-source software as a “pysop.” Rather, he stated that while writing buggy code has become trivial with AI help, writing secure code has shifted from nearly impossible to merely difficult.
Use of nonces
Separately, Buterin has previously proposed using nonces and limited storage to make Ethereum more scalable. As the method would enhance privacy capabilities, the founder stressed that it would also be a solution to making data storage more efficient.
According to Buterin, nullifiers from privacy transactions would accumulate permanently within the blockchain. As an illustration, the storage of nullifiers through privacy transactions at a rate of 2,000 per second over eight years can generate approximately 500 billion nullifiers.
Broader shift
Formal methods such as Lean have traditionally been linked with high-assurance situations, such as in the aerospace and defense industries. The greater availability of formal methods due to AI support can expand their application in blockchain development, as security breaches will involve considerable economic costs.
Buterin’s statement reveals a paradigm shift from accepting probable results and closed systems to using technologies that enable high-assurance programming in practice.
Also Read:Ondo Finance Surpasses $1B TVL in Tokenized Stocks and ETFs
