Nikolai Tillmann published a paper on DySy, a tool that can infer likely invariants by monitoring the code that is running.

DySy is was built on top of the infrastructure that Pex uses to generate test cases. In fact, it is one of our sample application :)