Lỗi của @Zcash dẫn đến Ironwood, xác minh hình thức cho mạch thanh toán Orchard. Tôi yêu thích và ủng hộ điều này. Tôi cũng muốn nhấn mạnh rằng @Starknet đã thực hiện việc này — xác minh hình thức — trong hơn 5 năm qua. Việc hỗ trợ các dự án tuyệt vời như Zcash vì phản ứng nhanh chóng, như trong trường hợp này, là rất quan trọng. Đồng thời, cũng rất quan trọng để ghi nhận những dự án có tính tương lai và đi trước xu hướng, như Starknet. (Chi tiết trong bài viết bên dưới) Tôi đã từng nói nhiều lần rằng Starknet là hệ thống đã sở hữu những thứ mà các chuỗi khác tuyên bố sẽ có trong tương lai gần. Điều này đã đúng với nhiều khía cạnh. Chúng tôi đã ở tuyến đầu của nhiều lựa chọn không phổ biến nhưng giờ đây ai cũng công nhận là quan trọng, bao gồm ZK-STARKs bảo mật sau lượng tử như giải pháp tối ưu cho khả năng mở rộng và bảo mật, zkVM nhẹ (Cairo là tốt nhất), khả năng sẵn có dữ liệu Validium và xác minh hình thức. Xác minh hình thức có nghĩa là bạn sử dụng các công cụ tự động như hệ thống Lean để chứng minh toán học rằng mã của bạn là an toàn. Việc nắm bắt đầy đủ từng khía cạnh của khái niệm “mã an toàn” là rất khó, nhưng dưới sự dẫn dắt của CTO @LiorGoldberg2 (đồng sáng tạo Cairo zkVM và ngôn ngữ), chúng tôi đã làm điều này trong hơn 5 năm. Bài báo đầu tiên về xác minh hình thức liên quan đến ZK (Giáo sư Jeremy Avigad, Yoav Seginer và những người khác) đã chứng minh rằng tập các ràng buộc đa thức định nghĩa Cairo VM là chính xác. Nếu bạn theo dõi tin tức gần đây, lỗi vừa được phát hiện bởi AI và hiện đã được sửa cho Zcash (một dự án khác mà tôi đồng sáng lập, và tôi rất tự hào cũng như ủng hộ) liên quan đến một ràng buộc bị thiếu. Quyết định xác minh mã của họ để loại bỏ các lỗi tương tự là bước đi đúng đắn. Việc chạy xác minh loại này cho Cairo core VM đã mang lại cho chúng tôi, đội ngũ StarkWare, sự chắc chắn toán học rằng không có ràng buộc nào bị thiếu trong Cairo VM của chúng tôi. Vì vậy, ngoài việc chứng minh Cairo core VM, chúng tôi còn chứng minh hệ thống S-two STARK, một phần của trình biên dịch, và nhiều hàm trong thư viện Cairo tiêu chuẩn. Công việc đã hoàn tất chưa? Chưa. Còn rất nhiều điều khác có thể được chứng minh một cách hình thức. Nhưng chúng tôi cam kết tiếp tục chứng minh hình thức tất cả các thuộc tính cốt lõi liên quan đến tính đúng đắn và an toàn của các hệ thống của chúng tôi. Thật tuyệt vời khi thấy các dự án khác chấp nhận xác minh hình thức như một công cụ quan trọng. Tôi tự hào rằng StarkWare cũng đã dẫn đường trong khía cạnh này. Đó là điều mà “blockchain tương lai” nghĩa với chúng tôi. Muốn tìm hiểu thêm? Dưới đây là bản tường thuật chi tiết về nỗ lực chứng minh Lean của chúng tôi trong vài năm qua