I've been working on a declarative, executable spec for Bitcoin consensus rules. Here's my paper write-up:

Hornet Node and the Hornet DSL: A minimal, executable specification for Bitcoin consensus.

hornetnode.org/paper.html

Feedback is welcome.