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.
Byron
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
Shelley
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
Goguen
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:
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
Basho
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:
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
Voltaire
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
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