WEBVTT Kind: captions Language: en 00:00:00.510 --> 00:00:19.070 align:start position:0% [Music] 00:00:19.070 --> 00:00:19.080 align:start position:0% 00:00:19.080 --> 00:00:22.390 align:start position:0% so<00:00:19.680> I<00:00:19.880> guess<00:00:20.080> we<00:00:20.240> all<00:00:20.480> agree<00:00:20.920> that<00:00:21.560> uh<00:00:22.160> it's 00:00:22.390 --> 00:00:22.400 align:start position:0% so I guess we all agree that uh it's 00:00:22.400 --> 00:00:25.910 align:start position:0% so I guess we all agree that uh it's really<00:00:22.680> really<00:00:22.920> hard<00:00:23.199> to<00:00:23.560> write<00:00:24.480> 100%<00:00:25.480> uh 00:00:25.910 --> 00:00:25.920 align:start position:0% really really hard to write 100% uh 00:00:25.920 --> 00:00:27.230 align:start position:0% really really hard to write 100% uh correct 00:00:27.230 --> 00:00:27.240 align:start position:0% correct 00:00:27.240 --> 00:00:29.550 align:start position:0% correct code<00:00:28.240> regardless<00:00:28.679> of<00:00:28.880> whether<00:00:29.279> this<00:00:29.359> is<00:00:29.480> a 00:00:29.550 --> 00:00:29.560 align:start position:0% code regardless of whether this is a 00:00:29.560 --> 00:00:31.830 align:start position:0% code regardless of whether this is a smart<00:00:29.800> cont<00:00:30.000> contract<00:00:30.439> or<00:00:30.920> any<00:00:31.199> other<00:00:31.640> piece 00:00:31.830 --> 00:00:31.840 align:start position:0% smart cont contract or any other piece 00:00:31.840 --> 00:00:35.630 align:start position:0% smart cont contract or any other piece of<00:00:32.280> code<00:00:33.280> and<00:00:34.280> but<00:00:35.079> what<00:00:35.160> does<00:00:35.280> it<00:00:35.440> actually 00:00:35.630 --> 00:00:35.640 align:start position:0% of code and but what does it actually 00:00:35.640 --> 00:00:37.630 align:start position:0% of code and but what does it actually mean<00:00:35.840> to<00:00:36.040> write<00:00:36.320> correct<00:00:36.640> code<00:00:37.000> what<00:00:37.200> what<00:00:37.320> is 00:00:37.630 --> 00:00:37.640 align:start position:0% mean to write correct code what what is 00:00:37.640 --> 00:00:40.990 align:start position:0% mean to write correct code what what is the<00:00:37.760> word<00:00:38.120> correct<00:00:38.680> mean<00:00:39.680> and<00:00:40.399> uh<00:00:40.520> I<00:00:40.600> think<00:00:40.840> the 00:00:40.990 --> 00:00:41.000 align:start position:0% the word correct mean and uh I think the 00:00:41.000 --> 00:00:44.830 align:start position:0% the word correct mean and uh I think the the<00:00:41.200> best<00:00:41.640> explanation<00:00:42.280> is<00:00:43.000> that<00:00:44.000> uh<00:00:44.399> code<00:00:44.680> is 00:00:44.830 --> 00:00:44.840 align:start position:0% the best explanation is that uh code is 00:00:44.840 --> 00:00:46.950 align:start position:0% the best explanation is that uh code is correct<00:00:45.399> when<00:00:45.520> it<00:00:45.680> does<00:00:46.120> exactly<00:00:46.520> the<00:00:46.680> same 00:00:46.950 --> 00:00:46.960 align:start position:0% correct when it does exactly the same 00:00:46.960 --> 00:00:49.630 align:start position:0% correct when it does exactly the same thing<00:00:47.640> as<00:00:48.120> the<00:00:48.360> the<00:00:48.520> programmer<00:00:49.079> intended<00:00:49.480> it 00:00:49.630 --> 00:00:49.640 align:start position:0% thing as the the programmer intended it 00:00:49.640 --> 00:00:51.790 align:start position:0% thing as the the programmer intended it to<00:00:49.760> do<00:00:49.960> so<00:00:50.199> the<00:00:50.640> the<00:00:50.800> mental<00:00:51.160> model<00:00:51.520> of<00:00:51.640> the 00:00:51.790 --> 00:00:51.800 align:start position:0% to do so the the mental model of the 00:00:51.800 --> 00:00:53.790 align:start position:0% to do so the the mental model of the programmer<00:00:52.359> about<00:00:52.680> smart<00:00:53.000> contract<00:00:53.359> or<00:00:53.480> about 00:00:53.790 --> 00:00:53.800 align:start position:0% programmer about smart contract or about 00:00:53.800 --> 00:00:57.430 align:start position:0% programmer about smart contract or about the<00:00:54.280> the<00:00:54.440> program<00:00:54.800> is<00:00:54.960> the<00:00:55.120> same<00:00:55.559> as<00:00:56.559> the<00:00:57.239> what 00:00:57.430 --> 00:00:57.440 align:start position:0% the the program is the same as the what 00:00:57.440 --> 00:00:59.029 align:start position:0% the the program is the same as the what the<00:00:57.600> the<00:00:57.719> actual<00:00:58.079> machine<00:00:58.440> does<00:00:58.719> with<00:00:58.879> the 00:00:59.029 --> 00:00:59.039 align:start position:0% the the actual machine does with the 00:00:59.039 --> 00:01:04.149 align:start position:0% the the actual machine does with the program<00:01:00.199> and<00:01:00.879> for<00:01:01.239> ethereum<00:01:02.239> uh<00:01:03.039> this<00:01:03.719> extends 00:01:04.149 --> 00:01:04.159 align:start position:0% program and for ethereum uh this extends 00:01:04.159 --> 00:01:07.950 align:start position:0% program and for ethereum uh this extends even<00:01:04.360> more<00:01:04.760> because<00:01:05.680> we<00:01:05.799> do<00:01:06.000> not<00:01:06.159> only<00:01:06.439> want<00:01:07.159> uh 00:01:07.950 --> 00:01:07.960 align:start position:0% even more because we do not only want uh 00:01:07.960 --> 00:01:10.670 align:start position:0% even more because we do not only want uh the<00:01:08.960> the<00:01:09.240> expectations<00:01:09.880> of<00:01:10.080> the<00:01:10.240> programmer 00:01:10.670 --> 00:01:10.680 align:start position:0% the the expectations of the programmer 00:01:10.680 --> 00:01:12.350 align:start position:0% the the expectations of the programmer to<00:01:10.799> match<00:01:11.080> the<00:01:11.240> actual<00:01:11.520> program<00:01:11.880> but<00:01:12.000> we<00:01:12.159> also 00:01:12.350 --> 00:01:12.360 align:start position:0% to match the actual program but we also 00:01:12.360 --> 00:01:14.390 align:start position:0% to match the actual program but we also want<00:01:12.520> to<00:01:12.680> match<00:01:13.320> uh<00:01:13.640> want<00:01:13.759> to<00:01:13.920> match<00:01:14.200> the 00:01:14.390 --> 00:01:14.400 align:start position:0% want to match uh want to match the 00:01:14.400 --> 00:01:17.030 align:start position:0% want to match uh want to match the expectations<00:01:14.840> of<00:01:15.000> the<00:01:15.119> user<00:01:16.000> to<00:01:16.200> match<00:01:16.640> the 00:01:17.030 --> 00:01:17.040 align:start position:0% expectations of the user to match the 00:01:17.040 --> 00:01:19.789 align:start position:0% expectations of the user to match the the<00:01:17.200> actual<00:01:17.520> execution<00:01:18.000> of<00:01:18.280> of<00:01:18.400> the 00:01:19.789 --> 00:01:19.799 align:start position:0% the actual execution of of the 00:01:19.799 --> 00:01:23.710 align:start position:0% the actual execution of of the program<00:01:20.799> and<00:01:21.720> so<00:01:22.720> how<00:01:22.840> do<00:01:23.000> we<00:01:23.159> get<00:01:23.320> to<00:01:23.479> that 00:01:23.710 --> 00:01:23.720 align:start position:0% program and so how do we get to that 00:01:23.720 --> 00:01:27.710 align:start position:0% program and so how do we get to that point<00:01:24.720> uh<00:01:25.320> and<00:01:26.200> there<00:01:26.320> are<00:01:26.479> of<00:01:26.600> course<00:01:26.880> several 00:01:27.710 --> 00:01:27.720 align:start position:0% point uh and there are of course several 00:01:27.720 --> 00:01:29.270 align:start position:0% point uh and there are of course several uh<00:01:27.920> well<00:01:28.119> established<00:01:28.640> techniques<00:01:29.040> and<00:01:29.159> one 00:01:29.270 --> 00:01:29.280 align:start position:0% uh well established techniques and one 00:01:29.280 --> 00:01:32.870 align:start position:0% uh well established techniques and one of<00:01:29.400> them<00:01:29.560> is<00:01:29.680> to<00:01:29.920> to<00:01:30.119> to<00:01:30.840> uh<00:01:31.400> yeah<00:01:31.680> write<00:01:32.280> use 00:01:32.870 --> 00:01:32.880 align:start position:0% of them is to to to uh yeah write use 00:01:32.880 --> 00:01:35.510 align:start position:0% of them is to to to uh yeah write use testing<00:01:33.320> unit<00:01:33.960> tests 00:01:35.510 --> 00:01:35.520 align:start position:0% testing unit tests 00:01:35.520 --> 00:01:38.109 align:start position:0% testing unit tests um<00:01:36.520> and<00:01:36.720> that<00:01:36.880> that's<00:01:37.040> quite<00:01:37.280> easy<00:01:37.600> easy<00:01:37.799> to<00:01:37.960> do 00:01:38.109 --> 00:01:38.119 align:start position:0% um and that that's quite easy easy to do 00:01:38.119 --> 00:01:42.630 align:start position:0% um and that that's quite easy easy to do you<00:01:38.320> just<00:01:39.040> think<00:01:39.320> about<00:01:40.240> uh<00:01:41.119> a<00:01:41.240> certain<00:01:41.560> input 00:01:42.630 --> 00:01:42.640 align:start position:0% you just think about uh a certain input 00:01:42.640 --> 00:01:44.990 align:start position:0% you just think about uh a certain input and<00:01:43.640> make<00:01:43.799> up<00:01:43.960> your<00:01:44.119> mind<00:01:44.360> about<00:01:44.600> what<00:01:44.719> you're 00:01:44.990 --> 00:01:45.000 align:start position:0% and make up your mind about what you're 00:01:45.000 --> 00:01:47.630 align:start position:0% and make up your mind about what you're expected<00:01:45.399> to<00:01:45.560> happen<00:01:46.040> and<00:01:46.240> then<00:01:47.159> run<00:01:47.439> the 00:01:47.630 --> 00:01:47.640 align:start position:0% expected to happen and then run the 00:01:47.640 --> 00:01:49.910 align:start position:0% expected to happen and then run the program<00:01:48.240> and<00:01:48.399> see<00:01:48.719> whether<00:01:48.920> that<00:01:49.079> actually 00:01:49.910 --> 00:01:49.920 align:start position:0% program and see whether that actually 00:01:49.920 --> 00:01:53.389 align:start position:0% program and see whether that actually happened<00:01:50.920> and<00:01:51.399> that's<00:01:51.799> good<00:01:52.040> to<00:01:52.759> to<00:01:53.000> check 00:01:53.389 --> 00:01:53.399 align:start position:0% happened and that's good to to check 00:01:53.399 --> 00:01:56.029 align:start position:0% happened and that's good to to check whether<00:01:54.200> uh<00:01:54.520> desired<00:01:54.960> behavior<00:01:55.360> is<00:01:55.560> actually 00:01:56.029 --> 00:01:56.039 align:start position:0% whether uh desired behavior is actually 00:01:56.039 --> 00:01:59.950 align:start position:0% whether uh desired behavior is actually there<00:01:57.039> but<00:01:57.399> it<00:01:57.640> fails<00:01:58.159> to<00:01:58.799> show<00:01:59.240> that<00:01:59.520> under 00:01:59.950 --> 00:01:59.960 align:start position:0% there but it fails to show that under 00:01:59.960 --> 00:02:03.270 align:start position:0% there but it fails to show that under desired<00:02:00.360> behavior<00:02:00.840> is<00:02:01.200> absent<00:02:01.840> so<00:02:02.600> you<00:02:02.960> cannot 00:02:03.270 --> 00:02:03.280 align:start position:0% desired behavior is absent so you cannot 00:02:03.280 --> 00:02:06.310 align:start position:0% desired behavior is absent so you cannot use<00:02:03.479> unit<00:02:03.799> testing<00:02:04.439> to<00:02:04.600> show<00:02:05.039> that<00:02:05.479> it's 00:02:06.310 --> 00:02:06.320 align:start position:0% use unit testing to show that it's 00:02:06.320 --> 00:02:08.790 align:start position:0% use unit testing to show that it's impossible<00:02:07.039> to<00:02:07.759> uh<00:02:07.960> withdraw<00:02:08.399> money<00:02:08.599> from 00:02:08.790 --> 00:02:08.800 align:start position:0% impossible to uh withdraw money from 00:02:08.800 --> 00:02:12.229 align:start position:0% impossible to uh withdraw money from your<00:02:09.000> smart<00:02:09.280> contract<00:02:09.720> by<00:02:10.039> a<00:02:10.160> malicious<00:02:10.879> actor 00:02:12.229 --> 00:02:12.239 align:start position:0% your smart contract by a malicious actor 00:02:12.239 --> 00:02:15.990 align:start position:0% your smart contract by a malicious actor and<00:02:13.239> the<00:02:13.400> reason<00:02:13.720> is<00:02:14.560> because<00:02:15.440> you<00:02:15.560> would<00:02:15.760> have 00:02:15.990 --> 00:02:16.000 align:start position:0% and the reason is because you would have 00:02:16.000 --> 00:02:19.150 align:start position:0% and the reason is because you would have to<00:02:16.519> check<00:02:17.160> all<00:02:17.560> possible<00:02:18.040> ways<00:02:18.400> to<00:02:18.680> call<00:02:18.959> the 00:02:19.150 --> 00:02:19.160 align:start position:0% to check all possible ways to call the 00:02:19.160 --> 00:02:22.470 align:start position:0% to check all possible ways to call the contract<00:02:19.840> and<00:02:20.040> that's<00:02:20.200> an<00:02:20.800> uh<00:02:21.000> infinite 00:02:22.470 --> 00:02:22.480 align:start position:0% contract and that's an uh infinite 00:02:22.480 --> 00:02:25.710 align:start position:0% contract and that's an uh infinite number<00:02:23.480> uh<00:02:23.800> and<00:02:24.319> yeah<00:02:24.480> testing<00:02:24.800> can<00:02:24.959> only<00:02:25.160> do 00:02:25.710 --> 00:02:25.720 align:start position:0% number uh and yeah testing can only do 00:02:25.720 --> 00:02:31.390 align:start position:0% number uh and yeah testing can only do uh<00:02:25.879> Finly<00:02:26.360> many<00:02:26.640> cases 00:02:31.390 --> 00:02:31.400 align:start position:0% 00:02:31.400 --> 00:02:36.350 align:start position:0% uh<00:02:32.080> let's<00:02:33.080> let's<00:02:33.640> so<00:02:34.160> yeah<00:02:34.519> and<00:02:35.519> but<00:02:36.040> there's<00:02:36.239> a 00:02:36.350 --> 00:02:36.360 align:start position:0% uh let's let's so yeah and but there's a 00:02:36.360 --> 00:02:38.350 align:start position:0% uh let's let's so yeah and but there's a solution<00:02:36.720> to<00:02:36.959> that<00:02:37.360> and<00:02:37.680> it<00:02:37.959> comes<00:02:38.200> in<00:02:38.280> the 00:02:38.350 --> 00:02:38.360 align:start position:0% solution to that and it comes in the 00:02:38.360 --> 00:02:40.670 align:start position:0% solution to that and it comes in the form<00:02:38.560> of<00:02:38.640> formal<00:02:39.000> verification<00:02:39.879> and<00:02:40.239> let's 00:02:40.670 --> 00:02:40.680 align:start position:0% form of formal verification and let's 00:02:40.680 --> 00:02:43.149 align:start position:0% form of formal verification and let's take<00:02:40.840> a<00:02:40.959> look<00:02:41.080> at<00:02:41.200> an<00:02:41.400> example<00:02:41.840> there<00:02:42.760> so<00:02:43.040> this 00:02:43.149 --> 00:02:43.159 align:start position:0% take a look at an example there so this 00:02:43.159 --> 00:02:46.030 align:start position:0% take a look at an example there so this is<00:02:43.319> an<00:02:43.720> this<00:02:43.840> is<00:02:43.920> an<00:02:44.080> easy<00:02:44.360> token<00:02:45.040> contract 00:02:46.030 --> 00:02:46.040 align:start position:0% is an this is an easy token contract 00:02:46.040 --> 00:02:49.149 align:start position:0% is an this is an easy token contract which<00:02:46.400> has<00:02:46.560> a<00:02:46.760> balances<00:02:47.440> mapping<00:02:48.200> and<00:02:48.840> uh<00:02:49.000> a 00:02:49.149 --> 00:02:49.159 align:start position:0% which has a balances mapping and uh a 00:02:49.159 --> 00:02:52.350 align:start position:0% which has a balances mapping and uh a function<00:02:49.519> that<00:02:49.640> allows<00:02:50.840> transferring<00:02:51.840> uh 00:02:52.350 --> 00:02:52.360 align:start position:0% function that allows transferring uh 00:02:52.360 --> 00:02:53.750 align:start position:0% function that allows transferring uh yeah<00:02:52.519> balances<00:02:52.959> from<00:02:53.120> one<00:02:53.319> account<00:02:53.519> to<00:02:53.680> the 00:02:53.750 --> 00:02:53.760 align:start position:0% yeah balances from one account to the 00:02:53.760 --> 00:02:57.309 align:start position:0% yeah balances from one account to the other<00:02:54.440> account<00:02:55.440> there<00:02:55.680> is<00:02:55.959> a<00:02:56.360> tiny<00:02:56.720> error<00:02:57.080> in 00:02:57.309 --> 00:02:57.319 align:start position:0% other account there is a tiny error in 00:02:57.319 --> 00:03:02.110 align:start position:0% other account there is a tiny error in there<00:02:58.319> and<00:02:58.599> not<00:02:58.760> sure<00:02:59.000> if<00:02:59.159> you<00:02:59.879> see 00:03:02.110 --> 00:03:02.120 align:start position:0% there and not sure if you see 00:03:02.120 --> 00:03:04.869 align:start position:0% there and not sure if you see that<00:03:03.120> and<00:03:03.480> I<00:03:03.599> would<00:03:03.799> argue 00:03:04.869 --> 00:03:04.879 align:start position:0% that and I would argue 00:03:04.879 --> 00:03:09.270 align:start position:0% that and I would argue that<00:03:06.040> so<00:03:07.040> yeah<00:03:07.440> testing<00:03:08.400> can<00:03:08.680> detect<00:03:09.080> that 00:03:09.270 --> 00:03:09.280 align:start position:0% that so yeah testing can detect that 00:03:09.280 --> 00:03:11.470 align:start position:0% that so yeah testing can detect that error<00:03:09.879> but<00:03:10.200> most<00:03:10.440> people<00:03:10.840> probably<00:03:11.159> won't 00:03:11.470 --> 00:03:11.480 align:start position:0% error but most people probably won't 00:03:11.480 --> 00:03:13.390 align:start position:0% error but most people probably won't think<00:03:11.720> of<00:03:12.080> this<00:03:12.319> specific<00:03:12.760> input<00:03:13.080> that<00:03:13.200> is 00:03:13.390 --> 00:03:13.400 align:start position:0% think of this specific input that is 00:03:13.400 --> 00:03:15.350 align:start position:0% think of this specific input that is required<00:03:13.799> to<00:03:13.959> trigger<00:03:14.319> the<00:03:14.480> test<00:03:14.920> or<00:03:15.080> trigger 00:03:15.350 --> 00:03:15.360 align:start position:0% required to trigger the test or trigger 00:03:15.360 --> 00:03:18.670 align:start position:0% required to trigger the test or trigger the<00:03:15.480> trigger<00:03:15.760> the 00:03:18.670 --> 00:03:18.680 align:start position:0% 00:03:18.680 --> 00:03:21.229 align:start position:0% failure<00:03:19.680> so 00:03:21.229 --> 00:03:21.239 align:start position:0% failure so 00:03:21.239 --> 00:03:23.670 align:start position:0% failure so uh<00:03:22.239> yeah<00:03:22.400> what's<00:03:22.560> the<00:03:22.720> problem 00:03:23.670 --> 00:03:23.680 align:start position:0% uh yeah what's the problem 00:03:23.680 --> 00:03:27.430 align:start position:0% uh yeah what's the problem here<00:03:24.680> it<00:03:24.840> looks<00:03:25.159> correct<00:03:25.680> but<00:03:26.319> uh<00:03:26.599> it<00:03:27.040> probably 00:03:27.430 --> 00:03:27.440 align:start position:0% here it looks correct but uh it probably 00:03:27.440 --> 00:03:30.030 align:start position:0% here it looks correct but uh it probably also<00:03:27.720> will<00:03:28.040> work<00:03:28.319> correctly<00:03:28.840> for<00:03:29.439> most<00:03:29.879> of<00:03:29.959> the 00:03:30.030 --> 00:03:30.040 align:start position:0% also will work correctly for most of the 00:03:30.040 --> 00:03:31.990 align:start position:0% also will work correctly for most of the token<00:03:30.280> contracts<00:03:30.760> out<00:03:30.959> there<00:03:31.480> but<00:03:31.640> what<00:03:31.760> it 00:03:31.990 --> 00:03:32.000 align:start position:0% token contracts out there but what it 00:03:32.000 --> 00:03:33.789 align:start position:0% token contracts out there but what it fails<00:03:32.360> to<00:03:32.599> test<00:03:32.959> is<00:03:33.200> whether<00:03:33.439> there's<00:03:33.599> an 00:03:33.789 --> 00:03:33.799 align:start position:0% fails to test is whether there's an 00:03:33.799 --> 00:03:37.030 align:start position:0% fails to test is whether there's an overflow<00:03:34.400> in<00:03:34.680> the<00:03:35.120> in<00:03:35.319> the<00:03:35.799> in<00:03:35.959> the<00:03:36.159> two<00:03:36.560> Fields 00:03:37.030 --> 00:03:37.040 align:start position:0% overflow in the in the in the two Fields 00:03:37.040 --> 00:03:39.750 align:start position:0% overflow in the in the in the two Fields so<00:03:38.040> if 00:03:39.750 --> 00:03:39.760 align:start position:0% so if 00:03:39.760 --> 00:03:42.910 align:start position:0% so if uh<00:03:40.760> if<00:03:40.920> the<00:03:41.120> amount<00:03:41.400> you<00:03:41.519> want<00:03:41.680> to<00:03:41.920> transfer 00:03:42.910 --> 00:03:42.920 align:start position:0% uh if the amount you want to transfer 00:03:42.920 --> 00:03:45.630 align:start position:0% uh if the amount you want to transfer and<00:03:43.519> the<00:03:43.720> amount<00:03:44.040> that<00:03:44.120> is<00:03:44.319> already<00:03:45.120> there<00:03:45.480> in 00:03:45.630 --> 00:03:45.640 align:start position:0% and the amount that is already there in 00:03:45.640 --> 00:03:49.030 align:start position:0% and the amount that is already there in the<00:03:45.879> Target<00:03:46.760> account<00:03:47.439> sums<00:03:47.879> over<00:03:48.480> 2<00:03:48.760> to<00:03:48.959> the 00:03:49.030 --> 00:03:49.040 align:start position:0% the Target account sums over 2 to the 00:03:49.040 --> 00:03:52.869 align:start position:0% the Target account sums over 2 to the 256<00:03:49.840> then<00:03:50.040> we<00:03:50.159> get<00:03:50.280> an<00:03:50.439> overflow<00:03:51.000> there<00:03:51.400> and<00:03:52.000> uh 00:03:52.869 --> 00:03:52.879 align:start position:0% 256 then we get an overflow there and uh 00:03:52.879 --> 00:03:55.470 align:start position:0% 256 then we get an overflow there and uh the<00:03:53.200> the<00:03:53.360> mechanics<00:03:54.159> don't<00:03:54.400> work 00:03:55.470 --> 00:03:55.480 align:start position:0% the the mechanics don't work 00:03:55.480 --> 00:03:56.470 align:start position:0% the the mechanics don't work correctly 00:03:56.470 --> 00:03:56.480 align:start position:0% correctly 00:03:56.480 --> 00:03:57.750 align:start position:0% correctly [Music] 00:03:57.750 --> 00:03:57.760 align:start position:0% [Music] 00:03:57.760 --> 00:04:00.509 align:start position:0% [Music] um<00:03:58.760> yes<00:03:59.040> so<00:03:59.560> uh 00:04:00.509 --> 00:04:00.519 align:start position:0% um yes so uh 00:04:00.519 --> 00:04:04.030 align:start position:0% um yes so uh and<00:04:01.519> formal<00:04:01.959> verification<00:04:02.840> allows<00:04:03.239> us<00:04:03.439> to<00:04:03.680> ask 00:04:04.030 --> 00:04:04.040 align:start position:0% and formal verification allows us to ask 00:04:04.040 --> 00:04:07.190 align:start position:0% and formal verification allows us to ask questions<00:04:04.680> like<00:04:05.360> uh<00:04:06.159> is<00:04:06.400> the<00:04:06.560> sum<00:04:06.840> of<00:04:07.000> all 00:04:07.190 --> 00:04:07.200 align:start position:0% questions like uh is the sum of all 00:04:07.200 --> 00:04:09.470 align:start position:0% questions like uh is the sum of all balances<00:04:07.799> unchanged<00:04:08.439> by<00:04:08.560> the<00:04:08.680> transfer 00:04:09.470 --> 00:04:09.480 align:start position:0% balances unchanged by the transfer 00:04:09.480 --> 00:04:12.630 align:start position:0% balances unchanged by the transfer function<00:04:10.480> considering<00:04:11.120> all<00:04:11.480> possible<00:04:11.959> states 00:04:12.630 --> 00:04:12.640 align:start position:0% function considering all possible states 00:04:12.640 --> 00:04:14.990 align:start position:0% function considering all possible states of<00:04:12.879> the<00:04:13.159> contract<00:04:13.799> and<00:04:14.040> all<00:04:14.319> possible 00:04:14.990 --> 00:04:15.000 align:start position:0% of the contract and all possible 00:04:15.000 --> 00:04:16.509 align:start position:0% of the contract and all possible possible<00:04:15.280> inputs<00:04:15.599> to<00:04:15.720> the 00:04:16.509 --> 00:04:16.519 align:start position:0% possible inputs to the 00:04:16.519 --> 00:04:19.069 align:start position:0% possible inputs to the function 00:04:19.069 --> 00:04:19.079 align:start position:0% function 00:04:19.079 --> 00:04:23.870 align:start position:0% function next<00:04:20.079> so<00:04:20.320> how<00:04:20.440> does<00:04:20.560> it<00:04:20.680> work<00:04:20.799> in<00:04:20.919> general 00:04:23.870 --> 00:04:23.880 align:start position:0% 00:04:23.880 --> 00:04:27.469 align:start position:0% um<00:04:24.880> so<00:04:25.199> you<00:04:25.520> you<00:04:25.880> provide<00:04:26.240> formal<00:04:26.639> statements 00:04:27.469 --> 00:04:27.479 align:start position:0% um so you you provide formal statements 00:04:27.479 --> 00:04:29.710 align:start position:0% um so you you provide formal statements formal<00:04:27.960> mathematical<00:04:28.600> statements<00:04:29.160> about<00:04:29.520> the 00:04:29.710 --> 00:04:29.720 align:start position:0% formal mathematical statements about the 00:04:29.720 --> 00:04:33.390 align:start position:0% formal mathematical statements about the the<00:04:29.800> behavior<00:04:30.160> of<00:04:30.280> a<00:04:30.440> contract<00:04:31.400> and<00:04:31.919> then<00:04:32.400> you 00:04:33.390 --> 00:04:33.400 align:start position:0% the behavior of a contract and then you 00:04:33.400 --> 00:04:36.790 align:start position:0% the behavior of a contract and then you use<00:04:33.800> mathematical<00:04:34.400> proofs<00:04:34.880> to<00:04:35.280> show<00:04:35.840> that<00:04:36.560> uh 00:04:36.790 --> 00:04:36.800 align:start position:0% use mathematical proofs to show that uh 00:04:36.800 --> 00:04:38.629 align:start position:0% use mathematical proofs to show that uh the<00:04:36.919> code<00:04:37.240> satisfies<00:04:37.880> these<00:04:38.039> statements<00:04:38.560> you 00:04:38.629 --> 00:04:38.639 align:start position:0% the code satisfies these statements you 00:04:38.639 --> 00:04:41.430 align:start position:0% the code satisfies these statements you can<00:04:38.800> do<00:04:39.000> that<00:04:39.759> manually<00:04:40.759> but<00:04:40.960> since<00:04:41.160> we<00:04:41.280> live 00:04:41.430 --> 00:04:41.440 align:start position:0% can do that manually but since we live 00:04:41.440 --> 00:04:43.510 align:start position:0% can do that manually but since we live in<00:04:41.560> 2016<00:04:42.360> there<00:04:42.479> are<00:04:42.960> there<00:04:43.080> are<00:04:43.199> of<00:04:43.320> course 00:04:43.510 --> 00:04:43.520 align:start position:0% in 2016 there are there are of course 00:04:43.520 --> 00:04:46.070 align:start position:0% in 2016 there are there are of course automated<00:04:43.960> provs<00:04:44.400> to<00:04:44.960> help<00:04:45.160> you<00:04:45.400> there<00:04:45.720> and 00:04:46.070 --> 00:04:46.080 align:start position:0% automated provs to help you there and 00:04:46.080 --> 00:04:49.430 align:start position:0% automated provs to help you there and find<00:04:46.520> the<00:04:46.759> the<00:04:46.919> mathematical 00:04:49.430 --> 00:04:49.440 align:start position:0% find the the mathematical 00:04:49.440 --> 00:04:51.909 align:start position:0% find the the mathematical proofs<00:04:50.440> um<00:04:50.759> but 00:04:51.909 --> 00:04:51.919 align:start position:0% proofs um but 00:04:51.919 --> 00:04:54.029 align:start position:0% proofs um but so<00:04:52.919> one<00:04:53.120> thing<00:04:53.240> I<00:04:53.320> want<00:04:53.440> to<00:04:53.520> stress<00:04:53.800> here<00:04:53.919> is 00:04:54.029 --> 00:04:54.039 align:start position:0% so one thing I want to stress here is 00:04:54.039 --> 00:04:55.870 align:start position:0% so one thing I want to stress here is that<00:04:54.160> formal<00:04:54.440> verification<00:04:54.880> is<00:04:55.000> not<00:04:55.160> a<00:04:55.240> silver 00:04:55.870 --> 00:04:55.880 align:start position:0% that formal verification is not a silver 00:04:55.880 --> 00:05:00.550 align:start position:0% that formal verification is not a silver bullet<00:04:56.880> the<00:04:57.080> reason<00:04:57.600> is<00:04:58.000> that<00:04:59.000> um 00:05:00.550 --> 00:05:00.560 align:start position:0% bullet the reason is that um 00:05:00.560 --> 00:05:03.749 align:start position:0% bullet the reason is that um so<00:05:00.919> the<00:05:01.039> the<00:05:01.160> source<00:05:01.479> code<00:05:02.280> so<00:05:03.160> a<00:05:03.320> programming 00:05:03.749 --> 00:05:03.759 align:start position:0% so the the source code so a programming 00:05:03.759 --> 00:05:06.790 align:start position:0% so the the source code so a programming language<00:05:04.199> is<00:05:04.400> already<00:05:05.199> a<00:05:05.360> formal<00:05:05.800> description 00:05:06.790 --> 00:05:06.800 align:start position:0% language is already a formal description 00:05:06.800 --> 00:05:12.070 align:start position:0% language is already a formal description of<00:05:07.800> a<00:05:08.120> program<00:05:09.120> so<00:05:10.120> and 00:05:12.070 --> 00:05:12.080 align:start position:0% of a program so and 00:05:12.080 --> 00:05:14.710 align:start position:0% of a program so and adding<00:05:13.080> adding<00:05:13.520> formal<00:05:13.960> statements<00:05:14.479> in 00:05:14.710 --> 00:05:14.720 align:start position:0% adding adding formal statements in 00:05:14.720 --> 00:05:15.870 align:start position:0% adding adding formal statements in another 00:05:15.870 --> 00:05:15.880 align:start position:0% another 00:05:15.880 --> 00:05:20.230 align:start position:0% another language<00:05:16.880> uh<00:05:17.560> or<00:05:18.560> completely<00:05:19.240> formalizing 00:05:20.230 --> 00:05:20.240 align:start position:0% language uh or completely formalizing 00:05:20.240 --> 00:05:21.990 align:start position:0% language uh or completely formalizing the<00:05:20.360> behavior<00:05:20.759> of<00:05:20.880> a<00:05:21.000> smart<00:05:21.319> contract<00:05:21.840> will 00:05:21.990 --> 00:05:22.000 align:start position:0% the behavior of a smart contract will 00:05:22.000 --> 00:05:23.870 align:start position:0% the behavior of a smart contract will not<00:05:22.199> really<00:05:22.440> help<00:05:22.759> because<00:05:23.240> as<00:05:23.319> I<00:05:23.440> said<00:05:23.680> in<00:05:23.759> the 00:05:23.870 --> 00:05:23.880 align:start position:0% not really help because as I said in the 00:05:23.880 --> 00:05:25.670 align:start position:0% not really help because as I said in the beginning<00:05:24.440> it's<00:05:24.600> all<00:05:24.759> about<00:05:25.080> the<00:05:25.319> mental 00:05:25.670 --> 00:05:25.680 align:start position:0% beginning it's all about the mental 00:05:25.680 --> 00:05:31.350 align:start position:0% beginning it's all about the mental model<00:05:26.199> of<00:05:26.400> the<00:05:26.880> humans<00:05:27.880> so<00:05:28.520> um<00:05:29.360> the 00:05:31.350 --> 00:05:31.360 align:start position:0% model of the humans so um the 00:05:31.360 --> 00:05:33.950 align:start position:0% model of the humans so um the the<00:05:31.720> key<00:05:32.120> goal<00:05:33.080> in<00:05:33.240> using<00:05:33.560> formal 00:05:33.950 --> 00:05:33.960 align:start position:0% the key goal in using formal 00:05:33.960 --> 00:05:35.909 align:start position:0% the key goal in using formal verification<00:05:34.560> is<00:05:34.680> to<00:05:34.880> reduce<00:05:35.240> the<00:05:35.400> complexity 00:05:35.909 --> 00:05:35.919 align:start position:0% verification is to reduce the complexity 00:05:35.919 --> 00:05:39.350 align:start position:0% verification is to reduce the complexity of<00:05:36.039> the<00:05:36.120> smart<00:05:36.440> contract<00:05:37.319> we<00:05:37.479> use<00:05:38.080> source<00:05:38.520> code 00:05:39.350 --> 00:05:39.360 align:start position:0% of the smart contract we use source code 00:05:39.360 --> 00:05:42.950 align:start position:0% of the smart contract we use source code uh<00:05:40.000> to<00:05:40.520> describe<00:05:41.520> how<00:05:41.720> an<00:05:41.880> algorithm<00:05:42.600> works 00:05:42.950 --> 00:05:42.960 align:start position:0% uh to describe how an algorithm works 00:05:42.960 --> 00:05:45.390 align:start position:0% uh to describe how an algorithm works and<00:05:43.160> how<00:05:43.319> a<00:05:43.479> smart<00:05:43.759> contract<00:05:44.160> works<00:05:44.919> and<00:05:45.080> then 00:05:45.390 --> 00:05:45.400 align:start position:0% and how a smart contract works and then 00:05:45.400 --> 00:05:47.830 align:start position:0% and how a smart contract works and then we<00:05:45.560> use<00:05:45.960> formal<00:05:46.360> verification<00:05:46.960> to<00:05:47.160> describe 00:05:47.830 --> 00:05:47.840 align:start position:0% we use formal verification to describe 00:05:47.840 --> 00:05:49.110 align:start position:0% we use formal verification to describe what<00:05:48.000> it 00:05:49.110 --> 00:05:49.120 align:start position:0% what it 00:05:49.120 --> 00:05:52.309 align:start position:0% what it does<00:05:50.120> and<00:05:50.280> the<00:05:50.400> idea<00:05:50.680> is<00:05:50.919> that<00:05:51.560> this<00:05:51.960> what<00:05:52.160> it 00:05:52.309 --> 00:05:52.319 align:start position:0% does and the idea is that this what it 00:05:52.319 --> 00:05:54.909 align:start position:0% does and the idea is that this what it does<00:05:52.720> is<00:05:53.080> easier<00:05:53.440> to<00:05:53.960> understand<00:05:54.240> then<00:05:54.560> how<00:05:54.759> it 00:05:54.909 --> 00:05:54.919 align:start position:0% does is easier to understand then how it 00:05:54.919 --> 00:05:55.830 align:start position:0% does is easier to understand then how it does 00:05:55.830 --> 00:05:55.840 align:start position:0% does 00:05:55.840 --> 00:06:01.309 align:start position:0% does it<00:05:56.840> and<00:05:57.560> another<00:05:58.560> another<00:05:59.160> great<00:06:00.080> uh<00:06:01.080> thing 00:06:01.309 --> 00:06:01.319 align:start position:0% it and another another great uh thing 00:06:01.319 --> 00:06:03.350 align:start position:0% it and another another great uh thing about<00:06:01.479> formal<00:06:01.840> verification<00:06:02.360> is<00:06:02.520> that<00:06:02.639> we<00:06:02.759> can 00:06:03.350 --> 00:06:03.360 align:start position:0% about formal verification is that we can 00:06:03.360 --> 00:06:05.830 align:start position:0% about formal verification is that we can ask<00:06:04.360> questions<00:06:04.840> about<00:06:05.080> the<00:06:05.199> behavior<00:06:05.600> of<00:06:05.720> the 00:06:05.830 --> 00:06:05.840 align:start position:0% ask questions about the behavior of the 00:06:05.840 --> 00:06:08.830 align:start position:0% ask questions about the behavior of the program<00:06:06.199> so<00:06:06.360> it's<00:06:06.560> not<00:06:06.759> only<00:06:07.199> about 00:06:08.830 --> 00:06:08.840 align:start position:0% program so it's not only about 00:06:08.840 --> 00:06:11.230 align:start position:0% program so it's not only about formalizing<00:06:09.840> it<00:06:10.120> in<00:06:10.479> in<00:06:10.560> a<00:06:10.720> kind<00:06:10.840> of<00:06:10.960> a 00:06:11.230 --> 00:06:11.240 align:start position:0% formalizing it in in a kind of a 00:06:11.240 --> 00:06:13.430 align:start position:0% formalizing it in in a kind of a specification<00:06:12.240> but<00:06:12.360> we<00:06:12.479> can<00:06:12.599> also<00:06:12.919> just<00:06:13.240> add 00:06:13.430 --> 00:06:13.440 align:start position:0% specification but we can also just add 00:06:13.440 --> 00:06:15.749 align:start position:0% specification but we can also just add to<00:06:13.680> that<00:06:13.880> and<00:06:14.199> ask<00:06:14.800> questions<00:06:15.240> like<00:06:15.440> is<00:06:15.639> the 00:06:15.749 --> 00:06:15.759 align:start position:0% to that and ask questions like is the 00:06:15.759 --> 00:06:18.150 align:start position:0% to that and ask questions like is the sum<00:06:15.960> of<00:06:16.080> all<00:06:16.240> balances<00:06:16.680> fixed<00:06:17.080> and<00:06:17.319> if<00:06:18.000> there 00:06:18.150 --> 00:06:18.160 align:start position:0% sum of all balances fixed and if there 00:06:18.160 --> 00:06:21.110 align:start position:0% sum of all balances fixed and if there is<00:06:18.400> some<00:06:18.759> way<00:06:19.280> to<00:06:19.759> modify<00:06:20.240> the<00:06:20.400> balances<00:06:20.919> so 00:06:21.110 --> 00:06:21.120 align:start position:0% is some way to modify the balances so 00:06:21.120 --> 00:06:23.390 align:start position:0% is some way to modify the balances so that<00:06:21.720> the<00:06:21.840> sum<00:06:22.160> is<00:06:22.360> not<00:06:22.560> fixed<00:06:22.919> between<00:06:23.199> two 00:06:23.390 --> 00:06:23.400 align:start position:0% that the sum is not fixed between two 00:06:23.400 --> 00:06:27.430 align:start position:0% that the sum is not fixed between two calls<00:06:24.039> then<00:06:24.639> uh<00:06:24.919> the<00:06:25.039> system<00:06:25.319> will<00:06:25.479> tell<00:06:25.680> us<00:06:26.560> or 00:06:27.430 --> 00:06:27.440 align:start position:0% calls then uh the system will tell us or 00:06:27.440 --> 00:06:29.309 align:start position:0% calls then uh the system will tell us or uh<00:06:27.840> yeah<00:06:28.000> we<00:06:28.080> can<00:06:28.240> also<00:06:28.520> ask<00:06:28.800> questions<00:06:29.120> like 00:06:29.309 --> 00:06:29.319 align:start position:0% uh yeah we can also ask questions like 00:06:29.319 --> 00:06:31.150 align:start position:0% uh yeah we can also ask questions like will<00:06:29.440> I<00:06:29.759> smart<00:06:30.000> contract<00:06:30.319> get<00:06:30.479> stuck<00:06:30.800> so<00:06:31.000> is 00:06:31.150 --> 00:06:31.160 align:start position:0% will I smart contract get stuck so is 00:06:31.160 --> 00:06:36.710 align:start position:0% will I smart contract get stuck so is there<00:06:31.560> any<00:06:31.840> way<00:06:32.720> to<00:06:34.080> uh<00:06:35.080> to<00:06:35.319> send<00:06:36.160> messages<00:06:36.560> to 00:06:36.710 --> 00:06:36.720 align:start position:0% there any way to uh to send messages to 00:06:36.720 --> 00:06:38.469 align:start position:0% there any way to uh to send messages to the<00:06:36.840> smart<00:06:37.120> contract<00:06:37.440> to<00:06:37.639> call<00:06:37.919> functions<00:06:38.400> in 00:06:38.469 --> 00:06:38.479 align:start position:0% the smart contract to call functions in 00:06:38.479 --> 00:06:40.510 align:start position:0% the smart contract to call functions in a<00:06:38.680> way<00:06:38.919> that<00:06:39.039> at<00:06:39.199> some<00:06:39.479> point<00:06:40.080> it's<00:06:40.280> not 00:06:40.510 --> 00:06:40.520 align:start position:0% a way that at some point it's not 00:06:40.520 --> 00:06:42.589 align:start position:0% a way that at some point it's not possible<00:06:40.840> to<00:06:41.039> move<00:06:41.280> forward<00:06:41.840> in<00:06:42.039> the<00:06:42.400> in<00:06:42.479> the 00:06:42.589 --> 00:06:42.599 align:start position:0% possible to move forward in the in the 00:06:42.599 --> 00:06:44.270 align:start position:0% possible to move forward in the in the states<00:06:42.919> of<00:06:43.039> the<00:06:43.160> smart<00:06:43.440> contract<00:06:43.800> or<00:06:43.919> it's<00:06:44.080> not 00:06:44.270 --> 00:06:44.280 align:start position:0% states of the smart contract or it's not 00:06:44.280 --> 00:06:48.150 align:start position:0% states of the smart contract or it's not possible<00:06:44.599> to<00:06:44.919> to<00:06:45.120> get<00:06:45.280> the<00:06:45.400> money<00:06:45.759> out<00:06:46.199> at<00:06:46.319> all 00:06:48.150 --> 00:06:48.160 align:start position:0% possible to to get the money out at all 00:06:48.160 --> 00:06:51.309 align:start position:0% possible to to get the money out at all anymore<00:06:49.160> so<00:06:49.759> uh<00:06:49.960> yeah<00:06:50.400> form<00:06:50.759> verification<00:06:51.199> is 00:06:51.309 --> 00:06:51.319 align:start position:0% anymore so uh yeah form verification is 00:06:51.319 --> 00:06:53.830 align:start position:0% anymore so uh yeah form verification is coming<00:06:51.520> to<00:06:51.680> ethereum<00:06:52.639> there<00:06:52.759> are 00:06:53.830 --> 00:06:53.840 align:start position:0% coming to ethereum there are 00:06:53.840 --> 00:06:56.510 align:start position:0% coming to ethereum there are already<00:06:54.840> uh<00:06:55.000> a<00:06:55.160> lot<00:06:55.319> of<00:06:55.520> research<00:06:55.960> papers<00:06:56.319> on 00:06:56.510 --> 00:06:56.520 align:start position:0% already uh a lot of research papers on 00:06:56.520 --> 00:06:59.990 align:start position:0% already uh a lot of research papers on that<00:06:56.759> topic<00:06:57.639> um 00:06:59.990 --> 00:07:00.000 align:start position:0% that topic um 00:07:00.000 --> 00:07:02.629 align:start position:0% that topic um and<00:07:00.639> the<00:07:00.879> reason<00:07:01.280> for<00:07:01.520> that<00:07:01.840> is<00:07:02.120> that 00:07:02.629 --> 00:07:02.639 align:start position:0% and the reason for that is that 00:07:02.639 --> 00:07:05.230 align:start position:0% and the reason for that is that blockchains<00:07:03.199> are<00:07:03.560> actually<00:07:04.560> a<00:07:04.720> paradise<00:07:05.080> of 00:07:05.230 --> 00:07:05.240 align:start position:0% blockchains are actually a paradise of 00:07:05.240 --> 00:07:08.670 align:start position:0% blockchains are actually a paradise of Home<00:07:05.479> verification<00:07:06.360> because<00:07:07.360> uh<00:07:08.120> yeah<00:07:08.440> the 00:07:08.670 --> 00:07:08.680 align:start position:0% Home verification because uh yeah the 00:07:08.680 --> 00:07:11.469 align:start position:0% Home verification because uh yeah the the<00:07:08.879> model<00:07:09.240> is<00:07:09.440> that<00:07:09.639> simple<00:07:10.039> but<00:07:10.400> uh<00:07:10.520> U<00:07:11.000> later 00:07:11.469 --> 00:07:11.479 align:start position:0% the model is that simple but uh U later 00:07:11.479 --> 00:07:13.790 align:start position:0% the model is that simple but uh U later will<00:07:11.879> tell<00:07:12.080> you<00:07:12.240> more<00:07:12.479> about 00:07:13.790 --> 00:07:13.800 align:start position:0% will tell you more about 00:07:13.800 --> 00:07:17.230 align:start position:0% will tell you more about that<00:07:15.240> um<00:07:16.240> okay 00:07:17.230 --> 00:07:17.240 align:start position:0% that um okay 00:07:17.240 --> 00:07:21.869 align:start position:0% that um okay and<00:07:18.240> formal<00:07:19.120> verification<00:07:20.160> tools<00:07:21.160> also<00:07:21.520> exist 00:07:21.869 --> 00:07:21.879 align:start position:0% and formal verification tools also exist 00:07:21.879 --> 00:07:24.749 align:start position:0% and formal verification tools also exist for<00:07:22.280> kind<00:07:22.440> of<00:07:22.800> a<00:07:23.080> common<00:07:23.560> languages<00:07:24.120> like<00:07:24.280> C 00:07:24.749 --> 00:07:24.759 align:start position:0% for kind of a common languages like C 00:07:24.759 --> 00:07:29.670 align:start position:0% for kind of a common languages like C and<00:07:25.280> Java<00:07:25.680> and<00:07:26.000> Adda<00:07:27.000> and<00:07:27.800> uh 00:07:29.670 --> 00:07:29.680 align:start position:0% and Java and Adda and uh 00:07:29.680 --> 00:07:33.909 align:start position:0% and Java and Adda and uh these<00:07:30.680> there<00:07:31.000> are<00:07:32.000> and<00:07:32.160> the<00:07:32.319> way<00:07:32.520> it<00:07:32.720> works<00:07:33.319> for 00:07:33.909 --> 00:07:33.919 align:start position:0% these there are and the way it works for 00:07:33.919 --> 00:07:36.029 align:start position:0% these there are and the way it works for these<00:07:34.120> tools<00:07:34.400> for<00:07:34.560> pharmacy<00:07:35.120> for<00:07:35.360> Kato<00:07:35.919> and 00:07:36.029 --> 00:07:36.039 align:start position:0% these tools for pharmacy for Kato and 00:07:36.039 --> 00:07:38.670 align:start position:0% these tools for pharmacy for Kato and for<00:07:36.199> spark<00:07:37.000> is<00:07:37.160> that<00:07:37.319> you<00:07:37.560> write<00:07:37.960> your<00:07:38.440> your 00:07:38.670 --> 00:07:38.680 align:start position:0% for spark is that you write your your 00:07:38.680 --> 00:07:40.790 align:start position:0% for spark is that you write your your program<00:07:39.120> in<00:07:39.400> the<00:07:39.680> the<00:07:39.840> ordinary<00:07:40.400> language 00:07:40.790 --> 00:07:40.800 align:start position:0% program in the the ordinary language 00:07:40.800 --> 00:07:44.430 align:start position:0% program in the the ordinary language you're<00:07:41.280> used<00:07:41.599> to<00:07:41.919> like<00:07:42.160> like<00:07:42.639> C<00:07:43.639> and<00:07:44.080> then<00:07:44.199> you 00:07:44.430 --> 00:07:44.440 align:start position:0% you're used to like like C and then you 00:07:44.440 --> 00:07:47.909 align:start position:0% you're used to like like C and then you annotate<00:07:45.120> this<00:07:45.759> uh<00:07:45.919> source<00:07:46.280> code<00:07:46.720> with<00:07:47.440> uh 00:07:47.909 --> 00:07:47.919 align:start position:0% annotate this uh source code with uh 00:07:47.919 --> 00:07:50.189 align:start position:0% annotate this uh source code with uh formal<00:07:48.319> statements<00:07:48.759> so<00:07:49.000> like<00:07:49.360> solve<00:07:49.759> balances 00:07:50.189 --> 00:07:50.199 align:start position:0% formal statements so like solve balances 00:07:50.199 --> 00:07:52.790 align:start position:0% formal statements so like solve balances is<00:07:50.319> a<00:07:50.680> is<00:07:50.759> fixed<00:07:51.080> between<00:07:51.319> two<00:07:51.479> function<00:07:51.800> calls 00:07:52.790 --> 00:07:52.800 align:start position:0% is a is fixed between two function calls 00:07:52.800 --> 00:07:54.350 align:start position:0% is a is fixed between two function calls and<00:07:53.199> then<00:07:53.479> there<00:07:53.599> are 00:07:54.350 --> 00:07:54.360 align:start position:0% and then there are 00:07:54.360 --> 00:07:58.110 align:start position:0% and then there are tools<00:07:55.360> which<00:07:55.800> compile<00:07:56.520> both<00:07:57.319> the<00:07:57.400> source<00:07:57.720> code 00:07:58.110 --> 00:07:58.120 align:start position:0% tools which compile both the source code 00:07:58.120 --> 00:08:01.230 align:start position:0% tools which compile both the source code and<00:07:58.319> these<00:07:58.520> annotations<00:07:59.159> into<00:07:59.520> to<00:08:00.000> a<00:08:00.240> language 00:08:01.230 --> 00:08:01.240 align:start position:0% and these annotations into to a language 00:08:01.240 --> 00:08:04.149 align:start position:0% and these annotations into to a language that<00:08:01.400> can<00:08:01.639> work<00:08:02.520> with<00:08:02.680> the<00:08:03.039> annotations<00:08:04.039> this 00:08:04.149 --> 00:08:04.159 align:start position:0% that can work with the annotations this 00:08:04.159 --> 00:08:08.869 align:start position:0% that can work with the annotations this is<00:08:04.319> often<00:08:05.039> Y3<00:08:06.039> uh<00:08:06.240> and<00:08:06.720> more<00:08:06.919> recently<00:08:07.720> we<00:08:07.919> have 00:08:08.869 --> 00:08:08.879 align:start position:0% is often Y3 uh and more recently we have 00:08:08.879 --> 00:08:13.070 align:start position:0% is often Y3 uh and more recently we have fstar<00:08:09.879> and<00:08:10.120> then<00:08:11.039> um<00:08:12.039> automated<00:08:12.520> provs<00:08:12.919> are 00:08:13.070 --> 00:08:13.080 align:start position:0% fstar and then um automated provs are 00:08:13.080 --> 00:08:16.629 align:start position:0% fstar and then um automated provs are used<00:08:13.440> to<00:08:14.080> verify<00:08:15.080> these<00:08:15.479> formal<00:08:15.759> statement<00:08:16.240> on 00:08:16.629 --> 00:08:16.639 align:start position:0% used to verify these formal statement on 00:08:16.639 --> 00:08:19.749 align:start position:0% used to verify these formal statement on the<00:08:17.280> translation<00:08:17.919> of<00:08:18.319> the<00:08:18.440> source<00:08:18.759> code<00:08:19.560> let's 00:08:19.749 --> 00:08:19.759 align:start position:0% the translation of the source code let's 00:08:19.759 --> 00:08:21.510 align:start position:0% the translation of the source code let's take<00:08:19.919> a<00:08:20.000> look<00:08:20.120> at<00:08:20.240> an<00:08:20.440> example<00:08:21.000> so<00:08:21.199> this<00:08:21.319> is 00:08:21.510 --> 00:08:21.520 align:start position:0% take a look at an example so this is 00:08:21.520 --> 00:08:22.909 align:start position:0% take a look at an example so this is this<00:08:21.639> is<00:08:21.720> from<00:08:22.000> a 00:08:22.909 --> 00:08:22.919 align:start position:0% this is from a 00:08:22.919 --> 00:08:27.350 align:start position:0% this is from a c<00:08:23.919> and<00:08:24.400> you<00:08:24.599> see 00:08:27.350 --> 00:08:27.360 align:start position:0% 00:08:27.360 --> 00:08:32.110 align:start position:0% that<00:08:28.360> no<00:08:28.639> no<00:08:28.840> pointer<00:08:29.800> um<00:08:30.599> so<00:08:30.840> you<00:08:30.960> see<00:08:31.199> that 00:08:32.110 --> 00:08:32.120 align:start position:0% that no no pointer um so you see that 00:08:32.120 --> 00:08:34.350 align:start position:0% that no no pointer um so you see that there<00:08:32.839> at<00:08:33.000> the<00:08:33.120> top<00:08:33.479> there<00:08:33.680> is<00:08:33.800> a<00:08:33.959> block<00:08:34.200> of 00:08:34.350 --> 00:08:34.360 align:start position:0% there at the top there is a block of 00:08:34.360 --> 00:08:36.949 align:start position:0% there at the top there is a block of comment<00:08:35.080> with<00:08:35.279> these<00:08:35.479> formal<00:08:35.880> statements<00:08:36.800> and 00:08:36.949 --> 00:08:36.959 align:start position:0% comment with these formal statements and 00:08:36.959 --> 00:08:39.790 align:start position:0% comment with these formal statements and then<00:08:37.279> at<00:08:37.479> the<00:08:37.640> bottom<00:08:38.560> you<00:08:38.760> have<00:08:39.080> regular<00:08:39.479> C 00:08:39.790 --> 00:08:39.800 align:start position:0% then at the bottom you have regular C 00:08:39.800 --> 00:08:42.509 align:start position:0% then at the bottom you have regular C code<00:08:40.200> and<00:08:40.800> uh<00:08:40.919> you<00:08:41.039> also<00:08:41.320> have<00:08:41.680> comment<00:08:42.159> inside 00:08:42.509 --> 00:08:42.519 align:start position:0% code and uh you also have comment inside 00:08:42.519 --> 00:08:46.509 align:start position:0% code and uh you also have comment inside the<00:08:42.640> C<00:08:42.919> code<00:08:43.240> where<00:08:43.360> you<00:08:43.519> can<00:08:44.320> refer<00:08:44.800> to<00:08:45.800> uh<00:08:46.360> the 00:08:46.509 --> 00:08:46.519 align:start position:0% the C code where you can refer to uh the 00:08:46.519 --> 00:08:49.430 align:start position:0% the C code where you can refer to uh the state<00:08:46.800> of<00:08:46.959> the<00:08:47.120> program<00:08:47.440> at<00:08:47.640> that 00:08:49.430 --> 00:08:49.440 align:start position:0% state of the program at that 00:08:49.440 --> 00:08:51.910 align:start position:0% state of the program at that point 00:08:51.910 --> 00:08:51.920 align:start position:0% point 00:08:51.920 --> 00:08:55.230 align:start position:0% point so<00:08:52.920> yeah<00:08:53.160> let's<00:08:53.320> not<00:08:53.519> get<00:08:53.680> into<00:08:53.920> detail<00:08:54.320> there 00:08:55.230 --> 00:08:55.240 align:start position:0% so yeah let's not get into detail there 00:08:55.240 --> 00:08:59.590 align:start position:0% so yeah let's not get into detail there and<00:08:56.240> uh<00:08:56.480> yeah<00:08:56.680> now<00:08:56.920> uich<00:08:57.640> will<00:08:58.480> take<00:08:58.760> over<00:08:59.480> here 00:08:59.590 --> 00:08:59.600 align:start position:0% and uh yeah now uich will take over here 00:08:59.600 --> 00:09:03.150 align:start position:0% and uh yeah now uich will take over here it<00:08:59.760> is<00:09:00.000> here<00:09:00.120> he<00:09:00.240> is<00:09:00.680> and<00:09:01.160> uh<00:09:01.279> so<00:09:01.519> uichi<00:09:02.000> is<00:09:02.480> uh<00:09:03.040> a 00:09:03.150 --> 00:09:03.160 align:start position:0% it is here he is and uh so uichi is uh a 00:09:03.160 --> 00:09:05.269 align:start position:0% it is here he is and uh so uichi is uh a formal<00:09:03.519> verification<00:09:04.160> engineer<00:09:05.040> who 00:09:05.269 --> 00:09:05.279 align:start position:0% formal verification engineer who 00:09:05.279 --> 00:09:07.630 align:start position:0% formal verification engineer who recently<00:09:06.040> started<00:09:06.839> at<00:09:07.040> the<00:09:07.160> etherum 00:09:07.630 --> 00:09:07.640 align:start position:0% recently started at the etherum 00:09:07.640 --> 00:09:09.990 align:start position:0% recently started at the etherum foundation<00:09:08.079> and<00:09:08.240> he<00:09:08.320> will<00:09:08.519> focus<00:09:08.920> on<00:09:09.839> uh 00:09:09.990 --> 00:09:10.000 align:start position:0% foundation and he will focus on uh 00:09:10.000 --> 00:09:12.069 align:start position:0% foundation and he will focus on uh extending<00:09:10.399> the<00:09:10.519> formal<00:09:10.920> verification<00:09:11.920> uh 00:09:12.069 --> 00:09:12.079 align:start position:0% extending the formal verification uh 00:09:12.079 --> 00:09:16.470 align:start position:0% extending the formal verification uh features<00:09:12.760> of 00:09:16.470 --> 00:09:16.480 align:start position:0% 00:09:16.480 --> 00:09:20.110 align:start position:0% solidity<00:09:17.480> hard<00:09:18.440> yes 00:09:20.110 --> 00:09:20.120 align:start position:0% solidity hard yes 00:09:20.120 --> 00:09:25.829 align:start position:0% solidity hard yes uh<00:09:21.120> so<00:09:21.519> Christian<00:09:22.800> started<00:09:23.800> this<00:09:24.440> solidity<00:09:25.360> to 00:09:25.829 --> 00:09:25.839 align:start position:0% uh so Christian started this solidity to 00:09:25.839 --> 00:09:27.389 align:start position:0% uh so Christian started this solidity to Y3 00:09:27.389 --> 00:09:27.399 align:start position:0% Y3 00:09:27.399 --> 00:09:31.230 align:start position:0% Y3 translator<00:09:28.399> um<00:09:28.800> that's<00:09:29.040> similar<00:09:29.519> that<00:09:30.240> flami 00:09:31.230 --> 00:09:31.240 align:start position:0% translator um that's similar that flami 00:09:31.240 --> 00:09:34.790 align:start position:0% translator um that's similar that flami but<00:09:31.480> for<00:09:32.000> the<00:09:32.360> smart<00:09:32.720> for<00:09:32.959> our<00:09:33.240> smart<00:09:33.800> contract 00:09:34.790 --> 00:09:34.800 align:start position:0% but for the smart for our smart contract 00:09:34.800 --> 00:09:36.870 align:start position:0% but for the smart for our smart contract language 00:09:36.870 --> 00:09:36.880 align:start position:0% language 00:09:36.880 --> 00:09:40.069 align:start position:0% language solidity<00:09:37.880> I<00:09:38.399> extended<00:09:39.000> the<00:09:39.120> framework<00:09:39.839> so 00:09:40.069 --> 00:09:40.079 align:start position:0% solidity I extended the framework so 00:09:40.079 --> 00:09:44.069 align:start position:0% solidity I extended the framework so that<00:09:40.320> it<00:09:40.480> can<00:09:40.680> deal<00:09:41.000> with<00:09:41.200> the<00:09:41.839> arrays<00:09:42.880> and<00:09:43.880> it 00:09:44.069 --> 00:09:44.079 align:start position:0% that it can deal with the arrays and it 00:09:44.079 --> 00:09:47.069 align:start position:0% that it can deal with the arrays and it can<00:09:44.240> deal<00:09:44.560> with<00:09:44.800> the<00:09:45.360> simple<00:09:45.760> token<00:09:46.279> contract 00:09:47.069 --> 00:09:47.079 align:start position:0% can deal with the simple token contract 00:09:47.079 --> 00:09:50.310 align:start position:0% can deal with the simple token contract with<00:09:47.560> just<00:09:47.880> one<00:09:48.800> transfer 00:09:50.310 --> 00:09:50.320 align:start position:0% with just one transfer 00:09:50.320 --> 00:09:56.750 align:start position:0% with just one transfer function<00:09:51.320> um<00:09:52.680> the<00:09:53.680> contract<00:09:54.320> itself<00:09:55.320> is<00:09:55.920> easy 00:09:56.750 --> 00:09:56.760 align:start position:0% function um the contract itself is easy 00:09:56.760 --> 00:09:59.630 align:start position:0% function um the contract itself is easy um<00:09:57.079> it<00:09:57.200> has<00:09:57.360> a<00:09:57.519> transfer<00:09:58.120> function 00:09:59.630 --> 00:09:59.640 align:start position:0% um it has a transfer function 00:09:59.640 --> 00:10:02.150 align:start position:0% um it has a transfer function uh<00:09:59.800> you<00:09:59.920> can<00:10:00.279> specify<00:10:00.800> the<00:10:00.959> from<00:10:01.360> address<00:10:01.760> to 00:10:02.150 --> 00:10:02.160 align:start position:0% uh you can specify the from address to 00:10:02.160 --> 00:10:06.350 align:start position:0% uh you can specify the from address to address<00:10:02.560> and<00:10:02.760> the<00:10:03.320> value<00:10:04.320> and<00:10:04.760> some<00:10:05.079> balances 00:10:06.350 --> 00:10:06.360 align:start position:0% address and the value and some balances 00:10:06.360 --> 00:10:10.590 align:start position:0% address and the value and some balances are<00:10:07.600> changed<00:10:08.600> um<00:10:08.839> this<00:10:08.959> is<00:10:09.120> the<00:10:09.279> same<00:10:09.519> thing<00:10:09.839> as 00:10:10.590 --> 00:10:10.600 align:start position:0% are changed um this is the same thing as 00:10:10.600 --> 00:10:13.269 align:start position:0% are changed um this is the same thing as Christian<00:10:11.040> showed<00:10:11.480> before<00:10:12.440> um<00:10:12.640> it<00:10:12.839> has<00:10:13.079> the 00:10:13.269 --> 00:10:13.279 align:start position:0% Christian showed before um it has the 00:10:13.279 --> 00:10:15.750 align:start position:0% Christian showed before um it has the same<00:10:13.640> problem<00:10:14.040> with<00:10:14.200> the<00:10:14.320> buffer<00:10:14.680> over<00:10:15.519> no 00:10:15.750 --> 00:10:15.760 align:start position:0% same problem with the buffer over no 00:10:15.760 --> 00:10:16.670 align:start position:0% same problem with the buffer over no integer 00:10:16.670 --> 00:10:16.680 align:start position:0% integer 00:10:16.680 --> 00:10:21.269 align:start position:0% integer overflow<00:10:17.680> um<00:10:18.480> the<00:10:18.720> tool<00:10:19.360> correctly<00:10:20.320> complains 00:10:21.269 --> 00:10:21.279 align:start position:0% overflow um the tool correctly complains 00:10:21.279 --> 00:10:23.990 align:start position:0% overflow um the tool correctly complains if<00:10:21.560> I<00:10:21.920> don't<00:10:22.440> specify<00:10:23.240> that<00:10:23.440> the<00:10:23.600> total 00:10:23.990 --> 00:10:24.000 align:start position:0% if I don't specify that the total 00:10:24.000 --> 00:10:26.710 align:start position:0% if I don't specify that the total balance<00:10:24.680> is<00:10:25.079> less<00:10:25.399> than<00:10:25.959> a<00:10:26.120> certain<00:10:26.440> big 00:10:26.710 --> 00:10:26.720 align:start position:0% balance is less than a certain big 00:10:26.720 --> 00:10:30.150 align:start position:0% balance is less than a certain big number<00:10:27.480> otherwise<00:10:27.959> the<00:10:28.120> to<00:10:28.560> complains 00:10:30.150 --> 00:10:30.160 align:start position:0% number otherwise the to complains 00:10:30.160 --> 00:10:34.470 align:start position:0% number otherwise the to complains next<00:10:30.480> slide<00:10:31.399> please<00:10:32.399> um<00:10:32.920> when<00:10:33.720> the<00:10:34.079> smart 00:10:34.470 --> 00:10:34.480 align:start position:0% next slide please um when the smart 00:10:34.480 --> 00:10:40.470 align:start position:0% next slide please um when the smart contract<00:10:34.920> has<00:10:35.079> a<00:10:36.000> problem<00:10:37.000> we<00:10:37.560> see<00:10:39.000> a<00:10:40.000> window 00:10:40.470 --> 00:10:40.480 align:start position:0% contract has a problem we see a window 00:10:40.480 --> 00:10:46.389 align:start position:0% contract has a problem we see a window like<00:10:40.800> this<00:10:41.600> um<00:10:42.079> this<00:10:42.240> is<00:10:42.880> Y3<00:10:44.040> GUI<00:10:45.040> Y3<00:10:45.720> is<00:10:46.200> a 00:10:46.389 --> 00:10:46.399 align:start position:0% like this um this is Y3 GUI Y3 is a 00:10:46.399 --> 00:10:49.990 align:start position:0% like this um this is Y3 GUI Y3 is a front<00:10:46.800> end<00:10:47.320> for<00:10:48.079> dozens<00:10:48.560> of<00:10:49.000> automatic<00:10:49.760> and 00:10:49.990 --> 00:10:50.000 align:start position:0% front end for dozens of automatic and 00:10:50.000 --> 00:10:52.030 align:start position:0% front end for dozens of automatic and manual<00:10:50.560> theorem 00:10:52.030 --> 00:10:52.040 align:start position:0% manual theorem 00:10:52.040 --> 00:10:56.670 align:start position:0% manual theorem provs<00:10:53.040> and<00:10:53.720> on<00:10:53.880> the<00:10:54.079> left<00:10:54.519> side<00:10:55.519> you<00:10:55.760> see<00:10:56.360> lots 00:10:56.670 --> 00:10:56.680 align:start position:0% provs and on the left side you see lots 00:10:56.680 --> 00:10:59.430 align:start position:0% provs and on the left side you see lots of<00:10:57.680> conditions 00:10:59.430 --> 00:10:59.440 align:start position:0% of conditions 00:10:59.440 --> 00:11:02.750 align:start position:0% of conditions desired<00:11:00.240> conditions<00:11:00.760> like<00:11:01.519> no<00:11:02.279> integer 00:11:02.750 --> 00:11:02.760 align:start position:0% desired conditions like no integer 00:11:02.760 --> 00:11:06.710 align:start position:0% desired conditions like no integer overflows<00:11:03.720> no<00:11:04.160> buffer<00:11:04.560> overflows<00:11:05.279> and<00:11:05.519> so<00:11:05.720> on 00:11:06.710 --> 00:11:06.720 align:start position:0% overflows no buffer overflows and so on 00:11:06.720 --> 00:11:10.150 align:start position:0% overflows no buffer overflows and so on you<00:11:06.920> see<00:11:07.360> many<00:11:07.839> green<00:11:08.360> chicks<00:11:09.360> the<00:11:09.519> green 00:11:10.150 --> 00:11:10.160 align:start position:0% you see many green chicks the green 00:11:10.160 --> 00:11:14.150 align:start position:0% you see many green chicks the green chicks<00:11:11.160> are<00:11:11.440> on<00:11:11.839> the<00:11:12.079> verified<00:11:13.160> conditions 00:11:14.150 --> 00:11:14.160 align:start position:0% chicks are on the verified conditions 00:11:14.160 --> 00:11:18.430 align:start position:0% chicks are on the verified conditions and<00:11:14.440> Y3<00:11:15.200> can<00:11:16.200> automatically<00:11:17.160> verify<00:11:17.839> most<00:11:18.160> of 00:11:18.430 --> 00:11:18.440 align:start position:0% and Y3 can automatically verify most of 00:11:18.440 --> 00:11:22.150 align:start position:0% and Y3 can automatically verify most of the<00:11:19.279> properties<00:11:20.279> but<00:11:20.639> you<00:11:20.839> also<00:11:21.160> see<00:11:21.480> some 00:11:22.150 --> 00:11:22.160 align:start position:0% the properties but you also see some 00:11:22.160 --> 00:11:25.190 align:start position:0% the properties but you also see some blue<00:11:22.680> question<00:11:23.320> marks<00:11:24.320> the<00:11:24.480> blue<00:11:24.880> question 00:11:25.190 --> 00:11:25.200 align:start position:0% blue question marks the blue question 00:11:25.200 --> 00:11:27.150 align:start position:0% blue question marks the blue question marks<00:11:25.600> are<00:11:25.920> on 00:11:27.150 --> 00:11:27.160 align:start position:0% marks are on 00:11:27.160 --> 00:11:30.509 align:start position:0% marks are on unverified<00:11:28.160> conditions<00:11:29.360> uh<00:11:29.560> wisely<00:11:30.200> still 00:11:30.509 --> 00:11:30.519 align:start position:0% unverified conditions uh wisely still 00:11:30.519 --> 00:11:35.069 align:start position:0% unverified conditions uh wisely still doesn't<00:11:30.959> know<00:11:31.880> if<00:11:32.279> these<00:11:33.200> blue<00:11:34.079> questioned 00:11:35.069 --> 00:11:35.079 align:start position:0% doesn't know if these blue questioned 00:11:35.079 --> 00:11:39.269 align:start position:0% doesn't know if these blue questioned properties<00:11:35.760> hold<00:11:36.480> or<00:11:37.200> not<00:11:38.200> um<00:11:38.760> when<00:11:38.880> you<00:11:39.040> click 00:11:39.269 --> 00:11:39.279 align:start position:0% properties hold or not um when you click 00:11:39.279 --> 00:11:41.670 align:start position:0% properties hold or not um when you click on<00:11:39.480> one<00:11:39.639> of<00:11:39.880> these<00:11:40.120> question<00:11:40.440> marks<00:11:41.320> on<00:11:41.480> the 00:11:41.670 --> 00:11:41.680 align:start position:0% on one of these question marks on the 00:11:41.680 --> 00:11:45.949 align:start position:0% on one of these question marks on the right<00:11:41.959> pan<00:11:42.959> you<00:11:43.200> see<00:11:44.000> a<00:11:44.360> yellow<00:11:44.880> highlight<00:11:45.680> on 00:11:45.949 --> 00:11:45.959 align:start position:0% right pan you see a yellow highlight on 00:11:45.959 --> 00:11:50.269 align:start position:0% right pan you see a yellow highlight on the<00:11:46.200> suspicious<00:11:47.040> piece<00:11:47.320> of<00:11:47.720> code<00:11:48.720> um<00:11:49.440> the<00:11:49.639> code 00:11:50.269 --> 00:11:50.279 align:start position:0% the suspicious piece of code um the code 00:11:50.279 --> 00:11:53.910 align:start position:0% the suspicious piece of code um the code is<00:11:51.279> a<00:11:51.480> translation<00:11:52.160> of<00:11:52.320> the<00:11:52.720> solidity 00:11:53.910 --> 00:11:53.920 align:start position:0% is a translation of the solidity 00:11:53.920 --> 00:11:57.550 align:start position:0% is a translation of the solidity contract<00:11:54.920> into<00:11:55.360> Y3<00:11:55.959> yml<00:11:56.639> language<00:11:57.120> that's<00:11:57.360> a 00:11:57.550 --> 00:11:57.560 align:start position:0% contract into Y3 yml language that's a 00:11:57.560 --> 00:12:01.150 align:start position:0% contract into Y3 yml language that's a language<00:11:57.959> for<00:11:58.360> Y3<00:11:59.519> and<00:11:59.920> here<00:12:00.279> the<00:12:00.519> highlighted 00:12:01.150 --> 00:12:01.160 align:start position:0% language for Y3 and here the highlighted 00:12:01.160 --> 00:12:04.230 align:start position:0% language for Y3 and here the highlighted line<00:12:02.079> is<00:12:02.800> uh 00:12:04.230 --> 00:12:04.240 align:start position:0% line is uh 00:12:04.240 --> 00:12:08.790 align:start position:0% line is uh subtraction<00:12:05.240> um<00:12:06.399> so<00:12:07.399> in<00:12:07.600> this<00:12:07.839> case<00:12:08.519> this 00:12:08.790 --> 00:12:08.800 align:start position:0% subtraction um so in this case this 00:12:08.800 --> 00:12:12.110 align:start position:0% subtraction um so in this case this might<00:12:09.320> underflow<00:12:10.320> um<00:12:11.240> and<00:12:11.399> when<00:12:11.560> you<00:12:11.639> see<00:12:11.880> such 00:12:12.110 --> 00:12:12.120 align:start position:0% might underflow um and when you see such 00:12:12.120 --> 00:12:14.829 align:start position:0% might underflow um and when you see such a<00:12:12.320> problem<00:12:12.920> you<00:12:13.040> can<00:12:13.279> either<00:12:13.639> modify<00:12:14.120> your<00:12:14.480> pro 00:12:14.829 --> 00:12:14.839 align:start position:0% a problem you can either modify your pro 00:12:14.839 --> 00:12:16.910 align:start position:0% a problem you can either modify your pro program<00:12:15.680> or 00:12:16.910 --> 00:12:16.920 align:start position:0% program or 00:12:16.920 --> 00:12:20.470 align:start position:0% program or annotate<00:12:17.920> your<00:12:18.240> program<00:12:18.680> more<00:12:19.000> and<00:12:19.320> more<00:12:20.240> um 00:12:20.470 --> 00:12:20.480 align:start position:0% annotate your program more and more um 00:12:20.480 --> 00:12:23.350 align:start position:0% annotate your program more and more um annotation<00:12:21.040> is<00:12:21.279> like<00:12:21.560> putting<00:12:22.120> assertions<00:12:23.120> in 00:12:23.350 --> 00:12:23.360 align:start position:0% annotation is like putting assertions in 00:12:23.360 --> 00:12:26.389 align:start position:0% annotation is like putting assertions in the<00:12:23.760> program<00:12:24.760> and<00:12:25.120> if<00:12:25.279> you<00:12:25.600> put<00:12:25.959> enough 00:12:26.389 --> 00:12:26.399 align:start position:0% the program and if you put enough 00:12:26.399 --> 00:12:27.670 align:start position:0% the program and if you put enough assumtions 00:12:27.670 --> 00:12:27.680 align:start position:0% assumtions 00:12:27.680 --> 00:12:32.069 align:start position:0% assumtions to<00:12:28.680> um<00:12:29.360> satisfy<00:12:30.079> the<00:12:30.279> automatic<00:12:31.079> provs<00:12:31.920> the 00:12:32.069 --> 00:12:32.079 align:start position:0% to um satisfy the automatic provs the 00:12:32.079 --> 00:12:35.069 align:start position:0% to um satisfy the automatic provs the automatic<00:12:32.600> provs<00:12:33.279> will<00:12:33.519> say<00:12:33.880> green<00:12:34.160> check<00:12:34.920> but 00:12:35.069 --> 00:12:35.079 align:start position:0% automatic provs will say green check but 00:12:35.079 --> 00:12:38.750 align:start position:0% automatic provs will say green check but in<00:12:35.279> many<00:12:35.800> cases<00:12:36.800> you<00:12:37.040> just<00:12:37.440> find<00:12:38.000> problems<00:12:38.519> in 00:12:38.750 --> 00:12:38.760 align:start position:0% in many cases you just find problems in 00:12:38.760 --> 00:12:41.350 align:start position:0% in many cases you just find problems in your<00:12:39.199> specification<00:12:40.000> so<00:12:40.199> it's<00:12:40.519> about 00:12:41.350 --> 00:12:41.360 align:start position:0% your specification so it's about 00:12:41.360 --> 00:12:44.230 align:start position:0% your specification so it's about adjusting<00:12:42.000> your<00:12:42.320> own<00:12:42.720> mental<00:12:43.120> model<00:12:43.959> next 00:12:44.230 --> 00:12:44.240 align:start position:0% adjusting your own mental model next 00:12:44.240 --> 00:12:46.189 align:start position:0% adjusting your own mental model next slide 00:12:46.189 --> 00:12:46.199 align:start position:0% slide 00:12:46.199 --> 00:12:48.670 align:start position:0% slide please 00:12:48.670 --> 00:12:48.680 align:start position:0% please 00:12:48.680 --> 00:12:52.189 align:start position:0% please um<00:12:49.680> so<00:12:49.920> before<00:12:50.240> finding<00:12:50.680> slm<00:12:51.560> I<00:12:51.680> was<00:12:51.920> looking 00:12:52.189 --> 00:12:52.199 align:start position:0% um so before finding slm I was looking 00:12:52.199 --> 00:12:55.189 align:start position:0% um so before finding slm I was looking for<00:12:52.399> a<00:12:52.600> place<00:12:53.440> where<00:12:53.680> formal<00:12:54.199> verification 00:12:55.189 --> 00:12:55.199 align:start position:0% for a place where formal verification 00:12:55.199 --> 00:12:59.629 align:start position:0% for a place where formal verification actually<00:12:56.079> makes<00:12:57.160> sense<00:12:58.160> um<00:12:58.360> before<00:12:58.720> the<00:12:59.519> I 00:12:59.629 --> 00:12:59.639 align:start position:0% actually makes sense um before the I 00:12:59.639 --> 00:13:02.189 align:start position:0% actually makes sense um before the I joined<00:12:59.920> the<00:13:00.040> research<00:13:00.480> institute<00:13:01.399> my<00:13:01.600> job<00:13:01.959> was 00:13:02.189 --> 00:13:02.199 align:start position:0% joined the research institute my job was 00:13:02.199 --> 00:13:04.350 align:start position:0% joined the research institute my job was to<00:13:02.480> spread<00:13:02.839> the<00:13:02.920> formal<00:13:03.320> methods<00:13:03.720> into<00:13:03.959> the 00:13:04.350 --> 00:13:04.360 align:start position:0% to spread the formal methods into the 00:13:04.360 --> 00:13:07.829 align:start position:0% to spread the formal methods into the industry<00:13:05.360> but<00:13:05.560> I<00:13:05.680> didn't<00:13:06.240> have<00:13:06.720> any<00:13:07.240> access<00:13:07.600> to 00:13:07.829 --> 00:13:07.839 align:start position:0% industry but I didn't have any access to 00:13:07.839 --> 00:13:09.629 align:start position:0% industry but I didn't have any access to any<00:13:08.120> company's<00:13:08.600> source 00:13:09.629 --> 00:13:09.639 align:start position:0% any company's source 00:13:09.639 --> 00:13:14.189 align:start position:0% any company's source code<00:13:10.800> so<00:13:11.800> it<00:13:11.880> was<00:13:12.120> hard<00:13:12.320> for<00:13:12.480> me<00:13:12.600> to<00:13:12.760> do<00:13:12.959> that<00:13:13.760> so 00:13:14.189 --> 00:13:14.199 align:start position:0% code so it was hard for me to do that so 00:13:14.199 --> 00:13:17.750 align:start position:0% code so it was hard for me to do that so I<00:13:14.680> joined<00:13:15.160> a<00:13:15.360> company<00:13:16.120> that<00:13:16.480> hired<00:13:17.240> former 00:13:17.750 --> 00:13:17.760 align:start position:0% I joined a company that hired former 00:13:17.760 --> 00:13:19.629 align:start position:0% I joined a company that hired former verification 00:13:19.629 --> 00:13:19.639 align:start position:0% verification 00:13:19.639 --> 00:13:23.150 align:start position:0% verification Engineers<00:13:20.639> that<00:13:20.839> was<00:13:21.000> a<00:13:21.160> US<00:13:21.519> company<00:13:22.440> I<00:13:22.639> had 00:13:23.150 --> 00:13:23.160 align:start position:0% Engineers that was a US company I had 00:13:23.160 --> 00:13:26.550 align:start position:0% Engineers that was a US company I had eight<00:13:23.440> colleagues<00:13:24.279> writing<00:13:25.040> proofs<00:13:26.040> were<00:13:26.440> a 00:13:26.550 --> 00:13:26.560 align:start position:0% eight colleagues writing proofs were a 00:13:26.560 --> 00:13:27.509 align:start position:0% eight colleagues writing proofs were a wonderful 00:13:27.509 --> 00:13:27.519 align:start position:0% wonderful 00:13:27.519 --> 00:13:30.710 align:start position:0% wonderful environment<00:13:28.519> but<00:13:28.920> I<00:13:29.120> I<00:13:29.199> was<00:13:29.440> not<00:13:29.760> happy 00:13:30.710 --> 00:13:30.720 align:start position:0% environment but I I was not happy 00:13:30.720 --> 00:13:33.389 align:start position:0% environment but I I was not happy because<00:13:31.079> our<00:13:31.399> proofs<00:13:32.000> were<00:13:32.320> not<00:13:32.680> about<00:13:33.160> the 00:13:33.389 --> 00:13:33.399 align:start position:0% because our proofs were not about the 00:13:33.399 --> 00:13:34.509 align:start position:0% because our proofs were not about the real 00:13:34.509 --> 00:13:34.519 align:start position:0% real 00:13:34.519 --> 00:13:37.949 align:start position:0% real thing<00:13:35.519> um<00:13:35.839> the<00:13:36.000> fundamental<00:13:36.560> problem<00:13:36.920> is<00:13:37.680> the 00:13:37.949 --> 00:13:37.959 align:start position:0% thing um the fundamental problem is the 00:13:37.959 --> 00:13:43.189 align:start position:0% thing um the fundamental problem is the real<00:13:38.760> CPUs<00:13:39.760> come<00:13:40.680> with<00:13:41.560> documentation 00:13:43.189 --> 00:13:43.199 align:start position:0% real CPUs come with documentation 00:13:43.199 --> 00:13:47.910 align:start position:0% real CPUs come with documentation 2,000<00:13:44.199> pages<00:13:45.199> long<00:13:46.199> and<00:13:46.760> nobody<00:13:47.279> has<00:13:47.519> ever 00:13:47.910 --> 00:13:47.920 align:start position:0% 2,000 pages long and nobody has ever 00:13:47.920 --> 00:13:49.870 align:start position:0% 2,000 pages long and nobody has ever translate<00:13:48.600> translated<00:13:49.120> the<00:13:49.279> whole<00:13:49.560> thing 00:13:49.870 --> 00:13:49.880 align:start position:0% translate translated the whole thing 00:13:49.880 --> 00:13:53.230 align:start position:0% translate translated the whole thing into<00:13:50.320> any<00:13:50.639> theor<00:13:50.959> and<00:13:51.399> provs<00:13:52.399> so<00:13:52.720> that<00:13:52.839> was<00:13:53.079> a 00:13:53.230 --> 00:13:53.240 align:start position:0% into any theor and provs so that was a 00:13:53.240 --> 00:13:56.670 align:start position:0% into any theor and provs so that was a huge<00:13:53.560> problem<00:13:53.920> we<00:13:54.079> couldn't<00:13:54.680> solve<00:13:55.680> um<00:13:56.560> I 00:13:56.670 --> 00:13:56.680 align:start position:0% huge problem we couldn't solve um I 00:13:56.680 --> 00:14:00.030 align:start position:0% huge problem we couldn't solve um I found<00:13:57.040> eum<00:13:57.759> I<00:13:57.839> saw<00:13:58.480> the<00:13:58.600> eum<00:13:59.120> virtual<00:13:59.440> machine 00:14:00.030 --> 00:14:00.040 align:start position:0% found eum I saw the eum virtual machine 00:14:00.040 --> 00:14:03.189 align:start position:0% found eum I saw the eum virtual machine I<00:14:00.160> saw<00:14:00.440> the<00:14:00.600> yellow<00:14:01.040> paper<00:14:01.519> the<00:14:02.199> specification 00:14:03.189 --> 00:14:03.199 align:start position:0% I saw the yellow paper the specification 00:14:03.199 --> 00:14:07.269 align:start position:0% I saw the yellow paper the specification uh<00:14:03.399> it<00:14:03.519> has<00:14:03.720> only<00:14:04.079> 32<00:14:04.759> pages<00:14:05.320> long<00:14:06.320> and<00:14:06.680> I<00:14:07.199> I 00:14:07.269 --> 00:14:07.279 align:start position:0% uh it has only 32 pages long and I I 00:14:07.279 --> 00:14:09.269 align:start position:0% uh it has only 32 pages long and I I thought<00:14:07.600> I<00:14:07.759> can<00:14:08.079> actually<00:14:08.440> translate<00:14:09.120> this 00:14:09.269 --> 00:14:09.279 align:start position:0% thought I can actually translate this 00:14:09.279 --> 00:14:11.670 align:start position:0% thought I can actually translate this thing<00:14:09.519> into<00:14:09.720> a<00:14:09.839> theorum<00:14:10.240> Pro<00:14:10.639> and<00:14:10.880> I<00:14:11.000> can<00:14:11.240> write 00:14:11.670 --> 00:14:11.680 align:start position:0% thing into a theorum Pro and I can write 00:14:11.680 --> 00:14:15.150 align:start position:0% thing into a theorum Pro and I can write proofs<00:14:12.320> about<00:14:12.759> smart<00:14:13.519> contracts<00:14:14.519> I<00:14:14.600> was<00:14:14.800> doing 00:14:15.150 --> 00:14:15.160 align:start position:0% proofs about smart contracts I was doing 00:14:15.160 --> 00:14:18.189 align:start position:0% proofs about smart contracts I was doing that<00:14:15.839> and<00:14:16.040> I<00:14:16.120> was<00:14:16.360> posting<00:14:17.040> the<00:14:17.800> partial 00:14:18.189 --> 00:14:18.199 align:start position:0% that and I was posting the partial 00:14:18.199 --> 00:14:20.749 align:start position:0% that and I was posting the partial results<00:14:18.720> on<00:14:19.000> vit<00:14:19.480> and<00:14:19.720> Christian<00:14:20.120> found<00:14:20.440> me 00:14:20.749 --> 00:14:20.759 align:start position:0% results on vit and Christian found me 00:14:20.759 --> 00:14:25.350 align:start position:0% results on vit and Christian found me and<00:14:21.759> I<00:14:21.920> ended<00:14:22.199> up<00:14:22.560> here 00:14:25.350 --> 00:14:25.360 align:start position:0% and I ended up here 00:14:25.360 --> 00:14:27.269 align:start position:0% and I ended up here um 00:14:27.269 --> 00:14:27.279 align:start position:0% um 00:14:27.279 --> 00:14:31.350 align:start position:0% um so<00:14:28.279> the<00:14:28.800> V<00:14:29.160> machine<00:14:29.480> is<00:14:29.720> wonderful<00:14:30.720> because<00:14:31.199> it 00:14:31.350 --> 00:14:31.360 align:start position:0% so the V machine is wonderful because it 00:14:31.360 --> 00:14:35.030 align:start position:0% so the V machine is wonderful because it has<00:14:31.600> a<00:14:31.920> small<00:14:32.839> specification<00:14:33.839> and<00:14:34.199> this<00:14:34.480> small 00:14:35.030 --> 00:14:35.040 align:start position:0% has a small specification and this small 00:14:35.040 --> 00:14:38.069 align:start position:0% has a small specification and this small specification<00:14:35.920> really<00:14:36.320> matches<00:14:36.839> the<00:14:37.079> reality 00:14:38.069 --> 00:14:38.079 align:start position:0% specification really matches the reality 00:14:38.079 --> 00:14:41.910 align:start position:0% specification really matches the reality because<00:14:38.480> all<00:14:39.000> clients<00:14:39.839> try<00:14:40.240> really<00:14:40.680> hard<00:14:41.360> to 00:14:41.910 --> 00:14:41.920 align:start position:0% because all clients try really hard to 00:14:41.920 --> 00:14:45.550 align:start position:0% because all clients try really hard to match<00:14:42.399> this<00:14:43.000> specification<00:14:44.360> otherwise<00:14:45.360> one 00:14:45.550 --> 00:14:45.560 align:start position:0% match this specification otherwise one 00:14:45.560 --> 00:14:48.230 align:start position:0% match this specification otherwise one of<00:14:45.800> these<00:14:46.480> clients<00:14:47.480> would<00:14:47.800> behave 00:14:48.230 --> 00:14:48.240 align:start position:0% of these clients would behave 00:14:48.240 --> 00:14:50.269 align:start position:0% of these clients would behave differently<00:14:48.759> from<00:14:49.079> others<00:14:49.480> and<00:14:49.800> that's<00:14:50.120> the 00:14:50.269 --> 00:14:50.279 align:start position:0% differently from others and that's the 00:14:50.279 --> 00:14:53.350 align:start position:0% differently from others and that's the worst<00:14:50.600> thing<00:14:50.839> they<00:14:51.000> want<00:14:51.880> so<00:14:52.880> they<00:14:53.120> really 00:14:53.350 --> 00:14:53.360 align:start position:0% worst thing they want so they really 00:14:53.360 --> 00:14:55.670 align:start position:0% worst thing they want so they really want<00:14:53.600> to<00:14:53.920> be<00:14:54.160> conformant<00:14:55.040> to<00:14:55.240> the 00:14:55.670 --> 00:14:55.680 align:start position:0% want to be conformant to the 00:14:55.680 --> 00:14:58.870 align:start position:0% want to be conformant to the specification<00:14:56.680> and<00:14:57.399> a<00:14:57.639> small<00:14:58.360> definition 00:14:58.870 --> 00:14:58.880 align:start position:0% specification and a small definition 00:14:58.880 --> 00:15:01.790 align:start position:0% specification and a small definition that<00:14:59.040> that<00:14:59.199> matches<00:14:59.680> reality<00:15:00.680> is<00:15:01.000> the 00:15:01.790 --> 00:15:01.800 align:start position:0% that that matches reality is the 00:15:01.800 --> 00:15:04.069 align:start position:0% that that matches reality is the fundamental<00:15:02.519> necessity<00:15:03.079> for<00:15:03.639> formal 00:15:04.069 --> 00:15:04.079 align:start position:0% fundamental necessity for formal 00:15:04.079 --> 00:15:07.110 align:start position:0% fundamental necessity for formal verification<00:15:04.720> engineer<00:15:05.279> I<00:15:05.440> found<00:15:05.720> it<00:15:05.880> in<00:15:06.120> E 00:15:07.110 --> 00:15:07.120 align:start position:0% verification engineer I found it in E 00:15:07.120 --> 00:15:09.470 align:start position:0% verification engineer I found it in E next<00:15:07.440> slide 00:15:09.470 --> 00:15:09.480 align:start position:0% next slide 00:15:09.480 --> 00:15:14.749 align:start position:0% next slide please<00:15:10.480> um<00:15:10.759> we<00:15:10.920> have<00:15:11.199> some<00:15:11.560> future<00:15:12.519> steps<00:15:13.639> um 00:15:14.749 --> 00:15:14.759 align:start position:0% please um we have some future steps um 00:15:14.759 --> 00:15:19.470 align:start position:0% please um we have some future steps um so<00:15:15.759> when<00:15:16.079> I'm<00:15:16.759> extending<00:15:17.600> the<00:15:17.959> solidity<00:15:18.880> wi3 00:15:19.470 --> 00:15:19.480 align:start position:0% so when I'm extending the solidity wi3 00:15:19.480 --> 00:15:22.230 align:start position:0% so when I'm extending the solidity wi3 framework<00:15:20.399> um<00:15:20.920> there<00:15:21.079> are<00:15:21.320> some<00:15:21.600> immediate 00:15:22.230 --> 00:15:22.240 align:start position:0% framework um there are some immediate 00:15:22.240 --> 00:15:26.550 align:start position:0% framework um there are some immediate problems<00:15:23.199> like<00:15:23.560> or<00:15:23.800> we<00:15:23.959> don't<00:15:24.440> have<00:15:25.040> the<00:15:25.759> Cora 00:15:26.550 --> 00:15:26.560 align:start position:0% problems like or we don't have the Cora 00:15:26.560 --> 00:15:30.670 align:start position:0% problems like or we don't have the Cora instruction<00:15:27.480> yet<00:15:27.920> in<00:15:28.319> the<00:15:29.199> ation<00:15:29.839> or<00:15:30.519> we 00:15:30.670 --> 00:15:30.680 align:start position:0% instruction yet in the ation or we 00:15:30.680 --> 00:15:34.030 align:start position:0% instruction yet in the ation or we cannot<00:15:31.040> deal<00:15:31.480> with<00:15:31.880> mapping<00:15:32.440> to<00:15:32.839> mapping<00:15:33.560> in 00:15:34.030 --> 00:15:34.040 align:start position:0% cannot deal with mapping to mapping in 00:15:34.040 --> 00:15:39.269 align:start position:0% cannot deal with mapping to mapping in Y3<00:15:34.759> in<00:15:35.079> a<00:15:35.399> short<00:15:35.800> and<00:15:36.079> elegant<00:15:36.759> way<00:15:38.000> um<00:15:39.000> because 00:15:39.269 --> 00:15:39.279 align:start position:0% Y3 in a short and elegant way um because 00:15:39.279 --> 00:15:42.629 align:start position:0% Y3 in a short and elegant way um because of<00:15:39.519> this<00:15:39.880> we<00:15:40.000> are<00:15:40.240> thinking<00:15:40.600> of<00:15:40.839> moving<00:15:41.440> to<00:15:42.240> F 00:15:42.629 --> 00:15:42.639 align:start position:0% of this we are thinking of moving to F 00:15:42.639 --> 00:15:47.670 align:start position:0% of this we are thinking of moving to F star<00:15:43.120> fstar<00:15:43.759> is<00:15:44.639> something<00:15:45.639> similar<00:15:46.079> to<00:15:46.839> Y3 00:15:47.670 --> 00:15:47.680 align:start position:0% star fstar is something similar to Y3 00:15:47.680 --> 00:15:49.670 align:start position:0% star fstar is something similar to Y3 but<00:15:47.920> it<00:15:48.160> has<00:15:48.360> more<00:15:48.639> advanced 00:15:49.670 --> 00:15:49.680 align:start position:0% but it has more advanced 00:15:49.680 --> 00:15:53.069 align:start position:0% but it has more advanced features<00:15:50.680> um<00:15:51.000> I<00:15:51.079> want<00:15:51.279> to<00:15:51.519> thank<00:15:52.240> Microsoft 00:15:53.069 --> 00:15:53.079 align:start position:0% features um I want to thank Microsoft 00:15:53.079 --> 00:15:57.790 align:start position:0% features um I want to thank Microsoft for<00:15:53.800> open<00:15:54.440> sourcing<00:15:55.440> F<00:15:55.800> star<00:15:56.120> and<00:15:56.319> also<00:15:56.680> G3<00:15:57.319> smt 00:15:57.790 --> 00:15:57.800 align:start position:0% for open sourcing F star and also G3 smt 00:15:57.800 --> 00:16:00.870 align:start position:0% for open sourcing F star and also G3 smt solers<00:15:58.399> and<00:15:58.600> we<00:15:59.240> extensively<00:15:59.959> use<00:16:00.240> it<00:16:00.639> um 00:16:00.870 --> 00:16:00.880 align:start position:0% solers and we extensively use it um 00:16:00.880 --> 00:16:04.069 align:start position:0% solers and we extensively use it um thank<00:16:01.040> you<00:16:01.240> very<00:16:01.680> much 00:16:04.069 --> 00:16:04.079 align:start position:0% thank you very much 00:16:04.079 --> 00:16:08.110 align:start position:0% thank you very much um<00:16:05.079> but<00:16:05.360> feature<00:16:05.959> wise<00:16:06.399> um<00:16:06.680> we<00:16:06.959> have<00:16:07.680> more 00:16:08.110 --> 00:16:08.120 align:start position:0% um but feature wise um we have more 00:16:08.120 --> 00:16:11.590 align:start position:0% um but feature wise um we have more problems<00:16:08.639> to<00:16:08.880> solve<00:16:09.360> than<00:16:09.720> just<00:16:10.079> verifying<00:16:11.079> uh 00:16:11.590 --> 00:16:11.600 align:start position:0% problems to solve than just verifying uh 00:16:11.600 --> 00:16:13.309 align:start position:0% problems to solve than just verifying uh one<00:16:12.000> solidity 00:16:13.309 --> 00:16:13.319 align:start position:0% one solidity 00:16:13.319 --> 00:16:15.350 align:start position:0% one solidity contract 00:16:15.350 --> 00:16:15.360 align:start position:0% contract 00:16:15.360 --> 00:16:19.389 align:start position:0% contract um<00:16:16.360> I<00:16:16.480> think<00:16:17.120> we<00:16:17.240> are<00:16:17.399> moving<00:16:17.800> to<00:16:18.399> many<00:16:18.800> small 00:16:19.389 --> 00:16:19.399 align:start position:0% um I think we are moving to many small 00:16:19.399 --> 00:16:22.030 align:start position:0% um I think we are moving to many small contracts<00:16:20.000> than<00:16:20.360> one<00:16:20.839> monolithic<00:16:21.720> big 00:16:22.030 --> 00:16:22.040 align:start position:0% contracts than one monolithic big 00:16:22.040 --> 00:16:25.710 align:start position:0% contracts than one monolithic big contract<00:16:22.680> so<00:16:23.440> we<00:16:23.600> have<00:16:23.800> to<00:16:24.639> be<00:16:24.959> able<00:16:25.160> to<00:16:25.319> reason 00:16:25.710 --> 00:16:25.720 align:start position:0% contract so we have to be able to reason 00:16:25.720 --> 00:16:29.700 align:start position:0% contract so we have to be able to reason about<00:16:26.279> multiple<00:16:27.079> cooperating<00:16:28.000> cond<00:16:28.519> contract 00:16:29.700 --> 00:16:29.710 align:start position:0% about multiple cooperating cond contract 00:16:29.710 --> 00:16:31.189 align:start position:0% about multiple cooperating cond contract [Music] 00:16:31.189 --> 00:16:31.199 align:start position:0% [Music] 00:16:31.199 --> 00:16:34.949 align:start position:0% [Music] and<00:16:32.199> and<00:16:32.440> then<00:16:33.440> just<00:16:34.040> reasoning<00:16:34.639> about 00:16:34.949 --> 00:16:34.959 align:start position:0% and and then just reasoning about 00:16:34.959 --> 00:16:38.990 align:start position:0% and and then just reasoning about solidity<00:16:35.560> code<00:16:35.839> is<00:16:36.040> not<00:16:36.639> enough<00:16:37.759> because<00:16:38.759> what 00:16:38.990 --> 00:16:39.000 align:start position:0% solidity code is not enough because what 00:16:39.000 --> 00:16:41.389 align:start position:0% solidity code is not enough because what runs<00:16:39.399> on<00:16:39.639> the<00:16:39.839> blockchain<00:16:40.399> is<00:16:40.560> not<00:16:40.720> a<00:16:40.839> solidity 00:16:41.389 --> 00:16:41.399 align:start position:0% runs on the blockchain is not a solidity 00:16:41.399 --> 00:16:45.430 align:start position:0% runs on the blockchain is not a solidity code<00:16:41.920> but<00:16:42.079> a<00:16:42.360> compiled<00:16:42.959> B<00:16:43.360> code<00:16:44.319> and<00:16:45.000> sometimes 00:16:45.430 --> 00:16:45.440 align:start position:0% code but a compiled B code and sometimes 00:16:45.440 --> 00:16:50.309 align:start position:0% code but a compiled B code and sometimes the<00:16:45.720> compiler<00:16:46.720> has<00:16:47.199> a<00:16:47.639> bug<00:16:48.639> so<00:16:49.639> somehow<00:16:50.120> we 00:16:50.309 --> 00:16:50.319 align:start position:0% the compiler has a bug so somehow we 00:16:50.319 --> 00:16:54.110 align:start position:0% the compiler has a bug so somehow we have<00:16:50.480> to<00:16:51.160> know<00:16:52.000> how<00:16:52.759> the<00:16:52.959> bite<00:16:53.279> code<00:16:53.600> behaves 00:16:54.110 --> 00:16:54.120 align:start position:0% have to know how the bite code behaves 00:16:54.120 --> 00:16:56.749 align:start position:0% have to know how the bite code behaves whether<00:16:54.399> it's<00:16:54.600> evm<00:16:55.199> or<00:16:55.440> the<00:16:55.600> evm<00:16:56.000> 2<00:16:56.360> the<00:16:56.480> second 00:16:56.749 --> 00:16:56.759 align:start position:0% whether it's evm or the evm 2 the second 00:16:56.759 --> 00:16:59.870 align:start position:0% whether it's evm or the evm 2 the second one<00:16:57.600> um 00:16:59.870 --> 00:16:59.880 align:start position:0% one um 00:16:59.880 --> 00:17:04.270 align:start position:0% one um so<00:17:00.120> somehow<00:17:00.440> we<00:17:00.560> have<00:17:00.680> to<00:17:00.800> do<00:17:01.000> that<00:17:01.279> but<00:17:01.880> um 00:17:04.270 --> 00:17:04.280 align:start position:0% so somehow we have to do that but um 00:17:04.280 --> 00:17:09.270 align:start position:0% so somehow we have to do that but um that's<00:17:05.280> easier<00:17:05.839> than<00:17:06.400> most<00:17:07.400> CPU 00:17:09.270 --> 00:17:09.280 align:start position:0% that's easier than most CPU 00:17:09.280 --> 00:17:11.990 align:start position:0% that's easier than most CPU architectures<00:17:10.280> out<00:17:10.679> there<00:17:11.079> so<00:17:11.319> I<00:17:11.480> think<00:17:11.839> this 00:17:11.990 --> 00:17:12.000 align:start position:0% architectures out there so I think this 00:17:12.000 --> 00:17:15.990 align:start position:0% architectures out there so I think this is<00:17:12.160> a<00:17:12.319> solvable<00:17:12.959> problem<00:17:13.959> um<00:17:14.919> the<00:17:15.120> next<00:17:15.360> one<00:17:15.600> is 00:17:15.990 --> 00:17:16.000 align:start position:0% is a solvable problem um the next one is 00:17:16.000 --> 00:17:18.470 align:start position:0% is a solvable problem um the next one is uh<00:17:16.160> multi<00:17:16.600> transaction<00:17:17.319> conditions<00:17:17.600> So 00:17:18.470 --> 00:17:18.480 align:start position:0% uh multi transaction conditions So 00:17:18.480 --> 00:17:20.870 align:start position:0% uh multi transaction conditions So currently<00:17:19.480> the<00:17:19.679> precondition<00:17:20.400> post 00:17:20.870 --> 00:17:20.880 align:start position:0% currently the precondition post 00:17:20.880 --> 00:17:23.510 align:start position:0% currently the precondition post condition<00:17:21.120> in<00:17:21.360> variance<00:17:21.880> on<00:17:22.199> the<00:17:22.520> contracts 00:17:23.510 --> 00:17:23.520 align:start position:0% condition in variance on the contracts 00:17:23.520 --> 00:17:25.390 align:start position:0% condition in variance on the contracts uh<00:17:23.760> just<00:17:24.120> on<00:17:24.520> one 00:17:25.390 --> 00:17:25.400 align:start position:0% uh just on one 00:17:25.400 --> 00:17:28.909 align:start position:0% uh just on one cord<00:17:26.400> um<00:17:26.959> it<00:17:27.079> can<00:17:27.280> already<00:17:27.559> deal<00:17:27.919> with<00:17:28.199> the<00:17:28.559> re 00:17:28.909 --> 00:17:28.919 align:start position:0% cord um it can already deal with the re 00:17:28.919 --> 00:17:33.630 align:start position:0% cord um it can already deal with the re entrance<00:17:29.880> but<00:17:30.440> uh<00:17:30.799> from<00:17:31.160> the<00:17:31.480> first<00:17:31.880> call<00:17:32.640> to 00:17:33.630 --> 00:17:33.640 align:start position:0% entrance but uh from the first call to 00:17:33.640 --> 00:17:37.549 align:start position:0% entrance but uh from the first call to the<00:17:34.000> last<00:17:34.559> return<00:17:34.880> and<00:17:35.160> that's<00:17:35.919> the<00:17:36.919> range<00:17:37.320> of 00:17:37.549 --> 00:17:37.559 align:start position:0% the last return and that's the range of 00:17:37.559 --> 00:17:40.909 align:start position:0% the last return and that's the range of verification<00:17:38.320> we<00:17:38.559> need<00:17:38.919> to<00:17:39.600> extend 00:17:40.909 --> 00:17:40.919 align:start position:0% verification we need to extend 00:17:40.919 --> 00:17:45.470 align:start position:0% verification we need to extend that<00:17:41.919> um<00:17:42.799> and<00:17:43.000> then<00:17:44.000> yes<00:17:44.440> and<00:17:44.679> combination 00:17:45.470 --> 00:17:45.480 align:start position:0% that um and then yes and combination 00:17:45.480 --> 00:17:49.510 align:start position:0% that um and then yes and combination with<00:17:45.720> offchain<00:17:46.360> protocol<00:17:47.200> um<00:17:47.640> this<00:17:47.799> is<00:17:48.000> harder 00:17:49.510 --> 00:17:49.520 align:start position:0% with offchain protocol um this is harder 00:17:49.520 --> 00:17:53.549 align:start position:0% with offchain protocol um this is harder because<00:17:50.520> the<00:17:50.720> moment<00:17:51.320> we<00:17:51.880> get<00:17:52.280> off<00:17:52.640> the 00:17:53.549 --> 00:17:53.559 align:start position:0% because the moment we get off the 00:17:53.559 --> 00:17:55.549 align:start position:0% because the moment we get off the blockchain<00:17:54.559> um 00:17:55.549 --> 00:17:55.559 align:start position:0% blockchain um 00:17:55.559 --> 00:17:59.549 align:start position:0% blockchain um people's<00:17:56.799> behavior<00:17:57.799> or<00:17:58.559> yeah<00:17:58.960> are<00:17:59.200> not 00:17:59.549 --> 00:17:59.559 align:start position:0% people's behavior or yeah are not 00:17:59.559 --> 00:18:01.070 align:start position:0% people's behavior or yeah are not constrained 00:18:01.070 --> 00:18:01.080 align:start position:0% constrained 00:18:01.080 --> 00:18:04.870 align:start position:0% constrained by<00:18:02.080> clear<00:18:02.440> rules<00:18:03.120> so<00:18:03.640> what's<00:18:03.960> good<00:18:04.159> for<00:18:04.520> people 00:18:04.870 --> 00:18:04.880 align:start position:0% by clear rules so what's good for people 00:18:04.880 --> 00:18:09.070 align:start position:0% by clear rules so what's good for people is<00:18:05.080> not<00:18:05.559> very<00:18:06.320> well<00:18:06.840> defined<00:18:07.520> but<00:18:07.880> somehow<00:18:08.880> we 00:18:09.070 --> 00:18:09.080 align:start position:0% is not very well defined but somehow we 00:18:09.080 --> 00:18:13.710 align:start position:0% is not very well defined but somehow we have<00:18:09.280> to<00:18:09.840> Def<00:18:10.200> Define<00:18:10.520> a<00:18:10.720> game<00:18:11.440> where<00:18:12.440> it's<00:18:13.400> in 00:18:13.710 --> 00:18:13.720 align:start position:0% have to Def Define a game where it's in 00:18:13.720 --> 00:18:17.149 align:start position:0% have to Def Define a game where it's in the<00:18:13.919> players's<00:18:14.440> interest<00:18:15.400> to<00:18:15.960> be<00:18:16.880> to 00:18:17.149 --> 00:18:17.159 align:start position:0% the players's interest to be to 00:18:17.159 --> 00:18:20.750 align:start position:0% the players's interest to be to coordinate<00:18:17.840> with<00:18:18.039> the<00:18:18.600> rules 00:18:20.750 --> 00:18:20.760 align:start position:0% coordinate with the rules 00:18:20.760 --> 00:18:23.870 align:start position:0% coordinate with the rules um<00:18:21.760> and<00:18:21.919> the<00:18:22.039> formal<00:18:22.400> methods<00:18:22.840> can<00:18:23.120> help<00:18:23.440> here 00:18:23.870 --> 00:18:23.880 align:start position:0% um and the formal methods can help here 00:18:23.880 --> 00:18:27.830 align:start position:0% um and the formal methods can help here because<00:18:24.400> it<00:18:24.640> can<00:18:25.400> explore<00:18:26.280> all<00:18:27.039> possibilities 00:18:27.830 --> 00:18:27.840 align:start position:0% because it can explore all possibilities 00:18:27.840 --> 00:18:30.149 align:start position:0% because it can explore all possibilities of<00:18:28.080> interaction 00:18:30.149 --> 00:18:30.159 align:start position:0% of interaction 00:18:30.159 --> 00:18:34.270 align:start position:0% of interaction um<00:18:30.840> the<00:18:31.080> last<00:18:31.360> point<00:18:31.640> is<00:18:32.000> rather<00:18:32.919> practical<00:18:33.840> um 00:18:34.270 --> 00:18:34.280 align:start position:0% um the last point is rather practical um 00:18:34.280 --> 00:18:37.110 align:start position:0% um the last point is rather practical um so<00:18:34.480> you<00:18:34.640> saw<00:18:34.919> some<00:18:35.240> blue<00:18:35.760> question<00:18:36.120> marks<00:18:36.919> but 00:18:37.110 --> 00:18:37.120 align:start position:0% so you saw some blue question marks but 00:18:37.120 --> 00:18:39.909 align:start position:0% so you saw some blue question marks but just<00:18:37.320> a<00:18:37.600> question<00:18:38.000> mark<00:18:38.440> is<00:18:39.360> sometimes<00:18:39.640> not 00:18:39.909 --> 00:18:39.919 align:start position:0% just a question mark is sometimes not 00:18:39.919 --> 00:18:43.190 align:start position:0% just a question mark is sometimes not enough<00:18:40.360> for<00:18:40.919> me<00:18:41.240> to<00:18:41.919> understand<00:18:42.200> the<00:18:42.400> problem 00:18:43.190 --> 00:18:43.200 align:start position:0% enough for me to understand the problem 00:18:43.200 --> 00:18:46.549 align:start position:0% enough for me to understand the problem so<00:18:43.559> it<00:18:43.720> would<00:18:44.039> help<00:18:44.880> if<00:18:45.159> we<00:18:45.360> can<00:18:45.559> see<00:18:46.080> counter 00:18:46.549 --> 00:18:46.559 align:start position:0% so it would help if we can see counter 00:18:46.559 --> 00:18:49.230 align:start position:0% so it would help if we can see counter examples<00:18:47.159> like<00:18:47.720> with<00:18:47.960> this<00:18:48.200> input<00:18:48.720> with<00:18:49.000> this 00:18:49.230 --> 00:18:49.240 align:start position:0% examples like with this input with this 00:18:49.240 --> 00:18:51.990 align:start position:0% examples like with this input with this state<00:18:49.679> this<00:18:49.840> is<00:18:50.039> broken<00:18:50.799> and<00:18:51.039> then<00:18:51.520> um<00:18:51.760> it's 00:18:51.990 --> 00:18:52.000 align:start position:0% state this is broken and then um it's 00:18:52.000 --> 00:18:53.750 align:start position:0% state this is broken and then um it's more<00:18:52.280> easily 00:18:53.750 --> 00:18:53.760 align:start position:0% more easily 00:18:53.760 --> 00:18:56.470 align:start position:0% more easily understood<00:18:54.760> um 00:18:56.470 --> 00:18:56.480 align:start position:0% understood um 00:18:56.480 --> 00:18:59.789 align:start position:0% understood um but<00:18:57.480> I<00:18:57.720> see<00:18:58.360> I<00:18:58.480> believe 00:18:59.789 --> 00:18:59.799 align:start position:0% but I see I believe 00:18:59.799 --> 00:19:01.870 align:start position:0% but I see I believe many<00:19:00.280> more<00:19:00.799> formal<00:19:01.240> verification 00:19:01.870 --> 00:19:01.880 align:start position:0% many more formal verification 00:19:01.880 --> 00:19:04.390 align:start position:0% many more formal verification researchers<00:19:02.840> are<00:19:03.120> coming<00:19:03.640> to<00:19:04.159> the 00:19:04.390 --> 00:19:04.400 align:start position:0% researchers are coming to the 00:19:04.400 --> 00:19:06.789 align:start position:0% researchers are coming to the verification<00:19:05.039> of<00:19:05.320> vum<00:19:05.880> smart 00:19:06.789 --> 00:19:06.799 align:start position:0% verification of vum smart 00:19:06.799 --> 00:19:10.350 align:start position:0% verification of vum smart contracts<00:19:07.799> because<00:19:08.400> of<00:19:09.280> the<00:19:09.600> reason<00:19:10.159> I 00:19:10.350 --> 00:19:10.360 align:start position:0% contracts because of the reason I 00:19:10.360 --> 00:19:13.390 align:start position:0% contracts because of the reason I mentioned<00:19:11.120> thism<00:19:11.760> virtual<00:19:12.120> machine<00:19:12.559> is<00:19:12.880> V 00:19:13.390 --> 00:19:13.400 align:start position:0% mentioned thism virtual machine is V 00:19:13.400 --> 00:19:15.350 align:start position:0% mentioned thism virtual machine is V Paradise<00:19:14.000> for<00:19:14.280> formal<00:19:14.679> verification 00:19:15.350 --> 00:19:15.360 align:start position:0% Paradise for formal verification 00:19:15.360 --> 00:19:19.230 align:start position:0% Paradise for formal verification engineer<00:19:16.159> thank<00:19:16.320> you<00:19:16.520> very 00:19:19.230 --> 00:19:19.240 align:start position:0% 00:19:19.240 --> 00:19:21.720 align:start position:0% much<00:19:20.240> thank<00:19:20.400> you 00:19:21.720 --> 00:19:21.730 align:start position:0% much thank you 00:19:21.730 --> 00:19:27.710 align:start position:0% much thank you [Music] 00:19:27.710 --> 00:19:27.720 align:start position:0% [Music] 00:19:27.720 --> 00:19:30.799 align:start position:0% [Music] Yi<00:19:28.720> and