Product Overview

Why are we building Quint?

We build Apalache in accordance with Informal Systems's conviction

that accessible specification languages, powerful solvers, and toolkits for integrating with modern software can transform our ability to build and maintain critical, trusted systems. We make formal methods technology more accessible by developing tools and processes to improve the quality and experience of software engineering.

Quint is a modern specification language that is a particularly good fit for distributed systems and blockchain protocols. It combines the robust theoretical basis of the Temporal Logic of Actions (TLA) with state-of-the-art static analysis and development tooling.