I think you'd want it to be a theorem (in Lean, Coq, Isabelle/HOL or whatever) instead of a constraint problem. So it would be more limited by developer effort

I think you'd want it to be a theorem (in Lean, Coq, Isabelle/HOL or whatever) instead of a constraint problem. So it would be more limited by developer effort than by computational power. Theoretically you can do this from software down to (idealized) gates, but in practice the effort is so great that it's only been done in extremely limited systems.