I built a Lisp VM in Rust that proves its own execution trace (STARKs + Winterfell)

Andrei Kochergin — Mon, 24 Nov 2025 11:00:00 +0000

Over the last few weeks I've been building an 8-register VM in Rust for a small Lisp-like DSL, plus a proof pipeline that turns programs into STARK proofs of execution.

The DSL is compiled by the zk-lisp-compiler crate into a compact Op sequence, and proofs are generated through a dedicated backend built on top of the winterfell crate.

A few details that might be interesting from a Rust/efficiency point of view:

Trace Layout & Generation

I defined a unified execution trace (VM registers, RAM tables, Merkle gadget, Poseidon2 lanes, ROM accumulator) in a single Columns layout. The VmTraceBuilder simulates the Op sequence, seeds registers, and fills a Winterfell TraceTable while keeping allocations predictable (pre-zeroed trace, cached Poseidon2 params, partition selection).

Multi-segment Execution

The backend implements a SegmentPlanner that cuts the padded trace into level-aligned segments under a max_segment_rows budget. The interesting part was remapping the unified Columns into per-segment traces and computing state hashes at boundaries for chaining without fighting the borrow checker too much.

STARK-in-STARK Recursion

Recursion is expressed via generic traits (RecursionBackend, RecursionStepProver). The pipeline proves each execution segment, then runs an aggregation STARK over the resulting step proofs. This required some heavy generic bounds and type plumbing to keep the frontend (zk-lisp-proof::frontend) fully backend-agnostic.

Example

To prove the VM actually handles state transitions, here is a batch processor I wrote in zk-lisp. It calculates the new state root and total fees for a batch of transactions:

;; Simple rollup-style benchmark for zk-lisp:
;; - N_ACCOUNTS balances in RAM
;; - N_TXS transfers (from, to, amt, fee)
;; - compute new balances and hash the state

(def N_ACCOUNTS       8)
(def N_TXS            16)
(def HASH_BALANCES_IV 12345)

;; RAM layout:
;; [0 .. N_ACCOUNTS-1] = balances
;; [N_ACCOUNTS .. N_ACCOUNTS+4*N_TXS-1] =
;;     tx data (from, to, amt, fee) per tx

(def (init_state)
  ;; Initialize account balances [0 .. N_ACCOUNTS-1].
  (loop :max N_ACCOUNTS ((i 0))
    (begin
      (store i 0))
    (recur (+ i 1)))

  ;; Initialize tx table [tx_base .. tx_base + 4*N_TXS-1].
  (loop :max N_TXS ((i 0))
    (let ((base (+ (tx_base) (* i 4))))
      (begin
        (store base       0)   ;; from
        (store (+ base 1) 1)   ;; to
        (store (+ base 2) 1)   ;; amount
        (store (+ base 3) 0))) ;; fee
    (recur (+ i 1))))

(def (tx_base)
  N_ACCOUNTS)

(def (tx_from i)
  (load (+ (tx_base) (* i 4))))

(def (tx_to i)
  (load (+ (tx_base) (+ 1 (* i 4)))))

(def (tx_amount i)
  (load (+ (tx_base) (+ 2 (* i 4)))))

(def (tx_fee i)
  (load (+ (tx_base) (+ 3 (* i 4)))))

;; Safe arithmetic helpers (wrapping into field but
;; using safe-add/safe-sub to enforce non-negative balances).

(def (apply_tx i)
  (let ((from (tx_from i))
        (to   (tx_to i)))
    (begin
      ;; Debit sender: from_bal - (amt + fee)
      (store from
        (safe-sub (load from)
                  (safe-add (tx_amount i) (tx_fee i))))
      ;; Credit receiver: to_bal + amt
      (store to
        (safe-add (load to) (tx_amount i)))
      ;; Return fee
      (tx_fee i))))

;; Loop over all N_TXS, accumulate total fee
(def (apply_batch)
  (loop :max N_TXS ((i 0) (fee_sum 0))
    fee_sum
    (recur (+ i 1) (safe-add fee_sum (apply_tx i)))))

;; Simple Poseidon2-based hash chain over balances
(def (hash_balances)
  (loop :max N_ACCOUNTS ((i 0) (h HASH_BALANCES_IV))
    h
    (recur (+ i 1) (hash2 h (load i)))))

(typed-fn main ((let u64) (let bytes32)) -> bytes32)
(def (main expected_fee_sum expected_root)
  (begin
    (init_state)
    (let ((fee_sum (apply_batch))
          (root    (hash_balances)))
      (begin
        (assert (= fee_sum expected_fee_sum))
        (assert (= root expected_root))
        root))))

This program compiles down to the VM opcodes, and Winterfell generates a proof attesting that "I know a list of valid transactions that result in this state root" without revealing the transactions themselves.

It's still a prototype (AGPL-3.0), but I'd really appreciate feedback on:

the trait structure around ZkBackend / recursion
whether the trace planner + VM trace builder design makes sense from a performance perspective

Repo: https://github.com/yoozzeek/zk-lisp

Smart engineers are no longer needed

Andrei Kochergin — Wed, 13 Aug 2025 03:46:12 +0000

In the ’70s and earlier, when conditions were harsh, the pioneers of computing knew exactly where every bit went. That hardware limitations made compute far more costly.

Just look at this:

🚀 Apollo Guidance Computer (Lunar Module, Moon landing):
~72KB of fixed “core‑rope” memory for program code
~4KB of erasable RAM for variables/scratch space

🛰️ Voyager probes (launched in 1977). Both are still operational and sending telemetry. One of them is now 25 billion kilometers from Earth and it’s still talking to us:

Command System (CCS): 2KB RAM + ~4KB ROM
Flight Data Subsystem (FDS): 8KB RAM + ~8KB ROM (science & engineering data)
Attitude & Articulation Control System (AACS): 2KB RAM + ~8KB ROM (controls orientation)

That’s it. No bloat. No margin for sloppiness. Precision was survival.

Now? Every React component or Node.js package weighs 10KB+. LLMs spit out infinite SELECT loops, store raw or SHA256’d passwords, and somehow… your app still works. Some top investors, like Paul Graham in his recent X post cheer on vibecoders pumping out 10,000 lines a day like that’s the gold standard.

How can you not relax and forget the basics?

I understand why nowadays many of my colleagues are frustrated by “vibe code” and next gen devs skipping the fundamentals. They think the basics are irrelevant now that LLMs can spit out code.

But this cycle isn’t new:

👴 In my (millennial) era “older” devs wrote PHP/Perl/Python engines from scratch, while I was so dummy that could only learning Joomla with its extensions, phpBB and HTML with CSS. “You don’t even know what’s under the hood!” I’d hear.

👴 In the ‘80s, C programmers manually managed memory, scoffing at C++ and OOP as “toys” with “unnecessary abstraction.”

👴 In the ‘60s, assembler veterans mocked FORTRAN and COBOL. “A compiler can’t optimize better than me!”

The cycle repeats.

But here’s what doesn’t change: the foundation. It’s the bedrock. It doesn’t shift with every new framework, hype wave, or trend.

Learn it. Dig deep. Know what you’re building on. That’s how you stop being a consumer and become a creator.

Because if you rely on LLMs without understanding the essence, you’re setting yourself up for failure.

The people pushing “AI will replace you” are selling hype. CEOs, corporations, and investors who preach that you no longer need to learn? They’ll throw your future, your job, even the planet under the bus for a return and control.

They have no ethical brakes.

Think LLMs are like drugs: they give the illusion of power. They make you feel like you’re building something. But in the end, you’ll be left with vibes while they collect your time, your money, your talent.

P.S. Of course, I also use LLM 💊, but only where it actually helps and doesn't hallucinate, overcomplicate (or "simplify" by suggesting rm -rf your-project): small scripts, simple examples, testing and documentation, study help, routine reviews, or fixing spelling in posts like this one. Not for real programming whether it’s a fresh project or some legacy beast.