I give 99% that fix of Curve25519 is safe, but the rest 1% doesn't let me to use the fix coz this part is the most critical part of Nxt. So without a formal proof I'll stick to loop inside Crypto.sign.
Last one from me:
There's nothing to prove, math stays the same, it's the implementation that's wrong not the math,.
All the math is already in the file in the comments, those comments were made by this "xmath" dude from sci.crypt (I assume this is Matthijs van Duin).
Do you have link Matthijs van Duin comments? Maybe that will convince CFB if you posted the link to Matthijs van Duin