Regarding "formally verified," I believe the "formal" refers to the formal in formal methods, but I agree that it can be weaselly.
In the case of seL4, however, I don't think it is because they are incredibly precise about defining their assumptions. They have verified the machine code for various architectures, subject to those assumptions.
Regarding "formally verified," I believe the "formal" refers to the formal in formal methods, but I agree that it can be weaselly.
In the case of seL4, however, I don't think it is because they are incredibly precise about defining their assumptions. They have verified the machine code for various architectures, subject to those assumptions.