Formal verification for Podlang code?

We may want to be able to formally verify certain properties of Podlang code using something like Z3's Constrained Horn Claude or SMT modes. To make this easier, we could export Podlang code in SMTLIB format.

The exact use-case is not obvious yet, but it may be worth discussing this as application-level code might benefit from ways to verify the correctness of application-level Podlang.