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

Creusot works on functionalisation if I recall correctly. It translates to coma (https://coma.paulpatault.fr/language/program.html https://coma.paulpatault.fr/language/program.html). Verus encodes directly to SMT. Creusot may gain some more automation perhaps from this approach.