I was a bit surprised nobody’s tried a “verified” implementation in something like Coq/Idris/Agda (unless i missed one - I wasn’t familiar with all the languages in the list).

Might be a fun project!