This paper presents an overview and status of a cyber fault tolerant system that uses a low overhead multi-variant execution environment and precise static binary analysis and efficient rewriting technology to produce structured variants which allow automated verification techniques to prove security properties of the system.