Can a verified microkernel actually secure a car?

In July 2015, two security researchers took control of a Jeep Cherokee while a journalist was driving it on a St. Louis highway. They reached it over the cellular network, through the entertainment system. From there they got onto the vehicle's internal bus and started sending commands to things that steer and stop the car. Chrysler recalled 1.4 million vehicles.

The technically interesting part of that story is not the initial break-in. Head units are complicated internet-connected computers running large amounts of third-party code, and complicated internet-connected computers get broken into. That is a permanent condition, not a bug someone forgot to fix.

The interesting part is what happened next: nothing stopped them. A compromise of the least safety-critical component on the vehicle became a compromise of the most safety-critical ones, because there was no structural reason it couldn't.

This is the problem formally verified microkernels are actually good at. It is worth understanding precisely what they solve, because the gap between what the technology delivers and what "runs a formally verified kernel" sounds like in a press release is large enough to drive a Jeep through.

What the proof actually says

seL4 is a microkernel developed by the Trustworthy Systems group, originally at NICTA and now at UNSW Sydney. It is roughly ten thousand lines of C, and it has a machine-checked mathematical proof that the implementation conforms to its specification — extended, on some architectures, all the way down to the compiled binary, which removes the C compiler from the set of things you have to trust.

For security purposes the proofs that matter are integrity and confidentiality. Informally: a component running on seL4 cannot modify data it holds no capability to write, and cannot learn information it holds no capability to read. Not "we tested this and it held." Not "we hardened it and hired a red team." It cannot, as a theorem, provided the stated assumptions hold.

That last clause is doing real work and we'll come back to it. But first, why this matters for cars.

Containment, not prevention

Nobody is claiming a microkernel stops your head unit from being hacked. The head unit runs a browser, a Bluetooth stack, a media parser, a cellular modem interface and an app framework. It is going to have vulnerabilities. The claim is narrower and more useful: when it is compromised, the attacker is stuck there.

DARPA's HACMS program produced the clean demonstration. Researchers retrofitted seL4-based software onto a Boeing Unmanned Little Bird helicopter, then gave a red team root access on a non-critical partition and told them to go. They could not reach the flight controls. The isolation held, and the reason it held was not that the team was clever about hardening — it was that the compromised partition simply did not possess the capabilities required to touch the flight control domain, and that fact was proven rather than hoped.

Applied to a vehicle, the architecture looks roughly like this:

This is not hypothetical. The Chinese EV maker NIO ships SkyOS-M, built on seL4, in the mass-produced ONVO L60. NIO is a Premium Member of the seL4 Foundation with a seat on its board, and their engineers presented the production story at the 2024 seL4 Summit. Whatever else you think about this approach, someone is now betting a car company on it.

Where the risk actually goes

Look at that diagram again, specifically the middle box.

The kernel enforces the policy you configured. It does not evaluate whether your policy is any good. And you are going to configure channels between those domains, because the driver wants to see tyre pressure on the touchscreen, adjust the cabin temperature from a phone app, and have the navigation system know how much charge is left. Real vehicles need infotainment and vehicle control to exchange data.

The moment that channel exists, an attack path exists along it. Your actual security now rests on the correctness of a filtering or gateway component that is ordinary, unverified application code, written by ordinary engineers under ordinary deadlines.

This is still a very large improvement. You have taken a system where the attack surface between domains was "twenty million lines of kernel and driver code" and reduced it to "one component whose entire job is to be small and auditable." That is precisely the trade a security architect wants to make. But it is a relocation of risk, not an elimination of it, and the marketing tends to skip that step.

The assumptions attached to the proof

The seL4 team documents these openly, which is to their credit, but several of them bite hard in an automotive context.

Direct memory access. The proofs assume DMA is either disabled or restricted to trusted drivers that you verify yourself. A car is full of DMA-capable peripherals. Handling this correctly means configuring the IOMMU/SMMU properly, and getting it wrong voids the guarantee silently — nothing fails loudly to tell you the theorem no longer applies.

Multicore. This is the sharpest limitation. seL4's proofs model sequential execution. Verification for multicore platforms remains an open problem; Trustworthy Systems have stated they now understand how to do it but lack the funding. An SMP configuration exists and people use it, but it is unverified, and defects have in fact been found in unverified configurations of the kernel including SMP. Automotive SoCs are multicore. The available workaround is a multikernel arrangement with one verified instance per core and hardware strictly partitioned between them, which still does not give whole-system guarantees, because those instances have to trust each other not to corrupt one another's data structures.

Timing channels. The confidentiality proof covers storage channels through architected state the kernel knows about. It explicitly does not address timing channels. Spectre-class microarchitectural leakage is out of scope. There is serious research underway on "time protection" as a principled answer, but the mechanisms so far work in restricted cases on cooperative hardware, and contemporary hardware is largely deficient for the purpose.

Everything underneath. Correctness of the boot code, of the assembly for kernel entry and exit, of TLB and cache-flush operations, and of the hardware behaving as specified. Also, in a real vehicle: the cellular modem's own firmware, any TrustZone secure-world code, and the supply chain that produced all of it.

Platform coverage. The full proof chain, including binary-level correctness, exists for specific architectures and configurations. If the SoC your vehicle programme selected is not among them, you get the architecture and the design discipline without the theorem.

None of these make seL4 a bad choice. They mean the honest claim is "verified under stated assumptions on supported configurations," and that anyone evaluating a vendor should ask which configuration is actually shipping.

What a microkernel does not touch at all

A separate category, and one that microkernel enthusiasm tends to obscure entirely.

The CAN bus is unauthenticated broadcast by design. It was specified in the 1980s for a closed system where every participant was trusted by construction. Any node that can transmit can impersonate any other node. If an attacker lands anywhere with legitimate CAN transmit rights — and something has to have them — isolation upstream does not help. The fixes here are message authentication such as AUTOSAR SecOC, zonal architectures, segmented networks, and moving to authenticated automotive Ethernet. None of these are kernel problems.

Equally untouched: signing and verification of over-the-air updates, key management and storage, physical access through the OBD-II port, relay attacks against keyless entry, and the security of the application code running inside each partition. A verified kernel does nothing for any of it.

So, is it worth it?

Yes, and it should probably be the default for new vehicle architectures. But the operative word is foundation.

What you get is a floor you can reason about mathematically instead of empirically. In security that is genuinely rare. Every other layer of the stack is defended by testing, review, and the accumulated judgment of people who have seen this go wrong before — all valuable, none of it capable of telling you that a class of attack is impossible rather than merely unobserved. seL4 shifts the burden of assurance from twenty million lines of code to roughly ten thousand, plus your inter-domain policy, plus a documented list of assumptions you can go and check.

What you do not get is a secure car. A vehicle built on seL4 with a sloppy gateway component, unauthenticated CAN traffic, and unsigned firmware updates will still be compromised. It will just take slightly longer, and the write-up will be more interesting.

The seL4 project itself is unusually straight about this. Their own FAQ, asked whether the kernel is bug-free, answers that in the formal sense yes, modulo the proof assumptions, and in the ordinary user's sense potentially, because hardware bugs or unmet assumptions may remain — and that the security properties may or may not be sufficient for what your system needs. That is exactly the right register, and it is a useful benchmark for evaluating anyone else who tells you their product is formally verified.

---

Further reading: the seL4 verification status and proof assumptions are documented at sel4.systems. Miller and Valasek's "Remote Exploitation of an Unaltered Passenger Vehicle" (2015) is the Jeep write-up. Klein et al., "seL4: Formal verification of an OS kernel" (SOSP 2009) is the original proof paper.

 

A history of microkernels

Most operating systems people use are monolithic. The kernel is a single large program running with full authority over the hardware, containing the scheduler, the memory manager, the file systems, the network stack, and the device drivers all in one address space. Linux is monolithic. So was classic Unix, and so is Windows in most respects that matter.

The microkernel is the alternative that has been proposed, abandoned, and revived roughly once per decade for over fifty years. The idea is to strip the kernel down to almost nothing — address spaces, threads, and a way for processes to talk to each other — and run everything else as ordinary user-level programs. A file system becomes a server. A disk driver becomes a process. If it crashes, it crashes alone.

This is the story of how that idea developed, why it kept failing, and what changed.

1969–1980: the nucleus

The first statement of the concept came from Per Brinch Hansen, working on the RC 4000 at Regnecentralen in Denmark. His 1969 system had what he called a nucleus, which deliberately implemented no policy at all. It provided a mechanism for processes to exchange messages and nothing more. Scheduling policy, resource allocation, and anything resembling an operating system were left to processes running above it. Brinch Hansen's 1970 paper describing it is the origin document for the whole tradition.

Through the 1970s, Carnegie Mellon's Hydra project on the C.mmp multiprocessor added the other half of the modern picture: capability-based protection. Rather than the kernel consulting a global table to decide whether a process may touch an object, the process holds an unforgeable token granting that specific right. Hydra also drew a hard line between mechanism and policy. Both ideas were absorbed into everything that followed.

The term "microkernel" itself did not come into common use until the late 1980s. The early systems were just called kernels or nuclei.

1980–1990: the first generation

The 1980s produced the first substantial crop of message-passing systems, and they came from quite different worlds.

Thoth and its descendants. David Cheriton's Thoth at the University of Waterloo (late 1970s) was a portable message-passing system that seeded two lineages. Cheriton took the ideas to Stanford and built the V System. Separately, Waterloo alumni Gordon Bell and Dan Dodge founded Quantum Software Systems and shipped QNX in 1982, a commercial real-time microkernel that is still in production more than forty years later. Canada's National Research Council also built Harmony, a real-time multiprocessor system from the same family, which is why "Harmony" occasionally causes confusion in this history.

Amoeba. Andrew Tanenbaum's group at the Vrije Universiteit in Amsterdam built Amoeba from around 1981 as a distributed system: a pool of processors presented to the user as a single machine, with capabilities used to name and protect objects across the network.

Chorus. Started at INRIA in France in 1979, later commercialised by Chorus Systèmes, and eventually acquired by Sun. Chorus was designed for distributed and real-time use and ended up in telecoms equipment.

Mach. The most consequential of the group, developed at CMU from 1985 under Rick Rashid and Avie Tevanian, and descended in part from the earlier Accent system. Mach's design goals were multiprocessor support and Unix compatibility, and it was funded heavily by DARPA. Critically, Mach was derived from BSD rather than written from scratch, and early versions still contained the entire BSD kernel inside the kernel address space. Only Mach 3.0, around 1990, moved the Unix personality out into user space and became a true microkernel.

MINIX. Tanenbaum wrote MINIX in 1987 as a teaching system to accompany his textbook Operating Systems: Design and Implementation. It was a microkernel with the file system and memory manager as separate processes, small enough that its full source could be printed in a book, and it ran on an 8088 with floppy disks and no hard drive.

AmigaOS. Often left out of academic accounts, but Commodore's AmigaOS (1985) was a message-passing microkernel design that shipped on millions of consumer machines and had better interactive response than anything else on a personal computer at the time. It achieved this by omitting memory protection entirely, which is a large asterisk, but it demonstrated that message passing need not be slow.

1988–1994: adoption, and the performance problem

For a few years it looked like the microkernel had won on the merits.

The Open Software Foundation chose Mach 3.0 as the base for OSF/1. Unix System Laboratories bet on Chorus. IBM planned the Workplace OS around Mach. NeXT built NeXTSTEP on Mach 2.5. The Free Software Foundation chose Mach as the base for the GNU Hurd, a multi-server Unix built from independent servers. Rashid published performance figures arguing that microkernel systems could match monolithic ones.

Then the measurements came in from everyone else.

Mach's IPC was slow, on the order of hundreds of microseconds, and its cache footprint was punishing. Every attempt to run a full Unix personality on top of Mach 3.0 produced something noticeably slower than the monolithic kernel it had replaced, and the overhead showed up worst in exactly the workloads that mattered commercially: network traffic and file I/O, where each operation crossed protection boundaries multiple times.

The consequences were structural. NeXTSTEP never moved to Mach 3.0's split design, and its descendant XNU — the kernel in macOS and iOS today — keeps Mach and BSD together in kernel space, making it a hybrid rather than a microkernel. Windows NT, designed in the same period with an executive layer that looks microkernel-shaped, moved the graphics subsystem into kernel mode in NT 4.0 for performance. IBM's Workplace OS was cancelled. The Hurd never reached production.

By the mid-1990s the field's working consensus was that the microkernel was architecturally correct and practically unaffordable.

1992: the Tanenbaum–Torvalds debate

The best-known artefact of this period is a Usenet argument that ran in comp.os.minix between late January and mid-February 1992.

Tanenbaum opened on 29 January under the subject "LINUX is obsolete," arguing that among people who design operating systems the microkernel debate was essentially settled, that writing a monolithic kernel in 1991 was a giant step back into the 1970s, and that tying a kernel to the 386 was a mistake because RISC would displace x86.

Torvalds replied the same day. He conceded the architectural point immediately — microkernels are nicer, and on theoretical grounds Linux loses — but argued that MINIX did not implement the concept well, and that a portable API mattered more than a portable implementation. Tanenbaum's rejoinder included the line about Torvalds being lucky not to be his student.

The thread is more interesting for its other participants. Ted Ts'o raised the context-switch and copying costs in OSF/1 Mach that were already sinking it commercially. Ken Thompson posted a brief note saying microkernels were probably the future but monolithic kernels were easier to build and easier to turn into a mess. Peter da Silva pointed out that AmigaOS had been shipping a message-passing design on three million machines while everyone argued about research systems. Several people questioned whether MINIX was really a microkernel in the sense Mach was.

The debate settled nothing technically. Its lasting significance is as a snapshot of what the field believed in 1992, and for the argument it drifted into later about whether distributed development without a single controlling architect could work.

1993–2000: the second generation

Jochen Liedtke at GMD in Germany rejected the conclusion that microkernels were inherently slow. His position was that Mach's overhead was an implementation artefact, and he demonstrated it empirically.

L3 (1993) and then L4 (1995) were written largely in hand-tuned assembly, with the design driven by cache behaviour rather than abstraction. L4's IPC was roughly ten to twenty times faster than Mach's. Liedtke's 1995 SOSP paper "On µ-kernel construction" supplied the field with its governing principle: a concept belongs inside the kernel only if moving it outside would prevent the implementation of required system functionality. Not if it is faster inside, not if it is convenient. Only if the system otherwise cannot work.

L4 became a family rather than a product. Fiasco was developed at TU Dresden, along with L4Linux, which ran a paravirtualised Linux kernel as a user-level server and demonstrated single-digit percentage overhead. L4Ka::Pistachio came from Karlsruhe, where Liedtke had moved. Hermann Härtig's group published the 1997 SOSP paper "The performance of µ-kernel-based systems," which put numbers behind the claim that the second generation had fixed the problem.

Liedtke died in 2001. His students carried the work forward, and one commercial descendant, OKL4 from Open Kernel Labs, went on to ship in billions of mobile phone basebands and Qualcomm modems — meaning that for much of the 2000s, most people carrying a phone were carrying a microkernel without knowing it.

Meanwhile the first generation persisted in places that valued isolation over benchmarks. QNX moved into automotive and industrial control. Green Hills shipped INTEGRITY for avionics. SYSGO shipped PikeOS for certified safety-critical use. These systems were never fashionable and never went away.

2000–2015: capabilities and proofs

The third generation of microkernels is distinguished by capability-based access control done properly, and by an ambition that would have seemed absurd earlier: proving the kernel correct.

Gernot Heiser, who had collaborated with Liedtke, moved to UNSW Sydney and later NICTA, where the group became Trustworthy Systems. Around 2004 they began asking whether an L4-style kernel could be made small enough to formally verify. The reasoning followed directly from Liedtke's minimality principle. The point of a microkernel is a tiny trusted computing base, and a tiny base is one you might actually be able to prove things about.

seL4 was a redesign rather than a verification of an existing kernel. Its central change was that the kernel never allocates memory dynamically: all kernel memory is explicitly accounted for through capabilities held at user level, which removes an entire class of behaviour that would otherwise be intractable to reason about.

In 2009, Gerwin Klein and colleagues published the functional correctness proof at SOSP — a machine-checked Isabelle/HOL proof that roughly 8,700 lines of C conformed to an abstract specification. Later work extended this to the compiled binary, removing the C compiler from the trusted base, and added proofs of integrity and confidentiality plus sound worst-case execution time analysis. NICTA released the sources and the proofs as open source in July 2014.

Tanenbaum, meanwhile, had returned to the subject from a different direction. MINIX 3, released in 2005, abandoned the teaching mission for a reliability one: drivers run as isolated user processes, and a reincarnation server detects a crashed driver and restarts it without taking down the system. MINIX 3 later acquired an unexpected distinction when researchers established that a version of it runs inside the Intel Management Engine on essentially every modern Intel chipset, arguably making it the most widely deployed operating system in the world.

Other third-generation work from this period includes NOVA, a capability-based hypervisor microkernel from Dresden, and the Barrelfish multikernel from ETH Zurich and Microsoft Research.

2015–present: back in production

Three things happened more or less at once.

seL4 moved from research to deployment. DARPA's HACMS program provided the public demonstration: a Boeing Unmanned Little Bird running seL4-based software resisted a red team that had been given root access on a non-critical partition and still could not reach the flight controls. The seL4 Foundation launched on 7 April 2020 under the Linux Foundation, and is now becoming an independent Swiss association. Verification has continued, with the AArch64 port recently gaining a proof of confidentiality enforcement on top of functional correctness and integrity.

Google built Fuchsia. Its Zircon kernel is a capability-based microkernel descended from the LK embedded kernel, and Fuchsia shipped commercially on the Nest Hub in 2021, though its longer-term role at Google has never been entirely clear.

Huawei put one under a phone. Work on the HongMeng kernel began around 2016 or 2017 and became urgent after the May 2019 Entity List placement threatened Android access. Early HarmonyOS versions were marketed as microkernel-based but ran a Linux kernel with AOSP compatibility layers on phones, with the actual microkernel confined to watches, IoT devices, and trusted execution environments — a gap that Heiser among others criticised publicly.

HarmonyOS NEXT closed it. Announced in August 2023 and released in October 2024 as HarmonyOS 5, it drops the AOSP layer entirely, cannot run Android APKs, and runs on the HongMeng microkernel over OpenHarmony. Huawei's OSDI 2024 paper describes HongMeng as a capability-based multi-server microkernel engineered for general-purpose performance and Linux ABI compatibility. All new Huawei devices in China now ship it. It is the first serious attempt to put a microkernel under a mass-market consumer smartphone, and its results will matter regardless of how they turn out.

Where things stand

The microkernel never won the general-purpose desktop or server market and shows no sign of doing so. Linux is monolithic and dominant. But the design has quietly become the default in the places where isolation is worth paying for: avionics, automotive, industrial control, secure separation kernels, phone basebands, and hardware security modules. Loadable kernel modules, which Linux adopted in 1995, absorbed enough of the modularity argument to remove the pressure elsewhere.

The more interesting shift is in what the argument is about. In 1992 it was performance and portability. Liedtke settled the performance question by 1997. What replaced it is assurance: how small can the part of the system you have to trust be made, and can you prove anything about it. That is a question a monolithic kernel cannot even ask, and it is the reason the idea is still alive fifty-five years after Brinch Hansen described it.

---

Further reading. Brinch Hansen's "The nucleus of a multiprogramming system" (CACM, 1970). Liedtke's "On µ-kernel construction" (SOSP, 1995). Klein et al., "seL4: Formal verification of an OS kernel" (SOSP, 2009). The 1992 Usenet thread is reprinted as Appendix A of Open Sources: Voices from the Open Source Revolution (O'Reilly, 1999).

 

Microkernels: a thirty-five year argument

In January 1992, Andrew Tanenbaum told a Usenet newsgroup that among people who actually design operating systems, the debate was over and microkernels had won. He was wrong for about thirty years. Linux ate the world. Mach became a punchline. The GNU Hurd never really shipped.

Then, in October 2024, Huawei put a capability-based microkernel underneath a mass-market consumer phone, and it worked. Meanwhile a formally verified microkernel from Sydney had spent a decade quietly becoming the default choice for anything where a kernel bug means someone dies.

So who won? The honest answer is that the question was badly posed, and it took the industry three decades and one very public flame war to figure out why. Here is how it went.

The idea

The core insight predates the word. Per Brinch Hansen's RC 4000 "nucleus" in 1969 proposed that a kernel should provide only a mechanism for processes to communicate. Everything else — file systems, drivers, network stacks — belongs in ordinary user processes. Carnegie Mellon's Hydra in the 1970s added capability-based protection, the idea that access rights are unforgeable tokens a process holds rather than entries in a global table the kernel consults.

The appeal is structural. A monolithic kernel is one enormous program running with total authority over the machine, where a bug in a printer driver can corrupt the file system. Push the drivers out into user processes and a driver crash becomes a process crash. The kernel shrinks to something you might actually be able to reason about.

The cost is that everything now requires message passing across a protection boundary, and protection boundaries are expensive.

The first generation, and why it failed

The 1980s produced the first real crop. Mach, developed at CMU from 1985 under Rick Rashid and Avie Tevanian, was the most influential by far. It was BSD-derived, it became the base for NeXTSTEP and later XNU in macOS and iOS, and it anchored both OSF/1 and the GNU Hurd. Alongside it ran Chorus in France, Amoeba (Tanenbaum's distributed system), QNX from 1982 (commercial, real-time, descended from Waterloo's Thoth), and MINIX, Tanenbaum's 1987 teaching system.

Mach is also what gave microkernels their bad reputation. IPC cost hundreds of microseconds. The cache footprint was terrible. Every serious attempt to build a Unix on top of it produced something measurably slower than the monolithic kernel it replaced. NeXTSTEP eventually gave up and folded BSD back into kernel space, which is why XNU today is a hybrid rather than a true microkernel. By the mid-1990s the working consensus was that the design was elegant and impractical.

The flame war

The famous argument happened in comp.os.minix between late January and mid-February 1992, and it is worth reading because almost nobody in it argued the way the legend says they did.

Tanenbaum opened on 29 January under the subject line "LINUX is obsolete." His case had two prongs. On architecture, he listed RC4000, Amoeba, Chorus, Mach and the unreleased Windows NT as microkernel systems, cited Rashid's Mach 3.0 performance papers as evidence that the old speed objection was dead, and called writing a monolithic kernel in 1991 a giant step back into the 1970s. On portability, he predicted RISC would displace x86, so binding a kernel to the 386 was a mistake. MINIX had been ported to 68000, SPARC and NS32016. Linux had been ported nowhere.

Torvalds replied the same day, and the reply is nastier than people remember. He went after the framing before the substance: Tanenbaum made money from MINIX while Linux was free. Being a professor, he said, was a fine excuse for MINIX's brain damage.

But then he conceded the architecture point immediately. Microkernels are nicer. On theoretical and aesthetic grounds, Linux loses. His counter was that MINIX did not actually do the microkernel thing well, with its single-threaded file system and its lack of real multitasking in the kernel. And on portability he drew the distinction that turned out to matter: the Linux API was portable because it followed Unix and POSIX, while the implementation was 386-specific by choice. He noted that the entire Linux kernel source was smaller than just the i386-dependent portion of Mach.

Tanenbaum's rejoinder defended MINIX's limits as pedagogical, since it had to run on a diskless 4.77 MHz PC, dismissed multithreaded file systems as a performance hack, and told Torvalds he should be thankful he wasn't his student, because that design would not earn a good grade. He extended the metaphor: a second F for the term, with a chance to pass on the final.

Torvalds apologised the next day for his tone, signing off as a hothead in his first and hopefully last flamefest.

The parts people forget

The thread's best technical content came from third parties, and their objections to Tanenbaum were sharper than Torvalds'.

Ted Ts'o cited Brent Welch's argument that the file system is a mature enough abstraction to belong in the kernel, and raised context-switch and copying costs in OSF/1 Mach for network traffic. That is precisely the problem that would sink Mach commercially. Lawrence Foard complained that OS theorists never test their ideas; Tanenbaum replied that he was mortally insulted and not a theorist, pointing at OSF, Chorus at USL, Amoeba, and QNX's 200,000 installed systems.

Peter da Silva defended microkernels from a completely different direction. AmigaOS was a message-passing microkernel design running on three million machines with better response time than anything else on a PC, and it had been shipping for years while everyone argued about research systems.

Ken Thompson posted a short, dry note: microkernels were probably the future, but a monolithic kernel is easier to implement, and also easier to turn into a mess as it is modified. Several people, including David Megginson and Douglas Graham, questioned whether MINIX was really a microkernel in the sense Mach was.

Then Tanenbaum posted "Unhappy campers," and the debate stopped being about kernels. He identified three sticking points, the third being whether software ought to be free, defended MINIX's $169 price, and asked whether Torvalds would ever let Linux out of his control. Torvalds' answer was two words: he wouldn't. He had already floated the idea of a kernel mailing list to make release decisions. Tanenbaum invoked Harlan Mills' surgical-team model and argued that a widely dispersed group hacking on complicated code without one person in charge produces anarchy.

That exchange, not the microkernel one, is what the next thirty years actually tested.

The third path nobody was arguing for

Six weeks after Tanenbaum's post, on 12 March 1992, Bill and Lynne Jolitz released 386BSD 0.0. Half the posters in the thread had been waiting for exactly this. Charles Hedrick and Richard Tobin both said they would jump ship the moment a free BSD or GNU appeared. Torvalds himself said in later years that if 386BSD had existed when he started, he probably would not have bothered writing Linux.

Jolitz never participated in the microkernel argument, as far as any surviving archive shows. His own famous 1992 Usenet post came in March, and it was about his split from BSDI, not about kernel structure. But his writing on kernel design is more interesting than his absence from the thread suggests.

In the very first installment of "Porting UNIX to the 386" in Dr. Dobb's Journal, published a full year before the debate, he asks why Unix kernels are so big and complex and answers it himself: different groups claim a piece of the kernel to further their own agendas, instead of redesigning for common support or moving out things that really belong in an application process. He cites the rumour that SVR4 alone contained fourteen filesystems that were variations on a theme, calls it a Chinese menu approach producing a bloated kernel that is hard to enhance or maintain, and says standards by accumulation do not work.

That is a minimality argument, published by a monolithic-kernel author, in a series Torvalds was reading while writing Linux.

By 386BSD Release 1.0 in October 1994, Jolitz had gone further. The release notes describe a kernel composed of independent modules, compile-time configuration replaced by a run-time metaphor, interface scope explicitly controlled at four levels (module, class, kernel, user), and module interfaces exportable to user mode or to the network. There are kernel threads, address-space sharing, and a stated goal of eliminating panic() entirely in favour of containing the damage, shedding the affected control path, releasing resources, and recovering integrity.

That last item is the microkernel reliability argument, the one Tanenbaum would make again about MINIX 3 a decade later, pursued from inside a monolithic BSD. Loadable modules were the compromise that made the pure monolithic-versus-microkernel framing obsolete in practice, and Linux adopted them in 1995.

L4: the implementation was the problem

Jochen Liedtke at GMD in Germany refused to accept that microkernels were inherently slow. His argument was that Mach was a bad implementation, not a bad idea, and he proved it with numbers. L3 in 1993 and L4 in 1995, hand-written in assembly, achieved IPC roughly ten to twenty times faster than Mach.

His 1995 SOSP paper "On µ-kernel construction" gave the field its governing principle: a feature belongs in the kernel only if moving it out would prevent the system from meeting a functional requirement. Not "if it's faster there." Not "if it's convenient." Only if the system otherwise cannot work.

L4 spawned a family: Fiasco at Dresden, L4Ka::Pistachio at Karlsruhe, and OKL4 from Open Kernel Labs, which shipped in billions of phone basebands and Qualcomm modems. Most people carrying a phone in 2010 were carrying a microkernel and had no idea. Liedtke died in 2001; his students carried the work on.

seL4: proving it

Gernot Heiser, one of Liedtke's collaborators, moved to UNSW Sydney and then NICTA. Around 2004 his group started asking a question that follows naturally from Liedtke's minimality principle: if the whole point of a microkernel is a tiny trusted computing base, and the base is tiny, could you formally prove it correct?

seL4 was a redesign rather than a verification of existing L4. Its key move was replacing ad-hoc memory management with a capability system in which all kernel memory is explicitly accounted for by user level, so the kernel never allocates dynamically. That makes the kernel's behaviour tractable to reason about.

In 2009 Gerwin Klein and colleagues published the functional correctness proof at SOSP: a machine-checked Isabelle/HOL proof that roughly 8,700 lines of C matched an abstract specification. Later work added binary-level proofs, removing the compiler from the trusted base, plus integrity, confidentiality, and worst-case execution time analysis.

NICTA open-sourced the kernel and the proofs in July 2014. The seL4 Foundation launched on 7 April 2020, initially hosted under the Linux Foundation, and is now becoming its own Swiss association. DARPA's HACMS program gave the technology its public demonstration when a Boeing Unmanned Little Bird running seL4-based software resisted a red team that had root access on a non-critical partition and still could not reach the flight controls.

Verification continues. The AArch64 port has now gained a proof of confidentiality enforcement, on top of functional correctness and integrity, showing formally that an application running on seL4 cannot learn information it is not authorised to see.

HongMeng: the consumer bet

Huawei began work on what became the HongMeng kernel around 2016 or 2017. The project became urgent after the May 2019 Entity List placement threatened its Android access. HarmonyOS launched later that year, described from the outset as microkernel-based, and reached phones and tablets with version 2.0 in 2021.

The microkernel claim was contested for years, and fairly so. HarmonyOS 1.x through 4.x on phones ran a Linux kernel with AOSP compatibility layers. The actual microkernel shipped mainly on watches, IoT devices, and trusted execution environments. Heiser and others criticised the marketing publicly. The open-source portion, OpenHarmony, was donated to the OpenAtom Foundation in 2020.

HarmonyOS NEXT changed that. Announced at HDC on 4 August 2023 and released in October 2024 as HarmonyOS 5, it drops the AOSP layer entirely, cannot run APKs, and runs on the HongMeng microkernel over OpenHarmony. Huawei published a paper at OSDI 2024 describing HongMeng as a capability-based multi-server microkernel engineered for general-purpose performance and Linux ABI compatibility. All new Huawei devices in China now ship it, with international expansion targeted for 2026.

The connection to seL4 is intellectual rather than genealogical. HongMeng borrows the capability model and the formal-verification ambition that seL4 established, and Huawei's formal methods teams cite that literature, but it is a separate codebase and its verification claims cover components rather than the whole kernel to seL4's standard.

So who won

Tanenbaum was right that microkernels were the better architecture and wrong about almost everything else. He was wrong about RISC displacing x86 on the timeline he predicted. He was wrong that the performance question was settled in 1992, since Mach's overheads were real and it took Liedtke three more years to fix them. He was most wrong about coordination, arguing that distributed development without a single controlling architect produces anarchy, at exactly the moment Torvalds was inventing the thing that disproved it.

Torvalds was right that availability beats elegance and that a portable API matters more than a portable implementation. He conceded the architectural point in his very first reply and has never really taken it back.

And the actual resolution came from neither of them. It came from Liedtke, who showed the performance objection was an implementation artifact; from Heiser's group, who showed a small kernel can be proven correct rather than merely asserted to be; from Jolitz and later Linux itself, whose loadable modules dissolved the binary framing; and now from Huawei, testing whether any of it survives contact with a billion consumers.

Thirty-five years on, the microkernel argument turns out to have been the wrong argument. The right one was about how small the part you have to trust can be made, and whether you can prove anything about it. On that question, the answer keeps getting better.

---

Sources: the full "LINUX is obsolete" thread is reprinted as Appendix A of Open Sources: Voices from the Open Source Revolution (O'Reilly, 1999). Jolitz's Dr. Dobb's series is archived on the Internet Archive as "Porting Unix to the 386," and the 386BSD 1.0 and 2.0 trees are on GitHub. seL4's proofs and verification status are documented at sel4.systems.

OpenHarmony

 https://en.wikipedia.org/wiki/OpenHarmony

The main official website for OpenHarmony is https://www.openharmony.cn/ .

This is the central hub for the open-source project, where you can find:

• Project introduction and governance information 

• Official documentation for developers 

• News and announcements about the project 

• Source code repository links (the code is hosted on Gitee at https://gitee.com/openharmony) 

🌐 For International Users

If you are located outside of mainland China, the project also maintains an international website: https://www.openharmony.io/ .

📚 Other Key Resources

Resource	URL
Official Documentation	https://www.openharmony.cn/docs/
Developer Documentation	https://docs.openharmony.cn/
Source Code (Main Repo)	https://gitee.com/openharmony
Online Discussion Forum	https://zulip.openharmony.cn/

🌐 Main Websites & Repositories

Resource	URL	Description
Source Code Repository	https://openharmony.gitee.com	Primary location for all OpenHarmony open-source code repositories.
Main Project Page	http://www.openharmony.cn	Official project homepage (Chinese).
Official Documentation	https://docs.openharmony.cn	Project documentation (Chinese).
DevEco Marketplace	https://repo.harmonyos.com	For obtaining open-source distributions and customizing bundles.

📥 Source Code Download Methods

There are three primary methods to obtain the code, depending on your needs.

1. Using repo & git from Gitee (Recommended)

This is the standard method for developers and those who want to work with the latest or most stable codebase.

• Prerequisites: You need to install git, git-lfs, and the repo tool. You should also register an account on Gitee and configure an SSH key for secure access.

• Latest Development Code ("Master" branch):

  bash

  repo init -u https://gitee.com/openharmony/manifest.git -b master --no-repo-verify
  repo sync -c
  repo forall -c 'git lfs pull'

  (To use SSH, replace the URL with git@gitee.com:openharmony/manifest.git) 

• Stable Release Version:
  Replace master with the specific version branch you need. For example, to get OpenHarmony 5.0:

  bash

  repo init -u https://gitee.com/openharmony/manifest.git -b OpenHarmony-5.0-Release --no-repo-verify
  repo sync -c
  repo forall -c 'git lfs pull'

2. Download via DevEco Marketplace

• Best for: Beginners or those who want a customized distribution by selecting specific components.

• How it works: You can browse and customize distributions on the DevEco Marketplace website. After making your selections, the system generates a bundle list, and you use a command-line tool called hpm-cli to download and install the bundles on your local machine.

3. Download Mirror Packages (Simple) 📦

• Best for: Quickly obtaining an older, stable version via a direct compressed file.

• Details: This method offers fast downloads from mirror sites but usually only for specific Long-Term Support (LTS) releases (like version 3.0). You can find the download links (.tar.gz files) and their checksums in the official documentation.