This repository is used to collect various formal methods projects on Cardano. In the future it may also house a 'Cardano Node properties' library, which would combine the Consensus and Ledger specifications and prove combined properties about them that cannot be stated or proven about either of them alone.
| Project | Link |
|---|---|
| Consensus Specification | https://github.com/IntersectMBO/ouroboros-consensus/tree/main/docs/agda-spec |
| Ledger Specification | https://github.com/IntersectMBO/formal-ledger-specifications |
| Plutus Metatheory | https://github.com/IntersectMBO/plutus/tree/master/plutus-metatheory |
Beside the specifications in the above repository, there are older specification documents for the eras before Conway. They can be found here:
| Era | Design Documents | Formal Specification | CDDL |
|---|---|---|---|
| Byron | Chain Spec, Ledger Spec | CDDL, PDF | |
| Shelley | Design | Spec | CDDL |
| Allegra | Same as Mary era below | Same as Mary era below | CDDL |
| Mary | Multi-Currency, UTXOma | Spec | CDDL |
| Alonzo | eUTXO | Spec | CDDL |
| Babbage | batch-verification, CIP-31, CIP-32, CIP-33 | Spec | CDDL |
Other Documents:
- Non-integer calculations specification: details on the parts of the Shelley specification that use real numbers.
- Stake pool ranking specification: details for a robust stake pool ranking mechanism.
- Explanation of the small-step-semantics framework: a guide to the notation and style used by our ledger rules.
The metatheory linked above is an Agda specification of both the typed and untyped layers of the Plutus Core language, and includes a specification for the CEK machine which evaluates them.
Additionally, there is the "paper" specification document which definies the language elements, and has denotational semantics for each of the supported builtin operations.