Several vulnerabilities have been discovered in the Linux kernel. As a reminder: millions of lines of code run in supervisor mode. This is what Linux is. It is not possible to fix all the bugs. This is simply not doable. The solution has to be fundamental. The microkernel multiserver system architecture, with a formally verified microkernel. Nothing else can guarantee enforcement of anything. In practice, this is the same as saying seL4, because there are no alternatives. Related: the seL4 summit 2026 vids are finally up. We need to switchover to microkernel operating systems ASAP or our entire computing infrastructure becomes a liability. There are good reasons for QNX becoming viable again in the automotive world. Linux / Android has so
The pattern revealed here is not a quirk of a particular operating system. It is a structural condition that appears whenever a body of code, rules, or mechanisms that must be trusted to enforce safety grows beyond the capacity of any human or automated process to exhaustively check it. When that happens, defects inevitably slip through, and the system becomes vulnerable to exploitation that cannot be patched by local fixes. The only robust response is to shrink the trusted portion to a size that can be verified with mathematical certainty and to relocate all other functionality to components that operate without privileged authority.
In the Linux case the trusted portion is the kernel monolith. Developers add device drivers, file‑system support, networking stacks, and security modules, each increasing the lines of code that run with full hardware access. The sheer volume makes exhaustive testing or formal proof infeasible; consequently, attackers find overlooked edge cases — buffer overruns, race conditions, incorrect permission checks — and turn them into privilege‑escalation exploits. The community reacts with patches, but each patch adds more code, further enlarging the unverified base and creating a feedback loop where the attack surface expands faster than the repair rate. The proposal to move to a microkernel with a formally verified core seL4 follows the logical conclusion: keep only the minimal set of operations that must run in supervisor mode — thread scheduling, inter‑process communication, memory protection — and prove those operations correct. Everything else, from drivers to file systems, runs in unprivileged servers where a failure cannot compromise the whole machine.
The same mechanism shows up in finance. Before 2008, banks bundled home mortgages into increasingly opaque securities — collateralized debt obligations, synthetic CDOs, and related derivatives. Rating agencies and regulators treated these instruments as trustworthy assets because the underlying cash flows appeared sound. Yet the models used to price them relied on assumptions about housing price correlation and borrower behavior that could not be validated against the actual, rapidly changing loan pools. As the volume of these products grew, the set of assumptions that needed to be trusted expanded beyond what any analyst could examine in detail. Defects in the assumptions — such as the failure to account for declining lending standards or geographic concentration — were not discovered until defaults began to cascade. The crisis was not solved by patching individual securities; it required a redesign of the trust framework: increasing capital requirements, moving standardized derivatives to central clearinghouses, and mandating greater transparency so that the trusted base of risk models could be kept small enough to stress‑test rigorously.
In aviation, the Boeing 737 MAX provides a parallel. To accommodate larger, more fuel‑efficient engines, Boeing added the Maneuvering Characteristics Augmentation System (MCAS), a flight‑control law that automatically adjusts the horizontal stabilizer when it detects a high angle‑of‑attack. MCAS relied on a single angle‑of‑attack sensor and lacked cross‑checks with other flight‑deck indications. The software was relatively small, but its activation logic was embedded in a larger flight‑control monolith that pilots could not easily inspect or override without navigating complex procedures. Because the trusted portion of the flight‑control software — the code that could move control surfaces without direct pilot confirmation — was not formally verified and its failure modes were not exhaustively explored, a faulty sensor reading could trigger repeated nose‑down commands that overwhelmed the crew. The accidents were not remedied by tweaking the sensor alone; the fix involved reducing the trusted authority of MCAS (limiting its authority, requiring sensor disagreement, and making the system more transparent to pilots) and adding procedural safeguards, effectively shrinking the privileged control code to a level that could be subjected to rigorous analysis.
Legal systems exhibit a comparable dynamic. The United States Internal Revenue Code has grown over decades through accretions of exemptions, credits, and special‑purpose provisions. Each addition creates a new region of the tax landscape that professionals must understand to advise clients accurately. As the code expands, the likelihood increases that some interaction of provisions yields an unintended tax advantage — a loophole — that is not obvious from reading any single section. Because the total body of law cannot be mentally held in its entirety, tax planners can exploit these interactions to reduce liability, and the IRS must devote substantial resources to detect and litigate abusive schemes. The historical response has periodically been to attempt simplification: the Tax Reform Act of 1986 stripped away many deductions and lowered rates precisely to shrink the trusted base of provisions that needed to be monitored for abuse. While the code has since grown again, each reform effort reflects the same insight — when the trusted regulatory corpus exceeds what can be verified, non‑compliance becomes systematic, and the remedy is to curtail the corpus to a size that can be audited comprehensively.
Even biology offers an illustration. The vertebrate adaptive immune system generates a vast repertoire of antigen receptors through random recombination. To prevent autoimmune attack, the body enforces central tolerance: developing lymphocytes that strongly recognize self‑antigens are deleted or diverted into regulatory lineages. This tolerance mechanism relies on a relatively small set of stromal cells and signaling molecules that present self‑peptides in the thymus. If the receptor repertoire expands faster than the tolerance mechanisms can cope — as can happen in certain genetic backgrounds or under chronic inflammation — self‑reactive clones escape deletion, leading to autoimmune disease. The effective “trusted base” here is the set of tolerance mechanisms; when it is overwhelmed relative to the potential threat space, the system fails. Therapeutic approaches that aim to restore tolerance (e.g., administering antigen‑specific regulatory cells or enhancing thymic output) operate by strengthening the verified core rather than trying to eliminate every possible self‑reactive clone individually.
Across these domains the causal chain is identical: actors produce or maintain a trusted component (kernel code, financial models, flight‑control law, tax statutes, immune tolerance mechanisms) because it is necessary for the system to function correctly. As pressure to add features, accommodate market innovations, satisfy regulatory complexity, or respond to evolutionary demands increases, the trusted component grows. Verification resources — whether human auditors, model‑checking tools, pilot checklists, legal reviewers, or biological selection pressures — scale sub‑linearly with that growth. Consequently, the probability that an unverified defect exists rises, and when a defect is encountered it can be exploited to produce system‑level harm (privilege escalation, financial loss, loss of control, tax avoidance, autoimmunity). The only intervention that reliably bounds the probability of harm is to reduce the trusted component to a size that can be exhaustively verified and to shift all additional functionality to untrusted, isolatable layers.
This mechanism does not depend on any particular technology, era, or cultural context. It is a property of any system where a privileged or essential layer must be correct for the whole to be safe, and where that layer is allowed to expand without a commensurate increase in verification capacity. The Linux kernel incident is merely a recent datum point that makes the mechanism visible; the same logic explains why the 2008 financial meltdown occurred, why the 737 MAX crashes happened, why tax shelters persist despite enforcement efforts, and why autoimmune diseases arise when the immune system’s tolerance network is overwhelmed. Recognizing the pattern lets us move beyond symptom‑chasing — patching individual bugs, tweaking individual securities, adjusting individual flight‑control gains, or closing individual loopholes — and instead address the root cause: the mismatch between the scale of what must be trusted and the scale of what can be verified. The essays that follow this insight will continue to examine other fields where the same mismatch produces failure, confident that the underlying mechanism remains unchanged.