Nền tảng hợp đồng thông minh của Cardano được tạo ra bởi thiết kế Cardano Computation Layer (CCL), họ tập trung chủ yếu vào việc đảm bảo rằng hợp đồng thông minh hoạt động tốt như trong thiết kế mà không bị các lỗ hổng bảo mật tiềm tàng nào. CCL bao gồm hai lớp: một lớp máy ảo và framework cho ngôn ngữ lập trình và lớp các ngôn ngữ lập trình được chỉ định chính thức. Tầng thấp nhất trong kiến trúc Cardano được gọi là IELE, cung cấp một máy ảo với thiết kế nhằm làm cho các công cụ xác minh định dạng xây dựng trở nên dễ dàng và một framework cho ngôn ngữ phổ quát để dịch các hợp đồng thông minh từ các ngôn ngữ cấp cao sang các chỉ lệnh. Quỹ nghiên cứu và phát triển IELE được tài trợ bởi IOHK và được dẫn dắt bởi Giáo sư UIUC: Grigore Rosu. Rosu và đội ngũ của mình đang áp dụng những kinh nghiệm sâu sắc từ nghiên cứu của họ về KEVM, một ngữ nghĩa chính thức trong K Framework cho máy ảo Ethereum, và KLLVM, một ngữ nghĩa chính thức trong K cho LLVM, để xây dựng một máy ảo an toàn hơn và hiệu quả hơn. Không giống như EVM là một máy ảo dựa trên ngăn xếp, IELE sẽ là một máy ảo dựa trên trình đăng ký, như LLVM. IELE sẽ có một số lượng không giới hạn các bộ đăng ký và cũng sẽ hỗ trợ bộ số nguyên không giới hạn. Với thiết kế tránh sử dụng một ngăn xếp có giới hạn và không phải lo lắng về ngăn xếp hoặc tràn số học sẽ làm cho đặc điểm kỹ thuật và xác minh hợp đồng thông minh dễ dàng hơn đáng kể. Giống như Ethereum, IELE sẽ sử dụng GAS để hạn chế sử dụng tài nguyên và ngăn chặn các cuộc tấn công DoS. Điều này cũng hàm chứa một số thách thức đối với việc xác minh chính thức mà nhóm nghiên cứu coi là "khó khăn nhưng có thể quản lý được". IELE thúc đẩy K Framework để đơn giản hóa việc phát triển các công cụ tự động xác minh hợp đồng thông minh phù hợp với các thông số kỹ thuật. Điều này cho phép IELE hỗ trợ các hợp đồng thông minh được viết bằng bất kỳ ngôn ngữ lập trình nào có ngữ nghĩa chính thức trong K. Ngôn ngữ Simon là một ví dụ. Theo như mô tả ngắn gọn trong bài báo về tầm nhìn của Cardano: Simon là một ngôn ngữ giao dịch có tính liên kết cao và có phân vùng cụ thể nhờ đó nó sẽ cung cấp một tập hợp các nguyên tắc giao dịch tài chính cơ bản được xác định chính xác và có thể kết hợp để tạo ra các hợp đồng phức tạp hơn với các tài sản có thể kiểm chứng được. Simon Peyton Jones là một trong những nhà thiết kế chính của Haskell, một ngôn ngữ đánh máy tĩnh, thường được sử dụng trong các ứng dụng ở các mỗi trường mà lỗi theo thời gian thực sẽ có chi phí cao (được sử dụng để triển khai Ouroboros). Thiết kế của Haskell làm cho nó thích nghi với các công cụ xác minh tự động và loại bỏ các khiếm khuyết trong quá trình phát triển phần mềm. Một nhà thiết kế khác của Haskell và ACM Fellow, Phil Wadler, là một cố vấn ngôn ngữ lập trình cho IOHK, vì vậy không có gì ngạc nhiên khi ngôn ngữ hợp đồng thông minh bậc cao của Cardano, Plutus, kết hợp rất nhiều khái niệm bên cạnh Haskell. Plutus là một ngôn ngữ đánh máy tĩnh, có chức năng giống như Haskell. Giống như Haskell, Plutus biên dịch ra một ngôn ngữ đơn giản hơn, Plutus Core, làm cho việc xác minh chính thức trở nên dễ dàng hơn. Các công cụ xác minh chính thức có thể giúp các nhà phát triển giải thích hợp đồng và chứng minh một số tính năng nhất định về hành vi của hợp đồng thông minh. Những bằng chứng này có thể là một công cụ mạnh để làm nổi bật và loại bỏ các lỗ hổng tiềm tàng của các lỗ hổng trong hợp đồng thông minh như xử lý các lỗi đầu vào không hợp lệ, lỗi về kiểu khác nhau của các tham số, các đường dẫn không rõ ràng, sự nhầm lẫn về phạm vi, lỗi đánh máy, tràn bộ nhớ, vv . Cardano cũng đang có kế hoạch hỗ trợ các ngôn ngữ cấp cao khác, bao gồm cả Solidity. Để Ethereum vẫn là nền tảng hợp đồng thông minh uy lực nhất thì nó cần phải thích ứng, bằng cách nâng cấp ngôn ngữ hợp đồng thông minh và chuỗi công cụ trước khi có một giải pháp thay thế tốt hơn. Cộng đồng Ethereum đang phát triển các ngôn ngữ lập trình mới như Bamboo và Viper, phù hợp hơn cho việc xác minh chính thức và hạn chế các lỗ hổng có thể được phát hiện bởi trình biên dịch chứ không phải là do tin tặc. Các ngôn ngữ này biên dịch sang mã EVM, vì vậy cần phải xác minh chính thức cả mã cao cấp lẫn mã byte code của EVM. Hiện tại có nhiều dự án trong cộng đồng Ethereum thẩm tra việc xác minh chính thức các hợp đồng thông minh và máy ảo Ethereum. Ethereum đang trong một cuộc chạy đua để loại trừ sự xuất hiện thường xuyên của các lỗi khai thác thông tin của hợp đồng Solidity trước khi một nền tảng cạnh tranh khác có thể kịp thời vượt qua.