This is the formal ledger specifications for the Cardano blockchain. It is written in Agda and is executable; Haskell code can be extracted and run for conformance testing.
The project consists entirely of literate Agda code from which the HTML documentation is generated. Thus the latest human-readable Cardano ledger specification is a collection of HTML files; these replace the PDF documents of previous eras.
The formal ledger GitHub repository contains formal ledger specifications for all eras, starting with Shelley, up to and including the Conway era. While the Agda formalization of the Conway era is complete, some pieces of the ledgers from previous eras have yet to be formalized. We hope to finish formalizing the outstanding pieces in the near future.
You can
-
read the HTML version of the Agda source code
-
interact with and/or contribute to the formal specification; instructions for building the artifacts, generating Haskell source code for conformance testing, or exploring the literate Agda files in a development environment are available in the Contributing Guide.
The table below provides links to the full formal ledger specification (as browsable HTML), as well as the legacy PDF artifacts.
| Artifact | Link | Description |
|---|---|---|
| Source Code | HTML | Interactive, hyperlinked version of the Agda source code |
| Formal Specification | HTML cardano-ledger.pdf† | Complete specification of the Cardano Ledger |
| Conway-Era PDF | conway-ledger.pdf† | Covers what's new in the Conway era |
† As we are migrating from a LaTeX-based to a Markdown-based documentation workflow, building PDFs from source is currently deprecated and unsupported. Please use the links above to access the pre-built PDF documents.
We welcome contributions and feedback!
For detailed instructions on setting up a development environment, running tests, and understanding the project structure, please see our Contributing Guide.
If you encounter any issues, please check the Troubleshooting Guide or submit a new issue in this repository.