Hydro merges Verus-checked commutativity proofs for distributed systems with zero hand-written specs
ShadajL · x · 2026-09-18
Developer Shadaj L merged a hydrolang feature building on Conor Power's PhD dissertation: Verus machine-checked proofs replacing manualproof! for commutativity annotations in the Hydro distributed stream-processing framework. Key design points:
- Users never write assertions — proof obligations are auto-generated by macros from the actual closure body;
- Proofs are shape-specific: fold/reduce requires equal final accumulators across both orders; map requires equal captured state plus equal output multisets (catching order-exposing outputs like running totals); filter requires matching decisions and retained multisets;
- Proofs flow through the generic property mechanism in q!, making reordering unobservable for every downstream effect.
A notable example of engineering formal verification into a dataflow framework with no hand-written specs.
More from coding & agent
- Pictify MCP Server lets AI assistants generate images, GIFs and PDFs from HTML/CSS — modelcontextprotocol · 2026-09-18
- convalytics adds read-only MCP analytics for Convex apps queryable from Claude — modelcontextprotocol · 2026-09-18
- Dev uses Codex to draft Slack replies that self-tune from what you actually send — alex_frantic · 2026-09-18
- New browser API proposal could verify email addresses without leaving the app — philnash · 2026-09-18
- Codex's Appshots feature, which grabs app metadata beyond screenshots, arrives on Windows — pvncher · 2026-09-18
- Muse Code 'crazy cheap and quite good': early take on Meta's coding model — AIandDesign · 2026-09-18