Hi all, My masters project Zeno was recently mentioned on this mailing list so I thought I'd announce that I've just finished a major update to it, bringing it slightly closer to being something useful. Zeno is a fully automated inductive theorem proving tool for Haskell programs. You can express a property such as "takeWhile p xs ++ dropWhile p xs === xs" and it will prove it to be true for all values of p :: a -> Bool and xs :: [a], over all types a, using only the function definitions. Now that it's updated it can use polymorphic types/functions, and you express properties in Haskell itself (thanks to SPJ for the suggestion). It still can't use all of Haskell's syntax: you can't have internal functions (let/where can only assign values), and you can't use type-classed polymorphic variables in function definitions - you'll have to create a monomorphic instance of the function -but I hope to have these added reasonably soon. It's also still missing primitive-types/IO/imports so it still can't be used with any real-world Haskell code, it's more a bit of theorem proving "fun". You can try it out at http://www.doc.ic.ac.uk/~ws506/tryzeno, the code file given there has some provable properties about a few prelude functions among other things. Another feature is that it lists all the sub-properties it has proven within each proof. When it verifies insertion-sort "sorted (insertsort xs) === True" it also proves the antisymmetry of "<=" and that the "insert" function preserves the "sorted" property. Any suggestions or feedback would be greatly appreciated. Cheers, Will