I am slowly working on a “programmable assembler” for basically this purpose — the hope is to start with making it easier to construct simple binaries while also leaving headroom to build abstractions for proofs as scripts.