Yes, the seL4 specification comes with proofs of strong integrity and information flow security guarantees, and with integrity and authority confinement proofs. It also comes with a configuration that is proved to be a static separation kernel.
The implementation, including the code emitted by gcc, implements this specification, and is guaranteed to be free of buffer overflows, pointer errors, memory leaks, arithmetic overflows, and undefined behavior.
The right next sentence is, "And by now it has proofs about further security properties (which show that the specification has the right properties)".
In particular, they formalized notions of confidentiality, integrity, and availability, and proved the specification (hence the source code, hence the binary) satisfies these notions.
Now you can ask whether these notions were formalized correctly. But that's still a LOT better than asking it for binary/source/specification.
> has the specification been proved to be bug-free?
Yes for SeL4, but no for a bunch of other systems advertised as "having been proven to be correct". Which often sadly only means "implemented as specified" but not "implemented as specified and proven to have the right properties".
Perhaps you are a brain in a vat being deceived into thinking that the specification exists. Perhaps any memories you have of reading the specification are false and implanted. Perhaps this very comment doesn't actually exist, you are merely hallucinating the memory of having read it.
Nothing can be known with absolute certainty. But a specification is much smaller than an implementation and misunderstandings of specifications are much less common than bugs in code. Don't let perfect be the enemy of good.
More importantly, a good specification is one that is triple-checked: by inspection by a human, having the program to conform to it, and by having to satisfy a bunch of nontrivial theorems about the spec that a human would expect from programs conforming to the spec. Sel4's integrity, confidentiality, and worst-case-execution-bounds proofs are an example of this... it's quite unlikely for a program to simultaneously provably satisfy a specification, the specification to provably satisfy nontrivial (first order) properties, and for those properties to nonetheless be defined incorrectly. Obviously there can still be holes in your model (for example, not considering certain side channels), but that's a pretty different situation from accidentally proving a different thing than you thought you were.
Philosophy of that sort offers little insight into correctness in formal software development, just as it offers little insight into the study of mathematics.
In practice, bugs can creep in at various stages of a formal development process, but they're much less common that with non-formal software development methodologies, as you say.
> Philosophy of that sort offers little insight into correctness in formal software development, just as it offers little insight into the study of mathematics.
I disagree. Knowing the limits of what is possible is important, so that we don't waste our time looking for the impossible.
Such a limit would be worth knowing about. But I see no reason to assume that limit exists in the absence of evidence, particularly as our tools and reasoning are improving all the time.
We can be pretty sure there is a limit. We're physical creatures in a (roughly) deterministic world, so ultimately we're bound by Rice's theorem just as computers are.
Can the human brain in principle be simulated by a (deterministic) algorithm? Seems to me the answer is obviously yes, as we are 'merely' extremely complex machines whose operation is governed by deterministic physical laws. If you agree, you are forced to agree that we are bound by Rice's theorem.
Whether it's ever likely to be a practical problem, is another matter.
edit: We already know there are mathematically interesting numbers so enormous they cannot be represented in our universe, let alone computed by humans or our machines. That's not really the kind of practical limit we're interested in, but it still shows a limit of a sort. TREE(3) for instance.
My perspective on results like Rice's theorem is that they tell us that the Turing machine formalism can express incomprehensible programs. I don't see that as a convincing argument that there are important or useful programs that we cannot comprehend; rather I see it as a demonstration the Turing machine model is broad, and an argument that we should look for stricter models that still admit all the programs we care about (probably based on some form of typed lambda calculus).
> My perspective on results like Rice's theorem is that they tell us that the Turing machine formalism can express incomprehensible programs.
I'm afraid I don't know what you're saying here.
> I don't see that as a convincing argument that there are important or useful programs that we cannot comprehend
I don't see that there's any way to contest it. The only way to deny that we are bound by Rice's theorem, is to deny that the human mind is algorithmic. This presumably requires the denial of determinism, which is fairly absurd.
If you're not following my argument, I'd be happy to rephrase it.
> an argument that we should look for stricter models that still admit all the programs we care about (probably based on some form of typed lambda calculus).
That offers no escape. We're still bound by Rice's theorem. Perhaps it will never be a practical issue, but the fact remains.
> If you're not following my argument, I'd be happy to rephrase it.
I'm not following what it is that you think Rice's theorem tells us.
Rice's theorem says that nontrivial properties of Turing machine programs are undecidable, i.e. for a given property, there will be Turing-machine programs for which we can't tell whether they have that property or not.
That doesn't tell us anything about what is possible for programs, or put any limits on programs that we do understand. It just says that in the Turing machine model there must exist programs that we don't understand. Fine. Who cares?
But, but, but ... has the specification been proved to be bug-free?
As in does the specification meet eg a set of security constraints?