"RedLeaf is a new operating system being developed from scratch to
utilize formal verification for implementing provably secure firmware.
RedLeaf is developed in a safe language, Rust, and relies on automated
reasoning using satisfiability modulo theories (SMT) solvers for
formal verification. RedLeaf builds on two premises: (1) Rust's linear
type system enables practical language safety even for systems with
tightest performance and resource budgets (e.g., firmware), and (2) a
combination of SMT-based reasoning and pointer discipline enforced by
linear types provides a unique way to automate and simplify
verification effort scaling it to the size of a small OS kernel."

https://dl.acm.org/citation.cfm?id=3321449
_______________________________________________
coreboot mailing list -- coreboot@coreboot.org
To unsubscribe send an email to coreboot-leave@coreboot.org