About us
We are interested in the Rust programming language, its ecosystem, and its contributors. We occasionally meet to talk about these things.
Find our Discord, live streams, and Rust job matching programs via https://rusteastcoast.com
Upcoming events
2
Rust NYC: Formally Verified Rust & SAT Solvers
Datadog, New York Times Bldg, 620 8th Avenue, 45th Floor, New York, NY, USJoin us on Tuesday, April 21 at Datadog Times Square. Doors open at 6:30 p.m. to give attendees plenty of time to grab pizza and socialize, and the talk begin at 7:15 p.m. Following the success of the UnConf we've absorbed all of your feedback and have two awesome speakers!
Tynan Daly – CEO at High Dimensional Research
Verifying Your Rust, Formally.Tynan Daly studied mathematics at Bates College with a focus in algebraic topology before spending a decade in ML research, where he productionalized one of the first transformer models in 2018 for dynamic pricing. He is the founder of High Dimensional Research, where he builds formal verification tools for coding agents, translating Rust into Lean specifications for correctness proofs. As coding agents write more of our software, Tynan believes the tooling to verify that software needs to keep pace. He brings a mathematician's instinct for rigor to the practical problem of trusting code at scale.
As coding agents produce more of the code we ship, the volume is outpacing what review alone can catch but in systems where failure matters, "trust but don't verify" isn't an option. This talk explores how formal verification can close that gap. Tynan will introduce Lean as a proof assistant and explain why, despite its power, rewriting your Rust codebase in Lean isn't the answer. Instead, he'll walk through how tools like Hermes and Aeneas bridge the two languages, letting you write Rust and verify it against Lean specifications. He'll demo what this looks like in practice and make the case that formal verification is the same bet Rust developers already made with memory safety: accepting upfront rigor to eliminate entire classes of bugs before your code ever runs.
Bob McNaughton – Director of Engineering at UBS
Use a Rust SAT Solver to play pickleball!Bob's career began last century, writing C++ and assembler for what was then Australia's only telecom company. Somehow, he ended up writing Go for financial companies in New York. He also managed to pick up degrees from Universities on both continents. He is not sure what the next step will be, but it looks like it will involve Rust. His self assessed USA Pickleball Association skill rating is probably somewhere around 2.5.
Many years ago, when I was an undergraduate CS student, my professor informed me that the Boolean Satisfiability problem was NP-Complete. I took this to mean it was not something I should waste any time thinking about or expect to be a useful tool in the future. Then, many years later, I was attending a Meetup involving some live coding, and the presenter casually imported a SAT solver library, fed it some boolean variables and conditions, and out popped a solution! Then, several weeks later at a Rust meetup, a different presenter equally casually imported a CSP library, and used it to solve a challenging scheduling problem.
Lawrence Harvey is Rust NYC's official recruitment partner, with Ross providing support as a co-organizer and financial support.
The space is generously sponsored by our partner Datadog.
94 attendeesRust NYC x OpenAI: Safer 'unsafe' & Barnum: The agentic workflow engine.
OpenAI, 295 Lafayette Street 3rd Floor, New York, NY, USPLEASE NOTE: FOR SECURITY PURPOSES, YOU MUST FILL OUT THE OPENAI SIGN UP PAGE AS WELL AS THIS, USE THIS LINK: Rust NYC x OpenAI - the password is Rust@OAI2026
Join us on Tuesday, April 28 at OpenAI NYC. Doors open at 6:15 p.m. to give attendees plenty of time to grab food, drinks and socialize, and the talk begin at a slightly earlier start time of 7:05pm.
Robert Balicki, Staff Engineer at Pinterest
Barnum: The missing workflow engine for agentic workflowsRobert Balicki is a staff engineer at Pinterest, where he works on the Web Platform team and helps the company adopt GraphQL. He previously worked on the relay team at Meta. He organizes the Rust NYC meetup, and his side projects include Isograph, an opinionated, compiler-driven framework for building data-driven apps (https://isograph.dev), and Barnum, the missing workflow engine for agentic workflows (https://barnum-circus.github.io).
Robert will be talking about Barnum, the missing workflow engine for agentic workflows. LLMs are incredibly powerful tools, and we're tasking them with increasingly complicated workflows, from writing code to controlling our computers. However, if the assigned task is too complicated, the LLMs become forgetful and cannot be relied upon to precisely execute the workflow. Plan mode helps, but it's also inherently difficult to express a complicated, tree-like, conditional workflow in a linear markdown file.
This is where Barnum comes in. The key insight of Barnum is that you can't build reliable tools upon a fundamentally unreliable primitive. So, instead of hoping that an inherently probabilistic agent can advance a deterministic state machine, we have the workflow invoke the agent. Developers provide Barnum with a detailed workflow, which the engine then drives. Tasks that are deterministic (such as type checking) are not sent to agents. Agents are asked to do just the minimal tasks where they are the best tool for the job (such as reading files and reasoning about them). This means it's structurally impossible for agents to wriggle out of requirements or cut corners, and because these invocations are ephemeral, there's no problem with context rot.
Don't want to bother writing a workflow? Don't worry, the APIs are fully statically typed and so agents are incredibly good at doing that part too.
Barnum has already been used successfully to generate hundreds of clean-up PRs, automatically performing complex migrations, remove dead code due to fully shipped experiments, power a RAG search engine and validate each claim in documentation. Turns out, precisely specifying the work up front increases the reliability of agents, allowing you to go much further than if you just YOLO'd it!Predrag Gruevski, Member of Technical Staff at OpenAI
Performance Wins at OpenAi scale: Safer 'unsafe' with Codex and MiriPredrag (https://predr.ag) is a performance engineer best known for his work on the cargo-semver-checks linter, the Trustfall query engine, and his blog post about debugging WiFi that only worked while it was raining. At OpenAI, Predrag works on distributed storage systems that power the training of frontier models.
At OpenAI scale, every millisecond counts. Rust is phenomenal for this out of the box, but occasionally `unsafe` is necessary to squeeze out the last drops of performance from a system. This talk is a case study of how we used unsafe Rust, Codex, and miri to ship a tricky optimization in a massive distributed system. We went from idea to production in record time — since we used Rust, everything worked on the first try!
Lawrence Harvey is Rust NYC's official recruitment partner, with Ross providing support as a co-organizer and financial support.
The space is generously sponsored by our partner OpenAI, who will have a number of their engineers from the Rust heavy teams present for you to mingle with and learn more about the Rust based projects they're currently building!
46 attendees
Past events
92
