Hội nghị học giả Web3 lần đầu tiên công bố mô hình LiDO: Cung cấp xác minh cơ học cho giao thức nhận thức chung phức tạp

Tại Hội nghị học giả Web3 năm 2025, giáo sư Shao Zhong của Khoa Khoa học Máy tính, Đại học Yale đã có bài phát biểu chủ đề mang tên "Bằng chứng an toàn và hoạt động của giao thức nhận thức chung dựa trên tinh chỉnh: LiDO và các mở rộng của nó". Đây là lần đầu tiên ông công bố mô hình LiDO và khung mở rộng LiDO-DAG mà nhóm của ông phát triển. Thành tựu đột phá này nhằm cung cấp bằng chứng an toàn và hoạt động có thể xác minh cơ học cho các giao thức nhận thức chung Byzantine Fault Tolerance (BFT), từ đó đặt nền tảng công nghệ cho sự tin cậy và phát triển quy mô của hệ sinh thái Web3.

Giáo sư Shao Zhong trong bài phát biểu đã chỉ ra rằng, mặc dù các giao thức nhận thức chung hiện có (như PBFT, Jolteon) đã được áp dụng rộng rãi, nhưng do tính phức tạp trong việc thực hiện, thường tiềm ẩn những lỗ hổng. Để giải quyết vấn đề này, mô hình LiDO đã đổi mới đề xuất một khung xác minh tinh chỉnh ba lớp:

1. Lớp trừu tượng an toàn: ánh xạ giao thức thành máy trạng thái tuyến tính, đảm bảo tính nhất quán của nhật ký (an toàn);
2. Lớp bảo đảm hoạt tính: Giới thiệu cơ chế "Pacemaker", giải quyết vấn đề độ trễ mạng thông qua phát sóng quá thời gian và đồng bộ vòng.
3. Lớp mở rộng DAG: Hỗ trợ các giao thức DAG mới nổi như Narwhal, Bullshark, thực hiện xác thực hiệu quả của Nhận thức chung không có người lãnh đạo.

Hiện tại, LiDO đã thành công trong việc áp dụng vào giao thức công nghiệp Jolteon (BFT hai giai đoạn) và nhiều giao thức DAG, hoàn thành việc chứng minh cơ học cho hơn mười ngàn dòng mã Coq, trong đó mã kiểm tra an toàn và hoạt động lần lượt đạt 4000 dòng và 1700 dòng. Giáo sư Shao Zhong nhấn mạnh: "Hiện nay, giao thức nhận thức chung PoS đang đối mặt với khó khăn trong việc đạt được an toàn, hoạt động và phi tập trung đồng thời. Mô hình LiDO chính là giải pháp thiết kế hệ thống được đưa ra nhằm phá vỡ khó khăn này."

Là nhà phát triển chính của hệ điều hành "không có lỗi" CertiKOS, hệ điều hành đầu tiên trên thế giới được xác minh bằng hình thức, Giáo sư Shao Zhong đã tích lũy được kinh nghiệm sâu sắc trong lĩnh vực an ninh hệ thống. Thành tựu này không chỉ củng cố vị thế của ông trong lĩnh vực công nghệ an toàn mà còn khẳng định khả năng chuyên môn của đội ngũ của ông trong lĩnh vực an ninh hệ thống. Trong những năm gần đây, Giáo sư Shao Zhong đã chuyển trọng tâm nghiên cứu sang an ninh blockchain, vào năm 2017, ông cùng với các đối tác thành lập một công ty chuyên về an ninh blockchain, áp dụng công nghệ xác minh hình thức vào việc bảo đảm an toàn cho hợp đồng thông minh và giao thức trên chuỗi, cung cấp bảo vệ an toàn cho các tài sản tiền điện tử trị giá hàng trăm tỷ đô la.

Mô hình LiDO hiện đã hoàn thành thiết kế và xác minh hình thức, và bắt đầu khám phá khả năng tích hợp với các chuỗi công khai và giao thức phi tập trung phổ biến. Giáo sư Shao Trung cho biết, họ cam kết xác minh các cơ chế chính trong Web3.0 để cung cấp sản phẩm và dịch vụ trong toàn bộ chu kỳ, hỗ trợ tốt hơn cho chiến lược phát triển lâu dài của các doanh nghiệp và hệ sinh thái Web3. Cuối buổi thuyết trình, giáo sư Shao Trung nhấn mạnh: "Một ngăn xếp giao thức mạng đáng tin cậy, an toàn và có thể xác minh sẽ là con đường chính dẫn đến tương lai phi tập trung thực sự."