>>13362I'm not an expert but I've talked to a sel4 engineer in person.
In mathematics, there are formal proofs.
We can make a mathematical statement and show that our stated assumptions guarantee the result is true.
(further interesting stuff)
https://en.wikipedia.org/wiki/List_of_mathematical_proofsWe can also apply a similar concept to software algorithms. I haven't looked into the techniques myself so I can't explain them, but essentially you can provide a formal proof on an abstract mathematical model of the system. Provided that model is accurate, it formally verifies the program does the defined function, no exceptions. You have a guarantee that the code's implementation does what was specified. That's very good for important things like cryptographic code where correctness is important.
This doesn't mean it's 'unhackable' or infallable: what if the actual
design specification has issues? Then they're provably in the implementation! But it does remove a lot of potential issues and bugs since there aren't any implementation bugs. Implementation bugs are a HUGE source of software security vulnerabilities.
Here's an example of a microkernel that has (partial) formal verification:
https://en.wikipedia.org/wiki/L4_microkernel_family#High_assurance:_seL4>A formal proof of functional correctness was completed in 2009. The proof provides a guarantee that the kernel's implementation is correct against its specification, and implies that it is free of implementation bugs such as deadlocks, livelocks, buffer overflows, arithmetic exceptions or use of uninitialised variables. seL4 is claimed to be the first-ever general-purpose operating-system kernel that has been verified.So that shows some of the kind of issues verification can avoid, which would potentially lead to a crash/failure or a security weakness if they were in there.