https://github.com/informalsystems/quint Skip to content Toggle navigation Sign in * Product + Actions Automate any workflow + Packages Host and manage packages + Security Find and fix vulnerabilities + Codespaces Instant dev environments + Copilot Write better code with AI + Code review Manage code changes + Issues Plan and track work + Discussions Collaborate outside of code Explore + All features + Documentation + GitHub Skills + Blog * Solutions For + Enterprise + Teams + Startups + Education By Solution + CI/CD & Automation + DevOps + DevSecOps Resources + Learning Pathways + White papers, Ebooks, Webinars + Customer Stories + Partners * Open Source + GitHub Sponsors Fund open source developers + The ReadME Project GitHub community articles Repositories + Topics + Trending + Collections * Pricing Search or jump to... Search code, repositories, users, issues, pull requests... Search [ ] Clear Search syntax tips Provide feedback We read every piece of feedback, and take your input very seriously. [ ] [ ] Include my email address so I can be contacted Cancel Submit feedback Saved searches Use saved searches to filter your results more quickly Name [ ] Query [ ] To see all available qualifiers, see our documentation. Cancel Create saved search Sign in Sign up You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session. You switched accounts on another tab or window. Reload to refresh your session. Dismiss alert {{ message }} informalsystems / quint Public * Notifications * Fork 22 * Star 425 An executable specification language with delightful tooling based on the temporal logic of actions (TLA) License Apache-2.0 license 425 stars 22 forks Activity Star Notifications * Code * Issues 198 * Pull requests 5 * Discussions * Actions * Projects 0 * Wiki * Security * Insights Additional navigation options * Code * Issues * Pull requests * Discussions * Actions * Projects * Wiki * Security * Insights informalsystems/quint This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository. main Switch branches/tags [ ] Branches Tags Could not load branches Nothing to show {{ refName }} default View all branches Could not load tags Nothing to show {{ refName }} default View all tags Name already in use A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch? Cancel Create 40 branches 31 tags Code * Local * Codespaces * Clone HTTPS GitHub CLI [https://github.com/i] Use Git or checkout with SVN using the web URL. [gh repo clone inform] Work fast with our official CLI. Learn more about the CLI. * Open with GitHub Desktop * Download ZIP Sign In Required Please sign in to use Codespaces. Launching GitHub Desktop If nothing happens, download GitHub Desktop and try again. Launching GitHub Desktop If nothing happens, download GitHub Desktop and try again. Launching Xcode If nothing happens, download Xcode and try again. Launching Visual Studio Code Your codespace will open once ready. There was a problem preparing your codespace, please try again. Latest commit @bugarela bugarela Merge pull request #1318 from ekexium/fix-dead-link ... a4cac64 Dec 20, 2023 Merge pull request #1318 from ekexium/fix-dead-link doc: fix dead link in roadmap.md a4cac64 Git stats * 2,815 commits Files Permalink Failed to load latest commit information. Type Name Latest commit message Commit time .github Upgrade Github actions September 19, 2023 11:09 doc Merge branch 'main' into fix-dead-link December 20, 2023 09:53 editor-plugins Add nvim path to syntax file instructions September 28, 2023 09:42 examples Change the runtime behavior of then (#1304) December 13, 2023 11:10 logos Remove padding from logo December 15, 2023 16:25 quint introduce type defences (#1306) December 13, 2023 14:39 tutorials Move documentation links into doc/README.md December 14, 2023 17:32 vscode VSCode Release v0.12.2 December 19, 2023 06:31 .gitattributes Treat .qnt files as bluespec (#962) June 19, 2023 12:18 .gitignore ignore .DS_Store (#1251) November 17, 2023 10:47 CHANGELOG.md Change the runtime behavior of then (#1304) December 13, 2023 11:10 CONTRIBUTING.md Update ADR indexing December 15, 2023 16:32 LICENSE update the license file (#943) June 15, 2023 09:26 Makefile Make examples/README.md phony July 4, 2023 10:55 README.md Add link to secret santa wiki article December 19, 2023 12:25 View code [ ] Quint Lang Overview Example code in Quint Features Motivation Installation Community Documentation On "Quint" Acknowledgments README.md Quint Lang Logo Quint Lang Installation * Documentation * Community build badge Visual Studio Marketplace Version npm (scoped) 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 Quint (with the help of Apalache) can check to ensure that after the bowl is empty, every participant has a santa! No kids crying when the gifts are exchanged . echo '{ "checker": { "no-deadlocks": true } }' > config.json quint verify quint_team_secret_santa.qnt --invariant=everyone_gets_a_santa --apalache-config=config.json [ok] No violation found (2119ms). You may increase --max-steps. Checking if no one gets themself This specification has no safeguards against people being their own santa! Quint (with the help of Apalache) can easily find a minimal example where this happens. Sorry kids, I hope you don't mind buying your own present ! quint verify quint_team_secret_santa.qnt --invariant=no_person_is_self_santa An example execution: [State 0] { quint_team_secret_santa::secret_santa::bowl: Set("Gabriela", "Igor", "Jure", "Shon", "Thomas"), quint_team_secret_santa::secret_santa::recipient_for_santa: Map() } [State 1] { quint_team_secret_santa::secret_santa::bowl: Set("Igor", "Jure", "Shon", "Thomas"), quint_team_secret_santa::secret_santa::recipient_for_santa: Map("Gabriela" -> "Gabriela") } [violation] Found an issue (2047ms). error: 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^+ Quint: type Status = Working | Prepared | Committed | Aborted const ResourceManagers: Set[str] var statuses: str -> Status action init = { statuses' = ResourceManagers.mapBy(_ => Working) } val canCommit: bool = ResourceManagers.forall(rm => statuses.get(rm).in(Set(Prepared, Committed))) val notCommitted: bool = ResourceManagers.forall(rm => statuses.get(rm) != Committed) action prepare(rm) = all { statuses.get(rm) == Working, statuses' = statuses.set(rm, Prepared) } TLA^+: CONSTANT ResourceManagers VARIABLE statuses TCTypeOK == statuses \in [ResourceManagers -> {"working", "prepared", "committed", "aborted"}] TCInit == statuses = [rm \in ResourceManagers |-> "working"] canCommit == \A rm \in ResourceManagers : statuses[rm] \in {"prepared", "committed"} notCommitted == \A rm \in ResourceManagers : statuses[rm] # "committed" Prepare(rm) == /\ statuses[rm] = "working" /\ statuses' = [statuses EXCEPT ![rm] = "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: + VSCode + Emacs + Vim 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. Vienna Business Agency About An executable specification language with delightful tooling based on the temporal logic of actions (TLA) Topics language specification tlaplus quint apalache Resources Readme License Apache-2.0 license Activity Stars 425 stars Watchers 18 watching Forks 22 forks Report repository Releases 30 v0.17.1 Latest Dec 5, 2023 + 29 releases Contributors 17 * @bugarela * @shonfeder * @konnov * @thpani * @Kukovec * @romac * @lasarojc * @p-offtermatt * @ivan-gavran * @josef-widder * @rnbguy * @cason * @achamayou * @ekexium + 3 contributors Languages * TypeScript 70.4% * Java 13.2% * Bluespec 11.5% * JavaScript 2.0% * ANTLR 1.0% * Shell 0.5% * Other 1.4% Footer (c) 2023 GitHub, Inc. Footer navigation * Terms * Privacy * Security * Status * Docs * Contact * Manage cookies * Do not share my personal information You can't perform that action at this time.