Comment by Kaizyn

Lamport isn't behind the P language, and it isn't as expressive as TLA+ so it isn't a replacement for his work in that area.