This repository implements a compiler-based optimization framework for zero-knowledge virtual machines (zkVMs), specifically targeting OpenVM and SP1. Its core innovation is Automatic Precompile Synthesis (APC), which analyzes execution traces of RISC-V guest programs and synthesizes optimized constraint systems (symbolic machines) that drastically reduce proof cost—achieving up to 9x column reduction and 88x constraint reduction on complex operations. The system combines profile-guided optimization (PGO), a sophisticated constraint solver with range reasoning and rule-based rewriting, and an optional Lean4 verified optimizer via FFI. The architecture is a multi-crate Rust workspace with a CLI (`powdr_openvm_riscv`) orchestrating a staged pipeline: generate APCs from execution profiles, select the best candidates using PGO metrics, setup the prover with the selected APCs, execute the program, and generate proofs. It supports CPU and GPU (CUDA) backends, and includes extensive benchmarking infrastructure with nightly regression analysis and a web-based APC effectiveness viewer. Bus interaction handling is abstracted via a `BusMap` and adapter pattern, making the optimization logic VM-agnostic. While primarily an application, the repository has strong research character: it includes domain-specific formal methods (Lean4, Datalog rules), empirical constraint detection, and a large corpus of snapshot tests documenting optimizer outputs. It is actively maintained with CI pipelines, but depends on several tightly coupled forks (OpenVM, SP1) and pinned nightly Rust toolchains, posing moderate technical drift risk.