1. Oh shit, AI can do my job better than me 2. Software engineering is dead! 3. I can vibe code as much slop as I want! 4. Oh, things are not going well. Fable/Sol/Opus all suuuck 5. But what if I constrain the agent? Put it in a straitjacket? 6. Oh, the results are pretty good now. How do I go deeper? 7. *Orders 12 software engineering books from Amazon* 8. Software engineering is alive!

People assume that in an AI doing formal verification world, they can take their existing codebase, ask AI to prove it correct, and get either a proof or a bug. Sadly reality has a few bones to pick with this, and one of them is the "existing codebase" part. And that's due to the good ol' halting problem. The short of it is that there is no general purpose algorithm that takes any program and input and correctly determines whether it will terminate or run forever. With a few mathematical flourishes we can extend that to "Rice's theorem" and prove this is true for any nontrivial semantic property, meaning we can't automatically prove arbitrary things about arbitrary programs. Now obviously we can prove some things about some programs, or else formal verification wouldn't exist as a field. The trick is that we write the code in a style suitable for verification. One example of this is totality: in Lean, all functions must be guaranteed to return a value for all inputs. If we want some code that runs forever (like f.ex a server), instead of `while true` we do `while (i < 10^60)` so that it's guaranteed to terminate and return a value (after the end of the universe). (Totality is also why, in Lean, `1/0 == 0`. If you convert your code to Lean without accounting for this, you could have correct lean but incorrect code!) Another "style" we use is state machines. Even if your code doesn't quite fit an SM architecture, if you want to prove it at scale, you're probably going to go with a state machine. State machines are the carcinisation of provable code. Hopefully by now the problem is clearer: even if your codebase is objectively correct, it might not be in the right shape to be proven correct! Okay, just have the AI rewrite your codebase into another form, right? Two problems. One: you don't know if you've introduced errors in the rewrite because you can't prove them equivalent (since one of them is not in a provable shape). Two: making code more verifiable can make it worse on other metrics, like modifiability, performance, and complexity. And now you've got the old bugbear of software engineers, the dreaded tradeoff. Now, don't get me wrong, formal verification has a huge role in the future of software, but it's not going to be a breezy "prove my Ruby thx" Claude prompt. It's still going to take work and expertise on our parts to prove our code, and to strike the right balance between formal verification and other forms of correctness. This is one reason I'm so excited to be working at @AntithesisHQ , which tackles a lot of the same properties as proof methods, but verifies them with "deterministic simulation testing" and fuzzing instead of with a proofs. So it's not as thorough and doesn't give you confidence in all inputs, but it automatically works on pretty much any code shape. I've literally grabbed open source projects off Github, told Claude "check properties XYZ in Antithesis thx", and gotten bug reports back. No state machine rewrites needed.

Agent code quality may look worse to a human observer, but in my experience agent build quality is better. Features have less bugs on launch and tend to "just work", whereas human-driven builds always tended to be myopic and fail for embarrassing reasons.

We put together a practical reference to formal verification tools: quint.sh/guides/formal-verif… If you're getting started, use it to explore the landscape. If you're already an expert, help us make it better. If you find a missing tool or any mistake, please tell us! We want this to be an accurate, useful, and current reference.

I don't mean to sound arrogant by saying this, but I just think it is just true that if people learned more neuroscience, and had a better idea how the human nervous system and brain actually works, then they would be better prepared to understand how machine intelligence is really not the same as human intelligence For example, neural networks are sort of loosely inspired by cortex, but that's about it I'm not trying to be a dick, but it's hard to have conversations on here sometimes because people's level of knowledge is just so low

Prediction: within ~1 year, formal methods will produce a capability spike in AI-assisted coding comparable in magnitude to the jump from GPT-2 to Astra.