Hacker News: rot256

Show HN: zkGolf – Competitive optimization of formally verified circuits

rot256 — Thu, 02 Jul 2026 15:40:05 +0000

Zero-Knowledge Proofs (ZKPs) let an untrusted proved show that computation was executed correctly without revealing the inputs to the verifier. However to prove anything, the computation first has to be expressed as a circuit: a system of polynomial equations (constraints) over a finite field. Circuits are the assembly language of zk and every constraint costs prover (and sometimes verifier) time, so production circuits are aggressively hand-optimized.

Over the last months, we have been experimenting with writing formal specifications instead and letting LLMs produce the circuits: as long as they could prove that their implementation was correct. It started with SHA-256: we hand wrote a specification in Lean for SHA-256 compression, and then we asked LLMs to write the circuit, targeting R1CS arithmetization and large fields.

It took a few hours of work for Opus 4.7, and some light steering into the right direction, but in the end the model came up with a reasonable implementation. We then asked the LLM to aggressively optimize the circuits, by driving down a cost metric of the circuit (number of constraints). We immediately got very promising results, just by asking to come up with optimization ideas, implement them and prove that the new circuit still satisfies soundness and completeness. Sometimes, it came up with unsound optimizations, however, since it could not prove them, it backtracked and got itself back on to the right approach.

The result was a (non-deterministic) circuit beating the current, human optimized, state of the art for SHA256 compression. This experience lead us to create "zk.golf" which is an open competition to produce optimized, formally verified circuits to lower the bar for the use of ZKPs and make their application more efficient.

Come play (https://zk.golf/llms.txt) and learn about formal verification.

Comments URL: https://news.ycombinator.com/item?id=48763246

Points: 69

# Comments: 12

SlopTacker: The AI Streaming Drain

rot256 — Thu, 18 Jun 2026 11:22:16 +0000

Article URL: https://sloptracker.org

Comments URL: https://news.ycombinator.com/item?id=48583721

Points: 4

# Comments: 0

Powers-of-Funbenius

rot256 — Tue, 05 May 2026 14:10:39 +0000

Article URL: https://blog.zksecurity.xyz/posts/powers-of-funbenius/

Comments URL: https://news.ycombinator.com/item?id=48022775

Points: 10

# Comments: 0

New comment by rot256 in "Is BGP safe yet?"

rot256 — Wed, 01 Apr 2026 19:07:32 +0000

For LetsEncrypt, routing is authentication: if packets routed to the IP in the A record end up at your place, you can get a cert for that domain.

New comment by rot256 in "Is BGP safe yet?"

rot256 — Wed, 01 Apr 2026 15:06:11 +0000

I think that way to solve BGPs security problems might be to use a new cryptographic hammer, "Proof-Carraying Data", where messages come with cryptographic proofs that they were produced correctly. This allows you to basically just run BGP, but every AS proves that it ran it correctly. The proofs take constant time to verify, regardless of how large the network is, or how many hops the routing message has taken. Feasibility is helped by latency not being super critical in BGP and BGP being a pretty simple protocol; which makes computing these proofs plausible.

https://rot256.dev/post/bgp-pcd/

Proof-carrying data has come a long way in the last 10 years.

EDIT: you would still need RPKI, but not BGPSec

New comment by rot256 in "RustTraining: Beginner, advanced, expert level Rust training material"

rot256 — Wed, 25 Mar 2026 14:59:29 +0000

This seems useless and misguided? This training material contents is clearly AI generated, if people can't be assed to write a book, then why should people read it?

Maybe it's my teaching background, but there is something uniquely soulless about teaching humans with AI slop passed off as a course; this is the stuff of "Amazon AI generated book spammers" and to be honest, I expected better from Microsoft.

If people wanted LLM output, they can generate it themselves...

New comment by rot256 in "Thank you Google for breaking my YouTube addiction"

rot256 — Sun, 18 May 2025 12:23:36 +0000

PipePipe? https://pipepipe.dev/

EDIT: also skips sponsor segments.

New comment by rot256 in "Reports of Putin's death might not be greatly exaggerated"

rot256 — Tue, 31 Oct 2023 15:36:48 +0000

As pointed out by Mark Galeotti, both the sources are less than reliable...

https://podcasts.apple.com/gb/podcast/in-moscows-shadows-120...

Whether dead or not, it is frankly disappointing that western media lends so much credence to sources which have been consistently wrong and made outright ridiculous claims before. Even if they try hedging it by calling them rumors, until more reliable sources emerge it is just noise...