Ironclad – formally verified, real-time capable, Unix-like OS kernel
6 months ago
- #formal-verification
- #operating-system
- #open-source
- Ironclad是一个经过形式化验证、类UNIX的操作系统内核，适用于通用计算和嵌入式场景。
- 采用SPARK/Ada语言编写，作为100%自由软件提供POSIX兼容接口。
- 核心特性包括抢占式多任务、强制访问控制(MAC)和硬实时任务调度。
- 基于GPLv3协议完全开源，无需任何专有固件支持。
- 通过SPARK形式化验证确保加密模块、MAC机制及用户接口零错误。
- 支持多平台移植，可通过GNU工具链轻松实现交叉编译。
- 项目资金来自NGI Zero Core计划，接受NLnet基金会和欧盟委员会资助，依靠捐赠和拨款维持发展。