Đặc tả kỹ thuật chính thức của Sổ cái Blockchain Cardano, được cơ chế hóa trong Agda
Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda.
Hệ thống Blockchain bao gồm phần mềm quan trọng xử lý các khoản tiền lớn, khiến chúng trở thành ứng viên tuyệt vời cho việc xác minh chính thức. Một trong những thành phần cốt lõi của Blockchain là sổ cái cơ bản thực hiện mọi công việc kế toán: theo dõi các giao dịch và tính hợp lệ của chúng, v.v. Thật không may, các nghiên cứu lý thuyết trước đây thường bị giới hạn trong thiết lập lý tưởng, trong khi các đặc tả kỹ thuật cho việc triển khai thực tế lại rất khan hiếm; hoặc hàm được triển khai trực tiếp mà không có đặc tả kỹ thuật phù hợp, hoặc tốt nhất là chỉ có đặc tả kỹ thuật không chính thức được viết trên lý thuyết. Công việc hiện tại mở rộng ra ngoài các nghiên cứu siêu lý thuyết trước đây về mô hình EUTxO để bao quát toàn bộ quy mô của Blockchain Cardano: đặc tả chính thức của các tác giả mô tả một hệ thống phân tầng các chuyển đổi mô đun bao gồm tất cả những điều phức tạp của một Blockchain thực tế, chẳng hạn như hợp đồng thông minh có khả năng biểu đạt đầy đủ và quản trị phi tập trung. Nó được cơ chế hóa trong một trợ lý chứng minh, do đó có tiêu chuẩn nghiêm ngặt hơn: kiểm tra kiểu ngăn ngừa những sơ suất nhỏ thường gặp trong các phương pháp tiếp cận không chính thức trước đây; các thuộc tính siêu lý thuyết quan trọng hiện có thể được chứng minh chính thức; nó là một đặc tả kỹ thuật có thể thực thi mà việc triển khai trong sản xuất đang được thử nghiệm để đảm bảo tuân thủ; và nó cung cấp nền tảng vững chắc cho việc xác minh hợp đồng thông minh. Ngoài mạng lưới an toàn giúp các tác giả kiểm soát, quá trình chính thức hóa còn cung cấp hướng dẫn cho thiết kế sổ cái: cái này cung cấp thông tin cho cái kia theo cách cộng sinh, đặc biệt là trong trường hợp các tính năng tiên tiến như quản trị phi tập trung, đây là một lĩnh vực nghiên cứu Blockchain mới nổi nhưng đòi hỏi một cách tiếp cận mang tính khám phá hơn. Tất cả các kết quả trình bày trong bài nghiên cứu này đã được cơ chế chế trong trợ lý chứng minh Agda và được công khai. Trên thực tế, tài liệu này tự nó là một tập lệnh Agda có trình độ và tất cả mã được kết xuất đã được kiểm tra kiểu thành công.