Why am I doing this talk? The candid motivation is I want you as developers to do more of the work that you assign to auditors yourselves. We get a lot of questions, you know, someone signs up for an audit, the audit's gonna start in two months, the code will be frozen, and then we invariably get the question, can we help you prepare for the audit somehow? Can we help you get, like, make sure that the audit runs smoothly? There's a few obvious ones. Do you have a pointer? I do. These things I'm not gonna talk about because I hope dearly that if you hire an auditing company, you have good tests, they run, they pass, you have integration tests, you got documentation, and you make sure that your devs are available for the couple of weeks that you're gonna spend in an audit in case a question comes up. Those are the basics. But I know a lot of teams are really, really highly skilled and they're very motivated and they want to do more if they can. So well, what can you do? What's, what's the secret sauce to getting a good audit? Actually, what's the secret sauce of the auditors, auditors like us? Different audit companies do different things, but we have our own little method of working, which I'm gonna share with you. Invariance. We like something called invariance. Sometimes you call them properties or property-based tests or whatever your favorite equations overstate. I usually just use the word invariance for everything. They help you find more bugs, write better docs, trust your code more. They help auditors because, you know, as auditors, especially we, we're gonna be looking at invariance and trying to find more of our, like, invariance of our own, basically. So if you come with a little set of these that you've already gone over, you've done some of our work for us. And we can focus on like either deeper work or we can work more efficiently and get you done faster. So we want you to come up with invariance if you're on-chain code. They're also good fuss targets. We're gonna get to that. They also, one thing we found, especially developers, they can tell you exactly like, oh, you have to go to this function and this function, you will see exactly where this variable get updated and everything. And once you start talking about invariance and we say things like, well, just a sum of all balances always match a total balance and so on, then we find that a lot of auditors, sorry, developers start looking at their code from a new angle because this is sort of a top-down angle. It's almost like you're coming back to the design phase, moving out of like the optimized imperative code and thinking in more declarative fashion. Don't have to read all this. I just like to have things. I know this is being recorded. I myself like to pause the talks and like read slides. So I put more on here than I'm gonna read, so don't read all of it. I'm just gonna say really quickly. Here's how we're gonna structure this talk. We're gonna go over like how to make invariance. I call that state is just equations. Then how to prove invariance, at least in a pen and paper fashion, which is what we often do. Talk about how to approach things when you can't really get your proof to work and also how to use your invariance to do fuss testing and even monitoring if that's something you want to do.  If something comes to mind and you want to write that down, please do that. I'll be working over an example from an audit we did a while ago. So if you don't have any code you're working on right now, or you just want to follow through now and then go out and start working on invariance on your own after this session, that's fine, too. I'll also, it's a lot to cover. An hour isn't really enough. Anyone here interested? We can just grab a table. I'm happy to take anyone from this crowd anywhere and just keep going with the workshop if you want to keep working on invariance afterwards. So just just grab me, we'll find a table somewhere, and as many of you who want to keep going, we'll just keep going. I like this a bit too much. It feels almost pathological, but I love when developers come up with invariance. So testing versus invariance, testing is, I guess, I didn't see the previous talk, but I think he was talking about how to do better tests. Tests are sort of like the camping knife.  It's our first and most robust line of defense. There's a myriad of resources to help you test better. There are talks here probably how to test better. So again, I assume you already know how to do tests. I assume you do unit tests, that you do integration tests, you try deploying on test nets and so on. And my analogy for tests is it's sort of like an experiment, right? You're trying a single thing. You're going to see what happens if I do exactly this call or I do this little sequence of calls. It's great. And we often like, especially test-driven developers like to talk about testing as, you know, some sort of silver bullet, or even if they say it's not, then you can kind of feel like, well, the testing is what you need and that's going to solve your problems. But I don't know any developer that actually trusts their code enough as, oh, my tests we passed, bring on the billion dollars TVL. That doesn't happen, right?  Like, have we thought about everything? And it's sort of like, that's sort of like theory. Recently about code is like developing a theory. It's like what if the experiment is, or if testing is just an experiment, like in a physics or like a science context, they help you verify that your theory is correct. And if you do enough experience, you might be pretty convinced. But you also probably want to make sure, go over your theory and see if like, are there any holes in it. Does my theory lead to inconsistencies? Even if you tried 200 prime numbers, where it may be prime number 201 is going to be the one that breaks your little mathematical theorem. So you need to be reasoning about what your theory is saying. The thing is there's very few resources about this. I had one five-minute talk by my professor when I started college saying like, here's how I run over code in my head. And I think that's that's the end of it. And it feels like reasoning about code is something you learn from experience. It's something we're always doing when we're debugging, doing code review, doing design discussions. We're kind of like simulating things in our head. But there's not much resources about it. No one's really teaching you how to do it. It's just sort of like, well, you're a good developer with time you learn it. So I want to change some of that by giving you some structure. If you don't know where to start reasoning about your code to make it more secure, here's going to be a few steps to get you going. This is meant to either intimidate you or titillate you depending on what your, what kind of person you are. But we're doing something that's sort of analogous to math proofs. So in math, you were taught both like computing answers, like figuring something specific out, but also how to do proofs, how to make sure that the algorithm that I'm doing is always going to work. Again, it's sort of like the analogy testing versus reasoning experiment versus theory. Reasoning about code is analogous for proofs before anyone say, Curry Howard, like I'm not talking about something like that. If you're a theoretical computer scientist, I'm talking about something very straightforward. And I think anyone who has taken a basic code bootcamp should be able to do. And just like proving there's a method. There's a bit of archistry. It's not always straightforward. I can't guarantee you that your proofs will work even if your theory is correct, but there's a structure to it. You don't have to just be flailing around trying to prove random stuff. And with that, we get to the actual invariance. What is an invariant? What are we looking for? What are we trying to do? So this is very small. So once the way to think of a good invariant, it's something that it's obvious that the code is doing or should be doing. But if it works correctly, it should be doing this specific thing, but it's sort of incidental from the code. Nowhere in the code is this like directly enforced. It's just something that sort of should be obvious from your business logic.  But to be completely honest, starting with really simple invariants will get you quite far most of the time. And we'll do a very simple invariant here today. And I can tell you from experience that even those really simple invariants that aren't like super high level claim that the entire protocol is perfectly secure, they still help you find bugs in your code and we find bugs all the time using them. Um, invariants defined as it's not varying, it's constant in mathematics is unaffected by a designated operation and or an invariant quantity function configuration of a system. It's something that's always true. You can think of what's the code behind the code because the code is very exact. It's imperative. It tells the computer or like the EVM exactly how to do every little step. Uh, so it's not, it's, it's imperative, not declarative is one way to say it. And here's your chance to be declarative. You say something like, you know, here's the equation that should always hold. I think any ERC, ERC 20 contract should have this property, right? You keep track of the total balance.  And we just kind of assume or like we hope or we might be very, very confident that the total balance is going to be the same as the balance is in each individual account that has interacted with. The mapping of balances. So this is just a way to say, take all the balances in the mapping and sum them up. If someone knows way too much about the EVM like I do, then, uh, just think of it as every, every time you wrote directly into a mapping. Technically, the mapping contains a bunch of other stuff, but, uh, don't worry about that. Uh, and again, a great invariant is something that's obvious from the intended business logic like this. Like, of course, you know, the total balance should be just all the actual balance that are out there, but it's not necessarily obvious from the code. No, we're in the code of the stat. There's no one summing over the balance anywhere in the code. Um, here's a working example. If you want to, if you don't have any code of your own, you want to pull up and follow along on your, uh, laptop. You can go to, uh, GitHub, alchemics, finance, V2 foundry repo. It should be pinned at the top. Uh, we're working at the contrast alchemists. So we're going to be like control effing through a little bit of it. If you want to follow along properly. Uh, or you can just watch the slides, uh, really quickly. This is sort of a slightly more involved version of the, the sum of all balances, total balance invariant. They have something called shares that they're used to, uh, that they used to make sure that you get your, you know, your, your yield in proportion to how much you have staked, uh, essentially. And then for every specific yield token, there exists a total shares valuable. So slightly more involved in this, the sum of all balances is total, total balance invariant. Here's how you frame it as a mathematical equation. Uh, if you go into the, uh, mapping of all the yield tokens where it contains the token address is a key and a set of params. That's this yield token params. If you go into the params total shares, that should be equal to the sum over all the accounts, uh, this value of each account. Uh, that's just one invariant we come up with. We proved, uh, it turned out helpful. I'm not sure if we actually find any, found any bug on that one, but you know, we do find bugs on those kinds of things quite often. Um, but the question is like, so if you're sitting here with your own code, for example, or you're watching this later, you're thinking about your own code. How do you come up with good invariants? Uh, how do you come up with like looking for something like this? And there's a few tricks. Um, first is to come up with many. Like try to think of anything you can state as an invariant, uh, state that as an invariant and then focus on the ones that seem to be important. Um, second one is go over storage variables. Do you have, uh, do they have like obvious relationships? This was a good example. You have the balances and you have the total balances. Of course, that should you stick out as a sore thumb, like that's these, these two things should have a very tight relationship between them. Um, ghost variables is a nice trick. That's sort of just like introducing variables that don't exist directly in the code. Um, but that you can use when you're reasoning over pen and paper. I'm going to give you an example. Um, deoptimizing is always fun. Like you're doing a lot of optimizations, even if you're not doing, even if you're not a big optimizer, or you're not iterating over all the accounts of all your users. For example, that's a sort of optimizations as solidity developers, we need to optimize. But what if you just think, I don't have to optimize at all.  And then you just state the invariant saying like, well, this, this naive implementation and this optimized implementation are identical modulo gas usage. Um, go to your design spec. I hope you have one. You all write design docs, right? Um, read it over to see if there's anything you're mentioning there. That's obvious. Like that's something that there's a good chance that says something in the design doc. Like, well, these, these two variables should have a relationship to each other that might not have been carried over to your code comments. So you should go to invariants and you can also work from unit tests, like replacing unit test values and start thinking about what if we'd start fussing it? What if we use symbolic values? What properties would they have to satisfy? And then just try to state them as, you know, equations or something similar. It doesn't have to be a mathematical equation. You can also just be a very exact description. That's what happens if you open a math paper. It's, it's not all just a set of equations. It's a formal, formal line of reasoning written in English. Uh, and that's fine too. Uh, so ghost variables are just a way to introduce variables into your invariants or your system descriptions that don't exist on the chain or that you don't have on the chain. Um, so. Impossible to compute functions. We've seen already some, some overall balances. You can think of that as sort of a ghost variable. You can't really do it on the chain for several reasons. Uh, but you're absolutely free to use it in your, uh, in your invariants and just make sure that, you know, whenever you're adding or subtracting from a balance somewhere in that mapping, then, you know, that some gets updated. Um, another one is like, well, total deposited ever, for example, how much ether has this contract ever received? Maybe you're not actually tracking that. You can't probably actually track that in your, in your contract. But if you're just reasoning about, uh, um, about your contract, then you can say like, well, how much ether has ever been in this contract? Make that a variable and use that in your equations. Um, and hopefully you may decide that some of these ghost variables actually deserve to become state variables. It might make sense to actually keep track of these on chain. The way we do with totals, uh, even if it's just for monitoring, even if it's just a little view function, even if it costs a little bit of gas, it's going to help you reason about your code, monitor your code, and like, make sure you can run your tests on, um, on chain state forever. Uh, here's an example of deoptimizing just to give you a quick look of what that can look like.  Uh, when you give rewards, then you increment the total reward ever. Variable, that should be a semicolon there. Uh, and where did all the semicolons go? Must have done a search replace. Oh, well, um, that's what happens when you keep copying over from different resources. Um, and then when you withdraw a reward, you just calculate, you know, whatever a user has a specific stake and you can say the last time they reserved it, they received a reward.   And then when they withdraw, you just set the rewards to zero and you send the tokens. You can't do that, right? That that's not really possible. And if you do that, I will slap your fingers. But if you can definitely make a statement like, Hey, these things will give the exact same, uh, results for a single user, right? If we call the give rewards with a certain number of amounts and then I call withdraw rewards, I should receive the same things from both of these implementations. That's a nice little invariant. Um, oh, no, this, this would be just like, you know, in a, in a dot, like we're going to get to like part of the reasoning. Yeah, I want to also emphasize and I will emphasize a few times you need to show your work again. Like, I feel like a math professor here, but like show your work because there's a lot, a lot of work involved in coming up with the invariants and improving them.  And that's can be expensive for you. So make sure that you, you know, have it, I don't know how you like to document things. If you like to do it in your codes, in your code comments, or if you want to have a Google Doc somewhere, whichever this, but, but this, like, you can have a few pages in a Google document that say like, Hey, what if we implemented like this? Here's our action implementation. These should be equivalent. Here's, you know, pen and paper proof showing that it should be. Yeah. So that this just doesn't work in, in a real contract because sorry. Oh, yeah. Yeah.  Like all the examples here are illustrative. It's not, they're not, this one isn't pulled from an actual deployed code. It's just, you know, a quick example of what the optimization looks like. Or I can say, oh, it's, it's pseudocode. Like, because some of you might be writing Viper and this is the process that works. So, okay. Now we get to actually proving them. So you come up with something that you say, like, well, this should always hold over my contract forever. Proving, I had a math teacher said, like, well, proving sounds scary. Like all you, you just need to convince someone. How good does your proof need to be? Well, you're going to have to show it to someone. If that's you, if that's your friend, if that's nature magazine, then, you know, whoever you're talking to, you need to convince them that, yes, I know, like, my argument is sound and it's complete and, you know, my, my, my theorem holds, right? The good thing about code is that it's usually boring and straightforward. It's pretty mechanical because hopefully the code is pretty straightforward. And all you need to do is check a bunch of places, which can be boring, but straightforward, usually. So how do you prove an invariant? Well, straightforward. You figure out where are all the variables or ghost variables that are ever written to? Where are they modified? You find all the locations in the code. You list every function that modify any of these invariants. You make a list. If it's a Google doc, if it's, you know, if you have some cool Emax tool to do that, go ahead. Just make sure you have a list of them. So this is like manual verification. Like of course there's, we work with tools. We mechanize things. We love building tools to do these things, but it's actually very, very useful, especially for smaller contracts that just do it as pen and paper a lot of the time. So don't get intimidated when I say, like, just write it down. Like write it down in the doc, document and follow through. It's, it doesn't actually take that long most of the time. Then you check what's called the base case. You check that the invariant will hold from the start in the constructor, the initializer, wherever, just make sure that like your invariant isn't invalidated immediately as the contract is deployed. That's usually the easy part. And then the hardest part is the inductive case. You find all the locations that you noted here and you go over all of them. You can assume as you go into the contract that that's the transaction start that the invariant holds. And then you just look at all the locations that modify the variables. You do some symbolic updates. Just say like, I'll show you what that means in a second. And then you check that your invariant still holds. If you do all these and you find that the invariant holds from the beginning and it holds at the end of each function, if it held in the beginning, then you're done. Like the invariant holds forever in this contract. On the working example, so if you pulled up the code, then you can control f for our variables, which are total shares and balances. If we look over the contract, I usually use a silver searcher and some other tools just look get an initial search for where all the places where these variables can be modified. There are more structured ways to do this, but just use the fastest. Make sure you look for assembly code because it can modify your storage variables. And make sure you find all the relevant locations. Also look in the contracts you inherit from because modifications can happen there as well. Use a dependency graph tool if you need to. In this case, we find these three functions modify our total shares and balances. Add yield token, issue shares for amount and burn shares. These two are internal, this one's external. I can just tell you the add, the first one, add yield token is fine. It just sets the values to zero. Constructor and initializer doesn't really touch any of this, so everything's zero. So we get initially zero equals zero because the total shares for every yield token starts at zero and all the balances start at zero. So this is the sum of zeros and we get zero equals zero. That's true. So the invariant holds initially. And then we go and find the issue shares for amount. We find that in these two locations, our variables to balances and total shares get modified. Technically, it also makes sense to reason about like is there, could there be re-entering scene here? Actually, in this case, that wouldn't matter. Are there many different paths through this function? No, it's a very straightforward function. Technically, there's a path here, but that doesn't matter for us because the only relevant changes are in this basic block. There's failures, but if this function fails, then the state doesn't get committed and it's still fine. So we find that we add a number of shares to total shares. Read very carefully. Accounts, recipient, balances, yield token shares, yes. Heal token, yield token, total shares, yes. Okay, we just add shares to both sides. Note that we don't really care how the shares were computed. Like this might be an external call. Like anything can happen here. It doesn't matter. What we know is that if we come to this location in the code and we go through this line and this line, our invariant will hold once we're out of it. This one is left as an exercise to the reader. It's slightly more not challenging. It's just the exact same thing. But I mean like now we've proven this invariant and it may sound slightly meaningless. That was one of those questions that come up as you're developing. Hey, am I sure that total shares and the balances, they should always match? I should check that at some point. Maybe I haven't, but now you have checked it and you've wrote down your proof, hopefully. And now you know and you don't have to worry about it. That's one good thing. You can convince everyone that the invariant holds. The case may seem trivial, but as things get hairier, the bugs get scarier. And this class of bugs are definitely out there. People do forget to do the second variable update. I mean, it wouldn't be crazy to find this code without the second line here. It happens.  Because this is actually used to calculate rewards. And if this line was missing, you'd be in deep trouble and your auditors would find it and report it at critical vulnerability. And again, make sure you save yourself somewhere useful, somewhere you can find it, somewhere you can show your colleagues. So you don't have to redo your work. Of course, did anyone pull up some of their own code and was looking for invariants in that? Someone, okay, cool. So I know that you're all hardcore super developers and your code is not always the straightforward. So what do you do then? Failed proofs, and I don't mean, if you find that the proof doesn't hold, then your invariant isn't validated and you need to make sure that, figure out why it doesn't work and fix that. What I talk about here is failed proofs is when you actually fail to prove it. You didn't really conclude that your invariant doesn't hold. You're not sure it holds. What can you do? Especially as code gets hairier. Well, so when that happens, it's actually a good guide to refactoring and refining your code. So here's some basic tools that we can use and we usually recommend, like if we can't prove an invariant and we really try to, then we usually ask you, like, hey, can you make this a bit more clear? Because we haven't been able to convince ourselves. We haven't been able to convince you. You should want to be convinced of this invariant. And until that happens, we should make sure that we can either help each other reason through the code or we can make the code more easy to reason about. So if the function's logic is too complex, if you really don't want to refactor, one thing you can do is you can, instead of giving a name to each function, you give a name to each basic block. Does everyone know what I mean when I say basic block? Okay. Going back. So a basic block of code is a code that will always be executed together. So for example, if you enter this, if you enter this function, this can't fail. There's no branching here. This can't fail. Well, this can fail actually. But if we ignore reverting failures, for this case, which we can, because reverts will just mean that nothing happened, these three lines will always be executed together. And so will this condition. But this line may or may not be executed. So you can think of this as a basic block and this as a basic block. If you have a while loop, then the body is a good example of a basic block if there's no more branching in it. Basically anything that's like, you can treat us a solid chunk of code that will always be executed together with each other. If you had thrown this line into here or like another if case, then it would not be in the same basic block. And then it would be harder to reason that your invariant holds. So yeah, I mean, that's what a basic block is. It's a single piece of code that will always be executed together. And if you have really complex logic and your functions are really big, you might want us instead of giving labels to just the functions, you give labels to each basic block. And the reasoning works the same way. If you can prove that after each basic block as you go into it and as you come out of it, the invariant holds, then your inductive proof is fine and your invariant holds. What we find sometimes is that you will only, like the variables that need to be updated together are updated in slightly different places. And then we get an argument like, well, you know, but they will always, because of like some sort of reasoning about the possible execution conditions, they will still always be executed together. Well, why don't just co-locate them? Put them right after one another to make it easier to reason about them. If you have complex arithmetic expressions with rounding, ignore that for now. Treat numbers as real numbers. Don't worry about rounding at all. You can do rounding error analysis separately. Write your stuff as functions. Imagine it's all real numbers. Make sure your invariant holds and then you do rounding error analysis. We did a talk on that yesterday. I'm sure you can find the link in the DevCon videos about how to do rounding error analysis to make sure your contracts are safe. If you have a bunch of different invariants, a nice thing is to do what's called framing conditions. You just write over each function, which storage it modifies. So you can look at a function and say, well, this function modifies all these storage variables. If it doesn't modify any one of the ones you care about, then you're fine. If it modifies one of the ones in your invariant but not one of the others, then you know, look out. But it's just a good way to build up your code with comments that will make it easier to reason about in a structured way if you're doing this more and more. Again, did you check everything? Imports, inheritance, both up and down.  Control f is not enough. And if the code keeps changing, if you're doing this as you're prototyping, you're doing it wrong.  So this is very much something you will do towards the end, ideally when the code is frozen or almost frozen. So again, if you're asking an audit firm to audit your code, you should ideally freeze it before. And whenever you freeze it, you can start doing this or slightly before. Do you have a question? For the live stream. So pretty much when I have the client that really likes to change the assumptions of the whole projects, basically, then I should, I guess, I should write those invariants, but recheck them every time the changes happen, yes? Yeah, and I mean, that can be a statement of work. Hey, we did all these things and then, oh, we just wanted to add a new functionality and like, okay, I'm going to recheck these things that's going to take me four days and like, but you already checked them like, well, you changed the code. It's like, that's sort of the negotiation with the client. And it also kind of emphasizes that you do need to freeze your code as much as possible. Again, if you document your proofs really well and they don't refactor everything and change the entire design, then change, like looking over the proofs should be pretty straightforward. If you're used to it, you can kind of work from the diff. Just, oh, they made this code diff and you can make sure that all these changes would serve respect the invariant. Just look at all those locations and make sure that the invariants are respected. Do you have the microphone? Thanks, Yoh. Yeah, I just wanted to add that maybe the thing he's talking about with frame conditions helps with that because you write down, you know, what storage slots each function is modifying until your client, hey, you make the modification, write down the updated storage slots, and then that minimizes how many functions you have to recheck your invariant for because if they didn't change which storage slots it was asking, you don't have to recheck it. I mean, there's a feedback loop here as well, right? I mean, if you write down the framing conditions, put them in the function, and then you can make sure that the client knows to respect them or, like, you know, again, update their framing conditions. And so one beautiful thing about this way of working that we found is a lot of our clients get trained to do this more and more themselves. They start producing better code, it's more readable, it's not always less complex but like the important things are more co-located and so on. So I would say if you personally, if clients keep changing the code, like make sure that they understand that there's a cost to that. If they still want to do it, of course they can do it. But also help them to train them to be better at when they do that. They also make sure that the proofs that you produced or that they produced that they have are also kept up to date, right?  This is sort of a kind of encapsulation. I know people don't always love using libraries for different reasons, you know, gas off my shizzes and so on, but try to make sure that your code behaves more like it, like you know, all the things that are relevant to this little data structure op that did in the same place. How do you recommend testing basic blocks if they're like within a function? Like unit testing them? Like for invariance, if you wanted a certain variance for a basic block? I mean, it's just the same thing, right?  I would name this basic block, whatever basic block these contain, I would name that something, and then instead of checking every function, instead of going over every function and proving this, I would just prove it over the basic block, like here. So I know I can assume as we go into this block, when we are here, assume the invariant holds. After the basic block, which I know will be executed together, I can show that it holds. And then for every basic block, you just go, well, in this basic block, it's not modified, so it holds before, then it holds after. This, the basic blocks up here, if it gets modified before, if it doesn't get modified, so it still holds, right? So instead of showing that the invariants hold over each function, you do it over the basic block and you give them a name or something. And if for some reason this was down here, one of the updates were down here, then that's a good reason to move it up, so that they're in the same place. Because that will make your reason, it's a lot harder to reason about it if they're in the different basic blocks, because then you have to think about everything that happens between there, but if you co-locate them, then it's a lot easier. Okay, I do want to, you need, I mean, technically, you could say like you need it to hold from, if it holds in the beginning of the transaction, it holds at the end of the transaction, but... I mean, maybe the, sorry, maybe the invariant breaks between two blocks, but your invariant holds for the whole function, how do you recommend dealing with that? It's just much hairier proof to make. Like it's just like, if you really need to do, like consider if you really need to do that, if you really need to do it that way, then you do need to treat the entire thing as one block and reason about all the possible paths between. I'm a little short on time if I want to get through this, so we do have 10 minutes of questions at the end, right? So if there's something that... Just one quick question. If you have like, hello, if you have like an ID, for instance, that you generate, and you increase one by one, this ID will eventually overflow, and you cannot prove that it will never overflow, but it will require millions of transactions. So in practice, you should not, you can prove it, but it will be never reachable. So what is your view on this? You state your assumptions. You make the assumption that there will now be two to the power 256 transactions on the Ethereum blockchain, and you move on with your day. That's it. All right. It's like the counter in open sampling contracts can be unchecked on its increment, because it will never update, it will never overflow. If you know what I'm talking about, if you don't, then it doesn't matter. So I just need to move on. So if you're having a lot of trouble, look at the invariant that's giving you trouble, pick one function, look at all the relevant variables, and try to group them. You may have to create a few different paths, use helper functions, like this one's really good. They have the burn shares and the issue shares. I think that might have been on our recommendation. Like, well, these things will have to be updated together. Let's make sure they're updated in a single place, where all the relevant things to burning shares happen together. Don't do it all over the code, if you can avoid it. Remember, this is what you need to show. The invariant holds at construction time initialization, and if the invariant holds at the beginning of a basic block, it holds at the end of the basic block, prove that for all the blocks, then the invariant holds. Anyone who likes discrete math, this is an induction proof. We're security auditors. We have slightly different priorities sometimes from developers. So security is the most important thing. Simplicity is the second most important thing. It can depend. But the thing is simplicity is so tied into security that we really care about simplicity, and we'd rather have you skip a neat bit of functionality if it just makes things too complex and then save that for version two or something or an extension. Optimizations are the least important thing. I know that doesn't resonate with everyone, but if these things are so much more important to you than keeping things simple and making it easy to reason about security, what you can do, again, it's a lot of work, but then again, you should probably spend 10 times more time on securing your smart contract code than you spend on writing it, so it might be worth it. You can start with simple functions and prove that they're sort of like the de-optimization thing. Start with something simple, prove that it's correct, then start doing incremental optimizations and prove at every step that your proof still holds. And you end up with slightly more complex proof, but you'll end up with a proof nonetheless saying that your invariant still holds over your more optimized code. I do want to talk about invariance as test targets. We like to use Foundry. You can take your invariance and you can create a bunch of tests to just test those as properties.  And at the end it checks your property. That's pretty straightforward. A really cool thing you can do is if you could instrument your testing to just at the end of every test you're running, check your invariant. Make sure your invariant just always holds everywhere. It can be hairier. There's some things. I'm going to show you one trick to do it. It's not the most elegant way, but it's the most simplest that will get you going quickly. Here's a dead simple idea. If we take the contract we just had and we just wrap it. So we take all the functions that affect user accounts. So we keep track of all the users we have so we can do the sum of all the balances thing. And then whenever there's an interaction we make sure we add that user to the set. Then we do the regular update and at the end of every function we check our invariance. And we do this for all the relevant functions in the contract. And checking the invariance is just checking, well, the ones we have, this one's called A2. So checking A2 is just doing this thing. We're summing over all the balances and then we make sure that matches the total shares. So now you're checking your invariant in each and every interaction you're doing with your contract. Again, I mean, I'm sure a bunch of you are cool hackers and you could do this with, I forget the name of the Foundry app code, but you can update the EVM code of the contract in place to do this in a cooler way and in a more robust way, but this will get you going pretty quickly. So yeah, basically your job is to update ghost variables. The variables that you have in the storage you can always check. Your ghost variables you need to keep track of with a wrapper. This might also convince you that some of your ghost variables should be actual variables. Maybe it makes sense to keep track of a set of all your users in your code. I don't know. It's a trade-off you have to make. And finally, I just want to mention you can also use this for monitoring. I think someone mentioned it. There's two approaches to monitoring. Roughly one of them is just doing it on-chain. If you find some important variants that you can check on-chain, you can put them in requires and assert clause and then if for some reason at the end of a transaction they are violated, you bail, you stop the protocol. That's good because you can halt the contract before bad things happen. No one's going to be able to mess with your toll shares and steal a bunch of yield that way. It is pretty scary though because it can cause liveness bugs. You don't want your contract to end up in a state where it can never proceed and now all the funds are stuck. So talk to your auditor. It's like talking to your doctor. Like, we're here. Have them on speed dial. Ask like, I'm not sure about this but I have this little thing in my code and they might say that's fine or they might say, come right in. Drop everything you're doing and let's talk about this. And obviously gas costs. You have to put the gas cost on all the users. Or you can do off-chain monitoring. A poor man's monitor will get to that but you can deploy it later even if you already have a protocol up and running. You can still deploy. Some off-chain monitoring. He can't cause liveness bugs, obviously. What do you do if you detect a failure? Maybe it's already too late. Your variant got violated. Someone stole all your money. And it may not prevent hacks that happen in a single block. Someone uses flash bots and violates some invariance and now the damage is already done before your sentinels can come in and halt your protocol. A poor man's monitor is actually just using your foundry fussing test and running them constantly against on-chain state and pinging a dev if for some reason they get violated. After that, well, first I should mention what can you do next? Well, you can keep finding invariance. You can add more, document them, share them with your auditors, share them with your users.  If you make bold statements, they will take that as a challenge to go around and try to find violations of them. And the good thing is you can kind of keep doing this long after deployment, finding good invariance, making, they will improve your documentation and they will improve your monitoring. So security doesn't end when you deploy. Another thing I want to mention is we like symbolic execution. We like formal verification. So we're working pretty hard on making sure that if you write your invariance in foundry and you fuss over them, you can try as many million inputs as you want. We also have a tool that will let you run it symbolically. So try it on all inputs. There's a bunch of trade-offs. You should do fussing first because it's fast. You can write your tests using solidity. Same thing because we used to foundry tests anyway. You're limited to what you can express in solidity, whereas with our KBM foundry implementation, you can kind of use all of matching logic, not all of matching logic, but a lot of matching logic. It's a nice logic. Fussing is extremely fast. This symbolic execution is pretty slow. It's getting faster. My CTO is looking at me. I might have called it as orange, but it's turning more and more yellow. Doesn't require any human intervention. This often requires human intervention because a symbolic execution engine or a prover might not be able to complete. It might not be able to say, yes, I proved it or no, I found a counter example. It might say, ah, C3 can't handle this query, so you're going to have to help me out here. And that can require some expert human intervention. Symbolic inputs are 100% input coverage. You're testing every possible value. So if you prove your invariance with KBM and foundry, then they're proven. This was contentious yesterday. The idea of false process and false negatives. I think it's unfair to say that you have false negatives with fussing because, well, it's not like foundry comes in or a kidnapped comes in and says, like, oh, actually we didn't find anything, so therefore it's safe. But the problem is sometimes that's what developers or users think. That's why you can think of that as a false positive. You can't really have a false negative or a false positive with symbolic execution. Either we prove that this doesn't hold or we prove that it holds. Either your invariance is correct or it's not. Or you get stuck and you need a human. And then you need to do some things that are easy to try. Hard to master. Easy to try means that you can get in on our alpha release and do it.  And we're happy to help you along. Here's what it can look like. Forge tests will run the standard 256 tests for you. You can turn this up to as many million as you want. KBM foundry. This is an example from Roll's talk yesterday. KBM was able to prove that a specific invariant just held that was written initially as a foundry test. Again, go and look at his video if you want to check that out. I would be remiss if I didn't mention that we are starting a research branch at runtime verification. So if anyone's research minded or just curious, please go to research.runtimerification.com. We have a bunch of research challenges there. If anyone of them look interesting, just reach out to us. We'll see how we can help you along or if we're happy to hear your ideas on any of the research challenges. I think that's what I got. We do have 10 minutes for questions I was promised, so I've seen a few hands. Again, if someone wants to try this right now, pull up some of your code, try to find a few invariants. I'll just do a little train out of here and we'll find a table somewhere and sit down and work for as long as we have to. If you go home and you do this later, write me at Twitter or at runtime.runtimerification.com. You can always reach out to us at Discord. We're happy to help. This is past talk. The video should come soon, so check that out as well. It's important to what you'll be doing because eventually your invariant will contain a division and then all bets are off and you need to know what you're doing. Cool, yeah. Yeah, so the idea that you can do pen and paper proofs as a really robust method is new to me. I guess my question is it might be a bit vague, but how do you think of the risk of, let's say, I take that seriously and I write my proof, I convince my team member, how do you think about the risk that we've still missed something? Is it common in your experience if a client takes it seriously that they kind of mess that process up? The good thing is that if they do, if you write invariants and like, hey, we have a proof, we will also check the proof. Like, I mean, we're part of the audit. Yeah, we're the ACM journal you're submitting to. We'll make sure that you're reasoning a sound because like, oh, this is a good invariant. We trust you guys, but let's double check, right? As for pen and paper versus, so this is still formal verification. Someone said like, oh, it's not formal verification because it's pen and paper. No, it is formal verification. It's not mechanized formal verification. You wouldn't take a math paper and say, oh, it's not a formal proof because it's in English. Like, it's still formal proof. It's about how you reason and how good you are at formal reasoning. It's about how many nines you need, right?  The world is chaotic, but if you start with your pen and paper proofs, they'll get you very long way. And in the end, like a few of these things might be like, like the invariant I showed you, I wouldn't even necessarily want to mechanize that because like, ah, there's more interesting things to mechanize, but here's the pen and paper proof that's fairly convincing and we'll make a little note somewhere that if anything happens that updates any of these variables, we need to double check it, right? It's sort of like an index for you to work with. I sort of grabbed the mic. Whoever has the mic, just go. Okay, so obviously like part of the limitations of defining invariants would be like, if it's a house and the invariant is no thief can go through the front door or come out if he somehow got in. Let's say that's the invariant, right? So obviously the limitation would be that, you know, we sort of like didn't define that, oh, there's also a window, you know, or there were roof tiles or there was something to that effect. Now, obviously you didn't make the statement that it's like an absolute thing, but how do we work towards like that kind of like comprehensive or exhaustive type of invariant definition? Well, so I mean, to work with your analogy, what you do is something like, instead of saying the thief can't go through the front door, you just like, what do you care about? The thief can't get in the house. And then you have to say, what are all the ways to get in the house? You know, what can happen? Is there a hole in the walls and where is there a window? Can you get in from the roof? It's sort of the same thing here is like, one thing we do a lot is like, a really good start nodded with is, where are all the places where any token transfers happen? Those are a great place to work backwards from. Because you know, and then there's always in line assembly, but let's let's forget that for now. But just look at all the places where tokens or ether changes hands. And then look, then you can start looking like, well, if we cover all the paths that can reach those locations, and those are all safe, then we're safe. And then, you know, of course, like, you know, what, what if the token can do weird things if it's like in block use or something, something you need to keep in mind? But yeah, that's sort of the approach, right? Like find like, well, take the floor of the house says the thing that this thief can never reach and then like exhaustively enumerate all the way someone can reach the floor of your house, I guess. Yeah, yeah. So I mean, like a lot of these things, like, well, you know, the devs can upgrade the contract and take all your money. Like that's, that's an assumption. Sorry, like, but barring that, we're doing reasoning. Who has the mic? I have a mic. So in the example you showed where you talked about basic blocks, my reaction was like, and, and reasoning about invariants before and after, they're not as it's written, they're not necessarily accessible to us to, to like, it's not maybe we instrument it. But yeah, I can't really get in there easily with the tools I have in my hand by hand, like forage and say, okay, this is an invariant that holds over this if statement or like the block in there. So, so I'm curious, like, you know, if there is a way I'm missing. And then this, this also maybe part two is like, does verifiable code look different than like readable code and testable code? Because if I'm to, I imagine pulling this out into a lot of helper functions, that's not my preference in this case. So I'd like to hear your thoughts on that.  So we can't, can't really unit test it with foundry. So, which is also a good reason to do this kind of reasoning, because like instead of having to go through all your code with a tool, you can just go and say like, well, I know solidity well enough to say that, well, the only way this storage slot can be modified is either in line assembly or somewhere where this is exactly named in this way, in this specific contract. I don't think anyone's made a solidity. No, there's no, yeah, there's no other way to round it right now. So, I mean, that's why this reasoning is pretty good. Like you can actually, especially right now with the state of solidity, you can track, tackle these things on pen and paper quite easily that you can't really do. With foundry, as for the readable over, I'd say that, I say they all come together pretty well in the sense that you don't have to have small helper functions all over, but like, again, the data structure example, right? Like if you think of your Java hash map as a single entity, make sure that like, it might be a good idea to have like, you know, the updates or deletions from that just be co-located and it might as well probably be a function, right? So, and it's not about going crazy. I wouldn't say like, break these out to in a helper function. Like we have burns when we have the issues, like that's fine, it's only two places.  But verifiable code, I'd say, now it just really relies on this, that you have all the relevant changes to things that have a clear relationship are co-located, whether that's in functions or anywhere else.  I'd say that the enemy of this is maintainable code. That's why it's like, the good thing here is like, well, things, we don't maintain that much code here, like we deploy it and then it's deployed. So you don't have to worry that much about like, well, what if we change the code and then we forget to update the code comments because like we're kind of relying on the idea that things get frozen here. That's one reason that formal methods doesn't, haven't really had a breakthrough in you know, Web 2 or standard back-end development because like, well, everything has to be maintainable. If you keep, if you have to redo your proofs all the time then, you know, it might not be worth it. So the fact that code is frozen is actually pretty important here. Does that answer it? Okay. I actually have a follow on question to that right here in the back. Hi, yeah. You said that you should be doing these proofs only during the, or when the code is frozen because you can, you don't want to be redoing your changes over and over, right? Which is right. You don't want to have to be redoing this work. But it's, you have something to mechanize the invariant checking. You can do it, you know, not only with changes but you can also get valuable feedback during the development cycle, right? So, and that has other benefits too that you sort of alluded to in your symbolic execution is that you don't have to rely on the fact that you have to manually look at all the places where storage is updated. You don't have to worry about the fact that you made a delegate call into a library and oops, actually that library had an inline assembly block that's a secretly changing that, that all gets sort of handled for you automatically during mechanized proving. So I just, I guess I quibble with what you have said there that you should only be doing your invariant proofs. You should probably be doing it much more frequently. Yeah, I mean, I'm more talking from experience. Like it's, I would say like start writing invariants. As soon as you hit your docs, like, you know, you're doing, do your design, start writing invariants, keep them up to date in code. Realistically, that doesn't happen as much as I'd like. If you want to be a unicorn and do that, I love you. But like, I know most people here won't do it. That's sort of what I was getting at.  It's also like from experience, sometimes the signs change enough during the process that maybe teams don't want to invest all that time in because these instrumented tests can take a while to do as well. If you want to have some examples, go to that alchemics v2 foundry repo. It's called that because we're working on setting up foundry tests sort of like this, but like even, even more powerful and extensive.  But all the invariants came from an audit where we found them and wrote like formal English proofs of them. Lucas over there actually did that.  If you just want more examples of this, this entire section, we would just go over like 10 different invariants and give fairly formal proofs or handwaves about why each of them holds. So it's a great place to go and see more examples. There's also links if you go again to the beginning in the lecture notes or slightly more extensive. There should be links in there. Kind of a follow up on that. It strikes me that some of this could be related to behavior driven development. I don't know if, I haven't really seen this in the Solidity Web 3 world, but think of like a TDD loop but then zoom out. So instead of writing a failing unit test, red, green refactor loop, you're doing a red, green refactor loop at like app or protocol functionality level. So instead of like the standard arrange, act, assert way that we might set up a unit test in behavior driven development, they call it given when then. So given some background when some action gets taken, then I expect these assertions at the end. And I think it could fit well with like threat modeling like actors, assets, actions. I was just curious if you've seen that because when we're doing BDD and I'm trying it out on a Solidity project, you get to keep those green. And so I wonder if there's a way to kind of drive some of your development with invariance that you use in the BDD world, use cucumber, which is like runnable English language. So I thought that might be a pattern. I didn't know if you've seen that. But I want to talk to you. That sounds great. I want to check that out. Cool. Hello. I just wanted to make one clarification that the inductive proof at the function level is what you need to perform to get the invariant to hold. But the basic block level is easier. That's why it's presented as an alternative. So if you can show it at the basic block level, then it holds at the function level, not necessarily the other way around. So if you can't show it at the basic block level, try it at the function level still might hold. Does it work with Viper? The KVM? I guess it's language-agnostic. KVM doesn't actually work over Viper. So the thing is like, well, the thing we're developing now works over Foundry and Foundry works over Solidity.  Because it's all EVM at the bottom anyway. So I'm sure someone's going to hack together a Viper extension of Foundry eventually. Just curious if you had any examples of mechanized invariant tests that you like to look to or that I could look over. Just I still haven't wrapped my head around the mental framework for parsing out what invariants should look like. Yeah, maybe a mix of English pen and paper invariants and code might be helpful. Yeah, I'd say check out the Alchemyx paper for a good run-through of... So there's a section in the beginning that lists some variants and there's a section in the end that proves the invariants. And in between are just all the findings reports. With mechanized proofs, I don't...  Come talk to us. It depends on your background and where you want to start. We have just a bunch of different resources, depending on what you're interested in your starting level. There's the maker die, multi-collateral die proofs. If you want like, well, here's a full formal treatment which has some English language stuff, but it's also like, you know, fully formally specified at the function level, all of it. And that's all verified. That's a good example, but, you know, hang around. We'll clear you up. Oh, yeah, yeah, anyone in a...  Anyone in a runtime verification t-shirt? Is there no workshop after this? Oh, okay, okay, cool. So yeah, we can't hang around here. No, okay, fair enough. Okay, thanks everyone.


Maybe let's turn to the room, to the audience, would there be questions, comments, Philippe, you would like, Mrs. Guarn? Yeah, may I say I'm a bit surprised, because in listening to you, I had the impression that the food problem was just a technological one, and with some money invested in the private sector there wouldn't be any more food problem. You didn't speak about one individual called the farmer, neither perhaps a bit, our friend from Nigeria, did you speak about public policies? May I remind you that in the 30s, Europe was a net food importer, that in the 50s the PL480 was created in the United States to send food aid, especially grains, to India. That very India, which is now threatening the food markets with embargo because they are exporter of rice, of sugar, of wheat. Where are the successes of Europe, of India? Perhaps technology is yes, but at first it was public policies, the common agricultural policy in Europe, and what is not enough studied, the Indian agricultural policy with a guarantee of renovative prices for farmers. Don't you think this is this thing which is important, that's true that Africa is dependent, is importing Nigeria, you're the world's biggest with Egypt. In fact, Nigeria in Egypt, you're the world's biggest wheat importer. In the 50s, Nigeria was a net food exporter, you were the biggest exporter of palm oil, if I remember. So don't you think that the first problem is a problem of public policy, of agricultural policies, and unfortunately in some of your countries, farmers don't vote or their political power is fairly limited. Well understood. The rebellion of public policy, let me ask before you. Maybe I'm going to ask Mrs. Korn also to intervene because we don't have much time left and then all of you will get a chance to include Mrs. Korn. Certainly I feel, thank you very much, first of all, thank you very much for sharing with us your very extraordinary activities and after Mr. Shalman's question, I feel suddenly, you know, my question is not very, very important, but I personally, I'm convinced that the technology is really one of the very important solution to the problem of our food insecurity issue, and especially just for that, I have a small question to Mr. Bach and I'm a personally very, very fascinated by this smart farm technology. But, you know, as one of the person who like very much to eat very good food, my concern is, you know, all products from a smart farm, do you think they can contain the same nutritional quality or taste? Okay, so again, you know, I think there's a third question. Unfortunately, very quickly, please, madam. It's very short. Yes, I was just surprised to hear that genetically modified GMOs, what it's all, the GMOs are sort of normalized now because they appear to be safe. What is that? Is there something official about that now? And that there's normally the World Organization, Mr. is here, maybe he would confirm has not really approved that. So can you give clarity on that issue? Thank you. Okay, fine. Thank you very much. So GMOs, maybe two minutes each so that we stick into our time frame. Mr. Bach, if you wish to start. I think the method we use in indoor vertical farm or controlled, you know, environment agriculture is different from like GMO. So we don't do any, you know, the fabrication to the crops. The only thing we do is we basically use water and nutrient and we don't use soil. Soil is actually something it can hold the crops, but we use some other methodology to hold the crops and then basically feeding nutrient. So when I say, you know, the theoretically modifying the taste or the ingredients, it's mainly done by controlling climate. So for example, the Korean strawberry is very sweet. If you try Korean strawberry, the sweetness is more twice more than the strawberry in US. They are typically grown in, you know, the traditional, the greenhouse. The reason Korean strawberry is sweet is not because it's modified. It's because of the temperature difference between the during the daytime and during the nighttime. So that's the techniques we are using it. When I say controlling the climate, so if you want to make strawberry sweeter, then, you know, you can control the difference in the temperature. Some of the. Thank you, Mr. Farber. Fortunately, everybody has to get a chance. So very quickly, 30 seconds. Two seconds. Like some of the crops with the high, the functional ingredients is also done by, you know, changing the light and then changing the temperature. You know, we don't do any modification and normally the crops we produce has the same nutrient as the crops produced in the traditional farming. Thank you very much, Mr. Park. Mr. Houdi, one last question. The question from Madame Biloa. I think that again, science has helped to demystify a lot of things and there is genetically modified food and there is today the improvement, for example, in seedling or in the makeup of foods that creates better yield, for example. I'll give you an instance. I own an agriculture business and we supply the supermarket chains in Nigeria. And today with science, with, you know, better seedling, you're able to produce in a 200,000-meters greenhouse controlled environment agriculture situation more food to supply the supermarket chains than we were able to do in 200 hectares of, you know, open-air farmland today. What is important in all of this is the safety and health and how to prove the safety of the seedlings that we use to produce food today. And I think that the issue of GMO is still one of these issues that are out there. I don't know what the official policy on them is, but certainly science has helped to prove that some of the practices that were yesterday seen as taboo are actually safe today. With regards to the question over there, yes, it starts with policy. And this is very ironical, especially for us coming from Africa. Many, many years ago, Nigeria gave the first palm seedling or palm trees to Malaysia. And today the reverse is the case where palm oil is imported from Malaysia into Nigeria. Very sad situation, but yes, it starts from public policy, from governments realizing that there is a big impact in not doing anything, and there is a big impact in doing something. And coupled to that is that private sector starts to see the economic benefit of making sure that there is resilience around supply chains. Today you have a lot of the meals, the flour meals, for example, in Africa, starting to see that you have all of these machinery and production lines, but you need supply chain contribution from places like Ukraine, for example, to get wheat, you know, to make sure that the factories are running. The more these people start, the more private sector starts to realize the impact of this, then maybe the hands of governments are forced with regards to public policy. But spot on, it's the truth. This is a very important area you raised. At Kanashogil, we work with 6,000 farmers. We reach about 20,000 farmers within three more years. You are right. The farmers do all the work and they get maybe 10 cents on the dollar from anything that's done. If there is food waste due to supply chain, the farmer is the he or she, and mostly it's she, the farmers. People think of farmers as the only men, mostly they are women. They are the ones who suffer. When it comes to public policy, people in agriculture, people forget the Treaty of Rome before the EU was probably in the beginning purely an agriculture project. The farmers are suffering all over the world. One of the issues is the lack of development in the public policy format and the legislation format. They don't have access to legal papers for their land, so they cannot get financing for the land because generally the land is given or inherited or is owned by several people. So they have to go to the industry, the other part of private sector who will charge them so much for ensuring funding and then the same thing on access to technology and access to seeds and what have you.  The farmer is now an educated person and sooner or later, if he or she will not vote with their electrical vote, they will vote with in different ways and it could become a ticking bomb. So I appreciated the question. We didn't address it in our presentation because that wasn't part of our brief on discussion, but we would need a quick update of public policy, of environmental, of the legislator changes that will cater to the traditional farmer. What we do is mechanize farming, which is different, but we will not be successful without working with the traditional farmers. Thank you very much, Mr. Camel. Yes, yes, yes, I'm not forgetting you because I'm sure that as a FAO official and senior official, you would be very happy to address the issue of public policy. Oh, sure. Thank you so much. I refer to many policies, for example, the Repurpose and Agenda is linked to policies linked to the information of the two cost accounting, which will be modified significantly the way we align policies. But also when we talk about innovation and science, which is central, it's one of the elements that we need to accelerate together with data, but also with institutions. And a good policy of innovation and science require policies behind to set them up requires institutions in place. If not, it would be very complex. So for sure, everything that we have been talking about is linked to the design and policies, but we need to be careful not to bring historic policies that will have worked in the past, but not necessarily will work today. We are in a different environment and we need to be very careful not to create new distortion. Second, I think it's important to correct some issues. Biofertification cannot happen, does not increase nutrition capacity. The only way you can increase nutrition capacity of a crop is through biotechnology, which is not biofortification. And the other element which was wrong, GMOs are not accepted and generalized, of course not. GMOs are managed and decided by each country. And there is a lot of scientific evidence behind them, especially more than GMOs on gene editing today. But this is country by country decision and the institutions and regulations have to be in place in each of the countries. So we need to be careful with that. And even in Europe, of course, GMOs are not there and there is still discussions on gene editing. So again, there is a lot of evidence already in place that we need to bring to inform people, but we need to assess all the different elements. And finally, on the on the control environment, horizontal and vertical. So you can have control environments horizontally and vertically. Horizontal have been cost effective. UAE is an extreme example because it's very costly to produce food in UAE, but they are profitable in China, Vietnam, Singapore and very profitable. Vertical farming is also starting to be profitable in terms of control environments. There are very good examples in China and Singapore and other regions of the world. So again, it's a way to satisfy food for the urban areas because you get closer to them in terms of production of vegetables and high value commodities. And that is not GMOs that is not biotechnology is basically is a high level precision agriculture to manage properly micro nutrients to the to the plants and water provision. And of course, the heat that is needed. So again, it's a technological innovation when you are in the high end of high value commodities, which is starting to be evolving rapidly and to make give access to urban especially for households. Thank you. Thank you, Mr. Cullen. We are now for this very interesting comments. We are now at the end of the session. I just would like to add as personally that I've spent now at least three decades of my professional life, supporting governments or establishing public agricultural policies in developing countries in Asia, in Africa, etc. And it's building on Philip's comment. It's of course a sobering situation to see that in many developing countries, not all, of course, but in many developing countries, agriculture has a much lower share of budget, investment and policy attention than it should if we wanted to address all the issues that we have here. So that's the reason for which I'm particularly grateful to the WPC, Thierry, Mrs. Kwan for insisting on having this discussion on agriculture, because it's not all, it's not only about discussing the substance, but also just per se, because there's discussion around it. And whatever we say that it shows the importance that it has in the global agenda and importance, which is really underestimated by many policy players. So thank you very much for allowing us to have this type of discussion continuing. Maybe if there is another discussion next year, trying to deepen even more some of these policy dimensions at the global level, but also at the national level and trying to dig into this agenda. Now, I think that all of you will have recognized that we had a fantastic group to address those issues on the screen and in the room and that they have enlightened us with their vision on policies, private investments and initiatives, science that opening new doors into our vision. So please upload them and thank them.


Welcome to the Knuckleheads of Liberty. There are weaponizing the arrests. Here is a case of a Missioner, a Michigan guy, his name is Ryan Kelly, and he is running for, as a Republican for governor in Michigan, trying to unseat Whitmer. And they arrested him just recently. They arrested him last week. And part of the reason they arrested him was because they said, they didn't claim he went into the Capitol, but they claimed he was on the Capitol grounds during that time, so therefore just round the ball up. You know, this is insanity, right? You know, just sort of going, you know, you don't want to talk about interfering with elections. This is pretty creepy stuff. You guys have any thoughts on this whole Ryan Kelly thing? Well, I want to know, are we still in America? Okay, are we still a constitutional republic? Nobody's claiming none of the FBI's documents that they filed on this case said this guy entered the Capitol. He was outside, he might have been on the ground somewhere, close to the steps or wherever it was. Nobody's claiming he entered the Capitol, but he had the arrest in this guy, this particular guy. Why? Okay, he's not denying that he was in the rally. He's not denying that, but he had the arrest of them. What's going on here? Are we still in a constitutional republic here? No. Where are we in China or North Korea? Where are we now? We're not. We're in a totalitarian, increasingly totalitarian regime, top-down, centrally planned. That's what they want, and that's what they're getting, this, you know, back to the old original way of running things, where you had one guy or a conglomeration of selected, elected, or however you want to call it, people that run everything, and their political opponents are going to be arrested, and they're going to be, you know, trumped up charges, and all this kind of stuff. Yeah, that's the, you're thinking of the old America, Leon, that's dead now. It's gone. After COVID, it's totally gone. Sorry, I'm just cynical. I know what the way it is. There's a side issue here. I don't know what's going on here. The side issue here that is not being investigated, I don't have answers, but there's also another side issue, which is the role of the FBI in those rats. There was a guy by the name of Ray Epps, who we have on video, I think it might have been even to the day before the actual ride. It might have been on January 5th. On video, encouraging people, we have to go into the capital. We have to go into the capital. That's what he was saying. He's on video saying this. Somebody, I don't know who took the video, but it's on video. It was showed on Fox News. And nobody's investigating this guy deeply. It is claimed, and I don't know if this part is true, that this guy was an FBI informant or is an FBI informant. If he is or was, was he working for the FBI that day? We don't know. But he is on video encouraging people to breach the capital. There he is. And he have not been arrested. Notice he have not been arrested. Okay. He's on video making claim, telling people to breach the capital. This other guy from Michigan, he was just on the capital grounds. The guy and Ray Kelly or Kelly, whatever Kelly's name was, he was arrested for being on the capital grounds. We have somebody actually encouraging people to breach the capital and he have not been arrested. Doesn't that look a little suspicious? And what kind of cements this as well as this whole Whitmer thing that happened, we talked about this on the show earlier, where there was a plot to kidnap Whitmer. But it turned out there were more FBI agents involved in the plot than there was actually conspirators. So, you know, it's kind of crazy. So, I mean, when we start to talk about some of this issue with, hey, you know, this is kind of weird that you can see people on video encouraging this and they're out being charged. What's going on here? Life, liberty and the pursuit of haptiness always and forever.


Big shit, big shit, big shit Name another podcast like this Who gonna bring it to the table, boss talk I, I'm gonna be honest with you I, I was the one that Me and, I'm a Yellow Beesie fan Big time That's my boy I know, I know y'all rock together Y'all, you, him, Half-Paint But I asked a question to Pusha Man last time I'm like, why when Yellow went Like he did, cause I know you You did some work with him I was like, why did him and Half-Paint Not link back up in all this time And that was one of my questions to Pusha Man Pusha Man like, you on something I don't know We talk about how to look All I'm saying is No matter what kind of camera he got No matter what he doing When y'all are family like that But I know business overseas and everything But some things ain't about business for me I'm being real Some things is more about You my dude And I don't care and I'm about the money Hey, but remember what I told you Remember what I told you last segment When you on that level You gotta get a look It's a certain look you gotta go for I know it I know it And you can't draw back I heard you say that in the other interview too Like you use different people sometimes as well So I heard that You have to You can't draw back You know what I mean At that time I personally know What was going on with that situation Oh I know you, cause y'all like this Three, all three It was more so just to look That he needed at the time Like they was trying to go You know the cameras playing got You know they covered the ground here And it's a big ground here But when you looking at that industry man Them folks walking around with reds Reds, yeah They walking around with every lens All that like so man That's true And that's what at the time frame Yella going on a double platinum red He can't put nothing out that look mediocre Yeah, but at the same time I know y'all so tight I'm like y'all could have made it happen I know a question you want to ask It most definitely Y'all could have made it happen It most definitely Y'all could have made it happen But that, I can't explain that You can't speak on that Cause that ain't your thing You see what I'm saying I get it But that's why I'm a fan So I'm on the outside looking in And I'm just I'm coming from a fan perspective My shit go crazy Too crazy right now We buying every camera That's what I'm talking about That's what he was going to say He wanted to figure out why Yella ain't buy the cameras for y'all That's what I'm talking about See I can't answer that I know I understand you can answer But those are some questions that come up on here Like what I'm on the outside looking in Y'all just looking Yeah for sure I'm like what the hell He's gonna go Cause every time that First phase with Trapping design Just a half paint film Boom Every time So that's the foundation That was the build up Exactly He should have bought the cameras Just out of love That's what I'm talking about Even if y'all didn't shoot the video He should have bought the cameras just out of love I don't tell I don't wait I don't wait I don't tell Boss talk one on one They feel like you should have bought Paint the goddamn camera yellow No no but see So how does have Have paint man You know him better, he's like your best friend. I gotta talk to this guy, how is this guy, man? What you mean, how is he? Is he a good dude or what? He seemed like a good dude. That's my little brother, bro.   Like, you know, you know he don't do right by him. And Mike Fresh, I met them around the same time they were young niggas. I think I was like 18, 19 when I met them. Yeah. They were 16, 15. So you came up, y'all know each other for real, for real. No. Yeah, yeah, yeah. Mama was all that. Hey man, you got the right niggas around here. They genuine. They so genuine.  Like Papa Run, like DJ, the whole time. That ain't nothing but God put that together because that don't make, that's not logical that y'all would be together like that growing.   Everybody now, if it's an artist, they've been brought in by like one of, you know, the bigger dogs, but as far as like all of the main folks, been us in 2008. Wow, that's been us a love, bro. So we all done grown, fought each other, all that. Like it ain't nothing but love or real. Were y'all a top off or no? No, yellow wasn't never top off, but yellow been around, yeah.  Yeah, yeah. Oh no, you and him been rocking for a long time. Erica was top off for show. Yeah, yeah. So when something like that happened and one of y'all break, y'all pretty much got the olive branch to go on and do. You for sure, you a boss. Okay. This boss already, hey, that's what we build over there. We want to build bosses, bro. Cause I'm gonna be honest with people when they see that from the outside, looking in here, I go again. You thinking how could this artist be on this and then do this and then don't forget about the path that they came through. Man, what I learned. But you said something earlier that was heavy. What I learned was to be attached to somebody else's legacy too. Like outside of your own, you want to be a part of somebody else's legacy. Like that's what make your name so much more concrete in the ground. You see what I'm saying? Like I heard you tell my yellow trapezoid like I recorded that.  Name another podcast like this. Who gonna bring it to the table? Boss talk, who your girlfriend fare? Boss talk, we gonna do it how you want it. Boss talk, yeah, everybody on it. Boss talk, it's a unique hustle.