A note has just been posted to the isabelle users list about new formal proofs of theorems related to CSP. Here are the urls: http://afp.sourceforge.net/entries/List_Interleaving.shtml http://afp.sourceforge.net/entries/Noninterference_Ipurge_Unwinding.shtml http://afp.sourceforge.net/entries/Noninterference_Generic_Unwinding.shtml Adrian Lawrence