[nextos]

Adam Chlipala is behind this and his formal methods books are outstanding.

In particular, FRAP is really great: http://adam.chlipala.net/frap