The end goal of this work is to prove that our validation rules for transactions, inputs, outputs and unlock blocks are enough to keep the UTxO ledger in a "valid" state. Goal: the ledger stays "valid" as long as the validations rules are enforced Steps: Define a formal model of IOTA ledger solely based on the RFCs allows us to detect any issue or unclear content that may appear in the RFCs