Paul Karger who was an engineer that worked with him early on doing pentests that were quite embarrassing to military and commercial sector. Paul designed and built a number of highly-secure systems at a time when it was little understood. Here's his publication list and an obituary summarizing some of his work.
My favorite was VAX Security Kernel whose design is still stronger than most modern VMM's. It was also the project where the application of covert-channel analysis discovered cache-based, timing channels in processors. The high-assurance, security field started freaking out about how insecure CPU hardware was around that point. Both problems ignored by other groups in security much like results and advice from MULTICS evaluation. His last project was a secure, smartcard OS for IBM designed for EAL7 evaluation. He and/or his team wisely split it up into intermediate deliverables that had independent value and potential sales to keep the long-term project funded despite effects of management impatience or changes.
The public access machine at NSA, DOCKMASTER, ran Multics until 1998.
I haven't tried to use it or anything. Just posting it for others.