On May 7, I gave a well-attended ACM Tech talk on “Software Verification in the Age of Artificial Intelligence”. There were more questions at the end than I had the time to answer, but I promised the participants that I would answer everything. In the meantime I had to finish my book AI for Smarties: Understanding Artificial Intelligence, but now that it is out I am coming back to this discussion. Thanks for all the great questions!
Yan Timanovsky, the organizer, provided me with the list of questions that had been written on the meeting chat and left unanswered. They are reproduced below. My plan is to provide answers — to those for which I can — over the next two or three weeks, so please come back once in a while.
The questions contained the name and email of each questioner; I removed this information to preserve participants’ privacy.
Feel free to add questions, or comments, using the Comment section below. I will do my best to answer promptly.
Looking forward to continuing the discussion!
Questions and (in progress) some answers
Is it ethical to use generative AI to generate code or test software, given that all major large language models (LLMs) are trained using stolen data (data used for training without authorization)?
[Other attendee comment],”Yes, absolutely. If we didn’t use innovations that came from impure origins, we’d be greatly impoverished, sicker, and would flourish less.”,
Can’t an innovation be both type L and type E?
[Other attendee answer],They seem opposite. Type L levels the playing field while type E amplifies inequality.,5/7/2026 12:12,
Can an innovation be another type like skill destroying or replacing….,5/7/2026 12:13
[Comment by other attendeed] I think what you mean by “”skill-destroying”” is the levelling type-L.
No innovation really “”destroys”” a skill, but some make skills irrelevant by allowing unskilled people to achieve the results that previously required a high skill-level.”,5/7/2026 12:56,
18,”How can we ensure software written by AI for safety-critical applications remains safe during operations, after verication was deemed complete prior to operations?”,5/7/2026 12:16,
As I hope the industry finally starts to increase the adoption of formal methods, moving toward a design by contract approach in building software systems (modern AI being the catalyst for the shift), what role will tests retain?
Do you think there is or will be a place for “AI” “agents” that work directly with bytecode or machine code as their canonical representation? I can see it could be useful for decompiling and maybe security tools. But maybe there are other use cases?,5/7/2026 12:23,
To what extent is it ethically viable for a software developer to register an application that relies on AI coding?
On the 11th of Septeember the CRA will start applying to software manufacturers and distributors at large, with the obligation to report security vulnerabilities and events to ENITSA.
Soon after, the recitals that allow ENITSA to inspect source code and query manufacturers come into force. Do you expect programmes generated with LLMs (that no human understands) to ever comply with the CRA?
Bertrand, you (and I :-) have long written about the need for formal specifications for critical software; English is completely inappropriate because of ambiguities, etc. This alone seems to put the lie to claims of AI eliminating the need for software engineers. Can AI help here, though, perhaps by drafting formal specs or something? Or is there basically no training data that could make this really effective?
Is there any initiative to allow independent research labs to be able to run **reproducible** benchmarks on these tools?
LLMs are fundamentally based on statistical inference, hence hallucinations. “Programmers/Hackers” will continue to be relevant to manage development. ABC ;)
What does it take to turn amateur-generated code into something you’d be able to work with? (If non-programmer staff generate an MVP and hand it over to you?),5/7/2026 12:41,Anonymous Attendee,,”In my experience, mainly time and money!!
Do Bertrand Meyer plan to implement Artificial Intelligence in the AutoProof tool to automate deductive verification of Eiffel programs?
Will the vibe coding tools ever get good at walking casual programmers through the process of developing a test suite so they can express crisply what is valid vs invalid output? That could help them improve the ability to state requirements in natural language. Most people who’ve never fielded software have no idea what all corner cases and failure modes need to be checked
“Can’t AI define attributes of provable code, and then generate such code?
What’s your experience been with using formal methods end to end for DO-178C V&V under DO-333? Any wisdom on introducing it to a conservative engineering org?
When will the orchestrator also become an Agent?
“If the problem statement was to find the 8th term of the Fibonacci sequence, the requirements specification has to fix the initial term of the sequence. Are agents required for fixing the requirements specification? Will it not be done better by a Human Being?
Any comments on sustainability and environmental impact?
What guarantees or explains how a human at the center will remain better at that role than an orchestrator agent?
With code generation, will we still talk and find senior developpers? will these AI impact and reduce our developping capabilities?
Can AI agentic coding be used for formal AI verification for the software we develop?,5/7/2026 12:52,Anonymous Attendee,,,,,
How does one protect their Intellectual Property when the various AIs just apply lines of code that they have found to solve the stated prompt?
Is there not rather an upcoming alignment between SE and AI through the need for robust AI development lifecyle ( to build AI-powered applications) derived from best SDLC practices?
Can we expect quality of available data on the web to continously worse due to the increasing percentage of AI generated code? Will this lead to worse trained AI model?
As someone who has spent a large percentage of my professional career thinking about software testing, particularly for very large, 24/7 systems that are usually safety or life critical, often embedded, so many of the successful techniques rely on our understanding of the types of bugs humans create. Given the increasing reliance on agentic code, do we have to totally rethink testing
Any thoughts on the impact on graduate software roles and a potential tallent gap to senior software engineer.
Is the process you propoed involve AI agent in writing specification or performing proofs?
What is the copyright situation? Does AI generated code belong to open domain?
As a language designer, do you feel that new languages are needed that are specifically designed to be generated by AI and reviewed by agentic systems as well as developers?
“Thanks a lot ,this is really great explanation. My Question is AI is there is help and empower system but still top level employee like CIO/ VP are so scare to adopt it. I am hoping as there is no ethical AI in palce or there is no define govenernce at place. what’s u r thought on this.
https://www.cs.cmu.edu/calendar/202819956 I’m speaking on this at CMU SCS on Wed 12th. I have a working software process like Dr. Meyer describes using a mix of programmatic review, agent processes and formal proof. Can you comment on a mixed process? I attempted a PSP/TSP style process and the LLMs failed but driving them from programmatic metrics works quite well.
Will there be a recording of your talk? That sounds interesting.
How can we train software engineers to recognize mistakes made by the AI if they haven’t made the mistakes themselves, assuming that experience is gained by learning from experiments (and mistakes)?
Will AI-generated code “eat its own tail”, because the mountain of sloppy code it produces effectively corrupts its own training corpus?
How can we ensure that the verification process (using AI) also account for hardware-specific constraints, like timing, power consumption, and thermal limits? these largely rely on large models, so how do we validate that these tools themselves behave consistently across different hardware architectures?
Do you feel that adversarial attacks on AI via hallucinations may become a big risk as long as our perceptions on hallucinations remain less understood?
Is there a use case for a new kind of architecture that’s ai native? like a probabilistic computer
Is there a future for non-LLM-based-agents, which may be activated by AI-powered assitants, to perform: code generation from formally-specified contracts (where suitable) justifying the _generated_ product via provable-correct transformations? Resurrecting theorem proving advances of yore.