Note
Project Status: Concluded Proof of Concept / Archived Lirien started as a proof of concept to demonstrate path-aware liquid type verification for JIT-compiled Python. Having successfully proven this architecture (implementing ADTs, SIMD, monomorphization, and a verified numerical stdlib), active development has been concluded. The repository remains archived for research, study, and educational reference.
Warning
Lirien is an experimental research compiler. It is not production-ready and should not be used in critical systems.
Python's type annotations are unenforced at runtime. The standard trade-off is to accept the overhead of runtime checks and the Global Interpreter Lock (GIL) for safety, or to rewrite performance-critical code in a systems language at the cost of development complexity.
Lirien takes a different approach: it treats type annotations as formal specifications, uses an SMT solver (Z3) to prove their correctness at compile time, and then JIT-compiles the code directly to native machine instructions (via Cranelift), bypassing the CPython interpreter and the GIL.
The result is a compiler that can statically guarantee the absence of common classes of runtime errors—division by zero, out-of-bounds array/buffer accesses, null pointer dereferences—while executing at native speed.
For deep, detailed guides on individual features, check out the Lirien Documentation Hub:
- Getting Started & Installation: Setup prerequisites, build command, and run tests.
- Core Concepts & Verification Contracts: Refinement types, the
Vplaceholder DSL, Design by Contract (assert), and inductive proofs. - Performance & Monomorphization: Static dispatch via
Protocol, GIL-free parallelism, flow-sensitive type narrowing, const generics, and SIMD. - Data Structures & Memory Layouts: Flat C-ABI structs, stack-allocated value types, ADTs,
TypedDict, growable lists, and tensors with kernel fusion. - Developer Tooling & Diagnostics: Bypassing verification via
@jit, context-based logtracing(), and source-level error messages. - Architecture & Compiler Pipeline: Internal SSA IR design, compilation steps, and the caching mechanism.
- Experimental
numStandard Library: JIT-compiled, SIMD-accelerated, and Z3-verified numerical operations, activations, and neural network layers.
from lirien import verify, i64, Refined, V
# A refinement type: an integer strictly greater than zero
Positive = Refined[i64, V > 0]
@verify
def divide_verified(n: i64, d: Positive) -> i64:
# Z3 proves 'd > 0' holds. ZeroDivisionError is statically impossible.
return n // d
print(divide_verified(100, 5)) # Executed in native JIT-compiled machine codeFirst, ensure you have Rust (1.80+), Python (3.10+), and Z3 (v4.12+) installed.
# Setup virtual environment
python3 -m venv .venv
source .venv/bin/activate
pip install maturin ruff
# Build extension module
maturin develop --release# Run Rust tests
cargo test
# Run Python integration tests
PYTHONPATH=./python python3 -m unittest discover tests/pythonBuilt with 🦀 & 🐍 by Seuriin. Distributed under the AGPL-3.0 License. See LICENSE for details.