That doesn't matter. I mean, you might be able to prove some properties in this way just as you could in others, but it is not a "solution" by any means -- it might work in some cases for some properties with some barely acceptable scalability, and that's about it. The reason is that the cost of reasoning about n components is not even a computable function of n (the cost grows in the same way if you were trying to prove the property on a monolith). See the blog post I linked to for a result that proved this, and an example of a case where two components are easily analyzed yet their composition isn't.
The main direction in formal methods research to increase scalability in a viable way is to reduce soundness.
AFAIU Component-Based Software Engineering has been a bedrock principle of applied formal verification for decades. It's a process approach. If a functional problem is sufficiently complex it's necessary, if not always sufficient, as a practical matter to use a component architecture. And even if it's not sufficient, a solution where some components are formally verified is better than where none are. Circumscribing soundness isn't an alternative, it's complementary.
You're right, it's not by itself a "solution" in the sense of completely resolving the problem; it's a "solution" in the other meaning of that word--a means of dealing with a problem.
Yes, and still the only software verified using such techniques has been tiny (< 10KLOC) and required extraordinary simplification and tremendous effort by specialists. It's like saying that particle accelerators have been a bedrock principle of turning lead into gold. It "works" but not in any sense that makes it a repeatable, affordable practice. Moreover, the gap between the size of programs verifiable in this way and the size of a "normal" piece of business software has stayed pretty much constant over the past four decades -- 3 orders of magnitude.
> And even if it's not sufficient, a solution where some components are formally verified is better than where none are.
Better in what sense? Is it better to soundly verify one component or to use unsound methods on an entire system (even assuming similar costs, but often the latter is cheaper). Soundness is costly and is never a real requirement as a software system is a physical system, anyway; machines only perform machine instructions according to spec with some probability, and probability is all engineers can ever hope for. But sure, sometimes there are small components that are easy enough to verify with deductive proofs, making it the most affordable path to high confidence, although I'd say that's the rare exception rather than the rule.
> Circumscribing soundness isn't an alternative, it's complementary.
It allows you to use automated methods that don't require careful modularity.
Exactly. And the solution is architectural modularization--implementing a solution as multiple components that can each be independently verified and then integrated in a verifiable manner. Microkernels are uniquely amenable to such an approach, regardless of language.
Which I think is the major reason why memory allocation in seL4, including memory for in-kernel runtime objects, is handled in user space, otherwise its tentacles would make kernel verification intractable. And it's not just that allocation is handled by a single user space daemon; it bleeds into the entire architecture. AFAIU, any request you make of the kernel must be accompanied by the necessary memory needed to satisfy the request. This also fits nicely into the capability model.