Hi Ron,
There is one potential problem that would make a Unicode version of TLA+ impossible: because of TLA+'s use of indentation, it would require a fixed-width Unicode font. So I suggest that you investigate whether one exists and can be used by ordinary Java programs. If it does, then this would not be too hard to implement, and I would be happy to help a volunteer do it.
Leslie