PlusCal is a high-level, algorithmic programming language designed to describe algorithms in a way that is both human-readable and suitable for formal verification. It was developed as part of the TLA+ (Temporal Logic of Actions) framework, which is a formal specification language used for describing and verifying the behavior of concurrent and distributed systems. PlusCal is designed to bridge the gap between informal algorithm descriptions and formal specifications.
New to topics? Read the docs here!