We spent fifty years making proofs impossible to fake. Then we let the coding agent pick what to prove. A research paper this month put a number on it.* AI wrote the formal spec, AI wrote the proof, the verifier accepted both. Then humans read the specs. Close to 60% proved something other than what the author meant. Not wrong proofs. Wrong specs. The verifier was right every time. That's the problem. Left to choose, the agent picks properties that are easy to prove and say nothing about the program, and the checker can't tell a useless theorem from a useful one. I'm calling it vibe verification: the agent writes the spec and the proof, the checker goes green, nobody reads the spec. This applies to Verus, Lean, Bend, TLA+, Dafny, [insert favorite formal language here]. Here's an example of an agent failing at something that feels too simple to fail: Ask for a verified sort. It writes a spec that says "the output is sorted" and proves it. What the spec never says is that the output has the same elements as the input, so a function that returns an empty list satisfies it, and the verifier accepts the proof. Trivially satisfiable specs are the default failure, not an edge case. Here's a formula that actually works. Don't say "formally verify the codebase." Say "show that [property] holds in [component]." A property is a precondition (true going in), a postcondition (true coming out), or an invariant (stays true the whole time). For example, "A session token is never accepted after the logout that revoked it" is a good invariant. The bottleneck is moving from code review to intent review, and the spec is where intent lives. So: read the spec before the code. Write 3 inputs it must accept and 3 it must reject. Treat a model-written spec with utmost paranoia and rely on your judgement as an engineer. Formal verification for software doesn't automatically create trust, it moves it, from the code to the spec. If a human didn't read the spec, you didn't verify anything. You vibe-verified it. Follow me for more on verification and agentic engineering. * Wang, Jiang, Liu et al., "VerusEval: Evaluating LLM-Generated Verus Specifications Beyond Verifier Acceptance", Shenzhen University, arXiv 2610.26464, October 2026

Where we started (left, 1979) vs. where we are now (right, 2026)

Everyone wants to draw conclusions about the future based on what they saw in the past. Usually this works really well for people, so why stop now?

The NCSC is encouraging UK organisations to prepare for immediate updating of systems using PHP. Where immediate remediation is not feasible, organisations should consider taking the system offline until it can be fully mitigated. For more⬇️ ncsc.gov.uk/news/critical-se…

iykyk