The L4.verified microkernel from NICTA, being commercialized by Open Kernel Labs, is the first operating system with a complete code-level proof of correctness. For critical systems, this level of correctness provides confidence beyond that possible by testing alone. Combined with Galois' capability to build high assurance software, the L4.verified microkernel enables Galois to implement solutions with higher assurance than previously possible. L4.verified currently runs on the ARM family of processors.
Collaborate with Us
Licensing - Obtain a license for one of our advanced technologies.
Research & Development - Solve your toughest problems by exploring new approaches with us.
Training - Learn how to use cutting-edge tools to increase trustworthiness in your critical systems.