Hello, Lava2000 has been uploaded to Hackage: http://hackage.haskell.org/cgi-bin/hackage-scripts/package/chalmers-lava2000 Lava is a structural hardware description library embedded in Haskell. This version of Lava focuses on verification, and connects to a number of different verification engines (although only Smv and Satzoo are maintained in this version). For documentation, see the tutorial included in the package. The code is located at http://www.cs.chalmers.se/~emax/darcs/chalmers-lava2000/ People who have other modified versions of the library are welcome to submit patches, so that we get a single version that can be used by everyone. A different version of Lava, with focus on FPGA generation, can be found on Satnam Sing's page: http://raintown.org/lava/ / Emil