Some months ago I have started a blog about static verification of software.

The blog already contains a significant amount or articles like "Functions, ghost functions and higher order functions", "Framing: An approach to mutability", "Introduction to the proof engine", "Proof procedures" etc.

For those of you who are interested in this topic, you can check it out at http://softwareverificaton.wordpress.com.