微核心（microkernel）
/ MY-kroh-ker-nel /
如果把整個作業系統放進一個特權程式很冒險，因為任何錯誤都能當掉一切，那麼相反的想法就是把特權核心保持得越小越好。微核心（microkernel）正是這麼做：以完整硬體特權執行的部分被縮減到極小的必要最低限度——基本上只有位址空間、執行緒排程與行程間通訊（IPC）——而檔案系統、裝置驅動程式與網路堆疊則以一般的使用者空間行程（伺服器）執行。想像一個極簡的政府只管法院、道路與郵政，其餘一切外包給獨立的公司；若某個承包商失敗，政府與其他承包商照常運作。
具體來說，在微核心裡，一個單核心用直接函式呼叫處理的請求，變成一場以訊息傳遞進行的對話。要讀一個檔案，你的程式（透過核心的 IPC）送一個訊息給檔案系統伺服器，後者可能再送一個訊息給磁碟驅動伺服器，回覆也循同樣的路徑回來。每個伺服器住在自己受保護的位址空間裡，因此譬如網路伺服器的當掉或被攻陷，無法伸進檔案系統伺服器的記憶體；系統往往甚至能在其餘部分照常運作的同時重新啟動一個故障的伺服器。著名的微核心包括 Mach（影響了 macOS）、L4 及其後裔、QNX（用於汽車與醫療裝置），以及 seL4——它已被形式化驗證為不含大類別的錯誤。
它之所以重要，是因為它是那場結構辯論的另一端。微核心的強處在於穩健（有缺陷的驅動程式無法當掉核心）、安全，以及小到足以被驗證。誠實的代價是效能：把核心內的函式呼叫換成跨保護邊界的訊息傳遞會增加開銷，這正是為什麼早期微核心讓人覺得慢，也是為什麼現代微核心拼命讓 IPC 變快。一個常見的誤解是以為微核心自動就比較好——它是把 IPC 成本拿去換取隔離與可驗證性的刻意取捨，對高保證系統是正確的選擇，但對純粹的產出率未必如此。
在一套以 QNX 為基礎的汽車系統上，磁碟驅動、網路堆疊與檔案系統各自以獨立的使用者空間伺服器執行。若網路伺服器撞上一個錯誤而死掉，核心可以只重新啟動那個伺服器，而引擎控制與顯示任務照常運作——這種故障圍堵的層次是單核心設計難以輕易做到的。
一個極小的特權核心；驅動程式與服務以被隔離的使用者空間伺服器執行，透過 IPC 對話。
seL4 之所以聞名，在於形式化驗證——一個證明核心符合其規格的數學證明——而這之所以可行，正是因為該核心極小。這種證明對一個數百萬行的單核心而言基本上不可能；小體積換來了可驗證性，這也是為什麼對攸關安全的系統來說，IPC 成本的取捨可能值得。