> ## Documentation Index
> Fetch the complete documentation index at: https://docs.qwedai.tech/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>

<Info>
  **Updated in v7.0.0 (breaking).** The security-scanning path (`CodeVerifier` and `SecureCodeExecutor`, backing `POST /verify/code`) also returns `DiagnosticResult` now, and proven-unsafe code is reported as `VERIFIED` with a separate admission decision. See [Security scanning](#security-scanning-codeverifier) below and the [changelog](/changelog#v7-0-0-—-full-diagnosticresult-engine-conformance).
</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`.

***

## Security scanning (`CodeVerifier`)

Separate from symbolic execution, `CodeVerifier` scans code for security vulnerabilities using AST and pattern analysis. It backs [`POST /verify/code`](/api/endpoints#post-%2Fverify%2Fcode) and the `CODE` item type in batch verification. As of v7.0.0, `verify_code()`, `verify_python_deep()`, and `verify_batch()` return a `DiagnosticResult`.

### Status semantics: `VERIFIED` is truth, not admission

| Outcome | `status` | `developer_fields` | `proof_ref` |
| - | - | - | - |
| Safe code | `VERIFIED` | `is_valid: true`, `is_safe: true`, `constraint_id: "code_verifier.code_safe"` | Present |
| Unsafe code | `VERIFIED` (as-unsafe) | `is_valid: false`, `is_safe: false`, `critical_count`, `issues` | Present |
| Empty code or non-string `language` | `BLOCKED` | `constraint_id: "code_verifier.unsupported_language"` | `null` |
| Internal error | `BLOCKED` | `constraint_id: "code_verifier.execution_error"` | `null` |

Proving that a snippet is unsafe is a successful proof, so unsafe code is `VERIFIED`, never `BLOCKED`. `BLOCKED` is reserved for cases where verification itself failed, and blocked results carry no `proof_ref`.

<Warning>
  Never treat `status == "VERIFIED"` as "safe to execute". Admission is a separate decision: `POST /verify/code` attaches an explicit `admission` field (`ADMIT` or `BLOCKED`), and `developer_fields.is_valid` is the safety gate. Gate execution on `admission` or `is_valid`, not on `status`.
</Warning>

### Shell and process execution is never admitted

`CodeVerifier` reports any shell or process execution as a `CRITICAL` issue with type `process_execution`, so the snippet is unsafe (`is_valid: false`) and `POST /verify/code` returns `admission: BLOCKED`. This applies even when the command is a constant. The following calls are covered:

* `os.system`, `os.popen`, `os.startfile`
* The `os.exec*`, `os.spawn*`, and `os.posix_spawn*` families
* `subprocess.*`
* `pty.spawn`
* `asyncio.create_subprocess_*`

Calls made through an aliased import are detected too, for example `import subprocess as sp`, `from os import system as run_it`, or `from os import *`. `verify_code()`, `verify_python_deep()`, and `POST /verify/code` all apply this rule.

```python theme={null}
from qwed_new.core.code_verifier import CodeVerifier

code_verifier = CodeVerifier()
result = code_verifier.verify_code(
    "import subprocess as sp\nsp.run(['ls', '-la'])",
    language="python",
)
print(result.developer_fields["is_valid"])     # False
print(result.developer_fields["issues"])
# [{"severity": "CRITICAL", "type": "process_execution", ...}]
```

If generated code needs to run commands, route them through a reviewed, sandboxed tool instead.

<Note>
  Before v7.2.3, these calls were warnings and the code was admitted. See [GHSA-6rxr-gq43-694g](https://github.com/QWED-AI/qwed-verification/security/advisories/GHSA-6rxr-gq43-694g).
</Note>

### Hardcoded OpenAI keys

The code verifier flags hardcoded OpenAI API keys, including project-scoped (`sk-proj-`), service-account (`sk-svcacct-`), and admin (`sk-admin-`) keys as well as legacy `sk-` keys. Detection of the scoped formats was added in v7.2.3 ([GHSA-64xf-wffc-63fm](https://github.com/QWED-AI/qwed-verification/security/advisories/GHSA-64xf-wffc-63fm)).

### Batch verification

`verify_batch()` returns a single `DiagnosticResult` with per-item `verdicts`, a `summary` (`safe` / `unsafe` / `blocked` counts and `total_critical`), and an overall `is_valid`. `is_valid` is `true` only when **all** snippets are safe — a batch with any unsafe or blocked item is non-admissible.

### `SecureCodeExecutor` dangerous-pattern gate

`SecureCodeExecutor.execute()` no longer admits execution on the verifier verdict alone. It applies an unconditional OWASP LLM06 dangerous-pattern gate (`os.`, `sys.`, `subprocess`, `__import__`, `eval`, `exec`, `compile`, `open(`, `socket`, `urllib`, `requests`, `http`, and similar) and blocks execution with `CONSTRAINT_DANGEROUS_PATTERN`. The scan is AST-aware: it matches actual executable operations (imports, attribute access, calls), so dangerous keywords appearing only in comments, docstrings, or string literals do not cause false denials. The advisory-only fallback is retained only when verification itself fails closed.

***

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


## Related topics

- [Math engine](/engines/math.md)
- [Logic engine — Z3 SAT/SMT verification with QWED-Logic DSL](/engines/logic.md)
- [Verification engine tiers: Proof, Policy, Advisory](/engines/overview.md)
- [QWED-Agent specification v1.1](/specs/agent.md)
- [QWED GitHub Action](/advanced/github-action.md)


This documentation is built and hosted on [Mintlify](https://mintlify.com), a developer documentation platform.