Sounds like the same sort of idea that was behind the UK government RSRE VIPER secure microprocessor in the 1980s. IIRC there was eventually some doubt about the formal definition proof.
"IIRC there was eventually some doubt about the formal definition proof" (for VIPER)
I think the big issue was they could not verify the layout tools that mapped the logic design to the actual chip. So the logic design was verified but how could you know what was on the chip? Probably the same but might be (or might not be if a logic change triggered a latent bug in the layout SW).
Also the thing was dog rough on speed with a 26Mhz clock to deliver 1MIPS (which didn't sound very impressive). I think it was implemented as a state machine on a Ferranti gate array but the ARM was around that time and mapped the logic to PLA's on chip, which with registers will give a viable state machine as well.
It's tough to find stuff on VIPER. It looks like RSRE quietly buried it. Vaguely 6502 like? Their work on reliable Ada lead to the work on SPADE and the founding of Praxis systems
Left Hand / Right Hand
So on one hand DARPA wants everything to be extra-secure with no holes, and on the other hand there's the NSA...
DARPA has been funding this sort of work for years
The DARPA CRASH-SAFE project (http://www.crash-safe.org/) delivered a lot of encouraging results during its run (2010-2015).
Many of the ideas developed as part of the CRASH-SAFE project have been picked up by the "Dover" project (http://www.draper.com/solution/inherently-secure-processor), and plans to include them in a RISC-V processor design: https://riscv.org/wp-content/uploads/2016/01/Wed1430-dover_riscv_jan2016_v3.pdf