Tại hội nghị các học giả Web3, giáo sư Shao Zhong đã công bố mô hình LiDO, thúc đẩy việc xác minh an toàn giao thức nhận thức chung.

Hội nghị học giả Web3 năm 2025 vừa diễn ra, 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 "Chứng minh an toàn và tính khả thi của giao thức nhận thức chung dựa trên sự tinh chỉnh: LiDO và mở rộng của nó". Ông đã công bố lần đầu tiên mô hình LiDO và khung mở rộng LiDO-DAG do nhóm của mình phát triển, thành tựu đột phá này nhằm cung cấp chứng minh an toàn và tính khả thi có thể cơ giới hóa cho các giao thức nhận thức chung BFT phức tạp, đặt nền tảng kỹ thuật cho sự phát triển đáng tin cậy và quy mô của hệ sinh thái Web3.

Giáo sư Shao Zhong trong bài phát biểu của mình đã chỉ ra rằng, các giao thức nhận thức chung hiện có như PBFT và Jolteon mặc dù được ứng dụng rộng rãi, nhưng do độ phức tạp trong việc thực hiện cao, thường ẩn chứa các lỗ hổng tiềm ẩn. Để giải quyết vấn đề này, mô hình LiDO đã sáng tạo ra một khung xác thực 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 minh hiệu quả nhận thức chung không 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 hơn mười nghìn dòng mã Coq trong chứng minh cơ học, trong đó mã xác minh an toàn và tính năng đạt lần lượt 4000 dòng và 1700 dòng. Giáo sư Shao Trung nhấn mạnh: "Hiện nay, các giao thức đồng thuận PoS đang phải đối mặt với khó khăn khi không thể đạt được đồng thời ba yếu tố an toàn, tính năng và phi tập trung. Mô hình LiDO chính là giải pháp thiết kế hệ thống được đưa ra để vượt qua nút thắt này."

Là một trong những nhà phát triển chính của hệ điều hành "không lỗ hổng" CertiKOS được xác minh một cách hình thức đầu tiên trên thế giới, giáo sư Shao Zhong đã tích lũy được nhiều kinh nghiệm trong lĩnh vực an toàn hệ thống. Thành tựu này không chỉ đặt nền tảng vững chắc cho các nghiên cứu tiếp theo của ông, mà còn thể hiện những đóng góp xuất sắc của ông trong lĩnh vực an toàn 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 toàn blockchain, và vào năm 2017, ông cùng các đối tác đã thành lập một công ty an ninh, tập trung vào việc áp dụng công nghệ xác minh hình thức vào bảo đảm an toàn cho hợp đồng thông minh và giao thức trên chuỗi, nhằm bảo vệ hàng trăm tỷ đô la tài sản tiền điện tử.

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 chính và các giao thức phi tập trung. Giáo sư Shao Trung cho biết, họ cam kết xác minh các cơ chế quan trọng trong Web3.0, nhằm cung cấp sản phẩm và dịch vụ toàn 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 bài phát biểu, giáo sư Shao Trung nhấn mạnh: "Giao thức mạng đáng tin cậy, an toàn, có thể xác minh sẽ là con đường then chốt dẫn đến tương lai phi tập trung thực sự."