New Shelley formal specifications complete

The goal of the Cardano Shelley era is to bring full decentralization to Cardano, moving beyond the federated epoch and handing control of the ledger over to the community via stake pools.  As part of the process of delivering Shelley, we create formal specifications which allow us to verify that the final code is in line with what the researchers initially envisaged in their publications. By creating implementation-independent specifications, we can build components of the system using different languages, confident that they will work together.

We are pleased to announce that we have successfully reached an important milestone in the Shelley journey, with the key specifications now completed. The finished specifications are as follows:

To provide a smooth transition from the Byron era to the Shelley era, the Shelley code will have to be compatible with the Byron rules. To enable this, we have created specifications for the Byron era as well:

The process of implementing these specifications in production code is well underway, and the specifications will continue to improve with feedback from the mathematics, research, and development communities.

For the most up to date version of the specifications, check the Formal Models for Ledger Rules GitHub repository.

Artwork,

Mike Beeple