x-rv-inc-buzz-vs-real-fv
Extract — Runtime Verification X: buzz vs real FV (response to Cherny)
Section titled “Extract — Runtime Verification X: buzz vs real FV (response to Cherny)”- URL: https://x.com/rv_inc/status/2102843017560510772
- Author: Runtime Verification (@rv_inc)
- Quotes: Cherny https://x.com/bcherny/status/2102543349102338309
- Read via: user-X
get_posts_by_ids(note_tweet full text) - Time (CST): 2026-09-24 03:30 CST
Claims (full note_tweet)
Section titled “Claims (full note_tweet)”Reactions split into two camps:
- Excitement about agent-driven formal-methods bug-finding workflow
- Skepticism in calling this formal verification
RV: both have a point.
- Decades of FM experience → “formal verification is the future of coding.”
- Agents on proof gen + code/specs raise the ceiling (even Linux kernel; cites their recent work).
- Don’t wait for end-to-end guarantees: already useful bugfinding via Specula’s TLA+ approach and RV’s K and Lean pipelines.
- Critical boundary:
“But proving something about a generated model isn’t automatically proving it about the code we run. For that, we need faithful translation, trusted language semantics, and trusted proof checkers.”
- Longer post promised.
Engagement (at fetch): ~4.9k impressions, 54 likes, 5 reposts, 3 replies.
DIY / fleet relevance
Section titled “DIY / fleet relevance”- Adopt RV’s three-trust chain for DIY Herdr gates: faithful model↔code link + semantics + checker before claiming product FV.
- Keep model CEx bugfinding (Cherny/Specula-style) as a first-class, lower-bar gate — valuable without overclaiming.
- Name-check Specula + K/Lean as production FM orgs’ agent-adjacent stacks.
- Brief overreach question: use this post as the “corrective framing” companion to Cherny.
Caveats
Section titled “Caveats”- Promotional / positioning post; “longer post coming soon” not fetched here.
- Kernel claim not evidenced in-thread.