形式化驗證
形式化驗證，是用數學證明一段軟體正確，而不只是用大量輸入去測試、然後祈禱。測試能顯示錯誤存在，卻永遠無法顯示錯誤都不存在——你無法試遍每一種可能的輸入。證明則不同：就像證明幾何定理那樣，它確立「對所有可能的輸入」，程式的行為都恰如其精確規格所言。對於核心這種如此關鍵、如此受信任的東西，這個差別極為巨大。
它的做法，是先為「程式碼應做什麼」寫下一份精確的數學規格，再用一個證明輔助器（一種逐步檢查邏輯、不容缺口的工具）一步步嚴謹地證明：實際的實作永遠滿足那份規格。里程碑式的成果是 seL4，一個微核心，其 C 實作被形式化地證明與其規格相符，且不含整類整類的錯誤——沒有壞記憶體存取造成的當機、沒有緩衝區溢位、正確地執行其隔離保證。這也是微核心觀念為何復興的部分原因：一個微核心夠小（數萬行），證明它正確才真的可行；而要證明一個數百萬行的單核心正確，以今日的能力遠不可及。
誠實的界限非常要緊。一個證明只保證規格所言之事，所以若規格本身錯誤或不完整，這份「經證明正確」的程式碼仍可能做錯事——錯誤只是搬進了規格裡。證明也立基於假設（編譯器、硬體與證明工具本身都正確），而且極度耗費人力，這正是為什麼經驗證的核心既小又罕見。形式化驗證能大幅提高保證程度；它無法交付絕對、無假設的確定性。
打造無人機的工程師想要確定：機上某個元件不能讀取另一個元件的記憶體。他們把關鍵任務跑在 seL4 上，其隔離性質已被數學證明。再多的測試也無法對每一種輸入給出那種保證；而證明一次涵蓋了它們全部——誠實地說，前提是規格與硬體一如假設。
一個證明一次涵蓋所有輸入；測試只能取樣其中一部分。
「經證明正確」指的是「相對於規格正確」——而非絕對安全。若規格錯了，或編譯器、硬體、證明工具有瑕疵，保證仍可能落空。錯誤搬到了假設裡，並未消失。