jonas_o

Nice! Seems however like there is no obvious approach to scale this proof to a machine with caches and multicycle memory accesses, where you can not flush the pipeline quite as conveniently.

You can get rid of metastability and high impendance in the proofs provided cycle time is large enough. Then you have cyclical binary logic. This is a classical result shown eg in "Computer Architecture" (Müller Paul)

I don't know anyone working on formal verification of quantum hardware, would be interesting if anyone does it.