Temporal Logic for JVM

Karat is a DSL to specify systems using linear temporal logic. From a single specification you can pursue two different avenues:

• Check the implementation against the model,
  • Using our integration with Kotest if you use Kotlin,
  • Or with our integration with Scalacheck if you use Scala;
• Verify properties of the model using our integration with Alloy.

The use of temporal logic to describe program properties has a long history. Some interesting pointers are:

• Quickstrom's Specification Language. Quickstrom is a tool for testing how a web application behaves when some events like clicking occur. It uses temporal logic to express the desired outcome.
• Formal Software Design with Alloy 6. Alloy is a tool for formal modeling and exploration of systems. In Alloy you use temporal logic to both describe the system and specify properties which should be verified.