Your intuition is pretty much on point from my POV, and you’ve also hit the same problem that people in the AD world encounter: branches mess up everything.
Basically, no, you can’t overload if from inside julia, since it’s not a function. See also this previous discussion about much the same topic.
That being said, you could theoretically build an interpreter of julia IR using the abstract interpretation framework, which ends up emitting not llvm IR, but SMT statements that you’d then feed to an existing solver like z3 or the like (or maybe some other solver, depending in what exactly you’re interested in).
Practically speaking though, this is still super difficult. The abstract interpreter interface is sparsely documented at best, and translating things like x::Foo = ... into an SMT clause is challenging, not to mention then actually proving useful properties. Specifications unfortunately don’t compose and even if they would do that cleanly, it’s still super difficult (if you only read one of these links, read this one) and complex to prove even comparatively simple things.