Metadata-Version: 2.5
Name: airtight-ai
Version: 0.1.0
Summary: Automated verification gate for AI-generated code. Ensures correctness through deterministic checks and cross-consistency validation.
Project-URL: Homepage, https://github.com/chempotharun/airtight-ai
Project-URL: Documentation, https://github.com/chempotharun/airtight-ai#readme
Project-URL: Repository, https://github.com/chempotharun/airtight-ai
Project-URL: Issues, https://github.com/chempotharun/airtight-ai/issues
Author-email: Arun Chempoth <chempoth.arun@gmail.com>
License-Expression: Apache-2.0
License-File: LICENSE
Keywords: ai,code-generation,formal-verification,testing,verification
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Developers
Classifier: License :: OSI Approved :: Apache Software License
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Programming Language :: Python :: 3.13
Classifier: Topic :: Software Development :: Quality Assurance
Classifier: Topic :: Software Development :: Testing
Requires-Python: >=3.10
Requires-Dist: hypothesis>=6.0
Provides-Extra: dev
Requires-Dist: mypy>=1.10; extra == 'dev'
Requires-Dist: pytest-cov>=5.0; extra == 'dev'
Requires-Dist: pytest>=8.0; extra == 'dev'
Requires-Dist: ruff>=0.5; extra == 'dev'
Provides-Extra: llm
Requires-Dist: anthropic>=0.30; extra == 'llm'
Requires-Dist: openai>=1.0; extra == 'llm'
Provides-Extra: smt
Requires-Dist: z3-solver>=4.12; extra == 'smt'
Description-Content-Type: text/markdown

# 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](https://arxiv.org/abs/2310.17807) 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).

```python
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.

| Approach | Catches syntax errors | Catches logic bugs | Catches spec violations | Guarantees soundness |
|---|---|---|---|---|
| Run and eyeball it | ✓ | Sometimes | No | No |
| Unit tests | ✓ | If you wrote the test | If you wrote the test | No |
| **Airtight** | ✓ | ✓ (property-based) | ✓ (formal spec) | **Yes** |

## Installation

```bash
pip install airtight-ai
```

With optional SMT solver support (Z3):
```bash
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:

```python
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

| Verdict | Meaning | Action |
|---|---|---|
| `full_pass` | All gates cleared | Ship it |
| `partial_pass` | Gate 1 passed, Gate 2+ failed | Requires human review |
| `hard_reject` | Gate 1 failed | Do not ship |

## 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](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
