Euclid Writes an Algorithm: A Fairytale.
Leslie Lamport · International Journal of Software and Informatics · 2011
This was an invited paper for a festschrift in honor of Manfred Broy’s 60th birthday. It’s a whimsical introduction to TLA+, including proofs. Judged as literature, it’s probably the best thing I have ever written.