The formal ledger specification has gone through a series of improvements since it was first used as a base for our formal block header specification, e.g. a reorganization of the directory structure, the removal of the local copy of the set theory library in favor of the use of agda-sets, etc. We shall replicate these changes in our formal block header specification.