Gerwin Klein has recently launched his blog proofcraft.org, which is on “the craft, art, and science of interactive machine-checked proof”. He further says:

This is a blog about formal software verification in general and a tendency towards interactive theorem proving and the prover Isabelle/HOL in particular.