The Final Form of Software Development
The article proposes that the 'final form' of software development combines AI-generated RISC-V assembly code with formal verification in the Lean proof assistant, eliminating higher-level languages and compilers to ensure bug-free, provably correct code for performance-critical zkVM applications. The author demonstrates this approach in the evm-asm project, where AI agents write and refactor assembly code and generate Lean proofs to verify correctness. Unlike traditional methods relying on formally verified compilers or high-level languages like Rust or C, this method avoids undefined behaviors and optimization unpredictability by working directly at the assembly level. The approach is both historically final—enabled by recent AI advances—and category-theoretically final as a canonical endpoint of software development paradigms.
Opening excerpt (first ~120 words) tap to expand
The Final Form of Software Development Yoichi Hirai April 29, 2026 9 min read zk formal-verification AI lean educative 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. — @pirapira Don't tell me you're building the fastest EVM implementation from your phone 😎 — @butta_eth 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.
…
Excerpt limited to ~120 words for fair-use compliance. The full article is at ZK/SEC Quarterly.
Discussion
0 commentsMore from ZK/SEC Quarterly
