ABOUT THIS EPISODE
Episode 87 · 1 year ago
SHARE THIS EPISODE
Episode 87 · 1 year ago
Hashing It Out #87-Informal Systems Ethan Buchman
ABOUT THIS EPISODE
I guess this ix episode has brought youby Avalanche Avalanche, solves the biggest challenges facing a theoriumsdeveloper and decentralize finance or defy community. That is velocitysecurity and time to finality, under three seconds on the firstdecentralized network, resistance to fifty one percent, a tax wis, completesupport for the asyrian virtual machine and all the tools that have fuel defiesgrowth to date, including metamask web three doas myetherwalet remix an manymore coming, avalanch Il Beet peridy with a therium for defi developers thatwant a much faster network without the staling issues holding them back etstarted today. Building without limits on avalanche by going to chat, dot,avax dot, network hat is chat, dot, a v Ax dot network xnow injryindw, welcome to hashing it out apocastfer.We talk to the teck intevator's, mind, blocked in introstructure anddecentralize networks. We dive into the weeds togut at Wyan how people buildthis technology the problems they face along the way I'm listening, tand learnfrom the best in the business syou can join EIR rekwelcome back everybody.This is episode. Eighty seven of hashing it out. I'm Dean I'm here today with Marellion,say: What's Upin Today we have on our show Eten bochmen of informal systems aeven and just GOINGTA. Let you quickly introduce yourself O, I'm Eten, most notably a copounderof the teniment and COMTOS project. U For a various Rorles over the year, butmost over the years were most recently ce of a new company, informal systemsthat focusd on Hom arification work in the Blockchan Pase, specifically ondistributed systems, consesses, protocalls and so on and implementations in rust. So thesedays we're focusing on the cosmost protocals implementing big chunk of thecostmo stack and rust. I doing a lot of Fon lerification work and TLA bus okay. So this starter question wealways ask everyone when they're on this show is what wrought you intoCristo. How did you get started? Well, I've answered this cuctin on many BarAFERFORI. Guess it to be CONSISTENC but e at somepoint on paint of meenter.Essentially, I saw my background was in in biophysics and I was sort ofstudying the origin of life and specifically how life emerge in auniverse. That's allegedly always running down where living systems arethese. You know amazing systems that are kind of emergent, ND and running up,so to speak, Um and backing around twent and thirteen. I sort ofdiscovered bitcoin and first kind of ignored ix S. I didn't understand itand then, after spending a little bit more time with it and hearing about itmore it Kindo. I kindo realized that it seemed likethis was the origin of life in the digital media, and this was like thefirst time that you know we had all these. You know communication protocalsover the Internet, but this was the first time we really had like a a real like emergence coordinationprotocol, Iacoptese communication protocols that allow something to kindof exist that wasn't really possible before that sort of had a life of itsown and that this could be the foundation for, like an explosion ofyou know so called digital living systems, and I got really hooked by that andobsessed with sort of applying iophysical, intuitions and intuitionsabout organisms, D and the nature of life and sustainability, and so on intothis domain.
And I've just been sort of enrapturedwith that ever since D, I guess a big part of it also was at the time Um I'dsort of been learning about the financial system and- and you know forthe first time paying attention to what you know the economic structures in theworld were like and how broken they were, and I was sort of studying you know,machine learning and stuff like that at the time as well. You know on applyingmachine learning to like biology and whatever, and I sort of realized that you know there's enough people workingon ai being accelerated in the current economic conditions. It's not going tobe a good thing to have. You know more intelligent, Ay eye. It's just going tobe used for exploitation and oppression. I think that's sort of being borne outand that you know what we really need is to is to fix the the global economicstructure and to have something more bottom up and more sustainable. An that.You know better resembles. You know the standility. We have in biologicalsystems and it seemed like the ideals and technology inherent in bigcoin weresort of t e, illuminating light on on a potential path for hod to do that, andso that I sort of went holly and on leveraging that kind of technology,consensus systems, croptography Game Theory et Cetera to you, know, solv these issues in in the global financial systemessentially and been been here ever since. Ok Awesome, so I really like the workof informal system and, as I hang out with Shawng quite a bit wo talk to hima lot. It's always an interesting conversation and whenever I look at thework you guys are doing, I kind of feel like or I ask myself why not everyonein this pace is like doing this approach that you guys are ndoing'cause. It just seems like the right thing to do what what brought you intothis Appo proach this method of building these systems. So we built tenoment in go and we diand.You know h. The problem is with a lot O with a lot of distributed systems isthere's like black magic involved. Like you hear stories of like of like Paxsosand how like Paxo systems were implemented and like you have like acredibly small number of people who are capable of like actually making changesto the system and who are depended on for Fror, maintaining the system- andyou know so- we sort of you- know we're in a similar world with tenerment fromall our experience of actually building that thing up and the way bugs wouldemerge. Um was really you know concerning that, like you have thislike incredibly complex thing and there's only a few people who reallyunderstand it deeply- and you know it's hard to you know- can be hard to testand it's hard to know it's hard to like really convince yourself that the thingis correct and then especially it's hard to maintain and to change. Soif you want to make modifications, you know it's a big integrated thing and totry to like dive into tenements 'cause. That's I package, for instance, andunderstand, what's going on in a way that you could make a change and gainconfidence in it was really challenging D O and a d Inot just about the actually it's not even just about the the code is also the protocol themselveright, Unso, we're all we're all building out these new consensusprotocols- and you know everyone and their grandmother at this point- has apeck consensus potocall and were all building out like protocols around them,and you know light client phrotocols, like all these debi protocols on top-and it's really hard to you- know to gain real assuranceis that theprotocols are correct and behave the way you want them to and then that theinvitation is correct and behave the way you want them to the invlanintation.You know really implementsd the protocol until we felt that you know,based on all all our experience like building Tenerment, and you know,difficulty of gaining confidence and making changes that it really madesense to look at form of verification for distributedsystems and to look into ways to actually build more confidence in both the protocolsdistribute system protocols and in...
...their implementations and finalways, tokeep those things and SINC can come up with better processes. For you know,building reliable distributed systems that would be more understandable bymore people and and more easy easier to maintain and easier to ensure thecorrectness of changes. So so when you say that you write theseformal mescifications for your protocols, what's the process therecause, I actually had this discussion with Sean as well and like Woitd, itintl a SPEC. For example, you have this Speng, but then how are you certainthat the co you're running or the implement at your rest? Implementationis actually a correct implementation of the Tiele Syeh so that that that's thenew count right and that's not something we've totally figured out yet. So you know, people in other for ofevication is actually a big field and there's many Kindof subcomponents andyou know one problem: Is that, like thereprobably isn't enough cross talk right, Andso people who people do things oneway and they won't do things other ways, and you know so, there's a wholethere's a whole world of formal arrification. Where that you actuallygenerate the code from the Speckso you right, like you, K, Ow, you write yourcoat and cock or something and you get like a poofet, a perfect like proof ofit, then you actually generate executable code and you R un, that codend and you never modify it as human and you know, and then all you have to dois really berify your the compiler there. And then you know that. Okay,now you have confidence, an Youcotas Crak, but Um. you know our our CN. We have a numberof concerns with that. One is like the the Um the. What are they calle? The prooveassistants are are quite fract, diling and difficult to use and require a lotof experts. And you know, building out of these, like complete proofs likelike in Cok, is actually a very M, very, very difficult enterprise and requires, like you, know,tremendous expertise and it's difficult to maintain them. If you Gif yourprotocal changes or something- and you know, there's this sense thatactually just generating the code also isn't going to be sufficient becausesomewhere along the line, you're going Na want to be able to make changes oradapted, or you know, integrated with W H, with other componants of code thatmaybe weren't generated by Bicok or whatever. And so it's a little bitfragile to think that everything is just going to be able to be generated,and so we're sort of trying to take a different approach. Um, where we're notreally focused right now on generating code, and you know, maybe thatsomething wul get into porcomponents of the system. But what we're looking atis using the the specifications as as a communication tool and as a way to Bildlike really clear, unambiguous understanding of what the protocolsshould be doing and and then trying to find touch points where we can alignthe specification and the implementation. The one thing we'redoing now is, for instance, a lot of parts of our specification are tagged,so they have like little labels. That say you know for a definition or for anEnbarient, that's supposed to hold or something like that, and then we havethose. We persist. Those lady bles in the code as well, so wherever that partof this pack is being implemented, we also have that label right and that ono trying to build sort of hooks between this back and the implementations, youcan sort of jump back and forth and sort of see directly. You know thatthis this code implements this pieace. So that's that's one thing, andobviously you know this isn't perfect. It's not th. It's not formerly verifiedcode per se, of course, but yo K ow we're trying. What we're trying to dois realybuild practical techniques that are going tobe accessible, that anyone can adopt without making you know major changesto their technology or to their stackar their way of doing things that allowthem to. You know incrementally Adot, more correctness, oriented practicesand so we're trying to build some tooling around sort of tracking thesetags between spects and implementation. You know and seeing okay, you have allthese tags an your spack. Are they all laid out in Hoir inremmentation insomething missing and then maybe making it easier to Jalk back between the twoor maybe building tools to show heres what the definition is and this packheres what the code is and the implementation you know now justinspect them as a human and just you know, facilitate human review. Anotherthing Wer we started looking at, which...
I think is actually pretty exciting, isgenerating tests, so it might be, you know, generating implementation.Fullblown implementations is a little bdaunting. Maybe a little bit fragile,but Um generating test is, is maybe again more accessible n. You can writethe implementation. The way you want- and then you have this like testing inher face and if Youre, if Yoespeck is written in he ia that really captureswhat the code should be doing. Then you and you're using a model checker likelike we do with Tla plus, then you can actually get counter examples, otef themodel checker that are like traces, you know of like a a bad case, not optimisticcae,something where, like you know, something went wrong, for instanceright and so then you can translate that into something that can be run actuallyagainst the imvementation. Then you have a much potenting, much moreefficient way of generating these, like pathological cases to test yourinformentation aguasnst right and again it's not. It doesn't mean you haveformerly verified code in the way that you know the coe that would run onsay aspaceship or UN certain other. Like critical appliances is going to be, youknow generated once and then never touched again, for instance, but itdoes help build greater confidence that the implementation is actually correct,because it's able to correctly execute these test cases generated from a modelchecker- and you know, model checkers- are very, very good. Finding theegecases right, because a lot of the a lot of the protocols were dealing with.You know, especially when you're dealing with like distributd systemsand concurrency there's so many interleavings in so many ways. Thetexecution could happen. That is really difficult to reason about the Egucases,and often the bus are in the edge cases, while they may be rare. When they dohappen, you know, then you're you're kind of you're kind of you knowstruggling to figure out what wet Ron and so with a model checker. It's a loteasier to actually find those ecucases and find things that, maybe youwouldn't have thought about and get a test for them that you can then runagainst our that you can then run against Ropontitation, so that that'sanother example of something we're doing with the TLA. Now um t that's sort of onon the TAFRN, butwe're also starting to look at what else can we do in the code and startlooking at actually meliving techniques to formally verify the code itself? Andthat's you know more like stack anaysis tools, extending the ruskconpiler to beable to check sort of more variancs about the code and so on and as allstill very exploratory and in a research phase. But you know what we'reour goal is. Really it isn't so much to have like to be ablne to put down astamp and say this is formly verified codes, it's more to make tools ofcorrectness, oriented development, processis, more accessible, and sowhatever we can do incrementally to make those kind of things available.That's really where our focus is pntile to be Yo, K, quite accessiblespecification language, and if we can build out, you know tools to integrateit with. You know: Poceedin amodelas testing that seems accessible. Thesetags, things like that that can just help people you know, give them sort ofhoops to build up. Their sort of you know correctness processes or is the idiot like ar really focused onBrust tooling, you mentioned like other depiponcalls and Um. Is there evasion of this thiscoingbeing accessible to other languages, or you focus on Hes Eure? I mean we outobe e Li to be as acpessible as possible. I mean T la, I is a you know: language,independent Spestification, language, trice and so to the extent that we'rebuilding tla specific tools, that's just making Tla as a poopestiicationlanguage, more accessible and tha we've been building a model, Checuer Portila,it called Appilacchi, so tla plus comes with a deepall modelchecker called TLC,but tl C is like an exquisit novel Checker, so it enumerates all thestates, and you know basically on you know, systems of larger than a fewnodes. He runs out of memory or runs at a time, and so you can't really doanything interesting. So I mean no, you can't do anything interesting. You knowamazons using in for systems and production whatever, but there's limits on on how much you canverify and so um and what kind of...
...behavior, and especially when you're,trying to model like Bysatin behavior and you know, adversarial activity. Youknow the state baseexplodes with the number of possible things that couldhappen right and so we've been developing oppilace, which was you know,N envelopment for years before informal, but is now sort of in house which is asymbolic model. Checker Portila clot, so at mass, the TLA spestification intois embollic representation that can then actually be sent over to Z, three,the SNT solver to do you know much much much more efficient checking of of certain properties, so you can getyou know for some expect. You can get orders ofmaginitude speed up, sosomething that TLC would take hours to do. OPALAZYOU might be able to do insecnds or minutes and certain things that TLC will never never complete.OPOLOGIC can actually complete. So that's that's really exciting and nat'saccessible to anyone. You know no matter what programming language you'reriting, but for the time being, we're writing our actual code and rust. We'refocused on you know, currently on the COSMOSICO system and building out youknow, tenement light client and I v C and ultimately attendant Bullno anddoing all that in rust, and so even that you know we're trying to align ourresearch efforts with our development efforts as much as possible.We'recocussing on you know, Verification Tools for Os, but we arehaying ou. You know forsus a little bit of attention to go and thinking aboutways that we might be able to apply like the the model based testing workto e go implementation of tenorment, so we can gain assurance. Th that you knowboth implementations are sort of correct d and things like that, but inin the longer term, obviously we'd like to expand to to more languages. But you know on theshort term work at as UNRUST 'cause. That's where I developed is so in doing this. Let's call it anexperiment of more berified software. Have you guyshad to change the way you think about code 'cause? It seems like it's acompletely different paragon, especially when you're trying to dothis motel based testing on on rust on your rustinplimitation, like whatwhat's been the biggest change from the way you think about code or PA thoughtabout cobefore versus Hou Yeah. So you know think I think o our our ourthought process has been involving quite a bit on this and you know we'relike rapidly in validating ideas, and so initially we kindof came to Itd dwere like OK. The way this works is first, you write your speck and butactually one's back isn't enough. You Ned M ultiple specks for differentlayers, O first, you write at like a high level back for the protocol. Youverify that and then you'll write a lower level back for what theinpleventation is going to look like, and then you bear it by that and thenyou know you can more or less just sort of follow this back and implement thecode, so it lines up kind, O directly, Um realize that doesn't work. We probablyshould have known ahead of time that that was sort of naive and optimistic,and what realizing is that? Really the the specification process and th? Youknow the development process really do need to go kind of hand in hand andhappen together, and they they heavily inform each other and the most valuablethings we've learn have been from from he back between the two. Where Um, where you know th the specification isongoing, is evolving as we're doing the development of developments on going asas we're evolving the spescification and the beeback is really important,and thinking about you know how to make this. Thespestication in thevarifocation work really accessible to the engineeringteam so that they can like take away fromthe the work that was done in the SPEC and actually understand what it meansfor an implementation. Um, and you know a lot of a lot of things, um a lot. Alot of like understanding of code hasn't really changed that much to be honest, I'sjust you know it's just a slower going process where you're kind of trying tomake sure that you'ren rent, just like rushing ahead with the code and thatyou're Sert ofing ball. You know entangled more deeply in in the in Thiack process and the merification process, and that researchers are sortof more involved in looking at the code and making sure that the that the design is actually going tomake sense from the perpective of...
...investication and that it will betestable and that forinpocent you'll be oin to write something that you'll beable to actually exercise with the withtheolt. What say from the modelbased from the MONDOL based testing, and so we've Goe back infor a fewthings. I don't know that there's anything any like major take away on the codethat isn't sort of already. You know standard Um. You know good practicesfor code in terms of how you attract and how you make sure things aretestable and and so on. You guys must have a really special setof developers. Cause like most developers that you work with alreadyhate writing any form of documentation. I can imagine like, and normal developer coming in andbeing told that before you implement something. You first has to write thisspick three times over her uhhh yeah. Well, you know the researcher t therthe's, a pretty big Tan of ether to I mean wereup again oum, you know earlyon, we were really focused on on theresearch side of things, and so researchers have been have beencontributing heavily, but we've really been trying to make sure that you knowit's an integrated team. It's not like recherd, just rine its back and thenthrow it over a wall that the engineers were then supposed to implement it. Youknow we're really trying to build that that eat back loop, Um W. where do you draw the line betweenwhat a researcher is and what I developers? This is a great question because we'recrying to eliminate the line he after got rid of you know her. Themain title on that was like research engineer, and you know anyone wascoming on in a research. Kind of capacity. is expected to be involved inCode Um, but you know we do a few folks or whoare kind, a you w who are professors in a past life. I guess before an formaland and sort of have know much more experience with like Um. You knowacademia and research agendas and really like unformalizing researchproblems and so on. You know there. I guess a little bit less involved withthe code, but even still we're trying to we're trying to keep them. You knowtightly integraded and looking at the code and trying to think about how toinsure in the correctness of the code, but I guess the You ow, the distinctionis really more about at, like time is spending kind offormalizing the protocol versus time you'R spending trying to implument thething right, and so we have been doing a lot of work really trying Yo know wetake we take a law to think e's for granted is what we're realizing andit's like you know, talking about like tenorent like clients for years D, it'slike Oh yeah, it's easy like Ezyit's. The light cint is trimial right, likeis so far from trivial, when you really try to like actually formalize themodel and find out what's going on and had a reason about it and had a reasonthrough it like fully so that you could specify it in. You know: Intla g hallchecker really to really check everything Um, it's it's a lot, and so you now, the like principal scientists have played ahuge role in actually like formalizing the model that this protocol wassupposed to operate it an helping everyone sort of understand that model,and then you know, then htheable Totsou can mo Ford Na step out like a bit higher level.Just for a moment I on on get backed into this stuff, but like how? How bigis your team right now um like what is th the business model? Inowyehso m. You know Wer we're initially set up as like RMD ServicesCompany, so you think about us in the same same spirit as Gawa or runheinverification or trail of bits, and you know sor like security, auditingcompanies or whatever, but folks that are like offering Om witarfication workas a service, and so you know we're open to h. Youknow we're really hoping to help really all the like layer, one wacangcompanies projects or put theire spestiications on moreformal pudding s. They can work with us and we'll help. You know formalize themodel and and start writing out dealing plus pestipications for it and anBerahii, and so it is a oferst order.
SERVICESCM reallwe're, trying to figureout a baseline, is how to build a sustainable kind of research for Um,and you know we're hoping that there is we're anticipating that demand forHormal Erification, and this kind of work is going to grow, especially asmore and more blockchains are launching and there's more. You know more of oworld depends on distibuted systems and- and you know these OPE sorse databases,inplement contensive, protocalls and wornvariations on them. So we're sortof betting on that on that growing market and on offering the this bacinpestication afamerrificationworked there. Of course, we're also a development shop and so we're hoping tohelping you know actually implemment things so prinsance. You know ourcurrent were currently engaged by the entertained foundations. Tha We spunout of the Entertained Foundation January and a big thunk of EUR team wasactually working there before we funt out into anformal. So we have a YOcontract, Minertin condation, to do her. Munch Ot. This work for cosmost tat,afformally Beriby, a lot of the protocols unto implementthem an Raston and were certainly open and are starting to talk to some otherprojects about doing similar work for them, sort of starting small to proveout our capabilities and then growing network overtimes. Really, for any, youknow any layer. One Project T has a Consentiv protocall Um that is kind of new and that that'spretty much all of them. You think about you know: popadod, a theorum twopointo near Protocol Tezos, like you know, Salana Sello, like everyone iskindof developing their own consensi protocol and many of them are actuallyyou know they can be seen as Marians of tenorment. You know a lot of peoplestart with tenement as like an initial kind of simple visiting Poltarqu Tansaomthing. They go from there and expandit whatever direction they wantto make it. You know more efficient, anddirstealable or you know whateverkind of change theyy're looking for, and I think that most of those areprobably insufficiently formalized, and you know we would love to help put allthose things in a more form of pudding and really establish a you know, clearunderstanding of what each protocoly is and how it works and say how itdifferencs from tenamentor from others and what properties at satisfies andand to actually verify those properties in a INA accessible way in the longerterm. You know we're we're, certainly interested in in Um, finding a product niche and so, forinstance, we expect that there's, you know, there's opportunities aroundAPPALACII, this model, checker and maybe ways to you, know to think about some. You knowopen core and you know selling services around it or you know, cloud hostedversions or whatever so we' we're exploring what potential longer termbusiness models might look like and Probab pespective m. we're also thatsomething I didn't really talk about, but yo e. We state inform of mission interms of verifiability for distributed systems and organizations that we'vebeen talking a lot about formal, arrification or discributed system. Butthere's this whole other piece here, which is motivated by the same kind ofexperiences and challenges of running distributed organizations and the sameway that distribute systems are hard to build and hard to know, they're,correct and hard to change and art to verify, and all this all the same stuffapplies to your organization. How do you know your? Your company is Crackeyou book Ar in Good Order Um, you know your your finances are good. Yourcontracts are r organized whatever, like you minio. All of this is, is very,very challenging and people end up haying ing up thousands of finethousands of dollars to accountants and lawyers who can't agree with each otheron. You know what the State of the company is or if it's correct, and sowe've sort of been looking at that problem as very similar to the problemfor tackling an distribute, sisteme space and thinking about coolas. Wecould build there for ourselves to make our own. You know improve thecorrectness of our own organization, but that could also potentially be spunout into other companies. SNLY, not not just like dows come tomind as es like this Thi's actual code, you can verify that Tas, like you know,O Organization Sone, think they're talking about like you actually have anobjector, a symbol that represents the...
...saleperson or something and that theyare youv defined to specify how they react in som even happens, and then Ilike actually verify Al Thist, omudition yeah I mean you can go. Youknow this. This thing can get Um Pretty Gysopiang, pretty fast thaf. You takeit all away, but T it's not to like. You know, try to exclude the autonomyof like the individual humans where farticipating and the dows have reallybeen focused on, like you know, automatic execution of of like businessprocesses and and I'm honestly, a little bit less concerned with theexecution than I am about. The state itself like what is the actual currentstate of the corporation and is it correct, is a compliant and if you wantto make changes, how do you track those changes right and I feel like th. Thebusiness of running businesses has so much to learn from open sourcedevelopment and from all the tools that were developed over the last couple ofdecades to facilitate distributed. Collaboration on code haven't reallybeen brought to bear on distributed, colaboration on t e business right andthat's things like plain tax things, like version control, continuousintegration right all these things that are now second natured to any developeron a giup repository that without it you know, it would be impossible toimagine how we would collaborate on on that piece of software. None of thatstuff has really been applied to businesses in any meadicul way andeveryone's just collabeorating on, like you know, g, sweet and some other setof proprietary products, and it's you know. Frankly, I find it like a bigdisgusting mess. The way everyone's data is a siloe and locked up in thesepreprietary systems, and you know, there's no, it's not open a I a theees,it's hard to digest another formats and so on, and so I really think what's missing islike a a sort of diff style approach to to running your businesses with yea,like I said, having more of the data in plain text in version control, so you in version control, so you can trackthe changes and continuous Andegration, so you can like have cheqks. That'slike. Oh. I wanted to make a change to my company. Did I do it all correctly?Like I, you know I drapted a contract. Is it all correct right like it couldactually verify all the componants that you know based on whatever the samething we do with codes b? I think there's a huge opportunity to actuallymanage our business es. The way we manage our software and that'ssomething. We've been investigating and loving at ways, and you know our our.Our hypothesis is like look if we can figure out how to build more correctsoftware more efficiently and more correct organizations more efficientlythan we can commine those two to build, correct software organizations, andmaybe have you know in the longer term, something like an incubator that youknow spins out. Companies were a lot of like the overhead, is kind ofadvertised through the varification tools and theorganization tools, but those ar those are the dreams in ashort term. weere really focused on on like cosmos, and you know the intloching indropability, the you know, explosion of opportunitythat will result from say IV s going alive and from having you know, manyproopostak walk chains online, a people actually using them. There's you knowprobably whole new business models. We can't even dream of yet that Ari toAmerge, so you know we're still, anticipating,potentially you know, pivoting to whatever, whatever merpy that ere ci yea, so it wso incurised to bring back more to the so the term that ou use. I what you'redoing I verification drivin development right like as opposed to Testin in development oryeah, whatever H for a tean out there who was interested in this Um, you knowmaybe they're Ritin, Buch of solidity kind of worried about that situation.O'd like to do I I want limited to slee utthat'sli where I live is, is mostlythe thing go, SMA, congecery, so sure ou ow. What what would they have to doto move from, hopefully they're doing...
...test wit in development already, maybethey've brinted. If they're motivated to Tomo to terrification, they probablyhave written good plan respects Um. What do they need to do to think aboutimpo, both culturally, as well as Um n, W, tactically processed wise ton,etcetera yeah? So so we've been we've Ben much less focus on you, O things like smart contract. I Arely sequential sequential programs right and there actually is already arich ecosystem of formal varification tools or things like solidity right. Soyou know the runhim vocation folks, have this k framework, its very nicepramework for t model Theyspecibi the EDM completelyin case, so you can now. You know, verify solidity contracts. Now Ihaven't, I haven't played with K myself. I know a lot of people engage, runtimeverification to bearby their contracts, and so that's something that you knowyou could you could be trying to do more ahead of time. The real the real,like you know thing about varification Di Development. Is that Varvocationisn't an afterthought? It's not like. First, you try to implement yourcontract as Bessyou can and then you try to verify it right. It's more likethe concerns of verification, the need to think how am I going to verify thiscode is actually you know part of the architectural discussion part of howyou how you write the Code Ho how you design things right- and you know, testdecripmant development- is very similar in that way. You want to architect thecodes that you can actually so you can actually write tests, butyou know test your an development like people are like. Okay. First, you writethe failing test, you know and then you inplement the code until the Teest Hassright and a lot of people have readly. So you know problems with that approachand I think the the main takeaway from tesscravent development isn't that youknow you have to sort of follow this letter of the law. First, you write thefailing test kind, O scenario, but more that the way you design the code. Youought to consider testing as you go and if you design an implement, you knowcode and is not testable. You know, then that's a problem and you can'tjust like figure out testing after the bact right- and I think so you know thevarification diven development is very similar that you sort of as you'rewriting the code. You need to be thinking about how it's going to beverified and what kind of things you might do. That might make a difficultto verify. You know, and it's a lot o there's a lot of commonality in termsof like you know, good practices, you know, like obviously having you knowmore functional code and ow less glocal variables. You know, good, clean abstraction andstuff like that is al, is all that's going to help make it make it more verifiable. But you knowother things like really limiting the amout of cancurrency you have andhaving like, really well justified, Um concurrency that you really need ityou're, not just like you know, for instance, fin in gold routines reallynoy just because he can. You know things like that. So, honestly, morerecently, as I was saying, sort of you know initially Yo re like well. First,you write your specks an then you're rit your code, and so therefore we havethis lie. Verification Group of development recently we've beenthinking about actually fhipping the thing and talking about development deArification, and that's also really interesting,because a lot of like varification work, especially in academic AAn, whateverright, though, just like you, know, here's my new verification techniqueand you know my new protocol and you now Goin to verify this thing and whocares if you can implement it, because I'm just like trying to get a papersubmitted about any varification tec, and so really thinking about you knowflipping that prom on his head and thie. How do we also do the verification workto maximize its relevance for Development, and you K W so really think taking bothof those Nan, varication, Gimen, evelop and development dafication is we'retaking them together is sort of the latest state of ourthinking on what that looks like so a couple of months ago, we published thislike very short dd guide, which was just like a current state of ourthoughts on at where we have these like multiple layers of specification, andnow you know who writes what and how it translates it to code and we sort ofrealized. It was a little bit a little bit too much apfrontid. You know wehaven't really updated exent, but we're learning a lot by trying to apply it aswe're writing this Ross Code and as we're kind of formalizing, thethecasmol Porto calls, and hopefully...
We'ill continue to update that you knowlater in the year, with more of our learnings and yeah. So this entire process of I I feel like a lot of the the majorreason why people don't formarly verify their codeas one it takes a long time and to it's its costy like there are't tla once you know it, you know it, butit's not easy to get into and it takes a while. There's not that many like it's a completely different paradisethan write and code a d. You have to learn something completely different.Has It so I guess the question is: Has it been valuable for you has? HasYour fieces been proven to be right in that you found sulfur bugs which haveproven that taking this time and spending these resources on this hasbeen worthin so artually? Yes, partially? Not So yes,because like forcing ourselves to actually be able to specify somethingin Tla forces us to really clarify Um, to clarify the protocols. Andto reallylike you know, disindiguate things and that actually, even just the process ofthe specification has has led US tobub, so even even notthey've, not even Benverihike, just just trying to specify the thing hasmade us realize. Oh actually, there's a Bu Heter's Bu there and that's happeneda few times so fron that perspective th, you kow, trying to get the thing intoTla has been, I think, very valuable in uncovering bugs where w things, I guesshave been less valuable is where we sort of m. You know over Emphasi, as onlike trying to figure out this PDD process upfront and really putting allthis effort into. Like writing. A bunch of you know different layers of Englishspecifications and you know sort of trying to turn it into a little bit ofa waterfall mated. You know that stuff has maybe not born as much fruit as wethought initially and that's why I was sort of gone back into you knowfocusing on development. You know this like development, Dron, varificationSto, but definitely having these deal like pospects has, has helped uncover a lot and we'reexpecting the value to compound, especially as we get into the modelbased testing, because once you have a speck, not only did it help clarifyyour thinking and might make it easier. You know to go and animplement eprotocol, but you now actually have a model that you can generate Testrom,which might help you find even morebogs, even independent of the varificationwork. HIC varication can oos not far FYING. Your Cote is verifying yourmodel, so we still, I still don't think wehave. We have found bugs through barification that we didn't alreadyrealize through the spestification processes like humans, thinkingediow,we're kind of keeping like a running. Calli of you know. Human versus model,Checker, Um and the humans are are still doingpretty good, but in all fairness, we're spending a lot more time, thinkingabout it than the Molchacke er spending running, so there thre's kind of that.But definitely you know the TLA is forcing us to really think about. Youknow formalizing and disanbiguating and that's been really helpful and I wouldsay it's more accessible than you think like it does require a little bit of achange in Paradim, because it's not a programming language and you can'tthink of it like a programming language, it's a it's, a mathematics, languageand you sa you're, like you know, you're you're laying out you know theset, like you know, n an logic essentially like what the state of thesystem is or could be rather than like imperatively. You know how you makechanges to to a state, it's more like these are the possible states and so that that takes a little bit of of a Paradin shift to do. But you knowit's not that hard to actually start using it directly. What is hard is actuallydoing the model check so actually...
...specifying the properties that you wantto check, and actually you know, justing your specification so that itactually can be checked by the existing tools requires like a lot of tricks and that's where you know th t that'swhere W we developed Abouttho special season where we expect we can help alot of other people, but you know actually just using Tlaitself, I think, is very accessible and can bring a lot of value, evenindependent of the model check and so yeah t T. it's been really interestingto see that see how just trying to write the thing in Tla has really helpsclarify the thinking and correct, and you know find some bugs just byinthrouet yeah from my experience of working withTla as like Um. First, you build or if you build thesoltware before it looks in subway, and then I n in Tla you by thinking aboutit so much. You learn how to simpliefy, because you have to build it in thisrather constrained o formal language, where it Neetsisto essentially be astate machine, Yeh and Han. So you, you essentially break AP on your entire.Whatever you were building anturned into a really really simplified statemachine where you can kind of throw away all the shape, you don't need andlay your stuff on pop of it, which I, which I think is superhelpful already,but I guess one of the reasons why um it may have not been so valuable yet isbecause, as he previously mentioned, this bridge between software andyouspect may still be too far to actually find funs. I I feel like once these tools aredeveloping, like your rustoos etcetera, that you could directly verify yourrespect against your coat that that output for that Um, I don't knowthat cost verses. Ganeratio becomes far higher than it currently can be. Yeah I mean dependswhat yo o a right. If you're you're saying formerly there by code or Fout,then Orfeel Ike Thato t going to help you, because it's not for ve ir. I Wat.I een O clerfy you're thinking about your Hor ar to the etent that it's acommunication cool to help. Other people understand what the curten Isenimplementing in a way that maybe more it coan be more clear than the Englishto besent that it or Fer utimery tymplefy what is happening and thatCanbe backround your cod and revolving your cerky and more maintainable and Ao,don't understand and that HAC Tach bobd an a protocol sooner by writing andfeel Li boslike. Yes, it seems expensive to do that work up from, butin the long term it seems like it's actually going to save people money intime, hecars bugs that would emerge only in production n from weird edcate,an can't repotate and that might literally cost you a lot of money intime, much less money in time. You probably could have you know sceprifiedand anfound Te funt it her. I e Gali, a so. For instance, Tokwhy Dila hadbecome fopretical, anie AWF yeah. They talk a little bit about this. You knowthey don't talk too much. ECAUSE E, like I actal becom, you know part oftheir Yeepas for what you know how they Bil the liable. O guns is that you knowthey actually besst by things and feel like Bo Fersa e, plerify them and notin Ahu. OFS is not. You know, they're not going to do things that Ar astearyright, like they're operating, Adim, gale and they're incredibly M ch. Toput it simply, I guess you know don't seem like Lavish Beg Efenders, and so, if they're doing something- andthey say you know it's Grot to go- you know it's not something to to to propout and H. Yes, it were e Seeng, more people,rnore adopted and gained value from it. We certainly have been we've been we'vebeen pushing the limits of what you can verify with ye like buss an like someof this. You know thes, like Henement, like plan phtocall that Wele verifyandit's like is crazy. It cannot be done...
...with DL C ot. The Disney model checkersjust will fall over like Al Friht away, but withot alaci really interesting, really interesting, redults out of it.So Um Yeah we've been very excited by what it e Ae to show of and and if theycan give it yo know'e reasong about some of the protocols like, forinstance, you want to knowthat. You know we're looking at her as nowwe're looving at Fort. In eer, I like a enterment quortovallis Notso wor, butif it does Bor, if you want to have thes property that, like you, canfigure out you cou D, The porticals accountable, you can figure out, youknow who done it essentially write it into that. He can punish Tham and Thasistate slashing all this stuff right. And so what you want to know is like exactly what the full set of possiblefaults is, so that you know that you, you have all bault covered, and so youK ow. Only these kinds of faults could cause a fork and nut be punished, justo right and so we've actually managed to at least wot the tenement consensusto write a complete spack and an ivariant that says, if there's a for,it, must have been caused by one of these um by one of these behaviors, andthen we can. You know, turn that into INS, a code who re actually punishingjust those behaviors and any other behavior that might look faulty. Youknow we don't have to worry about it, because we know from the model that itcan't actually cause a Um Covpor. It's interesting that you mentioned aAmazon because from like every tla case Studi, I look into everyone speakshighly positively about it, but it still, ironically, seems hard toconvince people to actually invest the time to good. I guess that's just'cause people are lazy and there's like nota directs, Um objective outcome from it like Ywho F,who fon Bugitla, Mogodi B Elastic Serge Um. I remember reading, like countlessstudies when I was trying to figure out which form Ol varivication languagethere is to look at for especially for distributed systems. Is there any otherlanguage to formerly verify distributed systems? ECAUSE calk isn't really forumdistributed algorithms as much as it is for algethms in general, the samewith Isabel, which is more of a mess, so those are othe provoi right, tee,rcategory of tool or Acetraton Trocka, fanal mathematical, T um of of theprotocol, Thateiti Acterpoerty, nerter, very, very mediculous, and verydifficult to actually. If not it's not like writing of that,because there you're actually building a proop of a sound mathematical groupwhere every single tey take needs to be proven, and you don't get Nthe Talen, Otere, throu em. They don't give you enough ee back at the Doo there. RECARSWO, really know why my prooer n validating what am I Gore riht rirtileis really different. CLA is, is it's a language of mathematic? It especification language. It is not a group Osisa Ri, you don't forget theoutpit of of Tla or given some kind of formal mathematical proof of yourprotocol, thin coud. You know checke Ov as nit exertya. You know aspecification of procentary, a state machine and in what change iseepossible, and then you can write also temporal logic. I A Feeli, ans orCEMPERAL ARBIC onactions. You can write a temporal logic statement that you canthen model ceck with an agotev model, checker that WOILL CECK for everypossible execution of thes state machine icpestify. Do these propertyspoll and that eete by Dagy property, the live, O properties and and Foro,and the really nice thing about morelteckers is if the property doesn'thold. It gives you a counter example ther'r, something that you can expectwith your eye and understand. Oh, I missed this thing because this datewere Pat Woran. This transition was enable TAT repolbl again to this day.So let me go back to my model and update it th. You know he to a Tou forthat pad and its really good at...
...uncovering the edcape right hat wat itee, the Molicacter, a great Bor and making sure that then you, you updateYoure Tanng. So you get this like a really nice steedback loot between you know running the model, CheckerInspecting Tho counter example and opdating Yourspack, in a way that youdon't really get out of the PROV assistance. Now there are other tools,so there's this stolcalled IV, which is sort of a newer dol. U Idis, really cool, because ive is sortof trying to bridge to the gap between model, Checker and poop assistant, andso it's sort of like a proof assistant in that you're building up these groups,but it also it's also a model checker in that you get counter examples as yougo, and so it's really really effective. You get that Nice beedback Goop, butyou also get these croups out of it and the way say Wat to do that. I is it'smy understanding I haven't used it exensily, but that it it constrains the logic you can writeit. So it's a it's like a subset of first gort or logic that it uses that sort of makes everything tractableand it forces you to really think about your specification of your protocols ina different way and you sort of have to operate a little bit more abstractlyand at a higher level. But what you get from that is essentially, like a youknow, pramatrized version of you protoalso with IV. You can get a profand you know model check it or you know consensus protocols with n processesright, whereas when you're rising thing NTA and you try to use the modelChecker, you have to actually fix an ye h to say any equal spool right. And ifyou, if you try to say Anepol said then you know the thing is going to blow upand it's never going to and WITHAPALACI. You know we're starting to get to anybltent. So that's like a major advancement is like now we can actuallymotecheck protocols with ten notes and that's huge, like you know, youcouldn't really do that untl c. But the Nice thing about IV is that it'sactually you can do it. For you know, paramatrize number of processes whichis wothe, powerful and again ivyis under the hood is also Usin. Xetree.Everything seems to be using a three of this ksolver these days, and so itseems like there'r, still a big a lot of space for improvement in these kindsof tools and forbridging. That gap between you know proof, assistant andOllthe, checkers, and so we've been working with we've actually beenworking with Gawa Wih, Giuliano Galua who's been working on. You know,starting a formerly Spescili by various CONSENSIV protocols in IV, and so youknow so we're working on now actually having the same work being done in IV,nd Tla plus, so that we can really compare them, and you know what youlook at. What you get in IV is a lot more high level. It can sort of be hardto see really what the low level details are. What the steps are thatthe protocol is taking depending on depending on what you're best fyingthere, but you get like a more powerful kind of solver as a result Um, whereasin Tla you have sort of a more lower level thing, it's a little bit moreaccessible and easy to work with. But you know it's limited in in the size of the system that he canaltemate lymole check. So there's lots of different trade off depending onwhat what tools ore using in and there's a number of other tools as well.There's other model checkers, there's other Um. There's other systems like the K,frameer WHOC, is more of, like a you, know, expression rewriting systemreally. For my understanding, it's a lot more for like verifying programminglanguages and for you know, compilers and forunderstanding systems implemented particular languages rather than a morgeneral kind of spestification language, even though it can be used for that.But t seems to really have become like Alingua Franca, sopestication language,but I would bet that a lot of t, the you know, probably a lot of the reasonsI have struggle to be adopted is because the user interface is stilllike trade out of the nineties. It's dislike Rarac, Oh God. I hate the TLAthing, O re, the Fuckin Ye Ejoa thingithat, like you kN W. It lookslike you're back in the night and you putcore you Hav in every day I's likehow am I ever Goingna? Not only do I not want o like download eything, Idon't want to run it or look at it. So, like God, Forbid, Um Yean doesn't likeplay well. The recodstructures O lot Ho issues there to witenot a lot o whore,really starn, O focuss on utigility you knwe are going to have to be integratedwith the you know, able to be...
...integrated with a dubos, the Wrovoworking on, like very practical things, like you know, having Gason as a as alanguage for forgetting in and out so theto Don townter example. An a doicenforman easier to re, maybe than the Eteparet feel fe for that, and so theyan actually translate the pree dal like plot and Jacen, for on Avege opect inDasin and writing cool really to make teel lik closes a language moreacceptible and Otelify as a model cecter easier to use in building aefport of you know: Gla Base Raripication Fatmore to we invite you.You know if you're, if we've been thinking about Tla and you G, havingwanted to deal with the Dulbok and owcomfortable Conan line or whateverkilok in Ala, hehuged. U Amflas and poal system flash O A tee ther soballimodel Cheker for Tla and Lookat from the examples there and we have beenusing it on very few world. O systems like a counlike, Cryan and othertenamen tercall Eturni e iian AD, been it be great te Gre in helping USunccover Um. You know interestingcounter examples that were now staring to use for actualTESTN. The worst thing about TLA toolbox. Isthis bug where, when you want to open a file, it's the same thing as creating afile? You just don't name it yet, and then it oopens it magically, and it'sbeen like an issue on their Gethub, for I think three years and they stilldon't fix it and there's Li E. I use it on my mack and there's like theweirdest hucking bugs whenever you try and do something like you save it andit's not actually saved or, like you want to put your confict in a certainco fig file that you can't afpord it properly yeah, there's a vscode extension forthe TLA tool box. That seems quite promising. I haven't used it yet,though, because I haven't been writing any TLA recently W I esed the one by my Microsoft right,yeah sod. So recently I was looking at this Um formalmerrification language which look or like can distributed algoritmverification language that looked quite promising as well, but it wascompletely abandoned. I don't know why? U Ta Ini' quite interesting. I forget thename. I have to look it up again, but but it seemed quite interesting. Ithink he used it to verify various gossip protocols to see if messages actually arrive at.I can send you the name once ive find it again. It's quite interesting that, like we,we've gone really far in how we develop distributed systems, but like thesebase tools, just like have not evolved that much like an Appalachi that youmentioned. That paper was released and was at eleast. There's been a couple of paters overthe years, better ort ther, but like for it to really gatraction took likequite somethitime. I feel like you guys, having like employed the guy, who wrotethe paper in actually giving him the time to help fund tit is what actuallyhelp push push it in this space, which is like Kiand of aw. Considering that theamount of like distributed systems there are versus the amount of like tools, theirart to actually like verify these things yeah. Well I mean it had. It hadmostly been an academic cool right, so yoosly we had EGORONA and fetbitter andwee we're in Diena and have been working together for years. An Co YoborOnewyor, but Um. So they're, like a Supergero del o like distributed tosome ferication, and these guys have been for years now, really reallypushing the bar few other collaborators, of course, on formally verifying dusnessing, FaltHolerin onemte system, and they didn't sort of German tools for doing that,and really like fleshing out abtractions and different ways ofsteaking about the protocols and make them more verifiable. And we, you knowthe Mans. The main infight was really...
...that you know wes probl, Wervariocation, because we're always krying to like come up withvarification tools. In like this Mose General Pap right but Evan actuallyknow by informing the varification by the Dorin, you can actually make it alot more progress right. So when you're thinking about verification as like a aproblem in general, like how do I form a Varhih, arbitrary protocols, you knowith like it's intractible eentially, but when you, when you sort ofconstrain the kinds of protocols you're thinking about and you can inform theactual varification technique by you- know, actions into domain nunderstanding of the Gomaine. You can make a lot more progressing. An yolhavehad a lot of you know: whowas visually, an expert and distibute D, hysdom o allpowerane Egore was more from the varications ID e sort of came together, but really makes ure get thevarification to be informed by to Detue, distributed cystem of knowledge and outof that they've developed. You know a lot of really interesting technique orformerly verifying business. Ebal powers is to that have resulted infutuals one being Palachi, which is you know, Palageis more sombolic macheckerfor Ta plus, but we're actually really using it. For businesing Bo power.Protocol Ha been often, but they also have M Bysineste Model CACTER, separate e Sefer Tul, for you know, representingbusiness e B, heard all is like Breshol ECOMETA and then monotracti nerve and that CN also been yoferring to feefon, the doctor, but y. He a really HAC. They theyere really academic cools, andit wasn't until you know we almost fun out and ehired than bore and someone else could really work Y, afull time. Liteta was prefering to bring it to an actural industrial toolthat people can use D and concent to rely on n at work ting to rely oniternally and and nothing great and egardy. You know the fact that we'realready starting to use it to generate PASK foreal ingimentation. I think thatis all really exfited. So Ye would lot Yor lest nurse Coul tryit out and get afeeback oen choose bi bugs? U You know afer after fetures, let us know wantout of it: IFIT'rworking for you and hopfully you'll find PLA asaccessible a we're, making an B and the Revalu to your organazation. So so what are some other projects? Youguys are? Looking at lute, maybe there's stuff beyond Cick, though, oreven like other block chains. That are interesting that you guys want to workon wit's with some of the other work you are looking at. So I mean, like I mentioned, we're lookinga little bit at like Organizational Pool Um the we sort of put that a Liviton the backcurner again so that we in Oa Dan on on ibfe right now s made abig push to you know. Caushous is going through this major upgrade right nowand ISS expected to launch. You know, sometime in the next few months andAndso we're trying to we're trying to really help prepare for that, but we have been sort of looking outthere at other discributed systems. There's a lot of open source databases,and, like you mentioned, a number of them have had some successevs with Tlaplus and so Wewu'd love to help those those projects that are specify thertheir protocols and understand whate guarintees. They get out of them alsothe Jefson tool, which has been sort of a industry standard to for likeblackbox testing of your distributed system, and you know flexing likevarious adversarial, never conditions and so on. Nothing fine, Bu find bugsin like everytting, so no one is safe from Jefson. So we did. We did someDepton zest on Tenermant a couple of years ago and actually, you know, came out relatively onscaffthere. You know they found some really silly issues in like single node datapersistence, but as far as like the contensus itself Y, it didn't manage toreally violate any of any of the guarantees there and so we're thinking about ways thatwe might be able to sort of combine. You Know Tla models and Jepson drulingand see if er ways to have more for the...
...targeted, targeted attacks Jep to thiskind of blackbox toolies or throw it at it, Roe out your system and it justsort of randomly Tryd de things and in search for violations. But maybe thereare ways for it to be a little bit more targeted and somehow possibly informedby by a formal mottel of the system. It'sactually testing, and so I just idea we've sort of been dadding around. Wehaven't really tried to do anything there, but really a lot of our focus has been onon IV, C and caof right now and n other block change, other blacking bcause enI potacalls and then starting to look at formalizing those we haven't reallybroken outside the block change base yet, but I was certainly open to thatso um, any anyone who's really. You know, building a distributn systemprotocal and looking for you know to increase that. A confidencein in its correctnesses is something we're open to to help and Workh andeven like you know, we putting together some PA, plass work shops and you knowsomesome training on how to use t the tools D had of varify systems within tolong. So hopefully that stuff will offer. You know once we get throughthis IV C: Push I'd bi person, Hey love to do AdelaborChupford to participate in one Sorryo, so we've just ABOUTF wrapped up anentire hour that went by pretty fast yere. Are there any more questions?Marillian from your side, I mean nothing. That's not Gan justextend this by another twenty minutes, so I think I'll I'll. Let it rest there. Okay, alsome! Well thanks ethink forhaving you on Alwas a super interest in conversation. I super excited to see what you guys doin the few FSURE and hopefully I'll be able to participate in one of yourTeele orchelf soon, and we Weran Peopl, learn more about you and and find youonline and Alwe. Are epomabout system? Is a website Ron, qhitter, fomovat andor GA hup e hug out con a an gon system, ca checkout, our penterment and IBC RUSepubitory there and Luckye there alsit.
In-Stream Audio Search
NEWSearch across all episodes within this podcast