Hội nghị học giả Web3: Giáo sư Yale đề xuất mô hình xác minh giao thức nhận thức chung sáng tạo
Hội nghị học giả Web3 năm 2025 vừa được tổ chức, giáo sư Shao Zhong từ khoa khoa học máy tính của Đại học Yale đã có bài phát biểu chính. Ông lần đầu tiên công khai mô hình LiDO và khung mở rộng LiDO-DAG mà đội ngũ của ông phát triển. Thành tựu đột phá này nhằm cung cấp sự bảo mật và chứng minh tính khả thi có thể cơ khí hóa cho giao thức đồng thuận Byzantine Fault Tolerance (BFT) phức tạp, đặt nền tảng kỹ thuật 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 của mình chỉ ra rằng, các giao thức nhận thức chung hiện tại tuy được ứng dụng rộng rãi, nhưng do việc thực hiện phức tạp 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 đã đổi mới đề xuất một khung xác minh tinh chỉnh ba lớp:
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);
Lớp bảo vệ hoạt tính: Giới thiệu cơ chế "Pacemaker", thông qua phát sóng quá thời gian và đồng bộ vòng để giải quyết vấn đề độ trễ mạng;
Lớp mở rộng DAG: Hỗ trợ giao thức DAG mới nổi, thực hiện xác minh hiệu quả của Nhận thức chung không có lãnh đạo.
Hiện tại, LiDO đã thành công trong việc áp dụng vào các giao thức công nghiệp và nhiều giao thức DAG, hoàn thành việc chứng minh cơ khí hơn 10.000 dòng mã Coq, với mã kiểm tra an toàn và tính khả thi lần lượt đạt 4.000 dòng và 1.700 dòng. Giáo sư Shao Zhong trong bài phát biểu của mình đã chỉ ra: "Hiện nay, các giao thức đồng thuận PoS thường phải đối mặt với tình huống khó khăn khi không thể đạt được cả ba yếu tố an toàn, tính khả thi và tính phi tập trung. Mô hình LiDO chính là một giải pháp thiết kế hệ thống được đưa ra để phá vỡ tình trạng này."
Giáo sư Shao Zhong dẫn dắt đội ngũ phát triển CertiKOS, hệ điều hành "không có lỗ hổng" đầu tiên trên thế giới được xác minh thông qua kiểm tra hình thức, được ca ngợi là "cột mốc an toàn cho hệ thống mạng vật lý". Thành tựu này không chỉ đặt nền tảng công nghệ cho công ty của ông, mà còn thể hiện sự tích lũy sâu 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 đã đào sâu vào an toàn blockchain, vào năm 2017 cùng với học trò của mình, giáo sư Gu Ronghui, thành lập công ty, đưa 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, bảo vệ an toàn tài sản tiền điện tử trị giá hàng tỷ đô la.
LiDO hiện đã hoàn thành thiết kế mô hình 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à 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ế then chốt trong Web3.0 để 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 dài hạn của các doanh nghiệp và hệ sinh thái Web3. Cuối buổi diễn thuyết, giáo sư Shao Trung nhấn mạnh: "Mạng lưới giao thức tin cậy, an toàn và có thể xác minh sẽ là con đường then chốt dẫn đến tương lai thực sự phi tập trung."
Trang này có thể chứa nội dung của bên thứ ba, được cung cấp chỉ nhằm mục đích thông tin (không phải là tuyên bố/bảo đảm) và không được coi là sự chứng thực cho quan điểm của Gate hoặc là lời khuyên về tài chính hoặc chuyên môn. Xem Tuyên bố từ chối trách nhiệm để biết chi tiết.
Giáo sư Yale công bố mô hình LiDO, vượt qua khó khăn trong việc xác minh giao thức nhận thức chung Web3.
Hội nghị học giả Web3: Giáo sư Yale đề xuất mô hình xác minh giao thức nhận thức chung sáng tạo
Hội nghị học giả Web3 năm 2025 vừa được tổ chức, giáo sư Shao Zhong từ khoa khoa học máy tính của Đại học Yale đã có bài phát biểu chính. Ông lần đầu tiên công khai mô hình LiDO và khung mở rộng LiDO-DAG mà đội ngũ của ông phát triển. Thành tựu đột phá này nhằm cung cấp sự bảo mật và chứng minh tính khả thi có thể cơ khí hóa cho giao thức đồng thuận Byzantine Fault Tolerance (BFT) phức tạp, đặt nền tảng kỹ thuật 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 của mình chỉ ra rằng, các giao thức nhận thức chung hiện tại tuy được ứng dụng rộng rãi, nhưng do việc thực hiện phức tạp 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 đã đổi mới đề xuất một khung xác minh tinh chỉnh ba lớp:
Hiện tại, LiDO đã thành công trong việc áp dụng vào các giao thức công nghiệp và nhiều giao thức DAG, hoàn thành việc chứng minh cơ khí hơn 10.000 dòng mã Coq, với mã kiểm tra an toàn và tính khả thi lần lượt đạt 4.000 dòng và 1.700 dòng. Giáo sư Shao Zhong trong bài phát biểu của mình đã chỉ ra: "Hiện nay, các giao thức đồng thuận PoS thường phải đối mặt với tình huống khó khăn khi không thể đạt được cả ba yếu tố an toàn, tính khả thi và tính phi tập trung. Mô hình LiDO chính là một giải pháp thiết kế hệ thống được đưa ra để phá vỡ tình trạng này."
Giáo sư Shao Zhong dẫn dắt đội ngũ phát triển CertiKOS, hệ điều hành "không có lỗ hổng" đầu tiên trên thế giới được xác minh thông qua kiểm tra hình thức, được ca ngợi là "cột mốc an toàn cho hệ thống mạng vật lý". Thành tựu này không chỉ đặt nền tảng công nghệ cho công ty của ông, mà còn thể hiện sự tích lũy sâu 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 đã đào sâu vào an toàn blockchain, vào năm 2017 cùng với học trò của mình, giáo sư Gu Ronghui, thành lập công ty, đưa 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, bảo vệ an toàn tài sản tiền điện tử trị giá hàng tỷ đô la.
LiDO hiện đã hoàn thành thiết kế mô hình 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à 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ế then chốt trong Web3.0 để 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 dài hạn của các doanh nghiệp và hệ sinh thái Web3. Cuối buổi diễn thuyết, giáo sư Shao Trung nhấn mạnh: "Mạng lưới giao thức tin cậy, an toàn và có thể xác minh sẽ là con đường then chốt dẫn đến tương lai thực sự phi tập trung."