JSONSerializer review, further study of reviewable coding techniques

Last time around, we took a look at some mutable state abstractions,
Prize and Milestone, to make the JSONWriter more reviewable. For
JSONSerializer, a client of JSONWriter, I haven't come up with any
interesting coding patterns, but do have a commenting question to
think about.

The JSONSerializer has some security relevant constraints to enforce
in its implementation, that, AFAICT, aren't readily expressible in the
language provided by Joe-E. So this produces some questions:

1. Is there an alternate design where the documented constraints could
be verified by Joe-E?
2. Is there some extension of the Joe-E verifier that would enable
this verification?
3. If verification is not feasible, what's the best way to explain how
the constraints are enforced?

What I've got so far is an implementation comment at the start of the
main method, which attempts to precisely define the enforced
constraints. The implementation is then written to make clear that the
constraints are being enforced, falling back to more comments in cases
where this may not be clear. The current version is at:

http://waterken.svn.sourceforge.net/viewvc/waterken/server/trunk/waterken/syntax/src/org/waterken/syntax/json/JSONSerializer.java?view=markup

So, is this the state-of-the-art? Can we do better?

--Tyler