WEBVTT Kind: captions Language: en 00:00:00.000 --> 00:00:04.350 align:start position:0% foreign 00:00:04.350 --> 00:00:04.360 align:start position:0% 00:00:04.360 --> 00:00:13.310 align:start position:0% [Music] 00:00:13.310 --> 00:00:13.320 align:start position:0% 00:00:13.320 --> 00:00:16.849 align:start position:0% thank<00:00:14.040> you<00:00:14.160> for<00:00:14.580> making<00:00:14.940> it<00:00:15.240> today 00:00:16.849 --> 00:00:16.859 align:start position:0% thank you for making it today 00:00:16.859 --> 00:00:17.630 align:start position:0% thank you for making it today um 00:00:17.630 --> 00:00:17.640 align:start position:0% um 00:00:17.640 --> 00:00:21.109 align:start position:0% um as<00:00:18.180> the<00:00:18.420> title<00:00:19.020> says<00:00:19.320> I'll<00:00:19.560> be<00:00:19.880> presenting<00:00:20.880> on 00:00:21.109 --> 00:00:21.119 align:start position:0% as the title says I'll be presenting on 00:00:21.119 --> 00:00:23.750 align:start position:0% as the title says I'll be presenting on our<00:00:21.359> work<00:00:21.840> on<00:00:22.080> formally<00:00:22.619> specifying<00:00:23.279> and 00:00:23.750 --> 00:00:23.760 align:start position:0% our work on formally specifying and 00:00:23.760 --> 00:00:25.849 align:start position:0% our work on formally specifying and formally<00:00:24.180> verifying<00:00:24.840> the<00:00:25.320> distributed 00:00:25.849 --> 00:00:25.859 align:start position:0% formally verifying the distributed 00:00:25.859 --> 00:00:27.890 align:start position:0% formally verifying the distributed validator<00:00:26.220> technology<00:00:26.760> protocol 00:00:27.890 --> 00:00:27.900 align:start position:0% validator technology protocol 00:00:27.900 --> 00:00:30.550 align:start position:0% validator technology protocol and<00:00:28.500> the<00:00:28.920> way<00:00:29.039> I'm<00:00:29.220> going<00:00:29.340> to<00:00:29.519> do<00:00:29.640> so<00:00:29.820> is<00:00:30.300> by 00:00:30.550 --> 00:00:30.560 align:start position:0% and the way I'm going to do so is by 00:00:30.560 --> 00:00:33.950 align:start position:0% and the way I'm going to do so is by answering<00:00:31.560> to<00:00:32.099> four<00:00:32.399> key<00:00:32.700> questions 00:00:33.950 --> 00:00:33.960 align:start position:0% answering to four key questions 00:00:33.960 --> 00:00:36.830 align:start position:0% answering to four key questions why<00:00:34.620> do<00:00:34.739> we<00:00:34.920> need<00:00:35.100> a<00:00:35.579> distributed<00:00:36.480> validator 00:00:36.830 --> 00:00:36.840 align:start position:0% why do we need a distributed validator 00:00:36.840 --> 00:00:39.290 align:start position:0% why do we need a distributed validator in<00:00:37.440> the<00:00:37.500> first<00:00:37.680> place<00:00:37.920> why<00:00:38.700> do<00:00:38.880> we<00:00:39.000> need<00:00:39.120> to 00:00:39.290 --> 00:00:39.300 align:start position:0% in the first place why do we need to 00:00:39.300 --> 00:00:42.470 align:start position:0% in the first place why do we need to formally<00:00:39.600> specify<00:00:40.200> and<00:00:40.800> formally<00:00:41.160> verify<00:00:41.700> the 00:00:42.470 --> 00:00:42.480 align:start position:0% formally specify and formally verify the 00:00:42.480 --> 00:00:45.590 align:start position:0% formally specify and formally verify the distributed<00:00:43.020> by<00:00:43.140> data<00:00:43.440> technology<00:00:43.860> protocol 00:00:45.590 --> 00:00:45.600 align:start position:0% distributed by data technology protocol 00:00:45.600 --> 00:00:48.470 align:start position:0% distributed by data technology protocol how<00:00:46.140> does<00:00:46.379> our<00:00:46.680> formula<00:00:47.399> specification<00:00:47.940> look 00:00:48.470 --> 00:00:48.480 align:start position:0% how does our formula specification look 00:00:48.480 --> 00:00:49.670 align:start position:0% how does our formula specification look like<00:00:48.660> and 00:00:49.670 --> 00:00:49.680 align:start position:0% like and 00:00:49.680 --> 00:00:51.590 align:start position:0% like and finally<00:00:50.219> what<00:00:50.640> they've<00:00:50.940> actually<00:00:51.059> achieved 00:00:51.590 --> 00:00:51.600 align:start position:0% finally what they've actually achieved 00:00:51.600 --> 00:00:54.410 align:start position:0% finally what they've actually achieved so<00:00:51.719> far<00:00:51.960> and<00:00:52.680> what<00:00:53.160> is<00:00:53.340> left<00:00:53.640> to<00:00:53.879> do<00:00:54.000> but<00:00:54.239> before 00:00:54.410 --> 00:00:54.420 align:start position:0% so far and what is left to do but before 00:00:54.420 --> 00:00:57.189 align:start position:0% so far and what is left to do but before diving<00:00:55.020> into<00:00:55.399> answering<00:00:56.399> to<00:00:56.699> these<00:00:57.000> questions 00:00:57.189 --> 00:00:57.199 align:start position:0% diving into answering to these questions 00:00:57.199 --> 00:01:01.250 align:start position:0% diving into answering to these questions some<00:00:58.199> do<00:00:58.440> acknowledgments<00:00:59.640> this<00:01:00.600> work<00:01:00.780> has 00:01:01.250 --> 00:01:01.260 align:start position:0% some do acknowledgments this work has 00:01:01.260 --> 00:01:04.549 align:start position:0% some do acknowledgments this work has been<00:01:01.440> carried<00:01:01.800> out<00:01:01.920> by<00:01:02.399> consensus<00:01:03.300> r<00:01:03.660> d 00:01:04.549 --> 00:01:04.559 align:start position:0% been carried out by consensus r d 00:01:04.559 --> 00:01:07.789 align:start position:0% been carried out by consensus r d as<00:01:05.100> I<00:01:05.280> received<00:01:05.700> a<00:01:05.939> grant<00:01:06.540> co-founded<00:01:07.380> by<00:01:07.619> the 00:01:07.789 --> 00:01:07.799 align:start position:0% as I received a grant co-founded by the 00:01:07.799 --> 00:01:11.109 align:start position:0% as I received a grant co-founded by the ethereum<00:01:08.159> foundation<00:01:08.659> oval<00:01:09.659> and<00:01:10.140> SSV<00:01:10.680> Network 00:01:11.109 --> 00:01:11.119 align:start position:0% ethereum foundation oval and SSV Network 00:01:11.119 --> 00:01:14.270 align:start position:0% ethereum foundation oval and SSV Network also<00:01:12.119> I'm<00:01:12.299> here<00:01:12.540> presenting<00:01:13.020> the<00:01:13.200> work<00:01:13.860> but 00:01:14.270 --> 00:01:14.280 align:start position:0% also I'm here presenting the work but 00:01:14.280 --> 00:01:16.730 align:start position:0% also I'm here presenting the work but this<00:01:14.520> was<00:01:14.760> done<00:01:14.939> together<00:01:15.240> with<00:01:15.780> tanaitran 00:01:16.730 --> 00:01:16.740 align:start position:0% this was done together with tanaitran 00:01:16.740 --> 00:01:18.649 align:start position:0% this was done together with tanaitran who<00:01:17.159> is<00:01:17.280> one<00:01:17.460> of<00:01:17.580> my<00:01:17.760> colleagues<00:01:18.119> in<00:01:18.420> the 00:01:18.649 --> 00:01:18.659 align:start position:0% who is one of my colleagues in the 00:01:18.659 --> 00:01:20.749 align:start position:0% who is one of my colleagues in the distributed<00:01:19.500> system<00:01:19.740> formal<00:01:20.280> verification 00:01:20.749 --> 00:01:20.759 align:start position:0% distributed system formal verification 00:01:20.759 --> 00:01:23.510 align:start position:0% distributed system formal verification team<00:01:21.119> at<00:01:21.600> consensus<00:01:22.200> everybody<00:01:22.680> I<00:01:23.159> think<00:01:23.340> so 00:01:23.510 --> 00:01:23.520 align:start position:0% team at consensus everybody I think so 00:01:23.520 --> 00:01:26.390 align:start position:0% team at consensus everybody I think so at<00:01:23.700> least<00:01:23.880> I<00:01:24.540> can<00:01:24.780> start<00:01:25.439> answering<00:01:26.040> to<00:01:26.220> the 00:01:26.390 --> 00:01:26.400 align:start position:0% at least I can start answering to the 00:01:26.400 --> 00:01:28.609 align:start position:0% at least I can start answering to the first<00:01:26.580> quick<00:01:26.939> questions 00:01:28.609 --> 00:01:28.619 align:start position:0% first quick questions 00:01:28.619 --> 00:01:30.350 align:start position:0% first quick questions why<00:01:28.979> do<00:01:29.220> we<00:01:29.280> need<00:01:29.400> a<00:01:29.520> distributable<00:01:30.060> validator 00:01:30.350 --> 00:01:30.360 align:start position:0% why do we need a distributable validator 00:01:30.360 --> 00:01:33.289 align:start position:0% why do we need a distributable validator now<00:01:30.720> if<00:01:31.140> you<00:01:31.259> are<00:01:31.380> here<00:01:31.560> before<00:01:31.820> the<00:01:32.820> talk<00:01:33.000> by 00:01:33.289 --> 00:01:33.299 align:start position:0% now if you are here before the talk by 00:01:33.299 --> 00:01:35.149 align:start position:0% now if you are here before the talk by Colin<00:01:33.720> Eisen<00:01:34.200> you<00:01:34.439> may<00:01:34.619> already<00:01:34.740> know<00:01:34.979> about 00:01:35.149 --> 00:01:35.159 align:start position:0% Colin Eisen you may already know about 00:01:35.159 --> 00:01:38.749 align:start position:0% Colin Eisen you may already know about why<00:01:35.579> but<00:01:36.299> I'll<00:01:36.659> briefly<00:01:37.140> go<00:01:37.320> over<00:01:37.500> it<00:01:38.159> actually 00:01:38.749 --> 00:01:38.759 align:start position:0% why but I'll briefly go over it actually 00:01:38.759 --> 00:01:42.230 align:start position:0% why but I'll briefly go over it actually the<00:01:39.060> way<00:01:39.659> I<00:01:40.200> go<00:01:40.320> over<00:01:40.500> it<00:01:40.799> it<00:01:41.520> will<00:01:41.759> be<00:01:41.880> by 00:01:42.230 --> 00:01:42.240 align:start position:0% the way I go over it it will be by 00:01:42.240 --> 00:01:45.289 align:start position:0% the way I go over it it will be by answering<00:01:43.140> to<00:01:43.259> another<00:01:43.439> question 00:01:45.289 --> 00:01:45.299 align:start position:0% answering to another question 00:01:45.299 --> 00:01:47.330 align:start position:0% answering to another question what<00:01:45.780> can<00:01:45.900> go<00:01:46.079> wrong<00:01:46.200> with<00:01:46.680> an<00:01:46.799> ethereumable 00:01:47.330 --> 00:01:47.340 align:start position:0% what can go wrong with an ethereumable 00:01:47.340 --> 00:01:48.410 align:start position:0% what can go wrong with an ethereumable data 00:01:48.410 --> 00:01:48.420 align:start position:0% data 00:01:48.420 --> 00:01:50.749 align:start position:0% data well<00:01:48.840> there<00:01:49.140> are<00:01:49.259> two<00:01:49.439> things<00:01:49.680> at<00:01:50.100> least<00:01:50.280> that 00:01:50.749 --> 00:01:50.759 align:start position:0% well there are two things at least that 00:01:50.759 --> 00:01:53.210 align:start position:0% well there are two things at least that can<00:01:50.939> go<00:01:51.060> wrong<00:01:51.180> with<00:01:51.420> an<00:01:51.540> ethereum<00:01:51.899> validator 00:01:53.210 --> 00:01:53.220 align:start position:0% can go wrong with an ethereum validator 00:01:53.220 --> 00:01:55.730 align:start position:0% can go wrong with an ethereum validator the<00:01:53.640> first<00:01:53.759> one<00:01:54.000> is<00:01:54.299> that<00:01:54.540> your<00:01:55.079> ethereum<00:01:55.560> no 00:01:55.730 --> 00:01:55.740 align:start position:0% the first one is that your ethereum no 00:01:55.740 --> 00:01:58.010 align:start position:0% the first one is that your ethereum no ethereum<00:01:56.159> validator<00:01:56.579> might<00:01:57.060> fail<00:01:57.360> and<00:01:57.899> let's 00:01:58.010 --> 00:01:58.020 align:start position:0% ethereum validator might fail and let's 00:01:58.020 --> 00:01:59.630 align:start position:0% ethereum validator might fail and let's see<00:01:58.200> what<00:01:58.320> this<00:01:58.500> means 00:01:59.630 --> 00:01:59.640 align:start position:0% see what this means 00:01:59.640 --> 00:02:01.789 align:start position:0% see what this means now<00:02:00.060> you<00:02:00.180> know<00:02:00.360> you<00:02:00.540> have<00:02:00.659> your<00:02:00.840> slots<00:02:01.259> in<00:02:01.619> some 00:02:01.789 --> 00:02:01.799 align:start position:0% now you know you have your slots in some 00:02:01.799 --> 00:02:03.350 align:start position:0% now you know you have your slots in some of<00:02:01.920> the<00:02:02.100> slots<00:02:02.399> you<00:02:02.579> have<00:02:02.700> to<00:02:02.820> propose<00:02:03.119> another 00:02:03.350 --> 00:02:03.360 align:start position:0% of the slots you have to propose another 00:02:03.360 --> 00:02:05.569 align:start position:0% of the slots you have to propose another you<00:02:03.780> are<00:02:03.899> a<00:02:04.200> tester<00:02:04.619> and<00:02:04.979> your<00:02:05.159> ethereum 00:02:05.569 --> 00:02:05.579 align:start position:0% you are a tester and your ethereum 00:02:05.579 --> 00:02:08.150 align:start position:0% you are a tester and your ethereum validator<00:02:06.000> is<00:02:06.360> working<00:02:06.899> what<00:02:07.619> this<00:02:07.799> means<00:02:08.039> is 00:02:08.150 --> 00:02:08.160 align:start position:0% validator is working what this means is 00:02:08.160 --> 00:02:10.910 align:start position:0% validator is working what this means is that<00:02:08.399> it<00:02:08.640> produces<00:02:09.119> blocks<00:02:09.599> you<00:02:10.140> get<00:02:10.319> you<00:02:10.739> get 00:02:10.910 --> 00:02:10.920 align:start position:0% that it produces blocks you get you get 00:02:10.920 --> 00:02:14.210 align:start position:0% that it produces blocks you get you get Rewards<00:02:11.879> produces<00:02:12.840> attestations<00:02:13.500> you<00:02:13.980> get 00:02:14.210 --> 00:02:14.220 align:start position:0% Rewards produces attestations you get 00:02:14.220 --> 00:02:15.470 align:start position:0% Rewards produces attestations you get Rewards 00:02:15.470 --> 00:02:15.480 align:start position:0% Rewards 00:02:15.480 --> 00:02:18.290 align:start position:0% Rewards but<00:02:16.020> now<00:02:16.260> suppose<00:02:16.800> that<00:02:16.920> your<00:02:17.099> node<00:02:17.340> fails<00:02:17.760> but 00:02:18.290 --> 00:02:18.300 align:start position:0% but now suppose that your node fails but 00:02:18.300 --> 00:02:19.670 align:start position:0% but now suppose that your node fails but what's<00:02:18.540> going<00:02:18.720> to<00:02:18.840> happen<00:02:18.900> is<00:02:19.200> you<00:02:19.500> start 00:02:19.670 --> 00:02:19.680 align:start position:0% what's going to happen is you start 00:02:19.680 --> 00:02:22.610 align:start position:0% what's going to happen is you start missing<00:02:20.160> uh<00:02:20.819> your<00:02:21.060> duties<00:02:21.480> so<00:02:22.200> if<00:02:22.379> you<00:02:22.500> miss 00:02:22.610 --> 00:02:22.620 align:start position:0% missing uh your duties so if you miss 00:02:22.620 --> 00:02:24.650 align:start position:0% missing uh your duties so if you miss the<00:02:22.800> blog<00:02:23.099> you<00:02:23.640> don't<00:02:23.760> receive<00:02:24.060> rewards<00:02:24.480> if 00:02:24.650 --> 00:02:24.660 align:start position:0% the blog you don't receive rewards if 00:02:24.660 --> 00:02:26.150 align:start position:0% the blog you don't receive rewards if you<00:02:24.780> miss<00:02:24.840> an<00:02:25.020> attestation<00:02:25.440> you<00:02:26.040> don't 00:02:26.150 --> 00:02:26.160 align:start position:0% you miss an attestation you don't 00:02:26.160 --> 00:02:28.729 align:start position:0% you miss an attestation you don't receive<00:02:26.520> the<00:02:26.580> rules<00:02:26.819> you<00:02:27.060> also<00:02:27.300> get<00:02:27.420> penalized 00:02:28.729 --> 00:02:28.739 align:start position:0% receive the rules you also get penalized 00:02:28.739 --> 00:02:31.070 align:start position:0% receive the rules you also get penalized what<00:02:29.099> this<00:02:29.280> means<00:02:29.580> basically<00:02:30.120> with<00:02:30.599> what<00:02:30.900> can 00:02:31.070 --> 00:02:31.080 align:start position:0% what this means basically with what can 00:02:31.080 --> 00:02:33.710 align:start position:0% what this means basically with what can happen<00:02:31.200> with<00:02:31.560> a<00:02:31.680> node<00:02:31.860> failure<00:02:32.340> is<00:02:33.000> that<00:02:33.300> you 00:02:33.710 --> 00:02:33.720 align:start position:0% happen with a node failure is that you 00:02:33.720 --> 00:02:35.630 align:start position:0% happen with a node failure is that you Minister<00:02:34.020> rewards<00:02:34.500> and<00:02:34.620> you<00:02:34.800> also<00:02:35.040> can<00:02:35.160> incorp 00:02:35.630 --> 00:02:35.640 align:start position:0% Minister rewards and you also can incorp 00:02:35.640 --> 00:02:37.070 align:start position:0% Minister rewards and you also can incorp penalties 00:02:37.070 --> 00:02:37.080 align:start position:0% penalties 00:02:37.080 --> 00:02:39.410 align:start position:0% penalties the<00:02:37.500> second<00:02:37.680> thing<00:02:37.920> that<00:02:38.160> can<00:02:38.340> go<00:02:38.459> wrong 00:02:39.410 --> 00:02:39.420 align:start position:0% the second thing that can go wrong 00:02:39.420 --> 00:02:42.229 align:start position:0% the second thing that can go wrong is<00:02:40.020> that<00:02:40.260> the<00:02:40.560> validator<00:02:40.980> key<00:02:41.340> might<00:02:41.940> be 00:02:42.229 --> 00:02:42.239 align:start position:0% is that the validator key might be 00:02:42.239 --> 00:02:43.970 align:start position:0% is that the validator key might be compromised<00:02:42.900> and<00:02:43.200> let's<00:02:43.500> see<00:02:43.680> what<00:02:43.800> this 00:02:43.970 --> 00:02:43.980 align:start position:0% compromised and let's see what this 00:02:43.980 --> 00:02:46.610 align:start position:0% compromised and let's see what this means<00:02:44.280> assuming<00:02:45.060> your<00:02:45.599> Assyrian<00:02:46.200> validator 00:02:46.610 --> 00:02:46.620 align:start position:0% means assuming your Assyrian validator 00:02:46.620 --> 00:02:49.729 align:start position:0% means assuming your Assyrian validator with<00:02:46.920> your<00:02:47.160> validator<00:02:48.000> signing<00:02:48.480> key<00:02:49.080> now<00:02:49.560> in 00:02:49.729 --> 00:02:49.739 align:start position:0% with your validator signing key now in 00:02:49.739 --> 00:02:51.890 align:start position:0% with your validator signing key now in malicious<00:02:50.099> note<00:02:50.280> is<00:02:50.519> somehow<00:02:50.760> able<00:02:51.120> to<00:02:51.239> steal 00:02:51.890 --> 00:02:51.900 align:start position:0% malicious note is somehow able to steal 00:02:51.900 --> 00:02:54.770 align:start position:0% malicious note is somehow able to steal it<00:02:52.560> what<00:02:52.860> these<00:02:53.040> Mauritius<00:02:53.459> Now<00:02:53.640> can<00:02:53.879> do<00:02:54.000> can 00:02:54.770 --> 00:02:54.780 align:start position:0% it what these Mauritius Now can do can 00:02:54.780 --> 00:02:57.830 align:start position:0% it what these Mauritius Now can do can actually<00:02:54.959> produce<00:02:55.500> for<00:02:56.280> example<00:02:56.580> two 00:02:57.830 --> 00:02:57.840 align:start position:0% actually produce for example two 00:02:57.840 --> 00:03:00.410 align:start position:0% actually produce for example two at<00:02:58.379> the<00:02:58.500> station<00:02:58.879> slashable<00:02:59.879> attestation 00:03:00.410 --> 00:03:00.420 align:start position:0% at the station slashable attestation 00:03:00.420 --> 00:03:03.290 align:start position:0% at the station slashable attestation sign<00:03:01.080> with<00:03:01.440> your<00:03:01.560> validator<00:03:02.099> signing<00:03:02.580> key<00:03:02.760> and 00:03:03.290 --> 00:03:03.300 align:start position:0% sign with your validator signing key and 00:03:03.300 --> 00:03:06.350 align:start position:0% sign with your validator signing key and package<00:03:03.780> all<00:03:04.560> of<00:03:04.680> this<00:03:04.860> into<00:03:05.099> a<00:03:05.580> slash<00:03:05.879> improve 00:03:06.350 --> 00:03:06.360 align:start position:0% package all of this into a slash improve 00:03:06.360 --> 00:03:09.290 align:start position:0% package all of this into a slash improve signed<00:03:06.959> with<00:03:07.019> a<00:03:07.140> malicious<00:03:07.500> note<00:03:07.760> signing<00:03:08.760> key 00:03:09.290 --> 00:03:09.300 align:start position:0% signed with a malicious note signing key 00:03:09.300 --> 00:03:11.509 align:start position:0% signed with a malicious note signing key and<00:03:09.840> propose<00:03:10.200> a<00:03:10.379> block<00:03:10.500> submit<00:03:11.099> it<00:03:11.220> to<00:03:11.340> the 00:03:11.509 --> 00:03:11.519 align:start position:0% and propose a block submit it to the 00:03:11.519 --> 00:03:13.490 align:start position:0% and propose a block submit it to the network<00:03:11.640> what's<00:03:12.239> going<00:03:12.480> to<00:03:12.599> happen<00:03:12.780> is<00:03:13.200> that 00:03:13.490 --> 00:03:13.500 align:start position:0% network what's going to happen is that 00:03:13.500 --> 00:03:15.830 align:start position:0% network what's going to happen is that of<00:03:13.860> course<00:03:13.980> you're<00:03:14.280> going<00:03:14.459> to<00:03:14.640> get<00:03:14.879> slashed 00:03:15.830 --> 00:03:15.840 align:start position:0% of course you're going to get slashed 00:03:15.840 --> 00:03:18.949 align:start position:0% of course you're going to get slashed and<00:03:16.560> some<00:03:16.739> of<00:03:16.920> your<00:03:17.040> funds<00:03:17.459> get<00:03:17.760> actually 00:03:18.949 --> 00:03:18.959 align:start position:0% and some of your funds get actually 00:03:18.959 --> 00:03:19.490 align:start position:0% and some of your funds get actually um 00:03:19.490 --> 00:03:19.500 align:start position:0% um 00:03:19.500 --> 00:03:22.070 align:start position:0% um kind<00:03:20.040> of<00:03:20.220> transfer<00:03:20.700> to<00:03:20.940> the<00:03:21.180> malicious<00:03:21.840> note 00:03:22.070 --> 00:03:22.080 align:start position:0% kind of transfer to the malicious note 00:03:22.080 --> 00:03:23.210 align:start position:0% kind of transfer to the malicious note so 00:03:23.210 --> 00:03:23.220 align:start position:0% so 00:03:23.220 --> 00:03:25.430 align:start position:0% so while<00:03:24.000> this<00:03:24.360> while<00:03:24.599> the<00:03:24.840> malicious<00:03:25.260> note 00:03:25.430 --> 00:03:25.440 align:start position:0% while this while the malicious note 00:03:25.440 --> 00:03:28.009 align:start position:0% while this while the malicious note doesn't<00:03:25.680> have<00:03:26.040> the<00:03:26.280> withdrawal<00:03:27.000> key<00:03:27.180> they<00:03:27.840> can 00:03:28.009 --> 00:03:28.019 align:start position:0% doesn't have the withdrawal key they can 00:03:28.019 --> 00:03:29.570 align:start position:0% doesn't have the withdrawal key they can still<00:03:28.200> somehow<00:03:28.560> get<00:03:28.739> some<00:03:28.920> of<00:03:29.040> your<00:03:29.159> funds<00:03:29.519> and 00:03:29.570 --> 00:03:29.580 align:start position:0% still somehow get some of your funds and 00:03:29.580 --> 00:03:31.670 align:start position:0% still somehow get some of your funds and this<00:03:29.760> is<00:03:29.879> very<00:03:30.060> bad<00:03:30.239> it's<00:03:30.360> bad<00:03:30.659> for<00:03:30.840> you<00:03:31.019> as<00:03:31.440> a 00:03:31.670 --> 00:03:31.680 align:start position:0% this is very bad it's bad for you as a 00:03:31.680 --> 00:03:33.350 align:start position:0% this is very bad it's bad for you as a Staker<00:03:32.040> it's<00:03:32.400> bad<00:03:32.580> for<00:03:32.760> the<00:03:32.879> network<00:03:33.000> because 00:03:33.350 --> 00:03:33.360 align:start position:0% Staker it's bad for the network because 00:03:33.360 --> 00:03:35.930 align:start position:0% Staker it's bad for the network because it<00:03:33.599> means<00:03:33.840> that<00:03:34.040> Malaysians<00:03:35.040> get<00:03:35.400> can<00:03:35.760> get 00:03:35.930 --> 00:03:35.940 align:start position:0% it means that Malaysians get can get 00:03:35.940 --> 00:03:37.970 align:start position:0% it means that Malaysians get can get more<00:03:36.420> and<00:03:36.599> more<00:03:36.780> power<00:03:37.019> more<00:03:37.440> and<00:03:37.560> more<00:03:37.680> stake 00:03:37.970 --> 00:03:37.980 align:start position:0% more and more power more and more stake 00:03:37.980 --> 00:03:39.710 align:start position:0% more and more power more and more stake and<00:03:38.220> we<00:03:38.400> don't<00:03:38.519> want<00:03:38.640> this<00:03:38.819> a<00:03:39.060> way<00:03:39.239> to<00:03:39.300> fix<00:03:39.480> this 00:03:39.710 --> 00:03:39.720 align:start position:0% and we don't want this a way to fix this 00:03:39.720 --> 00:03:42.170 align:start position:0% and we don't want this a way to fix this is<00:03:39.959> not<00:03:40.200> a<00:03:40.560> straightforward<00:03:41.519> as<00:03:41.700> one<00:03:42.000> might 00:03:42.170 --> 00:03:42.180 align:start position:0% is not a straightforward as one might 00:03:42.180 --> 00:03:44.570 align:start position:0% is not a straightforward as one might think<00:03:42.680> just<00:03:43.680> thinking<00:03:44.040> about<00:03:44.159> the<00:03:44.400> first 00:03:44.570 --> 00:03:44.580 align:start position:0% think just thinking about the first 00:03:44.580 --> 00:03:46.910 align:start position:0% think just thinking about the first issue<00:03:44.940> which<00:03:45.060> is<00:03:45.239> if<00:03:45.540> you<00:03:45.659> want<00:03:45.840> the<00:03:46.500> simplest 00:03:46.910 --> 00:03:46.920 align:start position:0% issue which is if you want the simplest 00:03:46.920 --> 00:03:50.390 align:start position:0% issue which is if you want the simplest one<00:03:47.700> might<00:03:47.940> think<00:03:48.120> well<00:03:48.299> let's<00:03:49.019> just<00:03:49.260> run<00:03:49.560> more 00:03:50.390 --> 00:03:50.400 align:start position:0% one might think well let's just run more 00:03:50.400 --> 00:03:53.330 align:start position:0% one might think well let's just run more than<00:03:50.580> one<00:03:50.760> ethereum<00:03:51.540> validator<00:03:51.959> and<00:03:52.260> well<00:03:52.560> we 00:03:53.330 --> 00:03:53.340 align:start position:0% than one ethereum validator and well we 00:03:53.340 --> 00:03:55.070 align:start position:0% than one ethereum validator and well we know<00:03:53.459> from<00:03:53.760> the<00:03:54.000> early<00:03:54.180> day<00:03:54.480> of<00:03:54.720> the<00:03:54.840> big 00:03:55.070 --> 00:03:55.080 align:start position:0% know from the early day of the big 00:03:55.080 --> 00:03:57.649 align:start position:0% know from the early day of the big contain<00:03:55.500> this<00:03:55.799> is<00:03:56.340> perfect<00:03:56.879> recipe<00:03:57.299> for 00:03:57.649 --> 00:03:57.659 align:start position:0% contain this is perfect recipe for 00:03:57.659 --> 00:04:00.110 align:start position:0% contain this is perfect recipe for getting<00:03:57.900> yourself<00:03:58.440> slash<00:03:58.980> too<00:03:59.220> yeah<00:03:59.519> we<00:04:00.000> know 00:04:00.110 --> 00:04:00.120 align:start position:0% getting yourself slash too yeah we know 00:04:00.120 --> 00:04:03.589 align:start position:0% getting yourself slash too yeah we know we<00:04:00.360> don't<00:04:00.480> can't<00:04:00.959> do<00:04:01.140> that<00:04:01.739> this<00:04:02.220> is<00:04:02.400> why<00:04:02.640> by 00:04:03.589 --> 00:04:03.599 align:start position:0% we don't can't do that this is why by 00:04:03.599 --> 00:04:06.309 align:start position:0% we don't can't do that this is why by the<00:04:03.780> female<00:04:03.959> Foundation 00:04:06.309 --> 00:04:06.319 align:start position:0% the female Foundation 00:04:06.319 --> 00:04:09.729 align:start position:0% the female Foundation car<00:04:07.319> and<00:04:07.680> come<00:04:07.980> up<00:04:08.099> with<00:04:08.280> the<00:04:08.580> concept<00:04:09.480> of 00:04:09.729 --> 00:04:09.739 align:start position:0% car and come up with the concept of 00:04:09.739 --> 00:04:11.990 align:start position:0% car and come up with the concept of distributed<00:04:10.739> by<00:04:10.860> data<00:04:11.159> technology<00:04:11.519> protocol 00:04:11.990 --> 00:04:12.000 align:start position:0% distributed by data technology protocol 00:04:12.000 --> 00:04:13.910 align:start position:0% distributed by data technology protocol which<00:04:12.599> is<00:04:13.140> um 00:04:13.910 --> 00:04:13.920 align:start position:0% which is um 00:04:13.920 --> 00:04:16.370 align:start position:0% which is um simplified<00:04:14.519> here<00:04:15.000> so<00:04:15.840> what<00:04:16.079> you<00:04:16.199> need 00:04:16.370 --> 00:04:16.380 align:start position:0% simplified here so what you need 00:04:16.380 --> 00:04:18.530 align:start position:0% simplified here so what you need essentially<00:04:17.100> is<00:04:17.519> you<00:04:17.639> need<00:04:17.880> a<00:04:18.060> coordination 00:04:18.530 --> 00:04:18.540 align:start position:0% essentially is you need a coordination 00:04:18.540 --> 00:04:21.349 align:start position:0% essentially is you need a coordination layer<00:04:19.019> between<00:04:19.320> the<00:04:19.620> different<00:04:19.799> nodes<00:04:20.359> you 00:04:21.349 --> 00:04:21.359 align:start position:0% layer between the different nodes you 00:04:21.359 --> 00:04:22.909 align:start position:0% layer between the different nodes you need<00:04:21.540> this<00:04:21.720> coordination<00:04:22.139> layer<00:04:22.560> because<00:04:22.740> you 00:04:22.909 --> 00:04:22.919 align:start position:0% need this coordination layer because you 00:04:22.919 --> 00:04:24.830 align:start position:0% need this coordination layer because you need<00:04:23.040> to<00:04:23.160> ensure<00:04:23.460> that 00:04:24.830 --> 00:04:24.840 align:start position:0% need to ensure that 00:04:24.840 --> 00:04:27.290 align:start position:0% need to ensure that whatever<00:04:25.320> attestations<00:04:26.100> are<00:04:26.639> submitted 00:04:27.290 --> 00:04:27.300 align:start position:0% whatever attestations are submitted 00:04:27.300 --> 00:04:29.030 align:start position:0% whatever attestations are submitted potentially<00:04:27.720> by<00:04:27.960> more<00:04:28.139> than<00:04:28.320> one<00:04:28.440> no<00:04:28.620> they<00:04:28.919> are 00:04:29.030 --> 00:04:29.040 align:start position:0% potentially by more than one no they are 00:04:29.040 --> 00:04:33.129 align:start position:0% potentially by more than one no they are not<00:04:29.220> slashable<00:04:29.940> and<00:04:30.780> this<00:04:31.199> relies<00:04:32.100> on<00:04:32.340> a 00:04:33.129 --> 00:04:33.139 align:start position:0% not slashable and this relies on a 00:04:33.139 --> 00:04:37.129 align:start position:0% not slashable and this relies on a consensus<00:04:34.160> protocol<00:04:35.160> that<00:04:35.900> so<00:04:36.900> basically 00:04:37.129 --> 00:04:37.139 align:start position:0% consensus protocol that so basically 00:04:37.139 --> 00:04:38.990 align:start position:0% consensus protocol that so basically have<00:04:37.380> a<00:04:37.500> middleware<00:04:37.919> between<00:04:38.400> the<00:04:38.639> beacon 00:04:38.990 --> 00:04:39.000 align:start position:0% have a middleware between the beacon 00:04:39.000 --> 00:04:41.570 align:start position:0% have a middleware between the beacon notes<00:04:39.360> and<00:04:39.540> the<00:04:40.139> remote<00:04:40.259> signer<00:04:40.919> and<00:04:41.460> this 00:04:41.570 --> 00:04:41.580 align:start position:0% notes and the remote signer and this 00:04:41.580 --> 00:04:44.570 align:start position:0% notes and the remote signer and this middleware<00:04:42.180> which<00:04:43.139> is<00:04:43.259> called<00:04:43.580> distributable 00:04:44.570 --> 00:04:44.580 align:start position:0% middleware which is called distributable 00:04:44.580 --> 00:04:46.909 align:start position:0% middleware which is called distributable editor<00:04:45.060> client<00:04:45.419> runs<00:04:46.139> underneath<00:04:46.620> a 00:04:46.909 --> 00:04:46.919 align:start position:0% editor client runs underneath a 00:04:46.919 --> 00:04:49.790 align:start position:0% editor client runs underneath a consensus<00:04:47.340> protocol<00:04:47.759> plus<00:04:48.360> another<00:04:49.080> layer<00:04:49.620> on 00:04:49.790 --> 00:04:49.800 align:start position:0% consensus protocol plus another layer on 00:04:49.800 --> 00:04:52.850 align:start position:0% consensus protocol plus another layer on top<00:04:49.919> that<00:04:50.340> ensures<00:04:50.759> that<00:04:51.320> we<00:04:52.320> must<00:04:52.500> ensure 00:04:52.850 --> 00:04:52.860 align:start position:0% top that ensures that we must ensure 00:04:52.860 --> 00:04:54.950 align:start position:0% top that ensures that we must ensure that<00:04:52.979> you<00:04:53.160> never<00:04:53.400> get<00:04:53.880> slashed<00:04:54.419> this<00:04:54.600> is<00:04:54.780> a 00:04:54.950 --> 00:04:54.960 align:start position:0% that you never get slashed this is a 00:04:54.960 --> 00:04:57.670 align:start position:0% that you never get slashed this is a protocol<00:04:55.199> that<00:04:55.860> allows<00:04:56.699> basically<00:04:57.120> splitting 00:04:57.670 --> 00:04:57.680 align:start position:0% protocol that allows basically splitting 00:04:57.680 --> 00:05:00.110 align:start position:0% protocol that allows basically splitting the<00:04:58.680> distributed<00:04:59.160> validator<00:04:59.520> signing<00:05:00.000> key 00:05:00.110 --> 00:05:00.120 align:start position:0% the distributed validator signing key 00:05:00.120 --> 00:05:03.170 align:start position:0% the distributed validator signing key into<00:05:00.840> different<00:05:01.500> key<00:05:01.860> shares<00:05:02.220> and<00:05:02.520> it's<00:05:02.880> a 00:05:03.170 --> 00:05:03.180 align:start position:0% into different key shares and it's a 00:05:03.180 --> 00:05:05.409 align:start position:0% into different key shares and it's a remote<00:05:03.479> signer<00:05:04.080> as<00:05:04.259> its<00:05:04.560> own<00:05:04.560> key<00:05:04.740> share<00:05:05.100> so 00:05:05.409 --> 00:05:05.419 align:start position:0% remote signer as its own key share so 00:05:05.419 --> 00:05:08.090 align:start position:0% remote signer as its own key share so none<00:05:06.419> of<00:05:06.540> the<00:05:06.720> remote<00:05:06.840> signer<00:05:07.380> as<00:05:07.620> the<00:05:07.979> full 00:05:08.090 --> 00:05:08.100 align:start position:0% none of the remote signer as the full 00:05:08.100 --> 00:05:11.330 align:start position:0% none of the remote signer as the full key<00:05:08.699> this<00:05:09.360> is<00:05:09.540> what<00:05:09.900> uh<00:05:10.320> ensures<00:05:10.860> protection 00:05:11.330 --> 00:05:11.340 align:start position:0% key this is what uh ensures protection 00:05:11.340 --> 00:05:14.810 align:start position:0% key this is what uh ensures protection and<00:05:11.580> against<00:05:12.560> uh<00:05:13.560> a<00:05:14.100> little<00:05:14.220> signing<00:05:14.639> key 00:05:14.810 --> 00:05:14.820 align:start position:0% and against uh a little signing key 00:05:14.820 --> 00:05:16.249 align:start position:0% and against uh a little signing key staining 00:05:16.249 --> 00:05:16.259 align:start position:0% staining 00:05:16.259 --> 00:05:21.290 align:start position:0% staining okay<00:05:16.800> now<00:05:17.520> we<00:05:18.300> know<00:05:18.479> why<00:05:18.840> it's<00:05:19.320> important<00:05:19.800> well 00:05:21.290 --> 00:05:21.300 align:start position:0% okay now we know why it's important well 00:05:21.300 --> 00:05:23.930 align:start position:0% okay now we know why it's important well why<00:05:21.900> do<00:05:22.020> we<00:05:22.080> need<00:05:22.259> to<00:05:22.440> formally<00:05:22.860> specify<00:05:23.400> and 00:05:23.930 --> 00:05:23.940 align:start position:0% why do we need to formally specify and 00:05:23.940 --> 00:05:25.850 align:start position:0% why do we need to formally specify and verify<00:05:24.360> such<00:05:24.660> a<00:05:24.900> protocol 00:05:25.850 --> 00:05:25.860 align:start position:0% verify such a protocol 00:05:25.860 --> 00:05:27.710 align:start position:0% verify such a protocol we<00:05:26.160> have<00:05:26.280> removed<00:05:26.639> any<00:05:26.880> single<00:05:27.240> point<00:05:27.419> of 00:05:27.710 --> 00:05:27.720 align:start position:0% we have removed any single point of 00:05:27.720 --> 00:05:31.070 align:start position:0% we have removed any single point of failure<00:05:28.139> and<00:05:28.800> so<00:05:28.979> we<00:05:29.220> have<00:05:29.400> higher<00:05:29.699> resiliency 00:05:31.070 --> 00:05:31.080 align:start position:0% failure and so we have higher resiliency 00:05:31.080 --> 00:05:33.890 align:start position:0% failure and so we have higher resiliency however<00:05:31.620> you<00:05:32.400> know<00:05:32.520> there<00:05:32.880> is<00:05:33.060> no<00:05:33.180> such<00:05:33.720> a 00:05:33.890 --> 00:05:33.900 align:start position:0% however you know there is no such a 00:05:33.900 --> 00:05:35.870 align:start position:0% however you know there is no such a thing<00:05:34.199> as<00:05:34.440> a<00:05:34.620> free<00:05:34.740> lunch 00:05:35.870 --> 00:05:35.880 align:start position:0% thing as a free lunch 00:05:35.880 --> 00:05:38.210 align:start position:0% thing as a free lunch we<00:05:36.780> have<00:05:36.900> increased<00:05:37.320> the<00:05:37.440> complexity<00:05:37.860> of<00:05:38.039> the 00:05:38.210 --> 00:05:38.220 align:start position:0% we have increased the complexity of the 00:05:38.220 --> 00:05:39.830 align:start position:0% we have increased the complexity of the system<00:05:38.400> now<00:05:38.759> we<00:05:38.880> have<00:05:39.000> a<00:05:39.120> distributed<00:05:39.660> system 00:05:39.830 --> 00:05:39.840 align:start position:0% system now we have a distributed system 00:05:39.840 --> 00:05:42.590 align:start position:0% system now we have a distributed system in<00:05:40.139> place<00:05:40.320> of<00:05:40.500> a<00:05:40.800> single<00:05:41.400> piece<00:05:41.820> of<00:05:41.880> code 00:05:42.590 --> 00:05:42.600 align:start position:0% in place of a single piece of code 00:05:42.600 --> 00:05:45.529 align:start position:0% in place of a single piece of code and<00:05:43.020> so<00:05:43.199> we<00:05:43.380> have<00:05:43.500> higher<00:05:43.919> senses<00:05:44.280> of<00:05:44.460> bugs 00:05:45.529 --> 00:05:45.539 align:start position:0% and so we have higher senses of bugs 00:05:45.539 --> 00:05:47.629 align:start position:0% and so we have higher senses of bugs and<00:05:46.020> this<00:05:46.199> is<00:05:46.320> where<00:05:46.620> firmware<00:05:47.220> verification 00:05:47.629 --> 00:05:47.639 align:start position:0% and this is where firmware verification 00:05:47.639 --> 00:05:49.430 align:start position:0% and this is where firmware verification can<00:05:48.000> really<00:05:48.180> help<00:05:48.539> us 00:05:49.430 --> 00:05:49.440 align:start position:0% can really help us 00:05:49.440 --> 00:05:51.469 align:start position:0% can really help us and<00:05:49.800> to<00:05:49.919> give<00:05:50.039> you<00:05:50.160> an<00:05:50.280> idea<00:05:50.580> of<00:05:50.699> how<00:05:50.940> it<00:05:51.300> can 00:05:51.469 --> 00:05:51.479 align:start position:0% and to give you an idea of how it can 00:05:51.479 --> 00:05:53.810 align:start position:0% and to give you an idea of how it can really<00:05:51.600> help<00:05:51.900> us<00:05:52.139> I<00:05:52.919> want<00:05:53.100> just<00:05:53.280> to<00:05:53.520> draw<00:05:53.639> a 00:05:53.810 --> 00:05:53.820 align:start position:0% really help us I want just to draw a 00:05:53.820 --> 00:05:56.570 align:start position:0% really help us I want just to draw a comparison<00:05:54.300> to<00:05:54.960> testing 00:05:56.570 --> 00:05:56.580 align:start position:0% comparison to testing 00:05:56.580 --> 00:05:59.029 align:start position:0% comparison to testing and<00:05:57.060> the<00:05:57.240> key<00:05:57.419> concept<00:05:57.840> here<00:05:58.080> is<00:05:58.440> that<00:05:58.560> formal 00:05:59.029 --> 00:05:59.039 align:start position:0% and the key concept here is that formal 00:05:59.039 --> 00:06:01.490 align:start position:0% and the key concept here is that formal verification<00:05:59.580> is<00:05:59.940> exhaustive<00:06:00.660> and<00:06:01.080> testing 00:06:01.490 --> 00:06:01.500 align:start position:0% verification is exhaustive and testing 00:06:01.500 --> 00:06:02.450 align:start position:0% verification is exhaustive and testing is<00:06:01.680> not 00:06:02.450 --> 00:06:02.460 align:start position:0% is not 00:06:02.460 --> 00:06:04.430 align:start position:0% is not to<00:06:02.820> give<00:06:02.940> you<00:06:03.060> an<00:06:03.120> idea<00:06:03.479> with<00:06:04.080> formal 00:06:04.430 --> 00:06:04.440 align:start position:0% to give you an idea with formal 00:06:04.440 --> 00:06:07.610 align:start position:0% to give you an idea with formal verification<00:06:04.860> we<00:06:05.280> can<00:06:05.600> consider<00:06:06.600> networks<00:06:07.259> of 00:06:07.610 --> 00:06:07.620 align:start position:0% verification we can consider networks of 00:06:07.620 --> 00:06:10.010 align:start position:0% verification we can consider networks of any<00:06:07.800> size<00:06:08.160> you<00:06:08.699> pick<00:06:08.880> a<00:06:09.060> number<00:06:09.180> we<00:06:09.479> can<00:06:09.720> deal 00:06:10.010 --> 00:06:10.020 align:start position:0% any size you pick a number we can deal 00:06:10.020 --> 00:06:12.590 align:start position:0% any size you pick a number we can deal with<00:06:10.259> it<00:06:10.380> you<00:06:10.860> can<00:06:10.979> do<00:06:11.160> that<00:06:11.280> with<00:06:11.520> testing<00:06:11.940> yep 00:06:12.590 --> 00:06:12.600 align:start position:0% with it you can do that with testing yep 00:06:12.600 --> 00:06:14.810 align:start position:0% with it you can do that with testing yep only<00:06:12.840> small<00:06:13.139> Network<00:06:13.380> sizes 00:06:14.810 --> 00:06:14.820 align:start position:0% only small Network sizes 00:06:14.820 --> 00:06:17.150 align:start position:0% only small Network sizes and<00:06:15.419> it's<00:06:15.600> very<00:06:15.840> important<00:06:16.440> when<00:06:16.680> it<00:06:16.800> comes<00:06:17.039> to 00:06:17.150 --> 00:06:17.160 align:start position:0% and it's very important when it comes to 00:06:17.160 --> 00:06:20.570 align:start position:0% and it's very important when it comes to Byzantine<00:06:17.820> Behavior<00:06:18.720> because<00:06:19.500> with<00:06:20.220> formal 00:06:20.570 --> 00:06:20.580 align:start position:0% Byzantine Behavior because with formal 00:06:20.580 --> 00:06:22.249 align:start position:0% Byzantine Behavior because with formal verification<00:06:20.940> we<00:06:21.180> can<00:06:21.360> really<00:06:21.479> consider<00:06:21.960> any 00:06:22.249 --> 00:06:22.259 align:start position:0% verification we can really consider any 00:06:22.259 --> 00:06:25.070 align:start position:0% verification we can really consider any any<00:06:22.620> Byzantine<00:06:23.160> Behavior<00:06:23.639> Uh<00:06:24.479> with<00:06:24.720> testing 00:06:25.070 --> 00:06:25.080 align:start position:0% any Byzantine Behavior Uh with testing 00:06:25.080 --> 00:06:27.529 align:start position:0% any Byzantine Behavior Uh with testing even<00:06:25.259> with<00:06:25.440> fuzzing<00:06:25.979> you<00:06:26.460> have<00:06:26.699> already<00:06:26.819> you 00:06:27.529 --> 00:06:27.539 align:start position:0% even with fuzzing you have already you 00:06:27.539 --> 00:06:29.390 align:start position:0% even with fuzzing you have already you can<00:06:27.660> only<00:06:27.960> consider<00:06:28.500> limited<00:06:28.979> set<00:06:29.220> of 00:06:29.390 --> 00:06:29.400 align:start position:0% can only consider limited set of 00:06:29.400 --> 00:06:31.370 align:start position:0% can only consider limited set of Byzantine<00:06:29.819> behaviors<00:06:30.300> perhaps<00:06:30.720> you<00:06:31.080> know<00:06:31.199> it 00:06:31.370 --> 00:06:31.380 align:start position:0% Byzantine behaviors perhaps you know it 00:06:31.380 --> 00:06:33.469 align:start position:0% Byzantine behaviors perhaps you know it doesn't<00:06:31.500> respond<00:06:31.979> but 00:06:33.469 --> 00:06:33.479 align:start position:0% doesn't respond but 00:06:33.479 --> 00:06:36.290 align:start position:0% doesn't respond but you<00:06:34.199> can't<00:06:34.380> really<00:06:34.759> exhaustively<00:06:35.759> consider 00:06:36.290 --> 00:06:36.300 align:start position:0% you can't really exhaustively consider 00:06:36.300 --> 00:06:39.050 align:start position:0% you can't really exhaustively consider all<00:06:36.479> of<00:06:36.660> them<00:06:36.780> also<00:06:37.740> if<00:06:38.039> you<00:06:38.160> want<00:06:38.280> to<00:06:38.460> make 00:06:39.050 --> 00:06:39.060 align:start position:0% all of them also if you want to make 00:06:39.060 --> 00:06:42.170 align:start position:0% all of them also if you want to make sure<00:06:39.240> that<00:06:39.479> a<00:06:39.660> property<00:06:40.020> is<00:06:40.560> insured<00:06:41.100> well 00:06:42.170 --> 00:06:42.180 align:start position:0% sure that a property is insured well 00:06:42.180 --> 00:06:44.150 align:start position:0% sure that a property is insured well and<00:06:42.780> and<00:06:43.020> this<00:06:43.259> property<00:06:43.620> actually<00:06:43.800> does<00:06:43.979> in 00:06:44.150 --> 00:06:44.160 align:start position:0% and and this property actually does in 00:06:44.160 --> 00:06:45.350 align:start position:0% and and this property actually does in thought<00:06:44.340> so<00:06:44.580> there<00:06:44.699> is<00:06:44.819> a<00:06:44.940> bug<00:06:45.000> in<00:06:45.240> the 00:06:45.350 --> 00:06:45.360 align:start position:0% thought so there is a bug in the 00:06:45.360 --> 00:06:47.390 align:start position:0% thought so there is a bug in the protocol<00:06:45.660> well<00:06:46.380> with<00:06:46.620> formal<00:06:46.979> verification 00:06:47.390 --> 00:06:47.400 align:start position:0% protocol well with formal verification 00:06:47.400 --> 00:06:49.490 align:start position:0% protocol well with formal verification it<00:06:48.000> can<00:06:48.180> be<00:06:48.300> detected 00:06:49.490 --> 00:06:49.500 align:start position:0% it can be detected 00:06:49.500 --> 00:06:52.610 align:start position:0% it can be detected with<00:06:50.039> testing<00:06:50.759> maybe<00:06:51.180> yes<00:06:51.600> maybe<00:06:51.900> no<00:06:52.139> it 00:06:52.610 --> 00:06:52.620 align:start position:0% with testing maybe yes maybe no it 00:06:52.620 --> 00:06:55.430 align:start position:0% with testing maybe yes maybe no it depends<00:06:52.979> uh<00:06:53.759> it's<00:06:54.240> not<00:06:54.360> exhaustive<00:06:54.900> so<00:06:55.199> you 00:06:55.430 --> 00:06:55.440 align:start position:0% depends uh it's not exhaustive so you 00:06:55.440 --> 00:06:56.629 align:start position:0% depends uh it's not exhaustive so you might<00:06:55.620> get<00:06:55.740> lucky 00:06:56.629 --> 00:06:56.639 align:start position:0% might get lucky 00:06:56.639 --> 00:06:58.909 align:start position:0% might get lucky moreover<00:06:57.360> if<00:06:57.780> a<00:06:57.900> property<00:06:58.139> is<00:06:58.319> actually<00:06:58.500> true 00:06:58.909 --> 00:06:58.919 align:start position:0% moreover if a property is actually true 00:06:58.919 --> 00:07:01.129 align:start position:0% moreover if a property is actually true well<00:06:59.759> with<00:07:00.000> phone<00:07:00.120> notification<00:07:00.660> we<00:07:00.960> can 00:07:01.129 --> 00:07:01.139 align:start position:0% well with phone notification we can 00:07:01.139 --> 00:07:03.770 align:start position:0% well with phone notification we can prove<00:07:01.440> that<00:07:01.800> is<00:07:01.979> true<00:07:02.220> when<00:07:03.120> we're<00:07:03.360> testing<00:07:03.600> we 00:07:03.770 --> 00:07:03.780 align:start position:0% prove that is true when we're testing we 00:07:03.780 --> 00:07:05.210 align:start position:0% prove that is true when we're testing we cannot<00:07:03.960> do<00:07:04.080> it<00:07:04.199> because 00:07:05.210 --> 00:07:05.220 align:start position:0% cannot do it because 00:07:05.220 --> 00:07:07.610 align:start position:0% cannot do it because again<00:07:05.639> it's<00:07:06.000> not<00:07:06.180> exhaustive<00:07:06.720> so 00:07:07.610 --> 00:07:07.620 align:start position:0% again it's not exhaustive so 00:07:07.620 --> 00:07:09.830 align:start position:0% again it's not exhaustive so this<00:07:08.039> is<00:07:08.160> the<00:07:08.400> benefit<00:07:08.520> this<00:07:09.180> is<00:07:09.300> why<00:07:09.479> formal 00:07:09.830 --> 00:07:09.840 align:start position:0% this is the benefit this is why formal 00:07:09.840 --> 00:07:11.990 align:start position:0% this is the benefit this is why formal verification<00:07:10.259> is<00:07:10.680> very<00:07:11.039> well<00:07:11.220> suited<00:07:11.580> for 00:07:11.990 --> 00:07:12.000 align:start position:0% verification is very well suited for 00:07:12.000 --> 00:07:13.790 align:start position:0% verification is very well suited for this<00:07:12.180> protocol 00:07:13.790 --> 00:07:13.800 align:start position:0% this protocol 00:07:13.800 --> 00:07:15.950 align:start position:0% this protocol now<00:07:14.340> I<00:07:14.880> want<00:07:14.940> to<00:07:15.060> give<00:07:15.180> you<00:07:15.300> an<00:07:15.419> idea<00:07:15.600> of<00:07:15.780> what 00:07:15.950 --> 00:07:15.960 align:start position:0% now I want to give you an idea of what 00:07:15.960 --> 00:07:19.129 align:start position:0% now I want to give you an idea of what formal<00:07:16.440> verification<00:07:16.919> consists<00:07:17.699> of<00:07:18.020> you<00:07:19.020> have 00:07:19.129 --> 00:07:19.139 align:start position:0% formal verification consists of you have 00:07:19.139 --> 00:07:21.529 align:start position:0% formal verification consists of you have a<00:07:19.319> formal<00:07:19.680> specification<00:07:20.220> which<00:07:21.180> essentially 00:07:21.529 --> 00:07:21.539 align:start position:0% a formal specification which essentially 00:07:21.539 --> 00:07:23.990 align:start position:0% a formal specification which essentially is<00:07:21.780> a<00:07:21.960> mathematical<00:07:22.500> definition<00:07:22.800> of<00:07:23.639> how<00:07:23.819> the 00:07:23.990 --> 00:07:24.000 align:start position:0% is a mathematical definition of how the 00:07:24.000 --> 00:07:26.089 align:start position:0% is a mathematical definition of how the protocol<00:07:24.300> is<00:07:24.539> supposed<00:07:24.720> to<00:07:24.900> behave<00:07:25.259> which 00:07:26.089 --> 00:07:26.099 align:start position:0% protocol is supposed to behave which 00:07:26.099 --> 00:07:28.070 align:start position:0% protocol is supposed to behave which says<00:07:26.460> basically<00:07:26.759> when<00:07:27.419> you<00:07:27.539> receive<00:07:27.840> message 00:07:28.070 --> 00:07:28.080 align:start position:0% says basically when you receive message 00:07:28.080 --> 00:07:31.249 align:start position:0% says basically when you receive message X<00:07:28.620> you<00:07:29.220> need<00:07:29.340> to<00:07:29.460> send<00:07:29.639> message<00:07:29.880> y 00:07:31.249 --> 00:07:31.259 align:start position:0% X you need to send message y 00:07:31.259 --> 00:07:33.230 align:start position:0% X you need to send message y then<00:07:31.800> you<00:07:32.039> have<00:07:32.220> a<00:07:32.400> property<00:07:33.000> definition 00:07:33.230 --> 00:07:33.240 align:start position:0% then you have a property definition 00:07:33.240 --> 00:07:35.629 align:start position:0% then you have a property definition which<00:07:34.139> is<00:07:34.259> a<00:07:34.440> mathematical<00:07:34.979> definition<00:07:35.220> of 00:07:35.629 --> 00:07:35.639 align:start position:0% which is a mathematical definition of 00:07:35.639 --> 00:07:36.950 align:start position:0% which is a mathematical definition of the<00:07:35.819> properties 00:07:36.950 --> 00:07:36.960 align:start position:0% the properties 00:07:36.960 --> 00:07:38.930 align:start position:0% the properties that<00:07:37.440> the<00:07:37.560> protocol<00:07:37.800> is<00:07:38.220> expecting<00:07:38.699> to 00:07:38.930 --> 00:07:38.940 align:start position:0% that the protocol is expecting to 00:07:38.940 --> 00:07:42.110 align:start position:0% that the protocol is expecting to guarantee<00:07:39.479> something<00:07:40.319> like<00:07:40.680> never<00:07:41.460> commit<00:07:41.940> a 00:07:42.110 --> 00:07:42.120 align:start position:0% guarantee something like never commit a 00:07:42.120 --> 00:07:43.490 align:start position:0% guarantee something like never commit a slashable<00:07:42.539> offense 00:07:43.490 --> 00:07:43.500 align:start position:0% slashable offense 00:07:43.500 --> 00:07:45.350 align:start position:0% slashable offense although<00:07:44.039> this<00:07:44.220> is<00:07:44.400> kind<00:07:44.639> of<00:07:44.759> packaged 00:07:45.350 --> 00:07:45.360 align:start position:0% although this is kind of packaged 00:07:45.360 --> 00:07:47.330 align:start position:0% although this is kind of packaged together<00:07:45.539> in<00:07:46.020> a<00:07:46.139> formal<00:07:46.440> proof 00:07:47.330 --> 00:07:47.340 align:start position:0% together in a formal proof 00:07:47.340 --> 00:07:49.309 align:start position:0% together in a formal proof which<00:07:47.699> is<00:07:47.819> a<00:07:48.000> mathematical<00:07:48.479> proof<00:07:48.840> that<00:07:49.080> the 00:07:49.309 --> 00:07:49.319 align:start position:0% which is a mathematical proof that the 00:07:49.319 --> 00:07:51.409 align:start position:0% which is a mathematical proof that the protocol<00:07:49.620> specification<00:07:50.400> ensures<00:07:51.180> the 00:07:51.409 --> 00:07:51.419 align:start position:0% protocol specification ensures the 00:07:51.419 --> 00:07:53.629 align:start position:0% protocol specification ensures the properties<00:07:51.780> now<00:07:52.380> what<00:07:52.620> we<00:07:52.740> do<00:07:52.860> we<00:07:53.099> take<00:07:53.280> this<00:07:53.460> a 00:07:53.629 --> 00:07:53.639 align:start position:0% properties now what we do we take this a 00:07:53.639 --> 00:07:54.770 align:start position:0% properties now what we do we take this a step<00:07:53.819> further 00:07:54.770 --> 00:07:54.780 align:start position:0% step further 00:07:54.780 --> 00:07:56.510 align:start position:0% step further and<00:07:55.139> we<00:07:55.319> work<00:07:55.500> with<00:07:55.680> machine<00:07:55.979> checkable 00:07:56.510 --> 00:07:56.520 align:start position:0% and we work with machine checkable 00:07:56.520 --> 00:08:00.290 align:start position:0% and we work with machine checkable proofs<00:07:57.000> it<00:07:57.599> means<00:07:57.780> that<00:07:57.900> our<00:07:58.080> proofs<00:07:58.620> are<00:07:59.300> very 00:08:00.290 --> 00:08:00.300 align:start position:0% proofs it means that our proofs are very 00:08:00.300 --> 00:08:02.330 align:start position:0% proofs it means that our proofs are very checked<00:08:01.080> by<00:08:01.259> a<00:08:01.440> computer 00:08:02.330 --> 00:08:02.340 align:start position:0% checked by a computer 00:08:02.340 --> 00:08:04.730 align:start position:0% checked by a computer and<00:08:02.940> this<00:08:03.180> provides<00:08:03.660> higher<00:08:04.139> guarantee<00:08:04.500> that 00:08:04.730 --> 00:08:04.740 align:start position:0% and this provides higher guarantee that 00:08:04.740 --> 00:08:09.409 align:start position:0% and this provides higher guarantee that the<00:08:04.860> proofs<00:08:05.220> actually<00:08:05.460> correct 00:08:09.409 --> 00:08:09.419 align:start position:0% 00:08:09.419 --> 00:08:11.990 align:start position:0% okay<00:08:09.900> now<00:08:10.319> we<00:08:10.500> know<00:08:10.680> why<00:08:10.800> we<00:08:11.099> need<00:08:11.220> to<00:08:11.280> do<00:08:11.460> that 00:08:11.990 --> 00:08:12.000 align:start position:0% okay now we know why we need to do that 00:08:12.000 --> 00:08:14.930 align:start position:0% okay now we know why we need to do that and<00:08:12.479> now<00:08:13.259> we<00:08:13.440> can<00:08:13.680> have<00:08:14.099> a<00:08:14.220> look<00:08:14.340> how<00:08:14.580> the 00:08:14.930 --> 00:08:14.940 align:start position:0% and now we can have a look how the 00:08:14.940 --> 00:08:17.210 align:start position:0% and now we can have a look how the specification<00:08:15.419> actually<00:08:15.660> looks<00:08:16.380> like 00:08:17.210 --> 00:08:17.220 align:start position:0% specification actually looks like 00:08:17.220 --> 00:08:19.430 align:start position:0% specification actually looks like now<00:08:17.639> the<00:08:18.240> specification<00:08:18.780> is<00:08:19.020> not<00:08:19.139> a<00:08:19.319> piece 00:08:19.430 --> 00:08:19.440 align:start position:0% now the specification is not a piece 00:08:19.440 --> 00:08:21.589 align:start position:0% now the specification is not a piece it's<00:08:19.680> not<00:08:19.860> a<00:08:19.979> single<00:08:20.220> piece<00:08:20.400> it's<00:08:20.520> modular 00:08:21.589 --> 00:08:21.599 align:start position:0% it's not a single piece it's modular 00:08:21.599 --> 00:08:23.689 align:start position:0% it's not a single piece it's modular we<00:08:21.900> need<00:08:22.020> to<00:08:22.139> specify<00:08:22.500> the<00:08:23.039> different<00:08:23.400> things 00:08:23.689 --> 00:08:23.699 align:start position:0% we need to specify the different things 00:08:23.699 --> 00:08:26.210 align:start position:0% we need to specify the different things we<00:08:24.479> need<00:08:24.599> to<00:08:24.720> specify<00:08:25.080> how<00:08:25.319> the<00:08:25.620> single<00:08:25.979> node 00:08:26.210 --> 00:08:26.220 align:start position:0% we need to specify how the single node 00:08:26.220 --> 00:08:28.309 align:start position:0% we need to specify how the single node you<00:08:26.699> know<00:08:26.819> the<00:08:26.940> DVC<00:08:27.360> the<00:08:27.780> middle<00:08:27.900> layer 00:08:28.309 --> 00:08:28.319 align:start position:0% you know the DVC the middle layer 00:08:28.319 --> 00:08:29.450 align:start position:0% you know the DVC the middle layer behaves 00:08:29.450 --> 00:08:29.460 align:start position:0% behaves 00:08:29.460 --> 00:08:31.550 align:start position:0% behaves but<00:08:29.879> you<00:08:30.000> also<00:08:30.180> need<00:08:30.300> to<00:08:30.419> specify<00:08:30.840> how<00:08:31.440> the 00:08:31.550 --> 00:08:31.560 align:start position:0% but you also need to specify how the 00:08:31.560 --> 00:08:35.269 align:start position:0% but you also need to specify how the Byzantine<00:08:32.039> node<00:08:32.700> behaves<00:08:33.719> and<00:08:34.620> actually<00:08:35.039> what 00:08:35.269 --> 00:08:35.279 align:start position:0% Byzantine node behaves and actually what 00:08:35.279 --> 00:08:39.050 align:start position:0% Byzantine node behaves and actually what we<00:08:35.459> need<00:08:35.640> to<00:08:35.820> do<00:08:35.940> is<00:08:36.419> specify<00:08:37.039> what<00:08:38.039> it<00:08:38.640> cannot 00:08:39.050 --> 00:08:39.060 align:start position:0% we need to do is specify what it cannot 00:08:39.060 --> 00:08:41.449 align:start position:0% we need to do is specify what it cannot do<00:08:39.659> so<00:08:40.140> there<00:08:40.620> are<00:08:40.800> things<00:08:40.919> the<00:08:41.039> percent<00:08:41.219> I 00:08:41.449 --> 00:08:41.459 align:start position:0% do so there are things the percent I 00:08:41.459 --> 00:08:43.190 align:start position:0% do so there are things the percent I know<00:08:41.640> it<00:08:41.760> cannot<00:08:41.940> do<00:08:42.060> cannot<00:08:42.419> for<00:08:42.539> Signature 00:08:43.190 --> 00:08:43.200 align:start position:0% know it cannot do cannot for Signature 00:08:43.200 --> 00:08:44.810 align:start position:0% know it cannot do cannot for Signature also<00:08:43.740> it<00:08:43.860> cannot<00:08:44.039> change<00:08:44.219> the<00:08:44.399> state<00:08:44.640> of 00:08:44.810 --> 00:08:44.820 align:start position:0% also it cannot change the state of 00:08:44.820 --> 00:08:46.850 align:start position:0% also it cannot change the state of another<00:08:44.940> node<00:08:45.300> so<00:08:45.720> all<00:08:45.839> these<00:08:46.140> things<00:08:46.260> need<00:08:46.680> to 00:08:46.850 --> 00:08:46.860 align:start position:0% another node so all these things need to 00:08:46.860 --> 00:08:49.550 align:start position:0% another node so all these things need to be<00:08:46.980> coded<00:08:47.760> in<00:08:47.880> the<00:08:48.060> specification<00:08:49.019> we<00:08:49.380> also 00:08:49.550 --> 00:08:49.560 align:start position:0% be coded in the specification we also 00:08:49.560 --> 00:08:51.230 align:start position:0% be coded in the specification we also have<00:08:49.680> a<00:08:49.800> specification<00:08:50.279> for<00:08:50.580> the<00:08:50.760> consensus 00:08:51.230 --> 00:08:51.240 align:start position:0% have a specification for the consensus 00:08:51.240 --> 00:08:53.269 align:start position:0% have a specification for the consensus protocol<00:08:51.660> this<00:08:52.140> is<00:08:52.260> because<00:08:52.500> the<00:08:52.860> DVT 00:08:53.269 --> 00:08:53.279 align:start position:0% protocol this is because the DVT 00:08:53.279 --> 00:08:55.490 align:start position:0% protocol this is because the DVT protocol<00:08:53.580> is<00:08:53.880> agnostic<00:08:54.420> of<00:08:54.899> the<00:08:55.080> consensus 00:08:55.490 --> 00:08:55.500 align:start position:0% protocol is agnostic of the consensus 00:08:55.500 --> 00:08:57.650 align:start position:0% protocol is agnostic of the consensus protocol<00:08:55.920> used<00:08:56.220> and<00:08:56.880> so<00:08:57.000> what<00:08:57.180> we<00:08:57.300> need<00:08:57.420> to<00:08:57.540> do 00:08:57.650 --> 00:08:57.660 align:start position:0% protocol used and so what we need to do 00:08:57.660 --> 00:09:00.470 align:start position:0% protocol used and so what we need to do we<00:08:57.899> need<00:08:58.019> to<00:08:58.140> specify<00:08:58.620> the<00:08:59.040> behavior<00:08:59.880> that<00:09:00.360> we 00:09:00.470 --> 00:09:00.480 align:start position:0% we need to specify the behavior that we 00:09:00.480 --> 00:09:02.509 align:start position:0% we need to specify the behavior that we expect<00:09:00.600> from<00:09:00.959> the<00:09:01.140> consensus<00:09:01.620> protocol 00:09:02.509 --> 00:09:02.519 align:start position:0% expect from the consensus protocol 00:09:02.519 --> 00:09:04.430 align:start position:0% expect from the consensus protocol we<00:09:02.940> also<00:09:03.120> need<00:09:03.300> to<00:09:03.420> specify<00:09:03.779> how<00:09:04.080> the<00:09:04.260> network 00:09:04.430 --> 00:09:04.440 align:start position:0% we also need to specify how the network 00:09:04.440 --> 00:09:07.670 align:start position:0% we also need to specify how the network is<00:09:04.860> supposed<00:09:05.399> to<00:09:05.640> behave<00:09:05.940> for<00:09:06.720> example<00:09:06.959> which 00:09:07.670 --> 00:09:07.680 align:start position:0% is supposed to behave for example which 00:09:07.680 --> 00:09:10.190 align:start position:0% is supposed to behave for example which sequencing<00:09:08.160> of<00:09:08.399> messages<00:09:08.580> in<00:09:09.120> my<00:09:09.300> event<00:09:09.540> I'll 00:09:10.190 --> 00:09:10.200 align:start position:0% sequencing of messages in my event I'll 00:09:10.200 --> 00:09:13.009 align:start position:0% sequencing of messages in my event I'll go<00:09:10.320> over<00:09:10.440> on<00:09:11.220> this<00:09:11.399> one<00:09:11.580> in<00:09:12.360> more<00:09:12.540> detail<00:09:12.779> later 00:09:13.009 --> 00:09:13.019 align:start position:0% go over on this one in more detail later 00:09:13.019 --> 00:09:15.170 align:start position:0% go over on this one in more detail later and<00:09:13.620> all<00:09:13.740> of<00:09:13.920> this<00:09:14.100> is<00:09:14.279> put<00:09:14.580> together<00:09:14.760> is 00:09:15.170 --> 00:09:15.180 align:start position:0% and all of this is put together is 00:09:15.180 --> 00:09:16.970 align:start position:0% and all of this is put together is linked<00:09:15.540> together<00:09:15.660> in<00:09:16.320> the<00:09:16.500> distributed 00:09:16.970 --> 00:09:16.980 align:start position:0% linked together in the distributed 00:09:16.980 --> 00:09:20.389 align:start position:0% linked together in the distributed validator<00:09:17.339> specification 00:09:20.389 --> 00:09:20.399 align:start position:0% 00:09:20.399 --> 00:09:22.550 align:start position:0% what<00:09:20.940> we<00:09:21.120> have<00:09:21.240> actually<00:09:21.480> we<00:09:21.899> also<00:09:22.140> have<00:09:22.320> an 00:09:22.550 --> 00:09:22.560 align:start position:0% what we have actually we also have an 00:09:22.560 --> 00:09:26.030 align:start position:0% what we have actually we also have an actually<00:09:22.760> uh<00:09:24.019> executable<00:09:25.040> reference 00:09:26.030 --> 00:09:26.040 align:start position:0% actually uh executable reference 00:09:26.040 --> 00:09:28.310 align:start position:0% actually uh executable reference implementation<00:09:26.640> that<00:09:27.140> implements<00:09:28.140> the 00:09:28.310 --> 00:09:28.320 align:start position:0% implementation that implements the 00:09:28.320 --> 00:09:30.110 align:start position:0% implementation that implements the single<00:09:28.680> node<00:09:28.860> specification 00:09:30.110 --> 00:09:30.120 align:start position:0% single node specification 00:09:30.120 --> 00:09:32.269 align:start position:0% single node specification and<00:09:30.480> all<00:09:30.660> of<00:09:30.839> this<00:09:30.959> is<00:09:31.080> written<00:09:31.500> for<00:09:32.040> this 00:09:32.269 --> 00:09:32.279 align:start position:0% and all of this is written for this 00:09:32.279 --> 00:09:33.829 align:start position:0% and all of this is written for this project<00:09:32.399> in<00:09:32.760> Daphne 00:09:33.829 --> 00:09:33.839 align:start position:0% project in Daphne 00:09:33.839 --> 00:09:36.290 align:start position:0% project in Daphne which<00:09:34.440> is<00:09:34.560> a<00:09:34.740> programming<00:09:35.160> language 00:09:36.290 --> 00:09:36.300 align:start position:0% which is a programming language 00:09:36.300 --> 00:09:38.630 align:start position:0% which is a programming language um<00:09:36.360> it<00:09:36.959> says<00:09:37.140> a<00:09:37.320> python<00:09:37.680> JavaScript<00:09:38.100> like 00:09:38.630 --> 00:09:38.640 align:start position:0% um it says a python JavaScript like 00:09:38.640 --> 00:09:40.009 align:start position:0% um it says a python JavaScript like syntax 00:09:40.009 --> 00:09:40.019 align:start position:0% syntax 00:09:40.019 --> 00:09:42.530 align:start position:0% syntax and<00:09:40.560> it's<00:09:40.680> a<00:09:40.920> formally<00:09:41.220> verification<00:09:41.820> aware 00:09:42.530 --> 00:09:42.540 align:start position:0% and it's a formally verification aware 00:09:42.540 --> 00:09:46.250 align:start position:0% and it's a formally verification aware language<00:09:43.100> and<00:09:44.100> so<00:09:45.000> I'm<00:09:45.600> going<00:09:45.779> to<00:09:45.899> go<00:09:46.080> over 00:09:46.250 --> 00:09:46.260 align:start position:0% language and so I'm going to go over 00:09:46.260 --> 00:09:48.110 align:start position:0% language and so I'm going to go over with<00:09:46.680> the<00:09:46.920> spec<00:09:47.040> by<00:09:47.459> starting<00:09:47.640> from<00:09:47.940> the 00:09:48.110 --> 00:09:48.120 align:start position:0% with the spec by starting from the 00:09:48.120 --> 00:09:51.530 align:start position:0% with the spec by starting from the bottom<00:09:48.420> has<00:09:48.959> been<00:09:49.440> a<00:09:49.680> bit<00:09:49.860> say<00:09:50.279> vague<00:09:51.000> abstract 00:09:51.530 --> 00:09:51.540 align:start position:0% bottom has been a bit say vague abstract 00:09:51.540 --> 00:09:54.230 align:start position:0% bottom has been a bit say vague abstract I<00:09:52.080> want<00:09:52.200> to<00:09:52.320> give<00:09:52.440> you<00:09:52.620> some<00:09:53.339> practical<00:09:53.940> code 00:09:54.230 --> 00:09:54.240 align:start position:0% I want to give you some practical code 00:09:54.240 --> 00:09:56.930 align:start position:0% I want to give you some practical code to<00:09:54.660> look<00:09:54.779> at<00:09:55.040> so<00:09:56.040> I<00:09:56.220> start<00:09:56.399> from<00:09:56.640> the 00:09:56.930 --> 00:09:56.940 align:start position:0% to look at so I start from the 00:09:56.940 --> 00:09:59.570 align:start position:0% to look at so I start from the executable<00:09:57.600> reference<00:09:58.080> implementation<00:09:58.740> what 00:09:59.570 --> 00:09:59.580 align:start position:0% executable reference implementation what 00:09:59.580 --> 00:10:01.130 align:start position:0% executable reference implementation what I<00:09:59.760> want<00:09:59.880> to<00:10:00.000> show<00:10:00.120> here<00:10:00.300> this<00:10:00.540> is<00:10:00.660> the<00:10:00.839> method 00:10:01.130 --> 00:10:01.140 align:start position:0% I want to show here this is the method 00:10:01.140 --> 00:10:02.590 align:start position:0% I want to show here this is the method that<00:10:01.380> is<00:10:01.560> called 00:10:02.590 --> 00:10:02.600 align:start position:0% that is called 00:10:02.600 --> 00:10:06.050 align:start position:0% that is called when<00:10:03.600> the<00:10:03.839> consensus<00:10:04.380> protocol<00:10:04.860> decides<00:10:05.700> on<00:10:05.880> a 00:10:06.050 --> 00:10:06.060 align:start position:0% when the consensus protocol decides on a 00:10:06.060 --> 00:10:07.850 align:start position:0% when the consensus protocol decides on a new<00:10:06.180> attestation<00:10:06.660> what<00:10:07.140> I<00:10:07.320> want<00:10:07.440> to<00:10:07.500> show<00:10:07.620> here 00:10:07.850 --> 00:10:07.860 align:start position:0% new attestation what I want to show here 00:10:07.860 --> 00:10:09.889 align:start position:0% new attestation what I want to show here is<00:10:08.040> that 00:10:09.889 --> 00:10:09.899 align:start position:0% is that 00:10:09.899 --> 00:10:13.070 align:start position:0% is that um the<00:10:10.620> code<00:10:11.040> is<00:10:11.339> pretty<00:10:11.760> easy<00:10:12.060> I<00:10:12.600> would<00:10:12.899> say 00:10:13.070 --> 00:10:13.080 align:start position:0% um the code is pretty easy I would say 00:10:13.080 --> 00:10:15.889 align:start position:0% um the code is pretty easy I would say to<00:10:13.380> understand<00:10:13.560> it's<00:10:14.220> a<00:10:14.459> really<00:10:14.880> I<00:10:15.480> think<00:10:15.660> that 00:10:15.889 --> 00:10:15.899 align:start position:0% to understand it's a really I think that 00:10:15.899 --> 00:10:18.590 align:start position:0% to understand it's a really I think that any<00:10:16.200> developer<00:10:16.740> would<00:10:16.980> be<00:10:17.100> able<00:10:17.279> to<00:10:17.399> read<00:10:17.640> it 00:10:18.590 --> 00:10:18.600 align:start position:0% any developer would be able to read it 00:10:18.600 --> 00:10:20.870 align:start position:0% any developer would be able to read it um<00:10:18.660> it's<00:10:18.959> really<00:10:19.140> a<00:10:19.440> mix<00:10:19.560> of<00:10:19.860> JavaScript<00:10:20.580> and 00:10:20.870 --> 00:10:20.880 align:start position:0% um it's really a mix of JavaScript and 00:10:20.880 --> 00:10:23.150 align:start position:0% um it's really a mix of JavaScript and python<00:10:21.360> you<00:10:21.660> have<00:10:21.839> some<00:10:22.019> form<00:10:22.500> of<00:10:22.680> some 00:10:23.150 --> 00:10:23.160 align:start position:0% python you have some form of some 00:10:23.160 --> 00:10:25.610 align:start position:0% python you have some form of some statements<00:10:23.760> that<00:10:24.480> are<00:10:24.660> required<00:10:25.019> for<00:10:25.200> formal 00:10:25.610 --> 00:10:25.620 align:start position:0% statements that are required for formal 00:10:25.620 --> 00:10:27.769 align:start position:0% statements that are required for formal verification<00:10:26.160> those<00:10:26.880> are<00:10:27.060> the<00:10:27.180> top<00:10:27.360> if<00:10:27.600> you 00:10:27.769 --> 00:10:27.779 align:start position:0% verification those are the top if you 00:10:27.779 --> 00:10:30.350 align:start position:0% verification those are the top if you are<00:10:27.899> just<00:10:28.019> interested<00:10:28.500> in<00:10:28.680> say<00:10:29.279> look<00:10:30.060> in<00:10:30.240> the 00:10:30.350 --> 00:10:30.360 align:start position:0% are just interested in say look in the 00:10:30.360 --> 00:10:32.570 align:start position:0% are just interested in say look in the reference<00:10:30.720> implementation<00:10:31.320> and<00:10:31.680> having<00:10:32.040> your 00:10:32.570 --> 00:10:32.580 align:start position:0% reference implementation and having your 00:10:32.580 --> 00:10:34.370 align:start position:0% reference implementation and having your own<00:10:32.700> implementation<00:10:33.240> you<00:10:33.600> can<00:10:33.779> just<00:10:33.959> ignore 00:10:34.370 --> 00:10:34.380 align:start position:0% own implementation you can just ignore 00:10:34.380 --> 00:10:37.310 align:start position:0% own implementation you can just ignore them<00:10:34.560> there<00:10:35.100> are<00:10:35.279> also<00:10:35.459> some<00:10:35.700> specific<00:10:36.320> syntax 00:10:37.310 --> 00:10:37.320 align:start position:0% them there are also some specific syntax 00:10:37.320 --> 00:10:39.050 align:start position:0% them there are also some specific syntax like<00:10:37.680> this<00:10:37.920> one<00:10:38.040> at<00:10:38.220> the<00:10:38.339> bottom<00:10:38.580> which<00:10:38.880> is 00:10:39.050 --> 00:10:39.060 align:start position:0% like this one at the bottom which is 00:10:39.060 --> 00:10:41.389 align:start position:0% like this one at the bottom which is kind<00:10:39.660> of<00:10:39.779> the<00:10:39.899> equivalent<00:10:40.320> in<00:10:40.800> some<00:10:40.920> sense<00:10:41.160> of 00:10:41.389 --> 00:10:41.399 align:start position:0% kind of the equivalent in some sense of 00:10:41.399 --> 00:10:44.090 align:start position:0% kind of the equivalent in some sense of exception<00:10:42.000> propagation<00:10:42.540> in<00:10:42.839> in<00:10:43.380> some<00:10:43.740> of<00:10:43.920> the 00:10:44.090 --> 00:10:44.100 align:start position:0% exception propagation in in some of the 00:10:44.100 --> 00:10:45.829 align:start position:0% exception propagation in in some of the common<00:10:44.339> languages<00:10:44.760> but<00:10:45.000> aside<00:10:45.300> from<00:10:45.480> this<00:10:45.600> is 00:10:45.829 --> 00:10:45.839 align:start position:0% common languages but aside from this is 00:10:45.839 --> 00:10:47.329 align:start position:0% common languages but aside from this is pretty<00:10:46.260> simple<00:10:46.500> and<00:10:46.680> this<00:10:46.860> is<00:10:46.920> one<00:10:47.100> of<00:10:47.220> the 00:10:47.329 --> 00:10:47.339 align:start position:0% pretty simple and this is one of the 00:10:47.339 --> 00:10:49.670 align:start position:0% pretty simple and this is one of the reason<00:10:47.940> we<00:10:48.420> have<00:10:48.600> chosen<00:10:48.959> definitely<00:10:49.440> for 00:10:49.670 --> 00:10:49.680 align:start position:0% reason we have chosen definitely for 00:10:49.680 --> 00:10:51.110 align:start position:0% reason we have chosen definitely for this<00:10:49.860> project<00:10:50.040> to 00:10:51.110 --> 00:10:51.120 align:start position:0% this project to 00:10:51.120 --> 00:10:54.110 align:start position:0% this project to to<00:10:51.660> to<00:10:51.660> to<00:10:51.720> to<00:10:52.040> basically<00:10:53.040> make<00:10:53.279> it<00:10:53.459> easier<00:10:53.940> as 00:10:54.110 --> 00:10:54.120 align:start position:0% to to to to basically make it easier as 00:10:54.120 --> 00:10:56.090 align:start position:0% to to to to basically make it easier as easy<00:10:54.300> as<00:10:54.480> possible<00:10:54.839> to<00:10:55.200> for<00:10:55.500> the<00:10:55.680> developer 00:10:56.090 --> 00:10:56.100 align:start position:0% easy as possible to for the developer 00:10:56.100 --> 00:10:58.370 align:start position:0% easy as possible to for the developer development<00:10:56.760> Community<00:10:57.000> to<00:10:57.600> really<00:10:57.779> use<00:10:58.079> and 00:10:58.370 --> 00:10:58.380 align:start position:0% development Community to really use and 00:10:58.380 --> 00:11:01.610 align:start position:0% development Community to really use and this<00:10:58.800> product<00:10:58.980> protocol<00:11:00.360> but<00:11:00.779> now<00:11:00.839> let's<00:11:01.260> go 00:11:01.610 --> 00:11:01.620 align:start position:0% this product protocol but now let's go 00:11:01.620 --> 00:11:03.730 align:start position:0% this product protocol but now let's go up<00:11:01.800> how<00:11:02.339> does<00:11:02.519> the<00:11:02.760> actual<00:11:03.060> specification 00:11:03.730 --> 00:11:03.740 align:start position:0% up how does the actual specification 00:11:03.740 --> 00:11:06.170 align:start position:0% up how does the actual specification looks<00:11:04.740> like<00:11:04.860> so<00:11:05.339> what<00:11:05.519> the<00:11:05.700> specification 00:11:06.170 --> 00:11:06.180 align:start position:0% looks like so what the specification 00:11:06.180 --> 00:11:09.889 align:start position:0% looks like so what the specification does<00:11:06.540> really<00:11:07.040> defines<00:11:08.040> how<00:11:08.660> the<00:11:09.660> system 00:11:09.889 --> 00:11:09.899 align:start position:0% does really defines how the system 00:11:09.899 --> 00:11:13.190 align:start position:0% does really defines how the system transition<00:11:10.560> from<00:11:11.220> one<00:11:11.459> state<00:11:11.640> to<00:11:11.820> the<00:11:12.000> next 00:11:13.190 --> 00:11:13.200 align:start position:0% transition from one state to the next 00:11:13.200 --> 00:11:16.130 align:start position:0% transition from one state to the next and<00:11:13.860> the<00:11:14.160> system<00:11:14.279> State<00:11:14.640> includes<00:11:15.360> the<00:11:15.959> state 00:11:16.130 --> 00:11:16.140 align:start position:0% and the system State includes the state 00:11:16.140 --> 00:11:19.069 align:start position:0% and the system State includes the state of<00:11:16.380> all<00:11:16.560> the<00:11:16.800> various<00:11:17.100> nodes<00:11:17.480> uh<00:11:18.480> the<00:11:18.779> state<00:11:18.899> of 00:11:19.069 --> 00:11:19.079 align:start position:0% of all the various nodes uh the state of 00:11:19.079 --> 00:11:20.630 align:start position:0% of all the various nodes uh the state of the<00:11:19.200> network<00:11:19.320> the<00:11:19.740> state<00:11:19.920> of<00:11:20.040> the<00:11:20.160> adversary 00:11:20.630 --> 00:11:20.640 align:start position:0% the network the state of the adversary 00:11:20.640 --> 00:11:23.389 align:start position:0% the network the state of the adversary the<00:11:21.360> state<00:11:21.540> of<00:11:21.720> the<00:11:21.899> consensus<00:11:22.500> so<00:11:22.920> all<00:11:23.100> these 00:11:23.389 --> 00:11:23.399 align:start position:0% the state of the consensus so all these 00:11:23.399 --> 00:11:26.930 align:start position:0% the state of the consensus so all these things<00:11:23.519> is<00:11:23.779> encapsulated<00:11:24.779> in<00:11:25.620> the 00:11:26.930 --> 00:11:26.940 align:start position:0% things is encapsulated in the 00:11:26.940 --> 00:11:29.030 align:start position:0% things is encapsulated in the in<00:11:27.540> different<00:11:27.720> fields<00:11:28.140> so<00:11:28.260> let's<00:11:28.440> say<00:11:28.560> of<00:11:28.800> the 00:11:29.030 --> 00:11:29.040 align:start position:0% in different fields so let's say of the 00:11:29.040 --> 00:11:30.769 align:start position:0% in different fields so let's say of the system<00:11:29.399> state 00:11:30.769 --> 00:11:30.779 align:start position:0% system state 00:11:30.779 --> 00:11:34.130 align:start position:0% system state now<00:11:31.260> the<00:11:31.500> transition<00:11:31.920> says<00:11:32.459> well<00:11:32.700> on<00:11:33.540> a<00:11:33.779> given 00:11:34.130 --> 00:11:34.140 align:start position:0% now the transition says well on a given 00:11:34.140 --> 00:11:36.470 align:start position:0% now the transition says well on a given event<00:11:34.320> which<00:11:34.860> can<00:11:35.040> be<00:11:35.279> a<00:11:35.519> new<00:11:35.640> set<00:11:35.820> of<00:11:36.000> Duties 00:11:36.470 --> 00:11:36.480 align:start position:0% event which can be a new set of Duties 00:11:36.480 --> 00:11:39.530 align:start position:0% event which can be a new set of Duties time<00:11:37.320> to<00:11:37.500> execute<00:11:37.860> the<00:11:38.040> next<00:11:38.279> Duty<00:11:38.640> message<00:11:39.180> I 00:11:39.530 --> 00:11:39.540 align:start position:0% time to execute the next Duty message I 00:11:39.540 --> 00:11:41.150 align:start position:0% time to execute the next Duty message I received<00:11:39.839> you<00:11:40.200> move<00:11:40.320> from<00:11:40.500> one<00:11:40.680> state<00:11:40.860> to<00:11:41.040> the 00:11:41.150 --> 00:11:41.160 align:start position:0% received you move from one state to the 00:11:41.160 --> 00:11:42.829 align:start position:0% received you move from one state to the next<00:11:41.279> slide<00:11:41.640> from<00:11:41.940> the<00:11:42.060> yellow<00:11:42.180> state<00:11:42.480> to<00:11:42.720> the 00:11:42.829 --> 00:11:42.839 align:start position:0% next slide from the yellow state to the 00:11:42.839 --> 00:11:44.750 align:start position:0% next slide from the yellow state to the Green<00:11:43.019> State 00:11:44.750 --> 00:11:44.760 align:start position:0% Green State 00:11:44.760 --> 00:11:47.269 align:start position:0% Green State one<00:11:45.240> very<00:11:45.480> important<00:11:45.899> characteristic<00:11:46.800> of<00:11:47.040> the 00:11:47.269 --> 00:11:47.279 align:start position:0% one very important characteristic of the 00:11:47.279 --> 00:11:49.910 align:start position:0% one very important characteristic of the way<00:11:47.459> this<00:11:48.120> specification<00:11:48.660> is<00:11:48.959> written<00:11:49.680> which 00:11:49.910 --> 00:11:49.920 align:start position:0% way this specification is written which 00:11:49.920 --> 00:11:53.810 align:start position:0% way this specification is written which is<00:11:50.600> commonly<00:11:51.600> also<00:11:51.899> to<00:11:52.019> our<00:11:52.200> Kelly<00:11:52.440> plus<00:11:52.860> way 00:11:53.810 --> 00:11:53.820 align:start position:0% is commonly also to our Kelly plus way 00:11:53.820 --> 00:11:56.449 align:start position:0% is commonly also to our Kelly plus way of<00:11:54.000> writing<00:11:54.480> specification<00:11:55.019> in<00:11:55.200> TNA<00:11:55.620> plus<00:11:55.800> we 00:11:56.449 --> 00:11:56.459 align:start position:0% of writing specification in TNA plus we 00:11:56.459 --> 00:11:58.190 align:start position:0% of writing specification in TNA plus we allow<00:11:56.760> non-deterministic<00:11:57.660> Behavior<00:11:58.019> now 00:11:58.190 --> 00:11:58.200 align:start position:0% allow non-deterministic Behavior now 00:11:58.200 --> 00:12:00.350 align:start position:0% allow non-deterministic Behavior now what<00:11:58.860> you<00:11:58.980> have<00:11:59.160> on<00:11:59.339> the<00:11:59.519> and<00:11:59.760> explain<00:12:00.060> why 00:12:00.350 --> 00:12:00.360 align:start position:0% what you have on the and explain why 00:12:00.360 --> 00:12:02.329 align:start position:0% what you have on the and explain why this<00:12:00.600> is<00:12:00.779> important<00:12:01.140> what<00:12:01.620> you<00:12:01.920> have<00:12:02.040> on<00:12:02.220> the 00:12:02.329 --> 00:12:02.339 align:start position:0% this is important what you have on the 00:12:02.339 --> 00:12:03.590 align:start position:0% this is important what you have on the left<00:12:02.579> hand<00:12:02.700> side<00:12:02.940> is<00:12:03.240> not<00:12:03.420> really 00:12:03.590 --> 00:12:03.600 align:start position:0% left hand side is not really 00:12:03.600 --> 00:12:06.410 align:start position:0% left hand side is not really non-deterministic<00:12:04.560> but<00:12:04.740> close<00:12:05.040> to<00:12:05.339> it<00:12:05.519> so 00:12:06.410 --> 00:12:06.420 align:start position:0% non-deterministic but close to it so 00:12:06.420 --> 00:12:09.310 align:start position:0% non-deterministic but close to it so what<00:12:06.660> can<00:12:06.839> happen<00:12:06.959> is<00:12:07.260> that<00:12:08.160> from<00:12:08.820> one<00:12:09.060> state 00:12:09.310 --> 00:12:09.320 align:start position:0% what can happen is that from one state 00:12:09.320 --> 00:12:12.290 align:start position:0% what can happen is that from one state you<00:12:10.320> might<00:12:10.500> have<00:12:10.680> more<00:12:11.040> than<00:12:11.160> one<00:12:11.339> event<00:12:11.519> that 00:12:12.290 --> 00:12:12.300 align:start position:0% you might have more than one event that 00:12:12.300 --> 00:12:14.090 align:start position:0% you might have more than one event that can<00:12:12.480> move<00:12:12.660> you<00:12:12.839> to<00:12:13.019> two<00:12:13.260> different<00:12:13.440> states<00:12:13.740> so 00:12:14.090 --> 00:12:14.100 align:start position:0% can move you to two different states so 00:12:14.100 --> 00:12:16.610 align:start position:0% can move you to two different states so so<00:12:14.579> for<00:12:14.820> example<00:12:15.120> a<00:12:15.300> node<00:12:15.540> might<00:12:15.779> receive<00:12:16.079> a 00:12:16.610 --> 00:12:16.620 align:start position:0% so for example a node might receive a 00:12:16.620 --> 00:12:19.310 align:start position:0% so for example a node might receive a message<00:12:16.800> from<00:12:17.640> node<00:12:17.940> 2<00:12:18.180> or<00:12:18.600> perhaps<00:12:18.959> on<00:12:19.079> Note 00:12:19.310 --> 00:12:19.320 align:start position:0% message from node 2 or perhaps on Note 00:12:19.320 --> 00:12:21.949 align:start position:0% message from node 2 or perhaps on Note 3.<00:12:19.920> and<00:12:20.399> this<00:12:20.519> this<00:12:20.940> is<00:12:21.120> what<00:12:21.360> allows<00:12:21.720> to 00:12:21.949 --> 00:12:21.959 align:start position:0% 3. and this this is what allows to 00:12:21.959 --> 00:12:24.590 align:start position:0% 3. and this this is what allows to capture 00:12:24.590 --> 00:12:24.600 align:start position:0% 00:12:24.600 --> 00:12:28.310 align:start position:0% okay<00:12:25.040> Network<00:12:26.060> asynchrony<00:12:27.060> so<00:12:27.660> and<00:12:28.079> this<00:12:28.260> is 00:12:28.310 --> 00:12:28.320 align:start position:0% okay Network asynchrony so and this is 00:12:28.320 --> 00:12:29.990 align:start position:0% okay Network asynchrony so and this is one<00:12:28.500> of<00:12:28.680> the<00:12:28.740> important<00:12:29.100> differences<00:12:29.579> to 00:12:29.990 --> 00:12:30.000 align:start position:0% one of the important differences to 00:12:30.000 --> 00:12:33.530 align:start position:0% one of the important differences to testing<00:12:30.480> we<00:12:31.320> can<00:12:31.500> really<00:12:31.680> reason<00:12:32.300> on<00:12:33.300> any 00:12:33.530 --> 00:12:33.540 align:start position:0% testing we can really reason on any 00:12:33.540 --> 00:12:36.230 align:start position:0% testing we can really reason on any possible<00:12:34.079> sequences<00:12:34.800> of<00:12:35.100> messages<00:12:35.279> any<00:12:36.000> that 00:12:36.230 --> 00:12:36.240 align:start position:0% possible sequences of messages any that 00:12:36.240 --> 00:12:40.190 align:start position:0% possible sequences of messages any that you<00:12:36.420> can<00:12:36.540> imagine<00:12:36.660> this<00:12:37.440> is<00:12:37.560> coded<00:12:37.980> in 00:12:40.190 --> 00:12:40.200 align:start position:0% 00:12:40.200 --> 00:12:42.410 align:start position:0% the<00:12:40.800> other 00:12:42.410 --> 00:12:42.420 align:start position:0% the other 00:12:42.420 --> 00:12:45.410 align:start position:0% the other point<00:12:43.079> I<00:12:43.440> want<00:12:43.620> to<00:12:43.740> make<00:12:43.860> is<00:12:44.279> really<00:12:44.940> about<00:12:45.240> the 00:12:45.410 --> 00:12:45.420 align:start position:0% point I want to make is really about the 00:12:45.420 --> 00:12:47.150 align:start position:0% point I want to make is really about the non-deterministic<00:12:46.260> behavior<00:12:46.620> so<00:12:46.800> from<00:12:46.980> one 00:12:47.150 --> 00:12:47.160 align:start position:0% non-deterministic behavior so from one 00:12:47.160 --> 00:12:50.090 align:start position:0% non-deterministic behavior so from one state<00:12:47.399> the<00:12:48.180> same<00:12:48.420> event<00:12:48.600> can<00:12:49.380> get<00:12:49.560> you<00:12:49.740> to<00:12:49.920> two 00:12:50.090 --> 00:12:50.100 align:start position:0% state the same event can get you to two 00:12:50.100 --> 00:12:53.030 align:start position:0% state the same event can get you to two different<00:12:50.279> states<00:12:51.120> and<00:12:51.600> now<00:12:51.839> why<00:12:52.680> this<00:12:52.860> can 00:12:53.030 --> 00:12:53.040 align:start position:0% different states and now why this can 00:12:53.040 --> 00:12:55.550 align:start position:0% different states and now why this can happen<00:12:53.300> mainly<00:12:54.300> because<00:12:54.480> of<00:12:54.720> that<00:12:54.899> adversary 00:12:55.550 --> 00:12:55.560 align:start position:0% happen mainly because of that adversary 00:12:55.560 --> 00:12:57.769 align:start position:0% happen mainly because of that adversary so<00:12:56.040> if<00:12:56.279> you<00:12:56.399> have<00:12:56.519> a<00:12:56.639> given<00:12:56.940> state 00:12:57.769 --> 00:12:57.779 align:start position:0% so if you have a given state 00:12:57.779 --> 00:12:59.750 align:start position:0% so if you have a given state the<00:12:58.139> adversity<00:12:58.680> can<00:12:58.920> behave<00:12:59.220> in<00:12:59.399> multiple 00:12:59.750 --> 00:12:59.760 align:start position:0% the adversity can behave in multiple 00:12:59.760 --> 00:13:02.569 align:start position:0% the adversity can behave in multiple ways<00:13:00.120> on<00:13:00.600> an<00:13:00.779> event<00:13:00.959> and<00:13:01.500> this<00:13:01.680> is<00:13:01.800> a<00:13:02.100> what 00:13:02.569 --> 00:13:02.579 align:start position:0% ways on an event and this is a what 00:13:02.579 --> 00:13:05.629 align:start position:0% ways on an event and this is a what allows<00:13:03.120> us<00:13:03.240> to<00:13:03.540> capture<00:13:03.959> this 00:13:05.629 --> 00:13:05.639 align:start position:0% allows us to capture this 00:13:05.639 --> 00:13:07.550 align:start position:0% allows us to capture this while<00:13:06.180> I<00:13:06.420> speak<00:13:06.660> about<00:13:06.839> this<00:13:07.019> I<00:13:07.200> want<00:13:07.320> to<00:13:07.440> draw 00:13:07.550 --> 00:13:07.560 align:start position:0% while I speak about this I want to draw 00:13:07.560 --> 00:13:10.310 align:start position:0% while I speak about this I want to draw a<00:13:07.740> comparison<00:13:08.160> to<00:13:08.339> model<00:13:09.060> checking<00:13:09.600> which<00:13:09.899> is 00:13:10.310 --> 00:13:10.320 align:start position:0% a comparison to model checking which is 00:13:10.320 --> 00:13:12.290 align:start position:0% a comparison to model checking which is a<00:13:10.500> different<00:13:10.620> technique<00:13:11.100> and<00:13:11.579> with<00:13:12.060> model 00:13:12.290 --> 00:13:12.300 align:start position:0% a different technique and with model 00:13:12.300 --> 00:13:13.730 align:start position:0% a different technique and with model checking<00:13:12.779> you<00:13:12.959> have<00:13:13.079> the<00:13:13.200> problem<00:13:13.320> of<00:13:13.500> State 00:13:13.730 --> 00:13:13.740 align:start position:0% checking you have the problem of State 00:13:13.740 --> 00:13:16.370 align:start position:0% checking you have the problem of State explosion<00:13:14.220> and<00:13:14.399> it's<00:13:15.060> very<00:13:15.300> it<00:13:15.600> will<00:13:16.079> take 00:13:16.370 --> 00:13:16.380 align:start position:0% explosion and it's very it will take 00:13:16.380 --> 00:13:18.650 align:start position:0% explosion and it's very it will take it's<00:13:16.740> very<00:13:16.980> hard<00:13:17.279> for<00:13:17.820> model<00:13:18.000> Checker<00:13:18.480> to 00:13:18.650 --> 00:13:18.660 align:start position:0% it's very hard for model Checker to 00:13:18.660 --> 00:13:19.550 align:start position:0% it's very hard for model Checker to really 00:13:19.550 --> 00:13:19.560 align:start position:0% really 00:13:19.560 --> 00:13:21.110 align:start position:0% really being<00:13:20.040> able<00:13:20.279> to<00:13:20.459> check<00:13:20.579> a<00:13:20.820> property 00:13:21.110 --> 00:13:21.120 align:start position:0% being able to check a property 00:13:21.120 --> 00:13:22.670 align:start position:0% being able to check a property considering<00:13:21.600> Byzantine<00:13:22.139> Behavior<00:13:22.560> because 00:13:22.670 --> 00:13:22.680 align:start position:0% considering Byzantine Behavior because 00:13:22.680 --> 00:13:25.250 align:start position:0% considering Byzantine Behavior because it<00:13:22.860> will<00:13:22.980> take<00:13:23.220> a<00:13:23.579> lot<00:13:23.700> of<00:13:23.820> time<00:13:24.000> and<00:13:24.360> with 00:13:25.250 --> 00:13:25.260 align:start position:0% it will take a lot of time and with 00:13:25.260 --> 00:13:27.110 align:start position:0% it will take a lot of time and with formal<00:13:25.860> verification<00:13:26.279> takes<00:13:26.639> a<00:13:26.760> lot<00:13:26.880> of<00:13:26.940> time 00:13:27.110 --> 00:13:27.120 align:start position:0% formal verification takes a lot of time 00:13:27.120 --> 00:13:28.610 align:start position:0% formal verification takes a lot of time to<00:13:27.300> put<00:13:27.420> together<00:13:27.540> the<00:13:27.779> proof<00:13:28.139> but<00:13:28.260> once<00:13:28.500> the 00:13:28.610 --> 00:13:28.620 align:start position:0% to put together the proof but once the 00:13:28.620 --> 00:13:30.290 align:start position:0% to put together the proof but once the proof<00:13:28.800> is<00:13:28.920> put<00:13:29.100> together<00:13:29.220> it's<00:13:29.820> quite<00:13:30.000> quick 00:13:30.290 --> 00:13:30.300 align:start position:0% proof is put together it's quite quick 00:13:30.300 --> 00:13:33.590 align:start position:0% proof is put together it's quite quick to<00:13:30.779> be<00:13:30.959> run<00:13:31.320> through 00:13:33.590 --> 00:13:33.600 align:start position:0% 00:13:33.600 --> 00:13:35.990 align:start position:0% now<00:13:34.079> looking<00:13:34.320> I<00:13:34.620> want<00:13:34.800> to<00:13:34.980> show<00:13:35.279> a<00:13:35.459> bit<00:13:35.579> code 00:13:35.990 --> 00:13:36.000 align:start position:0% now looking I want to show a bit code 00:13:36.000 --> 00:13:37.970 align:start position:0% now looking I want to show a bit code again<00:13:36.300> how<00:13:37.200> actually<00:13:37.380> the<00:13:37.620> formal 00:13:37.970 --> 00:13:37.980 align:start position:0% again how actually the formal 00:13:37.980 --> 00:13:41.269 align:start position:0% again how actually the formal specification<00:13:38.519> is<00:13:39.019> Brittany<00:13:40.019> Daphne 00:13:41.269 --> 00:13:41.279 align:start position:0% specification is Brittany Daphne 00:13:41.279 --> 00:13:45.050 align:start position:0% specification is Brittany Daphne um<00:13:41.339> let's<00:13:41.820> let's<00:13:42.120> focus<00:13:42.660> on<00:13:42.899> the<00:13:43.139> top<00:13:43.920> top<00:13:44.399> of 00:13:45.050 --> 00:13:45.060 align:start position:0% um let's let's focus on the top top of 00:13:45.060 --> 00:13:47.449 align:start position:0% um let's let's focus on the top top of the<00:13:45.180> slide<00:13:45.480> so<00:13:46.260> let's<00:13:46.440> assume<00:13:46.860> you<00:13:46.980> have<00:13:47.160> this 00:13:47.449 --> 00:13:47.459 align:start position:0% the slide so let's assume you have this 00:13:47.459 --> 00:13:49.970 align:start position:0% the slide so let's assume you have this transition<00:13:48.120> from<00:13:48.660> the<00:13:48.959> yellow<00:13:49.260> state<00:13:49.560> to<00:13:49.800> the 00:13:49.970 --> 00:13:49.980 align:start position:0% transition from the yellow state to the 00:13:49.980 --> 00:13:52.730 align:start position:0% transition from the yellow state to the green<00:13:50.100> and<00:13:50.459> purple<00:13:50.700> State<00:13:51.139> when<00:13:52.139> the<00:13:52.500> gray 00:13:52.730 --> 00:13:52.740 align:start position:0% green and purple State when the gray 00:13:52.740 --> 00:13:56.509 align:start position:0% green and purple State when the gray event<00:13:53.040> is<00:13:53.399> received<00:13:54.360> the<00:13:54.959> way<00:13:55.139> we<00:13:55.440> code<00:13:55.740> it<00:13:55.980> we 00:13:56.509 --> 00:13:56.519 align:start position:0% event is received the way we code it we 00:13:56.519 --> 00:13:58.430 align:start position:0% event is received the way we code it we essentially<00:13:56.880> have<00:13:57.060> a<00:13:57.240> function<00:13:57.540> that<00:13:58.019> takes<00:13:58.200> a 00:13:58.430 --> 00:13:58.440 align:start position:0% essentially have a function that takes a 00:13:58.440 --> 00:14:00.710 align:start position:0% essentially have a function that takes a source<00:13:58.740> date<00:13:58.920> an<00:13:59.399> event<00:13:59.579> and<00:14:00.180> the<00:14:00.360> destination 00:14:00.710 --> 00:14:00.720 align:start position:0% source date an event and the destination 00:14:00.720 --> 00:14:03.530 align:start position:0% source date an event and the destination State<00:14:01.079> and<00:14:01.800> returns<00:14:02.279> a<00:14:02.399> Boolean 00:14:03.530 --> 00:14:03.540 align:start position:0% State and returns a Boolean 00:14:03.540 --> 00:14:05.930 align:start position:0% State and returns a Boolean now<00:14:04.200> the<00:14:04.680> way<00:14:04.800> that<00:14:04.980> the<00:14:05.220> transition<00:14:05.639> is 00:14:05.930 --> 00:14:05.940 align:start position:0% now the way that the transition is 00:14:05.940 --> 00:14:08.870 align:start position:0% now the way that the transition is encoded<00:14:06.480> is<00:14:07.260> that<00:14:07.500> the<00:14:07.920> function<00:14:08.220> if<00:14:08.760> the 00:14:08.870 --> 00:14:08.880 align:start position:0% encoded is that the function if the 00:14:08.880 --> 00:14:12.110 align:start position:0% encoded is that the function if the function<00:14:09.120> returns<00:14:09.660> true<00:14:09.899> on<00:14:10.620> a<00:14:11.220> given<00:14:11.760> Source 00:14:12.110 --> 00:14:12.120 align:start position:0% function returns true on a given Source 00:14:12.120 --> 00:14:13.850 align:start position:0% function returns true on a given Source event<00:14:12.300> and<00:14:12.660> destination<00:14:13.019> state<00:14:13.320> it<00:14:13.680> means 00:14:13.850 --> 00:14:13.860 align:start position:0% event and destination state it means 00:14:13.860 --> 00:14:15.650 align:start position:0% event and destination state it means that<00:14:14.040> the<00:14:14.220> system<00:14:14.399> can<00:14:15.000> transition<00:14:15.360> from 00:14:15.650 --> 00:14:15.660 align:start position:0% that the system can transition from 00:14:15.660 --> 00:14:19.610 align:start position:0% that the system can transition from source<00:14:16.260> to<00:14:16.440> destination<00:14:17.000> given<00:14:18.000> the<00:14:18.240> event<00:14:18.899> if 00:14:19.610 --> 00:14:19.620 align:start position:0% source to destination given the event if 00:14:19.620 --> 00:14:21.230 align:start position:0% source to destination given the event if it<00:14:19.740> returns<00:14:20.100> Force<00:14:20.459> there<00:14:20.700> is<00:14:20.880> no<00:14:21.060> such 00:14:21.230 --> 00:14:21.240 align:start position:0% it returns Force there is no such 00:14:21.240 --> 00:14:22.910 align:start position:0% it returns Force there is no such transition<00:14:21.720> so<00:14:21.959> in<00:14:22.139> this<00:14:22.320> example<00:14:22.620> for 00:14:22.910 --> 00:14:22.920 align:start position:0% transition so in this example for 00:14:22.920 --> 00:14:27.650 align:start position:0% transition so in this example for example<00:14:23.240> is<00:14:24.240> true<00:14:24.480> for<00:14:24.720> a<00:14:25.500> yellow<00:14:25.920> gray<00:14:26.660> green 00:14:27.650 --> 00:14:27.660 align:start position:0% example is true for a yellow gray green 00:14:27.660 --> 00:14:30.590 align:start position:0% example is true for a yellow gray green and<00:14:28.380> purple<00:14:28.620> but<00:14:29.220> not<00:14:29.459> false<00:14:29.940> for<00:14:30.180> any<00:14:30.360> other 00:14:30.590 --> 00:14:30.600 align:start position:0% and purple but not false for any other 00:14:30.600 --> 00:14:32.150 align:start position:0% and purple but not false for any other combination 00:14:32.150 --> 00:14:32.160 align:start position:0% combination 00:14:32.160 --> 00:14:34.069 align:start position:0% combination and<00:14:32.700> this<00:14:32.880> is<00:14:32.940> you<00:14:33.180> can<00:14:33.300> see<00:14:33.420> at<00:14:33.600> the<00:14:33.720> bottom<00:14:33.899> is 00:14:34.069 --> 00:14:34.079 align:start position:0% and this is you can see at the bottom is 00:14:34.079 --> 00:14:36.530 align:start position:0% and this is you can see at the bottom is coded<00:14:34.500> in<00:14:34.700> this<00:14:35.700> is<00:14:35.760> how<00:14:35.880> it's<00:14:36.060> coded<00:14:36.420> in 00:14:36.530 --> 00:14:36.540 align:start position:0% coded in this is how it's coded in 00:14:36.540 --> 00:14:38.269 align:start position:0% coded in this is how it's coded in definitely<00:14:37.079> now<00:14:37.260> this<00:14:37.560> is<00:14:37.620> essentially<00:14:38.160> a 00:14:38.269 --> 00:14:38.279 align:start position:0% definitely now this is essentially a 00:14:38.279 --> 00:14:40.370 align:start position:0% definitely now this is essentially a simplification<00:14:39.000> of<00:14:39.240> this 00:14:40.370 --> 00:14:40.380 align:start position:0% simplification of this 00:14:40.380 --> 00:14:43.850 align:start position:0% simplification of this um but<00:14:41.040> it's<00:14:41.940> it's<00:14:42.180> a<00:14:42.779> um<00:14:42.779> this<00:14:43.199> is<00:14:43.320> expressed 00:14:43.850 --> 00:14:43.860 align:start position:0% um but it's it's a um this is expressed 00:14:43.860 --> 00:14:46.310 align:start position:0% um but it's it's a um this is expressed using<00:14:44.699> first<00:14:44.880> order<00:14:45.120> logic<00:14:45.600> you<00:14:45.779> know<00:14:45.899> this<00:14:46.199> is 00:14:46.310 --> 00:14:46.320 align:start position:0% using first order logic you know this is 00:14:46.320 --> 00:14:49.189 align:start position:0% using first order logic you know this is something<00:14:46.820> we<00:14:47.820> don't<00:14:47.940> see<00:14:48.120> often<00:14:48.420> in<00:14:48.779> standard 00:14:49.189 --> 00:14:49.199 align:start position:0% something we don't see often in standard 00:14:49.199 --> 00:14:51.590 align:start position:0% something we don't see often in standard uh<00:14:49.560> programming<00:14:50.100> languages<00:14:50.399> but 00:14:51.590 --> 00:14:51.600 align:start position:0% uh programming languages but 00:14:51.600 --> 00:14:54.250 align:start position:0% uh programming languages but it's not<00:14:52.139> much<00:14:52.560> of<00:14:52.800> a<00:14:52.920> stretch<00:14:53.279> to<00:14:53.399> say 00:14:54.250 --> 00:14:54.260 align:start position:0% it's not much of a stretch to say 00:14:54.260 --> 00:14:56.509 align:start position:0% it's not much of a stretch to say what<00:14:55.260> you<00:14:55.380> can<00:14:55.500> see<00:14:55.680> here 00:14:56.509 --> 00:14:56.519 align:start position:0% what you can see here 00:14:56.519 --> 00:14:59.870 align:start position:0% what you can see here this<00:14:57.120> is<00:14:57.300> essentially<00:14:57.660> an<00:14:58.440> end<00:14:58.680> of<00:14:59.399> different 00:14:59.870 --> 00:14:59.880 align:start position:0% this is essentially an end of different 00:14:59.880 --> 00:15:02.569 align:start position:0% this is essentially an end of different state<00:15:00.240> transition<00:15:00.720> and<00:15:01.079> here<00:15:01.800> we<00:15:02.040> have<00:15:02.220> the 00:15:02.569 --> 00:15:02.579 align:start position:0% state transition and here we have the 00:15:02.579 --> 00:15:05.930 align:start position:0% state transition and here we have the state<00:15:03.480> transition<00:15:03.899> for<00:15:04.260> the<00:15:04.500> honest<00:15:04.920> node<00:15:05.220> and 00:15:05.930 --> 00:15:05.940 align:start position:0% state transition for the honest node and 00:15:05.940 --> 00:15:08.090 align:start position:0% state transition for the honest node and you<00:15:06.120> can<00:15:06.240> see<00:15:06.360> here<00:15:06.660> we<00:15:07.019> say<00:15:07.320> basically<00:15:07.740> this 00:15:08.090 --> 00:15:08.100 align:start position:0% you can see here we say basically this 00:15:08.100 --> 00:15:10.069 align:start position:0% you can see here we say basically this much<00:15:08.279> true<00:15:08.519> for<00:15:08.760> hollowness<00:15:09.300> nodes<00:15:09.600> that's 00:15:10.069 --> 00:15:10.079 align:start position:0% much true for hollowness nodes that's 00:15:10.079 --> 00:15:11.569 align:start position:0% much true for hollowness nodes that's what<00:15:10.260> the<00:15:10.380> photo<00:15:10.620> does 00:15:11.569 --> 00:15:11.579 align:start position:0% what the photo does 00:15:11.579 --> 00:15:14.329 align:start position:0% what the photo does and<00:15:12.060> then<00:15:12.240> we<00:15:12.360> put<00:15:12.600> this<00:15:12.779> in<00:15:13.019> a<00:15:13.139> coin<00:15:13.500> end<00:15:13.740> with 00:15:14.329 --> 00:15:14.339 align:start position:0% and then we put this in a coin end with 00:15:14.339 --> 00:15:15.590 align:start position:0% and then we put this in a coin end with the<00:15:14.399> state<00:15:14.639> transition<00:15:15.060> for<00:15:15.360> Network 00:15:15.590 --> 00:15:15.600 align:start position:0% the state transition for Network 00:15:15.600 --> 00:15:18.290 align:start position:0% the state transition for Network adversary<00:15:16.560> and<00:15:17.040> consensus 00:15:18.290 --> 00:15:18.300 align:start position:0% adversary and consensus 00:15:18.300 --> 00:15:20.990 align:start position:0% adversary and consensus you<00:15:18.660> know<00:15:18.779> what<00:15:18.959> you<00:15:19.199> can<00:15:19.320> see<00:15:19.500> here<00:15:19.920> is<00:15:20.760> this 00:15:20.990 --> 00:15:21.000 align:start position:0% you know what you can see here is this 00:15:21.000 --> 00:15:23.569 align:start position:0% you know what you can see here is this exists<00:15:21.660> is<00:15:22.260> what<00:15:22.500> gives<00:15:23.220> us<00:15:23.339> the 00:15:23.569 --> 00:15:23.579 align:start position:0% exists is what gives us the 00:15:23.579 --> 00:15:25.550 align:start position:0% exists is what gives us the non-determinism<00:15:24.300> because<00:15:24.540> we're<00:15:24.779> saying 00:15:25.550 --> 00:15:25.560 align:start position:0% non-determinism because we're saying 00:15:25.560 --> 00:15:28.069 align:start position:0% non-determinism because we're saying this<00:15:25.920> function<00:15:26.279> returns<00:15:27.060> true<00:15:27.240> as<00:15:27.660> long<00:15:27.899> as 00:15:28.069 --> 00:15:28.079 align:start position:0% this function returns true as long as 00:15:28.079 --> 00:15:31.129 align:start position:0% this function returns true as long as there<00:15:28.980> exists<00:15:29.399> a<00:15:29.760> set<00:15:30.180> of<00:15:30.360> messages<00:15:30.540> received 00:15:31.129 --> 00:15:31.139 align:start position:0% there exists a set of messages received 00:15:31.139 --> 00:15:33.590 align:start position:0% there exists a set of messages received messages<00:15:31.500> sent<00:15:31.980> and<00:15:32.459> decided<00:15:32.880> value<00:15:33.120> says 00:15:33.590 --> 00:15:33.600 align:start position:0% messages sent and decided value says 00:15:33.600 --> 00:15:36.170 align:start position:0% messages sent and decided value says that<00:15:33.779> they<00:15:34.560> satisfy<00:15:35.220> all<00:15:35.760> the<00:15:35.880> various 00:15:36.170 --> 00:15:36.180 align:start position:0% that they satisfy all the various 00:15:36.180 --> 00:15:38.569 align:start position:0% that they satisfy all the various constraints<00:15:36.779> and<00:15:37.260> the<00:15:37.800> end<00:15:37.920> expression<00:15:38.399> at 00:15:38.569 --> 00:15:38.579 align:start position:0% constraints and the end expression at 00:15:38.579 --> 00:15:41.329 align:start position:0% constraints and the end expression at the<00:15:38.699> bottom 00:15:41.329 --> 00:15:41.339 align:start position:0% 00:15:41.339 --> 00:15:43.430 align:start position:0% now<00:15:41.760> before<00:15:42.180> going<00:15:42.660> into<00:15:42.839> what<00:15:43.079> we<00:15:43.260> actually 00:15:43.430 --> 00:15:43.440 align:start position:0% now before going into what we actually 00:15:43.440 --> 00:15:45.170 align:start position:0% now before going into what we actually achieved<00:15:43.920> I<00:15:44.220> need<00:15:44.459> to<00:15:44.579> make<00:15:44.699> sort<00:15:45.000> of 00:15:45.170 --> 00:15:45.180 align:start position:0% achieved I need to make sort of 00:15:45.180 --> 00:15:46.970 align:start position:0% achieved I need to make sort of disclosure<00:15:45.720> uh 00:15:46.970 --> 00:15:46.980 align:start position:0% disclosure uh 00:15:46.980 --> 00:15:50.150 align:start position:0% disclosure uh that<00:15:47.519> are<00:15:47.699> part<00:15:47.940> of<00:15:48.120> this<00:15:48.720> say<00:15:49.199> system<00:15:49.620> that 00:15:50.150 --> 00:15:50.160 align:start position:0% that are part of this say system that 00:15:50.160 --> 00:15:52.790 align:start position:0% that are part of this say system that needs<00:15:50.399> to<00:15:50.459> be<00:15:50.579> trusted<00:15:51.420> so<00:15:51.839> these<00:15:52.199> are<00:15:52.320> the 00:15:52.790 --> 00:15:52.800 align:start position:0% needs to be trusted so these are the 00:15:52.800 --> 00:15:56.030 align:start position:0% needs to be trusted so these are the parts<00:15:52.920> that<00:15:53.220> need<00:15:53.339> to<00:15:53.459> be<00:15:53.519> trusted<00:15:54.360> and<00:15:55.500> um<00:15:55.500> and 00:15:56.030 --> 00:15:56.040 align:start position:0% parts that need to be trusted and um and 00:15:56.040 --> 00:15:57.710 align:start position:0% parts that need to be trusted and um and these<00:15:56.160> are<00:15:56.279> the<00:15:56.399> parts<00:15:56.579> that<00:15:56.880> actually<00:15:57.060> we 00:15:57.710 --> 00:15:57.720 align:start position:0% these are the parts that actually we 00:15:57.720 --> 00:15:59.689 align:start position:0% these are the parts that actually we don't<00:15:57.839> trust<00:15:58.079> now<00:15:58.380> if<00:15:58.980> you<00:15:59.040> look<00:15:59.160> at<00:15:59.279> this<00:15:59.399> it 00:15:59.689 --> 00:15:59.699 align:start position:0% don't trust now if you look at this it 00:15:59.699 --> 00:16:02.030 align:start position:0% don't trust now if you look at this it seems<00:16:00.000> the<00:16:00.180> area<00:16:00.360> it's<00:16:01.019> quite<00:16:01.199> of<00:16:01.440> the<00:16:01.560> trusted 00:16:02.030 --> 00:16:02.040 align:start position:0% seems the area it's quite of the trusted 00:16:02.040 --> 00:16:04.670 align:start position:0% seems the area it's quite of the trusted and<00:16:02.220> non-trusted<00:16:02.880> but<00:16:03.180> you<00:16:03.899> know<00:16:03.959> the<00:16:04.380> error 00:16:04.670 --> 00:16:04.680 align:start position:0% and non-trusted but you know the error 00:16:04.680 --> 00:16:06.290 align:start position:0% and non-trusted but you know the error doesn't<00:16:04.800> really<00:16:05.040> represent<00:16:05.459> the<00:16:05.699> value<00:16:06.060> of 00:16:06.290 --> 00:16:06.300 align:start position:0% doesn't really represent the value of 00:16:06.300 --> 00:16:08.689 align:start position:0% doesn't really represent the value of complexity<00:16:06.779> also<00:16:07.500> it's<00:16:08.040> not<00:16:08.220> really<00:16:08.399> a 00:16:08.689 --> 00:16:08.699 align:start position:0% complexity also it's not really a 00:16:08.699 --> 00:16:11.389 align:start position:0% complexity also it's not really a problem<00:16:08.820> of<00:16:09.240> formal<00:16:10.019> verification<00:16:10.560> it's<00:16:10.920> a 00:16:11.389 --> 00:16:11.399 align:start position:0% problem of formal verification it's a 00:16:11.399 --> 00:16:14.150 align:start position:0% problem of formal verification it's a sort<00:16:11.519> of<00:16:11.639> existential<00:16:12.420> problem<00:16:12.660> you 00:16:14.150 --> 00:16:14.160 align:start position:0% sort of existential problem you 00:16:14.160 --> 00:16:16.850 align:start position:0% sort of existential problem you you<00:16:14.760> need<00:16:14.940> to<00:16:15.060> assume<00:16:15.540> how<00:16:16.079> the<00:16:16.380> adversary 00:16:16.850 --> 00:16:16.860 align:start position:0% you need to assume how the adversary 00:16:16.860 --> 00:16:18.829 align:start position:0% you need to assume how the adversary will<00:16:17.160> behave<00:16:17.459> in<00:16:17.639> your<00:16:17.820> system<00:16:18.060> even<00:16:18.540> if<00:16:18.720> you 00:16:18.829 --> 00:16:18.839 align:start position:0% will behave in your system even if you 00:16:18.839 --> 00:16:20.689 align:start position:0% will behave in your system even if you just<00:16:18.959> buy<00:16:19.139> software<00:16:19.560> you<00:16:19.800> do<00:16:19.920> you<00:16:20.100> write<00:16:20.279> tests 00:16:20.689 --> 00:16:20.699 align:start position:0% just buy software you do you write tests 00:16:20.699 --> 00:16:22.610 align:start position:0% just buy software you do you write tests whatever<00:16:20.880> you<00:16:21.180> do<00:16:21.300> you<00:16:21.779> need<00:16:21.959> to<00:16:22.019> assume<00:16:22.320> that 00:16:22.610 --> 00:16:22.620 align:start position:0% whatever you do you need to assume that 00:16:22.620 --> 00:16:25.250 align:start position:0% whatever you do you need to assume that you<00:16:22.920> have<00:16:23.220> a<00:16:23.459> consensus<00:16:24.420> that<00:16:24.720> or<00:16:24.839> a<00:16:25.079> library 00:16:25.250 --> 00:16:25.260 align:start position:0% you have a consensus that or a library 00:16:25.260 --> 00:16:26.870 align:start position:0% you have a consensus that or a library that<00:16:25.620> works<00:16:25.920> correctly<00:16:26.279> you<00:16:26.459> have<00:16:26.639> a<00:16:26.760> network 00:16:26.870 --> 00:16:26.880 align:start position:0% that works correctly you have a network 00:16:26.880 --> 00:16:29.930 align:start position:0% that works correctly you have a network you<00:16:27.180> assume<00:16:27.480> how<00:16:27.540> the<00:16:27.720> network<00:16:27.899> will<00:16:28.560> behave 00:16:29.930 --> 00:16:29.940 align:start position:0% you assume how the network will behave 00:16:29.940 --> 00:16:31.910 align:start position:0% you assume how the network will behave um<00:16:30.000> saying<00:16:30.720> things<00:16:30.839> for<00:16:31.019> properties<00:16:31.500> you 00:16:31.910 --> 00:16:31.920 align:start position:0% um saying things for properties you 00:16:31.920 --> 00:16:33.769 align:start position:0% um saying things for properties you assume<00:16:32.339> that<00:16:32.519> you<00:16:33.000> have<00:16:33.120> a<00:16:33.240> set<00:16:33.300> of<00:16:33.420> properties 00:16:33.769 --> 00:16:33.779 align:start position:0% assume that you have a set of properties 00:16:33.779 --> 00:16:35.629 align:start position:0% assume that you have a set of properties that<00:16:34.019> are<00:16:34.199> those<00:16:34.380> that<00:16:34.740> you<00:16:34.920> are<00:16:35.399> really 00:16:35.629 --> 00:16:35.639 align:start position:0% that are those that you are really 00:16:35.639 --> 00:16:36.889 align:start position:0% that are those that you are really interested<00:16:36.060> into 00:16:36.889 --> 00:16:36.899 align:start position:0% interested into 00:16:36.899 --> 00:16:38.509 align:start position:0% interested into so 00:16:38.509 --> 00:16:38.519 align:start position:0% so 00:16:38.519 --> 00:16:42.050 align:start position:0% so this<00:16:39.300> it's<00:16:39.720> it's<00:16:39.720> just<00:16:40.259> something<00:16:40.620> that<00:16:40.980> yes<00:16:41.639> a 00:16:42.050 --> 00:16:42.060 align:start position:0% this it's it's just something that yes a 00:16:42.060 --> 00:16:44.210 align:start position:0% this it's it's just something that yes a formal<00:16:42.660> verification<00:16:43.139> doesn't<00:16:43.620> doesn't 00:16:44.210 --> 00:16:44.220 align:start position:0% formal verification doesn't doesn't 00:16:44.220 --> 00:16:46.550 align:start position:0% formal verification doesn't doesn't solve<00:16:44.699> but<00:16:44.820> it<00:16:45.000> solves<00:16:45.360> a<00:16:45.600> good<00:16:46.079> chunk<00:16:46.320> of 00:16:46.550 --> 00:16:46.560 align:start position:0% solve but it solves a good chunk of 00:16:46.560 --> 00:16:49.430 align:start position:0% solve but it solves a good chunk of problems<00:16:47.100> in<00:16:47.339> ensuring<00:16:48.120> that<00:16:48.300> well<00:16:48.540> your 00:16:49.430 --> 00:16:49.440 align:start position:0% problems in ensuring that well your 00:16:49.440 --> 00:16:51.769 align:start position:0% problems in ensuring that well your single<00:16:49.860> node<00:16:50.100> as<00:16:50.519> it<00:16:50.699> is<00:16:50.820> specified<00:16:51.180> will<00:16:51.540> does 00:16:51.769 --> 00:16:51.779 align:start position:0% single node as it is specified will does 00:16:51.779 --> 00:16:53.870 align:start position:0% single node as it is specified will does we<00:16:52.079> guarantee<00:16:52.440> those<00:16:52.740> properties 00:16:53.870 --> 00:16:53.880 align:start position:0% we guarantee those properties 00:16:53.880 --> 00:16:57.590 align:start position:0% we guarantee those properties also<00:16:54.540> there<00:16:55.259> are<00:16:55.380> things<00:16:55.620> one<00:16:56.279> can<00:16:56.519> do<00:16:56.699> to 00:16:57.590 --> 00:16:57.600 align:start position:0% also there are things one can do to 00:16:57.600 --> 00:16:59.749 align:start position:0% also there are things one can do to increase<00:16:58.079> the<00:16:58.380> chances<00:16:58.740> that<00:16:59.100> the<00:16:59.279> trusted 00:16:59.749 --> 00:16:59.759 align:start position:0% increase the chances that the trusted 00:16:59.759 --> 00:17:01.310 align:start position:0% increase the chances that the trusted path<00:17:00.000> is<00:17:00.300> correct 00:17:01.310 --> 00:17:01.320 align:start position:0% path is correct 00:17:01.320 --> 00:17:04.429 align:start position:0% path is correct one<00:17:01.740> is<00:17:01.920> to<00:17:02.100> keep<00:17:02.399> the<00:17:02.880> trusted<00:17:03.600> specification 00:17:04.429 --> 00:17:04.439 align:start position:0% one is to keep the trusted specification 00:17:04.439 --> 00:17:06.289 align:start position:0% one is to keep the trusted specification as<00:17:04.860> simple<00:17:05.100> as<00:17:05.339> possible 00:17:06.289 --> 00:17:06.299 align:start position:0% as simple as possible 00:17:06.299 --> 00:17:08.630 align:start position:0% as simple as possible one<00:17:06.839> is<00:17:07.020> to<00:17:07.199> have<00:17:07.439> a<00:17:07.620> peer<00:17:07.919> review 00:17:08.630 --> 00:17:08.640 align:start position:0% one is to have a peer review 00:17:08.640 --> 00:17:12.890 align:start position:0% one is to have a peer review uh<00:17:09.480> also<00:17:10.020> for<00:17:10.860> the<00:17:11.160> tool<00:17:11.939> it's<00:17:12.299> important<00:17:12.660> to 00:17:12.890 --> 00:17:12.900 align:start position:0% uh also for the tool it's important to 00:17:12.900 --> 00:17:15.049 align:start position:0% uh also for the tool it's important to use<00:17:13.079> formal<00:17:13.679> verification<00:17:14.100> tools<00:17:14.699> that<00:17:14.819> have 00:17:15.049 --> 00:17:15.059 align:start position:0% use formal verification tools that have 00:17:15.059 --> 00:17:17.870 align:start position:0% use formal verification tools that have good<00:17:15.540> support<00:17:15.780> we<00:17:16.500> use<00:17:16.740> Daphne<00:17:17.100> Daphne<00:17:17.760> is 00:17:17.870 --> 00:17:17.880 align:start position:0% good support we use Daphne Daphne is 00:17:17.880 --> 00:17:22.189 align:start position:0% good support we use Daphne Daphne is very<00:17:18.120> active<00:17:18.660> bugs<00:17:19.620> get<00:17:20.160> fixed<00:17:20.579> very<00:17:20.819> quickly 00:17:22.189 --> 00:17:22.199 align:start position:0% very active bugs get fixed very quickly 00:17:22.199 --> 00:17:23.449 align:start position:0% very active bugs get fixed very quickly also 00:17:23.449 --> 00:17:23.459 align:start position:0% also 00:17:23.459 --> 00:17:24.710 align:start position:0% also uh 00:17:24.710 --> 00:17:24.720 align:start position:0% uh 00:17:24.720 --> 00:17:26.990 align:start position:0% uh in<00:17:25.500> distribute<00:17:25.980> the<00:17:26.100> system<00:17:26.220> usually<00:17:26.699> you 00:17:26.990 --> 00:17:27.000 align:start position:0% in distribute the system usually you 00:17:27.000 --> 00:17:29.090 align:start position:0% in distribute the system usually you have<00:17:27.120> two<00:17:27.299> types<00:17:27.660> of<00:17:27.720> properties<00:17:28.140> safety 00:17:29.090 --> 00:17:29.100 align:start position:0% have two types of properties safety 00:17:29.100 --> 00:17:31.610 align:start position:0% have two types of properties safety properties<00:17:29.460> which<00:17:30.000> say<00:17:30.299> something<00:17:31.020> bad<00:17:31.320> will 00:17:31.610 --> 00:17:31.620 align:start position:0% properties which say something bad will 00:17:31.620 --> 00:17:34.250 align:start position:0% properties which say something bad will never<00:17:31.799> happen<00:17:32.040> and<00:17:33.000> you<00:17:33.600> have<00:17:33.720> liveness 00:17:34.250 --> 00:17:34.260 align:start position:0% never happen and you have liveness 00:17:34.260 --> 00:17:36.110 align:start position:0% never happen and you have liveness property<00:17:34.620> where<00:17:34.919> they<00:17:35.100> say<00:17:35.280> something<00:17:35.820> good 00:17:36.110 --> 00:17:36.120 align:start position:0% property where they say something good 00:17:36.120 --> 00:17:38.570 align:start position:0% property where they say something good will<00:17:36.419> eventually<00:17:36.720> happen<00:17:37.020> now<00:17:37.799> being<00:17:38.100> if<00:17:38.520> you 00:17:38.570 --> 00:17:38.580 align:start position:0% will eventually happen now being if you 00:17:38.580 --> 00:17:40.610 align:start position:0% will eventually happen now being if you formally<00:17:38.880> prove<00:17:39.240> that<00:17:39.419> a<00:17:39.720> specification 00:17:40.610 --> 00:17:40.620 align:start position:0% formally prove that a specification 00:17:40.620 --> 00:17:42.650 align:start position:0% formally prove that a specification guarantees<00:17:41.460> both<00:17:41.580> it's<00:17:41.880> very 00:17:42.650 --> 00:17:42.660 align:start position:0% guarantees both it's very 00:17:42.660 --> 00:17:44.690 align:start position:0% guarantees both it's very it<00:17:43.320> it<00:17:43.500> really<00:17:43.679> increases<00:17:44.100> the<00:17:44.220> chances<00:17:44.520> that 00:17:44.690 --> 00:17:44.700 align:start position:0% it it really increases the chances that 00:17:44.700 --> 00:17:46.310 align:start position:0% it it really increases the chances that the<00:17:44.820> trusted<00:17:45.240> part<00:17:45.419> is<00:17:45.600> correct<00:17:45.840> it's<00:17:46.020> quite 00:17:46.310 --> 00:17:46.320 align:start position:0% the trusted part is correct it's quite 00:17:46.320 --> 00:17:48.230 align:start position:0% the trusted part is correct it's quite hard<00:17:46.500> to<00:17:46.679> put<00:17:46.860> together<00:17:46.980> a<00:17:47.760> specification 00:17:48.230 --> 00:17:48.240 align:start position:0% hard to put together a specification 00:17:48.240 --> 00:17:50.330 align:start position:0% hard to put together a specification guarantees<00:17:48.840> both<00:17:49.080> both<00:17:49.140> properties<00:17:49.799> it<00:17:50.220> is 00:17:50.330 --> 00:17:50.340 align:start position:0% guarantees both both properties it is 00:17:50.340 --> 00:17:52.190 align:start position:0% guarantees both both properties it is incorrect 00:17:52.190 --> 00:17:52.200 align:start position:0% incorrect 00:17:52.200 --> 00:17:54.289 align:start position:0% incorrect so<00:17:52.559> now<00:17:52.679> we<00:17:52.799> can<00:17:52.980> go<00:17:53.100> over<00:17:53.280> what<00:17:53.940> you<00:17:54.120> actually 00:17:54.289 --> 00:17:54.299 align:start position:0% so now we can go over what you actually 00:17:54.299 --> 00:18:00.950 align:start position:0% so now we can go over what you actually achieved<00:17:54.900> so<00:17:55.080> far<00:17:55.320> and<00:17:55.799> what<00:17:56.280> is<00:17:56.400> left<00:17:56.580> to<00:17:56.820> do 00:18:00.950 --> 00:18:00.960 align:start position:0% 00:18:00.960 --> 00:18:02.029 align:start position:0% so 00:18:02.029 --> 00:18:02.039 align:start position:0% so 00:18:02.039 --> 00:18:03.710 align:start position:0% so on<00:18:02.400> the<00:18:02.520> right<00:18:02.640> hand<00:18:02.880> side<00:18:03.059> you<00:18:03.360> have<00:18:03.480> what 00:18:03.710 --> 00:18:03.720 align:start position:0% on the right hand side you have what 00:18:03.720 --> 00:18:04.909 align:start position:0% on the right hand side you have what we've<00:18:03.840> been<00:18:03.960> able<00:18:04.140> to<00:18:04.260> prove<00:18:04.500> on<00:18:04.679> the<00:18:04.799> left 00:18:04.909 --> 00:18:04.919 align:start position:0% we've been able to prove on the left 00:18:04.919 --> 00:18:06.830 align:start position:0% we've been able to prove on the left hand<00:18:05.100> side<00:18:05.220> you<00:18:05.400> have<00:18:05.520> the<00:18:05.640> assumption 00:18:06.830 --> 00:18:06.840 align:start position:0% hand side you have the assumption 00:18:06.840 --> 00:18:10.029 align:start position:0% hand side you have the assumption to<00:18:07.140> have<00:18:07.320> been<00:18:07.380> able<00:18:07.559> to<00:18:07.679> prove<00:18:08.220> is<00:18:08.760> that 00:18:10.029 --> 00:18:10.039 align:start position:0% to have been able to prove is that 00:18:10.039 --> 00:18:13.070 align:start position:0% to have been able to prove is that slashable<00:18:11.039> attestation<00:18:11.640> signed<00:18:12.600> by<00:18:12.780> the 00:18:13.070 --> 00:18:13.080 align:start position:0% slashable attestation signed by the 00:18:13.080 --> 00:18:15.470 align:start position:0% slashable attestation signed by the distributable<00:18:14.039> data<00:18:14.460> signing<00:18:14.820> key<00:18:15.000> the<00:18:15.360> one 00:18:15.470 --> 00:18:15.480 align:start position:0% distributable data signing key the one 00:18:15.480 --> 00:18:16.970 align:start position:0% distributable data signing key the one that<00:18:15.660> is<00:18:15.840> shared 00:18:16.970 --> 00:18:16.980 align:start position:0% that is shared 00:18:16.980 --> 00:18:19.750 align:start position:0% that is shared they<00:18:17.520> can<00:18:17.700> never<00:18:17.820> be<00:18:18.059> created<00:18:18.419> in<00:18:19.140> other<00:18:19.260> words 00:18:19.750 --> 00:18:19.760 align:start position:0% they can never be created in other words 00:18:19.760 --> 00:18:22.370 align:start position:0% they can never be created in other words the<00:18:20.760> account<00:18:20.940> associated<00:18:21.660> with<00:18:22.140> the 00:18:22.370 --> 00:18:22.380 align:start position:0% the account associated with the 00:18:22.380 --> 00:18:24.230 align:start position:0% the account associated with the distributed<00:18:23.100> validator<00:18:23.460> signing<00:18:23.880> key<00:18:24.000> can 00:18:24.230 --> 00:18:24.240 align:start position:0% distributed validator signing key can 00:18:24.240 --> 00:18:26.150 align:start position:0% distributed validator signing key can never<00:18:24.360> get<00:18:24.600> slashed<00:18:25.020> because<00:18:25.260> of<00:18:25.500> attestation 00:18:26.150 --> 00:18:26.160 align:start position:0% never get slashed because of attestation 00:18:26.160 --> 00:18:28.130 align:start position:0% never get slashed because of attestation signing 00:18:28.130 --> 00:18:28.140 align:start position:0% signing 00:18:28.140 --> 00:18:29.510 align:start position:0% signing and<00:18:28.500> this<00:18:28.620> is<00:18:28.740> done<00:18:28.919> under<00:18:29.220> the<00:18:29.460> the 00:18:29.510 --> 00:18:29.520 align:start position:0% and this is done under the the 00:18:29.520 --> 00:18:32.510 align:start position:0% and this is done under the the assumptions<00:18:30.120> you<00:18:30.780> see<00:18:30.960> on<00:18:31.500> the<00:18:31.740> left<00:18:32.340> hand 00:18:32.510 --> 00:18:32.520 align:start position:0% assumptions you see on the left hand 00:18:32.520 --> 00:18:33.470 align:start position:0% assumptions you see on the left hand side 00:18:33.470 --> 00:18:33.480 align:start position:0% side 00:18:33.480 --> 00:18:36.289 align:start position:0% side and<00:18:33.900> assumption<00:18:34.380> is<00:18:34.559> as<00:18:34.860> again<00:18:35.039> we<00:18:35.400> have<00:18:35.580> any 00:18:36.289 --> 00:18:36.299 align:start position:0% and assumption is as again we have any 00:18:36.299 --> 00:18:39.830 align:start position:0% and assumption is as again we have any we<00:18:36.600> allow<00:18:36.960> for<00:18:37.140> any<00:18:37.740> message<00:18:38.580> delay<00:18:39.179> we<00:18:39.539> don't 00:18:39.830 --> 00:18:39.840 align:start position:0% we allow for any message delay we don't 00:18:39.840 --> 00:18:42.409 align:start position:0% we allow for any message delay we don't constrain<00:18:40.260> this<00:18:40.559> at<00:18:40.799> all<00:18:40.919> we<00:18:41.700> had<00:18:42.000> allow 00:18:42.409 --> 00:18:42.419 align:start position:0% constrain this at all we had allow 00:18:42.419 --> 00:18:44.330 align:start position:0% constrain this at all we had allow messages<00:18:42.840> to<00:18:43.260> be<00:18:43.380> lost 00:18:44.330 --> 00:18:44.340 align:start position:0% messages to be lost 00:18:44.340 --> 00:18:46.370 align:start position:0% messages to be lost we<00:18:44.940> also<00:18:45.179> allow 00:18:46.370 --> 00:18:46.380 align:start position:0% we also allow 00:18:46.380 --> 00:18:48.110 align:start position:0% we also allow the<00:18:46.799> biker<00:18:47.220> nodes 00:18:48.110 --> 00:18:48.120 align:start position:0% the biker nodes 00:18:48.120 --> 00:18:50.810 align:start position:0% the biker nodes okay<00:18:48.720> typical<00:18:49.500> notes<00:18:50.039> here<00:18:50.220> to<00:18:50.520> be<00:18:50.640> actually 00:18:50.810 --> 00:18:50.820 align:start position:0% okay typical notes here to be actually 00:18:50.820 --> 00:18:52.789 align:start position:0% okay typical notes here to be actually out<00:18:51.059> of<00:18:51.240> sync<00:18:51.600> for<00:18:51.840> this<00:18:52.020> proof<00:18:52.380> we<00:18:52.620> don't 00:18:52.789 --> 00:18:52.799 align:start position:0% out of sync for this proof we don't 00:18:52.799 --> 00:18:54.950 align:start position:0% out of sync for this proof we don't require<00:18:53.100> them<00:18:53.400> to<00:18:53.580> be<00:18:53.700> in<00:18:53.820> sync<00:18:54.179> they<00:18:54.600> could<00:18:54.840> be 00:18:54.950 --> 00:18:54.960 align:start position:0% require them to be in sync they could be 00:18:54.960 --> 00:18:57.230 align:start position:0% require them to be in sync they could be serving<00:18:55.440> completely<00:18:56.280> different<00:18:56.460> duties<00:18:57.000> and 00:18:57.230 --> 00:18:57.240 align:start position:0% serving completely different duties and 00:18:57.240 --> 00:18:59.510 align:start position:0% serving completely different duties and they<00:18:57.419> prove<00:18:57.720> still<00:18:57.960> old<00:18:58.200> and<00:18:59.100> then<00:18:59.220> we<00:18:59.400> have 00:18:59.510 --> 00:18:59.520 align:start position:0% they prove still old and then we have 00:18:59.520 --> 00:19:02.570 align:start position:0% they prove still old and then we have some<00:18:59.820> assumption<00:19:00.360> on<00:19:01.080> the<00:19:01.799> um<00:19:01.860> number<00:19:02.400> of 00:19:02.570 --> 00:19:02.580 align:start position:0% some assumption on the um number of 00:19:02.580 --> 00:19:05.330 align:start position:0% some assumption on the um number of nodes<00:19:02.820> that<00:19:03.179> can<00:19:03.360> that<00:19:03.960> are<00:19:04.320> either<00:19:04.620> Byzantine 00:19:05.330 --> 00:19:05.340 align:start position:0% nodes that can that are either Byzantine 00:19:05.340 --> 00:19:07.490 align:start position:0% nodes that can that are either Byzantine or<00:19:05.580> with<00:19:05.880> a<00:19:06.120> compromise<00:19:06.480> key<00:19:06.780> to<00:19:06.960> be<00:19:07.080> less<00:19:07.320> than 00:19:07.490 --> 00:19:07.500 align:start position:0% or with a compromise key to be less than 00:19:07.500 --> 00:19:09.710 align:start position:0% or with a compromise key to be less than one<00:19:07.740> thought<00:19:08.039> and<00:19:08.340> this<00:19:08.460> is 00:19:09.710 --> 00:19:09.720 align:start position:0% one thought and this is 00:19:09.720 --> 00:19:11.630 align:start position:0% one thought and this is um<00:19:09.780> theoretical<00:19:10.500> bound<00:19:10.740> on<00:19:11.039> consensus 00:19:11.630 --> 00:19:11.640 align:start position:0% um theoretical bound on consensus 00:19:11.640 --> 00:19:13.850 align:start position:0% um theoretical bound on consensus protocols<00:19:12.240> as<00:19:12.360> well<00:19:12.539> we<00:19:13.320> assume<00:19:13.679> that 00:19:13.850 --> 00:19:13.860 align:start position:0% protocols as well we assume that 00:19:13.860 --> 00:19:16.130 align:start position:0% protocols as well we assume that signatures<00:19:14.580> cannot<00:19:14.880> be<00:19:15.000> forged<00:19:15.480> and<00:19:15.840> they<00:19:15.960> are 00:19:16.130 --> 00:19:16.140 align:start position:0% signatures cannot be forged and they are 00:19:16.140 --> 00:19:18.169 align:start position:0% signatures cannot be forged and they are unique<00:19:16.440> and<00:19:17.039> also<00:19:17.340> that<00:19:17.520> you<00:19:17.640> have<00:19:17.820> a<00:19:18.000> sound 00:19:18.169 --> 00:19:18.179 align:start position:0% unique and also that you have a sound 00:19:18.179 --> 00:19:20.110 align:start position:0% unique and also that you have a sound two<00:19:18.720> third 00:19:20.110 --> 00:19:20.120 align:start position:0% two third 00:19:20.120 --> 00:19:22.430 align:start position:0% two third signature<00:19:21.120> scheme<00:19:21.480> and<00:19:21.660> then<00:19:21.840> these 00:19:22.430 --> 00:19:22.440 align:start position:0% signature scheme and then these 00:19:22.440 --> 00:19:23.690 align:start position:0% signature scheme and then these assumptions 00:19:23.690 --> 00:19:23.700 align:start position:0% assumptions 00:19:23.700 --> 00:19:26.270 align:start position:0% assumptions we've<00:19:24.299> been<00:19:24.480> able<00:19:24.780> to<00:19:24.900> prove<00:19:25.140> the<00:19:25.320> property 00:19:26.270 --> 00:19:26.280 align:start position:0% we've been able to prove the property 00:19:26.280 --> 00:19:28.730 align:start position:0% we've been able to prove the property we've<00:19:26.580> also<00:19:26.880> been<00:19:27.000> able<00:19:27.179> to<00:19:27.299> prove<00:19:27.660> that 00:19:28.730 --> 00:19:28.740 align:start position:0% we've also been able to prove that 00:19:28.740 --> 00:19:30.890 align:start position:0% we've also been able to prove that the<00:19:29.100> reference<00:19:29.400> implementation<00:19:30.059> adhes<00:19:30.660> to 00:19:30.890 --> 00:19:30.900 align:start position:0% the reference implementation adhes to 00:19:30.900 --> 00:19:32.570 align:start position:0% the reference implementation adhes to the<00:19:31.140> specification 00:19:32.570 --> 00:19:32.580 align:start position:0% the specification 00:19:32.580 --> 00:19:34.850 align:start position:0% the specification now<00:19:33.000> what<00:19:33.240> this<00:19:33.299> means<00:19:33.600> is<00:19:33.780> that<00:19:34.020> it<00:19:34.380> is<00:19:34.440> that 00:19:34.850 --> 00:19:34.860 align:start position:0% now what this means is that it is that 00:19:34.860 --> 00:19:38.150 align:start position:0% now what this means is that it is that if<00:19:34.980> you<00:19:35.100> deploy<00:19:35.400> a<00:19:35.580> system<00:19:35.900> uh<00:19:36.900> running<00:19:37.620> the 00:19:38.150 --> 00:19:38.160 align:start position:0% if you deploy a system uh running the 00:19:38.160 --> 00:19:40.669 align:start position:0% if you deploy a system uh running the reference<00:19:38.820> implementation<00:19:39.480> of<00:19:39.780> the<00:19:40.080> of<00:19:40.380> the 00:19:40.669 --> 00:19:40.679 align:start position:0% reference implementation of the of the 00:19:40.679 --> 00:19:42.890 align:start position:0% reference implementation of the of the distributable<00:19:41.280> data<00:19:41.640> client<00:19:41.940> node<00:19:42.240> what<00:19:42.780> you 00:19:42.890 --> 00:19:42.900 align:start position:0% distributable data client node what you 00:19:42.900 --> 00:19:46.330 align:start position:0% distributable data client node what you get<00:19:43.080> is<00:19:43.380> a<00:19:43.620> system<00:19:43.799> that<00:19:44.640> ensures<00:19:45.539> the 00:19:46.330 --> 00:19:46.340 align:start position:0% get is a system that ensures the 00:19:46.340 --> 00:19:50.210 align:start position:0% get is a system that ensures the non-slashable<00:19:47.340> attestation 00:19:50.210 --> 00:19:50.220 align:start position:0% 00:19:50.220 --> 00:19:52.010 align:start position:0% and 00:19:52.010 --> 00:19:52.020 align:start position:0% and 00:19:52.020 --> 00:19:53.690 align:start position:0% and so<00:19:52.620> looking 00:19:53.690 --> 00:19:53.700 align:start position:0% so looking 00:19:53.700 --> 00:19:55.909 align:start position:0% so looking that<00:19:54.179> what<00:19:54.419> is<00:19:54.600> left<00:19:54.780> to<00:19:54.960> do<00:19:55.080> so<00:19:55.559> we<00:19:55.740> put 00:19:55.909 --> 00:19:55.919 align:start position:0% that what is left to do so we put 00:19:55.919 --> 00:19:57.409 align:start position:0% that what is left to do so we put together<00:19:56.039> this<00:19:56.400> proof<00:19:56.760> we<00:19:57.120> have<00:19:57.240> the 00:19:57.409 --> 00:19:57.419 align:start position:0% together this proof we have the 00:19:57.419 --> 00:19:59.210 align:start position:0% together this proof we have the specification<00:19:58.020> we<00:19:58.620> have<00:19:58.740> the<00:19:58.860> reference 00:19:59.210 --> 00:19:59.220 align:start position:0% specification we have the reference 00:19:59.220 --> 00:20:00.710 align:start position:0% specification we have the reference implementation 00:20:00.710 --> 00:20:00.720 align:start position:0% implementation 00:20:00.720 --> 00:20:03.529 align:start position:0% implementation and<00:20:01.200> it's<00:20:01.380> all<00:20:01.559> open<00:20:01.799> sourced<00:20:02.340> on<00:20:02.520> the<00:20:02.760> on<00:20:03.299> the 00:20:03.529 --> 00:20:03.539 align:start position:0% and it's all open sourced on the on the 00:20:03.539 --> 00:20:06.890 align:start position:0% and it's all open sourced on the on the GitHub<00:20:04.320> repo<00:20:04.740> that<00:20:04.919> you<00:20:05.100> can<00:20:05.220> see<00:20:05.460> here<00:20:06.059> what 00:20:06.890 --> 00:20:06.900 align:start position:0% GitHub repo that you can see here what 00:20:06.900 --> 00:20:09.590 align:start position:0% GitHub repo that you can see here what is<00:20:07.020> left<00:20:07.200> to<00:20:07.440> do<00:20:07.559> is<00:20:08.280> to<00:20:08.460> extend<00:20:08.820> the 00:20:09.590 --> 00:20:09.600 align:start position:0% is left to do is to extend the 00:20:09.600 --> 00:20:11.090 align:start position:0% is left to do is to extend the specification<00:20:10.200> and<00:20:10.679> the<00:20:10.799> reference 00:20:11.090 --> 00:20:11.100 align:start position:0% specification and the reference 00:20:11.100 --> 00:20:14.330 align:start position:0% specification and the reference implementation<00:20:11.840> to<00:20:13.100> distribute<00:20:14.100> the<00:20:14.220> block 00:20:14.330 --> 00:20:14.340 align:start position:0% implementation to distribute the block 00:20:14.340 --> 00:20:18.230 align:start position:0% implementation to distribute the block proposing<00:20:15.059> and<00:20:15.780> block<00:20:16.080> header<00:20:16.620> signing<00:20:17.240> to 00:20:18.230 --> 00:20:18.240 align:start position:0% proposing and block header signing to 00:20:18.240 --> 00:20:20.870 align:start position:0% proposing and block header signing to extend<00:20:18.960> the<00:20:19.080> funnel<00:20:19.500> proof<00:20:19.799> of<00:20:20.160> noise<00:20:20.520> lash 00:20:20.870 --> 00:20:20.880 align:start position:0% extend the funnel proof of noise lash 00:20:20.880 --> 00:20:23.630 align:start position:0% extend the funnel proof of noise lash about<00:20:21.000> the<00:20:21.179> station<00:20:21.360> to<00:20:21.780> no<00:20:22.140> slashable<00:20:22.679> blocks 00:20:23.630 --> 00:20:23.640 align:start position:0% about the station to no slashable blocks 00:20:23.640 --> 00:20:25.970 align:start position:0% about the station to no slashable blocks and<00:20:24.419> then<00:20:24.840> to 00:20:25.970 --> 00:20:25.980 align:start position:0% and then to 00:20:25.980 --> 00:20:28.549 align:start position:0% and then to add<00:20:26.580> the<00:20:26.760> proof<00:20:27.120> of<00:20:27.240> liveness<00:20:27.840> as<00:20:28.140> I<00:20:28.380> mentioned 00:20:28.549 --> 00:20:28.559 align:start position:0% add the proof of liveness as I mentioned 00:20:28.559 --> 00:20:30.830 align:start position:0% add the proof of liveness as I mentioned before<00:20:28.740> so<00:20:29.100> proving<00:20:29.520> that<00:20:29.880> a<00:20:30.419> distributed 00:20:30.830 --> 00:20:30.840 align:start position:0% before so proving that a distributed 00:20:30.840 --> 00:20:33.770 align:start position:0% before so proving that a distributed validator<00:20:31.260> will<00:20:31.740> always<00:20:31.980> eventually<00:20:32.780> create 00:20:33.770 --> 00:20:33.780 align:start position:0% validator will always eventually create 00:20:33.780 --> 00:20:36.890 align:start position:0% validator will always eventually create a<00:20:34.140> valid<00:20:34.620> attestation<00:20:35.100> valid<00:20:35.820> blocks<00:20:36.240> and 00:20:36.890 --> 00:20:36.900 align:start position:0% a valid attestation valid blocks and 00:20:36.900 --> 00:20:39.049 align:start position:0% a valid attestation valid blocks and valid<00:20:37.559> header<00:20:37.919> signatures 00:20:39.049 --> 00:20:39.059 align:start position:0% valid header signatures 00:20:39.059 --> 00:20:41.510 align:start position:0% valid header signatures and<00:20:39.600> this<00:20:40.020> is<00:20:40.140> all<00:20:40.320> for<00:20:40.500> my<00:20:40.679> for<00:20:41.039> me<00:20:41.160> thank<00:20:41.400> you 00:20:41.510 --> 00:20:41.520 align:start position:0% and this is all for my for me thank you 00:20:41.520 --> 00:20:44.990 align:start position:0% and this is all for my for me thank you for<00:20:41.700> listening 00:20:44.990 --> 00:20:45.000 align:start position:0% 00:20:45.000 --> 00:20:47.450 align:start position:0% um what<00:20:45.419> techniques<00:20:45.900> were<00:20:46.020> used<00:20:46.320> to<00:20:47.220> prove 00:20:47.450 --> 00:20:47.460 align:start position:0% um what techniques were used to prove 00:20:47.460 --> 00:20:49.430 align:start position:0% um what techniques were used to prove that<00:20:47.640> reference<00:20:48.240> implementation<00:20:48.780> adheres<00:20:49.380> to 00:20:49.430 --> 00:20:49.440 align:start position:0% that reference implementation adheres to 00:20:49.440 --> 00:20:51.310 align:start position:0% that reference implementation adheres to the<00:20:49.559> specification 00:20:51.310 --> 00:20:51.320 align:start position:0% the specification 00:20:51.320 --> 00:20:52.970 align:start position:0% the specification so 00:20:52.970 --> 00:20:52.980 align:start position:0% so 00:20:52.980 --> 00:20:55.909 align:start position:0% so um 00:20:55.909 --> 00:20:55.919 align:start position:0% 00:20:55.919 --> 00:20:58.970 align:start position:0% okay<00:20:56.460> so<00:20:56.700> we<00:20:57.480> have<00:20:58.020> used<00:20:58.200> the<00:20:58.440> refinement 00:20:58.970 --> 00:20:58.980 align:start position:0% okay so we have used the refinement 00:20:58.980 --> 00:21:02.210 align:start position:0% okay so we have used the refinement technique<00:20:59.460> so<00:21:00.299> we<00:21:00.480> proved<00:21:01.260> through<00:21:01.980> a 00:21:02.210 --> 00:21:02.220 align:start position:0% technique so we proved through a 00:21:02.220 --> 00:21:04.310 align:start position:0% technique so we proved through a refinement<00:21:02.640> basically<00:21:03.120> yeah<00:21:03.419> showing<00:21:04.140> that 00:21:04.310 --> 00:21:04.320 align:start position:0% refinement basically yeah showing that 00:21:04.320 --> 00:21:07.070 align:start position:0% refinement basically yeah showing that if<00:21:04.500> there<00:21:04.919> is<00:21:05.100> a<00:21:05.640> relationship<00:21:06.059> between<00:21:06.539> the 00:21:07.070 --> 00:21:07.080 align:start position:0% if there is a relationship between the 00:21:07.080 --> 00:21:09.950 align:start position:0% if there is a relationship between the uh<00:21:08.039> rest<00:21:08.580> implementation<00:21:09.179> State<00:21:09.480> and<00:21:09.780> the 00:21:09.950 --> 00:21:09.960 align:start position:0% uh rest implementation State and the 00:21:09.960 --> 00:21:12.470 align:start position:0% uh rest implementation State and the specification<00:21:10.440> state<00:21:10.860> that<00:21:11.820> and<00:21:12.059> on<00:21:12.299> a 00:21:12.470 --> 00:21:12.480 align:start position:0% specification state that and on a 00:21:12.480 --> 00:21:16.730 align:start position:0% specification state that and on a transition<00:21:12.780> that<00:21:13.080> is<00:21:13.260> maintained 00:21:16.730 --> 00:21:16.740 align:start position:0% 00:21:16.740 --> 00:21:18.529 align:start position:0% how<00:21:17.340> far<00:21:17.460> away<00:21:17.640> do<00:21:17.880> you<00:21:18.000> think<00:21:18.059> we<00:21:18.179> are<00:21:18.360> from 00:21:18.529 --> 00:21:18.539 align:start position:0% how far away do you think we are from 00:21:18.539 --> 00:21:20.570 align:start position:0% how far away do you think we are from being<00:21:18.660> able<00:21:18.780> to<00:21:19.080> use<00:21:19.320> validator<00:21:19.799> pools<00:21:20.280> for 00:21:20.570 --> 00:21:20.580 align:start position:0% being able to use validator pools for 00:21:20.580 --> 00:21:24.289 align:start position:0% being able to use validator pools for either<00:21:20.820> eth2<00:21:21.480> or<00:21:21.840> other<00:21:22.020> protocols<00:21:22.860> I 00:21:24.289 --> 00:21:24.299 align:start position:0% either eth2 or other protocols I 00:21:24.299 --> 00:21:28.310 align:start position:0% either eth2 or other protocols I probably<00:21:24.720> this<00:21:25.200> is<00:21:25.320> a<00:21:25.980> question<00:21:26.460> I<00:21:26.940> need<00:21:27.360> to 00:21:28.310 --> 00:21:28.320 align:start position:0% probably this is a question I need to 00:21:28.320 --> 00:21:31.490 align:start position:0% probably this is a question I need to to<00:21:29.039> the<00:21:29.280> fair<00:21:29.460> to<00:21:29.700> someone<00:21:29.940> else<00:21:30.120> sorry<00:21:30.419> I<00:21:31.080> yeah 00:21:31.490 --> 00:21:31.500 align:start position:0% to the fair to someone else sorry I yeah 00:21:31.500 --> 00:21:32.990 align:start position:0% to the fair to someone else sorry I yeah it's 00:21:32.990 --> 00:21:33.000 align:start position:0% it's 00:21:33.000 --> 00:21:35.990 align:start position:0% it's only<00:21:33.720> this<00:21:34.679> is<00:21:34.799> about<00:21:34.919> implementation<00:21:35.700> so 00:21:35.990 --> 00:21:36.000 align:start position:0% only this is about implementation so 00:21:36.000 --> 00:21:38.390 align:start position:0% only this is about implementation so yeah<00:21:36.240> I<00:21:36.480> I<00:21:36.720> don't<00:21:37.020> have<00:21:37.260> that<00:21:37.500> answer<00:21:37.740> how 00:21:38.390 --> 00:21:38.400 align:start position:0% yeah I I don't have that answer how 00:21:38.400 --> 00:21:40.850 align:start position:0% yeah I I don't have that answer how difficult<00:21:38.760> is<00:21:39.000> the<00:21:39.179> learning<00:21:39.539> curve<00:21:39.900> to<00:21:40.320> kind 00:21:40.850 --> 00:21:40.860 align:start position:0% difficult is the learning curve to kind 00:21:40.860 --> 00:21:43.930 align:start position:0% difficult is the learning curve to kind of<00:21:40.980> become<00:21:41.340> someone<00:21:41.640> who<00:21:42.179> can<00:21:42.480> contribute<00:21:43.380> to 00:21:43.930 --> 00:21:43.940 align:start position:0% of become someone who can contribute to 00:21:43.940 --> 00:21:46.730 align:start position:0% of become someone who can contribute to this<00:21:44.940> uh<00:21:45.240> you<00:21:45.780> know<00:21:45.840> formal<00:21:46.260> verification 00:21:46.730 --> 00:21:46.740 align:start position:0% this uh you know formal verification 00:21:46.740 --> 00:21:48.770 align:start position:0% this uh you know formal verification things<00:21:47.100> and<00:21:47.400> be<00:21:47.580> able<00:21:47.760> to<00:21:48.059> to<00:21:48.240> start<00:21:48.480> working 00:21:48.770 --> 00:21:48.780 align:start position:0% things and be able to to start working 00:21:48.780 --> 00:21:50.029 align:start position:0% things and be able to to start working on<00:21:49.020> that 00:21:50.029 --> 00:21:50.039 align:start position:0% on that 00:21:50.039 --> 00:21:53.870 align:start position:0% on that it's<00:21:50.820> a 00:21:53.870 --> 00:21:53.880 align:start position:0% 00:21:53.880 --> 00:21:55.430 align:start position:0% reasonably 00:21:55.430 --> 00:21:55.440 align:start position:0% reasonably 00:21:55.440 --> 00:21:57.649 align:start position:0% reasonably say<00:21:55.980> steep<00:21:56.400> not<00:21:56.640> too<00:21:56.820> much<00:21:57.000> though<00:21:57.240> I<00:21:57.539> mean 00:21:57.649 --> 00:21:57.659 align:start position:0% say steep not too much though I mean 00:21:57.659 --> 00:22:01.070 align:start position:0% say steep not too much though I mean nowadays<00:21:58.440> with<00:21:58.679> tools<00:21:59.100> like<00:21:59.220> Daphne<00:21:59.960> I<00:22:00.960> think 00:22:01.070 --> 00:22:01.080 align:start position:0% nowadays with tools like Daphne I think 00:22:01.080 --> 00:22:03.289 align:start position:0% nowadays with tools like Daphne I think it's<00:22:01.320> much<00:22:01.559> simpler<00:22:02.100> than<00:22:02.640> having<00:22:02.880> to<00:22:03.120> learn 00:22:03.289 --> 00:22:03.299 align:start position:0% it's much simpler than having to learn 00:22:03.299 --> 00:22:05.510 align:start position:0% it's much simpler than having to learn something<00:22:03.600> like<00:22:04.260> Isabel<00:22:04.740> or<00:22:05.340> this 00:22:05.510 --> 00:22:05.520 align:start position:0% something like Isabel or this 00:22:05.520 --> 00:22:07.430 align:start position:0% something like Isabel or this pyramid<00:22:05.940> proves<00:22:06.240> that<00:22:06.419> are<00:22:06.539> a<00:22:06.780> bit<00:22:06.900> not<00:22:07.200> more 00:22:07.430 --> 00:22:07.440 align:start position:0% pyramid proves that are a bit not more 00:22:07.440 --> 00:22:10.610 align:start position:0% pyramid proves that are a bit not more you<00:22:07.740> say<00:22:08.460> abstract<00:22:09.179> syntax<00:22:09.659> and 00:22:10.610 --> 00:22:10.620 align:start position:0% you say abstract syntax and 00:22:10.620 --> 00:22:12.529 align:start position:0% you say abstract syntax and um<00:22:10.679> way<00:22:10.980> of<00:22:11.159> proving<00:22:11.460> things<00:22:11.640> so<00:22:11.940> things<00:22:12.360> are 00:22:12.529 --> 00:22:12.539 align:start position:0% um way of proving things so things are 00:22:12.539 --> 00:22:15.529 align:start position:0% um way of proving things so things are improving<00:22:12.960> but<00:22:13.200> that<00:22:13.740> is<00:22:13.919> that<00:22:14.220> is<00:22:14.640> a<00:22:14.880> bit<00:22:15.000> in 00:22:15.529 --> 00:22:15.539 align:start position:0% improving but that is that is a bit in 00:22:15.539 --> 00:22:16.850 align:start position:0% improving but that is that is a bit in terms<00:22:15.720> of<00:22:15.780> contributing<00:22:16.440> to<00:22:16.620> the 00:22:16.850 --> 00:22:16.860 align:start position:0% terms of contributing to the 00:22:16.860 --> 00:22:18.289 align:start position:0% terms of contributing to the specifications<00:22:17.460> say<00:22:17.820> or<00:22:18.000> reference 00:22:18.289 --> 00:22:18.299 align:start position:0% specifications say or reference 00:22:18.299 --> 00:22:21.649 align:start position:0% specifications say or reference implementation<00:22:18.919> I<00:22:19.919> think<00:22:20.039> it's<00:22:20.340> not<00:22:21.000> my<00:22:21.480> view 00:22:21.649 --> 00:22:21.659 align:start position:0% implementation I think it's not my view 00:22:21.659 --> 00:22:25.430 align:start position:0% implementation I think it's not my view not<00:22:22.380> as<00:22:22.679> much<00:22:23.039> harder<00:22:23.520> as<00:22:24.179> contributed<00:22:25.080> to<00:22:25.260> a 00:22:25.430 --> 00:22:25.440 align:start position:0% not as much harder as contributed to a 00:22:25.440 --> 00:22:26.690 align:start position:0% not as much harder as contributed to a python 00:22:26.690 --> 00:22:26.700 align:start position:0% python 00:22:26.700 --> 00:22:29.930 align:start position:0% python specification<00:22:27.980> so<00:22:28.980> it<00:22:29.100> won't<00:22:29.280> contribute 00:22:29.930 --> 00:22:29.940 align:start position:0% specification so it won't contribute 00:22:29.940 --> 00:22:31.789 align:start position:0% specification so it won't contribute just<00:22:30.120> to<00:22:30.299> the<00:22:30.360> specification<00:22:30.900> you<00:22:31.679> know 00:22:31.789 --> 00:22:31.799 align:start position:0% just to the specification you know 00:22:31.799 --> 00:22:33.649 align:start position:0% just to the specification you know necessarily<00:22:32.460> to<00:22:32.580> the<00:22:32.700> proof 00:22:33.649 --> 00:22:33.659 align:start position:0% necessarily to the proof 00:22:33.659 --> 00:22:35.690 align:start position:0% necessarily to the proof how<00:22:34.440> big<00:22:34.620> is<00:22:34.799> your<00:22:34.860> team<00:22:35.100> and<00:22:35.280> how<00:22:35.400> long<00:22:35.580> have 00:22:35.690 --> 00:22:35.700 align:start position:0% how big is your team and how long have 00:22:35.700 --> 00:22:37.430 align:start position:0% how big is your team and how long have you<00:22:35.880> been<00:22:36.059> working<00:22:36.360> on<00:22:36.600> this<00:22:36.720> proof<00:22:37.020> to<00:22:37.200> get<00:22:37.320> it 00:22:37.430 --> 00:22:37.440 align:start position:0% you been working on this proof to get it 00:22:37.440 --> 00:22:38.810 align:start position:0% you been working on this proof to get it to<00:22:37.500> this<00:22:37.679> point<00:22:37.860> now 00:22:38.810 --> 00:22:38.820 align:start position:0% to this point now 00:22:38.820 --> 00:22:42.529 align:start position:0% to this point now so<00:22:39.419> well<00:22:39.840> uh<00:22:40.679> the<00:22:41.100> the<00:22:41.100> theme<00:22:41.760> consists<00:22:42.419> of 00:22:42.529 --> 00:22:42.539 align:start position:0% so well uh the the theme consists of 00:22:42.539 --> 00:22:44.149 align:start position:0% so well uh the the theme consists of four<00:22:43.080> people 00:22:44.149 --> 00:22:44.159 align:start position:0% four people 00:22:44.159 --> 00:22:45.590 align:start position:0% four people um<00:22:44.220> but<00:22:44.580> on<00:22:44.760> this<00:22:44.940> one<00:22:45.059> I've<00:22:45.240> been<00:22:45.419> working 00:22:45.590 --> 00:22:45.600 align:start position:0% um but on this one I've been working 00:22:45.600 --> 00:22:50.210 align:start position:0% um but on this one I've been working just<00:22:46.080> myself<00:22:46.860> and<00:22:47.340> tanai<00:22:48.240> and<00:22:49.140> we've<00:22:50.100> been 00:22:50.210 --> 00:22:50.220 align:start position:0% just myself and tanai and we've been 00:22:50.220 --> 00:22:53.409 align:start position:0% just myself and tanai and we've been working<00:22:50.520> on<00:22:51.419> this<00:22:51.720> on<00:22:52.080> this<00:22:52.440> uh 00:22:53.409 --> 00:22:53.419 align:start position:0% working on this on this uh 00:22:53.419 --> 00:22:55.250 align:start position:0% working on this on this uh on<00:22:54.419> the 00:22:55.250 --> 00:22:55.260 align:start position:0% on the 00:22:55.260 --> 00:22:56.630 align:start position:0% on the we've<00:22:55.740> been<00:22:55.860> working<00:22:56.039> initially<00:22:56.400> in<00:22:56.520> the 00:22:56.630 --> 00:22:56.640 align:start position:0% we've been working initially in the 00:22:56.640 --> 00:22:59.390 align:start position:0% we've been working initially in the specification<00:22:57.120> so<00:22:57.539> on<00:22:57.720> specifically<00:22:58.500> on<00:22:59.220> the 00:22:59.390 --> 00:22:59.400 align:start position:0% specification so on specifically on the 00:22:59.400 --> 00:23:02.510 align:start position:0% specification so on specifically on the proof<00:22:59.880> I<00:23:00.659> say<00:23:00.840> since<00:23:01.260> June 00:23:02.510 --> 00:23:02.520 align:start position:0% proof I say since June 00:23:02.520 --> 00:23:04.610 align:start position:0% proof I say since June roughly<00:23:03.120> just<00:23:03.419> for<00:23:03.659> the<00:23:03.780> proof<00:23:04.020> there<00:23:04.320> was<00:23:04.500> a 00:23:04.610 --> 00:23:04.620 align:start position:0% roughly just for the proof there was a 00:23:04.620 --> 00:23:06.830 align:start position:0% roughly just for the proof there was a bit<00:23:04.679> of<00:23:04.919> fixing<00:23:05.820> up<00:23:05.940> of<00:23:06.120> the<00:23:06.299> specification 00:23:06.830 --> 00:23:06.840 align:start position:0% bit of fixing up of the specification 00:23:06.840 --> 00:23:09.890 align:start position:0% bit of fixing up of the specification before<00:23:07.200> that<00:23:07.500> so<00:23:08.280> why<00:23:08.460> Daphne<00:23:08.940> and<00:23:09.179> not<00:23:09.419> other 00:23:09.890 --> 00:23:09.900 align:start position:0% before that so why Daphne and not other 00:23:09.900 --> 00:23:12.049 align:start position:0% before that so why Daphne and not other languages<00:23:10.320> like<00:23:10.620> cocoa<00:23:11.280> or<00:23:11.400> Isabel<00:23:11.760> as<00:23:11.940> you 00:23:12.049 --> 00:23:12.059 align:start position:0% languages like cocoa or Isabel as you 00:23:12.059 --> 00:23:16.490 align:start position:0% languages like cocoa or Isabel as you said<00:23:12.179> yeah<00:23:12.919> one<00:23:13.919> of<00:23:14.039> the<00:23:14.159> reason<00:23:14.460> is<00:23:14.820> that<00:23:15.500> is 00:23:16.490 --> 00:23:16.500 align:start position:0% said yeah one of the reason is that is 00:23:16.500 --> 00:23:19.610 align:start position:0% said yeah one of the reason is that is for<00:23:16.799> the<00:23:17.340> said<00:23:18.000> the<00:23:18.539> fact<00:23:18.720> that<00:23:18.720> we<00:23:19.140> think<00:23:19.320> it's 00:23:19.610 --> 00:23:19.620 align:start position:0% for the said the fact that we think it's 00:23:19.620 --> 00:23:21.490 align:start position:0% for the said the fact that we think it's easier<00:23:20.039> for 00:23:21.490 --> 00:23:21.500 align:start position:0% easier for 00:23:21.500 --> 00:23:24.710 align:start position:0% easier for developers<00:23:22.500> to<00:23:22.799> understand<00:23:23.100> Daphne<00:23:23.760> compared 00:23:24.710 --> 00:23:24.720 align:start position:0% developers to understand Daphne compared 00:23:24.720 --> 00:23:28.370 align:start position:0% developers to understand Daphne compared to<00:23:25.980> or<00:23:26.159> lean<00:23:26.640> or<00:23:26.880> Isabel<00:23:27.480> that<00:23:28.200> that's 00:23:28.370 --> 00:23:28.380 align:start position:0% to or lean or Isabel that that's 00:23:28.380 --> 00:23:31.070 align:start position:0% to or lean or Isabel that that's one<00:23:28.740> of<00:23:28.860> the<00:23:29.039> of<00:23:29.340> the<00:23:29.580> reason<00:23:29.640> also<00:23:30.059> I<00:23:30.780> mean<00:23:30.960> you 00:23:31.070 --> 00:23:31.080 align:start position:0% one of the of the reason also I mean you 00:23:31.080 --> 00:23:33.590 align:start position:0% one of the of the reason also I mean you can<00:23:31.260> compile<00:23:31.679> uh 00:23:33.590 --> 00:23:33.600 align:start position:0% can compile uh 00:23:33.600 --> 00:23:37.310 align:start position:0% can compile uh if<00:23:34.140> they<00:23:34.500> I<00:23:34.740> think<00:23:34.860> or<00:23:35.400> Isabel<00:23:35.940> but 00:23:37.310 --> 00:23:37.320 align:start position:0% if they I think or Isabel but 00:23:37.320 --> 00:23:39.049 align:start position:0% if they I think or Isabel but it 00:23:39.049 --> 00:23:39.059 align:start position:0% it 00:23:39.059 --> 00:23:41.210 align:start position:0% it the<00:23:39.539> way<00:23:39.659> you<00:23:39.780> write<00:23:39.960> it<00:23:40.140> is<00:23:40.380> far<00:23:40.620> more<00:23:40.740> complex 00:23:41.210 --> 00:23:41.220 align:start position:0% the way you write it is far more complex 00:23:41.220 --> 00:23:43.310 align:start position:0% the way you write it is far more complex yeah<00:23:41.520> yeah<00:23:41.760> I'm<00:23:42.539> not 00:23:43.310 --> 00:23:43.320 align:start position:0% yeah yeah I'm not 00:23:43.320 --> 00:23:45.710 align:start position:0% yeah yeah I'm not pretty<00:23:43.740> sure<00:23:43.980> like<00:23:44.340> we<00:23:44.760> definitely<00:23:45.059> can<00:23:45.360> kind 00:23:45.710 --> 00:23:45.720 align:start position:0% pretty sure like we definitely can kind 00:23:45.720 --> 00:23:47.029 align:start position:0% pretty sure like we definitely can kind of 00:23:47.029 --> 00:23:47.039 align:start position:0% of 00:23:47.039 --> 00:23:49.070 align:start position:0% of um<00:23:47.159> use<00:23:47.940> a 00:23:49.070 --> 00:23:49.080 align:start position:0% um use a 00:23:49.080 --> 00:23:51.710 align:start position:0% um use a as<00:23:49.799> a<00:23:49.980> construct<00:23:50.280> that<00:23:50.520> is<00:23:50.820> as<00:23:51.059> the<00:23:51.240> concept<00:23:51.539> of 00:23:51.710 --> 00:23:51.720 align:start position:0% as a construct that is as the concept of 00:23:51.720 --> 00:23:53.570 align:start position:0% as a construct that is as the concept of classes<00:23:52.140> and<00:23:52.320> state<00:23:52.559> so<00:23:52.980> it's<00:23:53.159> very<00:23:53.280> similar 00:23:53.570 --> 00:23:53.580 align:start position:0% classes and state so it's very similar 00:23:53.580 --> 00:23:55.010 align:start position:0% classes and state so it's very similar to<00:23:53.700> programming<00:23:54.120> and<00:23:54.299> you<00:23:54.480> can<00:23:54.600> have<00:23:54.720> some 00:23:55.010 --> 00:23:55.020 align:start position:0% to programming and you can have some 00:23:55.020 --> 00:23:57.230 align:start position:0% to programming and you can have some give<00:23:55.320> some<00:23:55.679> of<00:23:55.799> the<00:23:55.919> things<00:23:56.460> unimplemented 00:23:57.230 --> 00:23:57.240 align:start position:0% give some of the things unimplemented 00:23:57.240 --> 00:24:02.000 align:start position:0% give some of the things unimplemented and<00:23:57.600> open<00:23:58.080> for<00:23:58.799> external<00:23:59.400> implementation