Hashing It Out
Hashing It Out

Episode 87 · 2 years ago

Hashing It Out #87-Informal Systems Ethan Buchman

ABOUT THIS EPISODE

Dean and John interview the CEO of Informal Systems Ethan Buchman. Informal Systems is a company seeking to bring a formal verification process for TLA to the Cosmos/Tendermint network.

Links:Informal Systems

The Bitcoin Podcast Network

Hey guys. This week's episode is brought to you by avalanche. Avalanche solves the biggest challenges facing etheriums, developer and decentralized finance or defy community, that is, velocity, security and time to finality under three seconds on the first decentralized network, resistance to fifty one percent attacks, with complete support for the etherium virtual machine and all of the tools that have fuel defies growth to date, including Meta Mask, web three, dot JS, my ether walllet remix in many more coming avalanche will be at parody with atherium. For Defy developers that want a much faster network without the scaling issues holding them back, get started today, building without limits on avalanche by going to chat dot ava x dot network, that is, chat dot a v X dot network. Thanks. Now entering incast work. Welcome to hashing it out, a podcast where we talked to the tech innovators behind blocked in infrastructure and decentralized networks. We dive into the weed to get at why and how people build this technology and the problems they face along the way. Come listen and learn from the best in the business so you can join their ranks. Welcome back everybody. This is episode eighty seven of hashing it out. I'm dean. I'm here today with my relion. Say what's up? Today we have on our show Ethan Bachmann of informal systems. Hey, Ethan, I'm just gonna let you quickly introduce yourself. Cool. I'm Ethan, most notably co founder of the tenement and Cosmos projects, through various worles over the year, but most over the years, but most recently CEO a new company informal systems that's focused on formal verification work in the blockchain space, specifically on distributed systems, consensus protocols and so on, and implementations in Russ so these days were focusing on the cosmos protocols, implementing a big chunk of the cosmos stack in Rust and doing a lot of formal verification work in Tla cuss okay, so the starter question we always ask everyone when they're on the show is what brought you into Crypto? How did you get started? Well, advanced detected on many podcasts, of course. I guess it could be consistent, but it from foinal paint of the answer. Essentially, I so my background was in biophysics and I was sort of studying the origin of life and specifically how life emerged in a universe that's allegedly always running down, or living systems are these, you know, amazing systems that are kind of emergent and running up, so to speak, and backing around two thousand and thirteen I sort of discovered bitcoin and first kind of ignoredics it and understand it, and then, after spending a little bit more time with it and hearing about it more, it kind of a kind of realized that it seemed like this was the origin of life in the digital medium, and this was like the first time that, you know, we've had all these communication protocols over the Internet, but this was the first time we really had like a real, like emergence coordination protocol built on top of these communication protocols that allowed something to kind of exist that wasn't really possible before, that sort of had a life of its own, and that this could be the foundation for like an explosion of you know socalled digital living systems, and I got really hooked by that and obsessed with sort of applying biophysical intuitions and intuitions about organisms and the nature of life and sustainability and so on into ...

...this domain and I've just been sort of enraptured with that ever since, and I guess I'm a big part of it. Also was at the time it'd sort of been learning about the financial system and and, you know, for the first time paying attention to what, you know, the economic structures in the world 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, in a line machine learning to like biology and whatever, and I sort of realized that, you know, there's enough people working on AI. It's being accelerated. In the current economic conditions, it's not going to be a good thing to have, you know, more intelligent Ai. It's just going to be used for exploitation and oppression. I think that's sort of being borne out and that, you know, what we really need is to is to fix the global economic structure and to have something more bottom up and more sustainable and that, you know, better resembles, you know, the sustainability we have in biological systems, and it seemed like the ideals and technology inherented Bitcoin were sort of the illuminating light on a potential path for how to do that, and so that's sort of went all in on leveraging that kind of technology, consensus systems, cryptography, Game Theory, etc. To, you know, solve these issues in in the global financial system essentially, and been been here ever since. Okay, awesome. So I really like the work of informal systems. I hang out with Shaun quite a bit, well, talk to him a lot. It's always an interesting conversation and whenever I look at the work you guys are doing, I kind of feel like, or I ask myself, why not everyone in this space is like doing this approach that you guys are doing, because it just seems like the right thing to do. What? What brought you into this approach, this method of building these systems? So you know, so we built tenement in go and we didn't do this. And you know that. The problem is with a lot of with a lot of distributed systems, is there's like black magic involved. Like you hear stories of like of like Paxos and how like Paxo systems were implemented and like you have like a credibly small number of people who are capable of like actually making changes to the system and who are depended on for for maintaining the system. And you know, and so we sort of you know, we're in a similar world. The tenement from all our experience of actually building that thing up and the way bugs would emerge was really, you know, concerning that, like you have this like incredibly complex thing and there's only a few people who really understand it deeply. And you know, it's hard to know, can be hard to test and it's hard to know. It's hard to like really convince yourself that the thing is correct and then, especially, it's hard to maintain and to change. So if you want to make modifications, you know it's a big integrated thing and to try to like dive into tenements, consensus package, for instance, and understand what's going on in a way that you could make a change and gain confidence in it was really challenging. And and so and and it's not just about the actually is not even just about the code. It's also the protocols themselves. Right until we're all we're all building out of these new consensus protocols and you know, everyone in their grandmother at this point has a pet consensus protocol and we're all building out like protocols around them. And, you know, like client protocols and like all these defy protocols on top, and it's really hard to, you know, to gain real assurances that the protocols are correct and behave the way you want them to, and then that the implementation is correct and behave the way you want them to. The implementation, you know, really implements the protocol. And so we felt that, based on all all our experience, like building tenorment and difficulty of gaining confidence and making changes, that it really made sense to look at form of verification for distributed systems and to look into ways to actually build more confidence in both the protocols, distributed...

...systems protocols and in their implementations and find ways to keep those things in sync and come up with better processes for, you know, building reliable distributed systems that would be more understandable by more people and more easy, easier to maintain and easier to ensure the correctness of changes. Okay, so so when you say that you write these formal specifications for your protocols, what's the process there? Because I actually had this discussion with Shawn as well, and, like with it the TLA spect for example, you have this spectment. But then how are you certain that the code you're running or the implemented, your rust implementation, is actually a correct implementation of the TLA spect yeah, so that that that's the huge count, right, and that's not something we've totally figured out yet. So you know, people in other formal verification is actually a big field and there's any kind of subcomponents and you know, one problem is that, like the probably isn't enough cross talk, right, and so people who people will do things one way and they won't do things other ways, and you know. So there's a whole there's a whole world of formal larification where that you actually generate the code from the back so you write like you write your code and cock or something, and you you get like a proof that it perfect, like proof of it. Then you actually generate executable code and you're on that code and you never modify it as a human and you know, and then all you have to do is really verify your the compiler there and then you know that okay, night of confidence that your code is correct. But you know, are can we have a number of concerns with that. One is like the the, the what are they called the proof assistants, are are quite fragile and difficult to use and require a lot of expertise and you know, building out these like complete proofs like can cock is actually a very, very, very difficult enterprise and requires like, you know, tremendous expertise, and it's difficult to maintain them if your protocol changes or something. And you know, there's this sense that actually just generating the code also isn't going to be sufficient, because somewhere along the line you're going to want to be able to make changes or adapted or, you know, integrated with with with other components of code that maybe weren't generated by by Cock or whatever, and so it's a little bit fragile 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 where we're or not really focused right now on generating code, and maybe that something will get into for components of the system, but what we're looking at is using the specifications as as a communication tool and as a way to build like really clear, unambiguous understanding of what the protocol should be doing and and then trying to find touch points where we can align the specification and the implementation. So one thing we're doing now is, for instance, a lot of parts of our specification are tag so they have like little labels that say, you know, for a definition or for an invariant that's supposed to hold or something like that, and then we have those we persist those labels in the code as well, so wherever that part of the SPEC is being implemented, we also have that label right and that way, and so trying to build sort of hooks between the Speck in the implementations you can sort of jump back and forth and sort of see directly, you know, that this this code implements this piece. So that's that's one thing. And obviously you know that this isn't perfect, it's not good, it's not formally verified code per say, of course, but you know, we're trying. What we're trying to do is really build practical techniques that are going to be accessible, that anyone can adopt without making, you know, major changes to their technology or to their stack or their way of doing things that allow them to, you know, incrementally adopt more correctness oriented practices. And so we're trying to build some tooling around sort of tracking these tags between spects and implementation, you know, and seeing, okay, you have all these tags in your SPEC are they all laid out in your implementation? Is something missing, and then maybe making it easier to jump back between to or maybe building tools to show here's what the definition is in the spect here's what the code is in the implementation. You know, now just inspect them as a human and just, you know, facilitate human review. Another thing where we've started looking...

...at, which the thing is actually pretty exciting, is generating tests. So it might be you know, Generating Implementation, fullblown implementations is a little bit dauncing is maybe a little bit fragile, but generating test is is maybe again, more accessible and you can write the implementation the way you want and then you have this like testing interface and if your if your speck is written in a way that really captures what the code should be doing, then you and you're using a model checker like like we do with the La plus, then you can actually get counter examples out of the model checker that are like traces, you know, of like a bad case and not optimistic case, something where like, you know, something went wrong, for instance right. And so then if you can translate that into something that can be run actually against the implementation, then you have a much potentially much more efficient way of generating these like pathological cases to test your implementation against. Right and again, it's not. It doesn't mean you have formally verified code in the way that you know the code that would run on, say, a spaceship or in certain other like critical appliances is going to be, you know, generated once and then never touched again, for instance, but it does help build greater confidence that the implementation is actually correct because it's able to correctly execute these test cases generated from a model checker. And you know, model checkers are very, very good at finding the edge cases right because a lot of the a lot of the protocols we're dealing with, you, especially when you're dealing with like distributed systems and can currency, there's so many interleavings, so many ways the execution could happen, that it's really difficult to reason about the edge cases. And often the bugs are in the edge cases and while they may be rare, when they do happen, you know then you're kind of your kind of you know, struggling to figure out what went wrong, and so with a model checker it's a lot easier to actually find those edge cases and find things that maybe you wouldn't have thought about and get a test for them that you can then run against your that you can then run against your implementation. So that's a that's another example of something we're doing with the TLA. Now that's sort of on the TLA front, but we're also starting to look at what else can we do in the code and start looking at actually developing techniques to formally verify the code itself, and that's, you know, more like static analysis tools, extending the rust compiler to be able to check sort of more in variance about the code and so on, and that's all still very exploratory and in a research phase. But you know what were our goal is really too? It isn't so much to have like to be able to put down a stamp and say this is formally verified code. It's more to make tools, a correctness oriented development process is more accessible, and so whatever we can do incrementally to make those kind of things available, that's really where our focus is and we find Tla to be, you know, a quite accessible specification language and if we can build out tools to integrate it with, you know, for seeking a model based testing that seems accessible, these tags things like that, that can just help people, give them sort of hooks to build up their sort of correctness processes. Or is the idea like they really focused on US tooling you mentioned, like other dpy protocols, and is there a vision of this, this cooling being accessible to other languages, or are you focused on rest? For sure? I mean we obviously did like to be as accessible as possible. I mean Tla is is a, you know language, independent specification language, right, and so to the extent that we're building Tila specific tools, that's just making Tla, as a formal specification language, more accessible. And so we've been building a model checker for Tla. It's called APPALACHI. So Tla plus comes with a default model checker called TLC, but TLC is like an explicit model checker. So it enumerates all the states and you know it. It basically on, you know, systems of larger than a few nodes, it runs out of memory or runs at the time, and so you can't really do anything interesting. So I mean no you can't do anything interesting. You know, amazons using it in for systems and production whatever, but there's limits on how much you can verify and so and...

...what kind of behaviors and especially when you're trying to model like Byzantine behavior and, you know, adversarial activity. You know, the states based explodes with a number of possible things that can happen. Right. And so we've been developing Appolachi, which was development for years before informal but is now sort of in house, which is a symbolic model checker for Tla plots. So it maps the TLA specification into a symbolic representation that can then actually be sent over to Zthree, the SMT solver, to do, you know, much much, much more efficient checking of certain properties. So you can get, you know, for some respect you can get orders of magnitude speed up. So something that TLC would take hours to do, apology might be able to do in seconds or minutes, and certain things that Tlc you will never, never, complete, apology can actually complete. So that's that's really exciting and that's successible to anyone, you know, no matter what programming language you're writing. But for the time being we're writing our actual code in rust. We're focused on, you know, currently on the cosmos ecosystem and building out tenement like clients and IBC and ultimately a tenement full mode, and doing all that in rust. And so, given that, you know, we're trying to align our research effort with their development efforts as much as possible, we're focusing on, you know, Verification Tools for us, but we are paying out, you know, for instance, a little bit of attention to go and thinking about ways that we might be able to apply like the model based testing work to the go implementation of Tenement so we can gain assurance that that, you know, both implementations are sort of correct and things like that. But in the longer term, obviously we'd like to expand to two more languages. But, you know, the short term we're focus on rust because that's where development which is so in doing this, let's call it an experiment, of more verified software. Have you guys had to change the way you think about code, because it seems like it's a completely different paradign especially when you're trying to do this model based testing on on rust, on your rust implementation. Like what's been the biggest change from the way you think about code or path thought about code before versus? Well, yeah, so, you know, did you think? Is Our big our thought process has been involving quite a bit on this and you know, we're like rapidly in validating ideas, and so initially we kind of came to it and we're like, okay, the way this works is first you write your speck and but actually one speck isn't enough. You need multiple spects for different layers. So first you write it like a high level of spect for the protocol, you verify that and then you'll write a lower level spack for what the implementation is going to look like, and then you verify that and then you know you can more or less just sort of follow this back and implement the code so it lines up kind of directly. We realize that doesn't work. We probably should have known ahead of time that that was sort of naive and optimistic, and what we're realizing is that really the the specification process and the you know, the development process really do need to go kind of hand in hand and happen together and they heavily inform each other. And the most valuable things we've learned have been from from feedback between the two where where you know that the specification is ongoing, is evolving as we're doing the development. The development's ongoing as we're evolving the specification, and the feedback is really important and thinking about, you know, how to make this, the specification in the verification work really accessible to the engineering team so that they can like take away from the work that was done in the Speck and actually understand what it means for an implementation. And, you know, a lot of a lot of things, a lot of a lot of like understanding of code hasn't really changed that much, to be honest. Is just, you know, it's just a slower going process where you're kind of trying to make sure that you're not just like rushing ahead with the code and that you're sort of involved, you know, entangled more deeply in the in the SPEC process and the verification process, and that researchers are sort of more involved in looking at the code and making sure that the that the design...

...is actually going to make sense from the perspective of the specification and that it will be testable and that, for instance, you'll be able to write something that you'll be able to actually exercise with the with the output's say, from the model, based from the model based testing, and so we've gone back and forth on a few things. I don't know that there's anything any like major takeaway on the code that isn't sort of already, you know, standard, you know good practices for code in terms of how you abstract and how you make sure things are testable and and so on. You guys must have a really special set of developers because, like most developers that you work with, already hate writing any form of documentation. That kind of imagine like a normal developer coming in and being told that before you implement something, you first has to write a speck three times over for yeah, well, you know the researcher. We've a pretty big theme of researcher. I mean that we're we'll get you. Earlier on we were really focused on on the research side of things, and so researchers have been have been contributing heavily, but we really been trying to make sure that, you know, it's an integrated team. It's not like researchers red aspect and then throw it over a wall to the engineers where then supposed to implement it. You know, we're really trying to build that feedback loop. Where do you draw the line between what a researchers and what it developers? This is the great question, because we're trying to eliminate the line. We're trying the actually got rid of, you know, our the the main title that was like research engineer, and you know, anyone who's coming on in a research kind of capacity is expected to be involved in the code. But, you know, we do. You know, a few folks are who are kind of, you know, who are professors in a past life, I guess, before informal and sort of have a much more experience with like, you know, academia and research agendas and really like, you know, formalizing research problems and so on. You know, they're, I guess, a little bit less involved with the code, but even still we're trying to we're trying to keep them, you know, tightly integrated and looking at the code and trying to think about how to ensure the correctness of the code. But I guess the you know, the distinction is really more about out at like time you're spending kind of formalizing the protocol versus time you're spending trying to implement the thing right, and so we have been doing a lot of work really trying to you know, we take we take a lot of things for granted. Is What we're realizing. And it's like, you know, talking about like Tenement, like clients for years and it's like Oh yeah, it's easy, like it's easy, it's the like client. It's trivial. Right, like is so far from trivial when you really try to like actually formalize the model and find out what's going on and had a reason about it and had a reason through it like fully so that you could specify it in, you know, in Tla, get the model checker to really to really check everything. It's a it's a lot. And so, you know, the the are like principal scientists have played a huge role in actually like formalizing the model that this protocol is supposed to operate in and helping everyone's sort of understand that model. And then you know then that that the implementation can move forward. It's step out like a bit higher level just for a moment now I get back into this stuff, but like how big is your team right now and like what is the business model? Yeah, so you know, we're initially set up as like RND services company. So you think about us in the same same spirit as Galoa or runtime verification or trailer bits and, you know, certain like security auditing companies or whatever, but folks that are like offering formal verification work as a service. And so you know, we're open to you know, we're really hoping to help really all the like layer one blockchain companies or projects sort of put their specifications on more formal footing so they can work with us and we'll help you formalize the model and start writing out Kel a plus specifications for it and and verify...

...it. And so it is, at a kind of first order, a services company. Really, what we're trying to figure out a baseline is how to build a sustainable kind of research for and you know, we're hoping that there's we're anticipating that demand for formal verification and this kind of work is going to grow, especially as more and more blockchains are launching and as more, you know, more of our world depends on distributed systems and you know, these open source databases implementing consensus protocols and warning variations on them. So we're sort of betting on that, on that growing market and on offering the the speck bestification and verification work there. But of course we're also a development shop. Until we're open to helping, you know, actually implement things. Until, for instance, you know our current we're currently engaged by the interchain foundation. So we spin out of the interchange foundation in January to big chunk of our team was actually working there before we spin out into informal and so we have a you know, a contract of the interchain foundation and do a bunch of this work for cosmost to formally verify a lot of the protocols and to implement them and rust and and we're certainly open and are starting to talk to some other projects about doing similar work for them, sort of starting small to prove out our capabilities and then growing that work over time. So really for any any layer one project that has a consensus protocol that is kind of new, and that's pretty much all of them. You can think about, you know, Polka dot a, theoryum, topoint no near protocol, Tazos, like you know, Salana Cello, like everyone is kind of developing their own consensus protocol and many of them are actually, you know, they can be seen as variants of tenement. You know, a lot of people start with tenement is like an initial kind of simple, Byzantine Vault on consensus, and then they go from there and expand it whatever direction they want to make it, you know, more efficient or scalable or, you know, whatever kind of change they're looking for, and I think the most of those are probably insufficiently formalized and you know, we would love to help put all those things in a more formal footing and really establish a, you know, clear understanding of what each protocol is and how it works and say how it differs from Tenerment or from others and what properties it satisfies and and actually verify those properties in a inaccessible way. In the longer term, you know, we're certainly interested in in finding a product niche and so, for instance, we expect that there's, you know, there's opportunities around up a Lachi this model checker and maybe ways to you know, to think about some you know open core and you know, selling services around it or, you know, cloud hosted versions or whatever. So we're exploring what potential longer term business models might look like. A product perspective. I'm we're also something I didn't really talk about, but you know, we we state informals mission in terms of verifiability for distributed systems and organizations. So we've been talking a lot about formal verification for distributed system but there's this whole other piece here which is motivated by the same kind of experiences and challenges of running distributed organizations and the same way that distributed systems are hard to build and hard to know they're correct and hard to change and hard to verify and all this, all the same stuff applies to your organization. How do you know your your company is correct? Your book there in Good Order? You know your finances are good, your contracts are organized whatever, like your minute book. All of this is very, very challenging and people end up paying, you know, thousands of on thousands of dollars to accounts and lawyers who can't agree with each other on you know, what the State of the company is or if it's correct. And so we've sort of been looking at that problem is very similar to the problem we're tackling and distributed system space and thinking about tools we can build there for ourselves to make our own you know, improve the correctness of our own organization, but that could also potentially be spun out into other companies. Like not, not just like vals come to mind as sort of like there's actual code. Can verify that. That's like, you know, on organization. It sounds like you're talking about like we actually have an object or symbol that represents the salesperson or...

...something, and that they are, you defined, you that's, and by how they react and from the event happens. And then you like actually verify all this computation. Yeah, I mean you can go you know this, this thing can get pretty dystopian pretty fast if you take it all the way. But it's not to like, you know, try to exclude the autonomy of like the individual humans who are participating. And the dowbs have really been focused on like, you know, automatic execution of like business processes and and I'm honestly a little bit less concerned with the execution than I am about the state itself. Like what is the actual current state of the corporation and is it correct? Is a compliant? And if you want to make changes, how do you track those changes right? And I feel like the the business of running businesses has so much to learn from open source development and from all the tools that were developed over the last couple decades to facilitate distributed collaboration on code haven't really been brought to bear on distributed collaboration on a business right, and that's things like plain text, things like version control, continuous integration right, all these things that are now second nature to any developer on a github repository that, without it, you know, would be impossible to imagine how we would collaborate on the piece of software. None of that stuff has really been applied to businesses in any meaningful way and everyone's just collaborating on like, you know, g suite and some other set of proprietary products, and it's a, frankly, I find it like a big discussing mess, the way everyone's data is kind of siload and locked up in these proprietary systems and you know, there's no, it's not open. There aren't I sapis, it's hard to digest in other formats and so on, and so I really think what's missing is like a a sort of get style approach to to running your businesses with, yeah, like I said, having more of the data in plain text in in version control so you can track the changes and we continuous integration so you can like have checks. That's like, Oh, I wanted to make a change to my company. Did I do it all correctly? Like I, you know, I drafted a contract. Is it all correct right? Like it could actually verify all the components that, you know, based on whatever, the same thing we do with codes. I think there's a huge opportunity to actually manage our businesses the way we manage our software and that's something we've been investigating and living at ways and you know, are our hypothesis is like look, if we can figure out how to build more correct software more efficiently and more correct organizations more efficiently, than we can combine those two to build correct software organizations and maybe have, in the longer term, something like an incubator that, you know, spins out companies. Were a lot of like the overhead is kind of advertized through the verification tools and the organization tools, but those are those are the dreams. In the short term, we really focused on on like Cosmos and, you know, the in block chain, in dropperability and and the you know, explosion of opportunity that will result from, say, IBC going live and from having, you know, many provostate blockchains online, people actually using them. There's probably whole new business models we can't even dream up yet. They are going to emerge and so, you know, we're still anticipating potentially, you know, pivoting to whatever, whatever emerging over time. So I'm curious to bring it back more to the so the term that use is, the way you're doing is verifications or in development, right, as opposed to test, drive, in development or yeah, whatever. For a team out there who is interested in this, you know, maybe they're ring a bunch of solidity. Kind of worried about that situation. Would like to do? I want to limit this Lee, but that's kind of like where I live is mostly thinking about smart conrectory. So there. You know, what would they have to do to move from hopefully they're doing tests in development already. Maybe they've written it. If...

...they're motivated to move to verification, they probably have written good playing English spects. What do they need to do to think about both both culturally as well as tactically, process wise, tooling, etc. Yeah, so so we've been we've been much less focused on, you know, things like smart contract which are really sequential, sequential programs, right. And there actually is already a rich ecosystem of formal verification tools for things like solidity, right. So you know the Runtime Verification Folks have this k framework, is a very nice framework for and you know they modeled, they specify the evm completely in k. So you can now, you know, verify solidity contracts. Now, I haven't, I haven't played with K myself. I know a lot of people engage runtime verification to verify their contracts and so that's something that you know, you could, you could be trying to do more ahead of time. The Real, the real, like you know, thing about verification driven development is that verification isn't an afterthought. It's not like first you try to implement your contract as best you can and then you try to verify right. It's more like the concerns of verification, the need to think how am I going to verify this code, is actually part of the architectural discussion, part of how you how you write the code, how you design things right, and you know, test driven development is very similar in that way. You want to architect the codes that you can actually you can actually write tests, but you know, test driven development. Like people are like, okay, first you write the failing test, you know, and then you implement the code until the test passes. Right, and a lot of people have rightly so. You know, problems with that approach and I think the main takeaway from test driven development isn't that, you know, you have to sort of follow this letter of the law. First you write the failing test kind of scenario, but more that the way you design the code, you ought to consider testing as you go and if you design and implement, you know, code and it's not testable, you know, then that's a problem and you can't just like figure out testing after the fact, right, and I think so. You know, the verification driven development is very similar, that you sort of as you're writing the code, you need to be thinking about how it's going to be verified and what kind of things you might do that might make it difficult to verify, you know, and it's a lot of there's a lot of commonality in terms of like, you know, good practices and you know, like obviously having more functional code and less global variables and you know, good clean abstraction and stuff like that. Is All because all that's going to help make it, make it more verifiable. But you know, other things like really limiting the amount of concurrency you have and having like really well justified concurrency that you really need it. You're not just like, you know, for instance, wanting go routines willy nilly just because you can. You know, things like that. So honestly, more recently, as I was saying, you're sort of you know, initially we're like, well, first you write your spects and then you write your code and you know. So we therefore we have this like Verification Group and development. Recently we've been thinking about actually flipping the thing and talking about development during verification, and that's also really interesting, because a lot of like verification work, especially in academy and whatever. Right they'll just like, you know, here's my new verification technique and you know my new protocol and I'm going to verify this thing and who cares if you can implement it, because I'm just like trying to get a paper submitted about my new verification texture. And so really thinking about you flipping that problem on his head and think about how do we also do the verification work to maximize its relevance for developments and and you know, so really think taking both of those things, Verification Driven Development and development driven verifications, or taking them together, is sort of the latest state of our thinking on what that looks like. So a couple months ago we publish this like very short bedd guide which was just like a current state of our thoughts on it, where we have these like multiple layers of specification and how who writes what and how it translates it to code, and we sort of realized it was a little bit a little bit too much up front and, you know, we haven't really updated it since, but we're learning a lot by trying to apply it as we're writing this Ross Code and as we're kind of formalizing the the cosmos protocols, and I hopefully will continue to update that, you know,...

...later in the year with more of our learnings. And Yeah, so this entire process of I feel like a lot of the the major reason why people don't formally verify their code is one it takes a long time and to it's it's costly, like there are Tla. Once you know what, you know it, but it's not easy to get into and it takes a while. There's not that many like it's a completely different paradigms than writing code and you have to learn something completely different. Has It? So I guess the question is, has it been valuable for you? Has has your thesis been proven to be right, in that you found software bugs which have proven that taking this time and spending these resources on this has been worth it? So partially yes, partially no. So yes, because like forcing ourselves to actually be able to specify something in Tla forces us to really clarify, to clarify the the protocols and to really like, you know, disambiguate things, and that actually even just the process of the specification has has led us to bug. So even even not there, not even verifying it, just just trying to specify the thing has made us realize though, actually, there's a bug here, there's a bug there, and that's happened a few times. So from that perspective, the trying to get the thing into Tla has been, I think, very valuable in uncovering bugs where were things, I guess, have been less valuable. is where we've sort of, you know, over emphasized on, like trying to figure out this vdd process up front and really putting all this effort into like writing a bunch of, you know, different layers of English specifications and, you know, sort of trying to turn it into a little bit of a waterfall method. You know, that stuff has maybe not born as much fruit as we thought initially, and that's why we've sort of gone back into focusing on art development and you know this like development R and verification stuff. But definitely having these TLA pluspects has has helped uncover a lot and we're expecting the the value to compound, especially as we get into the model based testing, because once you have a spect, not only did help clarify your thinking and might make it easier, you know, to go and and implement the protocol all, but you now actually have a model that you can generate test from, which might help you find even more bugs, even independent of the verification work, because the verification can it's not verifying your code, it's verifying your model. So we still I still don't think we have. We have found bugs through verification that we didn't already realize through the specification process. As like humans thinking about it. So we're kind of keeping like a running tally of, you know, human versus model checker and the humans are still doing pretty good, but in all fairness, we're spending a lot more time thinking about it and the model checker or spending running. So there's there's kind of that, but definitely, you know, the Tla is forcing us to really think about formalizing and disinbiguating and that's been really helpful and I would say it's more accessible than you think. Like it does require a little bit of a change in paradigm because it's not a programming language and you can't think of it like a programming language. It's a it's a mathematics language and you so you're like, you know, you're laying out, you know, the set, like you know in this and logic, essentially like what the state of the system is or could be, rather than like imperatively, you know how you make changes to a state. It's more like these are the possible states, and so that that takes a little bit of a paradigm shift to do. But you know, it's not that hard to actually start using it directly. What is hard is actually doing the model checks, so actually specifying the properties that you want to check and actually, you know,...

...dusting your specification so that it actually can be checked by the existing tools requires like a lot of tricks, and that's where, you know, that's where we developed a bunch of specialties in where we expect we can help a lot of other people. But you know, actually just using TLA itself, I think it's very accessible and can bring a lot of value even independent of the model check. And so, yeah, that's it's been really interesting to see that and to see how just trying to write the thing in Tla has really helps clarify the thinking and correct and, you know, find some bugs just by thinking through it. Yeah, from my experience of working with Tla as the like, first you built, or if you built, the software before, it looks in some way and then in Tla you, by thinking about it so much, you learn how to simplify because you have to build it in this rather constrained formal language where it needs to essentially be a state machine. Yeah, and so and so you you essentially break down on your entire whatever you were building and turn it into a really, really simplified state machine where you can kind of throw away all the shit you don't eat and layer stuff on help of it, which I which I think is super helpful already. But I guess one of the reasons why it may have not been so valuable yet is because, as you previously mentioned, this bridge between software and respect may still be too far to actually find funds. I feel like once these tools start developing, like your rust tools, etc, that you could directly verify your speck against your code, that that output or that I know that cost verses gain ratio becomes far higher than it currently can be. Yeah, I mean it depends what you storable. Right. If you're if you're saying formally verify code or buff, then I feel like that it is going to help you, because it's not formal there. Yeah, right, but to the extent and how to clarify you're thinking about your code, to the extent that it a communication tool to help other people understand what the code is even implementing in a way that maybe more it can be more clear than the English to the extent that it or for you to really simplify what is happening and that can feed back on your code and result in your code being more maintainable and easy to understand and that catch you can catch bugs in the protocol sooner by writing. And feel like buff like, yes, it seems expensive to do that work up front, but in the long term it seems like it's actually going to save people money in time, because bugs that would emerge only in production, in some weird edge base that you can't replicate and that might literally cost you a lot of money in time, with much less money in time, you probably could have, you know, specified and found front. So, for instance, that's why I feel as critical inside AWF. You know, they talk a little bit about this. You don't. You don't talk too much, because seems like it's actually become part of their secret cost for what you know how they build reliable systems is that, you know, they actually best by things and feel like lust person really clarify them, and that has been a huge you know, and interviews is not they're not going to do things that are necessary right, like they're operating at scale and they're incredibly cheap, to put it simply, I guess you know they're not. Don't seem like lavish the expenders. And so if they're doing something and they say, you know, it's critical, you know it's not something to stop that. And Yeah, so we're seeing more people starting to adopted and gain value from it, and we certainly have been. We've been, we've been pushing the limits of what you can verify with Thela plus and like some of the you know this, like Tenement, like client protocol that were verifying. It's like it's crazy. It cannot be done with Plc. So these...

...disting model checker just will fall over like almo right away, but without a latchy really interesting, really interesting results out of it. So, yeah, we've been very excited by what would's been able to show us and it can give it, you know, reason about some of the protocols like, for instance. You want to know that. You know we're looking at for instance, now we're looking at forks intendant, right, like you tenderments courtacol is, Notticle court. But if it does, for if you want to have this proper, be that like you can figure out, you get the protocols accountable, you can figure out you know who done it, essentially right in so that you can punish them. And that's prop stake slashing all this stuff right. And so what you want to know is, like exactly what the full set of possible faults is so that you know that you have all faults covered, and so you know only these kinds of faults could cause a fork and thus be punish just those right. And so we've actually managed to at least the tenement consensus, to write a complete speck and an invariant that says, if there's a fork, it must have been caused by one of these, by one of these behaviors, and then we can turn that into into code for actually punishing just those behaviors and any other behavior that might look faulty. You know, we don't have to worry about it because we know from the model that it can't actually cause a cause of form. Yeah, it's interesting that you mentioned Amazon because from like every Tla case study that you look into, everyone speaks highly positively about it, but it's still, ironically, seems hard to convince people to actually invest the time to do it. I guess that's just because people are lazy and there's like not a direct objective outcome from it, like, yeah, who found who found bugs? With Tla, Mongol DD elastic search, I remember up reading like countless studies when I was trying to figure out which formal verification language there is to look up for, especially for distributed systems. Is there any other language to formally verify distributed systems? Because Colk isn't really for distributed algorithms as much as it is for Algorithms in general. The same with Isabelle, which is more of a mess. So those are for those are proof of systems, right. Yeah, they're sort of a category of pool where you're actually trying to construct a formal mathematical proof of the protocol that a certain properties, and they are very, very meticulous and very difficult to actually it's not. It's not like writing affect, because there you're actually building a proof of a sound mathematical proof where every single step you take need to be proven and you don't get, you know, the challenge with the through of they don't give you enough feedback as you're doing there's hard to really know why my proof is invalidating. What am I doing wrong? Right, we're Rela. Is Really Different, is it? Hela? Is A is. It's a language of mathematics, it's a specification language. Is Not a proop of system. Right, you don't get the output of a Hela or isn't some kind of formal mathematical proof of your protocol that you could you know, check it all because like it's a it's a you know, a specification of essentially a state machine and you know what changes are possible and then you can write also temporal logic to feel like dance, where temporal logic of actions. You can write a temporal logic statement that you can then model check with an exhausted model checker that will check for every possible execution of the state machine. I'mpecified. Do these property hold and that and then confessed by fifty properties and liveness properties and sort of. And the really nice thing about model checkers is if the property doesn't hold, it gives you a counter example for something that you can expect if your eye and understand. Oh, I missed this thing because this date was pought. was in it, this transition was enabled, it was possible getting to this day. So let me go back to my model and update it, you know, to account for that cave. And it's really good at uncovering the edge case.

Right. That's what it that the model checkers are great for and making sure that then you update your staying so you get this like really nice feedback loop between, you know, running the model checker inspecting the counter examples and updating your spect in a way that you don't really get out of the proof assistance. Now there are other tools. So there's this tool called Ivy, which is sort of a newer tool. IV is really cool because ivy is sort of trying to bridge the gap between model Checker and proof assistant, and so it's sort of like a proof assistant in that you're building up these proofs, but it also it's also a model checker in that you get counter examples as you go and so it's really, really effective. You get that Nice feedback loop, but you also get these proofs out of it. And the way it's able to do that is, it's my understanding, I haven't used it extensibly, but is that its it constrains the logic you can write it. So it's a it's like a subset of first order logic are that it uses. That sort of makes everything tractable and it forces you to really think about your specification of your protocols in a different way and you sort of have to operate a little bit more abstractly and at a higher level. But what you get from that is essentially like a parametrized version of you protocol. So with IV you can get a proof and, you know, model check it for, you know, consensus protocols with n processes right, whereas when you write something in Tla you try to use the model check, you have to actually fix and you have to say an equal spore, right, and if you if you try to say an equal seven, you know the thing is going to blow up and it's never going to end. With Appalachi, you know, we're starting to get to an equals ten. So that's like a major advancement. Is like now we can actually model check protocols with ten notes and that's huge. Like, you know, you couldn't really do that in Tlc, but the Nice thing about Iv is that it's actually you can do it for, you know, parametrized number of processes, which is really powerful. And again, IV is under the hood is also using set three. Everything seems to be using that three, this he solver these days, and so it seems like they're still a big a lot of space for improvement in these kinds of tools and for bridging that gap be between, you know, proof assistance and model checkers, and so we've been working with we've actually been working with galowaw with Giuliano a Gal Wah, who's been working on, you know, starting to formally specify various consensus protocols in IV and so you know. So we're working on now actually having the same work being done in IV and Tla plus so that we can really compare them. And you know, what you look at, what you get an IV is a lot more high level. It can sort of be hard to see really what the low level details are with the steps are that the protocol is taking, depending on depending on what you're specifying there. But you get like a more powerful kind of solver as a result, and whereas in Tla you have sort of a more lower level thing. It's a little bit more accessible and easy to work with, but you know, it's limited in in the size of the system that you can ultimately model check. So there's lots of different trade off depending on what what tools to using. And and there's a number of other tools as well. There's other model checkers, there's other there's other systems like the Kframer, which is more of like a you know, expression rewriting system really, for in my understanding it's a lot more for like verifying programming languages and for, you know, compilers and for understanding systems implemented in particular languages, rather than a more general kind of specification language, even though it can be used for that. But Tla seems to really have become like a lingual front specification language. But I would bet that a lot of the you know, probably a lot of the reason to La a struggled to be adopted is because the user interface is still like straight out of the S. it's this like yeah, that, Oh God, I hate the Tla thing. Who feel like Hul the fucking yeah, the job of thing that like, you know, it looks like you're back in the nine be or you had. Everything is like how am I ever going to not only do I not want to like download this thing, I don't want to run it or look at it. So, like, God forbid, it doesn't like play well with directory structure. So about the issues there? So, without a lot you were really starting to focus on usability. You know, we are going to have it be integrated with the able to be integrated with the LA tool box, but we're...

...also working on like very practical things like, you know, having Jason as a as a language, for getting in and out so that you can don't counter example and reason format that's easier to read maybe than the eth peric feel fee format, and so that you can actually translate between feel like clos and Jason. So you want to have your effect Jason and writing tools really to make Tel like cloths of the language, more accessible. And Up Aldea is a model checker easier to use and building at that sort of, you know, Fela based Verification Platform. So we invite you. You know, if you're if you've been thinking about La and you st of haven't wanted to deal with the toolbox and or comfortable with the to them line or whatever, you look it up a lot. Key. You have the calm flash and formal systems flash a couple of team symbolic model checker for Tla, and look at from the examples there. And we have been using it on very few world systems like a kind of like client and other tenement protocols, and you're starting to use it right and it's been it's been great and it's really been helping us on cover, you know, interesting counter examples that we're now starting to use for actual testing. The worst thing about Tel a toolbox is this book where when you want to open the file, it's the same thing as creating a file. You just don't name it yet and then it opens it magically. And it's been like an issue on their GITHUB for I think three years and they still don't fix it. And there's like I use it on my Mac and there's like the weirdest fucking bugs whenever you try and do something, like you save it and it's not actually saved, or like you want to put your config in a certain config file but you can't afford it properly. Yeah, there's a vs code extension for the Tla toolbox that seems quite promising. I haven't used it yet, though, because I haven't been writing any TLA recently. Well, I've used the one by by Microsoft, right. Yeah, so recently I was looking at this formal verification language which look or like cold distribute it algorithm verification language. That look quite promising as well, but it was completely abandoned it. Don't know why. That one's quite interesting. I forget the name. I have to look it up again, but it seemed quite interesting. So I think he used it to verify various gossip protocols to see if message is actually arrived, I can send you the name once I find it again. It's quite interesting that like we've gone really far in how we develop distributed systems, but like these base tools just like have not evolved that much. Like Appalachi that you mentioned, that paper was released. Was that released? They've been a couple papers over the years better, but like for it to really gain traction took like quite some time. I feel like you guys, having like employed the guy who wrote the paper and actually giving him the time to help fund that this would actually help push push it in this space, which is like kind of kind of all considering that the amount of like distributed systems there are versus the amount of like tools there are to actually like verify these things. Yeah, well, I mean it had. It had mostly been an academic tool, right, so they were. Yeah, basically we you go a con art and your flitter. We're Indiana and have been working together for years. We called the Yogore. You you are, but they're like a superhero duo of like distributed system verification, and these guys have been for years now really really pushing the bar. A few other collaborators, of course, on formally verifying Disney team, fall cooller and contensive system and they didn't sort of building tools for doing that and really like fleshing out abstractions and different ways of thinking about the protocol and make them more verifiable. And really, you know, the main the main insight was really that, you know, we struggled with verification because they're always trying to...

...like come up with verification tool in like this most general paine right, but you can actually yeah, I informing the verification by the don't mean you can actually make a lot more progress. Right. So, when you're thinking about verification as like a the problem in general, like how do I formally verify arbitrary protocols, you know, it's like it's intractable, essentially. But when you when you sort of constrain the kinds of protocols you're thinking about and you can inform the actual verification technique by actions in the domain and an understanding of the domain, you can make a lot more progress. And so you also had a lot of you know, he was a basically an expert in distributed systems and Welt power and and Ecore, with more from the verification side, and they sort of came together to really make sure get the verification to be informed by the districted distributed systems knowledge and out of that they've developed, you know, a lot of really interesting techniques for formally verifying business in volt power systems. That have resulted in a few tools, one being Appalachi, which is, you know, apology is more to symbolic model checker for Ta plus, but we're actually really using it for Busintinae folt power and protocols is Ben ofwesome. But they also have the businestine model Checker, which is a separate a separate tool for you representing business de Vaults are protocols is like freshold of the DRAMATA and then model checking those and and that's also been staring to see some adoptors. But you know, those are really active, they are really academic tools and it wasn't until, you know, informal fun out and we hire to Yougore and you know, someone else could really work full time on a Pilachy that was starting to bring it to an actual industrial tool that people can use and start to a lot I on and that work and rely on internally and nothing great and it's already know the back that we're already starting to use it to generate test for real implementations. I think has it's all really excited. So We'd love your listeners to try it out and give as feedback, open issues, while bugs, you know, after after features. Let us know what you want out of it it's working for you and hopefully you'll find la as a fessible as we're making it out to be and deliver value for your organization. So what are some other projects you guys are looking at? Like maybe there's stuff beyond crypto or even like other block chains that are interesting that you guys want to work on. What's what's some of the other work you're looking at? So I mean, like I mentioned, we're looking a little bit at like organizational pool. We sort of put that a little bit on the back burner again so that we can just focus in on on IBC right now, making a big push to you know, Cosmos is going through this major upgrade right now and IBC is expected to launch, you know, some time in the next few months, and so we're trying to we're trying to really help prepare for that. But we have been sort of looking out there at other distributed systems there's a lot of open source databases and, like you mentioned, a number of them have had some successes with La plus, and so we would love to help those those projects better specify their their protocols and understand will guarantees they get out of them. There's also the the Jepson tool, which has been sort of a industry standard tool for like black box testing of your distributed system and, you know, flexing like various adversarial network conditions and so on, and that thing find but finds bugs in like everything. So no one is safe from Jepson. So we did we did some Jepson tests on tenement a couple years ago and actually came out relatively on scath there. You know, they found some really silly issues in like single node data persistence, but as far as like the consensus itself, you know, it didn't manage to really violate any of the any of the guarantees there. And so we're thinking about ways that we might be able to sort of combine, you know, Tla models and Jepson tooling and see if they're ways to have more sort of targeted targeted attacks jets to this kind of a black...

...box tool. You sort of throw it at it, throw it out your system and it just sort of randomly try to do things and search for violations. But maybe there are ways for it to be a little bit more targeted and somehow possibly informed by by a formal model of the system it's actually testing. And so these are just ideas we sort of batting around. We haven't really tried to do anything there. But really a lot of our focus has been on on BC and cause moos right now, and on other blockchain, other blockchain consented protocols, and starting to look at formalizing those. We haven't really broken outside the blockchain space yet, but we're certainly open to that. So any anyone who's really, you know, building a distributed system protocol and looking for, you know, to increase their confidence and in its correctness is something we're open to to help in with. And even, like you know, we're looking at putting together some t la plus workshops and, you know, some some training on how to use the tools and how to verify systems with it so long. So hopefully that stuff will offer you once we get through this IBC push. I personally love to do the FLA workshop or to participate in one sorry, so we've just about fit wrapped up an entire hour. That went by pretty fast. Yeah, are there any more questions? Morelian from your side? I mean nothing. That's like can just extend this by another twenty minutes, so I think I'll let it rest there. Okay, awesome. Well, thanks, Ethan, for having you on. It was a super interesting conversation. I super excited to see what you guys do in the few future and hopefully I'll be able to participate in one of your TELA which all soon. Off that and working we will learn more about you and find you online and all your what we are informal doctorystem is our website. We're on twitter at informal being and our Github you hubcom black informal system. You can check out our tennerment and IBC rough reposatories there, and alty is there. Yeah, awesome. Thank you, Thay Care. Thanks much.

In-Stream Audio Search

NEW

Search across all episodes within this podcast

Episodes (119)