This release of AFV adds counter example generation for both concrete bounded violations or for inconclusive results when the induction fails to converge. I also put Linux and Windows binaries here: http://tomahawkins.org/. http://hackage.haskell.org/package/afv -Tom