Hydro adds Verus-checked commutativity proofs without trusting LLM-written specs
ShadajL · x · 2026-09-23
Shadaj merged PR #3198 into hydro-project, adding machine-checked (Verus) proofs as an alternative to manual proofs for commutative = ... annotations in the Hydro language. Proof obligations are generated by macros from the actual closure body — users never write assertions — and are shape-specific:
- fold/reduce: final accumulator equal across both orders
- map: captured state equal and output multiset equal (catches order-exposing outputs like running totals)
- filter: captured state equal and retained multiset equal
The work builds on Conor Power's PhD dissertation, showing formal verification can be harnessed for distributed systems without trusting LLMs to write correct specs.
More from coding & agent
- Qwen 3.8 Flash Next plays Baldur's Gate 2 in a live agent experiment — Reasonable_Friend_77 · 2026-09-24
- Dev builds 100% local metasearch engine with DiffusionGemma on vLLM — bodonoghue85 · 2026-09-24
- Voice Agents Can't Tell Who's Talking: Voice Isolation Cuts WER from 23.3% to 6.2% — thetripathi58 · 2026-09-24
- Project Reportedly One-Shot by Claude Opus 5.5 With One Bug-Fix Prompt — Robert_Palgrave · 2026-09-24
- Dev spots aria-checked on a <button>: evidence vibe-coded LLM output isn't being challenged enough — jh3yy · 2026-09-24
- serve-sim adds iPhone Duo support with 3D model, camera dev, and agent-accessible tree inspection — Baconbrix · 2026-09-24