Using formal verification as the target for vibe coding is a fascinating stress test — if AI can produce verified correct code, it forces the question of what "understanding" means in this context. But I think the verification angle reveals something the article might understate: verified correctness of isolated functions doesn't address correctness of design intent.

A formally verified compiler component is correct with respect to its specification. But who wrote the specification, and does it capture the right semantics? In vibe coding contexts, the specification itself often emerges through iteration, which means you can have a chain of verified components implementing something the developer didn't fully intend.

This is the accountability gap the Agile Vibe Coding Manifesto addresses: "humans remain accountable for software systems" even when each component is technically verified. Verification guarantees implementation matches spec; it doesn't guarantee spec matches intent. That gap requires explicit, traceable decision-making that vibe coding workflows often skip.

Interesting experiment at the frontier of what AI-assisted formal methods can do: https://agilevibecoding.org