Thanks for sharing, this is super cool! Right now my approach to correctness it to just run as many tests as possible and fix them (torchtpu greatly expands the amount of available tests), but formal verification is also super cool. Having a look at your book https://lean.brettkoonce.com/blueprint.pdf

The Tenstorrent ISA is documented btw https://github.com/tenstorrent/tt-isa-documentation, I wonder if one could do the verification end-to-end with the hardware.