Recent work in computer science has produced techiniques for proving, mathematically, the correctness of programs. the techniques are currently too time-consuming and difficult for most applications, but are being used to develop the security kernel (central nucleus) for some secure operating system.