# shelley-ledger-specs¶

`shelley-ledger-specs`

Overview¶

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.

### nix-build Infrastructure¶

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.