Vitalik Shares Latest LLM Progress, Highlights Expanding Ethereum-AI Intersection on May 28

According to PANews, on May 28, Vitalik Buterin shared updates on his autonomous language model (LLM) setup, emphasizing the growing intersection between Ethereum infrastructure and artificial intelligence. He noted that Deepseek V4's 2-bit quantized version runs within 90GB memory at approximately 35 tokens per second on Apple hardware but only 7 tokens per second on AMD, stressing that multi-hardware vendor support is key to distinguishing "decentralized AI" from "CROPS AI." Mistral's Leanstral model, focused on Lean code writing, similarly runs in 70GB with performance comparable to 1T parameter models.

Vitalik elaborated on formal verification's role in enhancing code security, proposing that AI-assisted formal verification enables "end-to-end" security proofs applicable to STARKs, consensus algorithms, and EVM components. He highlighted that blockchain and ZK-SNARKs provide open verifiability and privacy scalability, while AI combined with formal verification improves code efficiency while restoring accuracy, forming a complementary tech stack.