Thank you, I wanted to do this last night but haven’t had the time.

I think it’s perfectly fine for an algorithm contest not to require a bugfree implementation… but I also feel that if we’re going to standardize on a cryptographic algorithm, throwing all the tools and formal methods we can at it during development of the reference implementation makes a lot of sense.