For this purpose, C is a very convenient and very portable assembly language. You could use a verified C compiler like CompCert to convert it to machine code.
In an ideal world, there’d be no C compiler in the loop at all, sure. But in practice it’s not causing any trouble at all in a ZZ -> C -> machine code workflow. Quite the reverse, targeting C has some major benefits. (There are C compilers that are very fast, very highly optimizing, very portable, and/or verifiably correct.)
Edit to add: just realised I might have totally misunderstood your comment, sorry! Apologies for jumping the gun if so.
If you just mean can we save the generated C to disk instead of compiling it, yes, I would hope so too.
Absolutely!
The zz export command just dumps the C and SMT code along with makefiles for common build systems and stops there. Very handy for using it within other toolchains.
Presumably we can dump the C before compilation?