CakeML is a verified implementation of a significant subset of Standard ML.

See Also