I seem to remember a CPU that was stack-based that was built for correctness. I think it was called the Viper, but I cannot seem to find it. It would be logical to me to run your formally trusted compiler on a chip designed the same way.
The original goal of the project was to have a verified computer stack, with proofs going from the software, compiler and processor all the way down to the gate level.
I am not sure how far they got, but I don't think the project is still active, which is a bit sad.