Our goal is to formally prove the Preservation of Value property, as stated in Section 15.1 of the document [A Formal Specification of the Cardano Ledger (Deliverable SL-D5)](https://hydra.iohk.io/build/1329332/download/1/ledger-spec.pdf).