Creusot works on functionalisation if I recall correctly. It translates to coma (https://coma.paulpatault.fr/language/program.html).

Verus encodes directly to SMT.

Creusot may gain some more automation perhaps from this approach.