VPA
Verified Portable Assembly — a safe, formally verified low-level virtual assembly language, reference interpreter, Lean 4 proof framework, and native/WASM compiler pipeline.
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.