<table cellspacing="0" cellpadding="0" border="0" ><tr><td valign="top" style="font: inherit;">Hi all:<br><br>I wanted to share what I have found recently:<br>http://web.archive.org/web/20010712210213/http://www.research.compaq.com/SRC/personal/lamport/tla/threads/threads.html<br><br>I would like to make that for POSIX 1003.4 (original DEC proposal) and post it, would Elegofolks mind to upload the Lamport to CVS tree, I think are important design notes of the Win32 Threads API if at all please let me know if interested.<br><br>Alas it's TLA code may be considered m3theory subdirectory of m3kernel<br><br>In fact there is a TLA checker written in connection with Zeus Algorithm Animation system for automating the animation of proofs, so I guess we just lack that part for further integration.<br><br>Thanks in advance <br></td></tr></table>