I just saw this paper[1] which claims to have an implementation of
ChaCha20-Poly1305 in vectorised assembly using a method which
"deliver[s] formally verified vectorized implementations which
outperform the fastest non-verified code"

Is there any interest in using this for Zinc (it's my understanding[2]
that the ChaCha20 and Poly1305 code in Zinc is *not* formally verified)?
The repo is [3]. It looks like they don't have verified generic C
implementations unfortunately, but aren't there verified C versions in
HACL*?

[1]: https://arxiv.org/abs/1904.04606
[2]: https://marc.info/?l=linux-kernel&m=155405777331772&w=2
[3]: https://github.com/tfaoliveira/libjc

-- 
Aleksa Sarai
Senior Software Engineer (Containers)
SUSE Linux GmbH
<https://www.cyphar.com/>