You can’t formally verify behavior with subtle and specific hardware failures. Or in general interaction with reality. You can formally verify only internal logic.