Frama-C is also very cool. Also Coq VST and however seL4 does it. I think out of all of these, CBMC requires the least expertise / has highest automation. I also don't see how it can scale beyond the unit test level, or patch together verification conditions into global properties. Perhaps this could be done by some meta framework plugging together calls to CBMC. Given the level of penetration of formal methods generally, I think the relatively low ambition of CBMC compared to these higher ceiling techniques is good.

Thanks, very interesting stuff!