Have you taken a look at admissibility-based transformations (ABT) [1]?

It seems to solve the issues that concern you (validating the correctness of OT).

[1] http://portal.acm.org/citation.cfm?id=1713726