One feature you can start using right now: prove an assertion with the WP plugin. [1] It's especially useful to prove the absence of some undefined behaviour, bounds on variables, or invariance conditions.

[1] http://frama-c.com/wp.html