RISC-V 基金會宣布，已在採用RISC-V指令集架構的系統上驗證了 seL4 微內核的功能。驗證過程簡化為對 seL4 可靠性的數學證明，顯示其完全符合以形式化語言定義的規範。
可靠性測試允許在基於RV64 RISC-V 處理器的關鍵任務系統中使用 seL4 ，這些系統需要更高的可靠性，但不能保證不會發生故障。
運行在seL4內核之上的軟件開發人員可以完全確定，如果系統某一部分發生故障，則該故障不會擴散到系統的其餘部分，尤其是其關鍵部分。
關於seL4
seL4 架構的顯著特點是將用於管理核心資源的部分從使用者空間移除，並對這些資源使用與使用者資源相同的存取控制方法。
微核心不提供現成的用於管理檔案、進程、網路連接等的高階抽象，而只提供用於控制對實體位址空間、中斷和處理器資源的存取的最小機制。
與計算機交互的高級抽象和控制器以用戶級別執行的任務的形式在微內核之上單獨實現。
通過定義規則來組織對此類任務對微內核中可用資源的訪問。
RISC-V 提供了一個開放且靈活的機器指令系統，允許為任意應用創建微處理器，而無需進行任何推導，也不施加任何使用條件。
RISC-V允許您創建完全開放的處理器和SoC。 當前，根據RISC-V規範，數家獲得各種免費許可的公司和社區（BSD，MIT，Apache 2.0）正在開發數十種已經生產的微處理器內核，SoC和芯片的變體。
自Glibc 2.27，binutils 2.30，gcc 7和Linux 4.15內核發布以來，對RISC-V的支持一直存在。
關於seL4微內核測試
最初，seL4 微核心針對 32 位元 ARM 處理器進行了驗證，後來又針對 64 位元 x86 處理器進行了驗證。
據觀察，開放的 RISC-V 硬體架構與開放的seL4 微核心相結合，將達到一個新的安全水平，因為未來的硬體組件也可以獲得完全驗證，而這對於專有硬體架構來說是不可能實現的。
檢查seL4時，必須假定硬件運行正常（即，如指定的那樣）。 假設首先要有一個明確的規範，但並非所有硬件都如此。
但是，即使存在這樣的規範並且是規範的（即以支持有關其屬性的數學推理的數學形式主義形式編寫的），我們如何知道它實際上捕獲了硬件的行為？
現實情況是，我們可以確定情況並非如此。 硬件與軟件沒有什麼不同，因為兩者都是錯誤的。
但是擁有一個開放的ISA不僅具有免版稅的優勢。 其一是它允許開源硬件實現。
檢查seL4時，假定設備按指示工作，並且規格充分描述了系統的行為，但實際上設備並非沒有錯誤，這在推測執行機制中經常出現的問題中得到了很好的說明。 。
開放硬體平台簡化了與安全相關的變更的集成，例如，透過第三方管道阻止所有可能的洩漏通道，在這種情況下，透過硬體消除問題比嘗試透過軟體尋找解決方案要高效得多。
最後，如果您想了解更多信息，可以參考以下連結中的文章。