Z is a FormalSpecification notation which can be automatically verified.
The notation is spelled "Z" and pronounced "zed", since it was created at Oxford and based on Zermelo-Fränkel SetTheory.
"zed", pronounced "zed", was also the stream editor on the IBM3084 mainframe at CambridgeUniversity in the 1980's. It was a lot like SedLanguage, including having a full-screen mode similar to vi. Some of the processing for my PhD thesis was done in zed.