S1 E2 - Annie Vella - Proving What AI Builds

Ray and John have a  conversation with Annie Vella in this episode about why formal verification, a discipline she first encountered more than twenty years ago, is suddenly becoming increasingly relevant in the age of AI-assisted software development.

With a background spanning mathematics, computer science, software engineering, DevOps, and large-scale banking systems, Annie Vella first studied formal methods at university in the early 2000s. At the time, proving software correct mathematically was intellectually rewarding but difficult, expensive, and rarely practical in everyday software development. Today, better tooling and the rapid rise of AI-generated code are changing that equation.

We explore a growing problem in software engineering: AI can generate code dramatically faster, but that simply moves the bottleneck downstream. If humans remain responsible for reviewing every generated line, the promised productivity gains become difficult to realize. Formal verification offers another possibility. Rather than manually inspecting everything an AI produces, can we mathematically verify the properties that actually matter?

That leads us into the importance of specifications. Annie discusses the renewed interest in spec-driven development, the difference between lengthy natural-language requirements and genuinely formal specifications, and how tools such as Dafny, Verus, Lean, SMT solvers, and emerging AI-assisted approaches could make rigorous verification more accessible to everyday engineers.

However, verifying AI-generated code is only part of the challenge. Agentic systems introduce an even deeper problem: agents can dynamically make decisions, invoke tools, generate code, and take actions at runtime. Annie offers a deceptively simple example that an agent instructed to delete duplicate files could technically satisfy that requirement by deleting every file. Correctness therefore depends not only on verifying an outcome, but on precisely defining what the system is and is not allowed to do.

We also examine what this could mean for highly regulated environments such as banking. Formal methods may provide a way to define critical invariants, constrain dangerous agent behavior, and even help modernize legacy systems by formally capturing essential properties before replacing decades-old implementations.

Ultimately, our conversation comes back to something deeper than tooling. Building trustworthy AI-enabled systems requires engineers to become better at defining what they actually mean by “correct.” Formal verification forces that clarity. As AI makes generating software increasingly cheap, the ability to specify, verify, and reason about what that software should do may become one of the most valuable engineering skills of all.

Show Notes:
Birgitta Böckeler and Laura Tacho on Spec Driven Development
https://www.thoughtworks.com/insights/podcasts/technology-podcasts/what-is-spec-driven-development

Developing provably correct Rust code with Verus
https://www.amazon.science/blog/developing-provably-correct-rust-code-with-verus

Dafny
https://dafny.org/

LemmaScript
https://lemmascript.org/

Guardians of the Agents: Formal verification of AI workflows by Erik Meijer
https://dl.acm.org/doi/10.1145/3777544

Fermat's Last Theorem, Xena project commentary on Anthropic's proof
https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/

Easy Approach to Requirements Syntax (EARS)
https://en.wikipedia.org/wiki/Easy_Approach_to_Requirements_Syntax

https://kiro.dev/blog/deep-spec-analysis/

https://www.amazon.science/blog/developing-provably-correct-rust-code-with-verus

https://cdn.amazon.science/bb/40/22ac44f84f6d8eb625ac9666a00f/formally-verified-cloud-scale-authorization.pdf

https://midspiral.com

https://dl.acm.org/doi/pdf/10.1145/3815784

https://dl.acm.org/doi/10.1145/3777544

https://kiro.dev/docs/specs/feature-specs/

https://dl.acm.org/doi/abs/10.1145/3815784

Transcript

Copy Transcript Copied

John Willis: [00:00:00] Hey, everybody. This is A Mere Formality though I-- we, I think we're gonna stick with the name, Ray, do you think? I don't know. This is the second episode. Yeah, why not? Why not? Unless somebody screams and kicks and hollers. Hey, Ray. So how's it going with you? 

Ray Myers: I'm doing good. 

John Willis: Good. Yeah, - this is our second episode.

 This is really more of an experiment, but if you listen to the first episode, hopefully you did it's probably a good idea to do that 'cause you could get a general sense of, like, why we're doing this podcast, what we're trying to accomplish. But we talked about, like, why now.

We gave a little back history how Ray had been doing this for a while, and really was encouraging me to learn more about it. And then, we kinda had a conversation about let's start a podcast. And I guess the thing for me is I kept seeing other people I knew, picking up on this idea which will lead us to our first guest.

But-- and then we talked about some distinctions, set the sorta tone of what, what was formal verification, what was formal methods, some practical [00:01:00] tools the opportunities. I think we even talked about a Docker moment, maybe at some point. And then the challenges, and, I think what's interesting to me is where I've always been interested in, is sort of risk, and when we get into agentics, it's just gonna be harder and harder to do inference on sort of instructional or tasks or programmatic decisions and this seems like a good opportunity.

Ray, anything to follow up there? 

Ray Myers: Yeah. I think, big recap of the first episode. Basically, formal methods are a family of techniques to bring mathematical rigor to software engineering. We're diving deep on formal verification, which is doing mathematical proofs about programs. And we talked about why, while this has been around for a long time, , you know, obscure, very niche technique, why it is having a moment, why a lot of people are seeing it as a kind of a missing piece of the puzzle [00:02:00] during how we're, using AI with programming now.

John Willis: Yeah. No. Me and Ray have conversations periodically over just all technology, certainly. I met Ray really through the sort of original following him on sort of the Swe-bench phenomena. And, he was way ahead of the curve, and I followed him and we got together.

And then, again, he was pushing this, this idea of formal verification. And then I was talking to Annie and Annie's one of my favorite people of all time, and, she's been doing DevOps at large banks, which to me that's as exciting as it can get. High consequence, you know- things that matter, particularly around risk, right?

, And then I think our last conversation was, I don't know, within the last six months, Annie, and I'm gonna let you introduce yourself here in a minute. I'll shut up. But and then I was like, somebody who I really admire, and then you had mentioned that you were thinking just out of the blue, thinking about it, going, "Oh my goodness."

And then I saw a couple other signposts from people, and I'm like, "Okay, this thing is, seems like it's getting [00:03:00] real." So Annie, you wanna go ahead and introduce yourself? 

Annie Vella: Sure. Thank you so much, John. It's lovely to see you both. Yeah, so I'm, I still call myself a software engineer, but to be honest, I haven't really had a hands-on coding role for a long time.

I've swung back and forth between manager and engineer roles for the last decade or a decade and a half. And, , most recently, I was a distinguished engineer at a big bank here in New Zealand. And, yeah, I left a couple of months ago because I guess I, I spent the last three years studying the impacts of AI on software engineering 'cause I care so much about the field.

I started coding when I was six years old, and I, , for me, it started as a hobby, as a passion. It turned into a great career, but it's changing so much, so fast and, some people it's amazing. For others it's not. And so I... between that and wanting to figure out how to build agentic systems that scale safely- Mm-hmm

'cause I can see all the failure modes. I, like you, John, I think about the [00:04:00] risks quite a bit. And, I think there are really interesting ways we could be exploring to make it a bit safer, and formal verification is one of those. And yeah, I just wasn't getting enough time to do that while having a full-time job, so I thought if ever there was a time to step out and try spending time on the things that I think are important, then now is it.

So yeah, I've, been away from a full-time job for a couple months, although I haven't really had the time to dive into everything that I had wanted to. Funnily enough, as soon as you tell people that you're a little more free, you do some panels, you do some podcasts, and then you end up in Spain with your dad walking across-

the Camino. And so yeah, I'm back now, and I'm hoping to spend a bit more time on all of this super interesting stuff moving forwards. 

John Willis: That's great. Yeah, maybe Ray will jumpstart you here. 

Ray Myers: Yeah. So you, actually had , a leg up in getting into formal verification because you've done some [00:05:00] research on this back in the day.

, So why don't you tell us a little bit about where your older research was? 

Annie Vella: Yeah, sure. So Funnily enough, yeah, it was 2003 when I was finishing my undergraduate, and I did an, an honors year. Here in New Zealand, a, a computer science degree is three years long, just a, a normal bachelor's, but you can stay on and do an honors year, and that's where I think I did the majority of my formal methods.

If I think back, there might've been one or two papers a little earlier than that, but it was my fourth year where I did three formal methods-related papers and, more papers than, research itself. But what was interesting about it was, there were, like, maybe one or two other people in the class.

It was not a very popular course even back then. But I'd done a conjoint degree. I did a maths degree and a comp sci degree, and I think I really enjoyed the math aspects a lot. , [00:06:00] More so perhaps than writing code. I just really, loved, the logic, , the proving, the algebraic, the... All of that stuff.

, It just made sense to me. So then when I discovered that sort of logic could be used to prove out code as well, or, algorithms, that was bringing together two of my passions, and it just, it made a lot of sense to me. But it was hard. I'm not gonna lie and say that I, , I just swum through those papers like nothing.

There was a lot to wrap your head around, and, I'm noticing that now, going back and looking at those papers. The notation, for a start, is really can be quite hard to wrap your head around all the different rules. Just the language that gets used it builds upon other knowledge that you will have learnt, and I think that's what is...

Yeah, I think we'll get onto that later. That's one of the reasons it might be quite hard for people to adopt and, for it to become more mainstream. But yeah, it was computational logic. I did a paper on proving concurrent systems. So yeah, a, [00:07:00] a lot of it was done by hand then, though. This was 2003.

I don't think that a lot of the tooling that we talk about now and the, the languages that we have now really existed then, or at least the thinking did. Like Hoare's logic and, things like that, that we then applied by hand. So my assignments were these blocks of w-working through the weakest preconditions and eventually, either by contrapositive or by induction, working out that, yes, this is true or it doesn't work out.

And so I'm looking back at that now, and honestly, most of it looks like hieroglyphics to me. I'm just trying to work back through it and relate it to what we have today. How does this relate to Lean? How do you use Daphne and it ends up with this? Is it something under the covers making it look like this?

And that's been quite interesting to try and reverse engineer. 

Ray Myers: Now, I realize it's been over twenty years, but when you say, proving concurrent systems, do you [00:08:00] recall an example of what does it mean to, to do that? It doesn't have to be something exactly from your research, right? But w- okay, what is the difference between a concurrent system and a proven concurrent system?

Annie Vella: Yeah. That-- So the one that I was looking at as an example from one of my old assignments was like, you've got this array, and there's a guard, and if the array values are s- are still zero, that's your guard. Then sum up all of the values like two to the power of i for all the values in an array like where i is just the index in the array.

And that way you need to prove that the total sum of all of the two to the power of i in an array of i length equals whatever the amount should be two to the power of n minus one or something like that. And it can happen at different... Like you can have multiple threads running on that, and it should always hold.

So then you start thinking about, okay, so what's my [00:09:00] invariant? Should I... Do I need to have an invariant here so that at any point during this algorithm that formula actually still holds? And it, that's the kind of thinking that they made us do at that time. Now, how appropriate or relevant that would be in the type of code that your average engineer is writing, that's something I have yet to work out.

But that, that provided some good examples, and I think this is what put some people off, to be honest. Even back then, they were like: But how is this useful? I wrote that code in two seconds, and now I'm gonna spend the next week working out how to do this proof. But the tooling we've got today, I think can really help with that.

So yeah, it's it's a changing field. It's really interesting. 

Ray Myers: The lack of tooling is certainly what held me back from getting more into code proofs when I was in school. I had professors that would try to get me into doing algorithm proofs, and I was not able to [00:10:00] understand, like, how big of a leap I can make.

E-exactly when am I using a property right to figure out how to express my intuition about why this is true in, in steps that are, we would consider valid, right? Yeah. And what I, I loved when I started picking up the, the prover tools is that it will tell me.

It'll accept it or it won't, and I have a feedback loop, and I was a... in this spiral of self-doubt every time I was trying to do proofs on paper. 

Annie Vella: Yeah. The, the tooling so Daphne seems to be a pretty well-considered language that people are using for formal verification now, so I thought maybe I should try learning a bit of Daphne.

And yeah, I installed the Visual Studio Code p-plugin and extension and it shows me that, yeah, it's either the conditions stands or, requires, ensures, great. But my immediate sense is, but why? How is this working under the covers? What-- how did this... And so I've been trying to, yeah, work [00:11:00] through, okay, so there's this thing called Boogie that sits underneath it, and then that passes it off to Z3, which is an SMT solver.

And w- okay, there's so much to learn here, but yeah, it's that intuition and then working. If you can get a bit of that intuition as well as just enough of an understanding of how the tooling stitches it together and eventually solves , it can give you a really sound sort of sense of this is correct, and I'm comfortable with that.

Ray Myers: So I do love that moment at which, your correctness has been validated by the machine. It is a, it's a very fulfilling, QED moment. But other than just cha-chasing that moment, can we talk about what's caused you to be motivated to get back into this area at this point, so all these years later

Annie Vella: sure. All right. I'll start by saying that I held onto a lot of my university papers and coursework 'cause I poured so much effort into it back then. I loved my [00:12:00] degree, but it was hard work. It paid off. I think I-- because I poured myself into it I felt understood things, and every year things got a little easier.

So by the time I was in that fourth year, even though the material was getting harder, I felt like I understood it better, and I was the like, yeah, it was just easier to do. And it culminated in these particular papers that I mentioned earlier, and I kept those assignments. I actually had them in digital form.

So all these years I had like PDFs of those assignments, and every now and then, if I was having a moment of like imposter syndrome or something, , I'd open up these assignments and be like I know at some point in my life I could do this stuff," so it's in there, right? And so I guess I've held onto this like romantic notion of how cool this work was, but I've never actually been able to use it in any job I've had.

Unfortunately, I've... Although I've had 11 different jobs because I'm a curious mind, and once I've solved problems, I wanna move on to solving the next thing. I've been a contractor. I've moved around the world a fair bit. Long story short, I've had a lot of different jobs, but most of them have [00:13:00] been for companies where, they're building e-commerce things, websites, mobile apps, and there was just no need for doing this type of work at all.

Nobody would've been interested in paying for it, or it would've been too costly. So all these years have gone past, and I've never touched it again, right? But I had these memories of it being super interesting and really satisfying And then, yeah, AI comes around November 2022, ChatGPT is released, our world's changed, and I, yeah, guess immediately thought, "This is gonna change the way we build software."

It has to. It's a large language model. It generates words really quickly. What is code? Bunch of words with a very strict syntax. So of course, this, these LLMs are gonna be really very appropriate for generating code. But we don't really trust it, right? Because we know that it can hallucinate.

We know that it can, I don't know, just get things subtly wrong. So as we've seen [00:14:00] now, what generative AI is particularly good at is the generating of code, but that's just pushing the bottleneck downstream to the review of the code. And of course, now everyone's talking about what do we do about this bottleneck at the code review stage.

And some people are going, they're telling their engineers you're still accountable for every single line of code that you generate, all right? So you better be reviewing every single line of code." And that, that just doesn't scale, right? If you want the 10X, 100X productivity gains, having somebody manually review every single line of code just is never gonna work out for you.

So we have to start thinking creatively about what else can we do? And in some cases, companies are saying, "Maybe we just shouldn't bother with code review anymore, or maybe get another different agent to review it." And they're trying all sorts of things. And yes, but how about maybe we could also leverage this, this more formal way of thinking about- How to verify code that has existed for a long time that we never really adopted because of cost [00:15:00] economics, need.

Now maybe there's a bit more... There's a few conditions that allow for it to become a little bit more relevant, right? The economics is, we don't sp- we're not spending that much time writing the code anymore, and we need this review or at least some form of verification. Two there's much better tooling now that AI can help us actually generate.

So you can get Claude to generate the three proofs and solve them directly if you don't want to use Daphne. And so it can help you with those as well. And the third I thought was super interesting. When I went back and looked at some of the papers that I had still stashed away from those early years, the language that's sprinkled throughout all of them is ver- specification and verification.

That's the language that formal methods people working in formal verification used back then. You have to have good formal specs that can then be formally verified. And what are we-- what's the language that we're [00:16:00] using today with AI? We're talking about how important it is to specify up front, which starts to sound a little bit waterfally, but specifications and the, how important the verification of the generated code is.

If you get the specs right, then the AI can generate your code a bit better, and then you can verify it on the other side. It's like there's a kind of weird parallel here, like a... it feels like it fits like a puzzle. 

Ray Myers: Yeah. Now, you've opened the door for a little digression that I might indulge in here.

Go for it. Because there was that moment of disclaimer where, to even talk about specs, we might be sounding waterfally, and I feel like we may want to explain that, that background a little bit. And y-you'd have a great perspective because you've worked in DevOps in regulated industries, right?

That sort of tension between people who may be more associated with a waterfall world versus DevOps [00:17:00] very much related to the, the agile- Yep ... revolutions. So what is that like? Why do people feel the need to have a disclaimer if they say there's going to be a spec? Where did this 

Annie Vella: come from?

Ah, that's a good question. I-- part of it, I think, is the word spec. It means such different things to different people, right? And I think that's part of the issue that we've got at the moment is spec-driven development was already a pretty common term a year and a half ago or even longer.

It's... We've been talking about spec-driven dev. But I think folks who do that a spec is this big, giant PRD written with the help of AI, like a really large, wordy document that describes the product that you're trying to build. That's not a formal spec whatsoever. That is a, a nice wordy description of it, right?

And now people are trying to work out whether if you can write that up and make it as unambiguous and [00:18:00] clear as possible, and then just feed it to the AI you're gonna end up with this perfect outcome at the other side, this without any mistakes whatsoever, but you have to get the spec right.

And then there's been some really good discussions between people like Birgitta Bockler and Laura Tacko at, who's now at AWS. They had this great podcast about how realistic is spec-driven development. Is it really gonna work? Because In some cases, people are, they're creating the spec and then do you have to keep it up to date with all the changes that you make later on?

'Cause we don't one-shot software development, right? We iterate on software. So does the spec become the new core artifact that you care about rather than the code? Can you essentially throw the code away and regenerate the entire thing every time? Now your spec and your code's out of sync. How do you keep them in sync?

Do you need a domain-specific language for the spec? So it starts... You start asking all these questions about what the spec really needs to be in order for spec-driven development to work the way [00:19:00] people imagine or would like for it to. But I think that's a different type of spec to the more formal specs that we might talk about.

Maybe you can derive one from the other, but like the formal specs do need to be a little more specific, let's say, than the specs that I've seen people write, which is what I refer to when I say a little bit more waterfully 'cause there's giant documents. No one's reading them. 

Ray Myers: And so historically, there's been a lot of backlash against the idea that we're just going to write down exhaustively everything that we hope that the software will do, which I guess it can fail in two ways, right?

In, in that the implementation might not match it, but also that you might not even be writing down what's actually needed. You might be making way too many assumptions up front. And I think, the waterfall criticism would probably apply in a situation where you're piling like years of assumptions into- Yeah

One giant bet. But I also, have seen an [00:20:00] overreaction to to calling things waterfall when they're any conceivable act of planning or specifying something, right? And- 

Annie Vella: Yeah ... 

Ray Myers: so I guess there's a question of at what point is this a valuable level of planning where we are still leaving open the opportunity to learn, we're not cutting ourselves off from that and when is it good communication, Yeah

and not just throw, throwing something over the wall in a, instead of communicating. 

Annie Vella: When I was thinking about what software development might look like a couple of years ago, I wrote a blog post about, How the AI was putting so much pressure on the software development life cycle and and the, the life cycle was pushing back in its own ways.

And what I was predicting, was some of what we're seeing now but I was also thinking about how we might be able to simplify the process and create it, create artifacts that would help us [00:21:00] generate code a bit better. So in terms of the specs, I actually thought what if we had things called like spec modules, for example?

Maybe we could actually have specs that are reusable to some degree. So when we are speccing it up front, it's... You're not starting from like ground zero and writing it all from- The basics. You can maybe have a spec module that is around how you read and write from a database and the sort of properties that you might expect there, and you might take concurrency into account.

And that might be something that you have a library of and that you can build up your spec from. So ma-- this is what I think of this moment in software development is so interesting because we can be quite creative and, but we need to be quite creative, actually. We keep saying we need to reimagine the software development life cycle, and all I see is the DevOps symbol with little, like, agent faces stuck around it.

And I think we can do better than that, right? Let's get creative about what a spec really should look like, and maybe some of it is okay.

John Willis: So one of my [00:22:00] questions then is so I'm thinking about, like for most of us who really didn't study computer science, like if, the most people I know we just, grabbed our bootstraps, we learned how to code.

We got thrown into big ISPs and, there's that sort of delta between the science. You can see it like, Mark Burgess is a good example of promise theory has never really... it's a brilliant idea, but it's never really saturated because you almost had to be a computer scientist with a scientist background.

And so when you talk about the tooling's gotten better and AI can help us sorta take the spec to verification, that this seems like there's going to have to be a sweet spot between... Like you talked about because of what you've done and your background, how you had to go to one layer, you went to Daphne, you had to figure out what Daphne was doing, then you had to figure out this.

And so I guess the question is gonna be what's going to be good enough to accomplish the spec [00:23:00] verification with the minimal amount of having to understand years of comp sci and formal, the science behind formal verification. Do you have any thoughts on that? Like, how do we get the masses, the people just like to code, but they're gonna see a window where this is useful, but it's got to be useful enough without putting all the- 

Annie Vella: Yeah.

I think what helps there are things like I was just reading about it last night, Verus. Verus is a I don't even know what to call it. Is it a tool? Is it a... Because it use-- you can use Verus on top of Rust to, Formally verify Rust algorithms or methods and that, in that case, you're not needing to learn a new language, for example.

You're just working in Rust, and if you already have some Rust code, you can already today add some pre and post-conditions and some invariants to the functions where it can be applied, and that's something else that you need to work out is not every function that you write would be able to be formally [00:24:00] verified if it's calling out to databases and APIs and may-- You know, Ray, you know much more about this than I do, but it feels like there's only certain types of logic that can-- that are more pure that can be verified.

So there's an element of knowing where it can be applied and where it can't be applied and why. But certainly having it in the language that you're already used to and that you're already building software in, I think that would be very helpful. Daphne to me looks a lot like JavaScript or it's quite a simple syntax.

But if you're, if you've already got some code, like I don't know how many people are building things from scratch in Daphne, for example. Yeah. So then you've got people like AWS did this. And also there's a really wonderful little startup called MidSpiral. I don't know if either of you have spoken with them, but like Nada and Fernando, they're doing some awesome work around building tooling like their LemmaScript, where you can do stuff in TypeScript, and it generates Daphne under the covers.

There's [00:25:00] people writing stuff that AWS did it the other way around. They wrote something in Daphne and then translated it to Java. So so people-- But then I feel like every time that you do that, there's another window of opportunity for some bugs to creep in. So- 

Like you, there's a trade-off there, so I would love to see languages, like common languages that we use, the Javas and the C#s, like the ones that the big enterprises who employ loads of software engineers use typically. I'd love to see them extend their languages with the right annotations for people to just use as part of their development.

So the requires and the ensures and the variants and invariants like that should just be part of the syntax of the language. And I'm not sure why it isn't. I don't... Maybe they tried and it didn't work out. I haven't worked that out yet. But that could help 

Ray Myers: Yeah, the, there are historical and practical and cultural reasons why we-- But it [00:26:00] hasn't really been it hasn't been as practical as this for very long- to where you could even say, "Oh, if we just had a connector to a mainstream language, now we would kinda be ready to do some proofs." A lot of things are kinda coming together. So you've- Yeah ... mentioned more prover tools have been made, and then we've got this increased need perceived to verify because we are using coding agents to generate a whole lot of plausible code, and we want more ways of verifying it.

So there are, maybe more interested parties that have kinda the risk to cost ratios and so on that they would that it would make sense for them to introduce this. So yeah, I think you're right in pointing out, what some of the parties are that are making it more accessible, the Verus project where you're writing in Rust, and these all kinda come with caveats of [00:27:00] Provided you're doing the specific kind of thing that is capable of verifying and that is ever-expanding.

I, I feel like I'm actually not giving this as, as much of a sell as I wanted to because I'm just pointing out how confusing- 

John Willis: Well- -

Ray Myers: this is right now. 

John Willis: I mean, that's, that's the whole point if you listen to the first episode, like we don't-- the thing where I think I'm trying to do, and if anybody's confused right now, it's me, by the way.

But the yeah, I think it's this whole point of this is to start a conversation that we can sorta aggregate around. I got two things I'm thinking about right now. One is, so when I first, and sometimes I'll see a vision and it'll be completely wrong, but that doesn't, that hasn't stopped me in the last five decades.

But one of the things I thought, though, going back to risk and sort of governance and, that sort of stuff that, you know, especially in banks, right? Like how do you let a second line or a third line validate what the first line is doing and all that sort of stuff and, we sorta solved that with DevOps [00:28:00] automated governance. And then when I saw, sort of inference-based tool, we've-- I think we've got a handle on that. I don't think the auditors are there yet, but with evaluation and LLM-as-a-judge capability, it's if I could prove out that I can set a risk profile of maybe five percent incorrectness and show every time I change the data or models, the embedding models, like I've stayed with that, right?

Hopefully, that all made sense. The thing that's really freaked me out then, which was there was no answer To agents that dynamically generate things on the fly b-based on inference. So I think, one of the things that wasn't clear to me before we started this podcast was there's sort of two problems here, and there's probably more than two.

One is, how do we verify code that gets generated and all the bottlenecks that are coming from there? And I've got some thoughts there. The-- And then there's the thing I think that sorta really concerns me because... [00:29:00] All right. Just to step back a second. Because I think part of that has to be done with the bottlenecks and all the new fast code being generated.

But at the end of the day, once the code's generated, it's an SDLC problem, which I think then becomes automated governance and do you have all the things that sort of satisfy that, right? And then it's just a backlog, it's a slop, it's a more audit, more, just more ROI not more waste.

But the thing that scares me is when we start turning on agents to make decisions about inference. So I'm gonna do these five things, and I'm gonna set sub-agents, and I'm gonna do that, where there is no way or without maybe, and there's probably other ways, but right now, other than possibly figuring out how to use some kind of formal verification spec and verification of did it actually do what we thought it was supposed to do?

Was there a risk? There's always-- In inference-based, there's always gonna [00:30:00] be a risk, except it has to be, right? Or else we can't use these tools. And then the question is, from an audit perspective, could we say when we built this agentic process that was gonna be inference-based, that was gonna make a ton of decisions, maybe buying things, selling things, doing these, depending on how exotic you're gonna allow the risk.

Did it-- Do we at least have a sense that it did the things that we wanted to do, not the things we didn't want to do, and do we have a feedback loop to correct You know, so that to me is the real scary problem, as opposed to the first side of the problem. Does that make sense? 

Annie Vella: A hundred percent, John.

I remember when I was thinking about maybe spending a bit more time relearning some of my formal verification knowledge from back then and how to apply it today. I kept getting caught up in exactly what you described. So am I interested in this from a the code that we generate perspective, or am I interested in this from the agentic workflows and the more [00:31:00] runtime sort of guardrails that we need to put around agents?

Because like you I'm hugely worried around that. If you think about remote code execution as a vulnerability- 

John Willis: Yeah ... 

Annie Vella: isn't that exactly what agents kinda do it with a bow on it, right? Like we are asking- Yeah, do it with a bow on it. Yeah, 

John Willis: I love it. Yeah, totally. Yeah. 

Annie Vella: Like please generate some code and execute it on the fly without anyone really having a chance to look at it and- yeah

validate that it's right. So I think b-both. It seems to me that it might be as an easier way to get back into it, looking at how to formally verify code that gets generated by AI because that's where we're used to well, w- for those who have been doing this for some time they're used to generating specs for well-defined algorithms full stop.

But then what you've just mentioned there are people like Eric Mayer who are looking at how to trying at runtime verify that the- 

Ray Myers: Yeah ... 

Annie Vella: the actions that agents are taking are [00:32:00] what you had hoped it would. So it's not sending an email to the wrong email address or domain name, or it's not attaching something or, like he's got this great paper called Guardians of the- Agentic something.

It's in the A-ACM publication. Okay. And yeah, it gives really good examples there of how you can formally verify that, for example, if you've got an agent that should clean up all the duplicate files on your desktop, it's not sufficient to say that all the duplicate files have been deleted because it could also achieve that outcome by deleting all the files on your desktop.

Yep. That included the duplicate ones, yeah. So you need to be more- 

John Willis: Or it didn't delete anything, right? But it said it did, right? Yeah. And then the next... Yeah. Or

Annie Vella: so that's where being able to more formally specify what you mean by delete the duplicates and- ... all the ones that aren't duplicates should remain, and at least one should have been deleted if it was duplicated.

And it's the ability to think through what those specifications [00:33:00] need to be for it to be correct. And I think potentially that becomes something that the software engineer of the future who is building safe agentic systems or using agents to generate code that is m-more correct, maybe this becomes something that's m-more, more important in the skill set or toolkit of a software engineer of the future.

I don't know. 

John Willis: I think that there's, and we'll get back to you, Ray, with your pipe hitting questions. But I think the, the-- both problems, both things have potential problems in different ways, right? So this one, I think you just did a great job of explaining it, and I think we'll have some good links and maybe a future guest.

But but the other problem I'm thinking about a lot lately is, we always talk about the aha to ka-ching in DevOps, right? And the truth is, we were lying because it really was commit to ka-ching. We didn't really s-- when Nicole, wrote Accelerate and she said, "We're sciencing the shit out of [00:34:00] DevOps," right?

Yeah. But we were really talking from the time you did the commit to the way, whatever got it to whatever was some form of production, right? That's the part we scienced. And and that was good enough because before that, we had nothing. It was terrible.

But now we had an accelerated process to get fast feedback, and we didn't really care about ideation.

I mean, we did, but we didn't, right? Like- 

Ray Myers: Yeah ... 

John Willis: we're terrible at idea... story points, sprints, right? It's just chaos. There's no science there. But now all of a sudden, we've got to a stage where, okay, we were doing really good. We solved for over a ten- or fifteen-year period.

We changed the industry on what we were calling the aha to ka-ching, but it was really the commit to ka-ching. And that was good enough. Y- I remember having a conversation with Mick Kirsten five years ago about, if you could take what you've done with flow time metrics and move that into ideation, you'll be a billionaire.

And, he was, like, taking notes. But we didn't have to. [00:35:00] 

Annie Vella: Yeah. 

John Willis: But now we have to, right? Because the bottleneck, right? We literally are now at a point where the ideation was a long window, right? Yeah. Even in the fastest mode, it was still, way longer than the commit to cha-ching, right?

And but now all of a sudden we've condensed that to minutes and, and we know the historical stories of people telling stories like, "It took us six months to do this. We did this in a week." Or, Topo Pal at Gene's conference last year, when it was still the Enterprise Summit or whatever, he talked about a project that his team said would have took six months.

He did it in a week, and that was at Fidelity. 

Ray Myers: Yeah. 

John Willis: Fidelity doesn't just put things in production, you know- That's right ... willy-nilly. And but now we've now exposed where ad-ideation has to be more science. And so on that side, that's, I think, really important to do this stuff about, getting specs in a format that cr- that can be, I'll just say, correlated or calibrated with verification.

But again, we still have the agents problem, [00:36:00] and the agent problem to me is the real risk and auditor problem. So- 

Annie Vella: Yeah ... 

John Willis: that's my two cents. 

Annie Vella: In, in terms of the, the specs needing to be Ideated and written down in a way that it can really help the agents generate the code that you intended.

I was reading a, an article just yesterday. Again I had a bit of time on my hands to look at these things. Kiro, so the- Yeah. 

Ray Myers: Yeah ... 

Annie Vella: Amazon new IDE that's quite agentic. They wrote up an article, I'll send it to you after the call. We they talk about requirements engineering and requirements analysis becoming far more structured so that by the time the agent gets a hold of the spec, it is almost essentially already been formally verified to some degree.

Ah, 

John Willis: okay. 

Annie Vella: So they're taking specs and then generating, so with the help of agents, they're generating... They're using the [00:37:00] EARS language, E-A-R-S. I can't remember what it stands for, but it's like a, a simplified English. It's a little bit like the given when then I think. And using that kind of a, a format, you can structure the specs, but you can provide the specs as a human.

You can provide them however you like, and then an agent helps you restructure them into this EARS language. And then you've got this set of, say, five requirements around how you want the withdraw function to work. And then they run some agents over that to see whether you've got any contradictory- Ah

assumptions because maybe you do you know, you hadn't even realized it. And then it helps flesh them out and create maybe some new ones where there might have been gaps. It asks you questions about what did you mean here, this is ambiguous. You're making some assumptions that you haven't written down.

And then they actually use an LLM as judge to run through a few different examples and- Wow ... the LLM as judge can work out whether there are clusters of, with real values, this [00:38:00] here won't work out. And that's not quite formal verification. In fact, it isn't at all, but it's trying to head in that direction.

And the last step is they do actually invoke SMT Lib, which is a, an SMT solver, Z3. It... Oh, they didn't actually say whether it was Z-Z3 or something else. But, so they are trying to formalize even just the spec into something that can be formally verified before it becomes code, and that's interesting. 

John Willis: But you know what?

The, this is a... and I do gonna turn the mic over to you, Ray, I promise. Amazon- Yeah, you can ... Amazon doesn't play nice with others. This sounds amazing but un-unfortunately, they what do they say? Dance to their own drum beat or whatever, right? Yeah. In other words this would be a great collaboration.

I mean, MCP is a nightmare, but at least it was a way for everybody to work the same way. Now, something what you just talked about, I'm gonna look at, 'cause that sounds exactly what I want, right? Or the direction I want, right? Yeah. Some way that starts adding some type [00:39:00] of... i've talked to, I've talked to Arise, I talked to...

'Cause they don't seem to have an answer for an LM as a judge for this problem, right? And that, that's-- but then I think about Amazon, and they literally just, their universe is usually, maybe hopefully not this time, but yeah. 

Annie Vella: At least they're writing about it and if 

John Willis: anything- That's right. There you go.

That's right. That's a good point. That's a good point. Yeah. Yeah.

Ray Myers: So just to catch some references we had here. Yeah. Eric Meyer, who, th-this marks day one of him not showing up on this show yet let's we'll rectify that at some point. Yeah I hope. That would be awesome. Guardians of the Agents: Formal Verification of AI Workflows was the paper you were mentioning there.

Yeah. So he's done that piece, which is about, let's rigorously define what actually this thing is allowed to execute under what circumstance. So that goes with the AI workflows. He's also done some work on the AI verified [00:40:00] development side with his language universalis. Universalis.

So he he's been on, on both sides of that. And EARS is Easy Approach to Requirement Syntax. So it is a form of controlled natural language. And so there are, yeah, the-these a lot of history of success with semi-formalizing English, just restricting a little bit how we use it, and it it coerces our thought processes into being more clear.

And is-- this works surprisingly well. And so then, yeah, in a way, formal specs are an extreme version of that. I when I've used provers at at jobs, oftentimes it is just to specify something, and the fact that I was able to put it in a verifiable context forced me to make my thoughts so much clearer than they would've already been.

And so I I get value out of it before I've even done any proofs about the thing I defined. This is just getting better at defining [00:41:00] things. What I worry about is that people we need to value the work of defining what we want- 

Annie Vella: Yeah ... 

Ray Myers: in order to actually leverage that. Otherwise, people will have coding agents, they'll get it in their head they need a bunch of tests, so the coding agents will write a bunch of tests, and they'll get it in their head maybe they need some proofs 'cause they, they heard the tests weren't enough 'cause they listened to our podcast.

And then they just, "Okay, a-agent, make me a bunch of proofs." But if you don't actually really get serious about, no, what do we care about defining, and invest in that, then you won't ultimately get the value. So this is what I worry about is making it a, a social process too.

Annie Vella: So much of software development is a socio-- the, the socio part of the sociotechnical system, right? We've got all the tooling in the world now that we could ever want. I think the next challenge for us is really to find ways to [00:42:00] make the, the process in-include these sorts of things and not make it feel like it's over the top or just done for the sake of doing it.

Because as you say, it's the sort of the process of thinking that through that actually makes the better software at the end of the day. It's not just about pumping out a bunch of specs and proofs that prove the wrong thing. There's still an element of validating that you're building the right thing. Yeah, and that's more of a people and process challenge than it is a tooling one. 

Ray Myers: Some news on the validation si-side that would be interesting to talk about here, though, Annie, I'm taking you off guard a little bit you can comment however you like or not. But as an example of sort of the extreme pull request review bottleneck, the extreme case, on the first episode, I said, imagine a formalization of the proof of Fermat's Last Theorem," which I- I look now- 

John Willis: That's [00:43:00] hilarious.

That's right. I forgot about that. Oh my God. That's hilarious. 

Ray Myers: I look now psychic, but of course, I was aware that they were working on it. 

Yeah. There was a formalization effort in progress to put the proof of Fermat's Last Theorem in Lean. But before it was complete, Anthropic came with a a-an agentic formalization that was, I think, over ten million lines long.

But this is illustrating, and I'll explain in a moment for those of you who aren't familiar what this, this theorem is. But it ex-- it shows the extreme form of having a pull request review bottleneck because we had over ten million lines of code in this case, and the-- when it was a, a paper proof, it was two hundred pages of proof that took years to to evaluate that, used results from all over mathematics.

If Lean verifies it, and Lean did verify it, then we [00:44:00] know that it is correct. It is a valid proof. It's an ugly proof that's ten million lines long, but we do know that it is one, that is accepted. W-- this in-- you know, it may not be as mathematically el-elegant, but if what we wanna do is know if our code works or not, we don't care how long you spent proving it.

We just know-- we just wanna know that it works, that it meets the requirements. And in this case, the specification of Fermat's Last Theorem is one line long. So by understanding one line and having over ten million lines of agentically generated code, the Lean prover is able to tell you that is in some sense correct.

And so that is... you may never hit that one to ten million line ratio- Yeah ...in your review ability, but that is the extreme case. That's what's possible 

Annie Vella: Wow. The-- if I understand correctly- ... one of the potential failure [00:45:00] modes of trying to come up with these, the specs and the proofs is, for example, not coming up with the weakest precondition and your preconditions are too strict and therefore not proving the right things.

Or the provers can come up with some axioms or lemmas that kind of say, "Oh, we don't need to prove that because we just take that as assumed." And then it's almost cheating, right? It's well- but can you just take that as assumed? I'm not sure that you can. Why did you say that? So I guess in this case that you just explained, Ray, the, the spec was, it's the one to ten million ratio.

It's so clear, it's so well writ... like that one line is so well specced out that actually it, you can trust that the proof that it generated, that Lean generated was good. And it, what is it? What is the term that we... the discharged the proof obligation. I've got a whiteboard behind me- Yes

where I'm writing these things. Exactly. This is the language that I'm trying to relearn. Yeah- ... discharging proof obligations that it did it correctly. But in other cases, [00:46:00] perhaps you need to have a sense of intuition around no you can't just go and create that as an axiom.

That's not a valid one and tell the agent to stop it. Do it right. And 

Ray Myers: in no situation would we ever really specify all the behavior about a piece of software we care about in just a couple of lines like that. But in what situation is there a whole lot of confidence that we- Yeah ... can buy with a small amount of spec that we can understand?

That is gonna tell us, what what some of the biggest wins are. And, maybe security is a good example where we have really well-understood properties that we're trying to assert. 

John Willis: So that, that's what I was just thinking about. So to bring it back a little closer to earth for me Andy you know the bank really well.

We probably, you can guess what kind of things are gonna be experimented with agentics there. What are the failure, the, the, the ones that are gonna be, "Ooh, yeah, we can't let that happen again." Or, somehow leads to maybe audit being able to [00:47:00] say, "Hey, we got this finding. Can you fix this?"

And, there's sort of a feedback loop, right? Which, you know- Yeah ... DevOps and DevOps automated governance gave us. I-is it then maybe makes sense that we could use this kind of stuff to look... like excluding what you just said about all three things that you have to do to get it right and you can't cheat or you could cheat.

But can we cheat by saying like- We need to make sure this never happens. Like we-- like I'm just gonna make an example, like what, sort of funds in a bank is something that cannot, under no circumstance be mutated, right? Or,

Ray Myers: yeah. 

John Willis: And so may... Is it like maybe it is a little simpler where like we can define some kind of spec verification for things that we know should never happen and start there and work our way back-backwards?

Annie Vella: , I had been thinking about maybe a good use case in something like a bank where, um, I think this is true of many banks around the world. They still have a lot of, let's call them [00:48:00] heritage systems. 

John Willis: Sure.

Yeah. 

Annie Vella: Lasted for a long time because, they were implemented well to start off with, and they're pretty resilient, so why change it, right?

But at some point, because either there's a lot more load on the system, thanks to AI agents that can willy-nilly just, query from systems that at a speed that humans would never have been able to do or- 

Yeah you just want to be able to do new s- new things that your older systems might not be.

But AWS, again, for example, they just recently... I read a paper about this. They took an auth engine that they had previously written in an, an older version of Java, I think, and they Wanted to rewrite it, but first what they did was formally verify it, the existing version and then apply that formal verification to an, a new implementation.

They actually wrote it all in Daphne, and they wrote their own Daphne to Java compiler because, or transpiler or, because they wanted to be able to [00:49:00] ultimately deploy Java code that was readable. But the same proof could be it was the, the Daphne at least was formally verified, and they used differential ran- differential random testing.

More stuff on my whiteboard here. Differential random testing to check that the old version of the Auth Engine and the Auth V2 were the same. And I wonder if there's a way that we could help banks modernize some of their oldest systems that might still be written in COBOL, for example. You might be able to do something similar there, where you have some formal verification of just the most core functionality that you just cannot afford to get wrong, and then use that as a baseline to...

This new-- You can then use that, those specs in generating your new Java or Rust or whatever, pick your new language that you wanna re-implement this logic in. But at least you'd have the, [00:50:00] the formal verification kind of sorted before you get started or the specs from which you can then do the formal verification.

So yes, I th- I think that might be a really interesting use cases for... use case for banks that m- are looking to modernize now because of all the reasons I just mentioned. 

But even in just generating new code if they wanna be building a new mobile app, maybe they can take some of this into account.

But it means that you have to... This is something I learned recently. You have to architect your code in a certain way so that you can get the most out of formal verification because like we said before, there's only certain types of logic that it will work on. And I think there's other, maybe property-based testing you can use for other functions, but...

Or TLA+, maybe you need a combination of all these things. Ray, you probably know better. But you have to structure your code in a certain way so that \ you keep the boundaries nice and clean so that this is the type of code that you can formally verify. This is the type of code that you would have to think about differently.[00:51:00] 

I don't know. I think it might affect the way we structure our code, which is not a bad thing, but- that's right ... we might have to be more deliberate. 

Ray Myers: Yeah, just like architecting for testability is s- was such a big deal. 

Annie Vella: Yeah.

Annie Vella: [00:00:00] So these are all the disciplines we've gotta learn now. People like- But when you- You to write about it, right? 

John Willis: Yeah. We need to do some of this, to a certain extent for cloud native, right? Like not everybody like adhered, but the original cloud native, we had to refactor the way we had to do things.

And so, so it's not uncommon for the industry to do this. I guess the one thing I guess I'd ask both of you is, , it sounds like, without me digging too deep, that Google and, the companies that have had scale issues have been doing this all along. And, maybe we're-- it's like everything else,

they were building infrastructure for, compute network and storage at a scale. Eventually, that escaped things like Kubernetes, things about, Amazon literally turning, whatever the history was of how they scaled, turned that into a commodity for everybody else, basically AWS,

Maybe what we're seeing is them exposing how they've [00:01:00] dealt with this whole other issue of scale in terms of formal verification, and maybe we're just gonna pick up on their lead. I mean, just based on this conversation from Amazon, I know Google's doing a lot of work with formal verification as well.

So is that-- does that seem like a logical path or something that might happen? 

Annie Vella: Yeah. I-I've only really started learning about how these sorts of companies have been leveraging formal verification just recently. And the more you look, the more you find. You're absolutely right. I guess it's the, not only the, the scale, but the reliability requirements that they have.

, Their customers would simply not stand for, "Oops, we had a little bug here." Yeah. That's right. Yeah, so they put the effort in. Like that rewrite of that auth engine that I mentioned before, it took them a considerable amount of effort to do that. But the end result, they were very confident with.

And just to get that level of confidence, maybe this is what it takes. [00:02:00] 

John Willis: Yeah, I f-found that link, by the way, so I'm gonna post all the links in the show notes. Yes. So yeah. Go ahead, Ray. Sorry. 

Ray Myers: So I think that's, it's absolutely right that there were, problems that their scale as the cloud providers, made them, need to innovate in solving.

I also... I worry sometimes that I, cite AWS so much that it sounds like they, , invented the field. But of course, there were, other areas, not only in academia, but in, in other areas with very high risk, right? As some of the first adopters would've been, , people making planes and spaceships a-and things.

That's 

John Willis: right. Yeah. 

Ray Myers: So then you have, this next level of slightly lower risk, but still very high commercial risk, and problems that need solving. And so I think the cloud providers are, , maybe the current front line of this, especially among the people that, average developers find pretty relatable because we use their stuff.

[00:03:00] That makes it a very, helpful example to communicate with. But when they're verifying things on one-- for one project within, it doesn't become infrastructure. It becomes these very isolated tools. And so I'm really excited about it turning into things where we don't have to reinvent the wheel every time we wanna do it, where there's something to pick up and just use.

John Willis: Yeah. Yeah. I think that, to, I guess my question earlier, does Amazon play nice with everybody? But the point is, as long as they're documenting this, and the more people like you and Ray and, , start digging more into what they're doing, the more we might find collaborative efforts to get, the sort of common way- Yeah

or the common path for us all to follow. I was telling you guys, I think earlier when we were setting up the call that I was at Quantum Week, last week, the IEEE Quantum Week, and everybody knows [00:04:00] me. I'm q-crazy over quantum right now. But it's funny that now you're seeing like chemists using massive agentics, which is scary, right?

Like, they're like literally it's like automating, like there was one story of a, a professor, unbelievable resume professor of University of Toronto, a chemistry person, but works for Nvidia. There's like all sorts of things. He talked about how they've built this agent that he got a name for it, and I forget what it is, that literally can do in thirty-six hours what used to be done in six months by a, a graduate student.

'Cause they've glued all the tools together. And I heard multiple stories of, , just research with agentics. They-- these people are pretty smart, so it didn't take them long to figure out how to use agents, most of them using Google stuff. But, every time I heard something, I'm like: "That sounds like formal verification."

So I'd throw my question in [00:05:00] there , and they'd say: "Yeah, no, of course, we use Lean," , and "Why would you ask such a stupid question?" . So the science background that just, like it was natural. So that was kinda interesting,

Annie Vella: I guess they live in a more formal sort of world where things have to be- 

John Willis: Yeah

Annie Vella: pretty well specified or pretty bad things could happen. So they're more used to thinking that way. Comes more naturally. 

John Willis: Or, or they're, they are living in a world where they're doing research and trying to prove the research, and therefore- Yeah ... it goes hand in hand. That's true. So I think we're at about an hour or maybe a little over, but, , anyways, we get-- we need to do this again with you, Annie.

I think, the more... we'll try to schedule some more. So I think what we can do is just keep following. We'll get some guests, but keep following the bouncing ball here because I think the ball is bouncing just on what you pointed out to some of the research you posted, like I think made this episode incredible.

Annie Vella: Awesome. 

John Willis: , Yeah. Because I think, anybody who's listening and paying attention or like me who's like on the [00:06:00] outskirts and saying, "Well, what is this stuff?" That we just dumped a whole lot of really good resources. 

Annie Vella: Fantastic. 

I loved the conversation. Thank you so much for inviting me. I'm still very much a novice.

I've, I wish that I could just reload everything that I once upon a time knew, but you know what? I'm starting to come to the realization that a lot has changed in the meantime anyway, so maybe it's not even all that relevant. But yeah, a little bit of that foundational knowledge won't hurt. But, , it...

there's certainly a lot to learn and, that's through conversations and sharing, exactly as you said earlier, John. All right. That's right. 

John Willis: Ray, any parting thoughts? 

Ray Myers: I guess, we're just looking forward to the day that, like those chemists you were talking to, people say, "Well, of course."

John Willis: Yeah, yeah, yeah. Of 

Ray Myers: course, we're proving 

John Willis: it. That's a stupid question. . Totally. Awesome. All right, y'all. It was a blast. Thank you so much. 

Ray Myers: Bye. 

Annie Vella: Thank you.