The RISC-V instruction set architecture has gained significant attention in recent years due to its open-source nature and potential to revolutionize the processor industry. RISC-V is designed to be simple, modular, and extensible, allowing for flexibility in implementation and customization for specific applications. However, the verification of RISC-V processors remains a critical challenge due to the complexity of the ISA and the need for rigorous testing to ensure correctness and reliability. Formal verification is a promising approach to address the challenge of RISC-V cores verification, as it provides rigorous mathematical proof of correctness that can guarantee the absence of bugs and errors in the design. Within the many initiatives of the RISC-V ecosystem, the RISC-V Formal framework by YosysHQ allows to apply formal verification to a RISC-V core. In this work formal verification was applied to the STRiVe2.4 core designed by STMicroelectronics, exploiting the RISC-V Formal framework. The implementation of the RISC-V Formal Interface (RVFI) was followed by the integration in the verification flow, using JasperGold to apply the formal checks to the core. The results obtained in this work demonstrate the potential of formal verification in bug hunting and trace the path for several possible developments.