The B+N ending in Kriegspiel was proven to be a win by Ferguson, notably published in a TCS (theoretical computer science) journal.

http://www.sciencedirect.com/science/article/pii/030439759290344F

He later handled B+B but I think it remained unpublished.

http://www.math.ucla.edu/~tom/papers/unpublished/kriegbishop.pdf

In general, proving draws (from fortresses) is easier than proving wins for humans. I guess you could write K+Q and K+R as induction proofs, and in general (see B+N) you want to progress from one goal to the next, but clarifying this is in an explicitly mathematical way is not typical.

There is a lot of misunderstanding regarding computers and fortresses, as usually the humans do not use the right tools (they will use a general computer program and "root search" for instance). Moreover, phrases like "decisive advantage" are not really meaningful to a computer until a win is actually proven (today's game of Giri versus Hou Yifan had some interpretations of computer scores erroneously giving a "decisive advantage in a 7-piece rook ending at a point when it was drawn). It is diverging into peculiarities of chess analysis, but one simple yet often superior alternative involves seeing (indicating the above Mamedyarov-Caruana draw quite easily, though proof is a different question) whether the computer's score increases or not as the search goes on (e.g., is some progress being made, such as pushing a pawn?). Of course, that will not likely help in extreme (contrived) examples, but in most practical cases this suffices. The programmer of "Houdini" had a special mode (reduction of 50-move rule) to try to suss out fortresses, demanding progress to be made faster. There is also Bleicher's "Freezer" that is a human/computer interactive proof: you make the "rules", and it iterates over positions.

http://www.minet.uni-jena.de/preprints/bleicher_04/FREEZER_.PDF

http://www.freezerchess.com/