Verifiable Computer Question

Has anyone gone to the trouble of building up a completely verifiable computer. I.e. starting with a known system--decapped 6502 for instance--and progressing to a functional system that can be 100% verifiably free of unintended--or maliciously intended--added functionality? I thought of going with the transistor computer build up or with a simpler computer like my hand soldered 1802 computer, but I am wondering if there's a better place to start. I was looking at the forth on pga computers since we have an open source tool chain, but I have to wait for that stuff to arrive. For instance, https://github.com/sylefeb/Verilog-Playground/blob/master/j1eforth-verilog/j1eforth.v which has readable Verilog and makes a very simple forth stack computer.