This post finishes software development. I found the final form. It's final in the historical sense, and final in the category theoretic sense too. Don't worry, it's fun.
I’m in a cafe in Portugal having a drink and contemplating on life while pull requests automatically pop up. They add new Lean theorems or refactor existing Lean proofs. CI green usually means correct. I can browse code on the phone and click merge.
Don't tell me you're building the fastest EVM implementation from your phone 😎
I'm doing this often on the phone and producing 200 to 600 commits per day. In the near future, I don't think I need to be even on the phone. Sometimes the agents make mistakes, but they notice the mistakes themselves when the proofs get stuck.
zkVMs need reliable guest programs
There are RISC-V virtual machines that produce succinct arguments of knowledge (zkVMs) cryptographically proving that a RISC-V program with a certain input produces certain output. What happens when a guest program has a bug? One day a verifier accepts a cryptographic proof for zkVM execution and causes trouble. You try to figure out what has gone wrong. From the publicly available information, you get cryptographic commitments and some openings of the commitments. These are usually nonsensical numbers. It takes a lot of time, and may even be impossible, to figure out what has gone wrong. For this reason it is very important that the guest programs of zkVMs are known to have no bugs.
Approach
My approach is to let AI agents (currently /loop command of Claude Code) write RISC-V assembly code and prove it correct in a proof assistant Lean. There are no Rust, no C, no C++, just RISC-V assembly code and Lean proofs.
This is a known approach: formal verification of assembly code is an old topic. My current approach is based on a research paper called "Coq: The world’s best macro assembler?" from 2013. I saw this paper roughly ten years ago. I've wanted to try the approach but the manual labor of writing Rocq (renamed from Coq) proofs seemed to consume too much time, so I never did try. In 2025, machines have started writing proofs in proof assistants (like Rocq and Lean) so now it's reasonable to use proof assistants as assembler.
This is easy: the RISC-V assembly is very easy to reason about. This is much easier than Rust, C and C++. When we write proofs about these programming languages we need to keep track of variables in scopes, objects in the memory, what has been constructed, virtual methods, adding signed integers might be undefined behavior, and so on. RISC-V has none of these except values in registers and memory. Moreover, since the AI agents are writing the assembly code themselves, they already know what the assembly code is doing and how it works. That's much easier than getting optimized outputs from compilers and performing detective work.
This works: you can have a look at evm-asm repo. Some parts of the Ethereum Virtual Machine have been written in RISC-V assembly code, and there are proven specifications about the RISC-V assembly code. My AI agents (currently /loop command of Claude Code) are currently performing lots of refactoring and developing a sophisticated division algorithm. I don't think I'll need a sophisticated division algorithm once zkVMs can receive hint inputs, but it's fun to watch.
How it looks
The code is just a sequence of instructions. This implements the 256-bit addition in EVM.
def evm_add : Program :=
-- Limb 0 (5 instructions)
LD .x7 .x12 0 ;; LD .x6 .x12 32 ;;
ADD .x7 .x7 .x6 ;; SLTU .x5 .x7 .x6 ;; SD .x12 .x7 32 ;;
-- Limb 1 (8 instructions)
LD .x7 .x12 8 ;; LD .x6 .x12 40 ;;
ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;
ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;
OR' .x5 .x11 .x6 ;; SD .x12 .x7 40 ;;
-- Limb 2 (8 instructions)
LD .x7 .x12 16 ;; LD .x6 .x12 48 ;;
ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;
ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;
OR' .x5 .x11 .x6 ;; SD .x12 .x7 48 ;;
-- Limb 3 (8 instructions)
LD .x7 .x12 24 ;; LD .x6 .x12 56 ;;
ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;
ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;
OR' .x5 .x11 .x6 ;; SD .x12 .x7 56 ;;
-- sp adjustment
ADDI .x12 .x12 32
The specification of this program looks like this
cpsTriple base (base + 120) code
(-- Registers + memory
(.x12 ↦ᵣ sp) ** (.x7 ↦ᵣ v7) ** (.x6 ↦ᵣ v6) ** (.x5 ↦ᵣ v5) ** (.x11 ↦ᵣ v11) **
evmWordIs sp a ** evmWordIs (sp + 32) b)
(-- Registers + memory (updated)
(.x12 ↦ᵣ (sp + 32)) ** (.x7 ↦ᵣ result3) ** (.x6 ↦ᵣ carry3b) **
(.x5 ↦ᵣ carry3) ** (.x11 ↦ᵣ carry3a) **
evmWordIs sp a ** evmWordIs (sp + 32) (a + b)) := by
The important thing is that b gets replaced by a + b. Here a + b is added as 256-bit numbers. Also sp moves to sp + 32. The change says that one EVM word is dropped from the EVM stack.
After this specification, there are 20 lines of cryptic code (called a Lean proof). That's only for convincing the Lean kernel that the specification always holds. I happen to be able to read Lean proofs to some extent, but I suspect this is becoming an obsolete skill; your coding agents can probably explain if you feed them a link.
Other options
I've been doing program verification for roughly ten years, so I can list ways to know there are no bugs. It's simple. Create correct source code, and turn it into correct machine code.
Formally verified compilers
There's a formally verified C compiler called CompCert. One approach is to perform formal verification of C source code, then feed the resulting correct C through CompCert to get correct RISC-V code.
I think this approach works. The only issue is performance of the generated code:
the code generated by CompCert runs at least twice as fast as the code generated by GCC without optimizations (gcc -O0), and approximately 10% slower than GCC 4 at optimization level 1 (gcc -O1), 15% slower at optimization level 2 (gcc -O2) and 20% slower at optimization level 3 (gcc -O3)
That's a blocker in a performance-centric situation where people are trying to get the zkVM prover to produce a cryptographic proof of a whole Ethereum block in a few seconds.
There's another formally verified compiler called CakeML. CakeML can compile StandardML. CakeML has a RISC-V backend. The produced RISC-V code performs garbage collection. When people are trying to squeeze the proving time in zkVMs, producing proofs about execution of garbage collection isn't appealing.
What about Rust?
Rust is designed by people who are familiar with program verification. Rust has many program verification tools. The bottleneck seems to be translating "correct" Rust code into a correct assembly program (either with a formally verified compiler or by comparing the assembly against the source after each compilation).
Why did I put quotations around "correct" Rust code? This is because I am not totally sure what a Rust program means. Rust's language specification is in development. For the moment the Rust compiler decides the meaning of a Rust program. The Rust compiler is written in Rust as well, so the meaning of the Rust compiler is determined by the Rust compiler itself. So, you'll end up looking at the assembly code or machine code.
Despite all that, it's possible to write your own Rust semantics in a proof assistant, and use that as an intermediate step for getting the assembly code formally verified. Maybe in the long run that's the way to go. That approach can be transformed to a "just assembly code and Lean" approach in a canonical way when you do all the steps in Lean. That's the canonical transformation that makes "just assembly code and Lean" the final approach in a category theoretic sense.
What about C and C++?
C and C++ have programming language specifications. The programming language specifications work as an interface between the compiler and the programmer. These language specifications say the behavior of a program is undefined when certain things happen (overflow of signed integers, adding a pointer and a pointer, computing pointers more than one item outside an array, accessing pointers that are wrong, etc). When you do program verification of C or C++, most of the effort goes into establishing none of these ever happen. The undefined behaviors are helpful for compilers especially when they optimize the output code. I made a trade. I didn't want to reason about lack of undefined behavior, so I dropped compilers. It was possible to generate assembly code instead, thanks to LLMs.
More academic projects
There are small programming languages that compile to RISC-V like bedrock2 and Jasmin. These languages have specifications in Rocq and formally verified compilers. Jasmin is focused on cryptography. Maybe it could be adapted for EVM implementation.
Bedrock2 is more general. The approach of bedrock2 is inspiring. The selling point of bedrock2 is holistic co-verification of software and hardware. In the setting of verified zkEVM, it's important that the formal verification of both zkVMs and guest programs is organized in a holistic way. The program logic of evm-asm is similar to that of Bedrock2.
Since the performance characteristics of zkVMs are very different from those of RISC-V hardware, the desired assembly code is probably very different, so I'll be experimenting with direct assembly programming. Moreover, we might want to modify the target zkVMs to deviate from RISC-V (maybe more registers).
Why final form
There are tons of programming languages and compilers. They have nice abstractions and nice optimization techniques. All of these can be translated into the assembly + Lean paradigm. This is why the assembly + Lean paradigm is the final form of software development.
Image generated by ChatGPT. Grammar, style and summary generation helped by Claude Code.