WEBVTT 00:00.000 --> 00:15.480 Yes, so hello everyone, I'm happy to be there and at the end of the first day, I've 00:15.480 --> 00:22.800 been a spectator to talk to you about formal verification, it's a technique to analyze 00:22.800 --> 00:32.240 code and to make a full coverage by making a mathematical analysis of a code, so we'll 00:32.240 --> 00:42.400 present you what it is in the big lines on how we can apply it, so MGM and I'm worked 00:42.400 --> 00:50.480 in the formal methods for maybe 10 or 15 years, since as a PhD student and after I've 00:50.480 --> 01:00.600 studied formal and agency to do formal verification, especially for the blockchain industry, 01:00.600 --> 01:07.580 so the motivation of formal methods is to go beyond testing, because even if testing is a very 01:07.580 --> 01:17.040 effective full effective in practice, we know we can always miss bugs, because it cannot cover 01:17.040 --> 01:25.080 all the scenarios, especially user can be very creative, as well as attackers, so we 01:25.080 --> 01:30.600 use this, for example, from a digital, seeing that testing can show the presence of bugs, 01:30.600 --> 01:43.480 but it cannot show that there are no bugs remaining, so it's been a few bugs, but because 01:43.560 --> 01:50.200 the big loss, so one of the things I often quoted is the bug of Iron 5, with a wall 01:50.200 --> 01:58.360 rocket explaining due to a bug, so there are domains where a single bug can cause loss of 01:58.360 --> 02:07.480 material or even loss of life, for example in trains or cars, for what we want to have 02:07.560 --> 02:18.440 mitodology at our reliable to find all the bugs, also there's a geopolitics, so all the 02:18.440 --> 02:25.320 pay agencies in the world they want to find the reliability to be able to attack over states, for 02:25.320 --> 02:34.360 example, the most recent, maybe Maduro, Maduro was taken by the US, they made an attack on the 02:34.440 --> 02:42.440 ground, but also a cyber attack to get the power lines, so it shows that if you're a president, 02:43.240 --> 02:54.040 you are concerned by the security and the government who invest more in protecting their systems, 02:55.240 --> 03:02.120 in the blockchain world, there's a North Korea that is expected to be behind a lot of big 03:02.200 --> 03:14.680 attacks, and they have, of course, great means to find all the bugs, and no big ripe coding wave, 03:14.680 --> 03:19.720 with a lot of people producing more and more code, and it's very hard to make sure that everything 03:19.720 --> 03:28.600 is correct, and in particular, they are good at writing code, but to make sure that everything is 03:28.600 --> 03:37.480 correct, it's a much harder because of a still-educination, and today there are no, there are a lot of 03:37.480 --> 03:44.840 offers to find bugs automatically with agents, especially the cyber security, but we see that 03:44.840 --> 03:50.440 varsity, the kind of bugs that they cannot find will Iably, like access control errors, 03:51.400 --> 04:00.440 for bad, it means that we need to better run more systematic tools, so for more 04:00.440 --> 04:08.120 verification, it's a mathematical method to ensure that a program is bug free for any possible input, 04:10.120 --> 04:15.560 so I don't know if some of you are familiar with the subject, 04:15.560 --> 04:27.640 but when I first saw it, I find bad surprising for many reasons, first of all, we say bug free, 04:28.440 --> 04:37.400 while we have the habit of seeing that a code is never 100% safe, but actually for 04:37.400 --> 04:43.560 programming languages, when we think about that, it's a fully deterministic, when we go down to 04:43.560 --> 04:50.760 the definition, it's 0-1-1, because the code will always return the same result every time we 04:50.760 --> 04:59.960 run it, at least when it's sequential code, why not having an idea that a code can be perfect, 05:01.000 --> 05:09.640 but we can prove that a code is a well-eback free, so the big drawback, of course, is that it's 05:10.440 --> 05:18.680 bug free or safe for given specifications, so we need to write a formal definition of what is considered 05:18.680 --> 05:28.920 as a bug or not a bug or a feature. Second surprise, maybe it's mathematical, so we are used to do 05:28.920 --> 05:39.000 math on a number of matrices or geometry, but there are also formulas to reason about code, 05:39.000 --> 05:48.360 to say what is a loop function, and this is a theory that is also behind the work of 05:48.360 --> 05:54.680 compilers to make sure that when we go from a long graduate of a top, don't do the assembly, 05:54.920 --> 06:03.000 we propagate the evaluation rules, it's quite interesting, and the third surprise is that we can 06:03.000 --> 06:12.200 cover all the all-in boots, even if in general there are infinitely many, or an exponential number, 06:12.760 --> 06:17.880 and this is because we are doing mathematical reasoning, we reason about a sense of value, 06:17.880 --> 06:24.680 what can be an infinite aim, so we can cover much more entries, and we are testing 06:24.680 --> 06:33.640 your testing test, for example, so we will directly show what is a concrete example of 06:33.640 --> 06:40.280 formal verification in the rock language, which was a previously named code, 06:40.600 --> 06:50.360 so for formal verification there are many different technologies, but all of them, 06:50.360 --> 06:55.640 we rely on some languages, but are related to programming languages, but a bit different, 06:55.640 --> 07:07.960 and especially more strict, and in rock, it's a language similar to a camel or a bit similar to 07:07.960 --> 07:14.760 the worst, as well, you can define a list, which is equivalent here for an enamine in rust, 07:15.640 --> 07:23.320 seeing that a list is a new type, which is polymorphic in A, and for two cases, the case where the list is 07:23.320 --> 07:30.200 empty, and the case where we have a head of a list on the rest of a list, and we can fill the 07:31.080 --> 07:40.600 linked list like that, so we have a small programming language, we can define functions, 07:40.600 --> 07:47.240 for example, to define the length of a list, we do much like in a in rust, and we can iterate, 07:47.880 --> 07:53.640 seeing that the list of Lyam Tiles, the length of the Lyam Tiles is 0, and when we have one 07:53.640 --> 08:01.720 more element, we take S, that is a successor for plus 1, so we compute one plus 1 plus 1 for 08:01.720 --> 08:08.200 all the elements of a list, and we have a lens, we can define other functions like for an 08:08.200 --> 08:18.040 but here the concatenation of to list, and the new thing that is not very programming languages, 08:18.520 --> 08:26.920 is that we can also stay properties, for example here we stay for any list L1 and L2, 08:27.560 --> 08:34.040 the length of concatenation is the sum of the length, it's quite a simple property, 08:35.160 --> 08:40.760 but with testing, we call only observe this property on a few examples, 08:41.320 --> 08:49.480 where we can actually cover all possible lists, and how do we do that, that we have also 08:49.480 --> 08:56.600 a part of a language, that is very to white mathematical proof, and we will do a reasoning about 08:56.600 --> 09:05.160 the code, with a few ingredients, I can verify any, almost any kind of program, so the first thing 09:05.160 --> 09:11.160 we do is that we consider any list L1 and L2, we have a pre-saysing anything, 09:11.160 --> 09:22.200 it's just a variable names, how we can talk about any list, and after we use the 09:22.200 --> 09:28.920 induction principle, so in the same way that when we return on integers, we can do proof by 09:28.920 --> 09:35.800 inducing that we show the case 0, and the case n plus 1, assuming that the case n is okay, 09:37.480 --> 09:44.200 it's principal, it can be realized also to list where we return about the list is empty, 09:44.200 --> 09:51.160 or the case where the list is a head element followed by the rest of the list, and when the list is 09:51.160 --> 10:00.280 empty, we can do, we can evaluate this expression, and we will return 0 on both sides, so we use 10:00.280 --> 10:05.320 a flexibility, say value of the equality is trivial, because it's a same thing on both sides, 10:06.680 --> 10:14.600 and for the induction case, we will have, but we have this equality for the rest of the list, 10:15.160 --> 10:23.720 and using this equality with the rewriting, we get back to the fact that the two sides are 10:23.720 --> 10:29.880 equal, and when we do cure this, the root system will check that our proof is actually correct, 10:31.160 --> 10:35.560 so the system is search, but if we make any mistake in the proof, 10:36.920 --> 10:41.400 or if the statement is not correct, we will never be able to wish to be n, 10:42.360 --> 10:49.400 and there is a small kernel, but people have been working on to make sure that there are no 10:50.120 --> 11:00.600 venerabilities or no bells meet, and to give a view also in a text editor, so it's very small, 11:00.600 --> 11:07.000 but generally you have your proof, you have a green portion, which is what is validated, 11:07.560 --> 11:16.040 you want to make the green go to the end of a file, and on the other side, you get what are your current hypothesis, 11:16.040 --> 11:21.080 and what is your current target, and you want to make sure that your target is smaller, 11:21.080 --> 11:29.000 smaller until it's obvious, so it's feels like a game, to find the white command to reduce the 11:29.000 --> 11:31.800 target goal until it's correct and everything is green, 11:31.800 --> 11:42.360 and who is using that, so there are many critical industries, like spacing industry, transport, 11:42.360 --> 11:49.240 defense, and also finance, especially blockchain, where the vulnerability can enable to still a lot of 11:49.240 --> 11:57.720 money very quickly, because it's not regulated, it's not centralized, so, 11:57.720 --> 12:10.520 but actually, even for those critical industries, the use is rather limited, and the main reason is the cost, 12:14.040 --> 12:19.880 and some estimates that it's 10 times more expensive to formally verify the code, 12:19.880 --> 12:26.360 than to white it, I think it greatly depends on the domain and the scope of verification, 12:27.320 --> 12:31.880 but the hopes is that we've a technical progress that are always going on, 12:31.880 --> 12:38.360 active with search project, and also with the help of AI, we can automate as much as possible 12:38.360 --> 12:49.560 the boring stuff, and especially in our role of vibrating the idea of writing code by starting from 12:49.640 --> 12:58.280 a spec, I think it's kind of a new trend, to be able to manage more code when it's 12:58.280 --> 13:03.960 the twiten by a human anymore, maybe a form of verification will be more popular, 13:06.600 --> 13:10.520 and in case of a property that we check on the code, 13:11.240 --> 13:18.280 first property we check is that there are no one time errors, so it means that there is no 13:18.280 --> 13:25.080 panic or segmentation fault, for example, and after another interesting one is that there are 13:25.080 --> 13:30.600 no restrictions, so that when you make an optimization of an existing code, you always get the 13:30.600 --> 13:39.080 same result for the same inputs, the functional correctness means that you show that your code 13:39.800 --> 13:45.640 behaves like reference simplifying implementation describing what it's supposed to do, 13:47.400 --> 13:51.240 and after you can create business rules also about a specific two-year domain, 13:52.040 --> 13:58.920 say that, for example, a user that is not admin is not supposed to access to certain set of values 14:00.040 --> 14:06.760 or things like that, and you need to define your business logic rules correctly, 14:07.000 --> 14:13.000 but you know, let's see, we attack surface is smaller when all of the code, 14:15.080 --> 14:19.560 there are many, many methods, it's a big bit of spectrum, 14:21.480 --> 14:28.120 it can start with phasing test and a property best test, and go up to the CRM Prover, 14:28.120 --> 14:35.000 a full form of verification approach, and even in the form of verification itself, 14:35.880 --> 14:41.720 there are many different tools, I think the two main categories are automated proofers and interactive 14:41.720 --> 14:47.400 proofers, we have a difference, it's when to have the right-hand specification, 14:48.040 --> 14:54.040 is the tool to automatically show that it's correct, or is it waiting for interaction with you 14:54.600 --> 15:04.120 to have some hints, so the automated proofers are typically less expressive and for a full 15:04.120 --> 15:11.880 menu, interactive ones, but interactive ones are also more complex, but it's comfortable to know 15:11.880 --> 15:17.400 that you will never be stuck when you use interactive proofers such as the Rock language, 15:17.400 --> 15:27.000 what I have shown, and I hope also that with AI it will be simpler, 15:27.720 --> 15:32.520 because since the indirect proof of a language AI can talk with systems, 15:33.080 --> 15:35.960 it has been a few investments like Armonic, 15:35.960 --> 15:43.000 in the logical intelligence recently, and this domain to use LLMs to talk to interactive proofers, 15:45.800 --> 15:52.280 the main languages are Rock, I was the one of the first one, 15:53.040 --> 15:59.320 Lina Agban, derivatives of Th objective-language, so they the word aforean language. 15:59.880 --> 16:06.200 So 11, 11,Müzik of coding, so we're chasing the first three move, 16:06.200 --> 16:12.360 so we're chasing the second, mission, nothing of that. 16:12.360 --> 16:18.120 So the first two moves, where we call atonement, 16:18.120 --> 16:20.420 the first time someone achieved to make 16:20.420 --> 16:22.520 a long-dike el culus extension. 16:22.520 --> 16:26.320 So minimal long-range, that is mixing well, 16:26.320 --> 16:30.920 programs and proofs in a way that things are. 16:30.920 --> 16:34.660 That you cannot make longer proofs and still 16:34.660 --> 16:35.900 white code. 16:38.600 --> 16:45.100 It's quite a good achievement where it was discovered. 16:45.100 --> 16:48.180 So it's both programming language. 16:48.180 --> 16:53.740 Like we have seen on the master language at the same time. 16:53.740 --> 16:56.340 So it means you can write proofs about your code, 16:56.340 --> 16:59.860 to show property that are always true programs. 16:59.860 --> 17:02.340 And you can even use it to be over where one, 17:02.340 --> 17:05.580 to write code, but it's generating proofs. 17:05.580 --> 17:07.860 So you can make decisions, procedures. 17:07.860 --> 17:10.780 So I have, for example, to be able to compute 17:10.780 --> 17:13.180 the vendor properties to our false. 17:13.180 --> 17:18.460 So you can use it both ways, very elegant, 17:18.460 --> 17:21.820 and there is a feature of dependent types, 17:21.820 --> 17:23.660 meaning that, for example, in C, 17:23.660 --> 17:29.580 when you have a certain size, you need to have the size 17:29.580 --> 17:33.180 that is almost always a constant, but there 17:33.180 --> 17:35.780 can be any expressions. 17:35.780 --> 17:37.940 And it will type check that, and you 17:37.940 --> 17:41.140 can be able to mix types and values freely. 17:45.380 --> 17:49.420 And in practice, to use such systems, 17:49.420 --> 17:51.420 we always have two steps. 17:51.420 --> 17:54.740 One is the translation from your programs, 17:54.740 --> 17:57.780 two formal systems. 17:57.780 --> 18:01.100 And after that, writing the specification 18:01.100 --> 18:05.540 and making the verification, the two steps are 18:05.540 --> 18:08.540 about a similar level of complexity, we'll see. 18:11.540 --> 18:14.980 The lightweight approach will do the translation 18:14.980 --> 18:17.420 from a global risk response program, 18:17.420 --> 18:23.540 a link, a counter, to the Rob system by hand. 18:23.540 --> 18:25.860 So this is convenient because it's very fast, 18:25.860 --> 18:29.060 but you can mix some details. 18:29.060 --> 18:32.300 Typically, here, the integers are 60 for bytes. 18:32.300 --> 18:35.740 So it means you have a overflow. 18:35.740 --> 18:37.820 And in this translation, it's a simplified, 18:37.820 --> 18:43.580 we use an abundant integer, but it can still 18:43.580 --> 18:45.860 be relevant to capture the main business logic 18:45.860 --> 18:50.660 and verify the main properties of some programs. 18:50.660 --> 18:53.820 If we want the full analysis of some code capturing 18:53.820 --> 18:57.420 all the details, like integers, size under everything, 18:57.420 --> 19:01.460 making sure we do not make any typo, 19:01.500 --> 19:03.940 we need a transpiler from the programming languages, 19:03.940 --> 19:06.780 to the formal systems. 19:06.780 --> 19:10.060 So for me, we have developed a few transpilers 19:10.060 --> 19:14.140 for various languages, with OKML as well, 19:14.140 --> 19:21.020 to the ROG system, taking the same examples, 19:21.020 --> 19:25.340 the generated code is much longer and a little horizontal. 19:25.340 --> 19:26.300 It can fit a bit. 19:26.300 --> 19:31.980 After inside the ROG system, we can prove 19:31.980 --> 19:34.460 that it's equivalent to this code, but it's similar 19:34.460 --> 19:38.860 to the ROG on the one, and the right type for the 64 byte, 19:38.860 --> 19:42.900 a 64 bits integer, and we can prove 19:42.900 --> 19:47.660 a property that the max values in the ROG 19:47.660 --> 19:54.660 are going to go down, as we show the expected from this. 19:54.660 --> 20:00.100 We have every incandone, so that way, 20:00.100 --> 20:04.140 we can have a fairly up-tarier risk-odd for up-tarier 20:04.140 --> 20:07.140 properties. 20:07.140 --> 20:09.540 On the last project we have made, we have to 20:09.540 --> 20:13.900 verify the ROG circuit, cryptographic programs, 20:13.900 --> 20:18.620 and the implementation of the Ethereum virtual machine, 20:18.620 --> 20:21.740 for solidity smart contracts, that is a whiter in the rest. 20:25.020 --> 20:27.460 So we have everything is open source. 20:27.460 --> 20:30.300 We have a web-ish things on our GitHub, 20:30.300 --> 20:34.900 and with the document also on our blog, 20:34.900 --> 20:41.300 we'll invite you to test, and for 2026, 20:41.300 --> 20:44.940 so my wish is that with the AI, 20:44.940 --> 20:49.340 we'll be able to see much border use of formal verification, 20:49.340 --> 20:51.540 so it will be nice, maybe, to achieve 20:51.540 --> 20:53.980 their findings, some open source projects, 20:53.980 --> 20:57.980 but are heavily used, like the TABS system, 20:57.980 --> 21:03.380 or the next commands, as well, 21:03.380 --> 21:05.940 making the use of formal verification, 21:05.940 --> 21:08.980 more important in our enterprise projects. 21:08.980 --> 21:12.180 So I think that because, by cutting, 21:12.180 --> 21:15.700 really hard to know whether the code is secure or not, 21:15.700 --> 21:18.260 there are ways to do laterate formal verification, 21:18.260 --> 21:26.900 to verify, for example, the control rules of software. 21:26.900 --> 21:31.180 Or maybe one other way to make the right-cutting scale, 21:31.180 --> 21:34.900 it would be good enough, safety. 21:34.900 --> 21:37.860 So we'll see, at the end of here. 21:37.940 --> 21:39.660 And yes, yes, thanks. 21:39.660 --> 21:42.340 Catch you next time. 21:42.340 --> 21:43.300 Thank you. 21:45.820 --> 21:47.500 Yeah. 21:48.500 --> 21:51.660 I can just get some sleep from here? 21:52.660 --> 21:57.020 I got very logged, although it was very insightful, 21:57.020 --> 21:59.660 and I was incompetent, in my perspective. 21:59.660 --> 22:01.200 I'm simply falling for someone, 22:01.200 --> 22:06.340 but it is to experience a complicated and long-セ 애� page 22:06.340 --> 22:18.340 You have a full set of files when you then point for proof that a regularity test would be the more advanced way to test the performance test. 22:18.340 --> 22:19.340 Yes. 22:19.340 --> 22:23.340 And I just have a little bit of information. 22:23.340 --> 22:27.340 And for me, the faster questions of proof can be learned in this case. 22:27.340 --> 22:30.340 I guess I can move a bit of this slide. 22:30.340 --> 22:33.340 But I also can make good points for you to write. 22:33.340 --> 22:34.340 Yes. 22:34.340 --> 22:35.340 Yes. 22:35.340 --> 22:36.340 Yes. 22:36.340 --> 22:37.340 Yes. 22:37.340 --> 22:38.340 Yes. 22:38.340 --> 22:39.340 Yes. 22:39.340 --> 22:40.340 Yes. 22:40.340 --> 22:41.340 We work this way. 22:41.340 --> 22:44.340 We sell this as a service as a service company. 22:44.340 --> 22:48.340 It's a solution to space for it. 22:48.340 --> 22:52.340 Otherwise, I think that for for more language, even if you use automated proofers, 22:52.340 --> 22:55.340 you can still need to learn how to use them. 22:55.340 --> 22:56.340 Yes. 22:56.340 --> 23:02.340 For automated proofers, you will need to learn how to split your specification in a piece that can be verified automatically. 23:03.340 --> 23:11.340 So I think it's kind of like learning about front end when you are back end or things like about necessarily text time. 23:11.340 --> 23:18.340 We have a catalogue of software that when writing the proof inside is an extraction. 23:18.340 --> 23:19.340 Yes. 23:19.340 --> 23:22.340 You get some feedback. 23:22.340 --> 23:35.340 You mean like some guides? 23:35.340 --> 23:38.340 For example, showcase. 23:38.340 --> 23:42.340 I think the biggest showcase was the Tesas project. 23:42.340 --> 23:45.340 Translating the core of the Tesas blockchain. 23:45.340 --> 23:51.340 It was one of the lines of OKML to work and then sharing parts of it. 23:51.340 --> 23:56.340 So we didn't find really a lot of bugs because it was already heavily. 23:56.340 --> 23:59.340 Yes. 23:59.340 --> 24:03.340 One quick question here at the back. 24:03.340 --> 24:08.340 Actually, hopefully very far it's a translation of pro practice. 24:08.340 --> 24:11.340 This was the same question for the whole language. 24:11.340 --> 24:12.340 Yes. 24:12.340 --> 24:15.340 But we have not very far did. 24:15.340 --> 24:20.340 One of the reasons is that for most of the language, we do not have a formal specification of the language itself. 24:20.340 --> 24:25.340 And also it's quite difficult to do. 24:25.340 --> 24:31.340 But we try to minimize the translation for example for rest to rock. 24:31.340 --> 24:37.340 We take the processing tax free and directly import it one to one. 24:37.340 --> 24:40.340 And after we define the semantics through this in rock. 24:40.340 --> 24:46.340 So we have no logic to be able to stress as much as possible translation. 24:47.340 --> 24:48.340 Yeah. 25:05.340 --> 25:06.340 Yes. 25:06.340 --> 25:07.340 Yes. 25:07.340 --> 25:09.340 So we have not verified the problem in floods. 25:09.340 --> 25:10.340 I think so. 25:10.340 --> 25:13.340 Some libraries formalizing clear how floods behave. 25:13.340 --> 25:15.340 Some projects have been done. 25:15.340 --> 25:17.340 Some projects have been done about floods. 25:17.340 --> 25:21.340 But I think in general, people do not use floods for critical code. 25:21.340 --> 25:25.340 We will just assume that it computes something but we. 25:25.340 --> 25:26.340 Yeah. 25:26.340 --> 25:27.340 Thank you. 25:27.340 --> 25:29.340 Thank you.