These videos come from the Verification Corner youtube channel. If you work through their list, the oldest (furthest from top of list) is the earlier ones on which the later ones build. These videos were done to promote a research project at Microsoft called Spec# where the developer of ESC/Java JML processor extended the approach for C# programs. There is a wikipedia entry for Spec#. There is a MicroSoft research home page on the project. At CodePlex, the source code can be downloaded (also included are instructions for building). Below I list them in `viewing order'.