#238 Dr. Amrit Kumar & Dr. Ilya Sergey: Scilla – A Formal Verification Oriented Contract Language

Transcript

[Music] this episode of epicenter is brought to by kenosis an open platform for businesses to create their own prediction market applications on top of a theorem network they recently launched venosus X a challenge inviting developers to build apps on top of the kenosis platform to learn more go to epicenter of TV slash enosis x hi welcome to epicenter he showed which talks about the technologies projects and people driving the decentralized technology and cryptocurrency revolution my name is

maja Roy and my name is sonia agarwal and today we have with us two guests from the silica project with us they are Amit Kumar who is the co-founder and head of research at silica and Illyria Sergey a assistant professor at the University College London so let's go ahead and start off with some background I'm right if you tell us a little bit about how you got involved with the blocks in space before everything you know hello to everyone and no it's great to be back here so yeah I'm um working with silica right now and before that I was a I did a PhD in temple security & privacy at in Rio and then I came up with to Singapore at National University

of Singapore where I did a postdoc for around a year and when I started to explore blockchains especially from the privacy perspective so that was interested in Manero which probably friendly and privacy enhancing cryptocurrencies and we try to analyze how how much privacy it gives in practice so this is how I got introduced into blockchain and then one day uh my advisor at anywhere so asked me if I was interested in building a scalable collection platform called silica and this is this is how I jumped into silica great and Ilya how about you how did you get involved with the space all right first of all great pleasure to be here it's my first time and I'm about to

enjoy it here alright so my background is in formal methods and programming language series so I did my PhD in Cattolica University of Louisville that's in Belgium and then I was a postdoc in in their software Institute and then I took this position as an assistant professor or lecturer is the coeds at University College London so since I doing most of my research career I was looking at the properties of programs that as we all know can be buggy as hell and can go wrong so I was looking for ways to prove programs behaving correctly being secured and obeying certain properties applications of blocking technology specifically

around 2015 when etherium started to emerge seems it seems like a super exciting area were lots of research and DL theory and formal methods can be applied so since then I start to look at this thinking about how can we possibly write safe and secure applications that run on top of this distributed architecture what are the properties that we are interested in and find out what other right programming language mechanism to express those sorts of computations and those sorts of properties and this is how we ended up collaborating with silica that I'm currently advising and we jointly are designing and building Scylla as a programming language on top of the

silicon platform awesome cool so I'm ready so you know you guys were on epicenter in the past about I think November of last year so could you tell us a little bit and on that last type of time you told us a lot about the basics of the protocol and I think this is like when you guys are like first getting started could you guys or when you first went public maybe could you guys tell us a little bit more about what are some of the progress and update that has come to silica since the last time you guys are on yeah sure so at that point of time we didn't have Scylla of course you were still working on designing and having a having this idea of what our language to

be so we have progressed in two different directions one is of course on the Scylla site where we have you know we we released our white paper that explains the design rationale and know for Silla in January this year and in parallel we were working on implementing the silica core protocol so we are at a stage where I mean our first estimate has been released that desmos allows you that kind of implements a Bitcoin like infrastructure where you can do payments we have a block Explorer and a web wallet that allows people to interact with the backend blockchain infrastructure you cannot join the network for now but we are going to open

it up very soon so you can become a miner they still have a lot of things to do for instance we have to put gas mechanics and incentive layer that's not there yet but we are actively working on it but in parallel we are working on on Silla together with where we are working on designing and implementing the interpreter and the language spec you know you'll see what kind of primitives the language will provide and support and recently we did a demo a couple of days ago where we demonstrated the first contract that that that that can run on silica that was a crowdfunding contract so yeah things are things are working pretty pretty well and fast outside but there are lots lots lots of things to do

very cool yeah when I actually our first read you guys's paper areas like super excited because I first like you know a lot of people use the work like proof of work and Nakamoto consensus interchangeably and I always used to bring up to people like technically you could do proof of work PFT I've just never seen anyone do it and it was really cool to see that you guys were actually trying to do proof of work PFT so in your current test net do you guys have implemented the sharding mechanism and stuff is that like live yes so we have sharding Rich's life so in the backend when you send transactions those transactions get shortened the network is shortened so it's not like a big

network as in as in Bitcoin or a theme it's it started so we have shorts built up and those shorts process are only a subset of transactions so yes charting is is life that's super cool I mean I personally look forward to joining the test that when you when you go live with it so so this episode is not focused on the sharding mechanism of of silica but rather the smart contract language which is Scylla and like Ilya you've you've worked for a long time on programming language theory and software verification and like scrolling through your past papers I see lots of work with this idea of mechanized proofs and

mechanized proofs will of course play a role later on in the conversation when we discuss Scylla but before we start on Scylla could you give us an idea of what is a mechanic's mechanized proof all right thanks for the question here so before I actually start talking about mechanized force let me erase the question what is a proof and this is rather philosophical so turns out that when we talk about proving something we usually have a certain statement in mind like a sum of two even numbers is even for example that already implies that we have a theory of natural numbers in our head and we know what an even number means and we know how the sum is defined

so all these together are the fact are the other components about which we can make statements and then there is a notion of logic in which we make the statements well most of the humans they have certain sense of logic they know what is true and what is not true but when we actually try to establish that certain statement is true ie it is correct we start invoking the rules of the logic for example we know if a and B are correct then either like both a and B are correct separately so this is like a simple rule that we all have in our heads or we know that if we if a implies B or and we know a then B holds true so all this rules

is something that mathematicians started to formalize and spell out in a mathematical system around the end of the 19th century and this is how the basics of logics have been laid out with many prominent scientists ciphers guru such as George and and many others and then there came the notion of a constructive proof so what are the statements that we can possibly prove well and this largely depends on what the rules we what the what rules we use and what are the what are the axioms so most of us are familiar with axioms of planar geometry such that the two parallel lines never intersect so this is something we take from granted but

there are other things that we don't take from granted we derive from this initial assumptions and we apply those rules ok so now what is the true statement well the true statement actually largely depends on your initial assumptions and on the rules that you use to prove this statement in different logics they come with different set of rules and most of us they have certain version of constructive logic in our head when we know how to combine facts together so we can derive more composite statements and mathematicians make it precise so if we can prove certain statement in a logic of choice then this statement is considered to be a true and if we can approve this data it's considered to be a false so the notion of falsehood is actually the the whole

platter of statements that cannot be proved so now approaching the the idea of mechanized proofs obviously most of us heard of proofs that are wrong a famous example is form as grade theorem that has existed for 300 years and only has been in it's only believed to be proven finally by Andrew Wiles in 1993 so why all the previous attempts were were unsuccessful well because this sequence of rules that mathematicians used to apply or proven the ultimate statement about about the numbers infamous theorem there were some rules which were applied wrongly so some rules which were applied out of place and for example I'll give

you steam so let me tell you that the sum okay so the example I gave before the sum of two even numbers is even this is something that we sort of believe because we know how numbers function but if I tell you that the sum of any two numbers is even well you know that suppose and you know it from experience but if I ask to prove you you will be probably invoking the definition of natural numbers the definition of addition the notion of evenness the notion of oddity and at some point when you try to combine the facts you'll see that you have no rule to deliver this final statement so this means that the proof is inconsistent the proof is wrong and obviously when we write such proof of proofs on papers and the proofs might be about any arbitrary mathematical

object so I use natural numbers as examples but those might be programs or those might be distributed protocols so it is often the case that the proofs contained are wrongly applied rules and this is where the idea of mechanized proof comes to their help so if we can write a proof as a sequence or rather a tree of applications of rules building our rules are the notion of outer notion of to ground up from the axioms by applying more and more and more proofs and maybe reusing the libraries of existing proofs in the way that programmers use the software libraries then we can delegate the task of checking the validity of such proof to a computer and this is what the software known as proof assistance or mechanized

theorem provers are doing they usually do not prove statements automatically that can be done but usually for very simple statements or statements within certain theories that are known to have decidable facts but I'd like the world the boldest comp is very complex and most of the theorems they actually require a human in the loop to construct this proofs and this is why we still have mathematicians and there are not a lot of job because humans are required to construct those proofs but quite frankly humans are not required to check the proofs this is something that the computer can do and if we give the computer the formal system such as the system of natural numbers which is where our objects leave we give the statement

about certain objects from the system and we give the proof of this statement then the software can put all these three things together and check that every single who in this derivation of the proof has been applied correctly and then if it says yes every single rules applied correctly and your axioms are good and the old consistent then you have the notion of mechanically checking proof so that is the proof of the statement that you had here the question is what if your statement is not good enough but that's a separate a separate question but the mechanized proofs is this idea that the computer can actually check certain derivation and that that can be done automatically so uh that's that's really fascinating

right so essentially the way I see it is like any programmer at some level they have data and they are functions and then they use functions to build other functions and then there is like a hierarchy of small functionality that is used to compose something big and mathematics is similar because like some complex statement like the foremast theorem could depend on simpler proofs of other other simpler things which depend on proofs of other simpler things which depends then on axioms that we take for the logic that logical system that we are considering and so whenever in a sense the way I understand a

mechanic's mechanized proof is I could express how I am proving Fermat's Last Theorem as as this cascading set of smaller proof statements give it to a computer and then the computer will verify the whole derivation of the proof and will give high assurance that that proof is correct this is very much correct vision thank you in fact this analogy that you have just distilled with the libraries of functions that the program has used and the textbooks of theorems that the mathematician refer to when they actually prove new theorems this

actually has a name and this is called Kari Javert correspondence or carry forward is Omar's business so Hospital Kari and Howard are the two very famous mathematicians who lived in the 20th century and they noticed this very elegant correspondence between the models of a certain classes of programming languages such as functional programming language so these are models that are now in power languages such as oak mo haskell and some others so and the idea of mathematical proof in the constructive logic so turns out that the statements the mathematicians write they

are very much similar to the types that people give to the programs written and functional language so for example if you have a function that takes an integer and returns a string you can think of it as of an application that takes something that is an integer and they gives you something that is a string so even the symbol is similar so that's an error and that's why this analogy is so powerful and this is why it actually has been very much used in implementation of the PUFA systems that now sort of combine proving and programming so writing a theorem is the very same as writing a type a notation to your function and proving the theorem

is very much similar to implement in this function it's like your programming but your types come before your implementations so in the programming that's usually the other way around so you first write the implementation and you think of the types and in fact it shouldn't come as a big surprise that programmers especially those who are programming languages such as Haskell and oh camel which have very very powerful type system they rigid do some sort of mechanized theorem proving even though they might not realize it so when they make sure that the type program type checks against the types they give so the compiler tries to construct the proof from the program and the types because like the theories there is very

simple so you don't need to have a human in the loop to make this additional third object which is the proof so compiler does that and then the compiler itself checks it so the process of type checking in languages like Haskell or camel is it incorporates to some extent a very simple version of theorem proven and the statement of theorem means that the program satisfies this type and the fact that program satisfies this type means that the program has certain properties and it doesn't go wrong so that's the famous statement so the well typed programs don't go wrong if you cannot send the type to the program it doesn't work so here we already have industrial skills here improvement well type systems they only give you very simple properties such as basic shape of your computations but in

order to prove some more complex properties such as safety and temporal something that we'll probably discuss later for that you need to have a human but yes so to elaborate on what we've said theorems and programs they are actually the two sides of the same coin and sorry the theorem sometimes there are two sides of the same coin and fools two theorems is the same as programs two types so that's carry forwards of course I'd like to actually take an example in order to sort of drive home this point and I mean I like to take an example that sort of derives maybe not derive but is related to one of the papers you

published which is mechanizing blockchain consensus essentially in this paper as I understand it you've you've implemented a distributed consensus algorithm and the blockchain data structure and you you prove that certain properties of this blockchain network will always be met so I'll try to take a simpler example right so when for example I am a blockchain node what I'm essentially doing is I'm hearing of transactions coming in to the blockchain node and these transactions are collected in a memo and then periodically then the software that is running on my node will compile some of

these transactions into a block right and it will try to add that block to the blockchain so there is some some some piece of software that is taking raw transactions and then compiling them into a block and then this block has to be valid right so we might imagine that we want a simple rule the simple rule is when we are when we are doing this process of taking transactions and compiling them into a block we don't want an older transaction which has already been confirmed on the network to be included in this in this block the the transactions ought to be unique that is a property we desire out of a node software and so our node has a previous list of transactions and it saw new

transactions it was now compiled but we as these users of the software want to prove this node running software will never create a block which repeats an older transaction and the way I understand it is like you can prove that a particular implementation that you are using will never make such a mistake using mechanized proves is that right yes this is this is very correct so let me just because this development in the light of the previous of the previous analogy so you have so what we did we actually define a new set of objects objects that represent the implementation of a very very simplistic

block chain consensus protocol and the objects are essentially the execution instructions that each node can invoke locally so this is this is what we can write statements about so the statement that you present we actually didn't prove that because that was sort of embedded by design it as I said the model was simplified in multiple possible ways and because we were focusing on slightly more global properties but the statement would be here are the instructions that the node can execute assuming that it has freedom to execute them in any order and so the whole thing just doesn't crash would it be the invariant that at any point of

time the node doesn't propose a stale transaction where the stable transaction is such that has been already proposed so this is what's called a safety property or an invariant and this is something that we can proof and the proof will will involve case analysis and introspection on the way the semantics for this instructions is defined so your again your objects are these instructions and semantics your statement is this invariant and the proof is something that you can write out of out of the semantics but you see here's here's an interesting point so what we had to do is to build the whole new small theory of blocking protocol implementations that's not granted that's not something that we can just take from an existent

implementation so what we need to do is to embed it into the general mathematical framework that allows to build this proofs and check them mechanically but yes this is possible and in fact we focused on somewhat more global properties so what we proved is an eventual consistency in the form of consensus meaning that if you are a local node and you interact with other nodes then if at some point there is no communication between you and other nodes then you know that all of you share the same knowledge of the ledger in other words you have reached the consensus how did we prove it well we took the rules of the system and we

formulated the property that implies implies this agreement notion so that's that's where so are you guys planning on like formally verifying than your actual blockchain implementation so like I know that the smart contracting system that you guys are creating is designed to be formally verified but so similar to how kaizo says writing their entire code base in okay mo so that they can formally verify the code base itself is this something you guys are looking into doing in the future or even right now okay so let me ask some part of this question to verify the entire infrastructure is a very ambitious

project so they're just like to give you an estimate projects of this scale actually a smaller scale we're fine something like mechanically defining and verifying and a small OS kernel or small compiler for a subset of C this is something that the humanity has conducted and that took literally tens of many years because you really I mean nothing is taken from granted you need to build the whole system ground up in this framework define the semantics of every single primitive every single bit vector operation and whatnot and then prove properties of that and then compositionally build do the proofs of the entire system so we are we are not sure if we are planning to undertake

such an effort right now and furthermore so the fact that something has written a camel doesn't make it immediately verifiable it makes it easier to translate into the language of theorem provers so that's a big help but it's not like a camel lends you some foundational verification results so what we had what we will probably try to start from is extending this work that mahir mentioned that we that we have done on mechanized blocking consensus and formulate the abstract model of Zuleika protocol in these terms so we at least could be sure that foundationally the protocol has no flaws in it that doesn't mean the implementation has no bugs this the

whole different level of complexity and typically it's done in several steps so at the top level you have your abstract specification abstract model when you prove some general properties thereof and then you show that your implementation or at least some parts of it very fine parts of the abstract specification and by means of proving this refinement you show that actually the same properties they are preserved but this this step this is the complex part so proving the refinement is complex and we might be able to do it in the long run for some parts of the protocol but not for not for of it and that's a big thing so as I said nothing is taken for granted all the crypto primitives all the system OS system interaction primitives this is like if you want to have ultimate

guarantees this is also something that needs to be embedded into the proof assistant and established correct and approving cryptographic implementations correct that's a huge endeavor by itself and several labs at in there MIT and India are currently taking on just refine these libraries that implement sha-256 and and similar ones so it would be good they can the ideal world if we could compose all these verifications results together but as always there is there is something there is some friction on the boundary we don't all speak the same interfaces and it's a it's a big it's a big goal so to answer the question I think what is feasible in the medium term around is to purify the

properties of model of silica and this is what we will be probably aiming for but I'm Reed might be able to elaborate on a future agenda I just add one point to it which answer I mean last time I talked about silica so you you you you have a few things in an abstract manner that you're using right when it's proof-of-work so using pbft and then you're using something called collective signing which is essentially if you have n people signing a message you could reduce that to just one signature so the signature size could be reduced from you know linear to constant size so you could even pick those pieces together I mean could you could either proof properties about those pieces individually and then you could try to combine at a abstract level at a very

abstract level but you know as as you just said you know proving properties about the implementation is another is another thing so yeah we will rather go with you know with baby steps and and see how far you can go [Music] this episode of epicenter is brought to you by kenosis enosis is an open platform for businesses to create their own prediction markets on the theory network prediction markets are powerful tools for aggregating information about the expected outcome of future events so this can be used for things like information gathering incentivizing behaviors making governance decisions or even creating insurance products so in order to turn kenosis into the most powerful forecasting tool in the world they recently launched gnosis X it's a

challenge that invites developers to build applications on top of the platform and the best applications per category will be rewarded up to $100,000 in GNO tokens so throughout the year kenosis will announce different categories for the challenge and the current challenge has categories for science in R&D token diligence and blockchain of project integration gnosis also provides the SDK which allows you to easily get started with everything you need to get coding and they also provide dedicated support channels throughout the challenge for teams and solar builders are you up for the challenge guess serve now to learn more and to sign up go to epicenter TV slash canosa's x we like to thank gnosis for their support of epicenter the

connection to the smart contracts here is is different like so when you have a an implementation of a blockchain node that is extremely complex and may be like proving properties of the implementation is is like tens of many years of work but on the other side for smart contracts the program's might be simple enough to be Ameen amenable so that amenable to proofs and the proofs might be useless so for example the instance I was thinking of was there are many people that have these days crypto wealth right lots of crypto wealth and presumably they might want to hand this crypto voice down to the next generation

in the form of a will right and the will can take the form of a smart contract so there's a smart contract I put my silica tokens or ether tokens in it and then when I die somebody puts in a message and then that smart contract so when I'm alive smart contract allows my address to withdraw the tokens from that from that smart contract but when somebody puts a message that I'm dead I'm no more then my then a different address which is controlled by let's say let's say my my child is then able to extract the ether or silica out of the smart contract so as a small program like that a smart

contract is can be really useful and the the place where mechanized proofs perhaps enters this space is if I'm going to commit lots of tokens to this smart contract well I want to know that all of this money will never get stuck in the smart contract that either me or my children will always be able to extract it right and correct that you're focusing on mechanized proofs in the smart contract language due to like these sorts of applications in mind yes so let me answer yes this is a fantastic summary of what we are trying to do so

the properties of smart contracts which we are mostly interested in are this large-scale safety and aliveness property so what you've given as an example is a perfect case of Linus property that informally means that something good eventually happens so something good in these contexts means that a person successors children's or grandchildren you'll be able to cash the check but that might not happen right now that might not take place now and certain conditions need to happen for this for this event to occur and you name this condition like somebody needs to send a send message that the person has passed away and then the successor

should contact with another scientist action what not so that is a great example of specifying this temporal property so what you've just said in plain English can be written in terms of let's say a lifetime execution property of the smart contract so if we have smart contract and the way to make statements about about the way make the statements about how it behaves over its lifetime so what changes does it make over certain conditions where does it transfer money under which condition that happens then we should be able to write this post and this is how this is what we try to build into the design of

Silla so that's the language whose semantics give you this notion of lifetime executions of the contract so you make it can make statements about them and you can phrase the statements in the context of of a proof assistant that already comes with all these foundations of Silla contract execution built in so actually knows the language that you're speaking and then you can use the machinery to write the proofs and the software will check that this process agree so in fact the property like you've mentioned a very similar one we have proven or a model of smart contract and coke which is which is the software or for chicken poops I'll tell more about it later that's the purpose of a kickstarter

contract which says that under certain conditions if you have bagged the campaign if the campaign fails and the goal has not reached and the deadline has passed and you happen to be a backer in the past then in the future you'll be able to withdraw your money and do it exactly one so this is the kind of glamorous profits that you want to establish and we and our language design helps you to do so cool so could you tell us a little bit then about more about what are the broader design goals of Scylla and like so you know one was easy transpose ability to caulk another one I've noticed was a very big focus on preventing reentrant see bugs what are

some of the other major design considerations that went into this okay so let me make a first step and then Amrita can can add more okay so from a general perspective I think it's very important to have a language that allows for formal certificates to be published and made available to people so it's often the case in systems like a theorem that the contract is compiled to bytecode and it's advertised as something that delivers certain surface but essentially the clients interact with it on their own risks so we want to reduce this risk by given a possibility to prove to put formal statements and

prove specifications for both contracts can and cannot do along with their proofs or some digest of the proofs to do the blockchain so this is the concept that has been studied but not in the context of blockchain it was very popular in late 90s was called proof carrying code when a certain code comes with a certain specification and the proof of the specification so now we want to try to do it in practice and the big challenge here is actually to come up with useful specifications so this is something that cannot be done automatically so the contract might be float but so might be the specification so it doesn't expose the flow so the big challenge who actually provide the right illogic abstractions to make statements about the contracts but so far we are

building the language even makes possible to specify properties like never suggested so that is my part of the vision and number it might be able to complement it lists with additional details yeah so when we started out you know we felt that we are building up a new block chain platform and he wanted to have a platform with spark or not features into it but then we feel that the way smart contracts exist today we have certain issues and you need a way to kind of improve upon them and one way was to you know structure the language in a way that it you know you can eliminate certain certain issues that appear at the language level and also to meet the language you know kind of proof friendly

to some accept so it becomes easier for you to to write let's say Co proof so it becomes easier for you to reason about you know the correctness properties or safety or lightness properties about the contract so and that's why you know people you kind of filled out you know these days I need to develop a new language and this is how we started started Silla I see and so you mentioned it's like one of the goals is to provide a platform for user for developers to submit formal proofs along with their code so a couple questions here right so one so does that mean that the language the code that goes on chain is a seller code rather than so like you know you

you got in the paper it's it presents Scylla as this intermediate language so is the idea that it's this intermediate language that will be pushed to the blockchain or is it the lower level language okay so let me take that we were discussing this particular design choice quite a lot and right now the conclusion is that we want to put intermediate level language on the blockchain because we value attract ability or the ability and possibility for formal verification more than the benefits whatever benefits the low level representation brings so I think there is there is a certain bias in the

community seen since the theorem was very very extremely successful as an implementation of a smart contract platform that's a very low level representation should go there because that's probably efficient to store that's efficient to execute but well EDM is not what actually executed per se in most of the theory on clients so it's Judith down to some low level architecture so it could run faster so if we do that we suppose the low-level UVM so why can't we just take a slightly higher level language and compile it as we process the blog that comes down so we are not particularly constrained with efficiency here because there's going to be compiled down to something low level and

practablity is the main concern that's why we are going to put the intermediate level language is Silla if I may just add two to this you know if you look at certain auditing you know tools or services that exists right now if you look at the smart contract that's going on the blocks it's in byte code and then if you want to audit it becomes very difficult you either need to be compile it or DSM bullet or you know figure out a way to to manage it in human terms but if you have if you have an intermediate representation that actually speaks you know the logic that you the contract actually implements it becomes much easier to understand what the contract is actually doing rather than you know putting a byte code on though on the blockchain and then separately

publishing the source code somewhere else so I think it's better I mean of course there are certain trade-offs that you will have to clear all with but to to because we are targeting security I we feel that it's a better idea to actually go with the Silla kind of representation directly on the blockchain yeah I mean this is always one of like the very like weird things I found about our theory I'm where you know on the blockchain all there is is that EVM bytecode and then whenever people want to look at the actual solidity code basically the default is just to go to ether scan and look at the solidity byte code there and you know that's a very like centralized thing that maybe we don't want to like we want something that's more accessible in a decentralized way yeah so actually like

this this sort of brings an imagination in into my head and I'm gonna lay out that imagination to sort of sketch out the vision you what I think the vision you're building towards is so today if I am a smart contract user right and let's say I'm going to use a multi signature contract right and I'm going to put money into this multi signature contract well before putting money into the multi signature contract a power user like me wants to know if that contract is security audited right and I then I'll go to this probably this audit from least Authority or trail of bits or something like that and I'll read the

audit report and then if the auditors say good things have heard the contract then I'll end up committing money to it but somehow somehow in this process I am trusting the judgment of the auditor right Leslie program and the programmer wrote the contract and then the auditor audited it and I am trusting the combination of the judgments of these two people in deciding that this contract is is safe so what you seem to be building towards is like 10 years later it's when I when I see a Multi signature contract I will go to the contract and then link to the contract will be a set of mathematical proofs that my browser can verify mechanically

and these mathematical proofs will ensure that large chunks of the functionality of that multi signature contract are correct from a mathematical proof perspective I do not need to rely on the judgment of a human security auditor in order to be sure that this multi-sig contract is is okay and sort of Scylla is sort of your way of building a language that allows this future to come about that is correct so instead of trusting the human auditor you will be trusting the cold-hearted soulless machine that takes the specification of the contract

and the proof and checks them and I hope it didn't come out bad it's not like we are trying to take out people's job rather build a new generation of Oh new opportunities for job because someone will actually have to write those probes as I said like ultimate like full automation is hardly possible and that requires trained qualified mathematicians and formal method experts to conduct some of those proofs but yeah that's that's essentially is the vision so the Devils in the details when we say correct we usually don't specify correct on which meaning so the most critical part of this thing is actually to come up with right specification and this is something that we don't have the

ultimate ask for for because it's very much domain-specific you came up with the specification for this wheel transfer in contract which was quite good was it the and the complete specification for this contract well I'm not sure I think you'll still need human auditors who will come up with the right specifications so the provers could prove them and then all will be safely put onto the blockchain and the machines could check that the proofs are good but I don't think we are at the stage when the specifications can be derived automatically and this is what we need to do much if I just may add one point to this which is you know if if we open this up at the community level you know you could say that look here is a I mean

this how our security standards came out right you know people came up with an idea as a draft and then you know people started voting for it and then we realize that okay these are the functionalities or specification they desire from from a new your security kind of contract and then you know what you had this all these functions and interfaces that came up so you could you could have something along those lines here as well so you could say that look now that ERC 20 kind of contract has been established the standard has been established now what are the properties that you are actually seeking so you know you could say that I want my money to be you know when I when I make a transfer I want to ensure that the right amount gets transfer or if the mapping is if the ERC 20

contract mean here's a mapping does not mean doesn't get manipulated or you know changed gets changed over time so you know you could have another you know another line of this vetting process where a committee can jump in and say here is the PR the properties that we expect this contract to have and then you could have one other human people who would come in and say look here is a proof that that I have come up with can you bet that this poof so you know it goes to another level where you are not just building standard for for contracts but you're building standards for proofs for instance and properties so like you said the at the moment the process of generating these proofs is a very like human intensive process and it's like you said you almost need like trained

mathematicians to do this so do you think this would cause like a lot of people to not even like go through this process so for example look you know in aetherium there are some very you know some decent tools like for very very preliminary checking such as like oh yeah hey and stuff but by your colleague at Loyola actually right and but you know there are so many contract on aetherium that are like vulnerable to things that Oriente would have easily picked up and so if it's like smart contract developers aren't even taking the time to like Oriente is literally like a one-click thing but still so many people aren't even taking the time to do that how do you how do we encourage

developers and to like go through this like rigorous formal verification process so uh this is actually well known trade off Ian's not just in the contract engineering it's a well known trade off in software engineering as well and where the community has spent the last five decades building tools for testing analysis and verification so by no means verification is their ultimate question that solves like all possible issues and one issue is the issue of how difficult is it to adopt the approach so even though we designed this whole language so it would be verification friendly we will sure provide the suit for basic

analysis and basic testing of the contract so this is sort of the right way to validate your code base the same way that the developers validate the code they write and other in other domains like okay so you can verify the compiler but then we will spend 10 years doing that or you can just implement the compiler and test it and have a 99% assurance that it's mostly bug free and if these are the chances you were willing to take well we will give you the tools for that so like one easy really really easy to implement analysis that is in our roadmap used to make sure that the contract does it doesn't leak money so with colleagues from in u.s. we have recently submitted ok so we made it public it's not published at the

conference yes the paper that has an analysis for EVM that the text with a high degree of assurance that the certain contract might actually block money the same way parity will it did that or it might give money to someone who is not supposed to receive that and we are planning to do the same analyzers for sale as well and as the second part we will probably make this another an analyzer certifying so for a property as generic and as simple as the contract doesn't leak money we actually don't have to we will not have we will not need to have trained proof engineers to prove that so there will be two that will be checking that and providing this certificate but that's again that's only again because the property is very basic and the property is very simple like the

property of this will transparent contract is something very domain-specific and that probably will require a certain amount of human effort will deliver it but that's with high restaurants comes higher cost of verification so dumb properties you can prove almost for free complicated ones you will need to invest the other point that I would like to add to this is if you look at the applications or the contracts that actually exists right now on popular blogging platforms like a cerium they can be categorized into very popular ones and not SuperFlow ones and those world which are very popular ones which are essentially let's see are c20 kind of contract or exchanges or you know some berries or auctions and for that

you could have templates the way you have templates for your c20 so you could say that here is how an e or C 20 contract should look like and here are the possible properties that you may want to prove on this contract and then you could have associated proof directly either coming from let's see open real community that we have or from from anyone who has was experience in developing core proofs the hard way which no one wants is is to impose developer to submit a contract in fact that you cannot submit a contract without actually having a proof that's that would be really cruel now say for anyone because maybe you are very familiar with JavaScript or solidity or sila but you may not be very very

familiar with compost so even if you want to do this you know you you you are still you know reluctant to do you know in doing this because then you really push away those developers will actually have very cool ideas but just because they don't have they are not familiar with coke pools you know they they can't build on you so yeah we will help have helper libraries for standard contracts and we'll have some you know basic properties that you can always prove or any contract for instance and then if you are if you know if your specialist you know feel free to write your own contract and you own properties okay let's first talk about what is because we have mentioned this to multiple times in the podcast and Iliya

give us an idea what it can do okay so if the question is about a very short overview what the tool can do or what it was designed for so the tool is actually a very bad ok it first of all it's very old and it's very established so it's started in late 80s and it has been mostly a tremendous success in the past that say twelve thirteen years so with initially it was almost a verbatim implementation of one of those very powerful logics to conduct mathematical proofs the logic is called calculus of inductive construction then it was extended to a number of times but because of this correspondence between proofs and the program's it turned out that also comes with a very decent programming language it's not two

incomplete you cannot write non terminating loops in it but you can create surprisingly many interesting and useful programs so pretty much anything you can come up with well anything that probably terminates and then it turned out to be the case that are in the very same environment you can write programs and you can write mathematical statements about them and you can write proof so all these three components that I mentioned before they can be implemented in the same framework and that was a very powerful insight and since then people wrote compilers in Coke which we are also verified and coke that's a famous concert project by nvm and savvy lor who was spearheading it and they wrote OS kernels and to the extent that

people women wrote distributed systems and coke and it's interesting because obviously coke doesn't come and keep with all the distribute its socket machinery and all the backend so when there is a certain level of trust involved so what you write and coke is the logic of nodes and then you trust that the network implementation is correct and it corresponds to what is your mathematical model of this network competition but that is just all to witness that coke is very very powerful and from if you are a programmer and you look at it the code looks very much similar to code in languages such as Kokomo so it's a functional programming language we can recognize similar library similar primitives so if you actually want to write something in

code that compiles and runs you don't even need to know about it's proof component it's fairly it's straight forward and that's it okay I have quite a number of years of experience with coke I used it for proven distributed systems correct and concurrent systems correct and that seems like a natural choice to adopt so essentially we designed Scylla to incorporate a significant subset of coke and add slightly more on top of it to account for the blockchain specifics and communication between the contracts but if you look at the most of the silicon it will look very similar to a subset of coke code and that's why it's so easy to translate Stiletto coke and proofs and who facts

so we've been mentioning a lot about like you know Oh camel and Haskell and these like more established functional languages that are also design are not designed perhaps that are easier to translate to caulk right so what made you guys decide to create your own language rather than try to adapt the existing languages so for example you know one of the things that was happening you know aetherium when could the EBM I decided to create its own some more contract languages like solidity and stuff and now you know I it seems to me that there's a general sentiment that like you know why did we go out like we

shouldn't have gone and like created our own languages now we have to create all the toolings around it and this sort of what some of the hype around webassembly is becoming where it's like oh this is awesome we can use the more established tooling around rust and go and C++ so did you got what were some of the trade-offs you guys had to make on like between using more established systems languages versus building your own alright so the process of designing a programming language is a series of very very painful trade offs and the trade those that we had to consider is expressivity first respectability so haskell and O'Connell okay let me focus on functional languages because those are closer to mathematics and

that's the reason why there is a lot of hype in the smart contract community about how contract should be written and functional paradigm so they're fantastic languages they're very expressive and you can express a lot of computation in a very few lines of code but that comes with the cost that the semantics of Haskell and semantics of a camel that is what the programmers need to know in order to write programs in them it's very big and it makes it very costly to embed this language in a formal reasoning framework Cypress code so in this way there wasn't it so essentially the the rationale was to scale down to the bare set of features that I required to write reasonable smart contracts keep

it readable but do not add stuff on top something like syntactic sugar something like type class operators what Haskell has type kind polymorphism and all these crazy goodies that dedicated Haskell hackers use so that's that's right so we wanted to have a minimalistic caboose and this is essentially how the basic research in programming languages go so if you want to have a formal system about which you can prove things you try to remove all the goodies that actually make programmers life easier and this is why we position this as an intermediate level language so we don't exclude the fact that something like a very large subset of a comma and Haskell can be translated down to Scylla when we come to this point but we wouldn't be proven stuff about this top-level program it

would be prune stuff about the programs that are that are represented instead so again the trade-off expressivity versus tractability or for the sake of formal reason so in a sense the the more expressive this a man takes the more the range of things programmers range of basic constructs the programmers can use in writing a program the more expressive a language it it is the harder it would be to prove properties about the programs that that result out of it and in silly ends Scylla is meant to be meant to have very little expressivity but amenable to proofs and then in the future presumably somebody could write

in Oh camel have it compiled down to Scylla and then prove properties about the code in in in this insula that is correct okay so uh we have a we have around like fifteen minutes left and one of these things we'd like to focus on and understand is how does Scylla compared to other efforts that are going on you know in the formal verification and smart contract space so of course like this idea that smart contracts ought to have proofs and they need to design languages so that tear improving is easy has been taken up

with by other projects and one of the most popular at least in terms of funding levels is is the pesos project which has developed this language called Mickelson or Michelson it seems to have very similar aims to Silla could you could you give us an idea of how the tezo's approach and this Silla approach might be similar and how they might be different all right so the question is about Mickelson language in tezo's and our Silla yes so the design goes are very similar in a sense that both tezo's community and us are very much interested and for more verification or rigor of the stated

properties of the contracts furthermore we share a lot of background because tezo's comes from Oh camel laps and most of the camel laps employs well specifically I Benjamin canoe and actually brakeman who were one of the founders they all come with so little camel background and formal methods background so it is quite unsurprising that they are after the same thing I think them and they also are functional programmers so Mickelson is very much a functional programming like a functional programming language so the devil is in the details so for some reason Mickelson was designed as a stack-based the snake based language something that mimics EVM or similar formalism closely

but it is not yet clear what are the trade-offs with regard to the form of verification so one of the claim that the interpreter for this tech based formalism is actually quite simple and it can be fully embedded and poke well I wouldn't say that the interpreter for Silla is much more difficult but a reason about the stack is not something very nature so that's that we haven't seen that many proofs about tezo's contracts so it's it's hard to have an apples to apples comparison and see what the poke embedding or let's say crowdfunding extractive contract enters in the concern would be like and how their proofs compare in terms of length so this is ultimately goes to benchmark in the

sizes and see and chicken whose proofs are a larger or not since they don't have them yet they might come soon that will be so uh in fact the okay so the idea of having this low-level step based based language in Mickelson leads to the second development and now they have liquidity which is a more high-level language which is actually quite similar to solar in the sense that it also looks like a subset of a camel and it has very similar functional programming mattias the thing which is missing from there or maybe it was a design choice is the explicit communication between the contracts in a sense that each contract is kind of this sealed autonomous actor that only receives the messages from

other contracts and send messages to other contexts and this is only the way for the contracts to interact on the blockchain so this is something that Silla as a language enforces syntactically so you like if you write the contract is going to be shaped as this actor that receives messages and sends messages so it's not enforced in liquidity and either it is in Mickelson and that's why I can only speculate the station properties like what we discussed before about this passenger in the future is going to be a bit more complicated should they have a formal and a formal model of liquidity somewhere income so yeah so basically the the main difference is that liquidity / Mickelson don't have them this after message passing model enforced at the language level and the

second is Mickelson a stack-based which makes it slightly more low-level then and still if I just may add to one point this is if you look at time since you're talking about other languages we should we should talk about this language from atheneum which is bamboo and again the idea was with bamboo is is the straightest trade-off between expressivity and the properties or the correct the safety in property that you can prove about about the contract so I would say that it's it's bamboo is another language which is lexis expressive to some extent but it's more structured in the sense that what they call you know polymorphic contracts and the idea is that you know the

contracting gives you a rigid structure and it tells you how the contract will change itself depending on how users are interacting with it so instead of having five let's say five functions or five transitions in your contract you would have one contract and then another contract and then another contract and this contract will eventually change depending on how users interact with this contract so it has a very pretty different kind of behavior to some extent how this contract will behave so I I feel that you know it's the idea that we are doing in Seoul is pretty close to me every Lea will be able to elaborate more on this but I feel that that my bamboo is has some elements that see La Silla has as well to some extent this skirt another kind of important difference I saw I'd notice as well was

that in Mickelson there seems to be a focus on making it purely functional while in Silla there is this ability to have like some sort of state that you their functions are allowed to modify and what were some of the trade-offs you did on making that decision okay so the question is why still is not purely functional while Mickelson and liquidity seem to be a purely functional so uh this is actually an interesting question because it very much comes down to the terminology of what you count as a functional and what you count as an imperative language so both Silla and Mickelson have stayed but in Mickelson

this state or liquidity which makes it even more explicit this state is made explicit so basically you pass this state around like accumulating certain components to it and you can even ship it to another contract and you can get it back from another contract and then you can finally give it back to the blocking back and it will probably store it so this is probably the level of verbosity that we wanted to exclude I mean I said that we offer taken minimalistic choices but having a state that the contract modified seems so paramount and so important that we said okay so we are going to have state we are going to have very small set of operators that interact with this state

and wells and stated something like this this was the sort of mutable I stated something the formal methods community knows how to deal with so there are many verifiers there are many program logics that can proof automatically the effects of program interaction with the state so we didn't really see the benefit of making it absolutely pure functional and to this extent Silla also has a bunch of other effects that are expressed on the semantics so in addition to change in state we also have send messages and in the future we will have emitting events so making these things part of the execution was important and obviously you can model all that through some

state pass and mechanisms but we thought that by the way for all right in certain specifications it will be better to implement them the way with it so bottom line most of the state manipulation you can do in Silla you can encode them Tasos in Intel's of Nicholson as well it's going to be less straightforward and it's at the moment it's not clear whether it's going to be exploitable in a certain way or not as I said since Mickelson implements interaction between the contracts using this state pass and mechanism rather than by sending messages the implications are not clear so another question then maybe somewhat related is you know we discussed earlier

one of the other main features of the silica platform is the whole full sharding mechanism so what were some of the design choices that went into the language as well as the overall vm design that were you know one of the big things that people often won't need with charting is you need the ability to do like a synchronous contract calls and stuff and so what were some of the thought process of a charting that went into the design of this system I mean for instance to start with though we don't have an EVM the way VM to be EVM it has a VM we are currently have we currently have an interpreter that takes

silicon track interpreters now the problem is you know you you have a short in architecture and you need a way to cut off as you said you know to ask messages you know in an asynchronous manner so it's a it's it's a work in progress where there are three different angles that we're exploring right now one is can you ensure that all from all transactions that somehow you know may be in conflict because they are touching the same seat or reading from the same stage or manipulating the same state gets shorted to the same shock so this is this is one idea if you can do that then you know you can even meet you know certain issues that near the idea is that can you actually have some kind of

a language support which easier would be able to I don't can you have some it some some level at the language which allows you to kind of merge certain transactions going in different shots and and there is could be other ideas for instance can you have some kind of a conflict detect detector or resolve was somewhere in the architecture that helps you helps you to you know solve those problems so we have we are currently actively exploring all these themes three directions and we have plans to write a paper around this which will be happy to make a publication so what we like to get a sense of is what is the current state of development of Silla and what can the community expect to see

in in the form of releases over the next six months so or what what we have right now is is an interpreter that it's not complete of course it's still working promise but it is it's it is in a stage where we can write we can still write some interesting contracts so we had an example in the sale of white paper initially or the kickstarter contract so that contract can be doubled by by our interpreter right now so we have that support ready there are some other examples that we are currently working on we will we are working on examples like ER c 2007 21 so uh the the deputies in the stage berry skin can handle

certain contracts it cannot handle all contracts that that you would imagine right now it doesn't have certain supports for certain data structures for instance but we do have we do have a working prototype where you know your user can deploy a contract to the silicon network and the silicon network and no Dena silicon network can actually run that contract and commit the state to the blockchain and the entire chain is ready our plan is to have the complete implement you know implementation of the interpreter ready by end of June when we are planning to have our second version of the test net where we have plans to you know to show to people you know here's how Silla looks like and you can play around with

contracts let me add to that so on the verification side we also have the prototype implementation of Silla in Coke which is done by means of what's called shallow embedding so essentially instead of implementing the whole language interpreter in Coke we only implement those primitives that Coke doesn't have and since there is a lot of shared parts between the syntax the rest is taken from Kok verbatim and in this prototype we can prove the properties like what we discussed and the very same Kickstarter contract is implemented in this in this formalism and the properties are established what is missing though is the connection link between what runs on the blockchain and

what is formalized and coke so that can be done by syntactic translation this is something that we will provide provide very very soon so you could write a contract and solar then yes expected to call their you prove the properties you know that is right and then you can go back to your implementation and rabbits on the silica blockchain cool we look forward to the the releases especially in the in the next version of the test net if people are able to deploy basic silicon tracks that would be pretty pretty cool we look forward to that so Amrit and Ilya it was a pleasure to have you on the show and we hope we'll catch up again on Silla and silica six months down the line when there's

there's more to report especially maybe what might be interesting is to discuss the interaction of programming languages and shouting and your in your paper there silica always remains one of the projects I a follow so I'm really looking forward to what comes out of this project when it goes into the main net so for our listeners thank you so much for joining us as you know we release new episodes of epicenter Bitcoin every Tuesday you can subscribe to iTunes SoundCloud or your favorite podcast app for iOS and Android to keep up to date with the epicenter you can

watch the video version of this show on our youtube channel at youtube.com slash epicenter Bitcoin also we've recently created a gaiter community where you can chat with us and other epicentre listeners at epicenter dot TV slash gator I find that the conversations here are are very intellectual because of the nature of the community we have we have built so check our channel out and of course your reviews and your feedback on Twitter and iTunes is very valuable to us and it keeps us going so support the show with leaving us a review on iTunes and we look forward to being back next week thank you for listening

[Music] [Music]