Xác minh chính thức? Nó là gì? Tìm hiểu thêm 🧵
Hàng triệu triệu đô la đang nằm trong các blockchain. Một lỗi đồng thuận = rút tiền ngay lập tức. Kiểm tra có thể phát hiện lỗi nhưng không thể chứng minh rằng chúng là không thể xảy ra. Xác minh chính thức cho các giao thức dựa trên DAG thay đổi cuộc chơi đó.
Xác minh chính thức mô hình hóa một giao thức như một máy trạng thái và cho phép một người chứng minh kiểm tra một cách toàn diện mọi chuyển tiếp—không chỉ là một mẫu thử.
Phần khó khăn? Việc viết chứng minh thì chậm. Sự hiểu biết của Sonic: chia nhỏ các giao thức thành các khối xây dựng có thể tái sử dụng thay vì phải phát minh lại các chứng minh mỗi lần.
Sonic Labs vừa mã nguồn mở một thư viện TLA+ mà chứng minh toán học tính an toàn cho DAG-Rider, Hashgraph, Bullshark, Aleph và nhiều hơn nữa—không có tường phí, không có NDA.
Dijkstra: “Kiểm tra chương trình có thể chỉ ra sự hiện diện của lỗi, nhưng không bao giờ có thể chứng minh sự vắng mặt của chúng.” Các chứng minh mang đến cho bạn phần vắng mặt.
Thư viện chia mọi thứ thành hai phần:
• Xây dựng DAG 🌳
• Sắp xếp / bầu cử lãnh đạo 🗳️
Mỗi khối có đặc điểm riêng + chứng minh được kiểm tra bằng máy.
Mất khoảng ~14 tháng người với 5 nhà nghiên cứu để mô hình hóa 5 giao thức. Việc thêm một giao thức thứ 6 bây giờ chỉ mất vài ngày, không phải vài tháng.
Công trình đã ra mắt tại NASA Formal Methods 2025. Nếu nó đủ mạnh cho tên lửa, thì có lẽ cũng tốt cho Sonic!
Lưu ý: những bằng chứng này bao gồm an toàn (không có fork, không có chi tiêu gấp đôi). Chúng không khắc phục được tính khả dụng hoặc các cuộc tấn công kinh tế - nhưng việc loại bỏ hoàn toàn các loại lỗi an toàn là một chiến thắng lớn.
Tóm lại — Danh sách kiểm tra kiểm toán là của năm 2020. Bằng chứng mở, có thể kết hợp là của năm 2025. Hãy biến "an toàn có thể chứng minh" thành mặc định trong crypto.
Blog →
Mã →
4,83 N
35
Nội dung trên trang này được cung cấp bởi các bên thứ ba. Trừ khi có quy định khác, OKX không phải là tác giả của bài viết được trích dẫn và không tuyên bố bất kỳ bản quyền nào trong các tài liệu. Nội dung được cung cấp chỉ nhằm mục đích thông tin và không thể hiện quan điểm của OKX. Nội dung này không nhằm chứng thực dưới bất kỳ hình thức nào và không được coi là lời khuyên đầu tư hoặc lời chào mời mua bán tài sản kỹ thuật số. Việc sử dụng AI nhằm cung cấp nội dung tóm tắt hoặc thông tin khác, nội dung do AI tạo ra có thể không chính xác hoặc không nhất quán. Vui lòng đọc bài viết trong liên kết để biết thêm chi tiết và thông tin. OKX không chịu trách nhiệm về nội dung được lưu trữ trên trang web của bên thứ ba. Việc nắm giữ tài sản kỹ thuật số, bao gồm stablecoin và NFT, có độ rủi ro cao và có thể biến động rất lớn. Bạn phải cân nhắc kỹ lưỡng xem việc giao dịch hoặc nắm giữ tài sản kỹ thuật số có phù hợp hay không dựa trên tình hình tài chính của bạn.