Hackers' Pub

Syntax	Description	Examples
`"` keyword `"`	Finds the string within quotes, including spaces. Case-insensitive. (Escape quotes inside with `\"`)	`"Hackers' Pub"`
`from:` handle	Finds content written by the specified user.	`from:hongminhee` `from:hongminhee@hollo.social`
`lang:` ISO 639-1	Finds content written in the specified language.	`lang:en`
`#` tag	Finds content with the specified tag. Case-insensitive.	`#HackersPub`
condition condition	Finds content that satisfies both conditions on either side of the space (logical AND).	`"Hackers' Pub" lang:en`
condition `OR` condition	Finds content that satisfies at least one of the conditions on either side of the OR operator (logical OR).	`#HackersPub OR "Hackers' Pub" lang:en`
`(` condition `)`	Combines the operators within the parentheses first.	`(#HackersPub OR "Hackers' Pub" OR "Hackers Pub") lang:en`

José A. Alonso @Jose_A_Alonso@mathstodon.xyz

3/30/2025, 9:57:29 AM

Public

Introducing clean, a formal verification DSL for zk circuits in Lean4. ~ Giorgio Dell'Immagine. https://blog.zksecurity.xyz/posts/clean/ #ITP #LeanProver

Introducing clean, a formal verification DSL for zk circuits in Lean4 - ZKSECURITY

We are really excited to share our initial steps towards building clean, an embedded DSL and formal verification framework for ZK circuits in Lean4. As we recently shared, Zero Knowledge circuits are full of bugs, but fortunately, techniques like formal verification can provide a huge confidence boost in the correctness of ZK circuits. Clean enables us to define circuits in Lean4, specify their desired properties, and – most importantly – formally prove them!

blog.zksecurity.xyz

If you have a fediverse account, you can quote this note from your own instance. Search https://mathstodon.xyz/users/Jose_A_Alonso/statuses/114250786366294861 on your instance and quote it. (Note that quoting is not supported in Mastodon.)