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

Get Started GitHub PyPI

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
✓ Check-In: my-project | main | clean
━━ /develop → SPECIFY (2/4) ━━
// Agent defines schema before implementation
const InterestInput = z.object({
principal: z.number().positive(),
rate: z.number().min(0),
years: z.number().int().positive()
});
function compoundInterest(input: InterestInput): number { ... }
━━ /develop → VALIDATE (4/4) ━━
$ npm run test
WARN: missing test case (compoundInterest)
// Agent adds tests, re-runs validation
$ npm run test
All tests passed. (3 tests)
✓ Final: tests PASS | 0 errors, 0 warnings

Get Started

One command to set up your project

cd your-project && uvx invar-tools init

Interactive mode — select your agent. Add pip install invar-runtime for runtime contracts.

✅ Claude Code

invar init --claude

✅ Pi

invar init --pi

🚧 Cursor / Other

In progress

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

Dependencies

deal returns CrossHair Hypothesis