Sonic Labs ra mắt Thư viện xác minh chính thức cho Giao thức đồng thuận DAG

Đội ngũ đứng sau blockchain Lớp 1 hiệu suất cao Sonic, Phòng thí nghiệm âm thanh đã giới thiệu một thư viện xác minh chính thức được thiết kế để tăng cường bảo mật trong các giao thức đồng thuận dựa trên DAG. Dưới sự chỉ đạo của Giám đốc nghiên cứu Tiến sĩ Bernhard Scholz, thư viện này nhằm mục đích cung cấp bằng chứng toán học về tính an toàn cho các blockchain Đồ thị không có chu trình có hướng (DAG), bao gồm cả mạng tương thích EVM của Sonic.

Được phát triển với sự hợp tác của các nhà nghiên cứu từ Đại học Sydney và INRIA, thư viện nguồn mở được xây dựng bằng trợ lý chứng minh TLA+. Nó cung cấp một khuôn khổ mô-đun và có thể tái sử dụng giúp hợp lý hóa quy trình mô hình hóa và xác minh cơ chế đồng thuận dựa trên kiến ​​trúc DAG.

Thư viện xác minh có các bằng chứng chính thức cho một số giao thức dựa trên DAG hiện có, chẳng hạn như DAG-Rider, Cordial Miner, Bullshark, Hashgraph và Aleph. Giao thức độc quyền của Sonic cũng đã được xác minh là một sản phẩm phái sinh trong khuôn khổ này. Nghiên cứu này lần đầu tiên được trình bày tại hội nghị NASA Formal Methods 2025, được tổ chức tại Williamsburg, Virginia, từ ngày 11 đến ngày 13 tháng XNUMX và thể hiện sự tiến bộ đáng chú ý trong các tiêu chuẩn xác minh blockchain.

Tiến sĩ Bernhard Scholz, Giám đốc nghiên cứu tại Sonic Labs, cho biết trong một tuyên bố bằng văn bản: "Trong blockchain, các lỗi bảo mật thường bắt nguồn từ các giả định không được kiểm tra cho đến khi quá muộn". "Với thư viện này, chúng tôi đang chuyển từ hy vọng sang bằng chứng, cung cấp các công cụ để xác minh với độ chắc chắn về mặt toán học rằng một giao thức sẽ hoạt động an toàn trong mọi điều kiện. Mục tiêu của chúng tôi là làm cho việc xác minh chính thức có thể tiếp cận được với mọi nhà phát triển giao thức", ông nói thêm.

Khi giá trị Blockchain tăng vọt, Sonic Labs ra mắt khuôn khổ xác minh chính thức để đảm bảo tính bảo mật và độ tin cậy của giao thức

Khi giá trị được bảo đảm bởi các mạng blockchain tiếp tục tăng, tác động tiềm tàng của các lỗ hổng trong các giao thức đồng thuận ngày càng trở nên đáng kể, với các rủi ro bao gồm chi tiêu gấp đôi và trạng thái sổ cái không nhất quán. Kiểm tra thông thường và kiểm toán mã bị hạn chế về khả năng đảm bảo các hệ thống không có lỗi. Để ứng phó, một phương pháp xác minh chính thức đã được áp dụng bởi Phòng thí nghiệm âm thanh , sử dụng các bằng chứng toán học để xác nhận tính bảo mật của giao thức trong mọi điều kiện có thể.

Phương pháp này không chỉ xác thực các giao thức đồng thuận hiện có mà còn hỗ trợ các nhà phát triển đang thiết kế các mô hình mới dựa trên Directed Acyclic Graph hoặc điều chỉnh các mô hình hiện tại. Phương pháp này hiện đang được triển khai để xác minh chính thức rằng blockchain Sonic không thể biểu hiện hành vi không an toàn, thiết lập độ tin cậy của giao thức thông qua xác thực toán học.

Bằng cách công khai thư viện xác minh, sáng kiến ​​này cung cấp cho các nhà phát triển blockchain các nguồn lực để xây dựng các hệ thống an toàn có thể chứng minh được. Điều này dự kiến ​​sẽ cải thiện khả năng phục hồi tổng thể của các hệ sinh thái phi tập trung và giảm nhu cầu về nguồn lực thường liên quan đến xác minh giao thức đồng thuận.