Formal and executable specifications for the new features to be introduced by Shelley.
The documents are built in our CI and can be readily accessed using the following links:
Shelley design specification: the primary design document for Cardano Shelley.
Shelley ledger formal specification: the formal mathematical specification of the Shelley era ledger rules.
Shelley binary format specification (CDDL): the binary formats for the Shelley ledger using CBOR CDDL schema notation.
Non-integer calculations specification: details on the parts of the Shelley specification that use real numbers.
Byron chain specification: the formal mathematical specification of the Byron era chain-level rules.
Byron ledger specification: the formal mathematical specification of the Byron era ledger rules.
Byron binary format specification (CDDL): the binary formats for the Byron ledger using CBOR CDDL schema notation.
Explanation of the small-step-semantics framework: a guide to the notation and style used by our ledger rules.
In addition, there is a formalization of the Ledger Specification in Isabelle/HOL which can be found here.
The artifacts in this repository can be built and tested using nix. This is additionally used by the Hydra CI to test building, including cross-compilation for other systems.