[foysavas]

> "specification of system behavior" sounds like a programming language to me

By "specification language" Lamport means one capable of verification via model checking.

In contrast, "programming languages" are not capable of such verification.