The Leftpad function, implemented and proven correct in various different proof and programming languages.