Questions and answers on AI and verification: a follow-up to my May ACM Tech Talk - Bertrand Meyer's technology+ blog

Skip to content

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.<br>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,<br>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.<br>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...