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

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.