16 ms·

When AI writes the software, who verifies it?

• rademaker 8mo ago
  In his latest essay, Leonardo de Moura makes a compelling case that if AI is going to write a significant portion of the world’s software, then verification must scale alongside generation. Testing and code review were never sufficient guarantees, even for human-written systems; with AI accelerating output, they become fundamentally inadequate. Leo argues that the only sustainable path forward is machine-checked formal verification — shifting effort from debugging to precise specification, and from informal reasoning to mathematical proof checked by a small, auditable kernel. This is precisely the vision behind Lean: a platform where programs and proofs coexist, enabling AI not just to generate code, but to generate code with correctness guarantees. Rather than slowing development, Lean-style verification enables trustworthy automation at scale.
• righthand 8mo ago
  No one really. Code is for humans to read and for machines to compile and execute. Llms are enabling people to just write the code and not have anyone read it. It’s solving a problem that didn’t really exist (we already had code generators before llms). It’s such an intoxicating copyright-abuse slot machine that a buddy who is building an ocaml+htmx tree editor told me “I always get stuck and end up going to the llm to generate code. Usually when I get to the html part.” I asked if he used a debugger before that, he said “that’s a good idea”.
  • galbar 8mo ago
    This is something I've been wondering about... If boilerplate was such a big issue, we should have worked on improving code generation. In fact, many tools and frameworks exist that did this already: - rails has fantastic code generation for CRUD use cases - intelliJ IDEs have been able to do many types of refactors and class generation that included some of the boilerplate I haven't reached a conclusion on this train of thought yet, though.
    • righthand 8mo ago
      Pre-llm corpos my thoughts were that we should be training juniors on code generators. Instead we’re somewhere between rtfm or dont.
  • hrmtst93837 8mo ago
    [flagged]
    • righthand 8mo ago
      I stopped worrying about that and just write code and do the debugging. Why pay for speed when the cruising lane is perfectly acceptable?
• acedTrex 8mo ago
  No one does currently, and its going to take a few very painful and high profile failures of vital systems for this industry to RELEARN its lesson about the price of speed. In fact it will probably need to happen a few times PER org for the dust to settle. It will take several years.
  • arscan 8mo ago
    Sure but industry cares about value (= benefit - price), not just price. Price could be astronomical, but that doesn’t matter if benefit is larger.
  • jcgrillo 8mo ago
    I feel like people used to talk about nines of uptime more. As in more than one. These days we've lost that: https://bsky.app/profile/jkachmar.com/post/3mg4u3e6nak2p https://bsky.app/profile/jkachmar.com/post/3mg4u3e6nak2p I recall a time, maybe around 2013-2017, when people were talking about 4 or 5 nines. But sometime around then the goalposts shifted, and instead of trying to make things as reliable as possible, it started becoming more about seeing how unreliable they can get before anyone notices or cares. It turns out people will suffer through a lot if there's some marginal benefit--remember what personal computers were like in the 1990s before memory protection? Vibe coding is just another chapter in that user hostile epic. Convenient reliability, like this author describes, (if it can be achieved) might actually make things better? But my money isn't on that.
• foolfoolz 8mo ago
  no one wants to believe this but there will be a point soon when an ai code review meets your compliance requirements to go to production. is that 2026? no. but it will come
  • righthand 8mo ago
    We already have specifications though, so that’s not different. What happens when the AI is wrong and wont let anyone deploy to production?
• oakpond 8mo ago
  You do. Even the latest models still frequently write really weird code. The problem is some developers now just submit code for review that they didn't bother to read. You can tell. Code review is more important than ever imho.
  • MrDarcy 8mo ago
    It is remarkably effective to have Claude Code do the code review and assign a quality score, call it a grade, to the contribution derived from your own expectations of quality. Then don’t even bother looking at C work or below.
    • NitpickLawyer 8mo ago
      IME it works even better if you use another model for review. We've seen code by cc and review by gpt5.2/3 work very well. Also works with planning before any coding sessions. Gemini + Opus + GPT-xhigh works to get a lot of questions answered before coding starts.
  • sausagefeet 8mo ago
    I agree with you. But I have to say, it is an uphill battle and all the incentives are against you. 1. AI is meant to make us go faster, reviews are slow, the AI is smart, let it go. 2. There are plenty of AI maximizers who only think we should be writing design docs and letting the AI go to town on it. Maybe, this might be a great time to start a company. Maximize the benefits of AI while you can without someone who has never written a line of code telling you that your job is going to disappear in 12 months. All the incentives are against someone who wants to use AI in a reasonable way, right now.
    • redhed 8mo ago
      I actually agree with good time to start a company. Lot of available software engineers that can actually understand code, AI at a level that can actually speed up development, and so many startups focusing on AI wrapper slop that you can actually make a useful product and separate yourself from the herd. Or you can be a grifter and make some AI wrapper yourself and cash out with some VC investment. So good time for a new company either way.
• _pdp_ 8mo ago
  I think the issue goes even deeper than verification. Verification is technically possible. You could, in theory, build a C compiler or a browser and use existing tests to confirm it works. The harder problem is discovery: how do you build something entirely new, something that has no existing test suite to validate against? Verification works because someone has already defined what "correct" looks like. There is possible a spec, or a reference implementation, or a set of expected behaviours. The system just has to match them. But truly novel creation does not have ground truth to compare against and no predefined finish line. You are not just solving a problem. You are figuring out what the problem even is.
  • Avshalom 8mo ago
    Well that's a problem the software industry has been building for itself for decades. Software has, since at least the adoption of "agile" created an industry culture of not just refusing to build to specs but insisting that specs are impossible to get from a customer.
    • pydry 8mo ago
      Agile is a pretty badly defined beast at the best of times but even the most twisted interpretation doesnt mean that. It's mainly just a rejection of BDUF.
    • daveguy 8mo ago
      Agile hasn't been insisting that specs are impossible to get from a customer. They have been insisting that getting specs from a customer is best performed as a dynamic process. In my opinion, that's one of agile's most significant contributions. It lines up with a learning process that doesn't assume the programmer or the customer knows the best course ahead of time.
      • skydhash 8mo ago
        And good luck when getting misaligned specs (communication issues customer side, docs that are not aligned with the product,...). Drafting specs and investigating failure will require both a diplomat hat and a detective hat. Maybe with the developer hat, we will get DDD being meaningful again.
• holtkam2 8mo ago
  At the end of the day you need humans who understand the business critical (or safety critical) systems that underpin the enterprise. Someone needs to be held accountable when things go wrong. Someone needs to be able to explain to the CEO why this or that is impossible. If you want to have AI generate all the code for your business critical software, fine, but you better make sure you understand it well. Sometimes the fastest path to deep understanding is just coding things out yourself - so be it. This is why the truly critical software doesn’t get developed much faster when AI tools are introduced. The bottleneck isn’t how fast the code can be created, it’s how fast humans can construct their understanding before they put their careers on the line by deploying it. Ofc… this doesn’t apply to prototypes, hackathons, POCs, etc. for those “low stakes” projects, vibe code away, if you wish.
  • sjajzh 8mo ago
    I think this gets to the heart of it. We’re gonna see a new class of devs & software emerge that only use AI and don’t read the code. The devs that understand code will still exist too, but there is certainly an appetite for going faster at the cost of quality. I personally find the “move fast and break thing” ethos morally abhorrent, but that doesn’t make it go away.
• lgl 8mo ago
  I'm in the process of building v2.0 of my app using opus 4.6 and largely agree with this. It's pretty awesome but still does a lot of basic idiotic stuff. I was implementing a feature that required a global keyboard shortcut and asked opus to define it, taking into account not to clash with common shortcuts. He built a field where only one modifier key was required. After mentioning that this was not safe since users could just define CTRL+C for the shortcut and we need more safeguards and require at least two modifier keys I got the usual "you're absolutely right" and proceeded to require two modifier keys. But then it also created a huge list of common shortcuts into a blacklist like copy, cut, paste, print, select all, etc.. basically a bunch of single modifier key shortcuts. Once I mentioned that since we're already forcing two modifier keys that's useless it said I'm right again and fixed it. The counter point of this idiocy is that it's very good overall at a lot of what is (in my mind) much more complicated stuff. It's a .NET app and stuff like creating models, viewmodels, usercontrols, setting up the entire hosting DI with pretty much all best practices for .net it does it pretty awesomely. tl;dr is that training wheels are still mandatory imho
• aplomb1026 8mo ago
  [flagged]
• indymike 8mo ago
  Because of the scale of generated code, often it is the AI verifying the AI's work.
  • tartoran 8mo ago
    So who's verifying the AI doing the verifying or is it yet another AI layer doing that? If something goes wrong who's liable, the AI?
    • visarga 8mo ago
      You have 2 paths - code tests and AI review which is just vibe test of LGTM kind, should be using both in tandem, code testing is cheap to run and you can build more complex systems if you apply it well. But ultimately it is the user or usage that needs to direct testing, or pay the price for formal verification. Most of the time it is usage, time passing reveals failure modes, hindsight is 20/20.
  • ptnpzwqd 8mo ago
    I of course cannot say what the future holds, but current frontier models are - in my experience - nowhere near good enough for such autonomy. Even with other agents reviewing the code, good test coverage, etc., both smaller - and every now and then larger - mistakes make their way through, and the existence of such mistakes in the codebase tend to accellerate even more of them. It for sure depends on many factors, but I have seen enough to feel confident that we are not there yet.
• simonw 8mo ago
  The "Nearly half of AI-generated code fails basic security tests" link provided in this piece is not credible in my opinion. It's a very thinly backed vendor report from a company selling security scanning software.
• muraiki 8mo ago
  The article says that AWS's Cedar authorization policy engine is written in Lean, but it's actually written in Dafny. Writing Dafny is a lot closer to writing "normal" code rather than the proofs you see in Lean. As a non-mathematician I gave up pretty early in the Lean tutorial, while in a recent prototype I learned enough Dafny to be semi-confident in reviewing Claude's Dafny code in about half a day. The Dafny code formed a security kernel at the core of a service, enforcing invariants like that an audit log must always be written to prior to a mutating operation being performed. Of course I still had bugs, usually from specification problems (poor spec / design) or Claude not taking the proof far enough (proving only for one of a number of related types, which could also have been a specification problem on my part). In the end I realized I'm writing a bunch of I/O bound glue code and plain 'ol test driven development was fine enough for my threat model. I can review Python code more quickly and accurately than Dafny (or the Go code it eventually had to link to), so I'm back to optimizing for humans again...
  • dranov 8mo ago
    Cedar used to be written in Dafny, but AWS abandoned that implementation and rewrote it in Lean. https://aws.amazon.com/blogs/opensource/lean-into-verified-software-development/ https://aws.amazon.com/blogs/opensource/lean-into-verified-s...
    • muraiki 8mo ago
      Oh whoops, thank you for the correction! I didn't realize that.
  • cpeterso 8mo ago
    Looks like LLMs also find Dafny easier to write than Lean. This study, “A benchmark for vericoding: formally verified program synthesis”, reports: > We present and test the largest benchmark for vericoding, LLM-generation of formally verified code from formal specifications … We find vericoding success rates of 27% in Lean, 44% in Verus/Rust and 82% in Dafny using off-the-shelf LLMs. https://arxiv.org/html/2509.22908v1 https://arxiv.org/html/2509.22908v1
• bitwize 8mo ago
  Also AI.
• yoaviram 8mo ago
  I just finished writing a post about exactly this. Software development, as the act of manually producing code, is dying. A new discipline is being born. It is much closer to proper engineering. Like an engineer overseeing the construction of a bridge, the job is not to lay bricks. It is to ensure the structure does not collapse. The marginal cost of code is collapsing. That single fact changes everything. https://nonstructured.com/zen-of-ai-coding/ https://nonstructured.com/zen-of-ai-coding/
  • MattDaEskimo 8mo ago
    Accountability then
    • yoaviram 8mo ago
      Anticipating modes of failure, creating tooling to identify and hedge against risks.
      • sjajzh 8mo ago
        If we could do this it would have been done already. Outsourced devs would be ubiquitous.
  • skydhash 8mo ago
    > I just finished writing a post about exactly this. Software development, as the act of manually producing code, is dying. It was never that. Take any textbook on software engineering and the focus was never the code, but on systems design and correctness. I'm looking at the table of contents of one (Software Engineering by David C. Kung) and these are a few sample chapters: ... 4. Software Requirement Elicitation 5. Domain Modelling 6. Architectural Design ... 8. Actor-System Interaction Modeling 9. Object Interaction Modeling ... 15. Modeling and Design of Rule-Based Systems ... 19. Software Quality Assurance ... 24. Software Security What you're talking about was coding, which has never been the bottleneck other than for beginners in some programming languages.
  • shinycode 8mo ago
• madrox 8mo ago
  I encourage everyone to RTFA and not just respond to the headline. This really is a glimpse into where the future is going. I've been saying "the last job to be automated will be QA" and it feels more true every day. It's one thing to be a product engineer in this era. It's another to be working at the level the author is, where code needs to be verifiable. However, once people stop vibing apps and start vibing kernels, it really does fundamentally change the game. I also have another saying: "any sufficiently advanced agent is indistinguishable from a DSL." I hadn't considered Lean in this equation, but I put these two ideas together and I feel like we're approaching some world where Lean eats the entire agentic framework stack and the entire operating system disappears. If you're thinking about building something today that will still be relevant in 10 years, this is insightful.
  • charlieflowers 8mo ago
    > "any sufficiently advanced agent is indistinguishable from a DSL." I don't quite follow but I'd love to hear more about that.
    • esafak 8mo ago
      https://en.wikipedia.org/wiki/Clarke's_three_laws https://en.wikipedia.org/wiki/Clarke's_three_laws
      • charlieflowers 8mo ago
        No i get the clarke reference. But how is an agent a dsl?
        • whattheheckheck 8mo ago
          Maybe not an agent exactly but I can see an agentic application is kind of like a dsl because the user space has a set of queries and commands they want to direct the computer to take action but they will describe those queries and commands in English and not with normal programming function calls
    • 8mo ago
• deleted 8mo ago
  [deleted]
• 50lo 8mo ago
  One thing that seems under-discussed in this space is the shift from verifying programs to verifying generation processes. If a piece of code is produced by an agent loop (prompt -> tool calls -> edits -> tests), the real artifact isn’t just the final code but the trace/pipeline that produced it. In that sense verification might look closer to: checking constraints on the generator (tests/specs/contracts), verifying the toolchain used by the agent, and replaying generation under controlled inputs. That feels closer to build reproducibility or supply-chain verification than traditional program proofs.
• deleted 8mo ago
  [deleted]
• mentalgear 8mo ago
  > Where this leads is clear. Layer by layer, the critical software stack will be reconstructed with mathematical proofs built in. The question is not whether this happens, but when.
• boznz 8mo ago
  This is the biggest problem going forward. I wrote about the problem many times on my blog, in talks, and as premises in my sci-fi novels Sitting in your cubical with your perfect set of test suites, code verification rules, SOP's and code reviews you wont want to hear this, but other companies will be gunning for your market; writing almost identical software to yours in the future from a series of prompts that generate the code they want fast, cheap, functionally identical, and quite possibly untested. As AI gets more proficient and are given more autonomy (OpenClaw++) they will also generate directly executable binaries completely replacing the compiler, making it unreadable to a normal human, and may even do this without prompts. The scenario is terrifying to professional software developers, but other people will do this regardless of what you think, and run it in production, and I expect we are months or just a few years away from this. Source code of the future will be the complete series of prompts used to generate the software, another AI to verify it, and an extensive test suites.
  • skydhash 8mo ago
    How do you get an extensive test suite?
    • boznz 8mo ago
      I wish I had a crystal ball to know how this will play out in the future, will a different AI create it from the SOP? How will humans fit in? For me with any new release of my winery production software I re-ran every job put into my clients production systems from job #1, about 200,000 jobs; Before going into production we checked all the balances, product compositions and inventory from this new software matches what the old system currently says. Takes about an hour to re-run fifteen years production and even a milliliter, or milligram difference was enough to trigger a stop/check. We had an extensive set of input data I could also feed in, to ensure mistakes were caught there too. I expect other people do it there own way, but as a business this would be the low bar of testing I would expect to be done.
  • Aldipower 8mo ago
    If you need to interact with some things in platform.openai.com, you know it is not months away, it is there already now. I had to go through forms and flows there, so buggy and untested, simply broken. They really eat their own dog food. Interacting with the support, resulted in literally weeks of ping pong between me and AI smoothed replies via email to fix their bugs. Terrible.
• bryanlarsen 8mo ago
  You can use AI to make a reviewers job much easier. Add documents, divide your MR into reviewable chunks, et cetera. If reviewing is the expensive part now, optimize for reviewability.
• sslayer 8mo ago
  State Sponsored Hackers AI will verify it.
• chromaton 8mo ago
  TFA seems to be big on mathematical proof of correctness, but how do you ever know you're proving the right thing?
• anonhacker199 8mo ago
  The biggest issue right now is most AI tools aren't hooked up appropriately to an environment they can test in (Chrome typically). Replit works extremely well because it has an integrated browser and testing strategy. AI works very well when it has the ability to check its own work.
• slopinthebag 8mo ago
  LLM generated code combined with formal verification just feels like we're entering the most ridiculous timeline. We know formal verification doesn't work at scale, hence we don't use it. We might get fully vibe coded systems but we sure as hell won't be able to verify them. The collapse of civilisation is real.
• bdcravens 8mo ago
  The same ones who verify it when I write it: my customers in production! /s (well, maybe /s)
• ozten 8mo ago
  This is really great and important progress, but Lean is still an island floating in space. Too hard to get actual work done building any real world system.
• nemo44x 8mo ago
  I believe the old ways, which agile destroyed, will come back because the implementation isn’t the hardest part now. Agile recognized correctly that implementation was the hard part to predict and that specification through requirements docs, UML, waterfall, etc. were out of date by the time the code was cooked. I don’t think we’ll get those exact things back but we will see more specification and design than we do today.
  • bwestergard 8mo ago
    Agile was a response to the coordination problems in certain types of firms. Waterfall persisted in organizations that have and require a more traditional bureaucratic structure. Waterfall makes sense if you are building a space probe or an unemployment insurance system, agile makes sense if you are trying to find product market fit for a smartphone app.
    • nemo44x 8mo ago
      Yeah and why I don’t think we’ll go back to that exactly. But software designed more deliberately and requirements that are more detailed and “documented” if that’s the right word?
  • miraculixx 7mo ago
    Sure because it worked great when we tried last time, right? Just spec it out first, and AI will churn out the perfect app. Not. For anyone who hasn't worked in a waterfall project and would like to try: You are kidding yourself. There is no such thing as a perfect spec. Read that again and say it outloud. It took humanity 50 years to figure out that perfect specs are impossible, unless of course you know exactly(!) what you need. And even then, the specs are never complete. The reality is that we often don't know, and can't know, what we want, exactly, until we actually see and experience what we said we wanted. Then we adjust. Try again. That's the reality for individuals already. By simply using logic we can deduct that entities made of more than one individual, aka companies, will not behave better. They just make it look better by giving you a nice document that says "we want this!", only to then come around when they see what they got, and to claim "wait, we didn't mean it like so!". That's just human nature. Not much we can do. AI will not change that. So when some people think AI will deliver perfect software given perfect specs, hence we have to write the specs first! That is just missing the boat my a mile. Agile is not a process but a human-friendly way of doing things. It simply says hey you want this? Let me build that and show you. Then let's adjust or move to the next thing. Rinse and repeat. Agile works because it matches how humans think and act. Step by step, day by day.
• dataviz1000 8mo ago
  100% of my innovation for the past month has been getting the coding agent to iterate with an OODA loop (I make it validate after act step) trying to figure out how to get it to not stop iterating. For example, I have discovered there is a big difference between prompting 'there is a look ahead bias' and 'there is a [T+1] look ahead bias' where the later will cause it to not stop until it finds the [T+1] look ahead bias. It will start to write scripts that will `.shift(1)` all values and do statistical analysis on the result set trying to find the look ahead bias. Now, I know there isn't look ahead bias, but the point is I was able to get it to iterate automatically trying different approaches to solve the problem. The software is going to verify itself eventually, sooner than later.
  • macrolet 8mo ago
    Your post is not clear to me. What did you innovate? Your example is unclear.
• drivebyhooting 8mo ago
  That was a prolix and meandering essay. Next time I’d rather just look at the prompts and hand edits that went into writing it rather than the final artifact; much like reviewing the documentation, spec, and proof over the generated code as extolled by the article.
• phyzome 8mo ago
  Verify? Seems like no one is even reviewing this stuff.
• furyofantares 8mo ago
  (answering the title) The lusers
• ljlolel 8mo ago
  The users verify and fix it on the fly with the Claude VM JIT https://jperla.com/blog/claude-is-a-jit https://jperla.com/blog/claude-is-a-jit
• csense 8mo ago
  It seems like sound testing methodology to identify important theorems related to the code, prove them, and then verify the proof. Verification gets sold as "bulletproof" but I'm skeptical for a couple reasons: - How do you establish the relationship between the code and the theorem? Lean theorem can be applied to zlib implemented in Lean, what if you want to check zlib implemented in a normal programming language like C, JS, Zig, or whatever? - How do you know the key properties mean what you think they mean? E.g. the theorem says "ZlibDecode.decompressSingle (ZlibEncode.compress data level) = .ok data" but it feels like it would be very easy to accidentally prove ∃ x s.t. decompress(compress(x)) == x while thinking you proved ∀ x, decompress(compress(x)) == x. I've tried Lean and Coq and...I don't really like them. The proofs use specialized programming languages. And they seem deliberately designed to require you to use a context explorer to have any hope of understanding the proof at all. OTOH a normal unit test is written in a general purpose programming language (usually the same one as the program being tested), I'm much more comfortable checking that a Claude-written unit test does what I think it's doing than a Claude-written Lean proof of correctness.
  • nextos 8mo ago
    Lean and Coq might not be the right choice. Perhaps something like Dafny, F*, or Why3, where code and theorems live together. Nevertheless, Lean 4 has closed the gap and it's closer to those than Coq at this stage.
  • anonymous6500 8mo ago
    The article does not reveal it to me either how the existing code would be mapped to Lean and back. The impression from zlib example is that I'd be expected to program in Lean. No way it's going to happen. The language is too complex for me and my average colleague. We're also not going to have two parallel implementations in ordinary language and Lean and compare them with 'differential random testing' (see https://aws.amazon.com/blogs/opensource/lean-into-verified-software-development/ https://aws.amazon.com/blogs/opensource/lean-into-verified-s... someone linked in the discussion), that's just too taxing for bigger products, let alone we typically don't have enough time to do one implementation right. The gap of having succinct, expressive, powerful and executable specification to be able to continuously verify AI-generated programs is real, but I don't see how Lean alone closes it. If the author's intention was to attract community to help build that out with Lean in the center, it's not clear to me where to even start. Since the author provided no hints or direction, I've a feeling it's not clear to them either.
• laalshaitaan 8mo ago
  Formal verification gets you to deploy with confidence but it's still a snapshot. What happens when real-world inputs drift from what you tested against? The subtler problem is runtime behavioral drift: an agent that's technically correct but consistently misunderstands a whole class of user queries is invisible to any pre-deploy check. Pre-deploy and post-deploy verification are genuinely different problems.
  • hackyhacky 8mo ago
    > What happens when real-world inputs drift from what you tested against? The whole point of formal verification is that you don't test. You prove the program correct mathematically for any input. > an agent that's technically correct but consistently misunderstands a whole class of user queries is invisible to any pre-deploy check The agent isn't verifying the program. The agent is writing the code that proves the program correct. If the agent misunderstands, it fails to verify the program.
• bfung 8mo ago
  When humans write the software, who verifies it? half sarcasm, half real-talk. TDD is nice, but human coders barely do it. At least AI can do it more!
  • nvlled 8mo ago
    > half sarcasm, half real-talk. If you could pause a bit from being awed by your own perceived insightfulness, you would think a just bit harder and realize that LLMs can generate hundreds of thousands of code that no human could every verify within a finite amount of time. Human-written software is human verifiable, AI-assisted human-written software is still human verifiable to some extent, but purely AI-written software can no longer be verified by humans.
    • nicbou 8mo ago
      That's a very unpleasant tone to take.
• faitswulff 8mo ago
  Someone actually did fuzz the claude c compiler: https://john.regehr.org/writing/claude_c_compiler.html https://john.regehr.org/writing/claude_c_compiler.html
• lateforwork 8mo ago
  The first thing you should have AI write is a comprehensive test suite. Then have it implement the main functionality. If the tests pass that is one level of verification. In addition you can have one AI check another AI's code. I routinely copy/paste code from Claude to ChatGPT and Gemini have them check each other's code. This works very well. During the process I have my own eyes verify the code as well.
  • void-star 8mo ago
    The advice that everyone seemed to agree on at least just a few months ago was to make sure _you_ write the comprehensive tests/specs and this is what I still would recommend doing to anyone asking. I guess even this may be falling out of fashion though…
    • p1necone 8mo ago
      Generate with carefully steered AI, sanity check carefully. For a big enough project writing actually comprehensive test coverage completely by hand could be months of work. Even state of the art AI models seem to have no taste, or sense of 'hang on, what's even the point of this test' so I've seen them diligently write hundreds of completely pointless tests and sometimes the reason they're pointless is some subtle thing that's hard to notice amongst all the legit looking expect code.
    • lateforwork 8mo ago
      There is no need to write tests manually. Just review the tests, and make sure there is good coverage, if there isn't ask AI for additional tests and give it guidance.
  • throwaway613746 8mo ago
    [dead]
  • sdiupIGPWEfh 8mo ago
    I was anticipating that having AI write code to pass tests (human and/or AI written tests) would be worthwhile, but in practice, I've found that even models such as Opus 4.6 Thinking, High Effort simply "cheats", or rather, fails to generalize much too often. It's occurred to me that perhaps I need some amount of randomness in the tests to keep the models honest, but it feels wrong. We'll see.
• p0u4a 8mo ago
  Someone once told me, agentic coding may lead to something akin to a "software engineering union" forming, where a set of guidelines control code quality. Namely, at least one of writing, testing, and reviewing of code must be done by a human.
• agenthustler 8mo ago
  [flagged]
• maltalex 8mo ago
  Maybe I'm missing something, but isn't this the same as writing code, but with extra steps? Currently, engineers work with loose specifications, which they translate into code. With the proposed approach, they would need to first convert those specifications into a formally verifiable form before using LLMs to generate the implementation. But to be production-ready, that spec would have to cover all possible use-cases, edge cases, error handling, performance targets, security and privacy controls, etc. That sounds awfully close to being an actual implementation, only in a different language.
  • hwayne 8mo ago
    The key bit is that specifications don't need to be "obviously computable", so they can be a lot simpler than the code that implements them. Consider the property "if some function has a reference to a value, that value will not change unless that function explicitly changes it". It's simple enough to express, but to implement it Rust needs the borrow checker, which is a pretty heavy piece of engineering. And proving the implementation actually guarantees that property isn't easy, either!
    • deleted 7mo ago
      [deleted]
  • nextos 8mo ago
    Formal specifications can be easier to write than code. Take refinement types in Dafny, for example. Because they are higher-level, you don't need to bother with tedious implementation details. By shifting our focus to formal specifications rather than manual coding, we could possibly leverage automation to not only develop software faster but also achieve a higher degree of assurance. Of course, this remains largely theoretical for now, but it is an exciting possibility. Note high-level specifications often overlook performance issues, but they are likely sufficient for most scenarios. Regardless, we have formal development methodologies able to decompose problems to an arbitrary level of granularity since the 1990s, all while preserving correctness. It is likely that many of these ideas will be revisited soon.
• heftykoo 8mo ago
  Another AI, obviously. And then a third AI to monitor the first two for conflicts of interest. Jokes aside, this is exactly the era where formal verification (like TLA+ or Lean, seeing the other post on the front page) actually makes commercial sense. If the code is generated, the only human output of value is the spec. We are moving from writing logic to writing constraints.
• roadbuster 8mo ago
  > The Claude C Compiler illustrates the other side: it optimizes for > passing tests, not for correctness. It hard-codes values to satisfy > the test suite. It will not generalize. This is one of the pain points I am suffering at work: workers ask coding agents to generate some code, and then to generate test coverage for the code. The LLM happily churns out unit tests which are simply reinforcing the existing behaviour of the code. At no point does anyone stop and ask whether the generated code implements the desired functional behaviour for the system ("business logic"). The icing on the cake is that LLMs are producing so much code that humans are just rubber stamping all of it. Off to merge and build it goes. I have no constructive recommendations; I feel the industry will keep their foot on the pedal until something catastrophic happens.
  • Herring 8mo ago
    > At no point does anyone stop and ask whether the generated code implements the desired functional behaviour for the system ("business logic"). Obvious question: why not? Let’s say you have competent devs, fair assumption. Maybe it’s because they don’t have enough time for solid QA? Lots of places are feature factories. In my personal projects I have more lines of code doing testing than implementation.
    • sarchertech 8mo ago
      It’s because people will do what they’re incentivized to do. And if no one cares about anything but whether the next feature goes out the door, that’s what programmers will focus on. Honestly I think the other thing that is happening is that a lot of people who know better are keeping their mouths shut and waiting for things to blow up. We’re at the very peak of the hype cycle right now, so it’s very hard to push back and tell people that maybe they should slow down and make sure they understand what the system is actually doing and what it should be doing.
      • shigawire 8mo ago
        Or if you say we should slow down your competence is questioned by others who are going very fast (and likely making mistakes we won't find until later). And there is an element of uncertainty. Am I just bad at using these new tools? To some degree probably, but does that mean I'm totally wrong and we should be going this fast?
• vicchenai 8mo ago
  The verification problem scales poorly with AI complexity. Current approaches rely on test suites, but AI-generated code tends to optimize for passing existing tests rather than correctness in the general case. What's interesting is this might be the forcing function that finally brings formal verification into mainstream use. Tools like Lean and Coq have been technically impressive but adoption-starved. If unverified AI code is too risky to deploy in critical systems, organizations may have no choice but to invest in formal specs. AI writes the software, proof assistants verify it. The irony: AI-generated code may be what makes formal methods economically viable.
• pnathan 8mo ago
  I am experimenting at a very early stage with using Verus in Rust to generate proveably correct Rust. I let the AI bang on the proof and trust the proof assistant to confirm it. There is another route with Lean where Rust generates the Lean and there is proof done there but I haven't chased that down fully. I think formal verification is a big win in the LLM era.
• mkoubaa 8mo ago
  PMs have been asking the same question about software developers for decades
• wyum 8mo ago
  I believe there is a Verification Complexity Barrier As you add components to a system, the time it takes to verify that the components work together increases superlinearly. At a certain point, the verification complexity takes off. You literally run out of time to verify everything. AI coding agents hit this barrier faster than ever, because of how quickly they can generate components (and how poorly they manage complexity). I think verification is now the problem of agentic software engineering. I think formal methods will help, but I don't see how they will apply to messy situations like end-to-end UI testing or interactions between the system and the real world. I posted more detailed thoughts on X: https://x.com/i/status/2027771813346820349 https://x.com/i/status/2027771813346820349
  • kaicianflone 8mo ago
    Thank you for the post. It's a good read. I'm working on governance/validation layers for n-LLMs and making them observable so your comments on runaway AIs resonated with me. My research is pointing me to reputation and stake consensus mechanisms being the validation layer either pre inference or pre-execution, and the time to verify decisions can be skipped with enough "decision liquidity" via reputation alone aka decision precedence.
  • thorn 8mo ago
    Very deep post on the problem. AI seems to worsen the issue of software correctness and given the nature of business, it won’t be ever solved.
  • codethief 8mo ago
    Hi William, thank you for the interesting post! > At a certain point, the verification complexity takes off. You literally run out of time to verify everything. Could you elaborate on this? Your post makes it sound as if the verification complexity diverged as the number of components n approaches a certain finite value n_0, but that seems unlikely to me. If, in contrast, the verification complexity remains finite at n_0, then verification should still be possible in finite time, shouldn't it? Yes, it might be a considerable amount of time but I assume your theorem doesn't predict lower bounds for the involved constants? Either way, this entire discussion assumes n will increase as more and more software gets written by AI. Couldn't it also be the opposite, though? AI might also lead us to removing unnecessarily complex dependencies from our software supply chain or stripping them down to the few features we need.
• Ronsenshi 8mo ago
  A bit unrelated to the article, more of a commentary about how many engineers at this point barely write any code or even do code review. It seems to me like a huge amount of engineers/developers in comments are turning into Tom Smykowski from The Office. Remember that guy? His job was to be a liaison between customers and engineers because he had "people skills": "I deal with the god damn customers so the engineers don't have to. I have people skills; I am good at dealing with people. Can't you understand that? What the hell is wrong with you people?" Except now, based on comments here it, some engineers are passing instructions from customers to AI because they have "AI skills". While AI is doing coding, helps with spec clarification, reviewing code and writing tests. That's scary and depressing. This field in a few years will be impossible to recognize.
• turlockmike 8mo ago
  This is where you can use adverserial systems. 1. Agent writes a minimal test against a spec. 2. Another agent writes minimal implementation to make test pass only. Repeat This is ping pong pair programming.
• midtake 8mo ago
  I do. I verify it so hard I've begun to mistrust it lately, seeing Gemini make glaring conceptual mistakes and refusing to align to my corrections.
• neya 8mo ago
  The fundamental problem is the verification loop for the average developer is grounded not in tests, but with results. Write code, reload browser, check output. Does it work the way I want? Good. We're done here. Not write code, write tests, ensure all test-cases are covered. Now, imagine such a flaky foundation is used to build on top of even more untested code. That's how bad quality software (that's usually unfixable without a major re-write) is born. Also, most vibe-coders don't have enough experience/knowledge to figure out what is wrong with the code generated by the AI. For that, you need to know more than the AI and have a strong foundation in the domain you're working on. Here is an example: You ask the AI to write the code for a comment form. It generates the backend and frontend code for you (let's say React/Svelte/Vue/whatever). The vibe-coder sees the UI - most likely written in Tailwind CSS and thinks "wow, that looks really good!" and they click approve. However, an experienced person might notice the form does not have CSRF protection in place. The vibe-coder might not even be aware of the concept of CSRF (let alone the top 10 OSWAP security risks). Hence, the fundamental problem is not knowing about the domain more than the AI to pick up the flaw. Unless this fundamental problem is solved - which I don't think it will anytime soon because everyone can generate code + UI these days, I don't see a solution to the verification problem. However, this is good news for consultants and the like because it creates more work down the line to fix the vide-coded mess because they got hacked the very next day and we can charge them a rush fee on top of it, too. So, it's not all that bad.
  • Spivak 8mo ago
    My impression has been with frontend tests is they come in two flavors: extremely hard to write to the point of impracticality, and useless. Most orgs settle for the latter and end up testing easily testable things like the final rendered dom and rely on human qa for all the hard bits like "does the page actually look like it's supposed to, does interacting with the UI elements behave correctly, and do the flows actually work." All largely stemming from the fact that tests can't meaningfully see and interact with the page like the end user will.
    • krackers 8mo ago
      >can't meaningfully see and interact with the page like the end user will Isn't this a great use case for LLM tests? Have a "computer use agent" and then describe the parameters of the test as "load the page, then navigate to bar, expect foo to happen". You don't need the LLM to generate a test using puppeteer or whatever which is coupled to the specific dom, you just describe what should happen.
• SurvivorForge 8mo ago
  The uncomfortable truth is that most teams were already bad at verification before AI entered the picture. The difference is that AI-generated code comes in faster, so the verification bottleneck becomes painfully obvious. I think the real opportunity here is that AI forcing us to think harder about specifications and correctness might actually improve the quality of human-written code too — it's making us confront the fact that "it works on my machine" was never real verification.
• Nevermark 8mo ago
  > When AI writes the software, who verifies it? The users. It's a start.
• phantomathkg 8mo ago
  Human writes the requirements, contains flaw. Human or AI translate that to specifications, and eventually code. It does not matter if the middle man is human or AI, or written in "traditional language" or "formal verification". Bugs will be there as human failed to defined a bullet proof requirements.
• saltyoldman 8mo ago
  the same agent that wrote it. it's not great now, but getting better each month. Agents will likely start performing visual testing, checking the database, etc... i don't think people understand quite how powerful these agents already are - or could be. In the next month someone will likely unlock new visual check agents (I mean it already happened but few people are using it so far).
• js8 8mo ago
  I think intelligence in general means solving (and manipulating) constraint problems. So when you ask AI to, say, write a "snake game", it figures out what this means in terms of constraints to all the possible source codes that can be written (so it will have things like the program is a game, so it has a score, there is a simple game world and there is user input connected to the display of the game world and all sorts of constraints like this), and then it further refines these constraints until it picks a point (from the space of all possible programs) that satisfies those constraints, more or less. One beautiful thing about current AI is that this process can handle fuzzy constraints. So you don't have to describe the requirements (constraints) exactly, but it can work with fuzzy sets and constraints (I am using "fuzzy" in the quite broad sense), such as "user can move snake head in 4 directions". Now, because of this fuzzy reasoning, it can sometimes fail. So the wrong point (source code) can get picked from the fuzzy set that represents "snake game". For example, it can be something buggy or something less like a canonical snake game. In that case of the failure, you can either sample another datapoint ("write another snake game"), or you can add additional constraints. Now, the article argues in favor of formal verification, which essentially means, somehow convert all these fuzzy constraints into hard constraints, so then when we get our data point (source code of the snake game), we can verify that it indeeds belongs to the (now exact) set of all snake games. So, while it can help with the sampling problem, the alignment problem still remains - how can we tell that the AI's (fuzzy) definition of a functional "snake game" is in line with our fuzzy definition? So that is something we don't know how to handle other than iteratively throwing AIs at many problems and slowly getting these definitions aligned with humans. And I think the latter problem (alignment with humans on definitions) is the real elephant in the room, and so the article is IMHO focusing on the wrong problem by thinking the fuzzy nature of the constraints is the main issue. Although I think it would definitely be useful if we had a better theoretical grasp on how AI handles fuzzy reasoning. As AI stands now, practicality has beaten theory. (You can formalize fuzzy logic in Lean, so in theory nothing prevents us from specifying fuzzy constraints in a formal way and then solving the resulting constraint problem formally, it just might be quite difficult, like solving an equation symbolically vs numerically.)
• mootoday 8mo ago
  AI of course
• 8note 8mo ago
  i think formal methods and math proofs will be useful like tests are for getting more feedback to the LLM to get to a working solution, but i dont think it at all solves the problem of "poisoned training data introduces specific bugs and vulnerabilities" the bug will also be introduced in the formal spec, and people will still miss it by not looking. i think fast response and fix time - anti-entropy - will win out against trying to increase the activation energy, to quote the various S3 talks. You need a cleanup method, rather than to prevent issues in the first place
• reenorap 8mo ago
  > Google and Microsoft both report that 25–30% of their new code is AI-generated. I think it's closer to 100%. I don't know anyone who isn't doing 100% ai-generated code. And we don't even code review it because why bother? If there's an error then we just regenerate the code or adjust the prompt.
• cagz 8mo ago
  > No one is formally verifying the result This might be the case for a hobby project or a start-up MVP being created in a rush, but in reality, there are a few points we may want to take into account: 1. Software teams I work with are maintaining the usual review practices. Even if a feature is completely created by AI. It goes through the usual PR review process. The dev may choose "Accept All", although I am not saying this is a good practice, the change still gets reviewed by a human. 2. From my experience, sub-agents intended for code and security review do a good job. It is even possible to use another model to review the code, which can provide a different perspective. 3. A year ago, code written by AI was failing to run the first time, requiring a painful joint troubleshooting effort. Now it works 95% of the time, but perhaps it is not optimal. Given the speed at which it is improving, it is safe to expect that in 6-9 months' time, it will not only work but will also be written to a good quality.
• signa11 8mo ago
  > When AI writes the software, who verifies it? oh thats quite simple: the dude / dudette who gets blamed is the one who verifies it.
• kazinator 8mo ago
  > What would a verification platform for the AI era require? A small, trusted kernel: a few thousand lines of code that check every step of every proof mechanically. The code is a stochastic parrot job produced with zero algorithmic understanding. Out of what magic unicorn's ass are you going to get a matching proof for it, to feed to this trusted kernel?
• __mharrison__ 8mo ago
  TDD...
• globular-toast 8mo ago
  I'm starting to think of this LLM thing a bit like fossil fuels. We've got fossil fuels that were deposited over millions of years, a timescale we are not even properly equipped to imagine. We've been tapping that reserve for a few decades and it's caused all kinds of problems. We've painted ourselves into a corner and can't get out. Now we've got a few decades worth of software to tap. When you use an LLM you don't create anything new, you just recycle what's already there. How long until we find ourselves in a very similar corner? The inability of people to think ahead really astounds me. Sustainability should be at the forefront of everyone's mind, but it's barely even an afterthought. Rather, people see a tap running and just drink from it without questioning once where the water is coming from. It's a real animal brain thing. It'll get you as far as reproducing, but that's about it.
• phyzix5761 8mo ago
  I found my best use of AI for writing code is with a TDD approach. I write 1 test, watch it fail, let the AI implement the solution, and then if I like it I commit. Write the next test and repeat. It keeps me in the loop, I'm testing actual functionality rather than code, and my code is always in a state where I can open a PR and merge it back to main.
• waterTanuki 8mo ago
  I've grown to hate using python in production since LLMs have been around. Python cannot enforce minimum standards like cleaning up unused variables, checking array access, and properly typing your functions. There's a number of tools built to do this but none of them can possibly replace a compiler. Compiled languages like Go and Rust are my new default for projects on the backend, typescript with strict typing on for the frontend, and I foresee the popularity growing the more LLM use grows. The moment you let an LLM loose in a Javascript/Python codebase everything goes off the rails.
• thorn 8mo ago
  I don’t think many people are interested in producing 100% correct code. I saw this at big companies and small startups. It is all the same: ship feature asap before competitors. Writing correct code is almost always punished indirectly in the way they only praise the feature delivering heroes that got promoted. Nobody got promoted for preventing bugs. Maybe in some other circles it is not like that, but I am sure that 90% of industry measures output in the amount of value produced and correct code is not the value you can show to the stockholders. It is sad state of affairs dictated by profit seeking way of life (capitalism).
  • Freak_NL 8mo ago
    Not value produced, but easily quantifiable value produced, I would say. There are lots of cases where some perfectly tweaked internal tool saves hours of work every week, or some mostly invisible (but crucial) project, application, or module just somehow always works. But the user never twigs they exist, and the customer doesn't care. The value is there (in saved hours, frustration, and stability), but it won't count.
    • thorn 8mo ago
      Yes, perceived value, I wanted to write. Your correction is spot on.
• milind-soni 8mo ago
  At this point, its the users
• titaniumrain 8mo ago
  a dinosaur...
• toastal 8mo ago
  Note that Lean doesn’t have a monopoly on verification languages. Dafney, Rocq, Why3, ATS, Agda, Idris… these all can do it too. The fact that Lean is controlled by Microsoft should cause folks pause considering how they are trying to monopolize so many other spaces… & the author works on Lean. Rather than comparing Lean to performance like OCaml/Haskell like the article does, Why3 is a superset of OCaml, Agda can compile to Haskell, & ATS2 compiles to C—rather than needing to adopt an entirely new language.
• KingOfCoders 8mo ago
  Most software the companies I worked for that was put into production, was not verified. There were spotty code reviews, mostly focusing on "I would have done it differently" and a limited amount of unit tests with low test coverage and Heisenberg E2E tests, often turned off because, Heisenberg. Sometimes overworked, bottle neck, testers. There is hope that with AI we get to better tested, better written, better verified software.
  • wolvesechoes 8mo ago
    > There is hope that with AI we get to better tested, better written, better verified software. And it is one thing we don't get for sure. This tech, in a different world, could be empowering common people and take some weight from their shoulders. But in this world its purpose is quite the opposite.
• raincole 8mo ago
  A little mental trick: every time you see a title with AI(or LLM or agent) and a question mark, replace 'AI' with 'humans' and ask the question again. The answer is no one, for most of the time.
• sublimefire 8mo ago
  At the end it mentions what the future engineers will do: > Engineers spend more time writing specifications and models, designing systems at a higher level of abstraction, defining precisely what systems must do, what invariants they must maintain, what failures they must tolerate. We do that already and the abstractions are very high. The other part is about knowing what the system is supposed to do way in advance, which is not how a lot of engineering is done because it is an exploratory problem. Very few of us write crypto or spend much time in a critical piece of code. And most importantly no user ever said if the software they buy is using proofs. Just like security these concerns are at the bottom of a barrel.
• voxleone 8mo ago
  What’s striking here is the convergence on a minimal axiomatic kernel (Lean) as the only scalable way to guarantee coherent reasoning. Some of us working on foundational physics are exploring the same methodological principle. In the “Functional Universe” framework[0], for example, we start from a small set of axioms and attempt to derive physical structure from that base. The domains are different, but the strategy is similar: don’t rely on heuristics or empirical patching; define a small trusted core of axioms and generate coherent structure compositionally from there. [0] https://voxleone.github.io/FunctionalUniverse https://voxleone.github.io/FunctionalUniverse
• liampulles 8mo ago
  Attention human: I have formally verified a route for converting the desks in the office into paperclips. Proceeding autonomously.
• amelius 8mo ago
  When AI writes the software, who is proud of it?
• geldedus 8mo ago
  The written specs and the acceptance tests.
• elif 8mo ago
  Users
• stpedgwdgfhgdd 8mo ago
  I don’t think this an AI specific problem, same can happen with humans.
• lenerdenator 8mo ago
  You verify it. The value proposition of a software engineer is no longer creating code; it is making sure that the ultra-fast code generating capability of the LLM fits the needs of the business. BDD/TDD, code reviews, deep dives on what the code does, and educating yourself on design patterns... all of these help.
• duxup 8mo ago
  It is wild to me how things SEEM to be playing out. With AI I code faster …. AND read / test more. I’m doing more verification than ever.
  • zackify 8mo ago
    Yeah exactly. I can't believe that people keep acting like everyone's just running hundreds of lines and no one's doing a code review. I find that I'm fastest when I iterate with it. If it's anything that's slightly ambiguous, I'm going to check as it goes and mention things during the edits it suggests.
• randusername 8mo ago
  > Most people think of verification as a cost, a tax on development, justified only for safety-critical systems. That framing is outdated. > The value is not in the verification workforce. It is in what verified delivery enables These takes misrepresent safety-critical software verification. The verification workforce is indispensable. Whereas the software engineers are usually highly specialized, the verification team owns the domain and project knowledge to make sure the whole thing integrates. They consult on requirements, anticipate oversights, build infrastructure and validate it, and execute the verification. So when the business needs a go / no-go call, they ask the verification lead. Automation and proofs have their place, but I don't see how verification without human accountability is workable.
• MickeyShmueli 8mo ago
  the test generation loop is brutal. i've been burned by this exact thing, you ask the agent to write code, then ask it to write tests for that code, and surprise, they all pass because the tests are literally just "does the code do what the code does" honestly think the answer isn't more tests, it's stricter contracts. like if your API has an OpenAPI spec, you can validate requests/responses against it automatically. the spec becomes the source of truth, not the tests, not the implementation we've been doing this backwards for years. write code, write tests that match the code, realize six months later that both the code and tests were implementing the wrong behavior. but if you have a machine-readable contract (openapi, json schema, whatever), at least you can verify one dimension automatically ngl this is why i'm skeptical of "AI will write all the code" takes. without formal specs, you're just getting really confident garbage that happens to pass its own tests. which tbh describes a lot of human-written code too lol
• flashbaby 8mo ago
  [flagged]
• testemailfordg2 8mo ago
  Time does...Microslop is an example
• ddanv 7mo ago
  So you feed the LLM some C code like zlib and it rewrites and proves it. The goal is to make the code write-only and replace it with spec declaration? ... math ppl still cant accept the "x = 1;" statement :)
• boristane007 7mo ago
  loving this! this is the proof of this love https://github.com/pravsingh/boris https://github.com/pravsingh/boris
• rcpffm 7mo ago
  extremely important, yes