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

> [!NOTE]
>
> **Updated in v5.3.0 (breaking).** Every `SymbolicVerifier` public method now returns a [`DiagnosticResult`](https://docs.qwedai.tech/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.

> [!NOTE]
>
> **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](https://docs.qwedai.tech/changelog.md#v7-0-0-—-full-diagnosticresult-engine-conformance).

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

> [!WARNING]
>
> CrossHair imports the module it analyzes, which runs that module's top-level code. QWED runs CrossHair only inside a hardened Docker container and never on the host. Without Docker or the sandbox image, `verify_code()` returns `BLOCKED` with `constraint_id = "symbolic_verifier.runtime_unavailable"`. See [Docker sandbox requirement](https://docs.qwedai.tech/advanced/symbolic-limits.md#docker-sandbox-requirement).

***

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

***

## Prerequisites

Install the symbolic extra, which includes CrossHair and the `docker` client, then build the sandbox image from a qwed-verification checkout:

```bash theme={null}
pip install "qwed[symbolic]"
docker build -t qwed-crosshair-sandbox:0.0.101 docker/crosshair-sandbox
```

The image is built from `docker/crosshair-sandbox/Dockerfile`. QWED never pulls it at runtime. Set `QWED_CROSSHAIR_IMAGE` to use a different tag.

## 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](https://docs.qwedai.tech/advanced/diagnostics.md): 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, code over 120 KiB, Docker sandbox unavailable). |

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 inside the Docker sandbox. QWED addresses each function by module qualname (`target.func` or `target.Class.method`). Functions nested inside other functions can't be loaded by name and are reported as unverifiable.

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

### 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](https://docs.qwedai.tech/advanced/symbolic-limits.md) 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](https://docs.qwedai.tech/advanced/symbolic-limits.md#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](https://docs.qwedai.tech/advanced/diagnostics.md) for the full 3-layer contract.

### 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`](https://docs.qwedai.tech/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` |
| Python that does not parse | `BLOCKED` | `constraint_id: "code_verifier.parse_error"` | `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`.

### 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
* `os.fork`, `os.forkpty`, and `pty.fork`
* `subprocess.*`
* `pty.spawn`
* `asyncio.create_subprocess_*`
* Dynamic import and execution: `importlib.import_module`, `importlib.__import__`, `runpy.run_module`, and `runpy.run_path`
* Native library loaders: `ctypes.CDLL`, `ctypes.cdll`, `ctypes.WinDLL`, `ctypes.windll`, `ctypes.OleDLL`, `ctypes.oledll`, and `ctypes.PyDLL`
* Any call on the raw OS backend modules `posix` and `nt`

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, shell and subprocess 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). Before v7.3.0, `fork`, dynamic import, `ctypes` loaders, `posix`/`nt`, and file and network access were warnings or undetected and the code was admitted. See [GHSA-4phf-6h72-9xfg](https://github.com/QWED-AI/qwed-verification/security/advisories/GHSA-4phf-6h72-9xfg).

### `eval`, `exec`, and `compile` are matched as names

`CodeVerifier` reports `eval`, `exec`, `compile`, `__import__`, `getattr`, and `setattr` as a `CRITICAL` issue with type `dangerous_function`. The verifier matches these names on the Python AST, not as substrings of a line. Longer identifiers that only contain them are not flagged, except that any line containing `__import__` is still reported as `dangerous_attribute`. Common safe calls are admitted:

* `cur.execute("SELECT ?", params)`, which is parameterised SQL
* `model.evaluate(x, y)` and `model.evaluate(ds, verbose=0)`
* `re.compile(r"[0-9]+")` in a snippet that has `import re`. Without the import in the snippet, `re.compile` is refused, because the verifier can't tell that `re` is the standard module
* `compile_report()`, and the names inside longer words in strings and comments, such as `"executing job"`

The matching is still strict where a name can reach the builtin another way. The verifier refuses the names when used as a value (`f = eval`), as a keyword argument, as a parameter or function name, in an import, as an attribute, or as a whole identifier in a string. It also follows names built from literals with `+` or `%`, such as `"ex" + "ec"`. It doesn't follow names built with `join` or `chr`. Longer helpers that run code or start a process, such as `exec_module` and the `os.exec*` family, stay refused. `model.eval()`, `model.evaluate(x)`, and `model.evaluate()` stay refused too. `ast.literal_eval` is admitted.

```python theme={null}
result = code_verifier.verify_code(
    "cur.execute('SELECT * FROM users WHERE id = ?', (user_id,))",
    language="python",
)
print(result.developer_fields["is_valid"])     # True

result = code_verifier.verify_code("f = eval\nf(user_input)", language="python")
print(result.developer_fields["is_valid"])     # False
print(result.developer_fields["issues"])
# [{"severity": "CRITICAL", "type": "dangerous_function", ...},
#  {"severity": "CRITICAL", "type": "builtin_not_admitted", ...}]   # second issue from v9.1.0
```

Python that does not parse is `BLOCKED` with `constraint_id: "code_verifier.parse_error"`, because the AST checks cannot run on it.

> [!NOTE]
>
> Before v9.0.0, the verifier matched these names anywhere in a line, so `cur.execute(...)`, `model.evaluate(...)`, and `re.compile(...)` were refused as `dangerous_function`. Python that did not parse was reported safe unless a line matched one of the patterns.

### File and network access is never admitted

`CodeVerifier` reports file system and network I/O that the code itself calls as a `CRITICAL` issue with type `file_or_network_access`, so the snippet is unsafe (`is_valid: false`) and `POST /verify/code` returns `admission: BLOCKED`. The following are covered, including through aliased imports:

* The bare `open()` builtin and `io.open`
* `shutil.*`, `pathlib.Path`, and file-mutating `os` calls such as `os.remove`, `os.rename`, `os.mkdir`, `os.chmod`, and `os.open`
* `socket.socket`, `socket.create_connection`, and `socket.create_server`
* `urllib.request`, `http.client`, `requests.*`, `httpx.*`, `aiohttp.*`, and `asyncio.open_connection`
* `ftplib`, `smtplib`, `telnetlib`, `poplib`, and `imaplib`

This check doesn't flag `os.path.*`. The string helpers such as `os.path.join` and `os.path.basename` are admitted. From v9.1.0, the `os.path` functions that read the file system, such as `os.path.exists`, `os.path.isfile` and `os.path.getsize`, are refused by the allowlist (`attribute_not_admitted`); see [Only listed modules, builtins and attributes are admitted](#only-listed-modules-builtins-and-attributes-are-admitted).

```python theme={null}
result = code_verifier.verify_code(
    "data = open('/etc/passwd').read()",
    language="python",
)
print(result.developer_fields["is_valid"])     # False
# [{"severity": "CRITICAL", "type": "file_or_network_access", ...}]
```

These checks cover calls the code makes by name. They don't see the objects your executor puts in the code's namespace: see the note under [Only listed modules, builtins and attributes are admitted](#only-listed-modules-builtins-and-attributes-are-admitted). If generated code needs to read files or call the network, route that I/O through a reviewed, sandboxed tool.

### Only listed modules, builtins and attributes are admitted

> [!NOTE]
>
> Changed in v9.1.0 ([GHSA-9r7q-mx75-hcj7](https://github.com/QWED-AI/qwed-verification/security/advisories/GHSA-9r7q-mx75-hcj7))

`CodeVerifier` admits Python code only when everything it uses is on QWED's lists. Lists of dangerous calls can't be complete: before v9.1.0, code that used `io.FileIO`, `urllib3`, `pickle.Unpickler`, `multiprocessing` or `os.environ` was `VERIFIED · ADMIT`. Python code is now admitted only when all of the following hold:

* Every module it imports, and every name it uses from that module, is on the list. The list holds standard-library modules that compute without files, the network, processes, the environment or the import system, such as `math`, `json`, `re`, `datetime`, `decimal`, `collections` and `itertools`. Third-party modules, such as `numpy`, `pandas` and `requests`, are not admitted, and nor are `asyncio`, `logging`, `subprocess`, `importlib` or `pathlib`. An import is refused even if the code calls nothing from the module.
* Every builtin it reads is listed. A read of `open`, `eval`, `exec`, `compile`, `__import__`, `vars`, `globals`, `locals`, `getattr`, `setattr`, `delattr`, `help`, `license`, `credits`, `copyright`, `breakpoint`, `memoryview` or `__build_class__` is refused, also where the name is the code's own variable or parameter. Rename the variable, for example to `help_text`. `print`, `input`, `exit` and `quit` are admitted.
* Every special attribute (`__x__`) it uses is listed. The protocol methods, such as `__init__`, `__len__` and `__eq__`, and plain data, such as `__name__` and `__doc__`, are listed. Attributes such as `__func__`, `__wrapped__`, `__get__`, `__getstate__`, `__reduce__`, `__dict__` and `__class__` are refused.
* It reads no attribute's value by a name made at run time. `hasattr(obj, name)` is admitted: it only answers whether the attribute exists, although the lookup can run a property. `.format` and `.format_map` need a template written in the code with no attribute in a field, such as `"{} items".format(n)`. Use an f-string otherwise. A class pattern with positional parts, such as `case Point(x, y)`, needs a class whose `__match_args__` is fixed.
* It uses no module as a value (`m = json`), writes to no module (`json.dumps = f`), and reads no frame or traceback.

Admission checks the code's text, not the objects your executor puts in its namespace. A name the code uses but doesn't define, such as `f` in `f("/etc/passwd")`, isn't checked, so if your executor binds `f` to `open`, admitted code can read files. Expose only the objects and callables the code needs.

Each refusal is a `CRITICAL` issue that names the module, builtin or attribute in its `pattern`. The issue `type` is one of `module_not_admitted`, `attribute_not_admitted`, `module_reference`, `module_write`, `builtin_not_admitted`, `special_attribute`, `frame_introspection` or `dynamic_lookup`.

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

code_verifier = CodeVerifier()
result = code_verifier.verify_code("import numpy as np\nprint(np.mean([1, 2, 3]))", language="python")
print(result.developer_fields["is_valid"])     # False
# [{"severity": "CRITICAL", "type": "module_not_admitted", "pattern": "numpy", ...}]

result = code_verifier.verify_code("import math\nprint(math.sqrt(16))", language="python")
print(result.developer_fields["is_valid"])     # True
```

> [!WARNING]
>
> **Upgrading to v9.1.0.** `POST /verify/code`, `QWEDLocal.verify_code` and the CLI can refuse code that v9.0.0 admitted. Read the issues on the result: each one names what to remove or replace.

#### Trusted modules

`CodeVerifier(trusted_modules=...)` takes top-level module names that your own runtime confines, such as a sandbox with its own import guard. Code may use a trusted module although it is not on the list, also as a value or by writing to it. The allowlist's module checks skip a trusted module, so don't rely on them for one. The checks from earlier releases still apply to it, such as the code-running modules and file, network and process calls: `CodeVerifier(trusted_modules=["timeit"])` still refuses `import timeit`. The builtin, attribute and frame checks also still apply.

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

sandbox_verifier = CodeVerifier(trusted_modules=["numpy", "pandas"])
```

QWED's code-execution sandbox passes `numpy`, `pandas`, `scipy`, `sklearn`, `statsmodels` and `patsy` as trusted, so the Stats engine still runs code that uses them.

### Code hidden from the checks is refused

> [!NOTE]
>
> Changed in v9.0.0

Before v9.0.0, the following code was `VERIFIED · ADMIT` because the checks never saw what it ran. It is now refused:

* **Modules taken by name from the import system** ([GHSA-qrp4-p44j-m484](https://github.com/QWED-AI/qwed-verification/security/advisories/GHSA-qrp4-p44j-m484)): `__loader__.load_module(...)`, `importlib.util.module_from_spec`, the importlib bootstrap, `pkgutil.resolve_name`, `pydoc.locate`, and any read of `sys.modules`.
* **Modules that run strings as code** ([GHSA-jrxf-9jh4-86w7](https://github.com/QWED-AI/qwed-verification/security/advisories/GHSA-jrxf-9jh4-86w7)): importing `timeit`, `cProfile`, `profile`, `pdb`, `bdb`, `code`, `codeop`, `trace`, `doctest`, `logging.config` or `idlelib`. File readers such as `tarfile`, `zipfile`, `codecs.open`, `linecache`, `fileinput`, `glob`, `tempfile`, `sqlite3`, `shelve` and `dbm` are file access.
* **Code in strings that typing evaluates** ([GHSA-p75q-7rg5-ff46](https://github.com/QWED-AI/qwed-verification/security/advisories/GHSA-p75q-7rg5-ff46)): string annotations and `ForwardRef` strings that hold a call, lambda, comprehension or assignment expression. `__forward_code__`, `__forward_arg__`, `__annotations__` and `__annotate__` are dangerous attributes.
* **A source encoding other than UTF-8** ([GHSA-pr6c-cqg8-6w5r](https://github.com/QWED-AI/qwed-verification/security/advisories/GHSA-pr6c-cqg8-6w5r)): under a `utf-7` or `unicode_escape` coding declaration, text checked as a comment can decode to statements when the code runs. A coding declaration whose codec is not UTF-8 is a `CRITICAL` issue of type `source_encoding`. Save the file as UTF-8, then remove the declaration or declare `utf-8`.

### SDK clients use `CodeVerifier`, not `CodeGuard`

As of v8.0.0, [`QWEDClient.verify_code`](https://docs.qwedai.tech/sdks/python#verify_code-code-language) always calls `POST /verify/code`, so `CodeVerifier` decides admission. When the server can't be reached, the client returns `UNVERIFIABLE`. [`QWEDLocal.verify_code`](https://docs.qwedai.tech/advanced/qwed-local#3-code-security-codeverifier) runs `CodeVerifier` in process. The [`CodeGuard`](https://docs.qwedai.tech/sdks/guards#codeguard) blocklist is a pre-filter only. It blocks reflective calls, `__builtins__`, dunder attributes, `importlib`, `builtins`, `ctypes`, `marshal`, and dotted imports, and it marks its own pass as `advisory`. See [GHSA-4rj3-8wqj-cqwc](https://github.com/QWED-AI/qwed-verification/security/advisories/GHSA-4rj3-8wqj-cqwc) and [GHSA-v8qq-v427-qrqc](https://github.com/QWED-AI/qwed-verification/security/advisories/GHSA-v8qq-v427-qrqc).

### 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](https://docs.qwedai.tech/advanced/diagnostics.md) — the `DiagnosticResult` contract in depth
* [Symbolic execution limits](https://docs.qwedai.tech/advanced/symbolic-limits.md) — when CrossHair works, when it doesn't, and how to bound it
* [SQL engine](https://docs.qwedai.tech/engines/sql.md) — verify SQL queries
* [Logic engine](https://docs.qwedai.tech/engines/logic.md) — verify logical constraints


## Related topics

- [Math engine](https://docs.qwedai.tech/engines/math.md)
- [Logic engine — Z3 SAT/SMT verification with QWED-Logic DSL](https://docs.qwedai.tech/engines/logic.md)
- [Verification engine tiers: Proof, Policy, Advisory](https://docs.qwedai.tech/engines/overview.md)
- [QWED-Agent specification v1.1](https://docs.qwedai.tech/specs/agent.md)
- [Changelog](https://docs.qwedai.tech/changelog.md)


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