• Executable: Quint has checked names and types and is executable. It can handle both English and Markdown. In contrast, some other specification languages are not checked and not executable.
• Abstract: Specification Languages focus only on what you care about, while Programming Languages define in detail how things happen.
• Modern: Quint has a familiar syntax and can be used with the CLI and your editor. Existing specification languages have a more math-y syntax and old GUI tools.
• Example: In the bank.qnt code, it defines a state variable balances to store account balances. There is an action withdraw to decrement the balance but forgets to check for enough balance. There is also an invariant no_negatives to ensure account balances are never negative. When running quint run bank.qnt --invariant=no_negatives, an example execution shows that the invariant is violated.