'The Y86 is a “toy” machine that is similar to the x86 but much simpler. It is a gentler introduction to assembly level programming than the x86. Just a few instructions as opposed
to hundreds for the x86. Fewer addressing modes. Simpler system state. Absolute addressing.'
If/when many qubits circuits can be fabricated, that also sounds like a mucho fun challenge for formal verification. It's an educated guess that people are already working/worked on it because the math usually precedes the hardware.
Internal multi-driver buses where you need Z states are such a pain that they're avoided wherever possible.
Of course, this means that you're still vulnerable to "outside context" attacks if they're outside the proof scope, such as fault injection over the power supply lines.
I don't know anyone working on formal verification of quantum hardware, would be interesting if anyone does it.