I really like the concept. However I have some doubts ...

1. How would Pex fare if the system is a state machine ? How would it limit the number of constraints it would need to test out. ?
2. What about unsafe blocks in code ?
3. Also when you say bugs these are purely functional right ..

Also is there any place I can have a look at a sample test report .
I am really looking forward to a fully functional release of Pex.

Regards,
Anand