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.

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