Quint

This extension provides language support for Quint, the specification language.

Features

• Syntax Highlighting
• Diagnostics:
  • Syntax errors
  • Undefined and conflicting names
  • Type errors
  • Effect errors
  • Mode errors

New features are listed and discussed on this GitHub discussion.

Parse errors are highlighted in red, and hovering over the error will show the error message.

Hovering over an expression or definition will show its inferred type and effect.

Type errors are highlighted in red, and hovering over the error will show the error message, including unification errors.

Effects can help you quickly notice if you forgot to update a state variable or are trying to update the same variables more than one time. Effect errors are highlighted in red, and hovering over the error will show the error message.

Modes can help you maintain expectations regarding an operator. pure operators can't interact with the state, defs and vals can read the state (but not write), and only actions can update the state. Mode errors are highlighted in red, and hovering over the error will show the error message.

Requirements

There are no external requirements.

Known Issues

Issues are tracked on GitHub under the Fvscode tag.