pysymex 0.1.0a5

EDUCATIONAL PURPOSES ONLY: A symbolic execution engine for studying formal verification concepts. Not for production use.

pysymex

Python Symbolic Execution Engine powered by Z3 Theorem Prover Mathematically prove your Python code won't crash.

╔══════════════════════════════════════════════════════════════════════════════╗
║                                                                              ║
║   p y s y m e x                                                              ║
║   ─────────────────────────────────────────────────────────────────────────  ║
║   Symbolic Execution · Formal Verification · Z3-Powered                      ║
║                                                                              ║
╚══════════════════════════════════════════════════════════════════════════════╝

---

EDUCATIONAL PURPOSES ONLY

This project is a research prototype designed for studying symbolic execution and formal verification concepts. It is NOT intended for production use, security auditing, or critical systems verification. Use at your own risk.

---

Table of Contents

1. Overview
2. Installation
3. Quick Start
4. Bug Types Detected
5. Architecture
6. Development
7. Requirements
8. Contributing
9. License
10. Documentation

---

1. Overview

pysymex (Python Symbolic Execution) is a bytecode-level symbolic execution engine that uses the Z3 SMT solver to formally verify Python programs. It explores all possible execution paths through your code, building mathematical constraints at each decision point, then uses Z3 to find concrete inputs that trigger bugs — or prove no such inputs exist.

What It Does

• Disassembles Python bytecode (CPython 3.11–3.13)
• Symbolically executes every reachable path
• Reports bugs with counterexamples (concrete crashing inputs)
• Interprocedural Analysis — crosses function boundaries via call graphs and summaries
• Asynchronous Execution — high-throughput scanning with asyncio and process pools

Features

Category	Features
Engine	Bytecode-level symbolic execution, CPython 3.13 opcode support, Z3 SMT integration
Optimization	CHTD path explosion mitigation, constraint independence (KLEE-style), adaptive path selection
Analysis	Interprocedural analysis, abstract interpretation, loop handling
Output	Text, JSON, HTML, SARIF 2.1.0 (GitHub Security tab compatible), Rich (colored panels)
Safety	20+ bug types, 40+ detectors, sandbox isolation

---

2. Installation

From PyPI

pip install pysymex

From Source (Development)

git clone https://github.com/darkoss1/pysymex.git
cd pysymex
pip install -e ".[dev]"

---

3. Quick Start

Command Line

# Scan a file
pysymex scan mycode.py

# Scan a directory recursively
pysymex scan src/ -r

# Generate SARIF report for CI/CD
pysymex scan src/ --format sarif -o report.sarif

# Analyze a specific function
pysymex analyze mycode.py -f risky_func --args x:int y:str

# Run built-in benchmarks
pysymex benchmark --format markdown

Examples

The examples/ directory contains numbered scenarios for the current tree:

• 01_basic_safety_guards.py
• 02_common_runtime_bugs.py
• 03_concolic_exploration.py
• 04_contract_verification.py
• 05_deep_path_loops.py
• 06_sandbox_security.py
• 07_symbolic_containers.py
• 08_exception_handling.py

Python API

from pysymex import analyze

def risky_divide(x: int, y: int) -> int:
    return x // y

# Analyze for potential crashes
result = analyze(risky_divide, {"x": "int", "y": "int"})

for issue in result.issues:
    print(f"Bug: {issue.message}")
    print(f"Counterexample: {issue.counterexample}")

Example Output

╭──────────────────────────────────────────────────────────────────────────────╮
│ pysymex - formal verification report                                         │
╰──────────────────────────────────────────────────────────────────────────────╯

ISSUES FOUND (1)
────────────────────────────────────────────────────────────
╭─ [ DIVISION_BY_ZERO ] ───────────────────────────────────────────────────────╮
│  Location: mycode.py:12 in unsafe_divide()                                   │
│  Type:    DIVISION_BY_ZERO                                                   │
│  Error:    Division by zero: y can be 0                                      │
│  Trigger:  y = 0                                                             │
╰──────────────────────────────────────────────────────────────────────────────╯

SUMMARY
────────────────────────────────────────────────────────────
Paths explored:         1
Paths completed:        1
Instructions:           4
Execution time:     0.018s

Proven safe:            0
Issues found:           1

---

4. Bug Types Detected

Bug Type	Description	Example
Division by Zero	Division where denominator can be 0	x / y where y=0
Modulo by Zero	Modulo where divisor can be 0	x % y where y=0
Index Error	Array access beyond bounds	arr[i] where i >= len(arr)
Key Error	Dictionary key not found	d[key] where key missing
Attribute Error	Missing attribute access	obj.missing_attr
None Dereference	Accessing attributes on None	obj.method() where obj=None
Type Error	Type mismatch in operations	str + int
Value Error	Invalid value for operation	int("abc")
Assertion Error	Assertions that can fail	assert x > 0
Overflow Error	Arithmetic overflow	x + 1 where x = MAX_INT
Unbound Local	Using unbound local variable	print(x) before assignment
Name Error	Using undefined name	print(undefined_var)
Resource Leak	Unclosed files or connections	f = open(p); return
Dead Code	Code that never executes	Code after absolute return
Unreachable Code	Code that cannot be reached	Code after raise Exception
Infinite Loop	Loop that never terminates	while True: pass
Injection	Code injection vulnerabilities	SQL injection, command injection
Syntax Error	Invalid syntax patterns	Malformed code constructs
Logical Contradiction	Impossible logical conditions	if x > 10 and x < 5
Contract Violation	Violated function contracts	Pre/post condition failures

---

5. Architecture

pysymex/
├── analysis/              # Analysis engines
│   ├── solver/            # Z3 verification core
│   ├── abstract/          # Abstract interpretation
│   ├── detectors/         # Bug detectors (40+)
│   └── path_manager.py    # Path selection
├── core/                  # Engine foundation
│   ├── types/             # Symbolic primitives
│   ├── state.py           # VM state management
│   └── solver.py          # Z3 wrapper
├── execution/             # Bytecode VM
│   ├── dispatcher.py      # Opcode dispatch
│   └── opcodes/           # Handlers (3.11-3.13)
├── accel/                 # Hardware acceleration
│   └── backends/          # CPU backends
├── models/                # Stdlib models
├── reporting/             # Output formatters
└── scanner/               # Static scanner

---

6. Development

Setup

# Format code
ruff format pysymex tests

# Type checking
pyright pysymex

# Run tests
pytest tests/ -v

# Run with coverage
pytest --cov=pysymex tests/ -v

---

7. Requirements

• Python 3.11+ (tested on 3.11, 3.12, 3.13)
• z3-solver == 4.15.3.0
• pydantic >= 2.12.0
• immutables == 0.21
• rich >= 13.0.0

Note: Dependency versions are carefully constrained to verified compatible versions.

---

8. Contributing

pysymex is currently an "Open Source, but Closed Contribution" project.

While the source code is available under the AGPLv3 license, we are not currently accepting external Pull Requests. This ensures the engine's architectural and mathematical integrity during its initial alpha phase.

If you find a bug or have a feature request, please open an issue.

See CONTRIBUTING.md for more details.

---

9. License

AGPL-3.0 License — see LICENSE.

---

10. Documentation

[!NOTE] Temporary Automated Documentation An automatically generated Code Wiki providing an architectural deep-dive and component reference is available at: https://codewiki.google/github.com/darkoss1/pysymex

Important Notices:

• The Wiki is generated automatically but may take time to refresh; please verify the generation and commit dates on the page.
• It may be slightly outdated compared to the latest main branch.
• This is NOT official documentation and is provided for research and architectural exploration purposes only. Do not fully rely on it for production implementation details.

---

_{Built for Formal Verification}