A verification logic supports formal reasoning about properties of programs in a specific programming language by embedding rules coherent with the semantics of the language. This talk will describe a verification logic for Haskell; the term language used in assertions is Haskell98. The logic has some novel aspects. The formula language is a modal mu-calculus in which the modalities are those of Haskell terms. In this logic, formulas distinguish strict from non-strict functions and constructors, finite from infinite data structures, and support assertions of detailed properties of data objects. I will also describe initial experiments in constructing strategy-directed proofs, using the strategy language Stratego as an inference engine.