Jessie library, from why certification tool, is useful for deductive verification. it is based on weakest precondition computation techniques and allows to prove that c functions satisfy their specification.