http://vfmd.org has an exhaustive and unambiguous formal spec for (a variant of) Markdown. As a bonus, it's easy to understand, nicely extensible, and has an example implementation. The only drawback I'm aware of is that it seems routinely ignored by nearly everyone. I wonder why?
I have not looked into the details of the grammar, but proving that a grammar is unambiguous is typically done by proving that it is in, say, LL(1) or LR(1) (or some related family). This approach towards unambiguity has the additional advantage that it is easy to derive a parsing algporithm directly from the grammar that has nice theoretical properties (e.g. linear parsing time in the input length; where the hidden constant depends on the grammar).
So it's basically as useless for general processing as Markdown, because you
won't have a grammar from which you can generate parser, hence all the parsers
will be handcoded with various quirks differing from one to another and none
of which will produce a parse tree.
I mean, Foo = "hello" / "hello" is totally acceptable, and if you have any indirection like Foo = XXX / YYY with XXX, YYY = "hello" you can then attach different semantics to XXX and YYY despite it being ambiguous. Add in more levels of indirection, and you have a lower chance of it being trivially obvious.
Great for library / parser implementers and it helps discover ambiguities.