Re: Even the 6502
"Yes it does guarantee the design is bug free."
No, it doesn't guarantee that, either. It guarantees that the design matches the formal specification, which just shifts the location of the bug.
If the formal specification says that a read issued from user-mode code to a supervisor-only page will send the read to the actual memory before validating the permissions (and furthermore use the returns of that in speculative execution that is discarded if the permissions fail), then the formal specification will validate a CPU that, nevertheless, has the Meltdown bug.