Verifiers have bugs too: flaws found in QED prover and RISC-V Lean model
xennygrimmato_ · x · 2026-10-28
A thread shows formal verifiers themselves can be buggy:
- The QED SQL equivalence prover has unsoundness issues (GitHub): every real constant is parsed as f32 then squeezed into i32/i32, so distinct literals like 16777217.0 and 16777216.0 are proved equal — non-equivalent queries get proven equivalent, and out-of-range literals panic.
- Porting Theorem Labs' RISC-V model from Rocq to Lean surfaced two bugs: the decoder disagreed with the spec on five instruction encodings (rejecting four valid instructions and executing one reserved instruction real hardware traps on), and fdiv missed the underflow flag when a tiny result rounds up to the smallest normal. Neither appears to affect Anthropic's published results; Theorem Labs confirmed and fixed both within two days.
More from coding & agent
- Multimodal GraphRAG models missing and contradictory evidence for storm damage assessment — JeremyCMorgan · 2026-10-28
- Vibe coding in real life: 20 hours of personal-project work done in 2 — gleech · 2026-10-28
- LangChain open-sources Content Studio, a Slack design agent, and shares its harness design — BraceSproul · 2026-10-28
- "If AI can do it, humans shouldn't": team lets AI agent review PRs — Yuchenj_UW · 2026-10-28
- Sequoia, Citi and OpenAI launch No Limit: build a poker bot in 60 minutes, $100K grand prize — polynoamial · 2026-10-28
- Nyxis: a Lean framework with formally proven authorization safety for AI-written backends — udmrzn · 2026-10-28