<p>achievement unlocked: synthesize an entire 16-bit CPU while performing logical equivalence checking (combinational and sequential) for every transformation the compiler does, thus proving it correct (modulo correctness of the SMT solver and the IR-to-SMT translation code)</p>