GitHub - informalsystems/quint: An executable specification language with delig...

Overview

Quint is a modern specification language that is a particularly good fit for distributed systems, such as blockchain protocols, distributed databases, and p2p protocols. Quint combines the robust theoretical basis of the Temporal Logic of Actions (TLA) with state-of-the-art type checking and development tooling.

Example code in Quint 🤶 🎁 🎅

Here is a small, partial, holiday special specification of the Secret Santa game:

module secret_santa {
  const participants: Set[str]

  /// get(recipient_for_santa, S) is the recipient for secret santa S
  var recipient_for_santa: str -> str

  /// the bowl of participants, containing a paper piece for each participant name
  var bowl: Set[str]

  val santas = recipient_for_santa.keys()
  val recipients = participants.map(p => get(recipient_for_santa, p))

  /// The initial state
  action init = all {
    recipient_for_santa' = Map(), // No santas or recipients
    bowl' = participants,         // Every participant's name in the bowl
  }

  action draw_recipient(santa: str): bool = {
    nondet recipient = oneOf(bowl)
    all {
      recipient_for_santa' = put(recipient_for_santa, santa, recipient),
      bowl' = bowl.exclude(Set(recipient)),
    }
  }

  action step = all {
    bowl.size() > 0,
    nondet next_santa = oneOf(participants.exclude(santas))
    draw_recipient(next_santa)
  }

  val everyone_gets_a_santa = (bowl.size() == 0).implies(participants == recipients)

  val no_person_is_self_santa = santas.forall(person =>
    get(recipient_for_santa, person) != person
  )

  val invariant = everyone_gets_a_santa and no_person_is_self_santa
}

module quint_team_secret_santa {
  import secret_santa(participants = Set("Gabriela", "Igor", "Jure", "Shon", "Thomas")).*
}

We can use this specification to check whether certain properties needed for a good game hold:

Checking if everyone gets a santa

echo '    true  '  .json
quint verify quint_team_secret_santa.qnt invarianteveryone_gets_a_santa apalache.json
ok No violation found 2119ms.
You may increase maxsteps.

Checking if no one gets themself

quint verify quint_team_secret_santa.qnt invariantno_person_is_self_santa
An example execution

State 

  quint_team_secret_santasecret_santabowl Set    
  quint_team_secret_santasecret_santarecipient_for_santa Map


State 

  quint_team_secret_santasecret_santabowl Set   
  quint_team_secret_santasecret_santarecipient_for_santa Map  


violation Found an issue 2047ms.
 found a counterexample

Features

A simple and familiar syntax to support engineers reading and writing specifications An expressive type system to ensure the domain model is coherent A novel effect system to ensure state updates are coherent IDE support via LSP giving real time feedback when writing specifications A REPL enabling interactive exploration of specifications A simulator enabling tests, trace generation, and exploration of your system A symbolic model checker to verify your specifications via Apalache

Motivation

Quint is inspired by TLA+ (the language) but provides an alternative surface syntax for specifying systems in TLA (the logic). The most important feature of our syntax is that it is minimal and regular, making Quint an easy target for advanced developer tooling and static analysis (see our design principles and previews of the tooling).

The syntax also aims to be familiar to engineers:

• At the lexical level, it borrows many principles from C-like languages.
• At the syntax level, it follows many principles found in functional languages.
• At the semantic level, Quint extends the standard programming paradigm with non-determinism and temporal formulas, which allow concise specification of protocol environments such as networks, faults, and time.

Thanks to its foundation in TLA and its alignment with TLA+, Quint comes with formal semantics built-in.

An example that highlights differences between Quint and TLA+

 Status  Working  Prepared  Committed  Aborted

const ResourceManagers Setstr
var statuses str  Status

 init  
  statuses'  ResourceManagers.mapBy_  Working


val canCommit bool  ResourceManagers.forallrm  statuses.getrm.inSetPrepared Committed
val notCommitted bool  ResourceManagers.forallrm  statuses.getrm  Committed

 preparerm  all 
  statuses.getrm  Working
  statuses'  statuses.setrm Prepared

 
 

         

        

          

         

     
                     = 

To learn more about Quint's motivation and design philosophy, watch this 15 minute presentation, delivered at Gateway to Cosmos in 2023.

Installation

1. Install the latest published version from npm:

   npm i @informalsystems/quint -g

2. Install IDE support for your editor:

3. Optionally, you may also install the VSCode plugin for visualizing traces.

Community

• Join the chat in the Quint zulip stream
• Join the Quint discussions on GitHub
• Contribute your spell to the collection of Quint spells
• Contribute to the development of Quint

Documentation

View the Quint documentation.

We aspire to having great, comprehensive documentation. At present, we have a good start, but still far to go. Please try what we have available and share with us any needs we have not yet been able to meet.

On "Quint"

Quint is short for 'quintessence', from alchemy, which refers to the fifth element. A lot of alchemy is about transmutation and energy, and Quint makes it possible to transmute specifications into executable assets and empower ideas to become referenced artifacts.

Acknowledgments

Quint has been designed and developed by the Apalache team: Gabriela Moreira, Igor Konnov, Jure Kukovec, Shon Feder, and Thomas Pani. ❤️

Thanks for notable contributions goes to Romain Ruetschi, Philip Offtermatt, Ivan Gavran, and, Ranadeep Biswas.

Quint is developed at Informal Systems.

Supported by the Vienna Business Agency.