> ## Documentation Index
> Fetch the complete documentation index at: https://qwed-ai-mintlify-cfa51465.mintlify.site/llms.txt
> Use this file to discover all available pages before exploring further.

# Code engine

> QWED Code engine reference: CrossHair symbolic execution for Python contracts, safety checks, and bounded model checking with DiagnosticResult output.

<Info>
  **Updated in v5.3.0 (breaking).** Every `SymbolicVerifier` public method now returns a [`DiagnosticResult`](/advanced/diagnostics) instead of an ad-hoc dict. See the [migration section](#migrating-from-the-legacy-dict-api) for a field-by-field mapping. The Code Engine is the first fully `DiagnosticResult`-conformant engine and serves as the reference implementation for future engine migrations.
</Info>

The Code Engine uses [CrossHair](https://github.com/pschanely/crosshair), a symbolic execution tool for Python, to verify code properties without running it.

***

## Capabilities

| Feature                    | Description                                           |
| -------------------------- | ----------------------------------------------------- |
| **Symbolic verification**  | CrossHair-driven property checking on typed functions |
| **Contract verification**  | Precondition and postcondition assertions             |
| **Safety analysis**        | Division-by-zero and index-out-of-bounds hazards      |
| **Bounded model checking** | Verify under explicit loop and recursion bounds       |
| **Complexity analysis**    | Loops, recursions, and path-budget estimates          |

***

## Quick start

```python theme={null}
from qwed_new.core.symbolic_verifier import SymbolicVerifier

verifier = SymbolicVerifier()

code = """
def divide(a: int, b: int) -> float:
    return a / b
"""

result = verifier.verify_code(code)
print(result.status)               # DiagnosticStatus.UNVERIFIABLE
print(result.is_verified)          # False
print(result.agent_message)        # "Symbolic verification found a counterexample..."
print(result.developer_fields["constraint_id"])
# "symbolic_verifier.counterexample_found"
```

Every method on `SymbolicVerifier` returns a `DiagnosticResult` with the same three layers described in [Verification Diagnostics](/advanced/diagnostics): a Layer 1 `agent_message`, a Layer 2 `developer_fields` dict, and a Layer 3 `proof_ref` (always `None` for this engine — see [Why `VERIFIED` is never emitted](#why-verified-is-never-emitted)).

***

## The `DiagnosticResult` contract

All six public methods — `verify_code`, `verify_function_contract`, `verify_safety_properties`, `verify_bounded`, `analyze_complexity`, `get_verification_budget` — return a `DiagnosticResult`.

### Status values

| `result.status`                 | Meaning                                                                             |
| ------------------------------- | ----------------------------------------------------------------------------------- |
| `DiagnosticStatus.VERIFIED`     | **Never emitted by this engine.** See [below](#why-verified-is-never-emitted).      |
| `DiagnosticStatus.UNVERIFIABLE` | Analysis ran but proof was incomplete, timed out, or found a counterexample.        |
| `DiagnosticStatus.BLOCKED`      | Verification could not be attempted (parse error, no functions, CrossHair missing). |

Read the specific reason from `result.developer_fields["constraint_id"]`.

### Common `developer_fields` keys

Every result carries `verification_mode` so callers can tell a plain symbolic run from a bounded run:

| Key                 | Type   | Description                                                                                        |
| ------------------- | ------ | -------------------------------------------------------------------------------------------------- |
| `constraint_id`     | string | Structured reason code, e.g. `symbolic_verifier.counterexample_found`.                             |
| `verification_mode` | string | `"symbolic"` for standard runs, `"bounded_symbolic"` for `verify_bounded()`.                       |
| `advisory_checks`   | array  | Non-proof-bearing analysis attached for developer or auditor review. Never influences the verdict. |

Method-specific keys (function counts, loop lists, budget estimates) are documented in the sections below.

### Why `VERIFIED` is never emitted

CrossHair's search is timeout-bounded, not a completeness proof. "No counterexample found" is not the same as "no counterexample exists," so a clean run maps to `UNVERIFIABLE` with `constraint_id = "symbolic_verifier.no_counterexample_found"` — never to `VERIFIED`. The `DiagnosticResult` contract structurally requires a `proof_ref` for `VERIFIED`, and this engine has no proof artifact to bind.

Downstream policy gates must reject `UNVERIFIABLE` results for control flow. Treat symbolic-execution output as a bug hunter, not an authority.

***

## Symbolic verification

`verify_code()` walks the AST, extracts every function with type annotations, and runs CrossHair on each one.

```python theme={null}
result = verifier.verify_code(code)

if result.is_verified:
    ...  # Never happens for this engine — see above
else:
    reason = result.developer_fields["constraint_id"]
    checked = result.developer_fields["functions_checked"]
    verified = result.developer_fields["functions_verified"]
    issues = result.developer_fields["issues"]
```

`developer_fields` on `verify_code()` results:

| Key                      | Description                                                            |
| ------------------------ | ---------------------------------------------------------------------- |
| `functions_discovered`   | Total functions found in the source.                                   |
| `functions_checked`      | Functions actually submitted to CrossHair.                             |
| `functions_verified`     | Functions CrossHair proved (no counterexample and no timeout).         |
| `functions_skipped`      | Functions with no type annotations.                                    |
| `functions_unverifiable` | Functions that could not be proven (skipped, timed out, or errored).   |
| `counterexamples_found`  | Count of counterexample issues reported by CrossHair.                  |
| `timeouts_found`         | Count of timeout issues.                                               |
| `issues`                 | Per-function issue records with `type`, `function`, and `description`. |

<Warning>
  `verify_code()` no longer accepts `check_assertions` — the parameter was never wired up. The current signature is `verify_code(self, code: str) -> DiagnosticResult`. Passing extra keyword arguments raises `TypeError`.
</Warning>

### Counterexample: division by zero

```python theme={null}
result = verifier.verify_code("""
def divide(a: int, b: int) -> float:
    return a / b
""")

result.status                                        # DiagnosticStatus.UNVERIFIABLE
result.developer_fields["constraint_id"]             # "symbolic_verifier.counterexample_found"
result.developer_fields["counterexamples_found"]     # 1
result.developer_fields["issues"][0]["type"]         # "counterexample"
```

### Untyped function: fails closed

CrossHair requires type hints. Untyped functions are reported as skipped and unverifiable — the result cannot be `is_verified: True`.

```python theme={null}
result = verifier.verify_code("""
def add(a, b):
    return a + b
""")

result.developer_fields["constraint_id"]         # "symbolic_verifier.no_typed_functions"
result.developer_fields["functions_discovered"]  # 1
result.developer_fields["functions_checked"]     # 0
result.developer_fields["functions_skipped"]     # 1
```

See [Symbolic execution limits](/advanced/symbolic-limits) for the full fail-closed matrix.

***

## Contract verification

`verify_function_contract()` injects preconditions as `assert` statements and re-runs `verify_code()` against the decorated source.

```python theme={null}
result = verifier.verify_function_contract(
    code="""
def sqrt(x: float) -> float:
    return x ** 0.5
""",
    function_name="sqrt",
    preconditions=["x >= 0"],
    postconditions=["__return__ >= 0"],
)
```

The returned `DiagnosticResult` follows the same shape as `verify_code()`. Read `result.developer_fields["issues"]` to find failing assertions.

***

## Safety property analysis

`verify_safety_properties()` scans the AST for division-by-zero and index-out-of-bounds hazards. It always returns `UNVERIFIABLE` (the check is advisory and does not prove the code is safe) with structured details in `developer_fields`.

```python theme={null}
result = verifier.verify_safety_properties("""
def divide(a: int, b: int) -> float:
    return a / b
""")

result.developer_fields["is_safe"]              # False
result.developer_fields["warnings"]             # 1
result.developer_fields["errors"]               # 0
result.developer_fields["issues"][0]["type"]    # "potential_division_by_zero"
```

The `advisory_checks` array carries a `safety_properties` entry with the same summary counts.

***

## Bounded model checking

`verify_bounded()` transforms the source to inject loop counters and recursion-depth checks, then calls `verify_code()` on the rewritten source. Every result from this method sets `verification_mode = "bounded_symbolic"` and includes the applied bounds plus the underlying complexity analysis.

```python theme={null}
result = verifier.verify_bounded(
    code=code,
    loop_bound=50,
    recursion_depth=20,
)

result.developer_fields["verification_mode"]     # "bounded_symbolic"
result.developer_fields["bounds_applied"]        # {"loop_bound": 50, "recursion_depth": 20, "prioritized": True}
result.developer_fields["complexity_analysis"]   # {"loops": [...], "recursions": [...], ...}
```

If the bounded-model transform itself fails, `verify_bounded()` returns `BLOCKED` with `constraint_id = "symbolic_verifier.bounds_transform_error"` instead of silently falling back to the untransformed source.

See [Bounded model checking](/advanced/symbolic-limits#bounded-model-checking) for configuration guidance and preset budgets.

***

## Complexity analysis

`analyze_complexity()` counts loops, direct and mutual recursions, and maximum loop-nesting depth. The result is always `UNVERIFIABLE` — the analysis is advisory and produces no proof.

```python theme={null}
result = verifier.analyze_complexity("""
def bubble_sort(arr: List[int]) -> List[int]:
    n = len(arr)
    for i in range(n):
        for j in range(n - 1):
            if arr[j] > arr[j + 1]:
                arr[j], arr[j + 1] = arr[j + 1], arr[j]
    return arr
""")

result.developer_fields["total_loops"]              # 2
result.developer_fields["max_loop_depth"]           # 2
result.developer_fields["total_recursive_functions"] # 0
result.developer_fields["complexity_score"]         # 4
result.developer_fields["recommendation"]["risk_level"] # "medium"
```

Use `recommendation` to pick sensible bounds for a follow-up `verify_bounded()` call.

***

## Verification budget

`get_verification_budget()` estimates the number of symbolic paths CrossHair would explore, so callers can decide whether to attempt verification or fall back to a cheaper check.

```python theme={null}
result = verifier.get_verification_budget(code, max_paths=1000)

result.developer_fields["estimated_paths"]    # e.g. 200
result.developer_fields["max_paths"]          # 1000
result.developer_fields["feasible"]           # True
```

Both this method and `analyze_complexity()` are advisory — treat their output as heuristics, not proof. The result carries an `advisory_checks` entry with the same summary details.

***

## Migrating from the legacy dict API

Before v5.3.0, `SymbolicVerifier` methods returned ad-hoc dicts (`result.verified`, `result["issues"]`, `result["complexity"]`, and so on). v5.3.0 removes those return types entirely — every method now returns a `DiagnosticResult`. Update your call sites using the map below.

### Field cheat sheet

| Legacy field                                            | Replacement                                                                                      |
| ------------------------------------------------------- | ------------------------------------------------------------------------------------------------ |
| `result.verified`                                       | `result.is_verified` (always `False` for this engine)                                            |
| `result["status"]` (string)                             | `result.status` (`DiagnosticStatus` enum) and `developer_fields["constraint_id"]`                |
| `result["message"]`                                     | `result.agent_message`                                                                           |
| `result["issues"]`                                      | `result.developer_fields["issues"]`                                                              |
| `result["functions_checked"]`                           | `result.developer_fields["functions_checked"]`                                                   |
| `result["complexity"]` / `"loop_depth"` / `"recursive"` | `result.developer_fields["complexity_score"]`, `"max_loop_depth"`, `"total_recursive_functions"` |
| `result["is_safe"]`                                     | `result.developer_fields["is_safe"]`                                                             |
| `result["bounds_applied"]`                              | `result.developer_fields["bounds_applied"]`                                                      |
| n/a                                                     | `result.developer_fields["verification_mode"]` — new, `"symbolic"` or `"bounded_symbolic"`       |
| n/a                                                     | `result.proof_ref` — always `None` for this engine                                               |

### Before

```python theme={null}
result = verifier.verify_code(code)

if result["status"] == "verified":
    admit(payload)
elif result["status"] == "counterexamples_found":
    for issue in result["issues"]:
        log(issue["description"])
else:
    reject(payload, reason=result["message"])
```

### After

```python theme={null}
from qwed_new.core.diagnostics import DiagnosticStatus

result = verifier.verify_code(code)

# This engine never emits VERIFIED — treat every result as unverified for
# control flow, and use developer_fields for the specific reason.
reject(payload, reason=result.agent_message)

if result.status is DiagnosticStatus.UNVERIFIABLE:
    reason = result.developer_fields["constraint_id"]
    if reason == "symbolic_verifier.counterexample_found":
        for issue in result.developer_fields["issues"]:
            log(issue["description"])
```

<Warning>
  Do not gate control flow on `is_verified` for symbolic-engine results — it is always `False`. Downstream authority checks must inspect `result.proof_ref`, which this engine intentionally leaves as `None`. See [Verification Diagnostics](/advanced/diagnostics) for the full 3-layer contract.
</Warning>

### Removed parameters

* `verify_code(code, check_assertions=...)` — the parameter was never used. Remove it from your call sites; passing it now raises `TypeError`.

***

## Language support

| Language   | Support level  |
| ---------- | -------------- |
| Python     | Full           |
| JavaScript | Basic (coming) |
| TypeScript | Basic (coming) |
| SQL        | Via SQL Engine |

***

## Next steps

* [Verification Diagnostics](/advanced/diagnostics) — the `DiagnosticResult` contract in depth
* [Symbolic execution limits](/advanced/symbolic-limits) — when CrossHair works, when it doesn't, and how to bound it
* [SQL engine](./sql) — verify SQL queries
* [Logic engine](./logic) — verify logical constraints