Đồng sáng lập Ethereum Vitalik Buterin đã đăng một bài phân tích chuyên sâu vào ngày 18/5, đánh giá hiện trạng và triển vọng của kỹ thuật xác minh hình thức (Formal Verification). Ông cho rằng xác minh hình thức được hỗ trợ bởi AI sẽ trở thành “dạng thức cuối cùng của phát triển phần mềm”, đồng thời chỉ ra rằng Ethereum sẽ là một phần quan trọng trong cấu trúc “lõi an toàn” trong tương lai.
Nguyên lý cốt lõi và các trường hợp áp dụng của xác minh hình thức
Theo phần xác nhận trong bài viết của Vitalik, xác minh hình thức đặc biệt phù hợp với các tình huống mà “mục tiêu quan trọng hơn việc thực hiện”. Ông cũng liệt kê rõ 4 nhóm thành phần kỹ thuật cốt lõi trong giai đoạn nâng cấp tiếp theo của Ethereum:
Chữ ký kháng lượng tử: công việc xác minh hình thức cho các biến thể chữ ký SPHINCS đã được triển khai
Hệ thống chứng minh STARK: dự án Arklib hướng tới việc tạo ra hiện thực STARK được xác minh hoàn toàn bằng hình thức
Thuật toán đồng thuận chịu lỗi Byzantine: hiện đang tập trung vào việc đặc tả chính thức và chứng minh các thuộc tính an toàn của đồng thuận dựa trên Lean
ZK-EVM: dự án evm-asm nhằm xây dựng hiện thực EVM được xác minh hình thức đầy đủ (viết trực tiếp bằng ngôn ngữ hợp ngữ RISC-V)
Vitalik trích dẫn quan điểm của Hiirai Yōichi, gọi phương pháp này là “dạng thức cuối cùng của phát triển phần mềm”.
Hướng phát triển của kiến trúc “lõi an toàn” theo mô tả của Vitalik
Theo phần xác nhận trong bài viết của Vitalik, ông mô tả mô hình tiến hoá của kiến trúc phần mềm trong tương lai:
Lõi an toàn: liên tục được củng cố bằng phương pháp hình thức, gánh vác mức tin cậy cao nhất; Vitalik nêu rõ Ethereum, lõi của hệ điều hành và các ứng dụng liên quan đến IoT sẽ trở thành lõi an toàn.
Biên không an toàn: các thành phần biên chạy trong môi trường sandbox, được cấp quyền tối thiểu cần thiết để hoàn thành công việc; nếu thành phần biên gặp lỗi, lõi an toàn sẽ cung cấp lớp bảo vệ.
Giới hạn xác nhận và các kiểu thất bại của xác minh hình thức
Vitalik thừa nhận rằng xác minh hình thức không phải “vạn năng”. Ông dẫn lại công trình của các nhà nghiên cứu như Nadim Kobeissi (Cryspen) và xác nhận 3 kiểu thất bại chính: bỏ sót một phần xác minh (chỉ kiểm tra một phần mã, trong khi phần chưa được kiểm tra có thể chứa lỗ hổng quan trọng); thiếu sót trong đặc tả (bản thân quy định an toàn có lỗi hoặc trong phép chứng có giả định sai); tấn công kênh bên (các cuộc tấn công qua kênh bên tại ranh giới giữa phần cứng và phần mềm khó được mô hình hiện có bắt được).
Vitalik nhấn mạnh rằng “tính đúng đắn có thể chứng minh” về bản chất chỉ xác minh tính nhất quán nội tại giữa các cách diễn đạt ý định khác nhau, chứ không phải sự tương ứng tuyệt đối với ý định thực sự của con người.
Các công cụ xác minh hình thức được hỗ trợ bởi AI
Theo các công cụ được Vitalik xác nhận trong bài viết: Lean (ngôn ngữ chứng minh toán học, có thể tự động xác minh định lý); Claude và Deepseek 4 Pro (Vitalik xác nhận đủ để dùng cho việc viết các chứng minh Lean); Leanstral (mô hình mã nguồn mở với trọng số 1190 tỷ tham số, được tinh chỉnh chuyên cho việc viết bằng Lean, có thể chạy cục bộ; hiệu năng trong benchmark tốt hơn nhiều so với các mô hình đa dụng cỡ lớn hơn).
Các câu hỏi thường gặp
Vì sao Vitalik cho rằng Ethereum nên trở thành “lõi an toàn”?
Theo bài viết của Vitalik, Ethereum tương tự như lõi của hệ điều hành, gánh vác mức độ tin cậy cao nhất trong quá trình số hoá xã hội. Ông cho biết mục tiêu thiết kế của lõi an toàn là đạt đến mức an toàn không cho phép tình trạng mã có lỗi tràn lan, đồng thời dồn toàn bộ năng lực tính toán bổ sung do AI mang lại vào việc nâng cao độ an toàn của lõi an toàn.
Vì sao xác minh hình thức đặc biệt phù hợp với các kỹ thuật như STARK, ZK-EVM?
Theo phân tích của Vitalik, điểm chung của các công nghệ này là “mục tiêu khó hơn nhiều so với việc hiện thực hoá” — các thuộc tính an toàn có thể được định nghĩa rõ ràng bằng ngôn ngữ toán học, nhưng phần hiện thực cụ thể lại vô cùng phức tạp, đúng là kiểu bối cảnh mà xác minh hình thức phát huy tác dụng mạnh nhất.
Vitalik khuyên nhà phát triển sử dụng AI hỗ trợ xác minh hình thức như thế nào trong thực tế?
Theo bài viết của Vitalik, ông khuyên để AI viết mã Lean và các chứng minh toán học, còn người dùng cuối cùng chỉ cần kiểm tra các câu/đoạn được chứng minh có phù hợp với kỳ vọng hay không, không cần tự viết mã chứng minh chi tiết ở lớp nền. Ông xác nhận Claude, Deepseek 4 Pro và Leanstral là các công cụ chính hiện đang có thể dùng.
Tuyên bố miễn trừ trách nhiệm: Thông tin trên trang này có thể đến từ các nguồn bên thứ ba và chỉ mang tính chất tham khảo. Thông tin này không phản ánh quan điểm hoặc ý kiến của Gate và không cấu thành bất kỳ lời khuyên tài chính, đầu tư hoặc pháp lý nào. Giao dịch tài sản ảo tiềm ẩn rủi ro cao. Vui lòng không chỉ dựa vào thông tin trên trang này khi đưa ra quyết định. Để biết thêm chi tiết, vui lòng xem
Tuyên bố miễn trừ trách nhiệm.
