Impressive if for no other reason than there are various disparate formally verified projects (seL4, compcert, certikos) that could potentially be unified under a single proof system. Additionally it may be possible to quickly extend existing proofs (e.g. seL4's proofs) to other architectures.