As we have mentioned before several times, one important aspect of mbeddr is the support for formal verification, directly integrated with the languages and the IDE. Dan has recently created an introductory screencast. Check it out a Youtube.