Invariant

Invariant Verified Code generation page
Invariant homepage
Invariant new contract page
Invariant Verified Code architecture diagram
Invariant verified Cardano Contract architecture diagram

Invariant: Automated Formal Verification

Invariant is a system that automatically turns natural-language intent into machine-checked, formally verified programs. Its core thesis is simple: large language models, when paired with carefully designed formal representations and proof tooling, can be used to generate real software with machine-checked correctness guarantees

Inspiration

Billions of dollars have been lost due to correctness and security flaws in smart contracts and other safety-critical code, particularly in DeFi, financial infrastructure and systems programming. Despite the severity and irreversibility of these failures, most production systems still rely on testing, audits, and informal reasoning rather than machine-checked proofs.

At the same time, recent advances in automated theorem proving have shown that formal proof systems are no longer purely academic. Systems such as Harmonic's Aristotle have demonstrated the ability to solve novel mathematical problems, indicating that tools like Lean can now support substantial, real-world reasoning rather than just verification of hand-written proofs.

In parallel, practical systems like AWS Cedar have shown that translation-based formal approaches can successfully underpin real production infrastructure, pairing executable implementations with machine-checked semantic models. This work strongly influenced our thinking beyond smart contracts.

With prior experience formalizing mathematics in Lean, including contributions to DeepMind’s Formal Conjectures repository, we saw an opportunity to connect these threads: use modern LLMs not merely to assist programmers, but to automatically generate programs together with formal correctness guarantees, closing the gap between informal intent and provably correct execution.

What Invariant Does

Invariant takes informal intent and produces formally verified code with precise correctness guarantees and concrete counterexamples when properties fail. The workflow for smart contracts proceeds as follows:

Confirm user intent and produce an informal specification of desired behavior.
Draft a contract in a high-level Haskell DSL.
Compile the DSL into a Lean embedding of the semantics.
Express safety and liveness properties in a domain-specific logic (e.g., “a seller cannot lose collateral unless the buyer pays the strike price”).
Extract all feasible execution paths, prune them with SMT via Z3, and search for counterexamples.
For properties beyond SMT’s reach, discharge them with Lean proofs.
Produce a machine-checked report stating exactly which properties were proved, which failed, and precise counterexample traces when failures occur, presenting users the option to refine the contract specification with these traces in mind.

To illustrate: Invariant can take a standard financial contract (e.g., a fixed-rate loan) specified in plain English, generate its executable Marlowe code, and then formally prove properties such as no unintended loss of principal, correct interest accrual over time, and proper settlement on maturity. All proofs and counterexamples appear in the final verification report.

Proof of Generality: Dual Verification Pipelines

In addition to the semantic embedding pipeline for smart contracts, Invariant includes a translation-based verification pipeline inspired by AWS Cedar. Instead of embedding Marlowe JSON directly, this pipeline generates C implementations, translates them into Lean, proves correctness properties using Aristotle, and performs differential testing between the C code and its Lean model. This dual design serves as evidence that the approach applies beyond smart contracts, making it a candidate architecture for broader classes of software.

Accomplishments

Invariant delivers a working, end-to-end system capable of generating machine-checked verification artifacts without human intervention. Key achievements include:

Successfully formalizing and verifying all 18 standard ACTUS financial contract types, including loans, options, swaps, and structured products, in a single pass through the pipeline. (Learn more)
Building a reusable Lean embedding and verification DSL that supports rich safety and liveness guarantees.
Demonstrating two distinct automated verification approaches: semantic embedding and translation-based proof with differential testing.
Deploying the full pipeline on AWS with containerized services coordinating generation, compilation, and verification.
Successfully formalizing and verifying solutions to Leetcode hard programming problems, including "44. Wildcard Matching."

Challenges and Lessons

Invariant’s development surfaced two major challenges:

Reliability of LLM generation: Small prompt changes lead to large semantic differences in output. Achieving structural and semantic consistency required extensive prompt engineering and intermediate representations.
Scalability of verification: Even though Marlowe contracts are finite, the number of execution paths can grow combinatorially. Effective SMT pruning and caching were essential to keep verification tractable.

We also learned that many correctness properties in financial smart contracts are left informal in traditional workflows, and that formal methods paired with LLMs can make formal verification a practical default rather than a costly afterthought.

What’s Next

Future work includes improving SMT performance for larger contracts, integrating with the Marlowe runtime for automated deployment of verified contracts, and expanding the approach into other safety-critical domains. A longer-term goal is automated specification discovery, closing the loop from intent, to code, to proof, and ultimately to deployment.