This page describes a restricted Python subset, not general CPython. See the full list of supported and unsupported constructs below.

Verified Python Execution

Write in a supported Python subset. The transpiler converts it to .syn, Z3 proves correctness properties when @inv annotations are present, and it executes as WebAssembly. Deterministic results, opt-in formal guarantees.

Execution Pipeline
Python
Source code in supported subset
→
.syn
Transpiled to AI-native IR
→
Z3 Verify
Proves pure, terminates, no_oob
→
Wasm
Compiled to WebAssembly bytecode
→
Result
Deterministic integer output + hash
Supported Constructs
Construct
Example
Variables
x = 10
Arithmetic
+, -, *, //, %
Augmented assignment
x += 1
Comparisons
==, !=, <, >, <=, >=
Boolean operators
and, or, not
if / elif / else
if x > 0: ...
while
while i < n: ...
for / range
for i in range(n): ...
def / return
def f(x): return x
abs / min / max / print / len
abs(-5)
Lists
a = [1, 2, 3]
Nested functions
def outer(): def inner(): ...
Not Supported
Construct
Why
import
No module system in the sandboxed runtime
class
No object model; functions and integers only
dict / set / tuple
Only lists are supported as compound types
Comprehensions
Use explicit for loops instead
try / except
No exception model; verification catches errors statically
with
No context managers in a pure execution model
String operations
All values are i64 integers; no string type
float
All arithmetic is integer-only (i64)
numpy / scipy
No external library support
*args / **kwargs
Fixed-arity functions only
Decorators
No metaprogramming constructs
lambda
Use named def instead
global / nonlocal
Lexical scoping only; no mutable global state
Semantic Differences from CPython
Integer-only arithmetic
All values are signed 64-bit integers (i64). There is no float, string, or object type.
Division is floor division
The / operator is not available. All division uses // (floor division), matching the i64 constraint.
No overflow protection
Integer arithmetic wraps at i64 bounds. Values exceeding the 64-bit signed range wrap silently.
Print outputs integers only
The print() function emits the integer representation of its argument. No string formatting.
Formal Verification

When .syn code includes @inv annotations, the Z3 theorem prover checks the specified properties before execution:

Verification is opt-in per function. Code without annotations compiles and executes normally but skips Z3 checking.

@inv pure
The function has no side effects beyond its return value. No mutable global state, no I/O beyond print.
@inv terminates
All loops have a provably decreasing variant. The function is guaranteed to halt.
@inv no_oob
All list accesses are within bounds. No out-of-bounds read or write can occur at runtime.

Verification is opt-in via @inv annotations. Non-annotated code compiles and executes normally but skips Z3 checking. When active, verification runs at sub-millisecond latency.

What's Next
NEXTf32 floating point support — currently all arithmetic is integer-only (i64)
PLANNEDBroader Python subset — print(), range(), list operations, float math
PLANNEDString type support and basic string operations
TARGET80% of typical data processing Python should transpile without errors