Skip to main content

Relevant research papers and specifications

Cardano is a third-generation blockchain platform that aims to provide the community with more advanced features than any protocol yet developed. As a proof-of-stake blockchain, it is built with the rigor of high-assurance formal development methods and aims to achieve the scalability, interoperability, and sustainability needed for real-world applications. Cardano is the first platform to evolve out of scientific philosophy based on discovery, peer review, and cryptographic research.

Building a strong foundation in the blockchain industry, Cardano has an ethos of openness and transparency. All the research and technical specifications that underpin Cardano are publicly published and available to the community.

Cardano’s development roadmap is divided into 5 eras that focus on the foundation, decentralization, smart-contract and multi-asset ledger deployment, scalability, and governance of a pioneering blockchain environment. Relevant research papers and specifications according to the Cardano development roadmap are outlined below.


A period dedicated to building a foundational federated network that enabled the purchase and sale of ada. The network ran the proof-of-stake Ouroboros consensus protocol.

Relevant research papers:

Ouroboros: A Provably Secure Proof-of-Stake Blockchain Protocol

Ouroboros-BFT: A Simple Byzantine Fault Tolerant Consensus Protocol

Relevant specifications:

A Formal Specification of the Cardano Ledger

Specification of the Blockchain Layer

Formal Specification for a Cardano Wallet

Small Step Semantics for Cardano


A period of growth and development for the network focused on ensuring greater decentralization, which will lead to enhanced security and a more robust environment once the majority of nodes are run by network participants.

Relevant research papers:

Ouroboros Praos: An adaptively-secure, semi-synchronous proof-of-stake blockchain

Ouroboros Genesis: Composable Proof-of-Stake Blockchains with Dynamic Availability

Stake-Bleeding Attacks on Proof-of-Stake Blockchains

Reward Sharing Schemes for Stake Pools

Account Management in Proof of Stake Ledgers

Flexible Formality: Practical Experience with Agile Formal Methods

Coalition-Safe Equilibria with Virtual Payoffs

Efficient Random Beacons with Adaptive Security for Ungrindable Blockchains

SecureCyclon: Dependable Peer Sampling

Practical Settlement Bounds for Longest-Chain Consensus

Blockchain Participation Games

Consensus Redux: Distributed Ledgers in the Face of Adversarial Supremacy

Relevant specifications:

Engineering Design Specification for Delegation and Incentives in Cardano–Shelley

A Specification of the Non-Integral Calculations in the Shelley Ledger


The Goguen era will introduce smart-contract functionality to build decentralized applications while supporting multi-functional assets, fungible, and non-fungible token standards.

Relevant research papers:

The Extended UTXO Model

UTXOma: UTXO with Multi-Asset Support

Native Custom Tokens in the Extended UTXO Model

Functional Blockchain Contracts

Scripting Smart Contracts for Distributed Ledger Technology

Marlowe: financial contracts on blockchain

Marlowe: implementing and analysing financial contracts on blockchain

Unraveling recursion: compiling an IR with recursion to System F

System F in Agda, for fun and profit

Translation Certification for Smart Contracts

Message-passing in the Extended UTxO Ledger Model

Structured Contracts in the EUTxO Ledger Model

Relevant specifications:

A Formal Specification of the Cardano Ledger with a Native Multi-Asset Implementation

A Formal Specification of the Cardano Ledger integrating Plutus Core


An era of optimization, improving the scalability and interoperability of the network. Enhancing the network performance, Basho will introduce sidechains, new blockchains, interoperable with the main Cardano chain, with immense potential to extend the network’s capabilities.

Relevant research papers:

Proof-of-Stake Sidechains

Hydra: Fast Isomorphic State Channels

Interhead Hydra: Two Heads are Better than One

Mithril: Stake-based Threshold Multisignatures

Babel Fees via Limited Liabilities

Djed: A Formally Verified Crypto-Backed Pegged Algorithmic Stablecoin

State Machines across Isomorphic Layer 2 Ledgers

Tiered Mechanisms for Blockchain Transaction Fees

Approximate Lower Bound Arguments

Relevant specifications:

Formal Specification of the Cardano Ledger for the Babbage era


A development era enabling the Cardano network to become a self-sustaining system. Voltaire will introduce a voting and treasury system that will enable network participants to use their stake and voting rights to influence the future development of the blockchain.

Relevant research papers:

A Treasury System for Cryptocurrencies: Enabling Better Collaborative Intelligence

Updatable Blockchains

SoK: Blockchain Governance

Fait Accompli Committee Selection: Improving the Size-Security Tradeoff of Stake-Based Committees

Relevant specifications:

CIP-1694: An On-Chain Decentralized Governance Mechanism for Voltaire

Formal specification is a work in progress

Formal specification of the Cardano blockchain ledger, mechanized in Agda