Alleged "microkernel mathematically proven to be bug free"

[Georgi Guninski]

> I have a rough outline for a "cloud computing grid" that verifiably:

verifiably? _really_ provable stuff is a very scarce resource IMHO
(especially in crypto. do you need crypto? Do you need P \ne NP?).

> But it absolutely requires a verified microkernel. I'm *very *excited to
> see that we're making progress towards it.

Is it really a progress?
There are assumption free proofs of False
in most formal proof systems.

Design flaws like \lor instead of \land
pass the verification process and later are
considered design flaws, not bugs in proof IMHO.

Knuth quote:
"Beware of bugs in the above code; I have only proved 
it correct, not tried it."