Clean, Haskell, LNT, LOTOS, Maude, mCRL2, OCaml, Opal, Rascal, Scala, SML, Stratego/XT, and Tom. We submitted these translations to sixteen compilers, interpreters, and rewrite engines: eleven of them reported that all the 203 tests passed successfully, while the other tools halted or timed out. Moreover, some involved components (namely, the binary adders and multipliers) have been validated separately using more than 30,000 test vectors.

Conclusion {#CONCLUSION}
==========

Twenty-five years after, we revisited the Message Authenticator Algorithm (MAA), which used to be a pioneering case study for cryptography in the 80s and for formal methods in the early 90s.

We developed a formal specification of the MAA, expressed as a term rewrite system encoded in the REC language. As far as we are aware, it is one of the largest handwritten term rewrite systems publicly available. This specification is self-contained and self-checking, as it includes 203 test vectors. It has been carefully validated using a dozen tools.

Parts of this specification (in particular, the binary adders and multipliers) are certainly reusable for different purposes, e.g., formal libraries for modular arithmetic or cryptography.

This study enabled us to discover various mistakes in prior MAA specifications. For instance, we corrected the test vectors 