The Coq mailing list

[Tom Prince <tom.prince AT ualberta.net>]

On Tue, 01 Nov 2011 13:40:38 -0400, Adam Chlipala 
<adamc AT csail.mit.edu>
 wrote:
> > I'm used to unit testing my programs with QuickCheck 
> > <http://www.yellosoft.us/quickcheck>, a probabilistic verifier that 
> > brute forces properties such as |propReversible :: String -> Bool| 
> > (Haskell notation). How easy would it be to refactor QuickCheck tests 
> > into Coq tests?
> >
> 
> I assume there is no deep technical challenge in porting QuickCheck to 
> Coq, but we care less about tests when we prove program correctness.  I 
> don't know of an extant QuickCheck-for-Coq implementation.

There is a partial implementation of quickcheck available in Seanj
Wilson's rippling plugin[1].

Footnotes: 
[1] https://github.com/tomprince/rippling