Don't Review the Code: Formal Specs First Smart Contract Development

Transcript

[music] [music] >> Hello everyone. My name is George. Currently I'm at Monad Foundation. Before that I were in DeFi and before that I was part of Solidity compiler team at EF. So today I will speak a little bit about smart contract development process and how it changed with AI. So how many of you have written smart contracts before?

And how many of you reviewed? Yeah. And lately have you have been tasked with like giant pull requests with a lot of code and you have to approve it somehow. I have seen that quite a while lately and I suffered and I couldn't spend any time on reviewing these things because it's just not scalable. And here I will present what what I have been experimenting with last [snorts] couple of months and yeah. So first we'll go with classic cycle.

It it was like this. You write contracts and unit tests for a while. Then you do maybe fuzzing and variant testing which to be honest most teams just don't do don't have time and [snorts] nowadays it's a little bit better but still these have their own problems and we'll see that later. And then you do the audit and finally maybe formal verification and some teams don't have time or resources to do it.

So this was for years. Uh, spec, like English specification of the contract or the system is usually white paper and developers do assume whatever is not spec'd and these assumptions can introduce bugs. Uh, so also tests are written you you write tests only to cover what you thought of. Uh, and that that puts a lot of pressure on the audit because all these places where there's no documentation, where you specify what the contract

should do, very good auditors point you and ask questions, but even they can miss some of these because there is a lot of them. Uh, and now fun part started when agents came into the loop. So you write a short prompt and then agent writes a bunch of code and tests which then [snorts] you are tasked to review as a developer or senior developer. Somebody comes to you.

Uh, the quality of that review is very basic. So you you really are tasked with five different contracts like that. So it's a a little bit hard. It's much faster. Agent does the same assumptions that developer did before. Spec becomes even shorter and sometimes people even write specs after the code is written. So uh, and yeah, as I said, too much code to review really.

And yeah. How many of you in the room is are familiar with what formal verification is? That's a nice a lot of hands. Uh, and how many of you have used it on your contracts? Yes nice. Uh so I'll do very short reminder and introduction for people who don't know what formal verification is. I will use a very simple example. Uh this function adds two numbers and returns the result.

Uh so you would write uh unit test that checks if it works properly. And then uh [clears throat] one of the properties that you can prove for this kind of function is that the result is always greater than A or greater than B. Uh so what prover does, it searches for any pair A and B that satisfies satisfies the negation of the rule. So it would search for A and B such that A + B is less than A. If there is a solution to that, uh it will report counter example and your

property doesn't hold. In this specific case uh since uh it assumes solidity 0.6 which doesn't have overflow checks, this one will fail and give you counter example looking something like this. Uh so yeah, this was very simple example. Much more complex functions require much more complex rules, but just to uh get some uh uh intro. Uh so I started experimenting with writing formal specification myself first and without a single line of solidity

first. So uh I write I I was writing myself formal specification. I was using Certora Cvl for that. Uh I've used also Act, uh but I will come later to that. So, an agent was a CI job that when I open a pull request with a spec, agent writes the rest of the Solidity. I tried also even going further and ask it to write Yul.

So, it's even harder for human to review, but yeah, I ended up writing Solidity with the agent. It produces the code and then the rest of the tooling runs the Certora prover does run proofs that are run. It's like running your code on every input, but in reality is just trying to find the places where mathematically code breaks. [cough] So, why [snorts] do I think it's better?

Because you are forced basically to define what the correct behavior is before you write any single line of code that forces you to actually think about some edge cases and not just skim and assume and go forward. Agent is tasked to write the code that satisfies these rules and even with formal spec first, I got a bunch of counter examples during the development. So, agent agent [snorts] was making a mistake a lot of these times. So, it's it's kind of it was scary a little bit scary.

But luckily, the tooling got it. The idea is that when you are tasked to review something, you don't review the code at all. You review the actual formal specification. Yes, that puts a lot of pressure on the specification to be right, but if you go step back and what was specification before and I think this is much better and much stronger ask and better to put pressure on reviewing the spec because I also do think security researchers I worked with would be super happy if they receive formal

specs together with the code. So my other thoughts were how do I check the tooling is right? So I did something called mutation testing. I planted the 11 bugs in the code that break different invariants. So how does that work? I do change code in some places and I expect the prover to fail and find the counter example.

So with all the process I forgot to mention that the agent wrote also invariant tests and the fuzzing for Foundry. So I was comparing so I was comparing what will fail in traditional setup with invariant tests and fuzzing and also what will fail with the prover. So you are you expect the tests are going to fail especially invariant tests but eight out of 11 were caught by invariant and the fuzzer.

Three were missed. Certora found counter examples for all 11. So yeah, I initially started by using Act plus H EVM. I ended up opening a bunch of PRs and but really it was it was missing some features that I needed and it was a little bit hard to to prove anything anything meaningful.

So I ended up at by using Sertora CVL language is maybe a little bit hard for someone who never saw it and but it works and it gives clear counter examples. There's one thing I used loops because I worked on the Central Limit Order Book. So the loops needed some extra work but it made them work.

So here is side by side what how these three compare to each other and the whole point is what the human needs to review. In the classic environment it was the code. In the Argentic one there was a lot of code and with the formal spec first it's the spec and I do think it's easier to review the spec and it's easier to trust the review if you find spec correct. And yeah this is something that I I ask [clears throat] if I do smart contract development I do it like this now and I do ask people that come to me

for reviews to do the same. So it's spec first not spec once. So whenever you start you write whatever feature set you have but if you want to add something else you need first to write the specs before any additional code is added. So it's just a loop and whenever there is a problem with the proofs or counter example is found it it either means that some rule is wrong or the code is wrong. Usually the code is wrong. So then you fix I mean agent fixes it. This was all set up as a CI job whenever there is a counter

example agent was working back to fix it. And that comes to like something that Muly mentioned during opening and that's informal specs. I think actually that this is the hardest problem. How do you write correct specs in plain English? Agents are super good transferring that to actual CVL or act or any other language.

So yeah on the right side you can see in plain English this one is rather simple. It was the vault that was used for deposits and withdrawals. It does explain what solvency means and agent is moving really quickly when there is something like this. Making informal specs correct I think is very humans are still much better than the agents. So my example which you can later find the QR code to the GitHub with the GitHub link but yeah it has the

factory that is permissionless and deploys the markets and it had a vault that is the only place where I have external calls to ERC 20 tokens. It was done like that to remove external calls to unknown source code to make market market rules are much more complex and I wanted to remove external calls from it so they only call to known code base.

And at the end, I was thinking how someone will review all these specs. So, I experimented a little bit with writing a dashboard that will explain the specs in a plain English. It it it is something that would for example help security researcher actually figure out what does every single rule mean. So, if you just go to the dashboard and you open a rule, it explains in plain English and then there is on the side how it was implemented with CVL.

That's just a nice thing and it can be automated as well. And yeah, my final thought was that you should point AI at writing the formal specs. Human writes the plain English. In what form that's something that I'm still thinking about. I I have some ideas. We'll spend a little bit more time on that by building something that is not DeFi or or order books because there is a lot of code that exists for these agents do

understand these already very good. So, I want to try with something more wild. And the next steps would be basically what I explained. Currently, my thinking is that some form of like if you have decided on the architecture, you could probably draft Solidity interfaces and use some kind of custom NAT spec maybe to write plain English rules and invariance of the contract and then feed that into the agent

to provide you back with the rules. But there there are other approaches as well. I'm still not decided with this. I will try other, but I think this one sound to me as a developer sounds the the most viable. And the automation of spec visuals is yeah, currently it is automated, but it requires still some fixes. Yeah.

And that's it. If you have any questions. >> [applause] >> Thank you very much for the talk. Now I think it's very clear to everyone and we'll get to the questions. So let's pick up the first question. You don't formally verify code. You formally verify some properties of the code. How do you ensure that you're not missing key properties in your specs?

>> Yeah, that's a good question. That's the same question for are you missing some properties if you write directly the code and I think the answer is the same. You have to review them and try to think of all the possible cases. So it's still a pressure on the human, but I think it's at the right place because the rest of the tooling is kind of solved. >> Okay. And what is the best level to formally verify smart contracts, solidity, EVM bytecode? >> I think personally that running the formal verification directly on EVM is the best on the compiled bytecode.

So you you have to trust the compiler otherwise, but I know there are some tooling also. It depends like if you basically use one version or the other version of the compiler, some properties might change with the breaking changes. So it's the best just to run it purely on the bytecode. >> Okay. The next question is current former verification tools have limits, hashes, loops, arbitrary length.

>> That's a very good question. I didn't run into these these problems with the example I built so far. Yes, these are the hardest problems and in some cases you cannot prove some of the properties, but in my experience, if you have formal specs, even if some parts cannot be proven, you get much better code from the agent compared to if you just one shot it without any formal specs before.

>> Okay, thank [snorts] you. And the next question Lin V4 was was suggested by Justin but isn't good for verifying specs for smart contracts. >> That's something that is an interesting and my opinion is some if there is a trusted tooling that can translate Solidity into Lin, it might be good, but I still think that the best way to formally verify is to formally verify execution and not the spec itself.

And I think Lin Lin part doesn't still do that. >> I like this one. Be honest. Who is better, you or your agent in writing code, be honest. If your agent is great, then will you open source the harness? >> [laughter] >> This is the best question ever. I still think I'm better, but I'm just super slow compared to an agent, but it might change very soon.

Yeah that's I can share and open source harness, but I don't think we will be ever writing the contracts again because of the speed. >> Thank you. And next question, do we need verification ever language for smart contract development another language? >> That would be interesting approach if there is a language there was when I was at Ethereum Foundation, I worked slightly on SMT checker, which was some kind of tool that would

help verify some properties of the contract. But if there is a language or a compiler that can [clears throat] target this specifically, that would be probably super cool, but I'm not aware of anyone currently doing that in a production grade way. >> Okay, so I think we can one shoot the last question. So what language features would you like to see in Solidity? And please one sentence.

>> I don't think Solidity feature set would matter that much here, but yeah, SMT checker was a nice try, and I think something like that would be very welcome from my side. I think productionizing that would be super cool. >> Okay, thank you very [clears throat] much George for the talk. And please >> [music]