People from the group developing Spec# at Microsoft Research finally published an article on their new Code Contracts approach.
Chosen excerpts: “embedding of contracts as code is a better approach”; “The language of conditions is just the language of expressions
in the programming language used”; “ForAll and Exists that work over integer ranges and collections”; “Any methods [...]