If you can't directly check from a provable formal system then it doesn't really help with validation and you have to jump through a lot of hoops to get there (like OP did).
So if you are going to write a specification, you really want to get maximum bang per buck out of the effort. Which means that it has to be good for many purposes:
- documentation - verifying processors - dynamic verification (i.e., testing) - formal verification - testing test suites - verifying application software - dynamic and formal verification - verifying OSes, RTOSes, microkernels and other bare-metal software - verifying compilers - generating machine readable descriptions
Verilog is great for one of these - but less good for all the others. Starting with a relatively neutral language gives you a lot more flexibility. It makes any individual task a bit harder than if that was your only goal but you save effort overall.
There is also the virtuous cycle that bug fixes and improvements that help any one goal are folded into the master copy - so all other sub-projects benefit.