Formal code verification technology developed at National ICT Australia (NICTA) has been included in MIT Technology Review’s 2011 TR10, an annual list of the world’s ten most important emerging technologies.

Each TR10 winner is drawn from the editors’ coverage of key fields, and is based on a single question: is the technology likely to change the world? These innovations — each represented by a researcher whose vision and work is driving the field — promise fundamental shifts in areas from energy to health care, computing to communications.


NICTA has developed the core of an operating system that can be mathematically proven to be crash proof, and this has applications in embedded computers that are essential to controlling modern cars and medical devices rely on software for their safe operation. In the past testing of that software has been largely a matter of trial and error

Senior project member Dr June Andronick said that NICTA’s seL4 microkernel verification applies mathematical, formal logic to program code and proves that the code will always work reliably, never crash, and at all times operate as its specification dictates, as long as the proof assumptions are met.

“The breakthrough was the demonstration that this kind of proof can be applied to complex, real-world software of realistic size," said Project Leader Prof. Gerwin Klein.

The microkernel is the result of a world-first research achievement announced by NICTA in 2009, in which a team including researchers from the University of New South Wales, completed the first formal machine checked proof of a general-purpose operating system kernel.

“NICTA leads the world in this important area of scientific research. This recognition from MIT is a fitting tribute to the vision and hard work of an enormously talented cross-disciplinary team and endorses NICTA’s unique research approach,” said Hugh Durrant-Whyte, NICTA’s Chief Executive Officer.

NICTA and the other companies included in the 2011 TR10 will be featured in the May/June edition of Technology Review and is posted on the Web at