The proof claimed in the preset work covers only the microkernel part of a full OS. This is a similar level of complexity to the lower levels of THE, even to the point that virtual memory was excluded from both proofs. In the case of THE, the hardware did not support it. In the case of the present work, the authors of the web site listed virtual memory as specifically excluded from the proof.
 
(THE had a software segmentation scheme, assisted by the compiler.)

In the 1960's Edsger Dijkstra (arguably one the founding fathers of "Computer Science", at least as a university subject) led a group at Eindhoven to develop a multiprocessing OS called "THE". The kernal was formally proven BY HAND .

I daresay the folks who have made this recent excellent achievement are likely well aware of THE, and therefore are being specious in claiming to be the world's first at doing this.

I really hope that the marketing folks at that company know what they are doing, because I found the voice used in their web site and white papers really condescending. There seems to be an assumption that the reader is utterly surprised that formal proof techniques exist, and also there seems to be an assumption that the reader will be bored by meaninful details - like "take our word for it, because you'd fall asleep or wander away if we really tried to explain it".

Odd, because on the other hand, they seem to be trying to be up front about the boundaries of their proof. I just think it is possible to layer a presentation to different degrees of interest without comming off so jerky.

He keeps talking about projectors at 1200 lumens using incandescent lamps - but I'm pretty sure he means "xenon plasma arc" lamps.

I don't doubt collision is possible; but I also consider that the discrete nature of the computation (for simulation of a naturally continuous system) has such a significant chance of error that to talk about these tiny chances being predicted by the computation is rediculous - I doubt the predictions are informative.

I think origin (0,0,0) [(0,0,0,0,0)?] should be at the Sun upon the start date - since the earth orbits the Sun _and_ rotates, this could remove a couple curliques from the system - of course I know the sun orbits the galactic center and other things, I'm just saying it would simplify the system some when it comes to resolving positional issues to some fine resolution in the future.

I agree X-ray sources are better than MHz sources.