Prompts Aren’t (Good) Specs: Correctness in the LLM Era

Transcript

All right. Hello everyone. So I decided to submit this talk because I saw this talk but about from the open AI guy about the new code where he talks about how specs will become the new code and I was very excited about yes specs and then I realized he was talking about English like really natural language is that where we are going um I didn't like that because how do we know if the LM actually understood what we meant in our English spec? How do we know if the spec is not ambiguous and do we really want to drop all the amazing tools we have like when you are working with code static analyzers compilers to just be reading? I don't think we want this and I think we definitely want the

productivity that we get and like that AI is so good at. So we do want the productivity but our profession still remains um like how do we know if my solution is actually a solution to this problem? Am I covering all the edge cases? Am I missing something for these questions? Natural language is a very bad tool to handle. Um, and I think we are collectively very excited but also tired about AI because we are tired of writing these huge prompts and agents in just like natural language um, and with no structure. And we are also very tired about like asking AI to do something and then AI gives us like a huge diff and then we have to read it and determine if

it's correct or not. And we feel very disconnected from that code that AI wrote for us. But most of all, we are really worried about the security and the hacks that will come out of this code that AI wrote and we try to read or our colleagues try to read, but we missed something because we missed that connection and we missed the thing that brought us to work with this stuff in the first place. So, uh, are is anyone here excited to audit this new code? I'm not. Um, so maybe instead of putting our really good tools in the trash, let's try to do the opposite. Let's give a really good tool, modesty aside, uh, to AI. So I believe the best tool that we can give to AI is executable specifications. And we wrote Quint this, uh, executable specification

language. I've worked on this for the last four years. Um, and now we tried giving Quintai and it sits between English and code. The problem with English is that we cannot run it, right? So it's not very interesting. You can just read it and with code you can claim that we can run it but like how often in web tree we actually get like one CLI command that you can run and then see if it's working or not. That's not usually the case and determining if something is working or not or defining correctness is super important in this LLM era. Uh and it's a very hard task. So um and because LLM, so this is a hard task, but it's super important because LLMs

can go really off track if you don't guard rail them enough. And it's hard to write this guard rails and this validation especially for things like like decentralized systems like consensus engines like Nexus and it's even harder when you're feeling super disconnected from your protocol because you use AI to generate it in the first place. Um so by playing with a queen spec you can have that connection back uh in that's so so important for LLMs. Uh so let me more concretely explain what we did. So say you want to make a change in your system that is very complex and you are scared and instead of going from your prompt directly to the code change which is what we usually do let's try to put queen in the middle.

So first we do uh we ask AI to change our spec for us our executable spec. AI does that and then we this is easy and then we uh are going to validate that spec and here is where we play with Quint. So we ask Quint oh is there is this behavior possible? Can I reach a scenario or certain things happens and and this is when we gain confidence and get the connection back. So this is when we we we feel confident about our protocol or algorithm again and only when you have the spec where you are confident about that's when you are going to ask AI to make the change on the code with that spec as input. So here AI changes the code but not only changes the code it also does the validation of the code by model based

testing. Model based testing is is a technique similar to differential fuzzing if you were here yesterday. Um so we have some validation that the code actually matches the spec where that we are confident about. So we tried this approach not on a toy example we tried it in a product called Malikite which we built at informal systems and two fun facts about malikite. First it was acquired by circle from USDC this year. So they build our new blockchain arc. So arc is running on malikite and second fun fact they are using quint from the very start. So all the protocol design for malikite was on using quint. Uh but that's not what I'm talking about. I want to talk about the how we apply this to malakite to make a very complex protocol change that people told me it would take two months with engineers and

we did it in under a week. So this was our first experiment and we are very excited about this and [snorts] yeah it was better than expected and I I'm excited to show you more about this experiment. So if you want to hear more, let's talk or let's uh you can also connect like connect with me next week when I'm back to Brazil and I can show you online. But our work is shifting from writing code to validating AI generated code and we need better better validation tools and prompts are not them. So let's stop treating natural language as specs.

Let's use something you can actually run query and trust and let's shift from reading to play. THAT'S [applause]