Invar Logo

From AI-Generated
to AI-Engineered Code

Invar brings decades of software engineering best practices to AI‑assisted development.

Through automated verification, structured workflows, and proven design patterns, agents write code that's correct by construction—not by accident.

🤖 Dogfooding — Invar's code is 100% AI-generated and AI-verified using itself

The Approach

Not a validator that checks code after the fact—a methodology that guides agents to write better code from the start.

Without Invar

  • No specification — Agent guesses intent, misses edge cases
  • No feedback loop — Errors accumulate undetected
  • No workflow — Jumps to implementation, skips validation
  • No separation — I/O mixed with logic, untestable

With Invar

  • Contracts as spec — @pre/@post define exact boundaries
  • Multi-layer verification — Static + doctest + property + symbolic
  • USBV workflow — Understand → Specify → Build → Validate
  • Core/Shell split — Pure logic isolated, 100% testable

The key insight: process determines quality. When agents follow proven engineering practices, they produce code that meets specifications—verified automatically.

What It Looks Like

Agent workflow with Invar guidance

✓ Check-In: my-project | main | clean
━━ /develop → SPECIFY (2/4) ━━
# Agent defines contract before implementation
@pre(lambda principal, rate, years: principal > 0 and rate >= 0)
@post(lambda result: result >= principal)
def compound_interest(principal, rate, years): ...
━━ /develop → VALIDATE (4/4) ━━
$ invar guard --changed
WARN: missing doctest example (compound_interest)
# Agent fixes automatically, re-runs guard
$ invar guard --changed
Guard passed. (1 file, 0 errors)
✓ Final: guard PASS | 0 errors, 0 warnings

Get Started

One command to set up your project

cd your-project && uvx invar-tools init --claude

Enter your project directory first. uvx runs tools in an isolated environment. Add pip install invar-runtime for runtime contracts.

Claude Code

Full experience: Skills, MCP tools, sub-agent review

Cursor / Windsurf

Protocol document + CLI verification

Others

CLI commands work everywhere

Built On

Decades of research, one integrated workflow

Foundational Theory

1976 Symbolic Execution (King)
1986 Design by Contract (Meyer)
2000 Property-Based Testing (QuickCheck)
2012 Functional Core/Imperative Shell (Bernhardt)

AI Code Generation Research

2023 Clover — Closed-loop verification
2023 Parsel — Hierarchical decomposition
2023 Reflexion — Self-reflection on failures
2024 AlphaCodium — Flow engineering

Inspired By

Eiffel Dafny Idris Haskell