TechFlow đưa tin, ngày 19 tháng 5, Vitalik Buterin đã đăng bài trên blog cá nhân, nêu rõ việc kiểm chứng hình thức (Formal Verification) đang nổi lên mạnh mẽ trong giới nghiên cứu Ethereum cũng như trong toàn bộ lĩnh vực tính toán nói chung. Kỹ thuật này xác minh tính đúng đắn của mã nguồn bằng cách xây dựng các chứng minh toán học có thể tự kiểm tra được trong các công cụ chứng minh toán học như Lean, và được các nhà nghiên cứu gọi là “hình thái cuối cùng của phát triển phần mềm”. Bài viết chỉ ra rằng kiểm chứng hình thức đặc biệt phù hợp với những trường hợp mục tiêu đơn giản nhưng hiện thực hóa phức tạp, bao gồm chữ ký chống lại máy tính lượng tử, STARKs, các thuật toán đồng thuận và ZK-EVM—những công nghệ cốt lõi của Ethereum. Đồng thời, Vitalik nhấn mạnh rằng kiểm chứng hình thức không phải là “thuốc chữa bách bệnh”: hạn chế lớn nhất của nó là không thể nắm bắt đầy đủ ý định của con người, đồng thời tồn tại các rủi ro như thiếu sót trong đặc tả hoặc một phần mã nguồn không được kiểm tra.
Về vấn đề này, ông bày tỏ quan điểm lạc quan: sự kết hợp giữa trí tuệ nhân tạo (AI) và kiểm chứng hình thức sẽ tạo nên sự bổ trợ lẫn nhau—AI đảm nhiệm vai trò tạo ra khối lượng lớn mã nguồn một cách hiệu quả, còn kiểm chứng hình thức đảm bảo tính chính xác của mã đó. Trong tương lai, an ninh phần mềm sẽ được xây dựng theo mô hình kiến trúc “lõi an toàn + vùng biên không an toàn dạng hộp cát”, trong đó Ethereum sẽ trở thành một trong những “lõi an toàn” quan trọng.
