RISC-V Compliance Testing

https://github.com/eth-act/zkevm-test-monitor/

https://eth-act.github.io/zkevm-test-monitor/

Upgraded RISC-V test suites to ACT v4.0.0; exposed more bugs

Formal RISC-V Compliance of ZisK

https://github.com/eth-act/zisk-fv

Gap between "AI wrote me some Lean proofs" and "I am convinced this is" is huge.

Progress is mostly technical; summary is here for those interested.

Met with Héctor Masip of ZisK, who's now ramping up to review and contribute.

RISC-V Fuzzing

Near-final deliverables are a fuzzing grant; code released at the end of the month.

• Built on Ere
• Rust and pure RISC-V
• Don't want to front-run too much :)

Innovations and ArkLib

• Flock proof system: no more algebraic hashes .
• ArkLib#449: Perfect completness of sumcheck; useful for WHIR, Flock and more.
• ArkLib#516: Ring switching formalism; will be useful for formalizing Flock.

https://github.com/frisitano/evm-sail

Experiment with a formal specification in Sail machine spec language

• Same language used for official RISC-V specs.
• sail-to-lean backend already in use in zisk-fv and its ancestors.
• Started June 13; sail-to-C compilation is passing ALL EEST TESTS .
• My dream: feature parity with python specs, then replace them.