[nextos]

I agree. The formalization is very impressive even if we consider it was done on a result that is already accepted as true and got a lot of help from humans to scaffold and build the structure.