Where will the formal specification of the block header validity rules live?

The new AGDA spec is described (in the README) as the "Complete specification of the Cardano Ledger". This is reasonable as the conventional understanding of ledger rules is the rules for the content of the blocks.

However the original document "A Formal Specification of the Cardano Ledger" (and its various subsequent updates) contains a specification of the validity rules for the whole block chain, not just the block body content. This covers what is conventionally understood to be the validity rules for blocks following a particular consensus protocol (such as Praos, transitional Praos etc).

It's totally reasonable to refactor things to gain a clearer separation of consensus versus ledger, but in doing so we must not loose the formal specification of the validity rules for block headers and blocks overall. Having such a specification is obviously vital.

So the question is where will this live? Will it also be ported to AGDA?

In the meantime, it would probably be wise for the README to point out that this new spec _only_ covers the ledger and not consensus (therefore no block headers) and point to the "legacy" specifications for the consensus parts (which is the Shelley spec as amended by the Babbage spec -- where Transitional Praos was replaced by Praos).

Note that it's a bit awkward to call them legacy specifications if they contain the most up to date version of the block header rules, but this is ok in a transitional state, provided there's a plan for where the consensus rules will live.