Proving a grammar unambiguous is in the general case undecidable; Hopcroft, Motwani and Ullman show this by equivalence to the Post correspondence problem in Introduction to Automata Theory, Languages and Computation. But every language that can be parsed with a deterministic pushdown automaton is unambiguous, and IIRC there are some other techniques as well.
I read through your STOKE paper, and I’m a little confused as to how transformation correctness would translate to this use case; is the generator function essentially the grammar itself? (I have a bad habit of thinking of grammars as discrete Markov chains, so I may be confusing myself.) Either way, though, it’s a really clever way of looking at the problem and I wouldn’t mind exploring it further.
I think I’ve gotten this one down to an L-attributed boolean grammar (CFG plus conjunction and negation), and if I understand Okhotin’s paper correctly, it sounds like it’s actually fairly easy to determine whether a boolean grammar is ambiguous or not. (I might well be wrong here, though.)