As digital designs become increasingly complex, it is essential to have reliable and automated safety verification techniques. To mitigate the negative impact of faults on design behavior, various hardening techniques are employed. This paper presents a fully automated formal-based fault injection technique for processor designs that can functionally verify safety-critical designs in the presence of faults. The experiments conducted demonstrate that multiple bugs can be detected in different hardening mechanisms without extra effort. Moreover, the proposed technique provides high-confidence fault propagation analysis. The study includes numerous experiments conducted on various processor components of two different RISC-V ISA variants. The experiments achieved better results than simulation-based approaches and at the same time yielded similar results to techniques based on Automated Test Pattern Generation (ATPG) fault propagation analysis.