End-to-End Formal Verification of a RISC-V Processor Extended with Capability Pointers To run the proof script, simply modify the first line of spec_setup.tcl to cd to the path of the cloned repository. All the RTL is included already.