Tin tức BlockBeats, ngày 19 tháng 5, Đồng sáng lập Ethereum Vitalik Buterin đã viết bài phân tích sâu về Công nghệ Xác minh Hình thức (Formal Verification), chỉ ra tình hình hiện tại và triển vọng của nó, cho rằng việc kết hợp Xác minh Hình thức với Trí tuệ Nhân tạo sẽ trở thành "hình thức cuối cùng của phát triển phần mềm", đồng thời là con đường chính để bảo vệ mạng lưới an toàn trước mặt đối thủ mạnh là Trí tuệ Nhân tạo. Vitalik chỉ ra rằng điểm cốt lõi của Xác minh Hình thức là chuyển đổi tính chính xác của mã thành một định lý toán học có thể được máy tính kiểm tra tự động, qua đó đảm bảo an ninh phần mềm theo cách chứng minh toán học, chứ không phải dựa vào kiểm thử truyền thống hoặc kiểm định thủ công. Anh cho rằng mô hình này đặc biệt phù hợp với các tình huống "Mục tiêu xa hơn cả việc thực hiện một cách đơn giản" — ví dụ như chữ ký chống lại lượng tử, hệ thống chứng minh STARK, thuật toán đồng thuận chống Byzantine Fault và ZK-EVM, những thành phần công nghệ cốt lõi của cập nhật tiếp theo của Ethereum.

Tuy nhiên, Vitalik cũng thừa nhận rằng Xác minh Hình thức không phải là phép màu. Mô hình thất bại phổ biến bao gồm: chỉ xác minh một phần mã và bỏ qua lỗ hổng quan trọng, quy chuẩn an ninh vốn có sơ sót, và khó khăn trong việc bắt lỗi phần dư thứ cứng mềm tại ranh giới. Anh nhấn mạnh rằng "sự chính xác có thể chứng minh" về bản chất là sự nhất quán bên trong giữa các ý định không giống nhau, chứ không phải là việc so sánh với ý định thực sự của con người một cách tuyệt đối.

Đối với thách thức an ninh mạng do Trí tuệ Nhân tạo mang lại, Vitalik lạc quan cẩn trọng. Anh cho rằng, Xác minh Hình thức hỗ trợ bởi Trí tuệ Nhân tạo sẽ thúc đẩy kiến trúc phần mềm tiến tới mô hình "Lõi an toàn và Rìa không an toàn": các thành phần rìa sẽ chạy trong hộp cát, chỉ được cấp quyền hạn tối thiểu; trong khi lõi an toàn sẽ tiếp tục được củng cố bằng phương pháp hình thức, chịu trách nhiệm với trách nhiệm tin cậy cấp cao nhất trong quá trình số hóa xã hội. Ethereum sẽ trở thành một phần quan trọng của lõi an toàn này.