Beyond Finding Bugs: Proving DeFi Safe | Hao Chen, CertiK | ETHTaipei 2026

Good morning everyone. Uh in the next few minutes I want to share with you that how former can help to reshape the landscape of the security in a smart contract development. So that basically also like answer the question of Matthew that we are trying to fix the trust problem of the trust your code is secure um I think it's still not working. So uh as we see in recent years the AI agent has a drastic advancement and the large lang models find much much more vulnerabilities that we can never imagined before and the trend is still not stopping as we can see that in the foresee that in the near future that the AI agents can reveal even much deeper vulnerabil abilities then we never see and also the takeaway is like this. So if your code contains any bugs AI agent will definitely find it.

So that becomes an asymmetric battle between the uh security engineers and the developers and the attackers. So in the past the security engineering the goal of the security engineering is about to increase the cost of the attack. As long as the cost of the attack is higher than the GAN of the exploit we can consider that the system is secure. However, with the help of the AI agent on both side, the balance is the weight is not balanced at here. As we can see that the attackers only need to find one bug in order to exploit the entire system.

However, the um security researchers and the developers needs to find all of them and also patch them and make sure that your p patch does not introduce more bugs. Also for the for a DI system those system always connect interconnected with each other. For example, a DAX usually needs some uh Oracle or bridges to make it work. So the attackers only needs to find the weakest model in the entire system hierarchy so that they can just launch the attack. However, the security researchers and the developers needs to strengthen the entire system in order to make it secure.

So it comes to the conclusion that the cost effective is not balanced between the attackers and the uh security researchers and developers both of them just I mean even a less skilled attackers they just can burn some of the tokens and they can exploit a huge amount of assets that is running behind the protocol of the D5 uh smart contract. But for the attack for the defenders they needs to like uh burn more tokens in order to exclude all the tokens or order to include all the bugs. So are there any solutions to this uh unbalanced or asymmetric pattern before we talk about solutions let's first write down the realities. The fact the first fact is that if there is a bug in your code AI will find it. And the second factor is that the defenders always cost more in finding bugs than the attackers.

And the third fact is that defenders have a head start. So I guess that is our last advantage over the attackers. So the goal is clear after we write down these three facts. We must eliminate all the bugs before a contract goes online and do it cost effectively. So let's look into our toolbox what we have for example testing fing or having a expert review all of them are trying to searching for the box now to eliminate them.

So there are probably there are good solutions probably not the answers that we are searching for and in this case we probably need to jump out of the box. We need to not just searching for the box. We need to find another solution. So can we just write a rule and can this rule ever be broken? And uh the answer is that if we can make sure all the cases all the scenarios this contract can accept all of them are only allowed by the model that we have writ.

So in that case we can make sure that our code is actually secure and it is eliminated all the bugs. So this way is usually called formal verification. So what is formal verification? It basically can be split into three steps. The first step is to turn of our code into a rigorous mathematical model.

So that in that model we can really reason about the execution of the code. And the second step is about specification. Specification help help us to translate uh help us to translate our uh intention or our expectation to the code into some uh uh into some mathematical based formulas. And the third step is to really write down the machine checkable proof that shows that for any cases if if our code execution that help that uh transits the state states from S to S prime then S and S prime is satisfied by the formal specification. So this phone verification seems very simple and uh it is very powerful but why most of the companies does not already use it right now.

So after decades of the working on the formification we have identified two obstacles to prevent this to be widely used. The first barrier is that how to write the proof. Uh if you can recall your high school geometry lessons or your college calculus lessons, you know that when you want to write a mathematical proof, it really needs a lot of efforts to put in. That alone if you want to prove your entire codebase is safe, you have to write the proof for each of the functions. And the second barrier is even harder than the first one that is that is how to um what what what should be right as a form of specification.

What should be what should we prove? In that case you have to not only know that uh what your code intends to do and what is the background of the code. You also needs to do the common tax scenarios and you must know you must be an uh security expert in order to write meaningful specifications. So after several years that we put into the form application on the smart contract we will see that this will about to change because we have developed uh we have basically tackled these two barriers. So for tackle the first barrier we have developed a new prover.

That prover is essentially a native prover and with that prover you can just write the proof as easy as just talking with AI agent and this prover is fundamentally built on top of two engines. The engine on the left side is automated prover on top of a SMT solver. Uh this prover it can handle all the basic proofs and to make sure all the proofs are sound and deterministic and on the right side that is the AI harness. it can just inter interact with the SMT back prover to make sure that all the undertaking tasks um can be translated into the basic proof conditions so that it can be uh automatically checked. And these two engines will work together to break down all of those hard proofs into very very small step proofs and to make sure all the small step proofs pass and all of them can construct the entire goal that we want to prove.

So to give you a concrete example, we recently have verified a highly optimized solidity exponential function uh from the scratch. So this function is optimized. It has like half of the code is written by inline assembly and the entire proof from the scratch to the end of the proof only take one day. Uh that includes the AI uh writing the proof plus the human review the proof and the entire proof generation and the checking only takes like seven minutes. And we uh and the entire proof script is about 2,000 lines of code.

Comparing to the linkful based uh proof, it basically takes only one10 of the proof scripts to fully generate the proof and it is not just a trivial proof. It basically uh uses tons of the proof technologies requires the mathematicians expert to construct the proof. for example, tail light expansion uh evaluation and so on. And to tackle the second barrier uh we have accumulated a methodology to help to know which part of the code is the high-risk area and to know uh how do we translate our attention into the expected security properties and turn them into the uh formal specifications. So we call it audit to proof.

So audio to proof uh you can imagine that after you uh after you write a very nice smart contract and before you release deploy it on chain you probably will do a audit on your code security audit on your code either internally or externally. After that audit you may find some uh you might find some findings and you will turn those findings into fixes into patches and that is most the team just end but we just take one step forward. We turn all those patches in into a new engagement that is called for verification and and afterwards we can produce a ton uh uh several lines of the specs surrounding of your functions and those specs you can view it as a transfer of the capabilities or decentralized of the security capabilities that we transfer it to you and afterwards you can integrate that specification into your uh DevOps operations or continuous integration uh process and you can run that spec at any time anywhere with any number of times as long as you want to optimize or change of your code you can always use the spec to check if your code is actually safe or not. So it's basically uh just leverage the auditors and the former application experts and the developers uh expertise into one specification that you can reuse. So to give you a hands-on uh let's look into a real world example.

So uh in in the RWA we tokenize everything and after we convert everything into tokens we want to treat them. So in order to trade them we want to swap our tokens into some commonly used token. So that is usually called liquidation and we really use a DAX or AMM to do that. And this real world exploit actually costs like $94 million. Um so the uh root cause of this uh uh uh of this is simple.

So usually the DAX or AMM they will just use a liquidation pool to um swap for tokens. For example, if a trader want to trade token B for token A, it will first give the token B to the uh DAX or liquidation liquidity pool and the liquidity pool will use a formula to calculate how much of the token A will return to the trader. So the liquidity pool needs to maintain this function uh that that is d prime that is the exchanged reservation combined reservation of the A and B uh to the uh to the combination before uh they must be equal and right right now we just make it approximate equal that is because the precision loss. So uh this exploit actually makes the uh actually the attacker leverage this precision loss. So you uh in one place the calculation should run the result up but actual the actual code just runs the result down.

So how to rule out this bug? We can do it at the microscope level. So we can just write direct the uh specification onto our code saying that uh so what you see above the function those uh annotation comments about the function they are formal specifications as you can see they are very close to what the solidity code look like. Uh so if you look at the 10 line uh line 10, it basically says that uh the result should make sure the uh the round is always rounding up and the line 11 says that rounding up should have a boundary that is uh between the precession precision and the actual result. But you may say that how do I know that uh which function I should run down or run up.

So that's fine. We can do it at at the designer's level. So for a designer you always want to maintain a invariant saying that uh the combination the curve of the A and B should be always larger than the curve of A and B before the function execute before the swap even happens. So with that you can always know that no matter how many swaps happens uh your value your reserved value will not decrease and we can even do it at a at a very high level at e economy level. So at economy level we can see that if I do a buy and then do a sale of the same token the client or the user can always receive a little bit less token than he paid.

So in that sense the uh AMM or DAX will never lose the money. So you can basically write the formal specification at any level and as long as one specification is fine to be violated. Violated means that the prover finds a counter example as shown below. Uh find that one example that uh the prover cannot construct the formal proof for your code against the formal specification. then you find a bug and you can use this to help you to debug and um finish the proof.

So uh after you receive the formal specification what we want is that you after you receive the full uh the specification you can integrate into the entire development process. So you can use it in every cycle of your development uh to make sure your code is always uh securely checked. So thank you for your attention. So AI lowers the boundary to the attack. Uh let's lower the barrier to secure our code with for application.

Um so I'm happy to