Clean, a formal verification DSL for ZK circuits in Lean4

Re:Clean, a formal verification DSL for ZK circuits in Lean4 by ted_dunning on Friday March 28, 2025 @03:14AM (#43502444)

I hate to sound sarcastic, but you answered your own question about an opaque acronym with another couple of opaque acronyms. And didn't repeat the answer that you found.

So what's EOF? What's EVM?

I happen to know that nvm probably means never mind, but that is not a given for other readers.

[ Parent | on HN ]

Re:Clean, a formal verification DSL for ZK circuits in Lean4 by vons on Friday March 28, 2025 @04:36AM (#43502946)

So, EOF is basically an object format for EVM (Ethereum Virtual Machine) bytecode. You can learn more here: https://evmobjectformat.org/. Clean is basically a DSL for writing zero-knowledge-proof circuits, so it is unrelated to the EVM.

[ Parent | on HN ]

Re:Clean, a formal verification DSL for ZK circuits in Lean4 by ted_dunning on Saturday March 29, 2025 @12:38AM (#43512777)

Thanks!

[ Parent | on HN ]