I think what flatestcat wants is something that actually functions and is proven to function correctly. Frama-C is yet another open source project that is long on hype but woefully short on delivery of actual, working code.

Replying to oneself using a bunch of different accounts is an abuse of this site.