VeriFast is a symbolic evaluator based on Separation Logic (wikipedia) for verifying C and Java code. Specifications can use inductive datatypes, primitive recursive functions and abstract predicates. As the name suggests, a key feature is performance though the abstract also mentions predictability.
Proof in VeriFast relies on symbolic evaluation (using an SMT solver) but can be assisted by lemmas that are written as imperative functions. I think the essence of this is that if you can prove correctness of a terminating lemma function with contract “requires P; ensures Q;”, then “P —∗ Q”. (Where “—∗” (pronounced “magic wand”) is “separating implication” from separation logic.) These lemma functions are allowed to be recursive so it is possible to write inductive proofs.