Yes, there is a formal spec for the Unprivileged RV32/64 IMAFDC and Privileged RISC-V ISAs.
The spec can be found at: https://github.com/riscv/sail-riscv
The spec is written in Sail, a language (DSL) for ISA formal
specifications from U.Cambridge, UK. Sail website: https://github.com/rems-project/sail
The RISC-V formal spec can be compiled into a simulator for RISC-V,
which can be used as a golden reference model. The executable is
capable of booting Linux in a few seconds.
A 2-year tour of the spec can be found at:
``A Tour of the RISC-V ISA Formal Specification'' https://github.com/rsnikhil/RISCV_ISA_Spec_Tour
R.S.Nikhil, RISC-V Summit 2019.
There was another talk on the subject at the RISC-V Summit a few weeks
ago, for which you may find links on the RISC-V Summit web site:
``High Level Sail Overview'', by Bill McSpadden, RISC-V Summit 2022.