O Quint é uma linguagem de especificação formal baseada no cálculo do TLA+, a lógica temporal de ações. Assim como o TLA+, ele foi projetado para ajudar a encontrar bugs sutis em sistemas complexos que envolvem concorrência. O diferencial do Quint em relação ao TLA+ está na sua legibilidade e na experiência da pessoa desenvolvedora. Ele possui uma sintaxe parecida com a do TypeScript, o que facilita a revisão de código, especialmente quando as especificações são geradas por agentes. Ele também vem com type checker, REPL e simulador, e pode ser instalado via npm. O simulador testa o modelo de forma leve usando execuções aleatórias e também consegue gerar traces a partir da especificação para testar a implementação real. Nossos times acharam a escolha entre Quint e TLA+ bem acirrada, ponderando o ecossistema de ferramentas do Quint contra a maturidade do TLA+. Esperamos que o seu desenvolvimento contínuo sinalize um ganho de tração para a verificação poliglota.
