The NICTA workshop on operating systems verification brought together invited researchers engaged in research on the development of formally verified operating systems. It was held on 5-8 October 2004 in Sydney, Australia, at the Kensington campus of the University of New South Wales.

These proceedings contain the following contributions. Jonathan Shapiro et al (Johns Hopkins University) attempt to create a verified general purpose operating system implementation, and show why they believe that there is a reasonable chance of success. Kevin Elphinstone (NICTA) introduces L4 as an example microkernel, overviews selected embedded applications benefiting from memory protection (focusing mostly on security related applications), and examines L4's applicability to those application domains. David von Oheimb and Volkmar Lotz (Siemens AG, Munich) describe a framework for modeling and verifying reactive systems, and demonstrate it on two examples: the LKW model of the Infineon SLE 66 smart card chip and Lowe's fix of the Needham-Schroeder Public-Key Protocol. Harvey Tuch and Gerwin Klein (NICTA) use the theorem prover Isabelle/HOL to build an abstract model of the virtual memory subsystem in L4, prove safety properties about this model, and then refine the page table abstraction, one part of the model, towards C source code. Norbert Schirmer (Technical University Munich) develops a general language model for sequential imperative programs together with a Hoare logic, integrated into Isabelle/HOL.