# VPA

Verified Portable Assembly — a safe, formally verified low-level virtual assembly language, reference interpreter, Lean 4 proof framework, and native/WASM compiler pipeline.

[Open in the WASM portfolio](https://yemelianov.dev/?project=vpa&detail=1)

Tags: compilers, formal-verification, assembly, rust, python
Source: private
Project: https://yemelianov.dev/?project=vpa&detail=1

Verified Portable Assembly (VPA) is a low-level, safe virtual assembly language designed for verified compilation, firmware execution, and formal proof generation.

VPA provides a memory-safe assembly model where registers and memory slices are strongly typed and bounds-checked by construction. The architecture features a reference interpreter, Lean 4 theorem proving integration for verification claims, and target emitters for ESP32 native C, WebAssembly (WASM), and LLVM-based environments.

Key highlights:
- **Formal Verification**: Verified module specs backed by Lean 4 semantics and proof terms.
- **Safety Profiles**: Edge safety enforcement prohibiting arbitrary pointer arithmetic or unverified memory access.
- **Multi-Target Codegen**: Lowers VPA modules to byte-stable C, WASM binaries (`.wasm` / `.wat`), and executable test harnesses.
- **LLM Integration Harness**: Built-in harness scripts and NVIDIA API subagents (`nvidia_client.py`, `vpa_llm_runner.py`) for automated VPA code generation, verification, and execution.