my only experience in this area is Dafny, which aggressively automates the proof-finding (by passing it to Z3), but when that fails the compiler is exceedingly

my only experience in this area is Dafny, which aggressively automates the proof-finding (by passing it to Z3), but when that fails the compiler is exceedingly vague on what remaining obligations need to be discharged. You have to stumble around in the dark, trying asserts and assumes, until you narrow down where it got stumped. are there other automated-proof languages that do a better job on this?