Qubes Formal Verification

General Discussion
1

Will Qubes ever have its code formally verified?

2

If OCaml can be converted into coq-of-ocaml, then we can do formal proofs on OCaml programs, which

means we can do formal proofs on MirageOS unikernels.

3