that's cool, what were they using for | PyPA | Page 1

muted moss Apr 22, 2026, 3:41 PM

#

It was Tynan Daly at High Dimensional Research, he was takling about throwing a swarm of agents at a problem and the review scaling problem and using this to formally verify the functions it produced. His specific problem was about low latency vm initialization. I've asked if there are slides or repo online over on the rust meetup discord.

#

He said one of the big advantages of this particular tool: https://github.com/google/zerocopy/tree/main/anneal

Is LLMs have a really good handle on Lean

GitHub

zerocopy/anneal at main · google/zerocopy

Zerocopy makes zero-cost memory manipulation effortless. We write unsafe so you don’t have to. - google/zerocopy

fading sage Apr 22, 2026, 3:53 PM

#

What was the utility that used lean for verification though?

muted moss Apr 22, 2026, 8:13 PM

#

It was some memory fork trick with a low latency VM, I don't remember the specific details

#that's cool, what were they using for