Thank you all. Eh, it's nice to be here. Uh, I hope you can hear me. I have been working in this field for quite some time. Uh, I've been working in industry and academia for a while now.
I've worked in many fields, and I think this is actually one of the most interesting jobs I've ever had. I am very, very excited. All of these things related to stocks are actually online. I like to receive questions either during the presentation or afterwards. I think this is something very interesting for this industry.
I want to really understand how many of you are coders. Uh, some. Okay, this is your report. But even if you don't intend to code this, I hope you enjoy it. Stop me with questions.
Stop me with questions, please. So, uh, it's obvious to all of you by now. Er you by now. Er , software, and I'm not really talking about necessarily a smart about necessarily a smart contract. We apply it in many areas.
So many areas. So , there are different problems. They are called all sorts of objects, but we need to understand that coding agents replace software. Even at Cetera, we work with very complex code. We have many engineers with doctorates in computer science.
We see programmers getting better at doing good things, just not as good as us. Also, hackers win. I do n't mean, we already told you that hackers win, and they win because they... because they... Part of it is we use artificial intelligence.
And we have a fantastic audit firm, including the audit firm from the Cetera days, and we have a lot of tools, but even with the tools and great auditing, we can't find all the mistakes. And some of them are in the code or not in the code. And what's worse, if you think the situation is worse today, tomorrow it will be even worse, because every time this company says Open AI, I don't want them to release a new model, a new threat appears. And on top of that, the code is getting more and more complex. So who can stop it?
And we know that companies and Tropic AI have this idea of intent, but they think about intent informally. And we think that's wrong. We don't think this is the right way to think about intentions informally. So our solution is a soft formal check. How many of you have heard of formal verification?
Some. How many of you have allergies How many of you have allergies ? A little. So the idea is that formal verification should be difficult, only used by PhDs or someone like that. And I've heard some of our competitors say that formal verification requires a PhD, that's nonsense.
We want to make formal verification as easy as testing. And in this talk, I can show you that it's not necessarily as good as what others are producing, but we actually have technology that will eventually make formal verification as easy as testing, and very, very affordable. And okay, by the way, if you have any questions, I have mechanisms for...So please stop me and ask. So, I'm super excited.
So a lot of things related to formal verification, I'm sure, you know, it goes back to the 50s. A lot of work, a lot of people are giants in formal verification, as in any other field, there are times when everything solves everything, and then we say that it solves nothing. All of this applies to artificial intelligence and many other industries. And there are many myths about formal verification. And the biggest myth, and you see many Italians saying that formal verification is unsolvable.
This is a very complex computational problem. And they even have a mathematical way of saying it's unsolvable. This is nonsense. Because we and others are finding a way to make formal verification possible for many things, if we know how to do it. So in reality, the computational problem of formal verification is not difficult.
So what's so complicated about formal verification? The idea is that the problem is formal verification and other myths that people have, and this goes back to Knuth and others who say, "I formally verify the code, it's correct." Okay, so you'll hear a lot of people say, "I don't need testing." need testing." I mean, I don't know if you know, one of the giants of computer science, Dijkstra.
He said, "Look, you don't need testing, you have formal verification." He was, of course, one of the most brilliant people, but this is completely wrong. Formal verification, the quality of formal verification, actually depends on the formal specification. So if you don't have a good formal specification, you don't have formal verification. Many teams say they did formal verification and then cracked it.
Why is that? Because they didn't formally verify the required property required property , okay? If I tell you that I can move from this place to this, it doesn't necessarily mean that you have another property that interests you. So, the biggest problem with formal verification is actually the formal specification. And this is where companies like Certora employ many smart people and others.
And this is where an LLM will help us. Search for a formal specification. And I'll show you small steps here, but that's the idea. We have a tool, it doesn't replace us yet, but it actually finds your formal specification. OK.
So, how is this tool progressing? You will see the user interface later, but the idea of this tool that is being released now is that it will be token-based and all the software will be open source. So the idea is that you write an intent the same way write an intent the same way you write an intent when you work with the cloud or others. You write the intention informally. Okay, here's the thing you say here's the thing you say : "Keep a balance : "Keep a balance ."
This is an informal statement. And then the tool will automatically come with the invariant. He can use our tool, he can use others use others . And the invariant, let's say, is that the . And the invariant, let's say, is that the balance amount is equal to the total amount.
So, the invariant is formal. OK? And once we have a formal specification, we can use a prover, we can use testing, we can use a lot of things. So, the idea behind this tool is that it bridges the gap between informal specification and formal specification. OK?
Okay, here's an idea. So, the developer writes the intent, then you translate it into a formal specification, and then you verify it, test it. This tool is, of course, used outside the formal verification. It is used if you want to conduct testing. It is used if you want to do many other things.
Good. So here I want to mention one of them again, which you all probably know, but it's a good friend, a computer scientist who's still alive, and a friend from Stanford, who always says, and I love this quote from Don Knuth. Don Don Knut has many...I'm sure you all know them, right? And you know about his work.
So basically what I want to say is, in addition to formal verification formal verification , we also want to do testing to do testing , and this tool helps you with that helps you with that . Why does this work? Good. So how does this fit into your development cycle? Honestly, we don't know yet.
We are starting to develop it, and we need you. We believe that the industry, at least in smart at least in smart contracts, is built on audit. Maybe this tool will replace auditing, we don't know. Right now we're looking at a tool that's used before an audit, okay before an audit, okay ? So, you develop your code, test it, and then use this Auto-Prover tool before the audit.
And this tool increases your security. This is not a replacement for an audit. I don't care if you decide, but the idea is that it's a complement to the audit. And what do you do in this tool? You start with properties that are written informally are written informally , and then it's an interactive process interactive process .
You need to talk and I'll show you. You need to talk to the person and find out if the hardest part is actually getting the informal properties right. And this is where you need interaction. And maybe eventually LLM will improve, but for now you need some interaction. And once you get that, you'll get into the formal specification.
Once you have a formal specification, you can use the tools, like others, to obtain evidence or detect errors. And of course, when you graduate, we think graduate, we think that maybe in the future this will change, you need a person. And the person reviews the code, reviews the specification, reviews everything. And if a person says everything is fine, they deploy him. If a person, like an auditor, says it's not true and you agree with that you agree with that , you need to repeat the process.
So, here's how this tool fits into the development cycle. There is quite a complex code inside. At the moment, it's about 10,000 lines of Python. We actually write it in Rust. But the nice thing about this tool is that many of you know that we developed Certora Prover, but it's actually agnostic to Certora Prover.
It can work with any technology. And in fact, it's not even needed, and we have... We're certainly not artificial intelligence, we have a lot of respect for it , but we understand engineering well, and we've done a lot of things to make this tool very, this tool very, very agnostic. And this tool actually advances the state of the art in artificial intelligence. And what it does is you start with the design documentation, you start with the specification, and you actually...
That's actually one of the most interesting things about it. Before doing anything, because what happened to us, we are a consulting company. We provide services for companies, such as auditing services. And sometimes we come to the client, we call, we tell them, is this what you're building? We say we wish you knew this sooner, we would have had to write the code in its entirety.
So we're here to help the guy help the guy . We help them strengthen the design. So we make the tool more...We make the design more conducive to formal verification for other things. So this is what we call design reinforcement.
This is an LLM agent. And this makes the design more ready for formal verification formal verification . And you can use it as early as possible. And you just take the document. I don't know, I have some kind of noise.
I hope you are all well. And then, of course, we go to the audit agent. There are many agents that we can use, you can use us, we have many other teams that will conduct the audit, you can connect your audit agent. And, essentially, we get a security review. We extract an informal specification.
We have an informal specification. This is something we could have talked about at the beginning. From the informal specification we move to the formal verification agent, we convert it into our own language or another language to write the formal specification. And then we actually try to create proof or create errors. We can use use any tool.
We are currently deploying it using various tools. Rock is an academic instrument. Actually, it used to be [ __ ]. We use it. We also use Lean Four, which is an Amazon standard.
We're going to use Almost, which is based on A16Z, and we're going to build using our own prover. And of course we want to deploy more, and it's easy to deploy more. It's open source, you can add things. So, that's an idea. And we believe that this makes your code strong enough.
Whether this will be an audit inclusion or not, we don't know. This remains to be seen. Let me show you two examples, and then I'll summarize. I want to show you two examples. One is a toy example.
I admit that it was created, the other one–it's actually one of the most interesting protocols in this field that we prevented. So I want to show you both, and please bear with me. So, here's how we apply this to toy examples toy examples . We need to apply this to more examples. Good.
So, this is a toy example. I'm sure everyone sees ERC, it's a counter. He has a mistake. This is a trivial mistake. Anyone can see the mistake.
Here you see that it doesn't use a parameter. This is a trivial mistake. This is just an illustrative example. It's not very complicated. You can find it using any tool.
But the interesting thing is that once you have the fix, we can actually test the fix. This is a big difference between other tools other tools . But any tool will find this error. So let's see what you do. You see, this is an agent.
The agent is actually small, he talks to you, and you see him find these properties in English, okay? And you actually interact with it, you see all of this, you interact with it in English. And then you have this collaboration. Then you translate it into a rule. You see how this translates into a rule.
You don't actually need to read the rule. You can read the rule if you want, but the informal specification is actually more interesting. And then you have the property. So, you see here, it proves the rules that it generates. She proves three rules.
Uh, out of three rules, sorry, I apologize sorry, I apologize . I'm too nervous. Of the three rules, two were tested and one was not. Okay, you see this, and there is an error. You can take a look at our user interface.
Our prover has an interface that explains the error, but you can also look informally. Informally, we tell you what the mistake is. So you don't really need to understand the internals of formal verification formal verification . And here's how this tool is used. You actually use it, and of course when it finds an error, it could be a bug in the code or a bug in the specification.
We really don't know. And you really don't know. And you , as a person, have to justify it. Because really all it finds is deviations between the specification and the code. Okay, you'll think about comparing the formal specification to the code.
So, here's the idea. You see him doing this . Okay, and you see here, you have this property. You see, eventually, when you fix the code, it actually has an error surface. This is the user interface of our tool.
It's a little hard to read sometimes, but people like it. But you can have, you can have informal too. You can take a look at our tool's interface, which is similar to a debugger, or you can see it informally. Okay, that's an idea. What am I showing you here ?
So, this is a broken property and, uh, there is a transformation. Okay, wait a second. So, I...Yes, now you fix it, you see the code is fixed. The code is fixed with a simple fix in this case using a parameter.
And in fact, in this case he can prove the property. And it's a completely different situation with LLM, because now you know that the next version of LLM, you know, MeTaL won't find the bug, because we have a mathematical proof that this code does what it's supposed to do. OK? OK. So, what about the actual code?
So, let's be frank. We have been playing with this instrument for about 7 months. We applied real code, in particular RVV4, which we use and want to use more in real code. We want to apply it to more real code on the blockchain and to more real code off the blockchain. So, this is an example.
This is a real example. We anonymized it. This is one of the interesting protocols that I want to show you. And this is actually code that is not an error, because why isn't it an error? Because it is code that is not deployed.
When the code is not deployed, even if it is more interesting, it is still not a bug. So, I want to show you what it finds in the code before deployment. So, this is a mistake that the tool prevents tool prevents . Good. So, this is a real- life example.
You can probably guess, but I try to be sufficiently anonymous. So, you see, this is a real-life example. And that's basically, we took the code, handed it over to LLM. Of course, we also handed over the design documentation design documentation . We gave everything we had .
We didn't provide any rules. And this is the project we were going to test going to test . We didn't do this before the audit. So the idea is that usually during an audit we have a team, a security researcher, a formal review. Before anyone looks at the code, we ask LLM to review it.
Good? So let's see Good? So let's see what LLM does. So, LLM comes with features. Good?
LM comes with properties. It comes with 15 properties. See? 1 2 3 It's coming, and maybe I can tell you what it is . Uh, you guessed it.
This...What do you call it? Something like a mechanism for gambling or something...You'll understand if you want, but it's a mechanism that allows you to gamble for money or something like that. And it identifies some properties of gambling, and it identifies some really interesting properties of it.
Again, I'm not saying they're as good as what people in Satara have who are very experienced in this business. But this is something that is a step, and it is done completely automatically. You can improve on this. This is done completely automatically completely automatically . You see it.
It has 15 properties. OK? And maybe I want to say the last thing that's simple, but actually people in this industry understand it as a function of as. When the contract is suspended the contract is suspended , the execution of work on the session, the sender must skip. So, this is some kind of condition.
In fact, we've seen hacker attacks that happen like this. So, this is actually some kind of condition that has actually been identified. It is identified automatically by the tool. So this is a property that, as you can see, has been derived. OK?
And so, this is a property that this tool automatically outputs automatically outputs . And what happened then? It has been transformed into a real image. This is an LLM. And in fact, you see that LLM finds a violation here.
LLM finds a violation. In fact, we confirm this by saying that this is actually a violation, which is a real mistake. And actually, it was also LLM that brought out the fix. LLM brought out the error, and LLM sorry, LLM brought out the specification with the same seriousness. This is actually interesting.
He tells you that I will use the C Z3 prover. And then he says what he does. He applies it. In fact, he doesn't need us. Does n't need us at all.
That's all he does here all he does here . And again, I'm not saying, but it's interesting, and I think we can do this for the lease protocol, we can do this for more things. Good? Well, what am I showing you? So here's the fix, you see, it actually writes the suggested fix to you.
Again , this isn't something you need to configure, but what's interesting is that we can test the fix. Because we have a rule that can actually give you a formal guarantee that once the fix is made, that rule will not be broken. We have a mathematical guarantee that this rule applies in all scenarios. Okay, so that's an idea. I don't know what I'm showing you.
Well, okay. So, what is the status of this tool? So, we have this tool available now, and it's only available at this time for reliability. We are in talks with other people about developing it in Rust and others. It is also GPL3.
This means you can contribute. This is the same thing we did with the proof. It's just a question of durability, but we're thinking about rust and other things. Also, one more interesting thing about this tool that I showed you for testing, but we don't mind testing. It generates tests.
It generates tests, just generates tests in the foundry . It will generate tests on other things as well. It will generate tests. And we also wanted to launch a product. We haven't always had it all right, but let's see if we can do it we can do it .
July 15th is our deadline. And please, there is a list you can sign up for. And the difference between this product and this product is that it actually uses LLM. It is agnostic to LLMs, but we only support a few of them at the moment. And by the way, this tool also includes error detection, including static analysis, includes many things.
Everything we did at Certora last time, including, of course, rounding errors. Everything we did, we combine into one basket. And all this with open source code. We have united everything. We are betting on LLM, like many other companies.
So we decided to combine all the tools together. None of this is perfect, but we will get better. So will get better. So , it will come on July 15th. Ideas we want to make to prevent many mistakes.
Pricing is very simple. We charge for the tokens we have, and it actually seems like AEF would want to sponsor some of that. It's not us. So our idea is that we will charge based on tokens. And of course, that's basically an idea, and I can give you a price range.
Right now we're talking about $300 to launch, but we want to bring that price down. We want to lower it. The idea, and again, this tool hopefully won't replace our professional service or any other people on the team, but it's a start. And this is the beginning for this industry. And I'm sure some people will abuse it, but it's the tool it is.
OK. I think, I hope, I'll be able to do a good job on time. I want to actually benefit from this. I think there are two very interesting conclusions from this report that actually surprise even me. The reason people are concerned is that I work in the formal verification field, I'm sure you can see from my age, which is at least 35 years old, maybe older.
The reason why we now have all the venture capitalists venture capitalists who are interested in formal verification is AI. Because they say, " Because they say, " Look, how do we prevent all this bad stuff from AI this bad stuff from AI ?" And you know, of course, we have competitors, Harmonic, Axiom, whoever. We actually have a lot of competitors who are amazing teams raising huge amounts of funding. Perfectly.
All friends, that's good. So, many competitors come to each of these reports , we have three companies coming for formal verification every day. This is great. Because people are trying, and also the internal amazing team, Amazon, Google, all these guys are trying to use formal verification. This is great.
So the idea is that these guys are trying to help against the hacker. Another interesting thing about AI is that it not only makes formal verification useful verification useful , but it actually helps make formal verification easy. And that helps with many, many things. This helps simplify the closer. It so happened that I'm going to show you how it gets the specification gets the specification , but I didn't show you that one of the things that this tool does is that it helps internally.
We have stories where the closer, our tool, found a bug that allows a contract to be completely exhausted, but our team has to spend two weeks understanding how this happens in this scenario. So, essentially, the tool takes the output of a saturable closer and tries to make it understandable to a human. We don't want a PhD to understand the result of a formal analysis and sometimes use a tool to find an error and tell you in this situation that you probably had an error. I don't know. We had this sushi bug that we prevented, which allows us to infect and exhaust all the code.
And it's interesting that the closer finds this in 5 minutes, while it took our engineer 3 weeks to figure it out. Eventually, we showed it to the developer. The developer said, " The developer said, " Forget about it." We know, we know." So, we want LLM to do the necessary formal verification, but this would simplify the formal verification.
So, we have here, we have a code, a QR code. Please register. Please ask us. Some of us are here. We have a stand.
Our engineers, in fact most of them who do this, are based in the US, but we are a global company. We have security researchers everywhere. Please ask us. We want you to actually use this tool. That's the idea.
And thank you very much for your attention, thank you. We hope you find this tool useful. Thank you very much. Thank you very much.
Automatic transcript — names and jargon may be misspelled.
