Although I never tested it, my idea for using it was to essentially analyze it in terms of branches like we do with other control flow. We assess correctness of each branch condition. If all work right, then the goto is fine.
There could be compiler concerns that come up. It was decades ago when I did deep research into it. So, I can't remember if different compilers handle goto differently in a way that can cause breakage. I'm for verifying source to object code equivalence anyway. Anyone doing that might dodge the problem. :)
EDIT: Decided to do a quick search. Found few publications about handling goto's. Just submitted one of most interesting below. I've only read the abstract, though, so I can't tell you more at the moment.
It is common for compiler frontends to translate structured control flow into conditional branches and gotos. GCC, LLVM, and DEC/HP GEM are some of the compilers that do this.  is an old Usenet thread that discusses this topic.