Vitalik Buterin: AI kết hợp kiểm chứng hình thức có thể tăng mạnh an toàn cho crypto

Vitalik Buterin: AI kết hợp với kiểm chứng hình thức có thể nâng độ an toàn của crypto

Vitalik Buterin cho rằng trí tuệ nhân tạo, nếu được dùng đúng cách cùng với phần mềm được kiểm chứng bằng toán học, có thể giúp hệ sinh thái tiền mã hóa và hạ tầng internet trọng yếu trở nên an toàn hơn. Quan điểm này được đồng sáng lập Ethereum nêu trong một bài viết dài đăng ngày 18/5/2026.

Ông nhấn mạnh rằng thay vì chỉ tạo ra mã nguồn nhanh hơn, AI có thể trở thành công cụ hỗ trợ phát hiện lỗi và xây dựng các bằng chứng xác minh cho phần mềm.

“Formal verification” là gì?

Kiểm chứng hình thức, hay formal verification, là phương pháp dùng các bằng chứng toán học mà máy có thể kiểm tra để đảm bảo phần mềm hoạt động đúng như thiết kế. Kỹ thuật này không mới, nhưng theo Buterin, những tiến bộ gần đây của AI đang khiến nó thực tế hơn đáng kể.

Lý do là AI có thể hỗ trợ lập trình viên trong cả hai việc:

• viết mã nguồn;
• tạo ra các chứng minh cần thiết để xác minh mã đó.

Vì sao Buterin xem đây là hướng đi quan trọng

Buterin đặt lập luận của mình trong bối cảnh mối lo ngày càng tăng rằng AI sẽ giúp tội phạm mạng tìm lỗ hổng nhanh hơn. Khi khả năng phát hiện lỗi được tăng tốc, bên phòng thủ có nguy cơ bị vượt mặt nếu vẫn dùng quy trình bảo mật truyền thống.

Trong lĩnh vực crypto, các vụ khai thác hợp đồng thông minh vẫn là vấn đề dai dẳng. Những kẻ tấn công thường rút hàng triệu USD từ các giao thức tài chính phi tập trung chỉ bằng một lỗ hổng nhỏ trong mã.

Theo Buterin, phần mềm được chứng minh bằng toán học có thể giúp đảo ngược xu hướng này, đặc biệt ở những nơi mà một lỗi nhỏ cũng gây hậu quả lớn.

Những mảng có thể hưởng lợi trực tiếp

Nhà đồng sáng lập Ethereum nêu rõ một số lĩnh vực mà formal verification có thể đặc biệt hữu ích:

1. Hạ tầng Ethereum.
2. Hệ thống zero-knowledge proof.
3. Cơ chế đồng thuận.
4. Mật mã hậu lượng tử.

Với các thành phần như vậy, rủi ro không chỉ nằm ở mất tiền, mà còn ở khả năng làm suy yếu cả lớp nền tảng của mạng lưới.

Buterin viết rằng lỗi trong phần mềm vốn đã đáng ngại, nhưng mức độ nguy hiểm còn lớn hơn nhiều khi mã đó điều khiển tài sản onchain không thể sửa đổi hoặc các hệ thống mật mã nâng cao.

AI không chỉ tạo rủi ro, mà còn có thể là một phần của lời giải

Bài viết của Buterin cũng phản biện quan điểm đang phổ biến trong một bộ phận giới nghiên cứu an ninh: rằng phần mềm do AI tạo ra ngày càng phức tạp đến mức không thể tin cậy hoàn toàn.

Ông cho rằng kịch bản tích cực hơn là AI sẽ giúp đội ngũ phát triển tìm và loại bỏ lỗ hổng nhanh hơn tốc độ khai thác của tin tặc.

Nói cách khác, AI có thể vừa là nguồn phát sinh rủi ro mới, vừa là công cụ giúp phòng thủ mạnh hơn nếu được kết hợp với quy trình xác minh chặt chẽ.

Nhưng đây không phải “liều thuốc chữa bách bệnh”

Dù lạc quan, Buterin vẫn lưu ý formal verification không giải quyết được mọi vấn đề. Một hệ thống được chứng minh toán học vẫn có thể gặp sự cố nếu:

• nhà phát triển xác minh sai giả định đầu vào;
• bỏ sót lỗ hổng từ phần cứng;
• hoặc để một phần nào đó của hệ thống không được kiểm tra.

Ông cũng cảnh báo rằng AI có thể giúp tạo ra lượng lớn mã nguồn rất nhanh, nhưng đổi lại là độ chính xác thấp hơn. Formal verification, theo ông, là cách để lấy lại phần “độ chính xác” đã mất đó.

Buterin kết luận rằng nếu chỉ để AI tạo ra mã ẩu, rủi ro sẽ tăng lên đáng kể. Tuy nhiên, nếu đi cùng kiểm chứng hình thức, tương lai an ninh mạng vẫn có thể đi theo hướng tích cực hơn.