I think we can do same for software, though. Just got to keep it simple, layered, and each layer building on one before it properly. I did it informally in a style that copied Wirth's Lilith work albeit special-purpose. Verisoft did quite a bit on full-stack for imperative. SAFE (crash-safe.org) is working on it for functional. I think a shortcut is to implement VLISP Scheme in hardware using hardware verification techniques along with previously verified I/O system. I've already seen LISP processors, VLISP for rigorous implementation, Shapiro made a security kernel, and the right hardware target can be reused for ML and Haskell code potentially. To counter hardware issues, run several in synch in same way as old Tandem NonStop architecture. Result should be flexible, fast enough for some workloads, enforce POLA, and have five 9's.
What you think of combining a verified LISP with hardware implementation as a time saver on goal to verification?
Note: Remember that, once we have that, building and verifying other toolchains is so much easier because we can work at high-level. Even highly-optimized systems such as yours could benefit from rigorously-verified systems maybe running same synthesis or checks overnight as a check against faster, possibly buggy implementations you use for iterations. Although, I mainly see them as a root-of-trust for other systems in network.