Hợp đồng có cấu trúc trong mô hình sổ cái EUTxO
Structured Contracts in the EUTxO Ledger Model.
Sổ cái Blockchain dựa trên mô hình UTxO mở rộng hỗ trợ các hợp đồng thông minh có khả năng biểu đạt đầy đủ để xác định quyền thực hiện một số hành động nhất định, chẳng hạn như chi tiêu đầu ra giao dịch hoặc đúc tài sản. Đã có một số nỗ lực chuẩn hóa việc triển khai các chương trình có trạng thái bằng cơ sở hạ tầng này, với các mức độ thành công khác nhau. Để khắc phục điều này, các tác giả giới thiệu khung hợp đồng có cấu trúc để chính thức hóa ý nghĩa của việc triển khai đúng chương trình có trạng thái trên sổ cái. Sử dụng ngữ nghĩa từng bước nhỏ, cách tiếp cận của các tác giả liên hệ các chuyển đổi sổ cái cấp thấp với các chuyển đổi cấp cao của hợp đồng thông minh đang được xác định, do đó cho phép người dùng chứng minh đặc tả kỹ thuật trừu tượng của họ được hiện thực hóa đầy đủ trên Blockchain. Các tác giả lập luận rằng khung đủ linh hoạt để bao gồm nhiều ví dụ, đặc biệt là chứng minh tính tương đương của nhiều triển khai cụ thể của cùng một đặc tả kỹ thuật trừu tượng. Dựa trên các kết quả siêu lý thuyết trước đây, kết quả của các tác giả đã được cơ chế hóa trong trợ lý chứng minh Agda, mở đường cho việc xác minh nghiêm ngặt các hợp đồng thông minh.