Airtight

Automated verification gate for AI-generated code.

Airtight sits between any AI code generator and production. It ensures the generated code is correct through deterministic checks and cross-consistency validation — inspired by Stanford's Clover paradigm for closed-loop verifiable code generation.

The core guarantee: Airtight never approves incorrect code. It may reject correct code it can't verify (false negatives), but it will never let broken code through (zero false positives).

from airtight import verify, Spec

result = verify(
    code='def sort_desc(items): return sorted(items, reverse=True)',
    intent='Sort items in descending order',
    spec=Spec(
        requires='len(items) >= 0',
        ensures='all(result[i] >= result[i+1] for i in range(len(result)-1))',
        invariant='sorted(result, reverse=True) == result',
        test_inputs=[
            {'items': [3, 1, 2]},
            {'items': []},
        ],
    ),
)

print(result.verdict)       # "full_pass"
print(result.gates_passed)  # ["gate1_deterministic"]

Why Airtight?

AI code generators (Copilot, Claude, GPT) produce code that looks correct but often contains subtle bugs — wrong sort direction, missing edge cases, violated invariants. Testing catches some of these. Airtight catches them systematically.

Installation

pip install airtight-ai

With optional SMT solver support (Z3):

pip install airtight-ai[smt]

Architecture

Airtight is a four-gate verification pipeline. Each gate is independently sound — if any gate rejects the code, the code is definitively non-conformant with respect to that check.

AI Generator → Gate 1 (Deterministic) → Gate 2 (Cross-consistency) → Gate 3 (N-candidate) → Gate 4 (Behavioral) → Verified
                  ↓ reject                 ↓ reject                    ↓ reject               ↓ reject

Gate 1 — Deterministic checks (v0.1, current)

• Syntax parsing (AST)
• Property-based testing via Hypothesis
• Spec pre/postcondition and invariant checking
• No LLM involvement — mathematically sound

Gate 2 — Cross-consistency (planned v0.2)

• Six-way Clover consistency checks between intent, spec, and code
• Reconstruction testing: can spec regenerate equivalent code?
• Uses a different LLM than the generator to break shared blind spots

Gate 3 — N-candidate filter (planned v0.3)

• Generate N independent candidates
• Run Gates 1+2 on each, take first to pass
• Budget-bounded with convergence detection

Gate 4 — Behavioral equivalence (planned v0.4)

• Concolic testing and fuzzing
• I/O comparison against spec expectations

Termination guarantee

Airtight always terminates in bounded time. The Budget object controls:

from airtight import Budget

budget = Budget(
    max_candidates=10,     # Max independent generations (k-factor)
    retries_per_gate=3,    # Max feedback retries per gate
    plateau_window=3,      # Stop if score plateaus for 3 candidates
    same_error_limit=3,    # Stop if same error class recurs 3 times
)

Worst case: 10 × (3 + 6×3) = 210 LLM calls, then STOP. Convergence detection typically exits after 2-4 candidates.

Verdicts

Theoretical foundation

Airtight is grounded in two bodies of work:

1. Clover (Sun et al., Stanford 2024) — Closed-loop verifiable code generation via six-way consistency checking between code, formal annotations, and docstrings. Achieved 87% acceptance of correct code with zero false positives.

2. Automated reasoning (resolution, SMT solvers, term rewriting) — Provides the deterministic verification backbone. SMT constraints are decidable and sound. Property-based testing via Hypothesis provides probabilistic coverage with formal guarantees.

Contributing

Contributions welcome! See CONTRIBUTING.md for guidelines.

Key areas where help is needed:

• Gate 2 implementation — Clover-style cross-consistency checks
• Language support — Currently Python only; JavaScript/TypeScript next
• Spec DSL — A more ergonomic way to write specifications
• Benchmarks — Datasets of correct/incorrect AI-generated code

License

Apache 2.0