Plus Frama-C, model-checkers, concurrency analyzer, CompCert in Coq, Simpl in HOL, symbolic execution in KLEE, path-based testing, and property-based... then it might be good to go.
On a capability-secure processor running in a VM in case new classes of attack against C code are discovered
Again. ;)
On a capability-secure processor running in a VM in case new classes of attack against C code are discovered Again. ;)