{"id":"tsVo1-TGnQM","title":"Formal Verification in the Age of AI | Illia Polosukhin and Alex Skidanov","description":"Illia Polosukhin and Alex discuss why formal verification is becoming increasingly important in the age of AI.\n\nAI is accelerating both software development and cyber attacks, making it harder for humans to reliably review and secure increasingly complex systems. Formal verification offers a different approach: mathematically proving that code behaves as intended.\n\nAs AI writes more of the world's software, being able to verify it becomes critical.\n\nNEAR is the Blockchain for AI\nWebsite: https://near.org/\nNEAR AI: https://near.ai/\nIntents: https://near.org/intents\nChain Abstraction: https://www.proximity.dev/\nSharding: https://nearone.org/\n\nFor the devs\nGitHub: https://github.com/near \nDev Docs: https://docs.near.org/\nDevhub: https://devhub.near.page/ @NEARDevHub\n\nConnect with socials\nTwitter:   / nearprotocol  \nBlog: https://near.org/blog/\nMedium:   / nearprotocol  \n#NEAR #nearprotocol #NEARAI","channel_name":"NEAR Protocol","published_at":"2026-09-14T00:00:00.000Z","thumbnail_url":"https://img.youtube.com/vi/tsVo1-TGnQM/hqdefault.jpg","transcript_text":"guys. Alex, good to have you as well. We're excited. Been working together for a while and uh feels good. How are you guys doing? Let's get really serious here. And just let me ask you how your Zcash positions are feeling today. You're doing fine. Okay, good. All right, guys. Let's talk formal verification. Uh there something that is very important in the era of privacy, right? So just to kind of like dumb it down for audience, I know we have a set of questions here, but just to kind of like set the stage from how I understand it so they can relate is when you have these privacy preserving technologies, you have this imminent issue of trying to always verify the total supply of an asset or whether an action or you know did or did not happen, right? Right. And so there's this constant issue of like the beauty of ZK and privacy kind of provides you this element of well privacy but the issue is having to verify you know what actually happens in that black box if you will. And so you guys have have been doing a ton of great work on formal verification. And so maybe you guys just want to set the stage for where NEAR is at on the formal verification roadmap and just kind of catch us up there. Yep. Yeah. Maybe just start. Go ahead. Go ahead. Yeah, formification is I mean not just for privacy. I think it's broader point that we're living in a world where what before was like a security paradigm where you know smart people looked at this code and they didn't find anything and so hopefully other smart people if they do find report it and everybody else will not be able to find it. That's been the paradigm up until now. the security audits, the kind of pent testing uh not just in crypto but in the broader uh broader u cyber world and with AI what we've seen right is now everybody's equipped effectively with you know super intelligent uh cyber attacker right that you know will um execute whatever you command um and so you know we obviously had a massive flew of hacks not just again in crypto in web true uh now we have agents who are you know doing this while while training to to attack systems they attack other systems so we're kind of already in a paradigm where effectively AI is the uh attacker system and so the general advice right now is like hey run agents to defend your system right models run AI you know protect yourself and you're kind of in this like cat and mouse game where you have you know you running a model that just came out but the guys who have, you know, training a new model already have that one. So you you don't know if that has like better capabilities and find something that yours didn't find. Somebody may just spend more compute, right? More reasoning tokens, more agent um on it as well. People may mix models, etc., right? Or fine-tune. And so you kind of have this like challenge that it's not enough to just run a defensive AI model to cover everything. And so the only true way to do it is to actually mathematically prove that code does exactly what it says it does, right? And I mean there's a whole slew of like the specifying that and we will talk about this but the fundamental is this idea of formification where you say hey and for for you know ZK for privacy for um it's one of the fundamental properties like hey let's prove that you know there's no way to mint you know new tokens without accounting there's no way to you know transfer somebody else's money without uh the you know source uh actually signing a transaction. action uh like in the simplest form right you know in AMM it's like there's no way to effectively get more money out of the trade or if you're putting liquidity there's always a way to withdraw it right you want to formally verify those properties of the protocols and you know as you go down the line so that's kind of the fundamental setup and yeah I mean Alex been working kind of for the past year uh to develop a bunch of stuff on this side so I'll pass it to him Yeah. Okay. So please so one thing uh before before I talk about what we've been building I I guess it's uh it's worth defining a little more what forification is because on the recent news like probably everybody have heard that entropic have has formalized uh the last uh firmas theorem uh and reading hacker news comments or like Twitter comments it's pretty clear that people are not quite uh they don't quite grasp what for notification means Right. So, so like for example, Entropic says, \"Hey, our proof is 13 million lines of code uh right and uh you know like have someone looked at those 13 million lines of code does anyone need to look at them etc. Right? So, so I think let's use that example very quickly to understand what it is, right? So, so formal theorem says that for no three numbers uh you know a a a a cubed plus b cubed is never equal to cubed something like this right and so in that in that example right we have the statement of the theorem that says hey it is the case or rather hey this is what we want to prove right and that's one line of code right and then we have 13 million lines of code of the proof right and then you if you feed them into lean lean is the uh tool everybody uses these days or or like it's it's one of the biggest tools people use uh the linen says hey the theorem is correct right so I think what's important to understand here is that you do need to trust that one line of code right so so if someone misspelled this line of code you know like they use like for example you know like a very simple example they can forget to specify that you know like the two numbers need to be greater than zero things like that right that would be an incorrect like you know a proof of a wrong thing is a useless thing right but if you do trust that one line and if you do trust that lean is correct uh then you do not need to trust the 13 million lines of code, right? Those are uh machine checked. Uh and if you know if you trust the first line and the link says, \"Hey, the proof has checked out, you do not need to trust the 13 million lines of code.\" They can be as sloppy as it gets. You know, they they can go all over the place, but if it says it's true, it is true, right? And so in the context of code, right, you can the now the flow is you have a smart contract and the smart contract would be very large, right? like you can imagine it has like a lot of logic a lot of special cases a lot like maybe I don't know optimizations etc right and reading the code of a smart contract is relatively involved process and so we have auditors and then you know we pay them a lot of money to read it right and then you would have some statement uh that you really care about like as a liquidity provider for example imagine I'm providing liquidity to some sort of unis swap v4 which is you know like unlike unis swap v1 is actually a relatively complex system the only thing I care about is if I deposit money right now at any point in the future I would be able to withdraw right and then then there's like you know there's some rule in terms of how much money I should be able to withdraw right and so then what you would do is you would have this statement that says hey uh if you deposit money as a user then no matter what happens to the contract you know like any like other users call any public interfaces available at any point in the future you will be able to withdraw you know you know assuming you did not withdraw before that right right and so and so you you put that statement in, right? And so that statement is much shorter than the than the smart contract itself, right? You read that that statement and then you need a proof that it is the case, right? And so until recently, until like I would say half a year ago, that proof was what was making it all impossible in practice because the proof like you know like if if it takes you like a week to write a smart contract, it would take you several years to prove that it is correct, right? [snorts] And so that was Go ahead. No, I was just going to ask is this this um this lean product that you're describing here, this kind of consolidation of all of this kind of complex, you know, code is is is is what you're describing this this concept of lean. So, so lean is a tool that will verify the proof, right? So, so it's also a language in which you will express it, right? Yeah. And [snorts] so, until recently, writing those proofs was prohibitively expensive like like an example of perma theorem, right? you would need to write 13 million lines of code. As a matter of fact, there was a an effort that started in 2004 like multi-year effort with a huge team under Kevin Bazard and Imperial College of London, right? And you know like and then Antropic did it in 11 days, right? So so that is an example of how of like what changed, right? So today proving became solved and and the reason it became solved is that because at the end of the proof it's either one or zero. It's an outstanding real environment and so every single model every single lab has lean as an environment and so they became extremely good at proving lean right and so today proving is practically solved right like if you have a theorem uh like you know for my last theorem was proven if you were following this debacle of openai and the neier stokes theorem that was proven in lin as well it wasn't just like a paper it was an actual formal proof that they have it proven right and so now the only question is uh can we write down this statement in a way that we can trust it right because the statement that you know like when you say hey I'm not going to lose money in in English it says easy to express in lin not so much right so you need to express it you need to read it you need to trust it right so now the frontier move there uh and the second question is how do you prove cheaply right so like there's a benchmark called putnam bench uh in which we recently announced uh we we solved it and we're on the first place right now uh and it is uh sorry it's 250 times cheaper than the second best solution submission and the second best submission was like $20,000 right which is quite pricey and ours was 111 right so that is the biggest thing we're working towards is like you know how do we prove like like proving became feasible uh but you know it doesn't need to be just feasible it needs to be cheap right and so how do you do it cheaply that's what we've been working on right so like the the effectively we have three directions right now one is how do you prove things very cheaply second one is how do formalize smart contracts in a way that you can trust the formalization uh you know and the third one uh is something I I mentioned at the beginning uh is that you also need to trust the LIN kernel and Lynn was designed for people who are friends with each other to trust each other right like you're a mathematician you have a mathematician colleague you're sending proofs to each other you would never have incentive to to trick each other right but now that you you know uh if I'm if I'm giving if I'm publishing a smart contract and I'm giving you a 13 million lines of proof that it is correct. I actually have a very strong incentive uh to lie to you. Right? So at this point breaking link kernel becomes actually very desirable, right? And so we're working on uh uh we're working on making sure that link kernel is correct, right? We're reducing it to a uh much simpler uh code base to much simpler for system. So actually I I'd love just to like your general reaction to like what the Navier Stokes like you know this whole situation how it's evolved. Obviously there's the privacy and the confidentiality of open AI potentially reading you know uh the chats of the researchers that were working on this problem. But it sounds as if the frontier is no longer trying to solve the problem. it has been solved according to lean, but now people are questioning whether lean is effective and airtight in expressing these proofs. Is that kind of the right way to think about like where this problem stands right now? I realize this is a little bit of a side quest, but it feels relevant to formal verification. So, I'm just curious like what is your general reaction both on the privacy element of this, but then also where Navier Stokes stands right now? Yeah, I mean I from my perspective it's it's the best highlight of everything we've been saying for the past three years on the privacy side, right? I think it's a pretty critical that the AI belongs to you, not to the company that provides you the service, right? And this example is just kind of you know yet another example in a string of kind of recent uh problems. I think the poller was the one who kind of introduced this idea that like hey the companies are effectively taking your data and you know turning that into their own products. And there's been a lot of rumors that even if you're like asking to not train on your data, they would create synthetic data out of it and then train on that. Uh, and I mean obviously it's rumors so like there's no clear evidence but this example is effectively kind of confirming that like hey guys you know they effectively like took something that had like an insight around how to do it and and and kind of expanded that right by spending a ton of compute to uh to finish a proof. I think where on the broader side the challenge as Alex mentioned has been in formalization itself. So like whenever you have a problem right now it's like how do you know that it's a correctly stated problem in the first place to solve to prove and I mean Alex maybe has a better better kind of understanding of where that stands uh latest yeah but there's no question that the proof that openai presented is correct I mean that that is that's what I wanted to convey at the beginning is that if lean says something is correct it is correct right with the uh discounting for the fact It could have a bug, but it's uh it's extremely unlikely that either the Ethereum or Navier Stokes uh actually used any bugs in Lynn, right? And and also Lynn has two kernels. So, sort of like you know how Ethereum has two clients, Lynn has two kernels and Ethereum is only correct if it passes both and they independently developed. Uh it is it's still not like if the model was malicious, it could potentially find two different bugs in both, right? create like you know like like little u uh you know little hidden gems in its proof that that utilize both to prove it eventually right but it's uh yeah it's it's highly unlikely that this is the route it took right and luckily we can still inspect the reasoning right so hopefully both entropic and open looked at those and like you would see if it says hey I cannot prove it let me just find a zero day uh right you you you would notice it yeah yeah so Alex one of the things that you were saying um you know kind of previously explain explaining the value of what you guys are doing with lean in. Formal verification is just this drastic reduction in cost to basically formally verify and um get to the conclusion of verifiable truth, you could say. And I actually had a really interesting podcast here a couple days ago with a with a fellow big- time investor who spoke about SpaceX and how their cost to bring one kilogram of matter to space has gone from $20,000 previously, you know, prior to SpaceX to now down to about $100. So, you know, a massive massive massive reduction in cost. And then what is the result of this is this massive opening of a new TAM of if we can get a lot more matter into space we can do a lot more up there. We can build data centers up there. We can we can do anti-uclear right. So there's this whole kind of like concept of and in any kind of market reduce the cost to you know achieve an outcome and then scale. And so when it comes to this by reducing the cost of formal verification by reducing the cost of this kind of proofs Ilia I'm curious from your perspective more from like the founder side and then Alex on the tech side what becomes possible right like what are you what what are you taking advantage of from the near side due to this drastic reduction in cost um and and how do you kind of expand the market for what you guys are building? Yeah, I think so from a software engineering perspective, from kind of building products, the slow part is not anymore the building, it's validation, right? Like my agent can write, you know, millions of code overnight, but I will have no idea, right, if it's doing stuff correctly. And so the bottleneck effectively moved from writing code to validation, verification, and relying on human reviews just doesn't work, right? you're effectively still using an agent to review it. And so that kind of gets into like, you know, AI reviewing AI, which we know uh doesn't always work as well. And so for formal verification as a framework allows us to uh shift from this human validation and you know AI validation to actually have a formal validation of what the code does, right? And this is especially you know important when you're dealing with a lot of money, right? when you this is blockchain code, this is smart contracts, um you know intents etc or anything else that's mission critical, you want to have a validation of correctness of that code down to the properties you care about, right? So you the money you you know trading in and saying you expecting this outcome, right? It should come out come out on the other side. And again before this was both slow and expensive, right? before like we would write a smart contract we would you know give it to auditors maybe you know there's like few firms that were doing kind of manual formification and you know 3 months later they would give you an audit report right maybe you fix some stuff but like the development speed of of kind of this engineering was extremely slow and so the idea here is that you have something that's fast intelligent and can plug in directly into your kind of continuous integration process where you can effectively verify that you know whatever change you did still uh proves down the properties that your users care about. And then from there this should be expanded beyond just you know smart contracts, money, blockchain but to things that you know we're really uh relying on that people don't think about which is like networking stack and you know other layers of kind of computing where we actually have a lot of zero day vulnerabilities that keep getting found right. And uh I mean there was like I don't know if you remember like a year ago there's a vulnerability where somebody could text you a image in on iPhone and it like effectively root your root your iPhone and like steal your crypto right and people were targeted in crypto with that right so this type of things you know should be formally verified to ensure that these kind of things doesn't happen so but that requires you know like iPhone iOS code base right there's millions of lines of code so you need something that can actually like verify cheaply across large code bases and have broader and broader properties. But I think the the big kind of question mark and this is still active research is how do we easier and easier now formalize and define what are the criteria that that needed to be proved. Right? So beyond you know simple like swaps and kind of multiigs etc which are pretty simple to do uh like for something as complex as like you know no way to exfiltrate your private keys. Uh there would be a really nice property right that if your private key never leaves your machine if you can just prove that for your operating system now you know at least you know it's not possible. So um so this is kind of things that you know will become possible now with this technology becoming cheaper and cheaper. given that um you know you guys are sort of taking uh a pi like a leadership role in formal verification one of the few blockchains that has gone and done this so far. You guys are implementing this into Near and we anticipate that this is something that is going to fit into pretty much not only every facet of blockchains and crypto but also broadly software stacks you know outside of crypto. Is there a chance that you know the work that you guys do internally at Near, you'll kind of create like a formal verification product and it won't really look like a blockchain product, but it'll be something that maybe like I don't know Near Labs is going to add to its product stack and then you know you can you guys can kind of offer that to companies that are looking at increasing formal verification across their own product stack. Yeah, potentially. I mean we have right now the neari the the agent that Alex built that effectively scorn and platinum bench it is under neari um it is open source people can run it and then yeah as we continue advancing this u it makes sense to productionize and kind of offer neari suite and then Alex just kind of uh closing out here on the kind of world that we're heading towards right with just kind of the we spoke spoke to E-mod, the exfounder of stability AI here on our AI show with Near and he basically described that we've we've now reached what he calls competent intelligence with AI, right? So, we're kind of at the point where it's it's getting to that point where it's pretty damn competent. Just talk to us about this future world of accelerating intelligence and why you feel that building these formal formal verification systems are so crucial to this future world that we're entering. Yeah, that's that's a great question and I I think a very good way to think about it is like like I'm pretty sure everyone today who's who's using like cloud code or codeex right have experienced in many many times this feeling where you you build like you might still want to review code that it's writing right but it's just becoming it's producing so much code so much um uh yeah it creates so much that it's it becomes completely infeasible for us to review it in any meaningful way, right? So, I think a very large number of people at this point switch to the mode where either they like build with one review with another or just build with one and like yeah, it's probably correct. Let me let me use it as is. And uh and it's only going to be getting worse, right? AI is getting better and better uh faster and faster, right? So, we're going to be creating more and more uh uh uh artifacts with it, right? Right. And I think formal verification here is extremely helpful because it can it it allows you to create a very large codebase, a very large product, right? And then a relatively small spec that you as a human actually is able to read. Prove it, right? And then and then you can say, hey, a AI created for me this massive thing that I wanted, right? It is way beyond my capability at this point to review it, right? But I want I cared about this this and this property. And here I have formal proofs that the thing it built does satisfy the proof which is right. So I can use it. Right? So that will allow us uh to to trust AI in building much more complex systems that we can reasonably trust it today uh and still be certain uh that they are correct and uh effectively still be able to an extent inspect what is what is actually being created without without trusting it blindly. Awesome gentlemen. Great work and we appreciate your time. I want to take this last minute here to just introduce the Let's get to the full screen now, please. Um, we're going to do the rollup persp launch, guys. Um, we have now launching the roll-up persp.ne.com. Yes, all you people in the chat who are bullish on Nearcat. Yes, all you people in the chat who are saying near is going to rip. You guys can trade, you guys can swap, you guys can do intense all on the rollup.nneer.com. This is the initial launch of what we're doing. And so basically, it's super simple. You just come in here, you create you create an account. All rollup traders that sign up through our website keep 20% of their platform fees in near tokens. We are also going to be doing a giveaway that we will announce towards the end of the stream and after the stream. It's it's a near.com front end. You come in, you click create account, it redirects you to near.com and then you're good to go. And so this is the initial iteration and we can come back to to us and close out here. And just to kind of give you guys our vision, the rollup has this media and distribution channel. We have this massive audience. Near.com is, you know, and obviously they're a partner of the show and we appreciate Alex and Ilia. This is the one of the best onchain trading experiences I've ever used. We've traded I've been trading on it for months now. Per, swaps, transfers, cells, everything. It is so goddamn easy. Pass key. So easy. Any chain, you don't need to think about chains. You don't need to think about wallets. It's just all there. So, don't think about gas as well. Nothing. Yeah. It's just like I just want to get long or shorter. And so guys, we're going to be trading live on the show a ton more. We're going to be incentivizing the usage of this in the uh initial period. So, I'm going to drop the link in the chat to all the channels, guys. Sign up. We're doing a thousand USDC giveaway to give this uh a big kickoff. And the roll-ups, pers, and intents are now live. Um Ilia, Alex, any closing thoughts on this? Well, I mean, excited for you guys to launch this. Um I think everybody should roll up their sleeves and uh go use it. [snorts] Uh but yeah, I think the the broader vision of like this unified liquidity that is private that is, you know, unites kind of AI and blockchain is life, right? And I think kind of the privacy is now the core thesis both for AI and for blockchain. I think privacy is freedom. Privacy is peace of mind as well. like when I you know do anything on chain now through near.com I don't need to think about you know where this data will come out and similarly when I use you know nearai I don't need to think about you know like I actually got banned by open AAI for for some stuff I was doing on like doing like actually doing trying to test cyber uh security stuff of a system but like you know it I'm effectively trying to attack right so they banned me so like this is where you need you know uh privacy because you can actually use stuff and not like double think of what's going to happen. So yeah, excited excited to partner with you guys. Excited to see this uh rolling out. Uh and yeah. Yeah. Awesome. Thank you, Alex, for joining us as well. Thank you, Ilia. I think we're going to move on to our next panel here. I really appreciate your time. And just one last word for me is that you know this is kind of like the very beginning. It's like our V.01. We're already talking with different teams about launching rollup vaults about expanding veneer AI uh with the Venice API capabilities into the site to kind of have more of like a you know robo advisor. Um and there's just more and more that we're trying to build into this into our own website as well and kind of bring this all together. You know we think we think that the future of media and markets are going to go hand in hand. If Robbie and Andy have good ideas, they are long a position, short a position, they're, you know, there's a rumor that's buzzing, we we want people to take action on that. Um, and we want people to take action on this website on the rollup.nneer.com. So guys, thanks for being a part of the show today and we got a long road ahead. So, uh, appreciate you guys being the first guests. Thanks so much, Jent. Couldn't do without you","transcript_synced_at":"2026-11-03T04:20:20.707Z","segments":[{"start_seconds":0,"text":"guys. Alex, good to have you as well. We're excited.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=0s"},{"start_seconds":3,"text":"Been working together for a while and uh feels good. How are you guys doing?","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=3s"},{"start_seconds":11,"text":"Let's get really serious here. And just let me ask you how your Zcash positions are feeling today.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=11s"},{"start_seconds":19,"text":"You're doing fine.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=19s"},{"start_seconds":20,"text":"Okay, good. All right, guys. Let's talk formal verification. Uh there something that is very important in the era of privacy, right? So just to kind of like dumb it down for audience, I know we","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=20s"},{"start_seconds":29,"text":"have a set of questions here, but just to kind of like set the stage from how I understand it so they can relate is when you have these privacy preserving","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=29s"},{"start_seconds":36,"text":"technologies, you have this imminent issue of trying to always verify the total supply of an asset or whether an","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=36s"},{"start_seconds":44,"text":"action or you know did or did not happen, right? Right. And so there's this constant issue of like the beauty of ZK and privacy kind of provides you","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=44s"},{"start_seconds":53,"text":"this element of well privacy but the issue is having to verify you know what actually happens in that black box if","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=53s"},{"start_seconds":61,"text":"you will. And so you guys have have been doing a ton of great work on formal verification. And so maybe you guys just want to set the stage for where NEAR is","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=61s"},{"start_seconds":69,"text":"at on the formal verification roadmap and just kind of catch us up there. Yep. Yeah. Maybe just start.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=69s"},{"start_seconds":76,"text":"Go ahead. Go ahead.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=76s"},{"start_seconds":78,"text":"Yeah, formification is I mean not just for privacy. I think it's broader point that we're living in a world where what","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=78s"},{"start_seconds":86,"text":"before was like a security paradigm where you know smart people looked at this code and they didn't find anything","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=86s"},{"start_seconds":95,"text":"and so hopefully other smart people if they do find report it and everybody else will not be able to find it. That's","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=95s"},{"start_seconds":103,"text":"been the paradigm up until now. the security audits, the kind of pent testing uh not just in crypto but in the","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=103s"},{"start_seconds":109,"text":"broader uh broader u cyber world and with AI what we've seen right is now","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=109s"},{"start_seconds":116,"text":"everybody's equipped effectively with you know super intelligent uh cyber attacker right that you know will um","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=116s"},{"start_seconds":125,"text":"execute whatever you command um and so you know we obviously had a massive flew of hacks not just again in crypto in web","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=125s"},{"start_seconds":134,"text":"true uh now we have agents who are you know doing this while while training to to attack systems they attack other","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=134s"},{"start_seconds":141,"text":"systems so we're kind of already in a paradigm where effectively AI is the uh attacker system and so the general","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=141s"},{"start_seconds":149,"text":"advice right now is like hey run agents to defend your system right models run AI you know protect yourself and you're","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=149s"},{"start_seconds":157,"text":"kind of in this like cat and mouse game where you have you know you running a model that just came out but the guys","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=157s"},{"start_seconds":164,"text":"who have, you know, training a new model already have that one. So you you don't know if that has like better capabilities and find something that","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=164s"},{"start_seconds":171,"text":"yours didn't find. Somebody may just spend more compute, right? More reasoning tokens, more agent um on it as well. People may mix models, etc.,","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=171s"},{"start_seconds":180,"text":"right? Or fine-tune. And so you kind of have this like challenge that it's not enough to just run a defensive AI model","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=180s"},{"start_seconds":187,"text":"to cover everything. And so the only true way to do it is to actually mathematically prove that code does","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=187s"},{"start_seconds":194,"text":"exactly what it says it does, right? And I mean there's a whole slew of like the specifying that and we will talk about","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=194s"},{"start_seconds":202,"text":"this but the fundamental is this idea of formification where you say hey and for for you know ZK for privacy for um it's","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=202s"},{"start_seconds":211,"text":"one of the fundamental properties like hey let's prove that you know there's no way to mint you know new tokens without accounting there's no way to you know","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=211s"},{"start_seconds":219,"text":"transfer somebody else's money without uh the you know source uh actually signing a transaction. action uh like in","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=219s"},{"start_seconds":228,"text":"the simplest form right you know in AMM it's like there's no way to effectively get more money out of the trade or if you're putting liquidity there's always","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=228s"},{"start_seconds":236,"text":"a way to withdraw it right you want to formally verify those properties of the protocols and you know as you go down the line so that's kind of the","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=236s"},{"start_seconds":244,"text":"fundamental setup and yeah I mean Alex been working kind of for the past year uh to develop a bunch of stuff on this side so I'll pass it to him Yeah.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=244s"},{"start_seconds":257,"text":"Okay. So please so one thing uh before before I talk about what we've been building I I guess it's uh it's worth defining a little","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=257s"},{"start_seconds":266,"text":"more what forification is because on the recent news like probably everybody have heard that entropic have has formalized","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=266s"},{"start_seconds":275,"text":"uh the last uh firmas theorem uh and reading hacker news comments or like Twitter comments it's pretty clear that","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=275s"},{"start_seconds":281,"text":"people are not quite uh they don't quite grasp what for notification means Right.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=281s"},{"start_seconds":287,"text":"So, so like for example, Entropic says, \"Hey, our proof is 13 million lines of code uh right and uh you know like","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=287s"},{"start_seconds":296,"text":"have someone looked at those 13 million lines of code does anyone need to look at them etc. Right? So, so I think let's use that example very quickly to","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=296s"},{"start_seconds":304,"text":"understand what it is, right? So, so formal theorem says that for no three numbers uh you know a a a a cubed plus b","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=304s"},{"start_seconds":312,"text":"cubed is never equal to cubed something like this right and so in that in that example right we have the statement of the theorem that says hey it is the case","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=312s"},{"start_seconds":320,"text":"or rather hey this is what we want to prove right and that's one line of code right and then we have 13 million lines of code of the proof right and then you","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=320s"},{"start_seconds":327,"text":"if you feed them into lean lean is the uh tool everybody uses these days or or like it's it's one of the biggest tools people use uh the linen says hey the","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=327s"},{"start_seconds":336,"text":"theorem is correct right so I think what's important to understand here is that you do need to trust that one line of code right so so if someone","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=336s"},{"start_seconds":344,"text":"misspelled this line of code you know like they use like for example you know like a very simple example they can forget to specify that you know like the two numbers need to be greater than zero","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=344s"},{"start_seconds":352,"text":"things like that right that would be an incorrect like you know a proof of a wrong thing is a useless thing right but if you do trust that one line","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=352s"},{"start_seconds":361,"text":"and if you do trust that lean is correct uh then you do not need to trust the 13 million lines of code, right? Those are","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=361s"},{"start_seconds":369,"text":"uh machine checked. Uh and if you know if you trust the first line and the link says, \"Hey, the proof has checked out, you do not need to trust the 13 million","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=369s"},{"start_seconds":377,"text":"lines of code.\" They can be as sloppy as it gets. You know, they they can go all over the place, but if it says it's true, it is true, right? And so in the","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=377s"},{"start_seconds":386,"text":"context of code, right, you can the now the flow is you have a smart contract and the smart contract would be very large, right? like you can imagine it","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=386s"},{"start_seconds":394,"text":"has like a lot of logic a lot of special cases a lot like maybe I don't know optimizations etc right and reading the code of a smart contract is relatively involved process and so we have auditors","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=394s"},{"start_seconds":403,"text":"and then you know we pay them a lot of money to read it right and then you would have some statement uh that you really care about like as a liquidity","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=403s"},{"start_seconds":410,"text":"provider for example imagine I'm providing liquidity to some sort of unis swap v4 which is you know like unlike unis swap v1 is actually a relatively","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=410s"},{"start_seconds":417,"text":"complex system the only thing I care about is if I deposit money right now at any point in the future I would be able to withdraw right and then then there's","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=417s"},{"start_seconds":426,"text":"like you know there's some rule in terms of how much money I should be able to withdraw right and so then what you would do is you would have this statement that says hey uh if you","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=426s"},{"start_seconds":434,"text":"deposit money as a user then no matter what happens to the contract you know like any like other users call any","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=434s"},{"start_seconds":441,"text":"public interfaces available at any point in the future you will be able to withdraw you know you know assuming you did not withdraw before that right","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=441s"},{"start_seconds":449,"text":"right and so and so you you put that statement in, right? And so that statement is much shorter than the than the smart contract","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=449s"},{"start_seconds":457,"text":"itself, right? You read that that statement and then you need a proof that it is the case, right? And so until recently, until like I would say half a","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=457s"},{"start_seconds":464,"text":"year ago, that proof was what was making it all impossible in practice because the proof like you know like if if it takes you like a week to write a smart","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=464s"},{"start_seconds":472,"text":"contract, it would take you several years to prove that it is correct, right? [snorts] And so that was Go ahead. No, I was just going to ask is","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=472s"},{"start_seconds":481,"text":"this this um this lean product that you're describing here, this kind of consolidation of all of this kind of","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=481s"},{"start_seconds":488,"text":"complex, you know, code is is is is what you're describing this this concept of lean.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=488s"},{"start_seconds":496,"text":"So, so lean is a tool that will verify the proof, right? So, so it's also a language in which you will express it, right? Yeah. And [snorts] so, until recently, writing those proofs was","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=496s"},{"start_seconds":504,"text":"prohibitively expensive like like an example of perma theorem, right? you would need to write 13 million lines of code. As a matter of fact, there was a an effort that started in 2004 like","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=504s"},{"start_seconds":513,"text":"multi-year effort with a huge team under Kevin Bazard and Imperial College of London, right? And you know like and then Antropic did it in 11 days, right?","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=513s"},{"start_seconds":522,"text":"So so that is an example of how of like what changed, right? So today proving became solved and and the reason it became solved is that because at the end of the proof it's either one or zero.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=522s"},{"start_seconds":532,"text":"It's an outstanding real environment and so every single model every single lab has lean as an environment and so they became extremely good at proving lean","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=532s"},{"start_seconds":541,"text":"right and so today proving is practically solved right like if you have a theorem uh like you know for my last theorem was proven if you were","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=541s"},{"start_seconds":548,"text":"following this debacle of openai and the neier stokes theorem that was proven in lin as well it wasn't just like a paper","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=548s"},{"start_seconds":557,"text":"it was an actual formal proof that they have it proven right and so now the only question is uh can we write down this","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=557s"},{"start_seconds":565,"text":"statement in a way that we can trust it right because the statement that you know like when you say hey I'm not going to lose money in in English it says easy","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=565s"},{"start_seconds":573,"text":"to express in lin not so much right so you need to express it you need to read it you need to trust it right so now the frontier move there uh and the second","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=573s"},{"start_seconds":581,"text":"question is how do you prove cheaply right so like there's a benchmark called putnam bench uh in which we recently announced uh we we solved it and we're","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=581s"},{"start_seconds":589,"text":"on the first place right now uh and it is uh sorry it's 250 times cheaper than the second best solution submission and the second best submission was like","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=589s"},{"start_seconds":598,"text":"$20,000 right which is quite pricey and ours was 111 right so that is the biggest thing we're working towards is like you know how do we prove like like","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=598s"},{"start_seconds":606,"text":"proving became feasible uh but you know it doesn't need to be just feasible it needs to be cheap right and so how do you do it cheaply that's what we've been","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=606s"},{"start_seconds":614,"text":"working on right so like the the effectively we have three directions right now one is how do you prove things very cheaply second one is how do","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=614s"},{"start_seconds":621,"text":"formalize smart contracts in a way that you can trust the formalization uh you know and the third one uh is something I","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=621s"},{"start_seconds":628,"text":"I mentioned at the beginning uh is that you also need to trust the LIN kernel and Lynn was designed for people who are","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=628s"},{"start_seconds":636,"text":"friends with each other to trust each other right like you're a mathematician you have a mathematician colleague you're sending proofs to each other you would never have incentive to to trick","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=636s"},{"start_seconds":644,"text":"each other right but now that you you know uh if I'm if I'm giving if I'm publishing a smart contract and I'm giving you a 13 million lines of proof","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=644s"},{"start_seconds":653,"text":"that it is correct. I actually have a very strong incentive uh to lie to you.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=653s"},{"start_seconds":657,"text":"Right? So at this point breaking link kernel becomes actually very desirable, right? And so we're working on uh","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=657s"},{"start_seconds":664,"text":"uh we're working on making sure that link kernel is correct, right? We're reducing it to a uh much simpler uh code","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=664s"},{"start_seconds":672,"text":"base to much simpler for system. So actually I I'd love just to like your general reaction to like","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=672s"},{"start_seconds":680,"text":"what the Navier Stokes like you know this whole situation how it's evolved.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=680s"},{"start_seconds":686,"text":"Obviously there's the privacy and the confidentiality of open AI potentially reading you know uh the chats of the","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=686s"},{"start_seconds":694,"text":"researchers that were working on this problem. But it sounds as if the frontier is no longer trying to solve the problem. it has been solved","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=694s"},{"start_seconds":703,"text":"according to lean, but now people are questioning whether lean is effective and airtight in expressing these proofs.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=703s"},{"start_seconds":710,"text":"Is that kind of the right way to think about like where this problem stands right now? I realize this is a little bit of a side quest, but it feels relevant to formal verification. So, I'm","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=710s"},{"start_seconds":719,"text":"just curious like what is your general reaction both on the privacy element of this, but then also where Navier Stokes stands right now?","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=719s"},{"start_seconds":726,"text":"Yeah, I mean I from my perspective it's it's the best highlight of everything we've been saying for the past three","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=726s"},{"start_seconds":734,"text":"years on the privacy side, right? I think it's a pretty critical that","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=734s"},{"start_seconds":740,"text":"the AI belongs to you, not to the company that provides you the service, right? And this example is just kind of","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=740s"},{"start_seconds":750,"text":"you know yet another example in a string of kind of recent uh problems. I think","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=750s"},{"start_seconds":758,"text":"the poller was the one who kind of introduced this idea that like hey the companies are effectively taking your","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=758s"},{"start_seconds":766,"text":"data and you know turning that into their own products. And there's been a lot of rumors that even if you're like","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=766s"},{"start_seconds":774,"text":"asking to not train on your data, they would create synthetic data out of it and then train on that. Uh, and I mean","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=774s"},{"start_seconds":783,"text":"obviously it's rumors so like there's no clear evidence but this example is effectively kind of confirming that like hey guys you know they effectively like","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=783s"},{"start_seconds":792,"text":"took something that had like an insight around how to do it and and and kind of expanded that right by spending","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=792s"},{"start_seconds":799,"text":"a ton of compute to uh to finish a proof. I think where on the broader side","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=799s"},{"start_seconds":807,"text":"the challenge as Alex mentioned has been in formalization itself. So like whenever you have a problem right now it's like how do you know that it's a","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=807s"},{"start_seconds":815,"text":"correctly stated problem in the first place to solve to prove and I mean Alex maybe has a better better kind of","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=815s"},{"start_seconds":822,"text":"understanding of where that stands uh latest yeah but there's no question that the","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=822s"},{"start_seconds":829,"text":"proof that openai presented is correct I mean that that is that's what I wanted to convey at the beginning is that if lean says something is correct it is","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=829s"},{"start_seconds":837,"text":"correct right with the uh discounting for the fact It could have a bug, but it's uh it's extremely unlikely that","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=837s"},{"start_seconds":844,"text":"either the Ethereum or Navier Stokes uh actually used any bugs in Lynn, right?","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=844s"},{"start_seconds":851,"text":"And and also Lynn has two kernels. So, sort of like you know how Ethereum has two clients, Lynn has two kernels and Ethereum is only correct if it passes both and they independently developed.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=851s"},{"start_seconds":860,"text":"Uh it is it's still not like if the model was malicious, it could potentially find two different bugs in both, right?","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=860s"},{"start_seconds":869,"text":"create like you know like like little u uh you know little hidden gems in its proof that that utilize both to prove it","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=869s"},{"start_seconds":877,"text":"eventually right but it's uh yeah it's it's highly unlikely that this is the route it took right and luckily we can still inspect the reasoning right so","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=877s"},{"start_seconds":885,"text":"hopefully both entropic and open looked at those and like you would see if it says hey I cannot prove it let me just find a zero day uh right you you you","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=885s"},{"start_seconds":893,"text":"would notice it yeah yeah so Alex one of the things that you were saying um you know kind of previously explain explaining the value of what you guys are doing with lean in.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=893s"},{"start_seconds":900,"text":"Formal verification is just this drastic reduction in cost to basically formally verify and um get to the conclusion of","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=900s"},{"start_seconds":910,"text":"verifiable truth, you could say. And I actually had a really interesting podcast here a couple days ago with a with a fellow big- time investor who","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=910s"},{"start_seconds":919,"text":"spoke about SpaceX and how their cost to bring one kilogram of matter to space has gone from $20,000 previously, you","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=919s"},{"start_seconds":928,"text":"know, prior to SpaceX to now down to about $100. So, you know, a massive massive massive reduction in cost. And","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=928s"},{"start_seconds":938,"text":"then what is the result of this is this massive opening of a new TAM of if we can get a lot more matter into space we can do a lot more up there. We can build","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=938s"},{"start_seconds":947,"text":"data centers up there. We can we can do anti-uclear right. So there's this whole kind of like concept of and in any kind of market reduce the cost to you know","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=947s"},{"start_seconds":955,"text":"achieve an outcome and then scale. And so when it comes to this by reducing the cost of formal verification by reducing","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=955s"},{"start_seconds":962,"text":"the cost of this kind of proofs Ilia I'm curious from your perspective more from like the founder side and then Alex on the tech side what becomes possible","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=962s"},{"start_seconds":970,"text":"right like what are you what what are you taking advantage of from the near side due to this drastic reduction in cost um and and how do you kind of","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=970s"},{"start_seconds":979,"text":"expand the market for what you guys are building?","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=979s"},{"start_seconds":984,"text":"Yeah, I think so from a software engineering perspective, from kind of building products, the slow part is not","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=984s"},{"start_seconds":992,"text":"anymore the building, it's validation, right? Like my agent can write, you know, millions of code overnight, but I","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=992s"},{"start_seconds":999,"text":"will have no idea, right, if it's doing stuff correctly. And so the bottleneck effectively moved from writing code to","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=999s"},{"start_seconds":1007,"text":"validation, verification, and relying on human reviews just doesn't work, right?","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1007s"},{"start_seconds":1012,"text":"you're effectively still using an agent to review it. And so that kind of gets into like, you know, AI reviewing AI, which we know uh doesn't always work as","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1012s"},{"start_seconds":1021,"text":"well. And so for formal verification as a framework allows us to uh shift from","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1021s"},{"start_seconds":1029,"text":"this human validation and you know AI validation to actually have a formal validation of what the code does, right?","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1029s"},{"start_seconds":1035,"text":"And this is especially you know important when you're dealing with a lot of money, right? when you this is blockchain code, this is smart","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1035s"},{"start_seconds":1042,"text":"contracts, um you know intents etc or anything else that's mission critical, you want to have a validation of","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1042s"},{"start_seconds":1051,"text":"correctness of that code down to the properties you care about, right? So you the money you you know trading in and","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1051s"},{"start_seconds":1059,"text":"saying you expecting this outcome, right? It should come out come out on the other side. And again before this was both slow and expensive, right?","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1059s"},{"start_seconds":1069,"text":"before like we would write a smart contract we would you know give it to auditors maybe you know there's like few firms that were doing kind of manual","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1069s"},{"start_seconds":1078,"text":"formification and you know 3 months later they would give you an audit report right maybe you fix some stuff but like the development speed of of","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1078s"},{"start_seconds":1086,"text":"kind of this engineering was extremely slow and so the idea here is that you have something that's fast intelligent and can plug in directly into your kind","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1086s"},{"start_seconds":1096,"text":"of continuous integration process where you can effectively verify that you know whatever change you did still uh proves","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1096s"},{"start_seconds":1103,"text":"down the properties that your users care about. And then from there this should be expanded beyond just you know smart","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1103s"},{"start_seconds":1111,"text":"contracts, money, blockchain but to things that you know we're really uh relying on that people don't think about","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1111s"},{"start_seconds":1118,"text":"which is like networking stack and you know other layers of kind of computing where we actually have a lot of zero day","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1118s"},{"start_seconds":1126,"text":"vulnerabilities that keep getting found right. And uh I mean there was like I don't know if you remember like a year ago there's a vulnerability where","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1126s"},{"start_seconds":1133,"text":"somebody could text you a image in on iPhone and it like effectively root your root your iPhone and like steal your","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1133s"},{"start_seconds":1141,"text":"crypto right and people were targeted in crypto with that right so this type of things you know should be formally verified to ensure that these kind of","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1141s"},{"start_seconds":1148,"text":"things doesn't happen so but that requires you know like iPhone iOS code base right there's millions of lines of","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1148s"},{"start_seconds":1156,"text":"code so you need something that can actually like verify cheaply across large code bases and have","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1156s"},{"start_seconds":1163,"text":"broader and broader properties. But I think the the big kind of question mark and this is still active research is how","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1163s"},{"start_seconds":1170,"text":"do we easier and easier now formalize and define what are the criteria that that needed to be proved. Right? So","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1170s"},{"start_seconds":1177,"text":"beyond you know simple like swaps and kind of multiigs etc which are pretty simple to do uh like for something as","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1177s"},{"start_seconds":1184,"text":"complex as like you know no way to exfiltrate your private keys. Uh there would be a really nice property right that if your private key never leaves","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1184s"},{"start_seconds":1192,"text":"your machine if you can just prove that for your operating system now you know at least you know it's not possible. So","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1192s"},{"start_seconds":1200,"text":"um so this is kind of things that you know will become possible now with this technology becoming cheaper and cheaper.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1200s"},{"start_seconds":1207,"text":"given that um you know you guys are sort of taking uh a pi like a leadership role in formal verification one of the few","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1207s"},{"start_seconds":1216,"text":"blockchains that has gone and done this so far. You guys are implementing this into Near and we anticipate that this is something that is going to fit into","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1216s"},{"start_seconds":1224,"text":"pretty much not only every facet of blockchains and crypto but also broadly software stacks you know outside of","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1224s"},{"start_seconds":1232,"text":"crypto. Is there a chance that you know the work that you guys do internally at Near, you'll kind of create like a","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1232s"},{"start_seconds":1239,"text":"formal verification product and it won't really look like a blockchain product, but it'll be something that maybe like I don't know Near Labs is going to add to","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1239s"},{"start_seconds":1247,"text":"its product stack and then you know you can you guys can kind of offer that to companies that are looking at increasing","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1247s"},{"start_seconds":1254,"text":"formal verification across their own product stack.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1254s"},{"start_seconds":1259,"text":"Yeah, potentially. I mean we have right now the neari the the agent that Alex built that effectively scorn and platinum bench it is under neari um it","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1259s"},{"start_seconds":1267,"text":"is open source people can run it and then yeah as we continue advancing this u it makes sense to productionize and","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1267s"},{"start_seconds":1275,"text":"kind of offer neari suite and then Alex just kind of uh closing","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1275s"},{"start_seconds":1281,"text":"out here on the kind of world that we're heading towards right with just kind of the we spoke spoke to E-mod, the","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1281s"},{"start_seconds":1290,"text":"exfounder of stability AI here on our AI show with Near and he basically described that we've we've now reached","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1290s"},{"start_seconds":1298,"text":"what he calls competent intelligence with AI, right? So, we're kind of at the point where it's it's getting to that point where it's pretty damn competent.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1298s"},{"start_seconds":1306,"text":"Just talk to us about this future world of accelerating intelligence and why you feel that building these formal formal","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1306s"},{"start_seconds":1314,"text":"verification systems are so crucial to this future world that we're entering.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1314s"},{"start_seconds":1319,"text":"Yeah, that's that's a great question and I I think a very good way to think about it is like like I'm pretty sure everyone today who's who's using like cloud code","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1319s"},{"start_seconds":1327,"text":"or codeex right have experienced in many many times this feeling where you you build like you might still want to","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1327s"},{"start_seconds":1335,"text":"review code that it's writing right but it's just becoming it's producing so much code so much um","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1335s"},{"start_seconds":1342,"text":"uh yeah it creates so much that it's it becomes completely infeasible for us to review it in any meaningful way, right?","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1342s"},{"start_seconds":1348,"text":"So, I think a very large number of people at this point switch to the mode where either they like build with one review with another or just build with one and like yeah, it's probably","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1348s"},{"start_seconds":1356,"text":"correct. Let me let me use it as is. And uh and it's only going to be getting worse, right? AI is getting better and better uh faster and faster, right? So,","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1356s"},{"start_seconds":1365,"text":"we're going to be creating more and more uh uh uh artifacts with it, right? Right. And","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1365s"},{"start_seconds":1373,"text":"I think formal verification here is extremely helpful because it can it it allows you to create a very large codebase, a very large product, right?","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1373s"},{"start_seconds":1381,"text":"And then a relatively small spec that you as a human actually is able to read.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1381s"},{"start_seconds":1386,"text":"Prove it, right? And then and then you can say, hey, a AI created for me this massive thing that I wanted, right? It is way beyond my capability at this","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1386s"},{"start_seconds":1394,"text":"point to review it, right? But I want I cared about this this and this property.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1394s"},{"start_seconds":1399,"text":"And here I have formal proofs that the thing it built does satisfy the proof which is right. So I can use it. Right?","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1399s"},{"start_seconds":1405,"text":"So that will allow us uh to to trust AI in building much more complex systems that we can reasonably trust it today uh","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1405s"},{"start_seconds":1412,"text":"and still be certain uh that they are correct and uh effectively still be able to an extent","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1412s"},{"start_seconds":1419,"text":"inspect what is what is actually being created without without trusting it blindly.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1419s"},{"start_seconds":1425,"text":"Awesome gentlemen. Great work and we appreciate your time. I want to take this last minute here to just introduce","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1425s"},{"start_seconds":1433,"text":"the Let's get to the full screen now, please. Um, we're going to do the rollup persp launch, guys. Um, we have now launching the roll-up persp.ne.com.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1433s"},{"start_seconds":1452,"text":"Yes, all you people in the chat who are bullish on Nearcat. Yes, all you people in the chat who are saying near is going to rip. You guys can trade, you guys can","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1452s"},{"start_seconds":1461,"text":"swap, you guys can do intense all on the rollup.nneer.com.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1461s"},{"start_seconds":1465,"text":"This is the initial launch of what we're doing. And so basically, it's super simple. You just come in here, you create you create an account. All rollup","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1465s"},{"start_seconds":1474,"text":"traders that sign up through our website keep 20% of their platform fees in near tokens. We are also going to be doing a","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1474s"},{"start_seconds":1482,"text":"giveaway that we will announce towards the end of the stream and after the stream. It's it's a near.com front end.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1482s"},{"start_seconds":1489,"text":"You come in, you click create account, it redirects you to near.com and then you're good to go. And so this is the initial iteration and we can come back","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1489s"},{"start_seconds":1498,"text":"to to us and close out here. And just to kind of give you guys our vision, the rollup has this media and distribution channel. We have this massive audience.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1498s"},{"start_seconds":1507,"text":"Near.com is, you know, and obviously they're a partner of the show and we appreciate Alex and Ilia. This is the one of the best onchain trading","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1507s"},{"start_seconds":1514,"text":"experiences I've ever used. We've traded I've been trading on it for months now.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1514s"},{"start_seconds":1518,"text":"Per, swaps, transfers, cells, everything. It is so goddamn easy. Pass key. So easy. Any chain, you don't need","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1518s"},{"start_seconds":1527,"text":"to think about chains. You don't need to think about wallets. It's just all there. So, don't think about gas as well.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1527s"},{"start_seconds":1533,"text":"Nothing. Yeah. It's just like I just want to get long or shorter. And so guys, we're going to be trading live on the show a ton more. We're going to be","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1533s"},{"start_seconds":1541,"text":"incentivizing the usage of this in the uh initial period. So, I'm going to drop the link in the chat to all the channels, guys. Sign up. We're doing a","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1541s"},{"start_seconds":1549,"text":"thousand USDC giveaway to give this uh a big kickoff. And the roll-ups, pers, and intents are now live. Um Ilia, Alex, any closing thoughts on this?","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1549s"},{"start_seconds":1561,"text":"Well, I mean, excited for you guys to launch this. Um I think everybody should roll up their sleeves and uh go use it.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1561s"},{"start_seconds":1567,"text":"[snorts]","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1567s"},{"start_seconds":1568,"text":"Uh but yeah, I think the the broader vision of like this unified liquidity that is private that is, you know,","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1568s"},{"start_seconds":1576,"text":"unites kind of AI and blockchain is life, right? And I think kind of the privacy is now the core thesis both for","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1576s"},{"start_seconds":1585,"text":"AI and for blockchain. I think privacy is freedom. Privacy is peace of mind as well. like when I you know do anything","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1585s"},{"start_seconds":1593,"text":"on chain now through near.com I don't need to think about you know where this data will come out and similarly when I","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1593s"},{"start_seconds":1600,"text":"use you know nearai I don't need to think about you know like I actually got banned by open AAI for for some stuff I was doing on like doing like actually","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1600s"},{"start_seconds":1609,"text":"doing trying to test cyber uh security stuff of a system but like you know it I'm effectively trying to attack right","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1609s"},{"start_seconds":1617,"text":"so they banned me so like this is where you need you know uh privacy because you can actually use stuff and not like double think of what's going to happen.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1617s"},{"start_seconds":1626,"text":"So yeah, excited excited to partner with you guys. Excited to see this uh rolling out. Uh and yeah.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1626s"},{"start_seconds":1633,"text":"Yeah. Awesome. Thank you, Alex, for joining us as well.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1633s"},{"start_seconds":1637,"text":"Thank you, Ilia. I think we're going to move on to our next panel here. I really appreciate your time. And just one last word for me is that you know this is kind of like the very beginning. It's","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1637s"},{"start_seconds":1646,"text":"like our V.01. We're already talking with different teams about launching rollup vaults about expanding veneer AI","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1646s"},{"start_seconds":1653,"text":"uh with the Venice API capabilities into the site to kind of have more of like a you know robo advisor. Um and there's","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1653s"},{"start_seconds":1661,"text":"just more and more that we're trying to build into this into our own website as well and kind of bring this all together. You know we think we think","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1661s"},{"start_seconds":1668,"text":"that the future of media and markets are going to go hand in hand. If Robbie and Andy have good ideas, they are long a position, short a position, they're, you","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1668s"},{"start_seconds":1677,"text":"know, there's a rumor that's buzzing, we we want people to take action on that.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1677s"},{"start_seconds":1681,"text":"Um, and we want people to take action on this website on the rollup.nneer.com.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1681s"},{"start_seconds":1686,"text":"So guys, thanks for being a part of the show today and we got a long road ahead.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1686s"},{"start_seconds":1690,"text":"So, uh, appreciate you guys being the first guests.","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1690s"},{"start_seconds":1695,"text":"Thanks so much, Jent. Couldn't do without you","url":"https://www.youtube.com/watch?v=tsVo1-TGnQM&t=1695s"}],"youtube_url":"https://youtube.com/watch?v=tsVo1-TGnQM","url":"https://near-pedia.xyz/videos/tsVo1-TGnQM"}