Metadata-Version: 2.4
Name: sequent-verify
Version: 0.1.0
Summary: Neural Formal Verification Engine — GNN proposes, Z3 disposes
Author-email: Devang Pratap Singh <devangpratapsingh@outlook.com>
License-Expression: MIT
Project-URL: Homepage, https://github.com/devangpratapsingh/sequent
Project-URL: Repository, https://github.com/devangpratapsingh/sequent
Keywords: verification,formal-methods,gnn,z3,bug-detection,neurosymbolic
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Developers
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.9
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Topic :: Software Development :: Quality Assurance
Classifier: Topic :: Software Development :: Testing
Requires-Python: >=3.9
Description-Content-Type: text/markdown
Requires-Dist: torch>=2.0.0
Requires-Dist: torch-geometric>=2.4.0
Requires-Dist: z3-solver>=4.12.0
Requires-Dist: numpy>=1.24.0
Provides-Extra: server
Requires-Dist: fastapi>=0.104.0; extra == "server"
Requires-Dist: uvicorn>=0.24.0; extra == "server"
Requires-Dist: pydantic>=2.0.0; extra == "server"
Provides-Extra: dev
Requires-Dist: fastapi>=0.104.0; extra == "dev"
Requires-Dist: uvicorn>=0.24.0; extra == "dev"
Requires-Dist: pydantic>=2.0.0; extra == "dev"
Requires-Dist: scikit-learn>=1.3.0; extra == "dev"
Requires-Dist: matplotlib>=3.7.0; extra == "dev"
Requires-Dist: pytest>=7.0.0; extra == "dev"

```
                           _
 ___ ___ __ _ _  _ ___ _ _| |_
(_-</ -_) _` | || / -_) ' \  _|
/__/\___\__, |\_,_\___|_||_\__|
           |_|
```

**Neural Formal Verification Engine** — GNN proposes, Z3 disposes.

Sequent is a neurosymbolic Python debugger that **proves your code correct** — or finds the exact counterexample that breaks it.

## How it works

```
Python Source → AST Parser → GATv2 (10M params) → Bug Predictions
                          → Z3 SMT Solver       → Formal Proofs
                          → Consensus Vote       → Verdict + Counterexample
                          → Auto-Repair          → Re-Verify
```

1. **GNN proposes**: A GATv2 graph neural network reads your Python AST and predicts which nodes are likely bugs
2. **Z3 disposes**: The Z3 SMT solver formally verifies 8 property classes against your code
3. **Consensus**: Neural predictions are merged with formal proofs — both must agree
4. **Auto-repair**: If a bug is found, Sequent generates a fix and re-verifies it through Z3

## Install

```bash
pip install sequent
```

## Usage

```bash
# Verify a file
sequent check main.py

# Verify a specific function
sequent check main.py -f binary_search

# Auto-repair detected bugs
sequent check main.py --repair -v

# Export proof certificate
sequent check main.py --cert report.json

# JSON output for CI
sequent check main.py --json
```

## Example

```bash
$ sequent check test_buggy.py

  binary_search  ✗ BUG DETECTED  (42ms)
  ────────────────────────────────────────────────────────
  GNN  Buggy (87.3%)  12ms
       ⚑ Suspect lines: [4]
  Z3   ✗ counterexample  28ms
       ✗ loop_invariant: Loop uses '<' instead of '<=': misses case when low == high
         ↳ counterexample: {"low": "n", "high": "n"}
  ────────────────────────────────────────────────────────
  Consensus: BUG CONFIRMED: GNN detected bug and Z3 produced a formal counterexample.

  safe_divide  ✓ VERIFIED  (18ms)
  ────────────────────────────────────────────────────────
  Consensus: VERIFIED: Both GNN and Z3 agree — no bugs detected.
```

## Supported bug classes

| Bug Type | Description |
|----------|-------------|
| `off_by_one` | Loop bounds off by 1 (`<` vs `<=`) |
| `boundary_error` | Array/index out of bounds |
| `wrong_operator` | Incorrect comparison/arithmetic operators |
| `none_deref` | Missing null/None checks |
| `integer_overflow` | Unchecked arithmetic overflow |
| `missing_return` | Missing return in code path |
| `wrong_init` | Incorrect variable initialization |

## Z3 property checks

- Comparison consistency (off-by-one in loops)
- Array index bounds (upper and lower)
- None/null safety
- Return completeness
- Division by zero / arithmetic safety
- Loop termination and invariants
- Dead code detection

## Architecture

- **Model**: GATv2 with 8 attention heads, 256 hidden channels, 3 layers (~10M params)
- **Graph**: Code Property Graph (CPG) = AST + CFG + data flow
- **Features**: 91 AST node types + structural features (depth, subtree size, loop/conditional context)
- **Edges**: Parent↔child (AST) + control flow (CFG) + data flow (def → use)
- **Training**: Focal loss + NT-Xent contrastive loss with Z3 verification outcomes as supervision
- **Dataset**: 14,144 synthetic mutations from 164 seed functions, seed-level train/test split
- **Metrics**: 74.0% accuracy, 83.0% precision, 73.6% recall, 78.0% F1

## Web playground

```bash
# Start the API server
pip install sequent[server]
python -m backend.server

# Start the frontend (development)
cd frontend && npm install && npm run dev
```

## GitHub Action

```yaml
- uses: actions/setup-python@v5
  with:
    python-version: '3.11'
- run: pip install sequent
- run: sequent check src/ --ci --cert sequent-report.json
```

## License

MIT
