NICTA has partnered with US military technology manufacturer General Dynamics to release its seL4 open source secure operating system.
According to NICTA, seL4 is the worlds most highly-assured operating system, and the first OS kernel with an end-to-end proof of implementation correctness and security enforcement.
NICTA claims it is one of the largest machine checked proofs ever done.
The seL4 open source release includes all of the kernel's source code, proof and specifications, plus tools, libraries and example programs useful for building highly trustworthy systems..
All are under standard open source licensing terms.
NICTA software systems research group leader, Gernot Heiser, said seL4 took software dependability to a new level and would support the development of a truly trustworthy systems.
"There is ample evidence of the fundamental shortcomings of today's critical software," he said.
"By open-sourcing seL4 we hope to create a world-wide community of developers of dependable systems, in application areas ranging from national security to automotive, avionics, medical implants, industrial automation and BYOD corporate events."
NICTA senior principal researcher, Gerwin Klein, said the release included the breakthrough proofs of 2009, as well as a host of advanced work built on top of that in the last five years.
"This includes new stronger security proofs, verification of not only the C code, but the binary of the kernel, and a large amount of support and example code that will enable developers to get started quickly."
The release was the result of four years' research by a team of 12 NICTA researchers, University of NSW PhD students and staff.
They successfully verified 7,500 lines of C code and proved more than 10,000 intermediate theorems in more than 200,000 lines of formal proof.
The proof was machine checked using the interactive theorem-proving program Isabelle.