zkWasm

1.개요#

WebAssembly 프로그램의 실행 결과를 영지식 증명으로 검증할 수 있도록 설계된 zkVM 시스템이다. 서틱은 2024년 zkWasm Halo2 회로의 실행 테이블·메모리 테이블·호출 스택·비트 연산 등 핵심 구성요소가 Wasm 실행 규칙에 부합하는지 Coq로 형식 검증했다. Rust 알고리즘 전체와 Wasmi 인터프리터, Halo2 자체 및 일부 제약조건 생성 코드는 검증 범위에서 제외됐다.

2.연표1건

1. 2026.09이정표서틱은 2024년 zkWasm Halo2 회로의 실행 테이블·메모리 테이블·호출 스택·비트 연산 등 핵심 구성요소가 Wasm 실행 규칙에 부합하는지 Coq로 형식 검증했다. Rust 알고리즘 전체와 Wasmi 인터프[2]