I wouldn't expect additional security from introducing an entirely new OS/kernel. Just unknown RCEs and other vulnerabilities waiting to be discovered.
Just like Linux so no change there, We still need to move on.
Because they use formal methods preventing this kind of thing from happening?
Even with your formal methods strawman, vulnerabilities like these are still possible in Linux and C. We need to move on.
You can formally verify C code against a spec though.