Vừa mới đọc xong bài viết mới nhất của Vitalik về xác minh chính thức và thực sự đáng để đọc. Ông ấy cơ bản đang phác thảo lý do tại sao các nhà phát triển trong không gian Ethereum ngày càng chuyển hướng tới phương pháp này, nơi bạn viết mã bằng các ngôn ngữ cấp thấp và sau đó chứng minh tính chính xác thông qua các bằng chứng toán học thay vì chỉ hy vọng các bài kiểm tra của bạn phát hiện mọi thứ.

Điều thú vị ở đây là sự chuyển đổi trong cách mọi người nghĩ về an ninh. Thay vì dựa vào kiểm thử thực nghiệm và kiểm toán mã (phương pháp truyền thống), có một mô hình mới nổi nơi các nhà phát triển xác nhận các đặc tính của chương trình thông qua các bằng chứng có thể kiểm tra bằng máy. Nó giống như chuyển an ninh từ 'chúng tôi nghĩ rằng điều này an toàn' sang 'điều này không thể thất bại theo cách này đã được chứng minh.' Hệ sinh thái đã bắt đầu áp dụng điều này cho hạ tầng quan trọng—các triển khai EVM, hệ thống chứng minh STARK, chữ ký chống lượng tử, và các giao thức như bằng chứng không biết (zero-knowledge proofs) hỗ trợ phần lớn các giao tiếp crypto hiện đại.

Nhưng đây là phần thực sự quan trọng: Vitalik cẩn thận lưu ý rằng đây không phải là viên đạn bạc. Xác minh chính thức có những giới hạn thực sự. Các định nghĩa về an ninh vẫn phụ thuộc vào cách con người mô hình hóa vấn đề. Một số hệ thống quá phức tạp để có thể hoàn toàn chính thức hóa. Và luôn có lớp phần cứng hoặc các mô-đun chưa được xác minh có thể trở thành các bề mặt tấn công. Ngay cả với các bằng chứng toán học chắc chắn, nếu đặc tả của bạn sai hoặc bạn bỏ lỡ một giả định, bạn vẫn dễ bị tấn công.

Quan điểm thực tế hơn mà Vitalik đề xuất là kết hợp xác minh chính thức với các phương pháp khác—lập trình hỗ trợ AI, hệ thống kiểu dữ liệu, khung kiểm thử. Ông ấy gợi ý rằng chúng ta đang hướng tới một tương lai nơi mã lệnh thể hiện ý định một cách dư thừa và tự động xác minh tính nhất quán. Khi AI bắt đầu tạo mã quy mô lớn, các hệ thống sẽ tự nhiên phân chia thành hai loại: các mô-đun biên dễ bị tấn công và các lõi an ninh cực kỳ đáng tin cậy.

Cơ hội thực sự nằm ở việc tập trung nỗ lực xác minh chính thức vào các hệ thống quan trọng—các giao thức blockchain, kernel hệ điều hành, những thứ mà thất bại có thể gây ra hậu quả dây chuyền. Đó là nơi bạn thu được lợi nhuận cao nhất từ công sức bỏ ra. Không phải là chứng minh mọi thứ, mà là củng cố chiến lược hạ tầng mà mọi thứ khác dựa vào.

Thông tin về việc áp dụng xác minh chính thức và tích hợp bằng chứng không biết phản ánh một sự trưởng thành rộng hơn trong cách ngành công nghiệp tiếp cận an ninh. Đáng chú ý nếu bạn đang theo dõi các phát triển ở cấp giao thức.