New Ethereum talks, every Monday. The week's conference uploads by event, in your inbox.

Loading player…

Stablecoins with MakerDAO | EthereumMadrid went to Berlin @Private Key Meetup

Ethereum MadridTue, Oct 9, 2018, 12:00 AM

This time we travelled to Berlin where we were invited by the Private Key Meetup to present our introduction to cryptoeconomics and the stablecoin project from MakerDAO. Part One (0'52) https://goo.gl/XfV8Qg Cryptoeconomics is the fundamental layer of all blockchains and blockchain projects. It is about using economic incentives to design mechanisms that encourage people to participate in the network by behaving in a certain way, the economic way. Sandra from Ethereum Madrid will introduce the fundamentals of cryptoeconomics. Part Two (14'14) https://goo.gl/oLYzMv Using Ether or Bitcoin to operate a company or to buy products has one great disadvantage: the volatility of the currency. As it is impossible to know the price of Bitcoin or Ether for the next few days or months, it is risky to use them as a mean of exchange. A stablecoin, which price would fluctuate as much as the major fiat currencies in circulation but without the volatility of the cryptocurrencies of today, would allow the ecosystem of blockchain-based organizations to pay wages and bills, borrow or raise capital in a more predictable and reliable way. How are stablecoins issued, how do they acquire value, and how are they stabilised? How are decisions made to correct deviations and how to deal with crisis? What are the economic incentives that allow decisions to be made in favor of stability and personal profit at the same time? All of this in a decentralised fashion, while at the same time making decision-makers responsible? Laurent and Sandra from EthereumMadrid will explain the stablecoin technology developed by Maker as an illustration of the concepts of cryptoeconomics. Part Three (56'43) https://goo.gl/9MF8Ey Denis, from the Maker team, will introduce how Maker is using formal verification in their smart contracts in order to mathematically verify and prove what can and cannot be done. Visit us at: http://ethereummadrid.com Join our cyptoeconomics meetup in Madrid: http://meetu.ps/c/39bt1/twKSG/f

Transcript

so hello everyone please stop talking because we're gonna have some presentation now so basically today we have a thanks to Aaron and private key meetup we're going to have a discussion and short presentations about crypt economics about stable coins then we're going to tell you about trip key that uses some elements of make Adel that and that's why we put it together so there's a business case there's theory and so on so I give a stage to Sandra we're going to talk about crypt economics and then we're gonna have maybe a little break and a discussion and then move into next short presentations that's it okay I present also shortly Laura and me we actually traveled from Madrid to Volyn to do this meetup here so we are really interesting for you and we know that you normally do more like something like a chat so feel free to ask whatever you want to ask and we keep it as short as we can because they also told us make short presentations really short presentations so I would start to speak about crypt economics well I don't know if you heard about this this topic I am quite sure I mean in Berlin everything is really advanced in this world isn't it so crypto economics is something like it's a mixture of cryptography and game theory that's why it's called economics and it's it's something similar to mechanism design so it's it's actually a concept to solve certain problems so if you if you know proof of work for example is an example of crypto economics because it used cryptography to show what has happened and it use incentives to actually manipulate sounds bad but actually to move human behavior in a certain direction okay and but this topic is so big that I will just make a really short presentation about 1% specific model and also how you can attack this model in a game Siri way so first of all in the middle of for at the heart of all blockchains public ones when you speak about public horns I guess it's the consensus algorithm and the thing is how can we actually achieve consensus but in a decentralized way and without having conversations really between us so therefore I want to make a quick game with you imagine you I know Casa yeah you and someone else you don't know this person and you actually have no possibility to speak with this person but you get a possibility to become free but only if you answer to a task with the same response as the other person will do and the task is to find a number in this line of numbers which is six digit long and it has to be the same number than the other person will choose so which number would you choose you have this numbers here and if if you choose the same one then the other person will choose exactly and and why this any idea already by this because you're lazy yeah because this is actually it's a concept like when you get rewarded to find the same answer someone else you look for characteristic which are special so you look for something because this is game theory no you think what will the other two so the other will also look for something special and therefore you choose this one and this is actually concept which was found out by too much shelling which certainly died last year because we need him now we need came Syria economists in this world right now and and he did this experiment in New York he said to people okay you don't have the possibility to communicate but if you meet at the same place at the same hour you will get a reward and where do they meet yeah that's a little bit a culture you know sensuous yeah maybe today it's fair works you know but this we also apply to to our crypto world to solve problems so in the proof of work so for example you as a miner even though it's a protocol but you are you have to choose which block III take no imagine you want to you want to be on the blockchain and you know that if you take the block everyone else is chosen you get actually the reward because you're on the main chain so you can actually enter directly the next competition to find the next block if your honor if you choose a block no one else will choose then you're on the wrong chain so you lose time because then you will find out later and then you have to jump so therefore you you look also actually something for what do the others to and when you get a block promoted you think everyone else will validate this block and therefore I will also validate this block because this will be then the main chain and I go to the next step yeah so therefore we have this incentive to find the block which everyone else will will choose because your reward is you on the main chain but this concept we use even more to do to solve problems with on chain applications like DF so whatever actually any smart contract who needs to know the truth of the off chain world this happens actually quite a lot now that behind the blockchain while we write smart contract but we need information for so for example about the weather or we need information about the price of the certain things and how can we get these choose of course we use Oracle's at the moment most of them they use centralized Oracle's what is web page Central's expects what's the problem with centralized or girls the problem we all know and we hate yeah exactly it's a central point of failure a central point of contra so what we need is decentralized Oracle's and therefore we can use the wisdom of the crowd which is actually using the intelligence of all the people together yeah I could now ask you is it rainy or is the not and you can give me the to the answer and I can make the average so this is what what this may be the truth and they say already the problem how can I now find out if it's the truth or not because people can lie and this is where the challenge come concept actually comes into place because I make new examples in new example imagine the question of a smart contract or the the need to know who wants the election so I ask this but there's a new condition you can now say Hillary or Trump and you know the truth is Trump but if you say I need to know the truth know so I can't ask you tell me the truth because I can't find out if you tell the truth or not but I can say to you if you say what everyone else says you get a reward and what will you say then so imagine I ask you Hillary or Trump and you get all free ice cream if you say what everyone else is saying well then you have to have the condition that actually the people knows the truth if they don't know the truth it's that's actually prediction market that's another thing but because you think what would everyone else says you say the truth because it's so much easier to agree on truth then on lie actually we also use this in in forensic when people do interviews they ask all this question because they know criminals the categories so easy on lies but on to Sudan it's easy to agree so the problem of this is of course this concept can be attacked him by the bribing attack model so how does this work now imagine the same game but new rules what are the rules now again I ask you who won the election Hillary or Trump and it's the same rule as before so if you say what the majority says you get a free ice cream but now I say I'm an attacker okay and so now I say if you say hello but all the others say Trump you get to ice cream so now what would you say then think about it if you say what everyone else says you get one ice cream but if you say Hillary Hillary and everyone else says Trump you beat two ice creams oh yeah I can even say you get also an ice cream exactly because now okay okay well anyway here because now you can't win in any case if you say Hillary because if you say Hillary and everyone else a celery I will pay you if you say Hillary and everyone else as Hillary you get the reward because you did what the majority does and this is the thing well actually I want to explain it first and how they could use it in proof of work they could attack the the proof of work consciousness a consensus algorithm by this because what I now can do is I put a bribe on the block I want to be included in the blockchain so now I do the same game now I say if you choose this block but everyone else is choosing a different block you get a reward but the thing is in the end because everyone is thinking like you do everyone will take this block so in the end we will be here and therefore I'm as a tracker I don't have to pay anyone because I just used game theory to reach a moment where I manipulate your behavior and in the end I don't have to pay and this is what is the cost versus versus budget model so if I do an attack the cost is actually what will I have to pay if my attack is not working and this can happen because some people actually you know they like to tell the truth so they are not easy to manipulate and this attack can also have communication problems so imagine they don't know about the bite and then I'm actually a little bit up no because then I have to pay sun-lee to all the people that set my my block but it wasn't the majority so then I have to pay these are the cost but the budget is zero because as I said if my attack is working you all say it so you actually get the normal we want and yeah this was just a really quick way of how crypto economics is supplied to to check on consensus algorithms and now law will continue come presenting the maker stable current project and then we see also some crypto economics applied and then yeah and you do some more technical [Applause] so we started and in 2016 we started with the Dow hack Meetup that was the first and we do meetups with it but we don't do only meetups we also focus a lot on education so we started I guess like all used I with passion with just wow this will change the world and now it's getting actually it's about creating a community and inform people that they don't only hear the word but actually get some real input and understand the whole dynamics about it so we do events we do courses we call operate we don't do I see oh so this is not so we are not promoted by anything we just do it by ourselves yeah come to my bit just to add about on what summer just said maker is one of them but other events that we we did in the past were about building blocks or what we like to consider building blocks of the ecosystem of blockchain and so by first doing something around the DAO hockey at the time we then move on to prediction markets you port with a identity bridge market was with the kurtosis and and makeup and all those topics stable corn prediction market identity for elements that we we all whatever the projects we all going to use them at some point in in those in those in those projects so maker is to me was the the worst the most difficult one I've ever looked at and I'm really grateful to have Dennis here with us tonight who is working with the maker team on something very specific that he will touch upon later in the presentation what we're going to do is online i is give us give you an overview of the projects and how it's heights work hard works but please know that we might make mistakes i won't we won't get around it and you can and you are encouraged to go deeper into the mechanics of the projects to grasp the the whole the whole thing right and we will put some references afterwards okay so the the ID is is really to to make a stable coin so why do we want a stable corn in the first place we can summarize the the problem with those two statements so cryptocurrencies are too volatile if and I insist if what you want is to use them in every day's activities like paying bills like you know set up a business plan for your company to pay your employees and so on if the variety if you use a normal typical two currency the volatility is it's like making two times a bet on this on this financial product and the other reason and this is why stable corn and this is for stable corn party in particular is that in today's economy people that are making decisions on how to for instance change the economic incentives or you know the interests on on the Euro or daughter or whatever they don't have skin in the game so whatever the decision they take if it's bad or wrong it doesn't matter they all get paid at the end of the day we're in maker are we going to see people taking decisions have skin in the game they are financially responsible of the decision they they take so briefly what are the properties that would like for our stable coin well we want a low volatility as low as possible but we still want some fluctuations around a stable point of reference so it's still a free-floating currency it will be allowed to vary through time we'll see that there is a an instrument that we use as a as a reference point of stability no central authority in the way decisions are taken so this is fully decentralized some automated actions to prevent some individual actors to do whatever they feel like doing and for the system to react to bad situations and we won't as I've said responsibility for the decision makers and a flexible governance so we still want people to be able to take decisions and to change some parameters in the system according to what's happening in in reality what do we need to do this basically economic incentives and this is why Sun Hat wasn't presented earlier something about crypto economics because this is how you design economic incentives in blockchain projects and all you also need a sounded business logic so it needs to be attractive to investors to user to actually use a stable coin to other people to take those decisions and have stake in the into your system to profit from it and so on so a sound business logic and economic incentives designed or weight stability what does it mean so stability in the maker ecosystem is as everything to do with what is called SDR SDR is an acronym for Special Drawing rights it's something created by the IMF the International Monetary Fund that is supposedly representing the global economy so it's a basket of five different currencies as you can see down here so the dollar euro rom be the yen and British Pound according to those percentages to reflect how the global economy is is doing as every time and this gets actualized updated sorry every four years I think and and so on so but this is the it's not the best but it's the the actual reference point of stability maker is is using to say this is stable okay you mean those percentages yeah so those are the percentages for each currency in the basket yeah it's like the value of SDR will be 44% defined by how the US dollar is doing and and successively for the other currency no it's not pegged because as you will see as the RS don't know but it is the reference point and then the way the the die which is the stable column will adjust to that is with something which is called the target the target price so it will still van situate around the SDR value is not paid okay it's a really good question this may be go through the mechanism and then ask no questions because it's going to become clear why is it not picked hmm okay no a peg it's would be yes but the price of dying is not equal to one SDR which will be packets so pegged would mean when one die is equal to one dollar or one is they are whatever and this is not the case it's adjusted through economic incentives with which we are describing so the first component of maker to issue the actual stable coin is a collateral assets right so to give birth to die the stable coin the first thing you need is the the cultural asset so you will need to lock something that has value like ether into a smart contract which is called SDP or collateralized at position to be able to issue die the actual stable coin and this can goes both ways right so you can lock up ether into a smart contract and issue die or you can pay back the die to the smart contract and get your collateral back then comes the stable part of the stable coin project which is okay so people will generate die or issue dies right and people will pay back die to get their collateral back so this will move the price of died anyway there is no where your point ignoring that fact so we have here a correspondence between SDR and die which should be the objective and we're going to move something inside this maker ecosystem which is called a target price to reflect where the die price should go so imagine that you have the die higher than the SDR price then it should go down so you will adjust the target price according accordingly to modify economic incentives through crypto economics in order to make the price of die going down but nobody will ever say you know this is not one anymore it's 0.9 worth of of SDR this should be done through economic incentives if this doesn't work still and we'll see a case where it is happening we have MKR holders so the MKR holders the lenders of last resort so if there is a crash or if there is something that goes horribly wrong we have another thing here which has values well it's it's very it's a MKR tokens that have previously been exchanged for for ether whatever and there will be an interaction with with die so if this goes around you have another thing of value here MKR to be used in that particular situation if you want to stabilize one currency you have to actually put both parts into so maker MKR is all relatively of one currency of 10 dimensions and die it's all stability so you have like one coin two parts MKR is the whole boot ility and is the most ability exactly MKR will absorb the volatility of dying yeah and not only that but your so no because die will remain stable and the vanity volatility of die can be absorbed by the in care if it works something volatile absorb the bullet to achieve something that is not volatile okay is getting out the volatility of die so that is stable we are saying now so that took me let me use an example yeah an example an example would be you know small variation of the price of die around the SDR will be dealt with by economic incentives okay but in the event of a crash let's say the ether goes from 250 now to a hundred that would be a massive depreciation of what was used to give birth to die in this event what will absorb that volatility in in die is n KR which we which is going to be used in that specific situation so this will be volatile as hell but this will remain stable well actually they define themselves as an autonomous monetary policy and they are still recreating a central bank infrastructure really because it is okay and so to come back to what Sandra was saying you will need Oracle's like a lot in this system to feed all the information of prices or the different prices of the currency that we are and we are using okay so why would we what we anyone participate in this system why is this attractive and to whom and we can we can see three kind of persons here interested in in making this working the first one would be the the user who would by die in order to pay beams and stuff like that and want to use this as a medium of exchange the storage of value because it has no volatility so I can use this as a way to pay whatever I need to pay how many people say it's so bad you will never use it for your daily purchases and we will need that a certain point we will need a stable point if we really want to create a quick to economy the adoption the adoption we won't get into because this is something specific to maker maybe then it can no because once you have died you can use that to do whatever you feel like like doing so you change one volatile cryptocurrency for another which is a lot less volatile over at I at home the second person who might be interested in in this Indian participate in this project the people who will borrow died so the people will issue new stable coins and those people will need collateral assets in order to do that and what they want is something different they don't specifically want to use die as a stable coin but they see it as a financial product in order to get exposure on another asset to do margin trading or in order to use the capital they have as a collateral and an issue die according to the current that the maker ecosystem can provide and a third space so that is the is the camera still on yeah can you let me know if it's if it turns off okay thank you so the collateral assets whatever crypto currency that is allowed to be used as collateral meaning to back the value of the dye that will be issued so for now it's ether Bitcoin digit goals and I think those are the three accepted today no they actually have to pay like sheep a stable fee because they get a stable coin so if you open up this CDO pin you have to pay and the longer you keep it open you mor have to pay because you can use the stable point yes but you will use also financial not instruments but I mean this is this as we'll see later but the small fluctuations around SDR will allow you that you have money inside a system to make profits of those variations by playing by the rules I insist and this is the beauty of the system by playing by the rules and by maintaining by stable you will make money and this is how you incentivize people to participate in the system and and the third type of person who might be interested in in joining other mpr holders so they are the ones who will take decisions on some parameters of the system for instance to accept a new cryptocurrency as as a collateral asset or to fix the ceiling of depth that the system can manage and so on and so forth or there are five or six diameters that MTR holders will vote on exactly and yeah so all this can be done by whoever wants to do it there is no you know specific title or background or academic credits that you need in order to join the system you can do whatever part you feel like doing at the economic level you you can afford basically how they incentivize can pay off like a bunch of money and something goes wrong and I have to push that money back into the system and how do I get so MKR orders provide financial security to the system or a financial a reserve a reserve of value to the system and in exchange for that service they will get fees out of all the movements between collateral assets and die so when people issue new die or remove die from circulation you will have small fees that will be paid to the mkr holders regulating it's the governance body it's the governance body yeah and but a governance model joined or in addition to an economic reserve so yeah we have skin in the game now and you decide on a cryptocurrency which will be included which is a really bad one so a decision was really bad then die will not be stable anymore because of your bad decision and then you are forced by the crypto economics to incentivize it so you would I mean another way to look at this is mkr holders are some sort of Board of Directors but decentralized and and there are many more than a Board of Directors and if they take bad decisions they get ripped off so they lose all the money they put in the system and but a new system can emerge new mko can be issued and this thing can start over again with new mkr holders so it's a way to test the decisions that are being taken and adjust accordingly but by looking at the market only there is nobody taking a decision to take over and that kind of thing now if the system remain stable everyone wins if but this but somebody else because that person will have lost money so unless you can put that same amount of money again it's going to be someone else joining the system we will get a bit more into the mechanics of it and UEL see so there are two situations normal conditions and extreme cases what what will happen under normal conditions you will have people as I said issuing die and and removing die from circulation by playing with those CDP's and you will have SDR as this stable reference point of stability and the target price right which can be adjusted inside maker to reflect where the price of die should should go up or down so under normal normal operations this is what would happen as we've seen whether I'm interested in boring die so I'm interested in in issuing new new die to do something with it whether it's to sell to other people or to use it as as a financial product to do margin trading for instance oh I'm interested in buying die to pay my bills okay so those are the two type of behavior we're going to observe and then to situation I can occur one is the price of die is above the target price or it's below the target price if what I want is to borrow die and the price of die is higher than the target price this is super good for me because what I'm investing in a CDP to issue die has a higher value than it should be because the die price is above the target price so I know in the future he's going to come to go down again but for now it's really interesting because I'm able to invest in this financial product and get more of my money and actually more than what it would cost me to close my position does that make sense no really it always looks for the target price and if the target price is actually below it's cheap to borrow so that's why I opened the CDP and these circumstances but the dry price is really high as we see so if I go to an exchange that is really expensive to buy sorry no I don't buy it well I I'm saying I'll wait a bit longer for the price to go down so what do we have what do we have here we have an increase in supply and a decrease in the demand resulting in a net effect of a decrease of the price of dye accordingly but pay attention that nobody took any decisions here we've just modifying with the target price the incentives to make people behave in a certain way and three economic incentives they should do it and we will get what we want which is a decrease in the price of dyeing and the exact opposite scenario can happen as well so if the dye price is lower than the target price what I'm issuing as a bar of dye is worth less than what I will have to pay if I close my position so I'd rather remove the dye I have issued so far so I close the position because it cost me less now to close that position than in the future because the dye price is too low and I know it's going to go up again on the contrary if as I was saying I just want to buy from the market to use it for me cheap so I buy it now it's a good moment and as a result we have a decrease in supply and an increase in demand resulting in an increase of the price of dying so but borrowing you mean I'm walking because I'm walking a portfolio of whatever coins and then I can issue diet against this portfolio whether portfolio is locked right yeah and then if if I want to take my coins out my ether or Dodge or whatever then I destroy the dye that is you'd kind of yeah you have you have to raise dye from the market or if you have it already it's fine but yeah so if Dyess cheap it's good for me to get out now because i can just buy a little die for nothing and get my portfolio this is one so you were talking about this case where the the dye price is below the target price super cheap for you to close your CDP no you might not be interesting in doing that but generally speaking this is what's going to happen because you take as the gentleman was saying in the back before you take advantage of those fluctuation around the target price all the times to do the right thing to maximize your profits which is which is beneficial for the system which is securing stability for the dye does that make sense no you see so you take advantages of those people collateral depth position it's really a collateral depth position so you're issuing debt which is exactly the same as in today's economy when you yeah you wish you knew new money it's a depth really okay and so this is fine but what's in it for the people that are securing the system so the nkr holders right so far we've just seen two people buying or borrowing dye and and we've seen that there are economic interest to do so the other thing which is to make the system interesting for MKR holders is that when you open a position and you issue new dye there is a stability fee that will start increasing so the longest the longer you leave open the most ability fee will be accumulated into that smart contract which also means that when you want to close that position the stability fee will be registered in the smart contract and this stability which is a small percentage of die in the end will be used to buy MKR from the market and burn it and this is where Dennis might correct me if you feel like doing so because I know things are changing all the time but not everything but things where your ways of doing things in maker are changing and this is something that might be reviewed due to a recent publication of the CCC exactly you're affecting the supply of money the supply of MK and then the value of each token goes up accordingly under de MK oh yeah thank you no this is deflationary because you burn them so you remove them from circulation yeah it's a way to if you want to join please do we will see how they are generated actually they already exists you can invest no in maker by buying MK are tokens right and during the system the system will burn like the if dye performs good then the system is deflationary so the maker supply will decrease from this million and if something bad happens like a Black Swan of that format trash then we will put like create a new maker and auction them and decentralized so the supply will increase and this increase and decrease in the tool supply of maker that also is tied to the maker price of course like if there was few coins each coin is priced now this is where theorem is questioned so you said that if in case of a crisis there is I didn't understand what what are the conditions for creating an auctioning out new you die if it's like good point because this is just what we're going to and I'm gonna ask you the question so what's the worst-case scenario that could happen to to make goes down or there is a you know there is a massive crash in the price of one of the collateral assets whether that's ether Bitcoin digit digits cold whatever cryptocurrency the mkr holders decided to include as a collateral a valid collateral to issue new die so if they take it back decisions and this kind of stuff happen we'll see what happened to them to the the money they put themselves in the system and the way these type of situations is resolved is like this so suddenly what was at the beginning the origin of the issuing of die has no less value than the die price market price in real life so what give birth what gave birth to die has less value than the die itself so we have a problem right because the value of dying does not reflect the value of the color that gave birth to it and so we have to adjust and what basically needs to be done is remove as quick as possible die from circulation now we cannot do that like you know I take your die and I take your die and we find no it has to be done in a decentralized fashion this is what Dennis was about to explain and this will be done by creating new MTR so we know this has value still we will issue more which will dilute the value of order outstanding m'kay are out there but this has value so the system will create new ones by die from the market to whoever wants to sell them and with enough dye we can close the positions the the CDP is there that are still open and we can get the collateral back and so and we can send that collateral to try to compensate for the MPR valueless that was was done by generating new and chaos so the process is we generate new tokens by the system so nobody's doing it but automatically with that value we buy back die from the market we closed the CDP that were open so the smart contract and by paying the smart contract back you are allowed to get the collateral back as well so we've empowered partly resolve the problem which was taking the back from circulation and then we use that collateral to compensate if we can no so if either still has a bit of value for instance we can use that to buy MKR back from the market and burn it again so in this way is like the opposite effects I know it's a bit mind-blowing it took me sometimes as we want to understand it but you're diluting mkr in general by emitting new one and then you burn them with a little bit of value that you still have here to do the opposite thing most likely MKR holders will get burned - yes certain because they carry their yes they are rewarded for caring yes so the whole thing gets to make sense unless of course this worst-case scenario what if just one fellow the glamour assets what if you just allow digits as collateral there you wouldn't have this you know a ninety five percent drop overnight race yeah it's not very likely that it will happen with either a Bitcoin I wouldn't be so sure about it one day hmm have you thought about this or doesn't doesn't make sense at all for some reason vernest you're wondering I think the goal is to actually keep the dice table and this is achieved by diversification so we are looking for the most stable assets which are and most diverse from each other so yeah gold would be a good example like a real estate would be another good example so it has to be liquid that's the big fungible but but yeah so the more assets we can go get from different markets so that if one asset class crashes all the other assets koechlin's when like real estate is tokenized for example then you could put those tokens into the basket because right now we'll pretty much all the credit tokens have a correlation of one point eight point nine sometimes so if they crash like almost everything crashes but I guess yeah but again I mean this is a decision that MKR holders are going to take so if you want to include the coin into the basket you're perfectly allowed to do so but you're going to have to assume the consequences of having included a coin into the basket it's called Sentinel and it's really interesting as well as a governance model and the way it's done is by measuring the activity that you have with your and your tokens so if you move them around a lot you're considered as a active user of nkr and therefore your token will be worth more votes it is going to have a higher voting weight another one would be left over I know one of the reasons why would you together with the trip you guys is because we actually using the world which is the the technologies that I believe is sort of pioneered by omakr so this is this is technic this is buy and burn mechanism right there 14 pads on no buying buying well this bind burn is is like reserved in the stability fee payment to em here although specifically here you have more things going on because you issue new MK off first and then you do some sort of stuff and then you burn some of them but not all of them but yeah okay because because in just I wanted to add that the business case for this sort of some of the mechanism of stabilizing your coin is is our ice cream sponsor today but I'm not sure if it's still used in maker is this contract called the vault that actually keeps this and wet weather weather it's no one we used maybe you know report you said I know maybe we're just but it's fine burn mechanism basically dad you know basically taking there from acre and I mean really it comes down to I'm not a developer but it's coming comes down to specify a smart contract where you can only send coin to but you cannot extract all take comes back from it I mean maybe people would be able to sell their coins for let's say ether from this contract and then the contract just burns yeah if this is the objective no we can what is happening like it's a contract which is which is made as as an option so it defines a price it wants to buy for something somehow I can solve your opossum yeah so let me show you this because just to recap we've we've pretty much done with with this but if you want to get more details about this let me show you what were what Dennis were talking about which is the double auction and this would be how you can you will be using em here in the system in the case of a crush right so you have a depth auction and a collateral auction this is done automatically in a case of a crash you create new MKR which dilute the supply of MKR tokens you sell MKR to bidders automatically because what you want is to buy die from it with a new token issued with this die you close the the CDP automatically again plus the liquidation penalty of course and you get the collateral back so the smart contract is handling new collateral from the CDP it has closed you need therefore liquidate the CDP so that's done you'd be done with it and so you go now to a collateral auction with the ether or the bid digit scores that were left in the CDP you can you will first sell it for for money and with what's left from the cell money you will use to buy back MGR and burn it and the die left over so I imagine that you know this was a bit a little bit too extreme or it closed more than it should you will have died left over and so this will go to a reverse bit mechanism in order to in order to [Music] give the control back to the original owner as well but this you should really look in into the white paper to get all the dynamics right because it's pretty hard Koster yes yes it's not paint but it's right if that fills the hole in your whole page is gone I can't tell you why but if the market is going down so fast went to save the sages or your audience which you made so this is happening for example in the case like when the China pens are CEOs salary you have in America cooling down so what do you do with your crypto do you existed here then it's maybe very public that you deal with what so what do you go with you are with the gates you make while waiting or investing and so one way is to move into other cryptocurrencies which are maybe more stable because they are less traded and they haven't a solid business case like we're not going to promote one but just an example is which is a couch decentralize doubt solution with a team in France waves are passing the ball like we saw with the tip China did and then you kidding again oh you can use temple which is basically the option of Tesla it's a statement comment but it's a shitty coin because it's not really packed with will so it's basically to to save your earnings which made without having to know but I mean one sorry but one complimentary explanation to why to choose SDR in the first place is what is what does stability mean I mean it's really hard to say something is stable if you can't use anything already existing in today's economy and so I mean by no means this is the best the best the best reference point of stability but it's the one that has the largest scale on earth today because it's supposedly representing the world largest economy as we've seen it's a basket of five fiat currencies maybe even the future and I think maker is also working on that we can find a better synonym of stability and one day euro when it start to get like this then I assume euro at one point might drop up from this basket and for another crystal point will enter so right now even though we don't like it we are still ruling the world so but this might change and then the SDR will change as well because then it might be actually stupid to use fear because stupid because we have might be not stable anymore in the future but now it's the most stable one so one last thing is if I may because Dennis is here and he's doing something which has great potential and it's not really heard about at the moment and it's called very sexy formal very verification and I'd like him to pre flee introduce the concept because this is I think something which will get more and more heard about an important for for building smart contracts products so Dennis I've probably make a dull team and I'm not really into the Crypt economics gonna have a pretty boring talk for all of you who are not developers but first of all let me ask who are programmers here so who write code ok so I will talk about formal verification on the blockchain and how we apply formal methods and at maker down so first of all why formal vacation at all so first of all we have something called unit tests and unit tests really what it is if you have a state-space of your app then you just pick holes in different specific states which you run the tests to and look at the outcome so it's like with a really specific value and address you run through through a test case a better thing which we also do is fast testing where you specify a sub area of your state and just like generates randomly different tests and poke in different state spaces and what formal verification allows you to do is make actually statements about the whole space without leaving any holes so here there are still holes inside and you can still get an exploit because you didn't really verify some specific state in your state space but formal education allows us to like close this hole and what for multiplication is all about is it's mainly about specification and verification in the development process and they will talk more about like what the specification into us and what with this verification really mean to us and we choose to go with lineal logic and logic as a whole is a really really old language so it's like being studied for hundreds of years and it's really sophisticated and a lot of things can be press really neatly in logic but usually logic expresses statements about truth so we can ask what is truth what is not true in some particular statement and linnea logic takes this into a logical state and resources so we are able to make statements about linearity and statements about security of resources and consumption of resources and consumption of states so what we do when we do formal notification is we write like statements like this with funny symbols and maybe you saw like in logic Larry says thing called implication so a implies beef for example if if it rains then the street is wet it's an implication which it's written usually with an arrow which implies a true statement so if it rains then it's true that the street is wet Alinea logic we have additionally to this because it's like a super set of classical logic we have a lolly and the lolly is kind of a promise or a linear implication so with this we have a promise that once we have an a we can always get a B the same thing here so this is called a tensor and the tensor is kind of like a simultaneous conjunction so if we have an a tensor B we know that a and B happening at the same time in a state like they are not separated but at the same time and we both happening and we have different conjunctions so but a good example about like how we can model states and logic is for example we have a we have psy as a coin which is parameterize in the owner so this size owned by Ellis and we have a promise that if psy owns an L Ellis owns a sigh she gives her side to Bob which she promised with this statement and given those two both statements we can prove which is this funny symbol that Bob has an as a token so we can go from this state and transition basically to this state or we can prove that once we have those resources which is Ellis coin and the promise that Ellis keeps her according to Bob then bob has a coin and with this we can fold up more difficult state spaces and like make formal statements about state spaces with yeah what we have right now is so it wasn't mentioned by you but before died because diaster is really huge complicated concept we have something called sigh and sigh is a simplified die so it's like a cut-down version without a lot of features which one collateral type which is the maker with which is the ether which is like like we just have one collateral which is basically ether we don't have this diversification but this is a thing of the future and we have modeled sy in linear logic and basically what we do then is just right finally formulas for every action which is possible in this size system for example this is join an exit which means that with your eath you can buy s KR or get s KR or you can like drop s KR and get it back so it looks funny and it's just 2 actions a user can make in the system question yeah so each possible behavior from someone that that whole design would be reflected here mathematic exactly it's just it's just state transition so it's it's a promise that once you reach this state where this and this and this and this holds at the same time you are free with when you have this promise also as a resource available to transition to this state which is this one so basically this is removed and this is put into the state space again but this is just a high level specification it's just like to get a really deep understanding a mathematical deep understanding of the system's whole so why we do we do this it's once we have done it we can make extra formal statements and looking for proofs so this thing actually means we have a proof and this means we don't have a proof so it's cross out and we don't have a proof of a state which is looked like this and this statement means that the total STR is less than some W and some W is a SK are owned by a user so a user can never owns more than there is SK are in the system which is basically just a sanity check of the system so you cannot put more collateral you cannot have more collateral in your balance then there is total collateral in the whole system just to say need to check but because we have this symbol previously and we can start a theory improver which gives us a proof of the impossibility of this statement with our modeling that this is never reached so we know that this state is impossible in the state space with an actual proof and everybody can verify because it's it's open and this was the kind of like the specification part so we specify our system in a really high-level language try to make different logical statements about it and poke into the system and once we have done it we go to the formal verification part and the formal verification is we do the same thing in linear logic again so basically with the whole lolly part we we're modeling the EVM inside of linear logic again it's the same models like with the same thing which we saw previously so we have a state which is we have a program counter we have the gas and we have set height that we have some code on our state space and once we have a proof that we have this at at our state and the uppercase variables are written as they are variables so they can abstract specifics specific values so PC for example would be a number and once we have a proof of this we can transition to this which would basically just execute push 1 onto our VM so just push the value onto our stick this is what it's saying but we have model of it in linear logic so what can you exclude with that proof from happening to the idiom later so we can actually once we have a model of the EVM we can make formal statements about a state so once we have a code we can formalize that a state on the EVM has never reached the for example that's on the stack position one never a value of zero is written and we can make a formal statement of it and because the EVM is deterministic we have a proof of it that it cannot happen it at all it's basically yeah yeah exactly if this is what we're doing so we have this EVM model written in linear logic what we do then and this is for example to push one instruction what we have now is we take a coat of for example some simple wallets which we put into our state and we can make simple proofs with it so we say once we have a coat and we have an initial state and we have an assumption and assumptions would be that for example on storage space one there is some certain ID address written that under those assumption with this coat and the initial state the same coat a final state and stop execution is written and it really depends what you put in your coat and what you put in your final States but you can derive a formal proof of some states will always happen never happen on it depends really on your logic because it's kind of a superset of classical logic so you can express really what you would you like and the next step which is actually the fun part is once we have a specification written in linear logic and we have an implementation with for example a simple wallet or a multi signature wallet with our EDM implementation put in linear logic we can make a V simulation be seen that the similarity in this simulation here with showing that our specification exactly implements the implementation and the implementation exactly implements the specification so they both behave in the same way and we can do it also inside of this theorem prover and then need part of it is that it's deterministic and the proof can can be generated automatically needs sometimes though the final step though is which is I still don't know whether it's possible or not but once you have the specification to actually generate the implementation so you don't need to write the the bytecode version of the contract yourself so currently there are different options so we have actually proven like really really small contracts like a simple wallet you is she wrote for larger things basically it explodes and since the solidity output is really large and you have to control every opcode because potentially you have to make assumptions or adjust your initial state space precisely you have to have a really deep understanding of your implementation on the opcode level and when you have large contracts which make your has it generates a really large amount of opcodes it's really not practical to go over it and try to understand it's what we do currently is for really small contracts for example and multi signature wallets is we try to implement it in up code ourselves because we have a deep understanding of it and this would basically eliminate this state so once we have a specification maybe it's possible to even generate the op codes here so you don't have to program them in solidity or an opcode level because this is the most time intensive part what's been SCAF so the research part is about scalability in the formal verification you could see something and we we still need to stay moment verification to be able to handle well even this is scalability this I would say is decidability I don't even know if it's decidable 2 or like practically doable to do this implementation but this is like the holy grail of what we try to research and do that's basically it so it was not too boring if you have questions I'm happy to answer actually like two months ago TL A+ well as the UM port that is again language to describe formally protocols and international silicone agents and I guess a DME mobile is basically similar the basic explore all the space of all the states that are possible in the system then you can put in variants and within violence again check if these systems behave incorrectly and I guess it's like more or less similar because your voltage weak here but if you're describing these states change right yeah yeah they are differ from state 0 to 1 this is lakeya TLS plus it's like 1 which is similar and more established than linea logic maybe the most advanced on the EVM part research is ke V M so there are a lot of papers about the K framework and KVM on verifying smart contracts on byte code level and actually the Dow hack for example was verified or like shown that this can catch today is difficult with current yeah we have we aren't that foreign or research to actually encounter real examples of state explosions but state explosions a real problem for example if you have large floating point operations there a state explosion happens because yes exactly but maybe you can abstract it away with like your assumptions so you say because of something happens and yes I kind of talk more about this we haven't encountered yet but this is a real problem which we will encounter when you reach this holy grave from going from specification to vacation don't you think it's might be not usable because then the gas prices are twice we were not healed like small contracts that have no gas price because so - so one of the naive approaches would be so because it's kind of like um there's a thing called Curie Howard as a morphism and this is really what's used behind hair still okay Mel and all those ml cell languages where you have a type system and this type system Europe actually is exactly corresponding to internist ecological and what is generating in in the background is lambda calculus representation of the proof of your statement which is in some cases way too big to put it on the blockchain this is a naive approach but maybe some optimization techniques can make overall for example Hesco and also be compiled down to a bytecode and not only interpret it in and this other way but yeah thank you very much [Applause]

Automatic transcript — names and jargon may be misspelled.