Trust AI Code
Without Reading Every Line

You use AI to write code. Reading every line defeats the purpose.

Invar provides mechanical verification so you can trust AI output without manual review.

Get Started View on GitHub PyPI

What You Get

Invar handles mechanical correctness. You focus on business logic.

✓ Invar Verifies

• Contracts exist (boundaries were considered)
• Contracts aren't empty placeholders
• Doctests pass (behavior is proven)
• Pure logic has no I/O calls
• Code size limits respected

👤 You Judge

• Whether contracts match business requirements
• Whether edge cases are covered
• Whether the architecture is correct
• Whether to ship

Two Verification Levels

Zero decisions — default runs full verification

$ invar guard --static # STATIC: rules only (~0.5s, debugging)
✓ Static analysis passed
$ invar guard # STANDARD: rules + doctests + CrossHair + Hypothesis (default)
✓ Static analysis passed
✓ Doctests passed
✓ CrossHair verified (2 files)
✓ Hypothesis property tests passed
$ invar guard --coverage # Branch coverage (doctest + hypothesis)
✓ Overall: 91% branch coverage
# Default runs full verification — no decisions needed
# Incremental mode: only changed files (~5s first, ~2s cached)

The Six Laws

Principles that make AI code verifiable

1

Separation

Pure logic (Core) and I/O (Shell) must be physically separate

2

Contract Complete

Define COMPLETE boundaries that uniquely determine implementation

3

Context Economy

Read map → signatures → implementation (only if needed)

4

Decompose First

Break complex tasks into sub-functions before implementing

5

Verify Reflectively

If fail: Reflect (why?) → Fix → Verify again

6

Integrate Fully

Verify all feature paths connect; local correctness ≠ global correctness

The Workflow: USBV

AI follows this workflow for every task — depth varies naturally

U
Understand
→
S
Specify
→
B
Build
→
V
Validate

Example — You: "Add a function to calculate discounted price"

UnderstandCore function (pure logic), check existing patterns with invar sig
Specify@pre: price > 0, discount ∈ [0,1]. @post: result ≥ 0. Decompose if needed.
BuildWrite code with contracts and doctests
Validateinvar guard — Smart Guard runs static + doctests. Iterate if needed.
@pre(lambda price, discount: price > 0 and 0 <= discount <= 1) @post(lambda result: result >= 0) def discounted_price(price: float, discount: float) -> float: """ >>> discounted_price(100, 0.2) 80.0 """ return price * (1 - discount)

MCP Integration

First-class tools for AI agents

invar_guard
Smart Guard verification (static + doctests + coverage)
Replaces: pytest, crosshair, coverage
invar_sig
Show function signatures with @pre/@post contracts
Replaces: reading entire files
invar_map
Symbol map with reference counts
Replaces: grep for definitions

invar init creates .mcp.json automatically

Built on Proven Foundations

Every law is grounded in research

Classic Software Engineering
1990s
Functional Purity
Haskell IO monad: separate pure logic from effects
→ Law 1: Separation
1986
Design by Contract
Bertrand Meyer's Eiffel: @pre/@post as specification
→ Law 2: Contract Complete
1970s
Symbolic Execution
Prove correctness via constraint solving, not just test
→ Law 5: Verify
Classic
Integration Testing
Unit tests pass ≠ system works; verify end-to-end
→ Law 6: Integrate Fully
LLM Code Generation Research (2023)
Clover
Closed-Loop Verification
Verify correctness via code ↔ spec consistency checking
→ Law 2: Contract Complete
Lost in Middle
Context Efficiency
LLMs struggle with info buried in long contexts
→ Law 3: Context Economy
Parsel
Hierarchical Decomposition
Decompose → implement leaves → compose upward
→ Law 4: Decompose First
Reflexion
Self-Reflection
Reflect on failures, learn from mistakes, retry
→ Law 5: Verify Reflectively

Quick Start

1

Initialize

uvx invar-tools init --claude
2

Code with AI

AI follows USBV workflow
3

Verify

uvx invar-tools guard

No install required! uvx runs tools in isolated environment.

Experience Tiers

Claude Code
Full: Skills + MCP + Sub-agent review
Cursor/Windsurf
Basic: Protocol + CLI
Others
Minimal: CLI only

Workflow skills (/develop, /review) require Claude Code's sub-agent capabilities

Session Protocol

✓ Check-In: MyProject | main | clean
... development work ...
✓ Final: guard PASS | 0 errors, 2 warnings

Check-In shows context. Guard runs in VALIDATE phase and Final.