I was also looking into it to turn normal python functions into some kind of constraints. But as you point out in your article it cannot really work through python imperative statements like conditions and loops, so you either need to find a way to cover all code paths, or only use a subset of Python (like Z3 does to some degree I believe). I still need to try it out further.

For your proof assistant it seems you could indeed use it if you limit yourself to Python expressions. Interesting stuff!