TechFlow đưa tin, ngày 18 tháng 5, Vitalik đã đăng bài viết có tựa đề “Một cái nhìn sơ lược về kiểm chứng hình thức”, giới thiệu tiến triển trong việc ứng dụng kiểm chứng hình thức vào nghiên cứu và phát triển tiên phong của Ethereum. Bài viết nêu rõ rằng các nhà phát triển có thể viết mã bằng ngôn ngữ Lean, bytecode EVM hoặc ngôn ngữ lắp ráp (assembly), sau đó sử dụng các chứng minh toán học có thể kiểm tra tự động để xác minh tính đúng đắn của mã, từ đó đồng thời nâng cao hiệu quả và độ an toàn của mã.
Ông cho biết kiểm chứng hình thức đặc biệt phù hợp với những hệ thống phức tạp nhưng mục tiêu bảo mật tương đối rõ ràng, chẳng hạn như STARK, cơ chế đồng thuận chịu lỗi Byzantine (BFT), ZK-EVM và chữ ký kháng lượng tử; đồng thời đề cập đến một số dự án liên quan như Arklib, VCV-io và evm-asm. Bài viết cũng 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”: nó vẫn có thể bị giới hạn bởi các vấn đề như định nghĩa đặc tả sai, mã chưa được kiểm tra đầy đủ, ranh giới phần cứng và các cuộc tấn công kênh bên (side-channel attacks).
