For formal proof purposes the system is usually treated as purely digital, and you rely on the lower level designers handling all the tedious initialisation and metastability issues. Generally you have a global reset signal to put everything into a known state, and a proof that anything that isn't known isn't read before it's written.

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.