Quite interested as well. If only formal proof was the currently accepted verification methodology and there were tools, etc. around it, then maybe we would be spending a lot less effort in verification. Very tempted to buy but it's a bit pricey and there is probably still a lot of work required to verify a real design in the way the title suggests
I have the same doubts: a bit pricey, will it say something really useful, and therefore worth it, or will it just be an educational but sterile reading on a practical level?
Who knows ...

I designed and implemented a toy-ISA, which has nothing interesting except for the C-like compiler I wrote, as it facilitates the machine level.
Now I am adding multi-processing and I need a way to validate things better, or rather, to spend less time than I have used so far.
The implementation I made has been carried forward and tested rigorously for modules, so, specific test-bench-units for each ALU circuit, COP0, COP1, load/store, register file (which has particular properties), etc.
Finally, the system integration test-benches.
I need to spend less effort in verification, so probably a better verification methodology.