Skip to content(if available)orjump to list(if available)

Clean, a formal verification DSL for ZK circuits in Lean4

Clean, a formal verification DSL for ZK circuits in Lean4

5 comments

·March 27, 2025
Visit

qqqult

Does EOF make this easier / more efficient?

gmitscha

What's EOF?

Edit: nvm found it! No it doesn't, as this is not dealing with EVM at all

ted_dunning

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.

vons

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.