Informal Systems says a Quint-plus-LLM workflow completed a core protocol change on Malachite — a production Byzantine Fault Tolerant consensus engine — in roughly one week, against an estimated several months by conventional methods. Engineer Gabriela Moreira published the case study, describing a four-step process that uses Quint executable specifications as guardrails for LLM-generated code changes. The argument: LLMs generate code efficiently but produce output that is hard to validate through review alone. <a href="/news/2026-03-14-codespeak-wants-to-replace-code-with-markdown-specs">Quint sits between natural language and implementation code</a> — abstract enough for human reasoning, mechanically verifiable through deterministic tooling including a simulator, a model checker backed by the Apalache TLA+ engine, and an interactive REPL. The workflow treats LLMs strictly as translators between specs and code, not as designers or correctness verifiers.
The demonstration centers on Malachite, which Circle — the company behind the USDC stablecoin — acquired to underpin its Arc blockchain. The specific change was migrating from classical Tendermint, which requires 3F+1 nodes to tolerate F Byzantine faults, to Fast Tendermint, a variant requiring 5F+1 nodes that eliminates one communication round. A critical prerequisite: the team already had an existing Quint spec for Tendermint written using their Choreo distributed-systems modeling framework. Two bugs in the English-language protocol description surfaced during a single afternoon of spec validation, before any code was written. Model-based testing via Quint Connect then verified that the Rust implementation matched the validated spec.
The approach offers a concrete answer to one of the <a href="/news/2026-03-14-ai-did-not-simplify-software-engineering">persistent problems in LLM-assisted engineering</a>: the gap between code that looks correct and code that is provably correct. Routing correctness guarantees through a deterministic model checker — rather than asking LLMs to self-verify — shifts that burden onto tooling that does not hallucinate. Informal Systems also announced the Quint LLM Kit, a set of AI agents and commands for generating and iterating on Quint specs. Reception on Hacker News was mixed. Commenters noted the post leans on sales-pitch framing while offering limited concrete technical detail, making independent evaluation of the methodology difficult. One pointed out that the fundamentals of reliable software — unit tests, integration tests, monitoring — remain unchanged regardless of AI tooling, a tension the post does not fully resolve.