We founded Velobyte to build compiler infrastructure that automates the expensive parts of performance engineering. Our first product, EvoCompiler, gives coding agents tools to investigate bottlenecks, test optimization ideas, and measure the resulting builds.
Existing compilers provide an extraordinary starting point. An engineer working on one application can also exploit information outside a compiler invocation: a representative workload, a protocol invariant, a deployment target, or a larger restructuring of the source. Turning that information into a dependable improvement requires experiments and reasoning that are usually performed by hand.
That is the work we want EvoCompiler to organize. It connects agent-driven exploration with compiler tuning, scoped correctness checks, and target-side measurement. The product is in beta; its most consequential engineering challenge is making these pieces compose into a build someone else can reproduce.
Source rewrites and compiler settings are different searches.
Compiler tuning explores choices within an existing implementation: optimization levels, inlining decisions, loop transformations, and other supported controls. The search space is constrained by the toolchain and the registered region. Evo derives legal choices from that context; the agent names the region, workload, objective, and budget instead of supplying an arbitrary command-line flag space.
A source rewrite changes the implementation itself. An agent might move a repeated calculation outside a search, change a data representation, or reorganize calls. These proposals can expose opportunities that flag tuning cannot express, but they also introduce new obligations about observable behavior. A plausible explanation of an algebraic change is insufficient when the C program has overflow, aliasing, or floating-point effects.
The searches interact. A rewrite can change which settings work best, and separately successful changes can interfere when combined. A result therefore belongs to a particular built program. Adding isolated speedup percentages does not establish the performance of their composition.
The agent proposes; other tools establish the result.
EvoCompiler exposes its investigation tools through MCP so an agent can work from its existing coding environment. The separation of authority matters more than the interface: the agent generates hypotheses, checking tools establish particular facts, and a runner builds and measures candidates in the registered target environment.
For a source proposal, the original code and applicable context facts must come from trusted project intake. The proposing agent cannot make a change legal by inventing a precondition. Likewise, a failed build or a correctness refusal must not become a timing result. Counterexamples, unsupported constructs, timeouts, and measurement failures give the next experiment different information.
Proposal
A reason to investigate
A source change or tuning candidate. Its author’s confidence establishes neither correctness nor speed.
Evidence
A claim with a scope
Checker assumptions, observed outputs, and repeated target measurements. Each answers a different question.
Deployable result
A build to reproduce
The accepted combination, with its build context and checks. Producing this reliably is the integration goal.
A useful change can shorten a serial path.
Our liblc3 experiment makes the distinction concrete. Its arithmetic decoder updates state after each symbol. Parallelizing that state machine was not the useful opportunity; reducing work on its dependency chain was. Inside the symbol binary search, each probe compared low < range * L. Computing q = low / range once allowed the probes to compare q < L instead.
For nonnegative integers and positive range, write low = q·range + rem, where 0 ≤ rem < range. Then low < range·L exactly when q < L. The decoder’s audited bounds ensure a nonzero divisor and a product that fits in its unsigned arithmetic. Those bounds connect the integer identity to this C comparison.
The rewrite reduced median decoder time by approximately 3–5.6% in two interleaved A/B experiments on an Apple M2 Pro. Outputs were byte-identical across the tested corpus of approximately 54,000 frames in four configurations. This was an agent-assisted engineering experiment alongside an Evo tuning campaign, not a fully automated product run. The change was submitted as upstream PR #89; it is not a merged upstream result. The maintainers pointed out that the division would regress on the microcontrollers and audio DSPs where liblc3 is most deployed, where a hardware divider is slow or absent. That feedback is the point of this note: a win on one machine is not a win on every machine, so the loop has to measure on the real target. Our later esp-dl change, measured on the device it ships on, is the better example of the result we are after.
The separate, small flag search did not establish an improvement over upstream -O3, and an output check rejected one candidate that changed the encoded bitstream. The detailed case study records the measurements and reproduction materials. The lesson is specific: the useful search changed the source-level critical path.
Proof and testing establish different facts.
The committed Z3 script proves the integer comparison identity under stated bounds. It does not prove the entire decoder or the generated machine code. Golden-output tests add evidence about actual executions; they do not cover all possible inputs. Keeping these claims separate makes both more useful.
Floating point makes the distinction particularly sharp. Real-number equality can permit reassociation that changes rounded results. Gimlet Labs’ kernel-verification work describes an exact-real model and bounded reductions, with corresponding limits on what equivalence means. Bit-exact behavior and application-defined numerical tolerance are different acceptance criteria.
Proof cost also belongs in the optimization loop. In the liblc3 investigation, direct bit-vector encodings stalled; an integer formulation using division axioms made the comparison lemma tractable. This suggests a useful role for language models: propose intermediate lemmas and invariants that make a difficult check easier to discharge. An independent checker must establish those lemmas, and program analysis must justify their assumptions. A model-written assumption cannot substitute for a fact about the code.
A timeout establishes neither equivalence nor a bug. Even a complete equivalence proof preserves defects already present in the reference. Application requirements and integration tests therefore remain necessary alongside transformation checks.
The search needs an experiment it cannot grade itself.
A search that compares absolute timings from different rounds can learn changes in machine load instead of better code. Evo’s paired measurement protocol carries candidate and baseline costs; ratio objectives compare candidate_cost / baseline_cost. Measuring the baseline nearby helps account for drift, but does not remove thermal effects, scheduling noise, or interference.
Selection creates another problem: the fastest observed candidate may be the luckiest. Our runner-driven campaign implementation adds a fresh paired confirmation of the best candidate before accepting it for replay. That is a repeatability check, not a confidence interval. Stronger release evidence requires repeated, interleaved runs and representative inputs held out of the search. A local win also needs an application-level check: speeding up a tiny region can leave the user’s objective unchanged.
An experiment should end in a build someone can reproduce.
Saving an agent’s patch is insufficient. A useful result must preserve the accepted source changes and compiler settings, the context in which they apply, and enough evidence to repeat the comparison. “Replay” means applying those saved decisions during a later build. A “pack” is our term for a portable result intended to support that use.
The current C path can freeze measured compiler policies and accepted source substitutions into one offline compiler version. Search happens ahead of time; replay needs no model inference and leaves the checked-in source intact. The combined build carries its own end-to-end measurement: adding individual trial speedups would not establish that result. Reuse remains conditional on matching source, toolchain, and target context. The practical acceptance test is a fresh checkout on which another engineer can reproduce the accepted combination and its performance comparison.
Beyond reproducibility, we want each investigation to improve the next one. A remembered identity, failed experiment, or useful decomposition can guide search on unfamiliar code. Whether it helps is measurable: less engineering time and machine budget to reach an independently checked improvement.