Nhóm nghiên cứu của Ethereum cho biết dự án Etheorem, xây dựng một đặc tả đồng thuận Ethereum có thể thực thi bằng ngôn ngữ chứng minh định lý Lean 4, đã đạt cột mốc mới khi vượt qua toàn bộ vector kiểm thử cho ba phiên bản hard fork sắp tới: Fulu, Gloas và Heze.

Theo bản cập nhật nghiên cứu, dự án sử dụng xác minh hình thức thay vì kiểm thử mã nguồn thông thường để kiểm tra logic đồng thuận của Ethereum. Mục tiêu là phát hiện sớm các điểm yếu logic và giảm khả năng chuỗi bị phân tách do các triển khai client khác nhau diễn giải quy tắc theo những cách khác nhau.

Tiến triển mới nhất bao gồm các lĩnh vực cốt lõi như chuyển đổi trạng thái và lựa chọn fork. Nhóm cho biết logic được kernel Lean xác minh độc lập, đưa khuôn khổ này thành một lớp nền có mức đảm bảo cao hơn cho các nâng cấp Ethereum trong tương lai. Thông báo không cho biết liệu đặc tả đã được các client sản xuất áp dụng trực tiếp hay chưa, cũng không nêu lịch trình triển khai ngoài phạm vi fork đã đề cập.

Công việc này nhắm vào một điểm yếu đã biết trong sự đánh đổi thiết kế của Ethereum. Ethereum dựa vào nhiều client được xây dựng độc lập thay vì một cơ sở mã nguồn duy nhất chiếm ưu thế, điều này cải thiện khả năng phục hồi nhưng cũng tạo ra khả năng phân kỳ nếu các triển khai hiểu sai hoặc mã hóa các thay đổi giao thức không nhất quán.

Rủi ro đó vẫn là một vấn đề kỹ thuật hiện hữu trong toàn hệ sinh thái. Các nỗ lực phát triển rộng hơn của Ethereum trong những năm gần đây ngày càng nhấn mạnh sự đa dạng client, củng cố đồng thuận và xác minh hình thức như một phần của khả năng phục hồi giao thức dài hạn, đặc biệt khi các nâng cấp sắp tới trở nên phức tạp hơn về mặt kỹ thuật.

Vì sao điều này quan trọng

Bản cập nhật này quan trọng vì tập trung vào hạ tầng bảo mật của Ethereum thay vì ra mắt một tính năng hướng đến người dùng. Việc chính thức hóa đặc tả đồng thuận trong một hệ thống được xác minh bằng toán học có thể tăng cường độ tin cậy của các nâng cấp và giảm xác suất xảy ra lỗi đồng thuận ảnh hưởng đến trình xác thực, tính chung cuộc và sự phối hợp của mạng.

Điều này cũng cho thấy sự thay đổi rộng hơn trong cách các blockchain lớn quản lý rủi ro giao thức. Khi Ethereum bổ sung các tính năng tinh vi hơn, các phương pháp xác minh có mức đảm bảo cao hơn có thể trở nên quan trọng hơn trong việc thu hẹp khoảng cách giữa các đặc tả bằng văn bản và hành vi thực tế của client.