Vitalik Buterin, trong bài viết mới nhất của mình, thảo luận về một mô hình mới đang nổi lên trong nghiên cứu tiên phong của Ethereum. Phương pháp này bao gồm việc lập trình trực tiếp bằng mã bytecode EVM, assembly hoặc Lean, và xác minh tính đúng đắn thông qua các bằng chứng toán học được kiểm tra tự động trong Lean. Việc xác minh hình thức có sự hỗ trợ của AI được kỳ vọng sẽ nâng cao cả hiệu quả mã và bảo mật, đặc biệt đối với các mô-đun bảo mật quan trọng như STARK, ZK-EVM, chữ ký chống lượng tử và các thuật toán đồng thuận. Tuy nhiên, Buterin cảnh báo rằng xác minh hình thức không phải là không thể sai sót, vì nó có thể thất bại do phạm vi bằng chứng không đầy đủ, lỗi đặc tả hoặc các kênh bên phần cứng. Ông hình dung phần mềm trong tương lai sẽ được chia thành "lõi bảo mật" và "các cạnh không bảo mật", với Ethereum được định vị trở thành một lõi bảo mật quan trọng.