WEBVTT Kind: captions Language: en 00:00:13.360 --> 00:00:16.299 align:start position:0% so<00:00:14.360> hi<00:00:14.719> everyone<00:00:15.169> my<00:00:15.349> name<00:00:15.499> is<00:00:15.530> Rita<00:00:15.829> twinkler 00:00:16.299 --> 00:00:16.309 align:start position:0% so hi everyone my name is Rita twinkler 00:00:16.309 --> 00:00:19.150 align:start position:0% so hi everyone my name is Rita twinkler I'm<00:00:16.789> the<00:00:17.510> chairman<00:00:17.870> and<00:00:18.080> co-founder<00:00:18.380> together 00:00:19.150 --> 00:00:19.160 align:start position:0% I'm the chairman and co-founder together 00:00:19.160 --> 00:00:22.450 align:start position:0% I'm the chairman and co-founder together with<00:00:19.370> Mona<00:00:19.580> Lisa<00:00:19.850> of<00:00:20.150> Mellon<00:00:20.600> port<00:00:20.840> and<00:00:21.460> Marcin 00:00:22.450 --> 00:00:22.460 align:start position:0% with Mona Lisa of Mellon port and Marcin 00:00:22.460 --> 00:00:31.090 align:start position:0% with Mona Lisa of Mellon port and Marcin advisor<00:00:22.940> to<00:00:23.240> the<00:00:23.330> web<00:00:23.480> 3<00:00:23.720> Foundation<00:00:25.510> so<00:00:30.100> great 00:00:31.090 --> 00:00:31.100 align:start position:0% advisor to the web 3 Foundation so great 00:00:31.100 --> 00:00:34.810 align:start position:0% advisor to the web 3 Foundation so great so<00:00:31.340> let's<00:00:31.520> starts<00:00:31.850> with<00:00:32.980> formal<00:00:33.980> education<00:00:34.550> so 00:00:34.810 --> 00:00:34.820 align:start position:0% so let's starts with formal education so 00:00:34.820 --> 00:00:38.590 align:start position:0% so let's starts with formal education so formal<00:00:35.510> verification<00:00:35.660> is<00:00:37.240> the<00:00:38.240> act<00:00:38.420> of 00:00:38.590 --> 00:00:38.600 align:start position:0% formal verification is the act of 00:00:38.600 --> 00:00:42.280 align:start position:0% formal verification is the act of proving<00:00:39.260> or<00:00:39.410> disproving<00:00:39.560> an<00:00:40.040> algorithm<00:00:41.290> with 00:00:42.280 --> 00:00:42.290 align:start position:0% proving or disproving an algorithm with 00:00:42.290 --> 00:00:44.710 align:start position:0% proving or disproving an algorithm with respect<00:00:42.650> to<00:00:42.890> an<00:00:43.310> Intendant<00:00:44.239> underlying 00:00:44.710 --> 00:00:44.720 align:start position:0% respect to an Intendant underlying 00:00:44.720 --> 00:00:47.410 align:start position:0% respect to an Intendant underlying algorithm<00:00:45.320> so<00:00:46.280> this<00:00:46.430> algorithm<00:00:46.880> is<00:00:46.970> specified 00:00:47.410 --> 00:00:47.420 align:start position:0% algorithm so this algorithm is specified 00:00:47.420 --> 00:00:50.590 align:start position:0% algorithm so this algorithm is specified in<00:00:47.570> a<00:00:47.690> in<00:00:47.870> a<00:00:47.960> formal<00:00:48.350> specification<00:00:49.120> so<00:00:50.120> I'd 00:00:50.590 --> 00:00:50.600 align:start position:0% in a in a formal specification so I'd 00:00:50.600 --> 00:00:53.049 align:start position:0% in a in a formal specification so I'd like<00:00:50.780> to<00:00:50.840> ask<00:00:51.110> all<00:00:51.440> of<00:00:51.500> you<00:00:51.770> what<00:00:52.489> makes<00:00:52.730> a<00:00:52.910> good 00:00:53.049 --> 00:00:53.059 align:start position:0% like to ask all of you what makes a good 00:00:53.059 --> 00:01:03.370 align:start position:0% like to ask all of you what makes a good specification<00:01:01.989> what<00:01:02.989> makes<00:01:03.170> a<00:01:03.290> good 00:01:03.370 --> 00:01:03.380 align:start position:0% specification what makes a good 00:01:03.380 --> 00:01:04.959 align:start position:0% specification what makes a good specification<00:01:04.070> that's<00:01:04.189> a<00:01:04.309> good<00:01:04.460> question<00:01:04.790> so 00:01:04.959 --> 00:01:04.969 align:start position:0% specification that's a good question so 00:01:04.969 --> 00:01:07.450 align:start position:0% specification that's a good question so I<00:01:05.570> think<00:01:05.840> theoretically<00:01:06.440> the<00:01:06.799> the<00:01:07.040> answer<00:01:07.280> is 00:01:07.450 --> 00:01:07.460 align:start position:0% I think theoretically the the answer is 00:01:07.460 --> 00:01:09.130 align:start position:0% I think theoretically the the answer is that<00:01:07.700> the<00:01:07.850> specification<00:01:08.540> accurately 00:01:09.130 --> 00:01:09.140 align:start position:0% that the specification accurately 00:01:09.140 --> 00:01:11.260 align:start position:0% that the specification accurately captures<00:01:09.620> the<00:01:09.830> intent<00:01:10.250> of<00:01:10.520> the<00:01:10.670> developer<00:01:11.150> who 00:01:11.260 --> 00:01:11.270 align:start position:0% captures the intent of the developer who 00:01:11.270 --> 00:01:14.440 align:start position:0% captures the intent of the developer who wrote<00:01:11.479> it<00:01:12.310> making<00:01:13.310> sure<00:01:13.549> that's<00:01:13.790> the<00:01:14.000> case<00:01:14.180> is 00:01:14.440 --> 00:01:14.450 align:start position:0% wrote it making sure that's the case is 00:01:14.450 --> 00:01:17.050 align:start position:0% wrote it making sure that's the case is obviously<00:01:14.990> very<00:01:15.110> difficult<00:01:15.560> so<00:01:16.310> I<00:01:16.340> think<00:01:16.729> a 00:01:17.050 --> 00:01:17.060 align:start position:0% obviously very difficult so I think a 00:01:17.060 --> 00:01:18.580 align:start position:0% obviously very difficult so I think a lot<00:01:17.360> of<00:01:17.390> that<00:01:17.600> depends<00:01:17.960> on<00:01:18.170> sort<00:01:18.380> of<00:01:18.409> your 00:01:18.580 --> 00:01:18.590 align:start position:0% lot of that depends on sort of your 00:01:18.590 --> 00:01:19.990 align:start position:0% lot of that depends on sort of your tooling<00:01:18.950> and<00:01:19.130> the<00:01:19.340> feedback<00:01:19.549> that<00:01:19.909> it 00:01:19.990 --> 00:01:20.000 align:start position:0% tooling and the feedback that it 00:01:20.000 --> 00:01:21.010 align:start position:0% tooling and the feedback that it provides<00:01:20.330> when<00:01:20.540> you're<00:01:20.659> writing<00:01:20.930> the 00:01:21.010 --> 00:01:21.020 align:start position:0% provides when you're writing the 00:01:21.020 --> 00:01:23.980 align:start position:0% provides when you're writing the specification<00:01:22.030> but<00:01:23.030> in<00:01:23.210> general<00:01:23.570> I'd<00:01:23.690> say<00:01:23.960> a 00:01:23.980 --> 00:01:23.990 align:start position:0% specification but in general I'd say a 00:01:23.990 --> 00:01:25.780 align:start position:0% specification but in general I'd say a good<00:01:24.290> specification<00:01:24.979> accurately<00:01:25.460> reflects 00:01:25.780 --> 00:01:25.790 align:start position:0% good specification accurately reflects 00:01:25.790 --> 00:01:27.550 align:start position:0% good specification accurately reflects the<00:01:25.970> intent<00:01:26.180> of<00:01:26.360> the<00:01:26.450> developer<00:01:26.930> and<00:01:27.200> also 00:01:27.550 --> 00:01:27.560 align:start position:0% the intent of the developer and also 00:01:27.560 --> 00:01:29.530 align:start position:0% the intent of the developer and also encodes<00:01:28.010> sort<00:01:28.400> of<00:01:28.490> all<00:01:28.700> of<00:01:28.880> the<00:01:28.970> assumptions 00:01:29.530 --> 00:01:29.540 align:start position:0% encodes sort of all of the assumptions 00:01:29.540 --> 00:01:31.570 align:start position:0% encodes sort of all of the assumptions that<00:01:29.690> the<00:01:30.290> smart<00:01:30.530> contract<00:01:30.979> makes<00:01:31.220> very 00:01:31.570 --> 00:01:31.580 align:start position:0% that the smart contract makes very 00:01:31.580 --> 00:01:34.149 align:start position:0% that the smart contract makes very explicitly<00:01:32.150> and<00:01:32.360> very<00:01:32.540> clearly<00:01:32.920> so<00:01:33.920> that<00:01:33.950> if 00:01:34.149 --> 00:01:34.159 align:start position:0% explicitly and very clearly so that if 00:01:34.159 --> 00:01:35.260 align:start position:0% explicitly and very clearly so that if someone<00:01:34.340> were<00:01:34.490> to<00:01:34.549> update<00:01:34.760> the<00:01:35.060> smart 00:01:35.260 --> 00:01:35.270 align:start position:0% someone were to update the smart 00:01:35.270 --> 00:01:36.640 align:start position:0% someone were to update the smart contract<00:01:35.659> later<00:01:35.840> or<00:01:36.080> something<00:01:36.409> they<00:01:36.530> would 00:01:36.640 --> 00:01:36.650 align:start position:0% contract later or something they would 00:01:36.650 --> 00:01:40.600 align:start position:0% contract later or something they would all<00:01:36.740> be<00:01:36.770> very<00:01:37.670> nicely<00:01:37.909> in<00:01:38.119> the<00:01:38.180> same<00:01:38.360> place<00:01:39.610> is 00:01:40.600 --> 00:01:40.610 align:start position:0% all be very nicely in the same place is 00:01:40.610 --> 00:01:42.670 align:start position:0% all be very nicely in the same place is going<00:01:40.790> to<00:01:40.850> add<00:01:41.000> a<00:01:41.030> little<00:01:41.270> bit<00:01:41.420> more<00:01:41.689> I<00:01:41.930> think<00:01:42.290> a 00:01:42.670 --> 00:01:42.680 align:start position:0% going to add a little bit more I think a 00:01:42.680 --> 00:01:44.620 align:start position:0% going to add a little bit more I think a good<00:01:43.010> specifications<00:01:43.520> to<00:01:44.030> be<00:01:44.210> easy<00:01:44.450> to 00:01:44.620 --> 00:01:44.630 align:start position:0% good specifications to be easy to 00:01:44.630 --> 00:01:47.950 align:start position:0% good specifications to be easy to understand<00:01:45.200> and<00:01:45.409> to<00:01:46.189> be<00:01:46.340> easily<00:01:46.640> to<00:01:47.000> for<00:01:47.840> other 00:01:47.950 --> 00:01:47.960 align:start position:0% understand and to be easily to for other 00:01:47.960 --> 00:01:49.810 align:start position:0% understand and to be easily to for other to<00:01:48.259> you<00:01:48.619> know<00:01:48.710> read<00:01:48.920> and<00:01:49.189> you<00:01:49.310> know<00:01:49.400> built<00:01:49.670> ask 00:01:49.810 --> 00:01:49.820 align:start position:0% to you know read and you know built ask 00:01:49.820 --> 00:01:53.080 align:start position:0% to you know read and you know built ask a<00:01:49.970> little<00:01:50.420> and<00:01:51.340> it's<00:01:52.340> clearly<00:01:52.549> you<00:01:52.790> know<00:01:52.939> it 00:01:53.080 --> 00:01:53.090 align:start position:0% a little and it's clearly you know it 00:01:53.090 --> 00:01:57.249 align:start position:0% a little and it's clearly you know it follows<00:01:53.420> some<00:01:53.450> standard<00:01:54.020> as<00:01:54.200> well<00:01:54.439> I<00:01:55.900> think<00:01:56.900> in 00:01:57.249 --> 00:01:57.259 align:start position:0% follows some standard as well I think in 00:01:57.259 --> 00:01:59.230 align:start position:0% follows some standard as well I think in general<00:01:57.290> any<00:01:57.950> specification<00:01:58.610> is<00:01:58.729> better<00:01:58.970> than 00:01:59.230 --> 00:01:59.240 align:start position:0% general any specification is better than 00:01:59.240 --> 00:02:00.850 align:start position:0% general any specification is better than what<00:01:59.869> most<00:02:00.079> people<00:02:00.350> do<00:02:00.470> which<00:02:00.590> is<00:02:00.710> no 00:02:00.850 --> 00:02:00.860 align:start position:0% what most people do which is no 00:02:00.860 --> 00:02:03.969 align:start position:0% what most people do which is no specification<00:02:02.200> so<00:02:03.200> that's<00:02:03.560> probably<00:02:03.799> a<00:02:03.860> good 00:02:03.969 --> 00:02:03.979 align:start position:0% specification so that's probably a good 00:02:03.979 --> 00:02:05.590 align:start position:0% specification so that's probably a good place<00:02:04.040> to<00:02:04.220> start<00:02:04.640> ideally<00:02:05.060> you'd<00:02:05.240> you<00:02:05.479> know 00:02:05.590 --> 00:02:05.600 align:start position:0% place to start ideally you'd you know 00:02:05.600 --> 00:02:07.359 align:start position:0% place to start ideally you'd you know write<00:02:05.810> a<00:02:05.840> specification<00:02:06.079> and<00:02:06.740> then<00:02:06.860> argue 00:02:07.359 --> 00:02:07.369 align:start position:0% write a specification and then argue 00:02:07.369 --> 00:02:08.979 align:start position:0% write a specification and then argue over<00:02:07.579> that<00:02:07.729> for<00:02:07.970> a<00:02:08.000> few<00:02:08.179> days<00:02:08.329> at<00:02:08.539> least<00:02:08.659> and 00:02:08.979 --> 00:02:08.989 align:start position:0% over that for a few days at least and 00:02:08.989 --> 00:02:10.990 align:start position:0% over that for a few days at least and then<00:02:09.079> you<00:02:09.920> know<00:02:10.009> write<00:02:10.220> your<00:02:10.369> tests<00:02:10.729> and<00:02:10.819> then 00:02:10.990 --> 00:02:11.000 align:start position:0% then you know write your tests and then 00:02:11.000 --> 00:02:12.910 align:start position:0% then you know write your tests and then the<00:02:11.180> encoding<00:02:11.720> but<00:02:11.959> a<00:02:12.170> lot<00:02:12.290> of<00:02:12.410> people<00:02:12.620> kind<00:02:12.800> of 00:02:12.910 --> 00:02:12.920 align:start position:0% the encoding but a lot of people kind of 00:02:12.920 --> 00:02:14.589 align:start position:0% the encoding but a lot of people kind of do<00:02:13.010> it<00:02:13.130> maybe<00:02:13.640> in<00:02:13.819> the<00:02:13.880> reverse<00:02:14.090> order<00:02:14.330> or 00:02:14.589 --> 00:02:14.599 align:start position:0% do it maybe in the reverse order or 00:02:14.599 --> 00:02:15.250 align:start position:0% do it maybe in the reverse order or something<00:02:14.750> like<00:02:14.989> that 00:02:15.250 --> 00:02:15.260 align:start position:0% something like that 00:02:15.260 --> 00:02:16.119 align:start position:0% something like that maybe<00:02:15.470> they<00:02:15.620> never<00:02:15.769> even<00:02:15.890> read<00:02:16.099> a 00:02:16.119 --> 00:02:16.129 align:start position:0% maybe they never even read a 00:02:16.129 --> 00:02:21.550 align:start position:0% maybe they never even read a specification<00:02:16.489> so<00:02:19.720> please<00:02:20.720> answer<00:02:20.900> captures 00:02:21.550 --> 00:02:21.560 align:start position:0% specification so please answer captures 00:02:21.560 --> 00:02:25.059 align:start position:0% specification so please answer captures it<00:02:21.769> but<00:02:22.420> maybe<00:02:23.420> a<00:02:23.569> good<00:02:23.810> specification<00:02:24.650> should 00:02:25.059 --> 00:02:25.069 align:start position:0% it but maybe a good specification should 00:02:25.069 --> 00:02:30.009 align:start position:0% it but maybe a good specification should put<00:02:26.200> contract<00:02:27.200> in<00:02:27.530> bigger<00:02:28.220> picture<00:02:28.760> what<00:02:29.659> kind 00:02:30.009 --> 00:02:30.019 align:start position:0% put contract in bigger picture what kind 00:02:30.019 --> 00:02:32.949 align:start position:0% put contract in bigger picture what kind of<00:02:30.200> game<00:02:30.439> people<00:02:30.950> can<00:02:31.579> play<00:02:31.879> on<00:02:32.120> it<00:02:32.360> what<00:02:32.720> would 00:02:32.949 --> 00:02:32.959 align:start position:0% of game people can play on it what would 00:02:32.959 --> 00:02:35.770 align:start position:0% of game people can play on it what would be<00:02:33.170> the<00:02:34.510> well-paced 00:02:35.770 --> 00:02:35.780 align:start position:0% be the well-paced 00:02:35.780 --> 00:02:40.349 align:start position:0% be the well-paced strategy<00:02:36.590> for<00:02:36.860> rational<00:02:37.250> players<00:02:37.819> and<00:02:38.750> so 00:02:40.349 --> 00:02:40.359 align:start position:0% strategy for rational players and so 00:02:40.359 --> 00:02:43.809 align:start position:0% strategy for rational players and so yeah<00:02:41.359> if<00:02:41.510> a<00:02:41.959> specification<00:02:42.470> fits<00:02:43.129> into<00:02:43.489> this 00:02:43.809 --> 00:02:43.819 align:start position:0% yeah if a specification fits into this 00:02:43.819 --> 00:02:46.300 align:start position:0% yeah if a specification fits into this script<00:02:44.390> economic<00:02:45.109> mechanic<00:02:46.040> game<00:02:46.280> a 00:02:46.300 --> 00:02:46.310 align:start position:0% script economic mechanic game a 00:02:46.310 --> 00:02:49.300 align:start position:0% script economic mechanic game a theoretic<00:02:46.760> reasoning<00:02:47.510> that<00:02:48.129> something<00:02:49.129> nice 00:02:49.300 --> 00:02:49.310 align:start position:0% theoretic reasoning that something nice 00:02:49.310 --> 00:02:51.069 align:start position:0% theoretic reasoning that something nice but<00:02:49.519> the<00:02:49.819> yeah<00:02:50.000> this<00:02:50.239> depends<00:02:50.750> on<00:02:50.840> the 00:02:51.069 --> 00:02:51.079 align:start position:0% but the yeah this depends on the 00:02:51.079 --> 00:02:54.160 align:start position:0% but the yeah this depends on the application<00:02:52.989> Thanks 00:02:54.160 --> 00:02:54.170 align:start position:0% application Thanks 00:02:54.170 --> 00:02:56.770 align:start position:0% application Thanks so<00:02:54.440> so<00:02:54.769> what<00:02:54.920> is<00:02:55.010> your<00:02:55.099> take<00:02:55.280> on<00:02:55.780> a 00:02:56.770 --> 00:02:56.780 align:start position:0% so so what is your take on a 00:02:56.780 --> 00:03:00.520 align:start position:0% so so what is your take on a specification<00:02:57.639> kind<00:02:58.639> of<00:02:58.760> you<00:02:59.540> know<00:02:59.659> specified 00:03:00.520 --> 00:03:00.530 align:start position:0% specification kind of you know specified 00:03:00.530 --> 00:03:01.720 align:start position:0% specification kind of you know specified kind<00:03:00.829> of<00:03:00.980> abstractly 00:03:01.720 --> 00:03:01.730 align:start position:0% kind of abstractly 00:03:01.730 --> 00:03:04.030 align:start position:0% kind of abstractly with<00:03:02.239> formal<00:03:02.599> methods<00:03:02.900> of<00:03:03.139> mathematics<00:03:03.680> Bosch 00:03:04.030 --> 00:03:04.040 align:start position:0% with formal methods of mathematics Bosch 00:03:04.040 --> 00:03:07.059 align:start position:0% with formal methods of mathematics Bosch versus<00:03:05.379> specification<00:03:06.379> implemented<00:03:06.950> for 00:03:07.059 --> 00:03:07.069 align:start position:0% versus specification implemented for 00:03:07.069 --> 00:03:14.680 align:start position:0% versus specification implemented for example<00:03:07.430> in<00:03:07.519> Haskell<00:03:12.250> so<00:03:13.250> I<00:03:13.579> mean<00:03:13.970> one<00:03:14.329> is<00:03:14.450> kind 00:03:14.680 --> 00:03:14.690 align:start position:0% example in Haskell so I mean one is kind 00:03:14.690 --> 00:03:16.569 align:start position:0% example in Haskell so I mean one is kind of<00:03:14.750> like<00:03:15.109> a<00:03:15.139> reference<00:03:15.530> implementation<00:03:15.680> in 00:03:16.569 --> 00:03:16.579 align:start position:0% of like a reference implementation in 00:03:16.579 --> 00:03:18.129 align:start position:0% of like a reference implementation in Haskell<00:03:17.090> and<00:03:17.299> the<00:03:17.450> other<00:03:17.569> is<00:03:17.690> just<00:03:17.930> kind<00:03:18.079> of 00:03:18.129 --> 00:03:18.139 align:start position:0% Haskell and the other is just kind of 00:03:18.139 --> 00:03:21.759 align:start position:0% Haskell and the other is just kind of abstract<00:03:18.650> like<00:03:18.920> purely<00:03:19.430> theoretical<00:03:20.739> well<00:03:21.739> I 00:03:21.759 --> 00:03:21.769 align:start position:0% abstract like purely theoretical well I 00:03:21.769 --> 00:03:24.909 align:start position:0% abstract like purely theoretical well I think<00:03:21.949> that<00:03:22.599> a<00:03:23.599> reference<00:03:24.169> implementation<00:03:24.319> in 00:03:24.909 --> 00:03:24.919 align:start position:0% think that a reference implementation in 00:03:24.919 --> 00:03:25.890 align:start position:0% think that a reference implementation in Haskell<00:03:25.280> is<00:03:25.400> a<00:03:25.459> perfectly<00:03:25.760> fine 00:03:25.890 --> 00:03:25.900 align:start position:0% Haskell is a perfectly fine 00:03:25.900 --> 00:03:29.979 align:start position:0% Haskell is a perfectly fine specification<00:03:26.900> honestly<00:03:27.319> I<00:03:28.120> think<00:03:29.120> a<00:03:29.480> lot<00:03:29.959> of 00:03:29.979 --> 00:03:29.989 align:start position:0% specification honestly I think a lot of 00:03:29.989 --> 00:03:31.059 align:start position:0% specification honestly I think a lot of people<00:03:30.590> when<00:03:30.680> they<00:03:30.709> think<00:03:30.859> of<00:03:30.980> a 00:03:31.059 --> 00:03:31.069 align:start position:0% people when they think of a 00:03:31.069 --> 00:03:32.860 align:start position:0% people when they think of a specification<00:03:31.370> think<00:03:31.819> of<00:03:31.970> kind<00:03:32.359> of<00:03:32.480> just<00:03:32.690> an 00:03:32.860 --> 00:03:32.870 align:start position:0% specification think of kind of just an 00:03:32.870 --> 00:03:34.780 align:start position:0% specification think of kind of just an English<00:03:33.230> language<00:03:33.799> document<00:03:34.370> or<00:03:34.519> something 00:03:34.780 --> 00:03:34.790 align:start position:0% English language document or something 00:03:34.790 --> 00:03:36.849 align:start position:0% English language document or something like<00:03:34.879> that<00:03:34.940> but<00:03:35.389> at<00:03:35.959> least<00:03:36.019> in<00:03:36.319> our<00:03:36.440> group<00:03:36.650> we 00:03:36.849 --> 00:03:36.859 align:start position:0% like that but at least in our group we 00:03:36.859 --> 00:03:39.750 align:start position:0% like that but at least in our group we focus<00:03:37.310> a<00:03:37.400> lot<00:03:37.430> on<00:03:37.579> executable<00:03:38.359> specifications 00:03:39.750 --> 00:03:39.760 align:start position:0% focus a lot on executable specifications 00:03:39.760 --> 00:03:42.300 align:start position:0% focus a lot on executable specifications so<00:03:40.760> I<00:03:40.790> think<00:03:40.940> you<00:03:41.419> know<00:03:41.510> a<00:03:41.540> Haskell 00:03:42.300 --> 00:03:42.310 align:start position:0% so I think you know a Haskell 00:03:42.310 --> 00:03:44.289 align:start position:0% so I think you know a Haskell implementation<00:03:43.310> you<00:03:43.459> know<00:03:43.579> that's<00:03:43.819> a<00:03:43.940> whole 00:03:44.289 --> 00:03:44.299 align:start position:0% implementation you know that's a whole 00:03:44.299 --> 00:03:45.819 align:start position:0% implementation you know that's a whole lot<00:03:44.480> hell<00:03:44.690> of<00:03:44.810> a<00:03:44.870> lot<00:03:45.019> better<00:03:45.139> than<00:03:45.290> no 00:03:45.819 --> 00:03:45.829 align:start position:0% lot hell of a lot better than no 00:03:45.829 --> 00:03:47.259 align:start position:0% lot hell of a lot better than no specification<00:03:46.250> once<00:03:46.699> again<00:03:46.910> and<00:03:47.060> at<00:03:47.120> least 00:03:47.259 --> 00:03:47.269 align:start position:0% specification once again and at least 00:03:47.269 --> 00:03:49.240 align:start position:0% specification once again and at least you<00:03:47.389> can<00:03:47.510> test<00:03:47.720> it<00:03:47.870> right<00:03:48.199> you<00:03:48.410> can<00:03:48.590> you<00:03:49.129> can 00:03:49.240 --> 00:03:49.250 align:start position:0% you can test it right you can you can 00:03:49.250 --> 00:03:50.589 align:start position:0% you can test it right you can you can run<00:03:49.400> tests<00:03:49.699> against<00:03:49.940> your<00:03:50.030> specification 00:03:50.589 --> 00:03:50.599 align:start position:0% run tests against your specification 00:03:50.599 --> 00:03:52.059 align:start position:0% run tests against your specification even<00:03:50.780> before<00:03:51.049> you<00:03:51.169> go<00:03:51.319> to<00:03:51.379> implementing<00:03:51.980> the 00:03:52.059 --> 00:03:52.069 align:start position:0% even before you go to implementing the 00:03:52.069 --> 00:03:54.250 align:start position:0% even before you go to implementing the final<00:03:52.370> thing<00:03:52.549> so<00:03:52.790> that's<00:03:52.930> that's<00:03:53.930> already<00:03:54.169> a 00:03:54.250 --> 00:03:54.260 align:start position:0% final thing so that's that's already a 00:03:54.260 --> 00:03:56.949 align:start position:0% final thing so that's that's already a huge<00:03:54.699> huge<00:03:55.699> advantage<00:03:56.150> over<00:03:56.329> an<00:03:56.690> English 00:03:56.949 --> 00:03:56.959 align:start position:0% huge huge advantage over an English 00:03:56.959 --> 00:03:58.599 align:start position:0% huge huge advantage over an English language<00:03:57.290> specification<00:03:57.889> for<00:03:58.040> example<00:03:58.430> but 00:03:58.599 --> 00:03:58.609 align:start position:0% language specification for example but 00:03:58.609 --> 00:03:59.740 align:start position:0% language specification for example but certainly<00:03:59.299> English<00:03:59.389> language 00:03:59.740 --> 00:03:59.750 align:start position:0% certainly English language 00:03:59.750 --> 00:04:01.119 align:start position:0% certainly English language specifications<00:04:00.199> are<00:04:00.290> easier<00:04:00.560> to<00:04:00.620> write<00:04:00.799> so 00:04:01.119 --> 00:04:01.129 align:start position:0% specifications are easier to write so 00:04:01.129 --> 00:04:02.409 align:start position:0% specifications are easier to write so maybe<00:04:01.370> you<00:04:01.489> start<00:04:01.760> with<00:04:01.879> that<00:04:02.000> and<00:04:02.060> then<00:04:02.299> do 00:04:02.409 --> 00:04:02.419 align:start position:0% maybe you start with that and then do 00:04:02.419 --> 00:04:05.770 align:start position:0% maybe you start with that and then do the<00:04:02.510> Haskell<00:04:02.870> or<00:04:02.900> something<00:04:03.290> like<00:04:03.379> that<00:04:04.780> yeah 00:04:05.770 --> 00:04:05.780 align:start position:0% the Haskell or something like that yeah 00:04:05.780 --> 00:04:07.780 align:start position:0% the Haskell or something like that yeah I<00:04:05.810> totally<00:04:06.470> agree<00:04:06.650> with<00:04:06.859> everything<00:04:07.400> that<00:04:07.549> was 00:04:07.780 --> 00:04:07.790 align:start position:0% I totally agree with everything that was 00:04:07.790 --> 00:04:10.479 align:start position:0% I totally agree with everything that was just<00:04:07.819> said<00:04:08.060> and<00:04:08.840> I<00:04:09.199> sort<00:04:09.739> of<00:04:09.829> want<00:04:09.980> to<00:04:10.129> add<00:04:10.220> that 00:04:10.479 --> 00:04:10.489 align:start position:0% just said and I sort of want to add that 00:04:10.489 --> 00:04:12.580 align:start position:0% just said and I sort of want to add that you<00:04:10.549> can<00:04:10.909> have<00:04:11.060> good<00:04:11.359> or<00:04:11.569> bad<00:04:11.599> specifications 00:04:12.580 --> 00:04:12.590 align:start position:0% you can have good or bad specifications 00:04:12.590 --> 00:04:15.490 align:start position:0% you can have good or bad specifications in<00:04:12.829> any<00:04:13.220> format<00:04:13.609> so<00:04:14.109> absolutely<00:04:15.109> while<00:04:15.349> it's 00:04:15.490 --> 00:04:15.500 align:start position:0% in any format so absolutely while it's 00:04:15.500 --> 00:04:17.469 align:start position:0% in any format so absolutely while it's nice<00:04:15.680> to<00:04:15.889> have<00:04:16.010> a<00:04:16.039> specification<00:04:16.489> be<00:04:16.970> testable 00:04:17.469 --> 00:04:17.479 align:start position:0% nice to have a specification be testable 00:04:17.479 --> 00:04:20.020 align:start position:0% nice to have a specification be testable and<00:04:18.049> clear<00:04:18.530> and<00:04:18.889> readable<00:04:19.070> you<00:04:19.519> can<00:04:19.880> have 00:04:20.020 --> 00:04:20.030 align:start position:0% and clear and readable you can have 00:04:20.030 --> 00:04:21.729 align:start position:0% and clear and readable you can have really<00:04:20.299> really<00:04:20.630> good<00:04:20.780> at<00:04:20.959> Haskell<00:04:21.079> language 00:04:21.729 --> 00:04:21.739 align:start position:0% really really good at Haskell language 00:04:21.739 --> 00:04:23.409 align:start position:0% really really good at Haskell language specifications<00:04:22.460> or<00:04:22.760> you<00:04:22.880> can<00:04:23.000> have<00:04:23.180> pretty 00:04:23.409 --> 00:04:23.419 align:start position:0% specifications or you can have pretty 00:04:23.419 --> 00:04:26.290 align:start position:0% specifications or you can have pretty bad<00:04:23.599> Haskell<00:04:24.400> specifications<00:04:25.400> and<00:04:25.610> I've<00:04:25.969> even 00:04:26.290 --> 00:04:26.300 align:start position:0% bad Haskell specifications and I've even 00:04:26.300 --> 00:04:28.029 align:start position:0% bad Haskell specifications and I've even seen<00:04:26.510> English<00:04:26.930> language<00:04:27.289> specifications 00:04:28.029 --> 00:04:28.039 align:start position:0% seen English language specifications 00:04:28.039 --> 00:04:29.110 align:start position:0% seen English language specifications that<00:04:28.219> are<00:04:28.310> not<00:04:28.460> entirely 00:04:29.110 --> 00:04:29.120 align:start position:0% that are not entirely 00:04:29.120 --> 00:04:32.260 align:start position:0% that are not entirely so<00:04:29.860> sort<00:04:30.860> of<00:04:30.919> goes<00:04:31.250> more<00:04:31.520> to<00:04:31.669> the<00:04:31.699> expertise<00:04:32.240> of 00:04:32.260 --> 00:04:32.270 align:start position:0% so sort of goes more to the expertise of 00:04:32.270 --> 00:04:36.990 align:start position:0% so sort of goes more to the expertise of whoever's<00:04:32.750> implementing<00:04:33.260> it<00:04:33.350> I<00:04:33.440> think<00:04:34.060> great 00:04:36.990 --> 00:04:37.000 align:start position:0% whoever's implementing it I think great 00:04:37.000 --> 00:04:39.930 align:start position:0% whoever's implementing it I think great [Music] 00:04:39.930 --> 00:04:39.940 align:start position:0% [Music] 00:04:39.940 --> 00:04:43.659 align:start position:0% [Music] so<00:04:41.320> like<00:04:42.320> could<00:04:42.919> you<00:04:42.949> maybe<00:04:43.100> share<00:04:43.490> a<00:04:43.520> bit 00:04:43.659 --> 00:04:43.669 align:start position:0% so like could you maybe share a bit 00:04:43.669 --> 00:04:45.930 align:start position:0% so like could you maybe share a bit about<00:04:43.790> what<00:04:44.180> is<00:04:44.300> like<00:04:44.540> new<00:04:44.930> and<00:04:45.110> unique<00:04:45.260> about 00:04:45.930 --> 00:04:45.940 align:start position:0% about what is like new and unique about 00:04:45.940 --> 00:04:48.310 align:start position:0% about what is like new and unique about formally<00:04:46.940> verifying<00:04:47.360> smart<00:04:47.930> contracts 00:04:48.310 --> 00:04:48.320 align:start position:0% formally verifying smart contracts 00:04:48.320 --> 00:04:50.070 align:start position:0% formally verifying smart contracts blockchains 00:04:50.070 --> 00:04:50.080 align:start position:0% blockchains 00:04:50.080 --> 00:04:52.960 align:start position:0% blockchains kind<00:04:51.080> of<00:04:51.139> compared<00:04:51.470> to<00:04:51.620> you<00:04:52.490> know<00:04:52.580> safety 00:04:52.960 --> 00:04:52.970 align:start position:0% kind of compared to you know safety 00:04:52.970 --> 00:04:55.930 align:start position:0% kind of compared to you know safety critical<00:04:53.120> hardware<00:04:53.720> verification<00:04:54.260> and<00:04:54.979> what 00:04:55.930 --> 00:04:55.940 align:start position:0% critical hardware verification and what 00:04:55.940 --> 00:04:57.640 align:start position:0% critical hardware verification and what are<00:04:56.060> the<00:04:56.210> corresponding<00:04:56.440> opportunities<00:04:57.440> of 00:04:57.640 --> 00:04:57.650 align:start position:0% are the corresponding opportunities of 00:04:57.650 --> 00:05:01.210 align:start position:0% are the corresponding opportunities of it<00:04:58.600> you<00:04:59.600> know<00:04:59.750> what<00:04:59.900> is<00:05:00.020> new<00:05:00.260> and<00:05:00.440> unique<00:05:00.590> about 00:05:01.210 --> 00:05:01.220 align:start position:0% it you know what is new and unique about 00:05:01.220 --> 00:05:03.340 align:start position:0% it you know what is new and unique about formally<00:05:01.700> verifying<00:05:02.090> smart<00:05:02.840> contracts<00:05:03.290> or 00:05:03.340 --> 00:05:03.350 align:start position:0% formally verifying smart contracts or 00:05:03.350 --> 00:05:05.050 align:start position:0% formally verifying smart contracts or blockchains<00:05:03.830> compared<00:05:04.400> to<00:05:04.550> like<00:05:04.700> for<00:05:05.000> example 00:05:05.050 --> 00:05:05.060 align:start position:0% blockchains compared to like for example 00:05:05.060 --> 00:05:08.020 align:start position:0% blockchains compared to like for example verifying<00:05:05.660> hardware<00:05:06.400> and<00:05:07.400> what<00:05:07.580> are<00:05:07.880> the 00:05:08.020 --> 00:05:08.030 align:start position:0% verifying hardware and what are the 00:05:08.030 --> 00:05:13.480 align:start position:0% verifying hardware and what are the opportunities<00:05:08.180> of<00:05:08.660> it<00:05:08.780> I<00:05:10.419> guess<00:05:12.490> smart 00:05:13.480 --> 00:05:13.490 align:start position:0% opportunities of it I guess smart 00:05:13.490 --> 00:05:16.210 align:start position:0% opportunities of it I guess smart contracts<00:05:13.790> has<00:05:13.940> a<00:05:13.970> new<00:05:15.070> sort<00:05:16.070> of<00:05:16.100> play 00:05:16.210 --> 00:05:16.220 align:start position:0% contracts has a new sort of play 00:05:16.220 --> 00:05:18.520 align:start position:0% contracts has a new sort of play semantics<00:05:16.700> right<00:05:16.940> so<00:05:17.300> we<00:05:17.450> have<00:05:17.570> a<00:05:17.600> concept<00:05:18.050> and 00:05:18.520 --> 00:05:18.530 align:start position:0% semantics right so we have a concept and 00:05:18.530 --> 00:05:21.279 align:start position:0% semantics right so we have a concept and action<00:05:18.889> at<00:05:19.580> the<00:05:19.700> conservative<00:05:20.210> gas<00:05:20.419> and<00:05:20.810> solid 00:05:21.279 --> 00:05:21.289 align:start position:0% action at the conservative gas and solid 00:05:21.289 --> 00:05:25.300 align:start position:0% action at the conservative gas and solid token<00:05:21.650> heater<00:05:22.960> which<00:05:23.960> you<00:05:24.200> know<00:05:24.320> doesn't 00:05:25.300 --> 00:05:25.310 align:start position:0% token heater which you know doesn't 00:05:25.310 --> 00:05:27.370 align:start position:0% token heater which you know doesn't exist<00:05:25.370> in<00:05:25.789> in<00:05:26.180> you<00:05:26.539> know<00:05:26.570> existing<00:05:27.050> system 00:05:27.370 --> 00:05:27.380 align:start position:0% exist in in you know existing system 00:05:27.380 --> 00:05:29.800 align:start position:0% exist in in you know existing system like<00:05:27.620> you<00:05:27.830> know<00:05:27.919> critical<00:05:28.630> hardware<00:05:29.630> or 00:05:29.800 --> 00:05:29.810 align:start position:0% like you know critical hardware or 00:05:29.810 --> 00:05:32.830 align:start position:0% like you know critical hardware or software<00:05:29.840> system<00:05:31.449> so<00:05:32.449> when<00:05:32.600> you<00:05:32.720> really 00:05:32.830 --> 00:05:32.840 align:start position:0% software system so when you really 00:05:32.840 --> 00:05:35.020 align:start position:0% software system so when you really formally<00:05:33.560> verified<00:05:33.590> I<00:05:34.250> think<00:05:34.550> you<00:05:34.669> you<00:05:34.910> need 00:05:35.020 --> 00:05:35.030 align:start position:0% formally verified I think you you need 00:05:35.030 --> 00:05:36.490 align:start position:0% formally verified I think you you need literally<00:05:35.330> find<00:05:35.570> new<00:05:35.720> property<00:05:36.169> that<00:05:36.380> you 00:05:36.490 --> 00:05:36.500 align:start position:0% literally find new property that you 00:05:36.500 --> 00:05:38.890 align:start position:0% literally find new property that you want<00:05:36.530> to<00:05:36.740> verify<00:05:36.889> that<00:05:37.729> only<00:05:38.030> exists<00:05:38.479> in<00:05:38.630> you 00:05:38.890 --> 00:05:38.900 align:start position:0% want to verify that only exists in you 00:05:38.900 --> 00:05:43.020 align:start position:0% want to verify that only exists in you know<00:05:38.990> smart<00:05:39.289> contract<00:05:39.650> and<00:05:39.889> also<00:05:40.310> it<00:05:41.210> Orion 00:05:43.020 --> 00:05:43.030 align:start position:0% know smart contract and also it Orion 00:05:43.030 --> 00:05:45.040 align:start position:0% know smart contract and also it Orion there's<00:05:44.030> definitely<00:05:44.479> some<00:05:44.630> really<00:05:44.870> nice 00:05:45.040 --> 00:05:45.050 align:start position:0% there's definitely some really nice 00:05:45.050 --> 00:05:47.320 align:start position:0% there's definitely some really nice things<00:05:45.380> about<00:05:45.500> smart<00:05:45.979> contracts<00:05:46.400> they<00:05:47.270> are 00:05:47.320 --> 00:05:47.330 align:start position:0% things about smart contracts they are 00:05:47.330 --> 00:05:49.779 align:start position:0% things about smart contracts they are bounded<00:05:48.020> in<00:05:48.260> terms<00:05:48.530> of<00:05:48.740> their<00:05:48.889> execution<00:05:49.280> time 00:05:49.779 --> 00:05:49.789 align:start position:0% bounded in terms of their execution time 00:05:49.789 --> 00:05:51.909 align:start position:0% bounded in terms of their execution time there<00:05:50.419> are<00:05:50.510> generally<00:05:50.960> very<00:05:51.200> small<00:05:51.590> simple 00:05:51.909 --> 00:05:51.919 align:start position:0% there are generally very small simple 00:05:51.919 --> 00:05:53.890 align:start position:0% there are generally very small simple programs<00:05:52.490> at<00:05:53.030> least<00:05:53.090> compared<00:05:53.599> to<00:05:53.660> something 00:05:53.890 --> 00:05:53.900 align:start position:0% programs at least compared to something 00:05:53.900 --> 00:05:56.110 align:start position:0% programs at least compared to something you'd<00:05:54.110> see<00:05:54.349> in<00:05:54.380> a<00:05:54.830> safety<00:05:55.250> critical<00:05:55.370> system<00:05:55.940> a 00:05:56.110 --> 00:05:56.120 align:start position:0% you'd see in a safety critical system a 00:05:56.120 --> 00:05:57.670 align:start position:0% you'd see in a safety critical system a car<00:05:56.300> or<00:05:56.599> an<00:05:56.720> airplane<00:05:56.840> or<00:05:57.289> something<00:05:57.320> like 00:05:57.670 --> 00:05:57.680 align:start position:0% car or an airplane or something like 00:05:57.680 --> 00:06:00.190 align:start position:0% car or an airplane or something like that<00:05:57.940> and<00:05:58.940> they<00:05:59.270> directly<00:05:59.690> handle<00:05:59.990> large 00:06:00.190 --> 00:06:00.200 align:start position:0% that and they directly handle large 00:06:00.200 --> 00:06:02.230 align:start position:0% that and they directly handle large quantities<00:06:00.680> of<00:06:00.710> money<00:06:01.010> so<00:06:01.610> actually<00:06:02.120> I'm 00:06:02.230 --> 00:06:02.240 align:start position:0% quantities of money so actually I'm 00:06:02.240 --> 00:06:04.180 align:start position:0% quantities of money so actually I'm really<00:06:02.419> excited<00:06:02.720> I<00:06:02.960> think<00:06:03.020> that<00:06:03.380> I<00:06:03.620> said<00:06:04.070> this 00:06:04.180 --> 00:06:04.190 align:start position:0% really excited I think that I said this 00:06:04.190 --> 00:06:05.740 align:start position:0% really excited I think that I said this last<00:06:04.370> year<00:06:04.639> and<00:06:04.789> I<00:06:04.849> still<00:06:05.030> strongly<00:06:05.389> believe 00:06:05.740 --> 00:06:05.750 align:start position:0% last year and I still strongly believe 00:06:05.750 --> 00:06:07.450 align:start position:0% last year and I still strongly believe it<00:06:05.930> that<00:06:06.110> as<00:06:06.289> a<00:06:06.320> space<00:06:06.710> we<00:06:06.979> have<00:06:07.190> an 00:06:07.450 --> 00:06:07.460 align:start position:0% it that as a space we have an 00:06:07.460 --> 00:06:09.760 align:start position:0% it that as a space we have an opportunity<00:06:08.030> to<00:06:08.240> set<00:06:08.450> standards<00:06:09.229> for<00:06:09.380> how 00:06:09.760 --> 00:06:09.770 align:start position:0% opportunity to set standards for how 00:06:09.770 --> 00:06:11.500 align:start position:0% opportunity to set standards for how software<00:06:10.160> is<00:06:10.280> developed<00:06:10.430> even<00:06:10.820> beyond<00:06:11.240> block 00:06:11.500 --> 00:06:11.510 align:start position:0% software is developed even beyond block 00:06:11.510 --> 00:06:14.200 align:start position:0% software is developed even beyond block chains<00:06:11.780> and<00:06:11.930> smart<00:06:12.200> contracts<00:06:13.060> because<00:06:14.060> I 00:06:14.200 --> 00:06:14.210 align:start position:0% chains and smart contracts because I 00:06:14.210 --> 00:06:16.330 align:start position:0% chains and smart contracts because I think<00:06:14.360> the<00:06:14.690> users<00:06:15.020> of<00:06:15.349> smart<00:06:15.770> contracts<00:06:16.160> and 00:06:16.330 --> 00:06:16.340 align:start position:0% think the users of smart contracts and 00:06:16.340 --> 00:06:17.440 align:start position:0% think the users of smart contracts and block<00:06:16.490> chains<00:06:16.760> have<00:06:16.940> a<00:06:16.970> much<00:06:17.210> stronger 00:06:17.440 --> 00:06:17.450 align:start position:0% block chains have a much stronger 00:06:17.450 --> 00:06:19.240 align:start position:0% block chains have a much stronger understanding<00:06:17.810> and<00:06:18.380> demand<00:06:18.680> for<00:06:18.889> this<00:06:19.010> kind 00:06:19.240 --> 00:06:19.250 align:start position:0% understanding and demand for this kind 00:06:19.250 --> 00:06:21.430 align:start position:0% understanding and demand for this kind of<00:06:19.310> technology<00:06:19.490> than<00:06:20.090> the<00:06:20.539> users<00:06:20.810> of<00:06:20.930> a<00:06:21.020> car<00:06:21.200> or 00:06:21.430 --> 00:06:21.440 align:start position:0% of technology than the users of a car or 00:06:21.440 --> 00:06:28.600 align:start position:0% of technology than the users of a car or something<00:06:21.889> like<00:06:21.979> that<00:06:23.919> so<00:06:26.500> it's<00:06:27.500> room<00:06:27.770> torture 00:06:28.600 --> 00:06:28.610 align:start position:0% something like that so it's room torture 00:06:28.610 --> 00:06:33.820 align:start position:0% something like that so it's room torture machine<00:06:28.760> has<00:06:29.090> no<00:06:29.440> non<00:06:30.440> determined<00:06:32.830> behaviors 00:06:33.820 --> 00:06:33.830 align:start position:0% machine has no non determined behaviors 00:06:33.830 --> 00:06:36.670 align:start position:0% machine has no non determined behaviors no<00:06:34.370> not<00:06:34.580> defined<00:06:34.849> behaviors<00:06:35.419> because<00:06:36.380> that 00:06:36.670 --> 00:06:36.680 align:start position:0% no not defined behaviors because that 00:06:36.680 --> 00:06:41.150 align:start position:0% no not defined behaviors because that means<00:06:37.070> consensus<00:06:37.940> folks<00:06:39.070> so 00:06:41.150 --> 00:06:41.160 align:start position:0% means consensus folks so 00:06:41.160 --> 00:06:44.600 align:start position:0% means consensus folks so so<00:06:41.940> this<00:06:42.260> possibility<00:06:43.260> of<00:06:43.400> different<00:06:44.400> clients 00:06:44.600 --> 00:06:44.610 align:start position:0% so this possibility of different clients 00:06:44.610 --> 00:06:46.550 align:start position:0% so this possibility of different clients following<00:06:45.240> different<00:06:45.570> folks<00:06:45.840> is<00:06:46.140> a<00:06:46.170> huge 00:06:46.550 --> 00:06:46.560 align:start position:0% following different folks is a huge 00:06:46.560 --> 00:06:50.480 align:start position:0% following different folks is a huge problem<00:06:46.830> but<00:06:47.640> it's<00:06:47.900> really<00:06:48.900> bracing<00:06:49.740> for<00:06:50.190> us 00:06:50.480 --> 00:06:50.490 align:start position:0% problem but it's really bracing for us 00:06:50.490 --> 00:06:52.880 align:start position:0% problem but it's really bracing for us on<00:06:51.270> top<00:06:51.540> of<00:06:51.780> the<00:06:51.960> virtual<00:06:52.230> machine<00:06:52.530> because 00:06:52.880 --> 00:06:52.890 align:start position:0% on top of the virtual machine because 00:06:52.890 --> 00:06:55.010 align:start position:0% on top of the virtual machine because that<00:06:53.130> means<00:06:53.310> the<00:06:53.610> specification<00:06:54.360> is<00:06:54.510> really 00:06:55.010 --> 00:06:55.020 align:start position:0% that means the specification is really 00:06:55.020 --> 00:06:58.670 align:start position:0% that means the specification is really always<00:06:55.200> deterministic<00:06:57.110> that's<00:06:58.110> a<00:06:58.440> huge 00:06:58.670 --> 00:06:58.680 align:start position:0% always deterministic that's a huge 00:06:58.680 --> 00:07:01.310 align:start position:0% always deterministic that's a huge improvement<00:06:59.130> over<00:06:59.390> proving<00:07:00.390> anything<00:07:00.780> over 00:07:01.310 --> 00:07:01.320 align:start position:0% improvement over proving anything over 00:07:01.320 --> 00:07:07.510 align:start position:0% improvement over proving anything over intelligible<00:07:02.130> so<00:07:02.400> our<00:07:02.550> cheapest<00:07:04.700> Thanks 00:07:07.510 --> 00:07:07.520 align:start position:0% intelligible so our cheapest Thanks 00:07:07.520 --> 00:07:09.890 align:start position:0% intelligible so our cheapest Thanks pretty<00:07:08.520> much<00:07:08.610> agree<00:07:08.910> with<00:07:09.210> what<00:07:09.450> people<00:07:09.690> said 00:07:09.890 --> 00:07:09.900 align:start position:0% pretty much agree with what people said 00:07:09.900 --> 00:07:11.390 align:start position:0% pretty much agree with what people said the<00:07:10.170> non<00:07:10.320> determinism<00:07:10.770> makes<00:07:11.010> it<00:07:11.130> easy<00:07:11.280> to 00:07:11.390 --> 00:07:11.400 align:start position:0% the non determinism makes it easy to 00:07:11.400 --> 00:07:13.520 align:start position:0% the non determinism makes it easy to bound<00:07:11.640> it<00:07:11.760> gas<00:07:11.970> makes<00:07:12.510> it<00:07:12.690> kind<00:07:13.320> of<00:07:13.380> nice 00:07:13.520 --> 00:07:13.530 align:start position:0% bound it gas makes it kind of nice 00:07:13.530 --> 00:07:14.870 align:start position:0% bound it gas makes it kind of nice although<00:07:13.860> sometimes<00:07:14.070> it's<00:07:14.430> hard<00:07:14.610> to<00:07:14.700> reason 00:07:14.870 --> 00:07:14.880 align:start position:0% although sometimes it's hard to reason 00:07:14.880 --> 00:07:16.670 align:start position:0% although sometimes it's hard to reason about<00:07:15.030> exactly<00:07:15.570> how<00:07:15.810> much<00:07:15.930> gas<00:07:16.110> the<00:07:16.290> contract 00:07:16.670 --> 00:07:16.680 align:start position:0% about exactly how much gas the contract 00:07:16.680 --> 00:07:20.510 align:start position:0% about exactly how much gas the contract will<00:07:16.800> use<00:07:17.270> and<00:07:18.270> basically<00:07:19.130> you<00:07:20.130> know<00:07:20.250> what's 00:07:20.510 --> 00:07:20.520 align:start position:0% will use and basically you know what's 00:07:20.520 --> 00:07:22.640 align:start position:0% will use and basically you know what's making<00:07:20.820> the<00:07:21.690> most<00:07:21.870> driving<00:07:22.260> force<00:07:22.470> behind 00:07:22.640 --> 00:07:22.650 align:start position:0% making the most driving force behind 00:07:22.650 --> 00:07:25.070 align:start position:0% making the most driving force behind this<00:07:22.980> is<00:07:23.280> the<00:07:23.310> amount<00:07:23.640> of<00:07:23.760> money<00:07:23.910> being<00:07:24.180> at 00:07:25.070 --> 00:07:25.080 align:start position:0% this is the amount of money being at 00:07:25.080 --> 00:07:27.050 align:start position:0% this is the amount of money being at stake<00:07:25.380> essentially<00:07:25.980> as<00:07:26.460> opposed<00:07:26.760> to<00:07:26.880> just 00:07:27.050 --> 00:07:27.060 align:start position:0% stake essentially as opposed to just 00:07:27.060 --> 00:07:30.650 align:start position:0% stake essentially as opposed to just normal<00:07:27.390> programs<00:07:27.870> in<00:07:28.320> other<00:07:28.860> settings<00:07:29.480> let<00:07:30.480> me 00:07:30.650 --> 00:07:30.660 align:start position:0% normal programs in other settings let me 00:07:30.660 --> 00:07:34.250 align:start position:0% normal programs in other settings let me move<00:07:30.810> over<00:07:30.990> because<00:07:31.560> a<00:07:32.130> course<00:07:32.510> really<00:07:33.510> equals 00:07:34.250 --> 00:07:34.260 align:start position:0% move over because a course really equals 00:07:34.260 --> 00:07:36.520 align:start position:0% move over because a course really equals to<00:07:34.320> make<00:07:34.500> it<00:07:34.680> really<00:07:34.980> hard<00:07:35.010> hard<00:07:35.790> for<00:07:36.000> me<00:07:36.090> to 00:07:36.520 --> 00:07:36.530 align:start position:0% to make it really hard hard for me to 00:07:36.530 --> 00:07:41.330 align:start position:0% to make it really hard hard for me to understand<00:07:37.530> the<00:07:37.590> question<00:07:39.860> yeah<00:07:40.860> it's<00:07:41.040> it's 00:07:41.330 --> 00:07:41.340 align:start position:0% understand the question yeah it's it's 00:07:41.340 --> 00:07:42.740 align:start position:0% understand the question yeah it's it's kind<00:07:41.520> of<00:07:41.580> interesting<00:07:41.820> how<00:07:42.120> people<00:07:42.150> care<00:07:42.720> a 00:07:42.740 --> 00:07:42.750 align:start position:0% kind of interesting how people care a 00:07:42.750 --> 00:07:44.210 align:start position:0% kind of interesting how people care a little<00:07:42.900> bit<00:07:43.110> more<00:07:43.320> about<00:07:43.530> money<00:07:43.830> than<00:07:44.070> their 00:07:44.210 --> 00:07:44.220 align:start position:0% little bit more about money than their 00:07:44.220 --> 00:07:45.920 align:start position:0% little bit more about money than their lives<00:07:44.430> right<00:07:44.820> you<00:07:45.210> have<00:07:45.360> someone<00:07:45.690> lose<00:07:45.900> their 00:07:45.920 --> 00:07:45.930 align:start position:0% lives right you have someone lose their 00:07:45.930 --> 00:07:48.050 align:start position:0% lives right you have someone lose their fifty<00:07:46.710> thousand<00:07:47.100> endow<00:07:47.310> tokens<00:07:47.790> and<00:07:47.940> they're 00:07:48.050 --> 00:07:48.060 align:start position:0% fifty thousand endow tokens and they're 00:07:48.060 --> 00:07:50.270 align:start position:0% fifty thousand endow tokens and they're clamoring<00:07:48.240> for<00:07:48.720> formal<00:07:48.990> verification<00:07:49.280> but 00:07:50.270 --> 00:07:50.280 align:start position:0% clamoring for formal verification but 00:07:50.280 --> 00:07:52.190 align:start position:0% clamoring for formal verification but then<00:07:50.430> Toyota<00:07:50.850> has<00:07:51.060> an<00:07:51.300> issue<00:07:51.420> in<00:07:51.600> their<00:07:51.690> ECU's 00:07:52.190 --> 00:07:52.200 align:start position:0% then Toyota has an issue in their ECU's 00:07:52.200 --> 00:07:54.290 align:start position:0% then Toyota has an issue in their ECU's that<00:07:52.500> kills<00:07:52.740> 20<00:07:52.980> people<00:07:53.340> and<00:07:53.730> Toyota 00:07:54.290 --> 00:07:54.300 align:start position:0% that kills 20 people and Toyota 00:07:54.300 --> 00:07:56.000 align:start position:0% that kills 20 people and Toyota customers<00:07:54.720> could<00:07:54.960> not<00:07:55.110> care<00:07:55.320> less<00:07:55.350> about<00:07:55.590> the 00:07:56.000 --> 00:07:56.010 align:start position:0% customers could not care less about the 00:07:56.010 --> 00:07:58.760 align:start position:0% customers could not care less about the software<00:07:56.310> in<00:07:56.430> their<00:07:56.550> car<00:07:57.050> so<00:07:58.050> I<00:07:58.410> just<00:07:58.590> think 00:07:58.760 --> 00:07:58.770 align:start position:0% software in their car so I just think 00:07:58.770 --> 00:07:59.480 align:start position:0% software in their car so I just think that's<00:07:58.860> kind<00:07:59.190> of<00:07:59.250> an<00:07:59.370> interesting 00:07:59.480 --> 00:07:59.490 align:start position:0% that's kind of an interesting 00:07:59.490 --> 00:08:02.450 align:start position:0% that's kind of an interesting observation<00:07:59.910> on<00:08:00.330> humanity<00:08:01.070> it<00:08:02.070> is<00:08:02.190> kind<00:08:02.430> of 00:08:02.450 --> 00:08:02.460 align:start position:0% observation on humanity it is kind of 00:08:02.460 --> 00:08:06.530 align:start position:0% observation on humanity it is kind of interesting<00:08:02.669> yeah<00:08:04.310> right<00:08:05.340> so<00:08:05.640> could<00:08:06.480> you 00:08:06.530 --> 00:08:06.540 align:start position:0% interesting yeah right so could you 00:08:06.540 --> 00:08:08.690 align:start position:0% interesting yeah right so could you maybe<00:08:06.600> talk<00:08:07.140> a<00:08:07.200> bit<00:08:07.440> about<00:08:07.470> the<00:08:08.130> limitations 00:08:08.690 --> 00:08:08.700 align:start position:0% maybe talk a bit about the limitations 00:08:08.700 --> 00:08:10.850 align:start position:0% maybe talk a bit about the limitations and<00:08:08.850> challenging<00:08:09.510> challenges<00:08:10.470> so<00:08:10.650> for 00:08:10.850 --> 00:08:10.860 align:start position:0% and challenging challenges so for 00:08:10.860 --> 00:08:13.420 align:start position:0% and challenging challenges so for modification<00:08:11.580> and<00:08:11.760> maybe<00:08:12.360> also<00:08:12.810> like 00:08:13.420 --> 00:08:13.430 align:start position:0% modification and maybe also like 00:08:13.430 --> 00:08:15.380 align:start position:0% modification and maybe also like introduced<00:08:14.430> the<00:08:14.820> project<00:08:15.150> that<00:08:15.270> you're 00:08:15.380 --> 00:08:15.390 align:start position:0% introduced the project that you're 00:08:15.390 --> 00:08:17.300 align:start position:0% introduced the project that you're involved<00:08:15.750> with<00:08:15.990> and<00:08:16.290> how<00:08:16.410> your<00:08:16.590> project<00:08:16.860> kind 00:08:17.300 --> 00:08:17.310 align:start position:0% involved with and how your project kind 00:08:17.310 --> 00:08:22.990 align:start position:0% involved with and how your project kind of<00:08:17.400> tries<00:08:17.790> to<00:08:17.970> make<00:08:18.120> things<00:08:18.480> easier<00:08:18.870> or<00:08:18.990> better 00:08:22.990 --> 00:08:23.000 align:start position:0% 00:08:23.000 --> 00:08:26.840 align:start position:0% so<00:08:24.110> my<00:08:25.110> background<00:08:25.980> the<00:08:26.070> interactive<00:08:26.580> theorem 00:08:26.840 --> 00:08:26.850 align:start position:0% so my background the interactive theorem 00:08:26.850 --> 00:08:31.570 align:start position:0% so my background the interactive theorem proving<00:08:27.240> is<00:08:27.510> not<00:08:27.960> user<00:08:28.740> friendly<00:08:29.690> so<00:08:30.690> take 00:08:31.570 --> 00:08:31.580 align:start position:0% proving is not user friendly so take 00:08:31.580 --> 00:08:34.779 align:start position:0% proving is not user friendly so take class<00:08:32.580> of<00:08:32.849> computer<00:08:33.300> science<00:08:33.599> students<00:08:34.289> of 00:08:34.779 --> 00:08:34.789 align:start position:0% class of computer science students of 00:08:34.789 --> 00:08:38.209 align:start position:0% class of computer science students of thirty<00:08:35.789> people<00:08:36.060> maybe<00:08:37.050> a<00:08:37.530> couple<00:08:37.830> of<00:08:38.010> them 00:08:38.209 --> 00:08:38.219 align:start position:0% thirty people maybe a couple of them 00:08:38.219 --> 00:08:40.190 align:start position:0% thirty people maybe a couple of them willing<00:08:38.669> to<00:08:39.000> use<00:08:39.210> interactive<00:08:39.690> theorem 00:08:40.190 --> 00:08:40.200 align:start position:0% willing to use interactive theorem 00:08:40.200 --> 00:08:42.800 align:start position:0% willing to use interactive theorem provers<00:08:40.590> maybe<00:08:41.490> only<00:08:41.849> one<00:08:42.030> of<00:08:42.210> them<00:08:42.360> can 00:08:42.800 --> 00:08:42.810 align:start position:0% provers maybe only one of them can 00:08:42.810 --> 00:08:46.820 align:start position:0% provers maybe only one of them can finish<00:08:43.289> verifying<00:08:43.950> a<00:08:44.370> program<00:08:44.790> of<00:08:45.000> like<00:08:45.830> 2030 00:08:46.820 --> 00:08:46.830 align:start position:0% finish verifying a program of like 2030 00:08:46.830 --> 00:08:48.680 align:start position:0% finish verifying a program of like 2030 times 00:08:48.680 --> 00:08:48.690 align:start position:0% times 00:08:48.690 --> 00:08:52.100 align:start position:0% times in<00:08:49.079> the<00:08:49.560> month<00:08:49.769> also<00:08:50.720> so<00:08:51.720> it's<00:08:51.870> kind<00:08:52.050> of 00:08:52.100 --> 00:08:52.110 align:start position:0% in the month also so it's kind of 00:08:52.110 --> 00:08:58.309 align:start position:0% in the month also so it's kind of challenging<00:08:53.750> actually<00:08:56.690> verifying<00:08:57.690> software 00:08:58.309 --> 00:08:58.319 align:start position:0% challenging actually verifying software 00:08:58.319 --> 00:09:00.259 align:start position:0% challenging actually verifying software using<00:08:58.889> these<00:08:59.009> interactive<00:08:59.610> theorem<00:08:59.879> provers 00:09:00.259 --> 00:09:00.269 align:start position:0% using these interactive theorem provers 00:09:00.269 --> 00:09:05.329 align:start position:0% using these interactive theorem provers is<00:09:00.540> so<00:09:01.259> challenging<00:09:01.440> that<00:09:01.889> I<00:09:01.949> don't<00:09:02.670> see<00:09:04.339> much 00:09:05.329 --> 00:09:05.339 align:start position:0% is so challenging that I don't see much 00:09:05.339 --> 00:09:09.199 align:start position:0% is so challenging that I don't see much I<00:09:05.639> don't<00:09:05.819> see<00:09:06.259> many<00:09:07.339> successful<00:09:08.339> applications 00:09:09.199 --> 00:09:09.209 align:start position:0% I don't see many successful applications 00:09:09.209 --> 00:09:13.189 align:start position:0% I don't see many successful applications so<00:09:09.769> but<00:09:10.769> for<00:09:11.160> the<00:09:11.250> reasons<00:09:11.610> described<00:09:12.199> before 00:09:13.189 --> 00:09:13.199 align:start position:0% so but for the reasons described before 00:09:13.199 --> 00:09:15.889 align:start position:0% so but for the reasons described before I<00:09:13.230> believe<00:09:13.889> in<00:09:14.370> a<00:09:14.550> theorem<00:09:14.819> it<00:09:15.000> might<00:09:15.509> still 00:09:15.889 --> 00:09:15.899 align:start position:0% I believe in a theorem it might still 00:09:15.899 --> 00:09:20.749 align:start position:0% I believe in a theorem it might still make<00:09:16.110> sense<00:09:16.410> I<00:09:18.949> guess<00:09:19.949> you<00:09:20.160> know<00:09:20.250> it's<00:09:20.459> really 00:09:20.749 --> 00:09:20.759 align:start position:0% make sense I guess you know it's really 00:09:20.759 --> 00:09:23.059 align:start position:0% make sense I guess you know it's really hardly<00:09:21.029> to<00:09:21.240> formally<00:09:21.779> prove<00:09:22.439> you<00:09:22.949> know 00:09:23.059 --> 00:09:23.069 align:start position:0% hardly to formally prove you know 00:09:23.069 --> 00:09:25.579 align:start position:0% hardly to formally prove you know existing<00:09:23.879> smart<00:09:24.149> contract<00:09:24.540> especially<00:09:25.079> the 00:09:25.579 --> 00:09:25.589 align:start position:0% existing smart contract especially the 00:09:25.589 --> 00:09:28.009 align:start position:0% existing smart contract especially the complicated<00:09:26.459> one<00:09:26.699> because<00:09:27.360> you<00:09:27.720> know<00:09:27.810> first 00:09:28.009 --> 00:09:28.019 align:start position:0% complicated one because you know first 00:09:28.019 --> 00:09:30.499 align:start position:0% complicated one because you know first of<00:09:28.139> all<00:09:28.230> you<00:09:28.290> need<00:09:28.560> like<00:09:28.769> to<00:09:29.329> represent<00:09:30.329> them 00:09:30.499 --> 00:09:30.509 align:start position:0% of all you need like to represent them 00:09:30.509 --> 00:09:32.749 align:start position:0% of all you need like to represent them in<00:09:30.660> some<00:09:30.949> mathematical<00:09:31.949> model<00:09:32.250> that<00:09:32.490> you<00:09:32.610> can 00:09:32.749 --> 00:09:32.759 align:start position:0% in some mathematical model that you can 00:09:32.759 --> 00:09:35.300 align:start position:0% in some mathematical model that you can easily<00:09:32.939> prove<00:09:33.449> some<00:09:33.839> property<00:09:34.199> later<00:09:34.410> on<00:09:34.560> but 00:09:35.300 --> 00:09:35.310 align:start position:0% easily prove some property later on but 00:09:35.310 --> 00:09:37.480 align:start position:0% easily prove some property later on but you<00:09:35.519> know<00:09:35.610> it's<00:09:35.790> really<00:09:35.850> hardly<00:09:36.449> to<00:09:36.629> you<00:09:36.959> know 00:09:37.480 --> 00:09:37.490 align:start position:0% you know it's really hardly to you know 00:09:37.490 --> 00:09:40.910 align:start position:0% you know it's really hardly to you know you<00:09:38.490> know<00:09:38.579> convert<00:09:39.540> or<00:09:39.750> transfer<00:09:40.110> or<00:09:40.439> you<00:09:40.800> know 00:09:40.910 --> 00:09:40.920 align:start position:0% you know convert or transfer or you know 00:09:40.920 --> 00:09:42.740 align:start position:0% you know convert or transfer or you know interpret<00:09:41.670> the<00:09:41.850> program<00:09:42.180> into<00:09:42.509> the<00:09:42.629> new 00:09:42.740 --> 00:09:42.750 align:start position:0% interpret the program into the new 00:09:42.750 --> 00:09:44.809 align:start position:0% interpret the program into the new language<00:09:43.259> or<00:09:43.589> the<00:09:43.889> new<00:09:44.009> model<00:09:44.279> because<00:09:44.639> of<00:09:44.670> the 00:09:44.809 --> 00:09:44.819 align:start position:0% language or the new model because of the 00:09:44.819 --> 00:09:47.240 align:start position:0% language or the new model because of the you<00:09:45.420> know<00:09:45.449> compare<00:09:45.870> compatibility<00:09:46.649> issues 00:09:47.240 --> 00:09:47.250 align:start position:0% you know compare compatibility issues 00:09:47.250 --> 00:09:49.790 align:start position:0% you know compare compatibility issues right<00:09:47.670> and<00:09:47.939> also<00:09:48.779> sometimes<00:09:49.050> you<00:09:49.319> cannot<00:09:49.589> even 00:09:49.790 --> 00:09:49.800 align:start position:0% right and also sometimes you cannot even 00:09:49.800 --> 00:09:51.619 align:start position:0% right and also sometimes you cannot even explore<00:09:50.339> all<00:09:50.610> the<00:09:50.730> possible 00:09:51.619 --> 00:09:51.629 align:start position:0% explore all the possible 00:09:51.629 --> 00:09:54.530 align:start position:0% explore all the possible you<00:09:52.079> know<00:09:52.310> outcomes<00:09:53.310> or<00:09:53.550> in<00:09:53.910> properties<00:09:54.329> of 00:09:54.530 --> 00:09:54.540 align:start position:0% you know outcomes or in properties of 00:09:54.540 --> 00:09:58.309 align:start position:0% you know outcomes or in properties of the<00:09:54.660> program<00:09:55.610> and<00:09:56.839> you<00:09:57.839> know<00:09:57.930> most<00:09:58.170> of<00:09:58.259> the 00:09:58.309 --> 00:09:58.319 align:start position:0% the program and you know most of the 00:09:58.319 --> 00:10:00.710 align:start position:0% the program and you know most of the formal<00:09:59.040> verification<00:09:59.250> true<00:09:59.790> requires<00:10:00.420> you 00:10:00.710 --> 00:10:00.720 align:start position:0% formal verification true requires you 00:10:00.720 --> 00:10:03.350 align:start position:0% formal verification true requires you know<00:10:00.870> a<00:10:01.470> strong<00:10:02.100> background<00:10:02.399> and<00:10:02.759> and<00:10:03.120> you 00:10:03.350 --> 00:10:03.360 align:start position:0% know a strong background and and you 00:10:03.360 --> 00:10:06.530 align:start position:0% know a strong background and and you know<00:10:03.509> human<00:10:04.470> involved<00:10:04.860> right<00:10:05.100> and<00:10:05.360> most<00:10:06.360> of 00:10:06.530 --> 00:10:06.540 align:start position:0% know human involved right and most of 00:10:06.540 --> 00:10:09.860 align:start position:0% know human involved right and most of the<00:10:06.630> project<00:10:07.110> and<00:10:08.120> companies<00:10:09.120> do<00:10:09.449> not<00:10:09.689> have 00:10:09.860 --> 00:10:09.870 align:start position:0% the project and companies do not have 00:10:09.870 --> 00:10:13.879 align:start position:0% the project and companies do not have these<00:10:10.259> you<00:10:10.560> know<00:10:10.589> people<00:10:10.699> so<00:10:12.649> so<00:10:13.649> you<00:10:13.860> know 00:10:13.879 --> 00:10:13.889 align:start position:0% these you know people so so you know 00:10:13.889 --> 00:10:16.009 align:start position:0% these you know people so so you know we're<00:10:14.189> really<00:10:14.759> like<00:10:15.060> we<00:10:15.240> we<00:10:15.480> need<00:10:15.660> like<00:10:15.839> some 00:10:16.009 --> 00:10:16.019 align:start position:0% we're really like we we need like some 00:10:16.019 --> 00:10:19.699 align:start position:0% we're really like we we need like some sort<00:10:16.199> of<00:10:16.259> like<00:10:16.470> you<00:10:17.750> user-friendly<00:10:18.750> developer 00:10:19.699 --> 00:10:19.709 align:start position:0% sort of like you user-friendly developer 00:10:19.709 --> 00:10:23.090 align:start position:0% sort of like you user-friendly developer tool<00:10:19.980> so<00:10:20.519> that<00:10:20.550> you<00:10:20.730> know<00:10:21.589> you<00:10:22.589> can<00:10:22.740> just<00:10:22.889> like 00:10:23.090 --> 00:10:23.100 align:start position:0% tool so that you know you can just like 00:10:23.100 --> 00:10:24.679 align:start position:0% tool so that you know you can just like run<00:10:23.310> the<00:10:23.459> tool<00:10:23.639> with<00:10:23.819> some<00:10:24.029> existing<00:10:24.509> smart 00:10:24.679 --> 00:10:24.689 align:start position:0% run the tool with some existing smart 00:10:24.689 --> 00:10:26.809 align:start position:0% run the tool with some existing smart contract<00:10:25.079> and<00:10:25.230> it<00:10:25.350> will<00:10:25.560> produce<00:10:25.800> other<00:10:26.189> or 00:10:26.809 --> 00:10:26.819 align:start position:0% contract and it will produce other or 00:10:26.819 --> 00:10:30.939 align:start position:0% contract and it will produce other or the<00:10:27.180> headphone<00:10:27.899> output<00:10:28.310> for<00:10:29.310> the<00:10:29.399> developers 00:10:30.939 --> 00:10:30.949 align:start position:0% the headphone output for the developers 00:10:30.949 --> 00:10:34.460 align:start position:0% the headphone output for the developers Thanks<00:10:32.149> yeah<00:10:33.149> so<00:10:33.389> I<00:10:33.420> work<00:10:33.750> on<00:10:33.930> sort<00:10:34.259> of<00:10:34.350> a 00:10:34.460 --> 00:10:34.470 align:start position:0% Thanks yeah so I work on sort of a 00:10:34.470 --> 00:10:36.230 align:start position:0% Thanks yeah so I work on sort of a number<00:10:34.800> of<00:10:34.980> projects<00:10:35.519> in<00:10:35.699> the<00:10:35.850> correctness 00:10:36.230 --> 00:10:36.240 align:start position:0% number of projects in the correctness 00:10:36.240 --> 00:10:38.480 align:start position:0% number of projects in the correctness space<00:10:36.600> one<00:10:37.290> of<00:10:37.410> them<00:10:37.529> is<00:10:37.709> I'm<00:10:37.889> advising<00:10:38.220> this 00:10:38.480 --> 00:10:38.490 align:start position:0% space one of them is I'm advising this 00:10:38.490 --> 00:10:39.740 align:start position:0% space one of them is I'm advising this sort<00:10:38.730> of<00:10:38.790> heavier<00:10:39.120> weight<00:10:39.360> formal 00:10:39.740 --> 00:10:39.750 align:start position:0% sort of heavier weight formal 00:10:39.750 --> 00:10:42.230 align:start position:0% sort of heavier weight formal verification<00:10:39.899> project<00:10:40.470> called<00:10:40.860> KVM<00:10:41.370> I'll<00:10:42.029> let 00:10:42.230 --> 00:10:42.240 align:start position:0% verification project called KVM I'll let 00:10:42.240 --> 00:10:43.549 align:start position:0% verification project called KVM I'll let Everett<00:10:42.569> describe<00:10:42.899> that<00:10:43.110> since<00:10:43.380> he's 00:10:43.549 --> 00:10:43.559 align:start position:0% Everett describe that since he's 00:10:43.559 --> 00:10:47.119 align:start position:0% Everett describe that since he's actually<00:10:43.769> the<00:10:44.009> lead<00:10:44.540> but<00:10:45.540> to<00:10:45.930> speak<00:10:46.889> to<00:10:47.040> the 00:10:47.119 --> 00:10:47.129 align:start position:0% actually the lead but to speak to the 00:10:47.129 --> 00:10:48.350 align:start position:0% actually the lead but to speak to the broader<00:10:47.250> point<00:10:47.579> I<00:10:47.819> think<00:10:47.879> there's<00:10:48.180> like<00:10:48.300> a 00:10:48.350 --> 00:10:48.360 align:start position:0% broader point I think there's like a 00:10:48.360 --> 00:10:50.240 align:start position:0% broader point I think there's like a very<00:10:48.660> wide<00:10:48.959> range<00:10:48.990> of<00:10:49.680> correctness 00:10:50.240 --> 00:10:50.250 align:start position:0% very wide range of correctness 00:10:50.250 --> 00:10:52.129 align:start position:0% very wide range of correctness techniques<00:10:50.730> that<00:10:50.939> we<00:10:51.029> have<00:10:51.180> here<00:10:51.420> both<00:10:51.629> formal 00:10:52.129 --> 00:10:52.139 align:start position:0% techniques that we have here both formal 00:10:52.139 --> 00:10:56.059 align:start position:0% techniques that we have here both formal informal<00:10:52.410> and<00:10:52.949> semi<00:10:53.250> formal<00:10:53.720> and<00:10:54.889> another<00:10:55.889> one 00:10:56.059 --> 00:10:56.069 align:start position:0% informal and semi formal and another one 00:10:56.069 --> 00:10:57.799 align:start position:0% informal and semi formal and another one of<00:10:56.160> the<00:10:56.250> projects<00:10:56.610> I'm<00:10:56.730> on<00:10:56.910> Hydra<00:10:57.420> is<00:10:57.480> sort<00:10:57.750> of 00:10:57.799 --> 00:10:57.809 align:start position:0% of the projects I'm on Hydra is sort of 00:10:57.809 --> 00:10:59.780 align:start position:0% of the projects I'm on Hydra is sort of a<00:10:57.899> lighter-weight<00:10:58.170> approach<00:10:58.529> to<00:10:58.709> this<00:10:58.829> where 00:10:59.780 --> 00:10:59.790 align:start position:0% a lighter-weight approach to this where 00:10:59.790 --> 00:11:02.870 align:start position:0% a lighter-weight approach to this where you<00:10:59.970> abandon<00:11:00.750> full<00:11:01.140> formal<00:11:01.530> guarantees<00:11:02.040> for 00:11:02.870 --> 00:11:02.880 align:start position:0% you abandon full formal guarantees for 00:11:02.880 --> 00:11:06.140 align:start position:0% you abandon full formal guarantees for sort<00:11:03.180> of<00:11:03.300> low<00:11:03.540> cost<00:11:03.930> and<00:11:04.500> easy<00:11:04.740> startup<00:11:05.400> which 00:11:06.140 --> 00:11:06.150 align:start position:0% sort of low cost and easy startup which 00:11:06.150 --> 00:11:08.000 align:start position:0% sort of low cost and easy startup which i<00:11:06.360> think<00:11:06.480> is<00:11:06.840> a<00:11:06.870> very<00:11:07.140> valuable<00:11:07.500> thing<00:11:07.620> to<00:11:07.980> a 00:11:08.000 --> 00:11:08.010 align:start position:0% i think is a very valuable thing to a 00:11:08.010 --> 00:11:09.740 align:start position:0% i think is a very valuable thing to a lot<00:11:08.160> of<00:11:08.190> companies<00:11:08.640> who<00:11:08.850> aren't<00:11:09.030> going<00:11:09.480> to<00:11:09.600> be 00:11:09.740 --> 00:11:09.750 align:start position:0% lot of companies who aren't going to be 00:11:09.750 --> 00:11:12.680 align:start position:0% lot of companies who aren't going to be able<00:11:09.870> to<00:11:10.050> as<00:11:10.920> Lowe<00:11:11.490> said<00:11:11.820> hire<00:11:12.360> the<00:11:12.600> right 00:11:12.680 --> 00:11:12.690 align:start position:0% able to as Lowe said hire the right 00:11:12.690 --> 00:11:15.110 align:start position:0% able to as Lowe said hire the right people<00:11:13.080> or<00:11:13.170> have<00:11:13.410> the<00:11:13.560> right<00:11:13.680> expertise<00:11:14.220> at 00:11:15.110 --> 00:11:15.120 align:start position:0% people or have the right expertise at 00:11:15.120 --> 00:11:16.280 align:start position:0% people or have the right expertise at the<00:11:15.270> end<00:11:15.390> of<00:11:15.480> the<00:11:15.540> day<00:11:15.660> formal<00:11:16.110> verification 00:11:16.280 --> 00:11:16.290 align:start position:0% the end of the day formal verification 00:11:16.290 --> 00:11:19.310 align:start position:0% the end of the day formal verification is<00:11:16.920> still<00:11:17.220> super<00:11:17.580> expensive<00:11:17.900> it's<00:11:18.900> still<00:11:19.080> hard 00:11:19.310 --> 00:11:19.320 align:start position:0% is still super expensive it's still hard 00:11:19.320 --> 00:11:20.780 align:start position:0% is still super expensive it's still hard to<00:11:19.350> do<00:11:19.530> and<00:11:19.860> it<00:11:20.010> still<00:11:20.220> doesn't<00:11:20.430> give<00:11:20.550> you 00:11:20.780 --> 00:11:20.790 align:start position:0% to do and it still doesn't give you 00:11:20.790 --> 00:11:22.520 align:start position:0% to do and it still doesn't give you perfect<00:11:21.120> guarantees<00:11:21.690> so<00:11:22.380> it's 00:11:22.520 --> 00:11:22.530 align:start position:0% perfect guarantees so it's 00:11:22.530 --> 00:11:24.590 align:start position:0% perfect guarantees so it's understandable<00:11:23.220> why<00:11:23.370> for<00:11:24.000> a<00:11:24.030> lot<00:11:24.210> of<00:11:24.330> people 00:11:24.590 --> 00:11:24.600 align:start position:0% understandable why for a lot of people 00:11:24.600 --> 00:11:26.360 align:start position:0% understandable why for a lot of people especially<00:11:24.870> now<00:11:25.680> that<00:11:25.710> the<00:11:25.920> tools<00:11:26.160> are<00:11:26.340> not 00:11:26.360 --> 00:11:26.370 align:start position:0% especially now that the tools are not 00:11:26.370 --> 00:11:29.390 align:start position:0% especially now that the tools are not totally<00:11:27.120> mature<00:11:27.500> the<00:11:28.500> business<00:11:28.830> case<00:11:29.070> sort<00:11:29.310> of 00:11:29.390 --> 00:11:29.400 align:start position:0% totally mature the business case sort of 00:11:29.400 --> 00:11:31.340 align:start position:0% totally mature the business case sort of isn't<00:11:29.670> there<00:11:29.880> so<00:11:30.690> I<00:11:30.720> think<00:11:30.840> we<00:11:31.050> need<00:11:31.200> to 00:11:31.340 --> 00:11:31.350 align:start position:0% isn't there so I think we need to 00:11:31.350 --> 00:11:33.320 align:start position:0% isn't there so I think we need to develop<00:11:31.680> a<00:11:31.980> range<00:11:32.250> of<00:11:32.490> techniques<00:11:32.820> and<00:11:33.120> ask 00:11:33.320 --> 00:11:33.330 align:start position:0% develop a range of techniques and ask 00:11:33.330 --> 00:11:34.940 align:start position:0% develop a range of techniques and ask ourselves<00:11:33.540> what<00:11:34.050> are<00:11:34.080> really<00:11:34.290> our<00:11:34.470> high 00:11:34.940 --> 00:11:34.950 align:start position:0% ourselves what are really our high 00:11:34.950 --> 00:11:37.370 align:start position:0% ourselves what are really our high assurance<00:11:35.070> contracts<00:11:35.820> here<00:11:36.120> to<00:11:36.150> use<00:11:36.930> our<00:11:37.140> full 00:11:37.370 --> 00:11:37.380 align:start position:0% assurance contracts here to use our full 00:11:37.380 --> 00:11:39.710 align:start position:0% assurance contracts here to use our full fledge<00:11:37.620> techniques<00:11:38.070> and<00:11:38.340> how<00:11:38.970> can<00:11:39.030> we<00:11:39.360> get<00:11:39.570> the 00:11:39.710 --> 00:11:39.720 align:start position:0% fledge techniques and how can we get the 00:11:39.720 --> 00:11:41.420 align:start position:0% fledge techniques and how can we get the other<00:11:39.870> ones<00:11:40.140> to<00:11:40.410> a<00:11:40.440> better<00:11:40.710> level<00:11:41.070> of<00:11:41.160> security 00:11:41.420 --> 00:11:41.430 align:start position:0% other ones to a better level of security 00:11:41.430 --> 00:11:42.710 align:start position:0% other ones to a better level of security with<00:11:41.670> like<00:11:42.000> the<00:11:42.120> lower<00:11:42.270> hanging<00:11:42.570> fruit 00:11:42.710 --> 00:11:42.720 align:start position:0% with like the lower hanging fruit 00:11:42.720 --> 00:11:46.340 align:start position:0% with like the lower hanging fruit techniques<00:11:44.570> you<00:11:45.570> know<00:11:45.630> I<00:11:45.660> think<00:11:45.810> I<00:11:46.050> agree 00:11:46.340 --> 00:11:46.350 align:start position:0% techniques you know I think I agree 00:11:46.350 --> 00:11:48.110 align:start position:0% techniques you know I think I agree pretty<00:11:46.710> much<00:11:46.950> with<00:11:47.130> what<00:11:47.280> Phil's<00:11:47.550> saying<00:11:47.850> here 00:11:48.110 --> 00:11:48.120 align:start position:0% pretty much with what Phil's saying here 00:11:48.120 --> 00:11:50.240 align:start position:0% pretty much with what Phil's saying here and<00:11:48.810> actually<00:11:49.320> it<00:11:49.410> makes<00:11:49.740> me<00:11:49.890> really<00:11:50.040> happy 00:11:50.240 --> 00:11:50.250 align:start position:0% and actually it makes me really happy 00:11:50.250 --> 00:11:51.760 align:start position:0% and actually it makes me really happy that<00:11:50.520> I<00:11:50.580> see<00:11:50.760> so<00:11:50.940> many<00:11:51.060> people<00:11:51.180> just 00:11:51.760 --> 00:11:51.770 align:start position:0% that I see so many people just 00:11:51.770 --> 00:11:53.510 align:start position:0% that I see so many people just emphasizing<00:11:52.770> the<00:11:52.860> importance<00:11:53.220> of<00:11:53.310> testing 00:11:53.510 --> 00:11:53.520 align:start position:0% emphasizing the importance of testing 00:11:53.520 --> 00:11:55.400 align:start position:0% emphasizing the importance of testing and<00:11:53.910> of<00:11:54.030> writing<00:11:54.330> specifications<00:11:54.510> because 00:11:55.400 --> 00:11:55.410 align:start position:0% and of writing specifications because 00:11:55.410 --> 00:11:58.160 align:start position:0% and of writing specifications because just<00:11:55.680> those<00:11:55.860> two<00:11:56.070> steps<00:11:56.310> alone<00:11:57.050> forced<00:11:58.050> you<00:11:58.140> to 00:11:58.160 --> 00:11:58.170 align:start position:0% just those two steps alone forced you to 00:11:58.170 --> 00:11:59.990 align:start position:0% just those two steps alone forced you to you<00:11:58.560> know<00:11:58.650> first<00:11:58.950> clarify<00:11:59.400> in<00:11:59.550> your<00:11:59.670> head<00:11:59.820> what 00:11:59.990 --> 00:12:00.000 align:start position:0% you know first clarify in your head what 00:12:00.000 --> 00:12:01.610 align:start position:0% you know first clarify in your head what is<00:12:00.120> it<00:12:00.300> I'm<00:12:00.420> trying<00:12:00.570> to<00:12:00.720> do<00:12:00.900> which<00:12:01.350> so<00:12:01.530> many 00:12:01.610 --> 00:12:01.620 align:start position:0% is it I'm trying to do which so many 00:12:01.620 --> 00:12:03.110 align:start position:0% is it I'm trying to do which so many people<00:12:01.920> don't<00:12:02.010> even<00:12:02.160> do<00:12:02.340> they<00:12:02.490> just<00:12:02.670> sit<00:12:03.090> down 00:12:03.110 --> 00:12:03.120 align:start position:0% people don't even do they just sit down 00:12:03.120 --> 00:12:04.750 align:start position:0% people don't even do they just sit down and<00:12:03.390> start<00:12:03.600> kind<00:12:03.720> of<00:12:03.810> clunking<00:12:04.200> away<00:12:04.320> at<00:12:04.440> code 00:12:04.750 --> 00:12:04.760 align:start position:0% and start kind of clunking away at code 00:12:04.760 --> 00:12:07.970 align:start position:0% and start kind of clunking away at code and<00:12:05.760> then<00:12:05.880> second<00:12:06.420> to<00:12:06.660> kind<00:12:07.410> of<00:12:07.500> conker<00:12:07.830> ties 00:12:07.970 --> 00:12:07.980 align:start position:0% and then second to kind of conker ties 00:12:07.980 --> 00:12:09.830 align:start position:0% and then second to kind of conker ties that<00:12:08.160> by<00:12:08.310> writing<00:12:08.520> some<00:12:08.760> tests<00:12:09.120> and<00:12:09.300> then<00:12:09.420> say 00:12:09.830 --> 00:12:09.840 align:start position:0% that by writing some tests and then say 00:12:09.840 --> 00:12:12.110 align:start position:0% that by writing some tests and then say like<00:12:10.050> is<00:12:10.320> what<00:12:10.560> I<00:12:10.590> did<00:12:10.830> actually<00:12:11.100> you<00:12:12.030> know 00:12:12.110 --> 00:12:12.120 align:start position:0% like is what I did actually you know 00:12:12.120 --> 00:12:14.180 align:start position:0% like is what I did actually you know implementing<00:12:12.780> these<00:12:12.900> these<00:12:13.410> tests<00:12:13.890> so<00:12:14.100> the 00:12:14.180 --> 00:12:14.190 align:start position:0% implementing these these tests so the 00:12:14.190 --> 00:12:16.700 align:start position:0% implementing these these tests so the test<00:12:14.400> kind<00:12:14.610> of<00:12:14.700> serve<00:12:14.970> as<00:12:15.180> a<00:12:15.710> semi 00:12:16.700 --> 00:12:16.710 align:start position:0% test kind of serve as a semi 00:12:16.710 --> 00:12:18.050 align:start position:0% test kind of serve as a semi specification<00:12:17.520> if<00:12:17.610> you<00:12:17.700> will<00:12:17.850> or 00:12:18.050 --> 00:12:18.060 align:start position:0% specification if you will or 00:12:18.060 --> 00:12:20.470 align:start position:0% specification if you will or concretization<00:12:18.540> of<00:12:18.900> the<00:12:18.960> specification 00:12:20.470 --> 00:12:20.480 align:start position:0% concretization of the specification 00:12:20.480 --> 00:12:23.720 align:start position:0% concretization of the specification regarding<00:12:21.480> the<00:12:21.570> KVM<00:12:22.110> project<00:12:22.650> that<00:12:23.520> Phil 00:12:23.720 --> 00:12:23.730 align:start position:0% regarding the KVM project that Phil 00:12:23.730 --> 00:12:26.660 align:start position:0% regarding the KVM project that Phil mentioned<00:12:24.000> you<00:12:24.510> know<00:12:24.600> I<00:12:24.630> think<00:12:24.900> it<00:12:25.800> helps<00:12:26.250> with 00:12:26.660 --> 00:12:26.670 align:start position:0% mentioned you know I think it helps with 00:12:26.670 --> 00:12:28.130 align:start position:0% mentioned you know I think it helps with the<00:12:26.820> entire<00:12:27.150> you<00:12:27.600> know<00:12:27.690> there's<00:12:27.870> the<00:12:27.930> entire 00:12:28.130 --> 00:12:28.140 align:start position:0% the entire you know there's the entire 00:12:28.140 --> 00:12:30.770 align:start position:0% the entire you know there's the entire range<00:12:28.440> of<00:12:29.150> verification<00:12:30.150> that<00:12:30.270> you<00:12:30.330> can<00:12:30.600> go 00:12:30.770 --> 00:12:30.780 align:start position:0% range of verification that you can go 00:12:30.780 --> 00:12:32.270 align:start position:0% range of verification that you can go through<00:12:30.960> right<00:12:31.170> you<00:12:31.320> can<00:12:31.440> start<00:12:31.680> at<00:12:31.830> testing 00:12:32.270 --> 00:12:32.280 align:start position:0% through right you can start at testing 00:12:32.280 --> 00:12:34.130 align:start position:0% through right you can start at testing and<00:12:32.490> you<00:12:32.550> can<00:12:32.700> move<00:12:33.360> up<00:12:33.540> to<00:12:33.570> some<00:12:33.900> sort<00:12:34.110> of 00:12:34.130 --> 00:12:34.140 align:start position:0% and you can move up to some sort of 00:12:34.140 --> 00:12:36.200 align:start position:0% and you can move up to some sort of runtime<00:12:34.350> verification<00:12:35.280> or<00:12:35.520> runtime<00:12:35.910> model 00:12:36.200 --> 00:12:36.210 align:start position:0% runtime verification or runtime model 00:12:36.210 --> 00:12:38.960 align:start position:0% runtime verification or runtime model checking<00:12:36.630> up<00:12:37.530> to<00:12:37.800> model<00:12:38.100> checking<00:12:38.310> which<00:12:38.760> is 00:12:38.960 --> 00:12:38.970 align:start position:0% checking up to model checking which is 00:12:38.970 --> 00:12:40.220 align:start position:0% checking up to model checking which is where<00:12:39.120> you<00:12:39.210> explore<00:12:39.480> the<00:12:39.600> whole<00:12:39.750> state<00:12:39.960> space 00:12:40.220 --> 00:12:40.230 align:start position:0% where you explore the whole state space 00:12:40.230 --> 00:12:41.810 align:start position:0% where you explore the whole state space of<00:12:40.590> a<00:12:40.650> program<00:12:41.010> and<00:12:41.160> then<00:12:41.280> up<00:12:41.430> to<00:12:41.550> theorem 00:12:41.810 --> 00:12:41.820 align:start position:0% of a program and then up to theorem 00:12:41.820 --> 00:12:43.520 align:start position:0% of a program and then up to theorem proving<00:12:42.090> where<00:12:42.300> you<00:12:42.450> use<00:12:42.960> more<00:12:43.200> advanced 00:12:43.520 --> 00:12:43.530 align:start position:0% proving where you use more advanced 00:12:43.530 --> 00:12:44.810 align:start position:0% proving where you use more advanced techniques<00:12:43.890> to<00:12:44.010> prove<00:12:44.220> that<00:12:44.370> a<00:12:44.430> program<00:12:44.790> is 00:12:44.810 --> 00:12:44.820 align:start position:0% techniques to prove that a program is 00:12:44.820 --> 00:12:47.080 align:start position:0% techniques to prove that a program is behaving<00:12:45.720> correctly<00:12:45.840> and<00:12:46.200> K<00:12:46.350> gives<00:12:46.590> you<00:12:46.680> tools 00:12:47.080 --> 00:12:47.090 align:start position:0% behaving correctly and K gives you tools 00:12:47.090 --> 00:12:50.960 align:start position:0% behaving correctly and K gives you tools for<00:12:48.090> all<00:12:48.210> of<00:12:48.330> those<00:12:48.420> things<00:12:48.690> actually<00:12:49.170> so<00:12:49.970> I 00:12:50.960 --> 00:12:50.970 align:start position:0% for all of those things actually so I 00:12:50.970 --> 00:12:53.330 align:start position:0% for all of those things actually so I think<00:12:51.180> you<00:12:51.600> know<00:12:51.690> KTM<00:12:52.140> can<00:12:52.320> be<00:12:52.410> a<00:12:52.440> useful<00:12:52.680> tool 00:12:53.330 --> 00:12:53.340 align:start position:0% think you know KTM can be a useful tool 00:12:53.340 --> 00:12:54.800 align:start position:0% think you know KTM can be a useful tool in<00:12:53.850> that<00:12:53.940> space<00:12:54.120> it<00:12:54.240> doesn't<00:12:54.360> have<00:12:54.540> quite<00:12:54.780> a 00:12:54.800 --> 00:12:54.810 align:start position:0% in that space it doesn't have quite a 00:12:54.810 --> 00:12:57.610 align:start position:0% in that space it doesn't have quite a nice<00:12:55.050> user<00:12:55.890> interface<00:12:56.060> unfortunately<00:12:57.060> so<00:12:57.330> it 00:12:57.610 --> 00:12:57.620 align:start position:0% nice user interface unfortunately so it 00:12:57.620 --> 00:13:00.650 align:start position:0% nice user interface unfortunately so it suffers<00:12:58.620> from<00:12:58.650> that<00:12:58.950> but<00:12:59.310> I<00:12:59.520> think<00:13:00.480> it<00:13:00.570> can 00:13:00.650 --> 00:13:00.660 align:start position:0% suffers from that but I think it can 00:13:00.660 --> 00:13:05.560 align:start position:0% suffers from that but I think it can help<00:13:00.810> a<00:13:00.930> lot<00:13:01.080> in<00:13:01.320> in<00:13:01.770> all<00:13:01.890> those<00:13:02.070> areas<00:13:04.280> Thanks 00:13:05.560 --> 00:13:05.570 align:start position:0% help a lot in in all those areas Thanks 00:13:05.570 --> 00:13:09.500 align:start position:0% help a lot in in all those areas Thanks so<00:13:06.570> it<00:13:06.630> seems<00:13:06.840> like<00:13:06.930> a<00:13:07.190> common<00:13:08.190> theme<00:13:08.970> seems<00:13:09.270> to 00:13:09.500 --> 00:13:09.510 align:start position:0% so it seems like a common theme seems to 00:13:09.510 --> 00:13:13.530 align:start position:0% so it seems like a common theme seems to be<00:13:09.630> it's<00:13:09.840> like<00:13:09.900> too<00:13:10.260> complicated<00:13:10.680> so<00:13:11.570> so<00:13:12.570> how 00:13:13.530 --> 00:13:13.540 align:start position:0% be it's like too complicated so so how 00:13:13.540 --> 00:13:16.980 align:start position:0% be it's like too complicated so so how can<00:13:13.690> we<00:13:13.810> make<00:13:13.959> tools<00:13:14.290> and/or<00:13:15.660> how<00:13:16.660> can<00:13:16.839> we 00:13:16.980 --> 00:13:16.990 align:start position:0% can we make tools and/or how can we 00:13:16.990 --> 00:13:19.740 align:start position:0% can we make tools and/or how can we develop<00:13:17.440> approaches<00:13:18.100> or<00:13:18.339> more<00:13:18.670> accessible<00:13:19.420> to 00:13:19.740 --> 00:13:19.750 align:start position:0% develop approaches or more accessible to 00:13:19.750 --> 00:13:24.810 align:start position:0% develop approaches or more accessible to the<00:13:19.990> end-user<00:13:20.380> I<00:13:22.320> think<00:13:23.320> in<00:13:23.560> the<00:13:23.769> end<00:13:23.860> it's<00:13:24.399> not 00:13:24.810 --> 00:13:24.820 align:start position:0% the end-user I think in the end it's not 00:13:24.820 --> 00:13:28.639 align:start position:0% the end-user I think in the end it's not reasonable<00:13:25.269> to<00:13:25.690> expect<00:13:25.810> the<00:13:26.529> end<00:13:26.620> users<00:13:27.360> or 00:13:28.639 --> 00:13:28.649 align:start position:0% reasonable to expect the end users or 00:13:28.649 --> 00:13:33.120 align:start position:0% reasonable to expect the end users or users<00:13:29.649> to<00:13:30.040> read<00:13:30.339> logical<00:13:31.029> formulas<00:13:31.569> or<00:13:32.130> maybe 00:13:33.120 --> 00:13:33.130 align:start position:0% users to read logical formulas or maybe 00:13:33.130 --> 00:13:36.030 align:start position:0% users to read logical formulas or maybe K<00:13:33.699> configurations<00:13:34.690> are<00:13:34.959> more<00:13:35.110> accessible<00:13:35.860> but 00:13:36.030 --> 00:13:36.040 align:start position:0% K configurations are more accessible but 00:13:36.040 --> 00:13:39.569 align:start position:0% K configurations are more accessible but it's<00:13:36.610> hard<00:13:37.240> so<00:13:37.990> at<00:13:38.319> the<00:13:38.470> end<00:13:38.589> what<00:13:38.920> we<00:13:39.130> want<00:13:39.370> is 00:13:39.569 --> 00:13:39.579 align:start position:0% it's hard so at the end what we want is 00:13:39.579 --> 00:13:42.740 align:start position:0% it's hard so at the end what we want is sure<00:13:40.569> that<00:13:40.870> can<00:13:41.110> synthesize<00:13:41.380> an<00:13:41.949> advisory 00:13:42.740 --> 00:13:42.750 align:start position:0% sure that can synthesize an advisory 00:13:42.750 --> 00:13:48.059 align:start position:0% sure that can synthesize an advisory based<00:13:43.750> on<00:13:44.019> the<00:13:45.509> unproven<00:13:46.509> goals<00:13:47.170> this 00:13:48.059 --> 00:13:48.069 align:start position:0% based on the unproven goals this 00:13:48.069 --> 00:13:53.150 align:start position:0% based on the unproven goals this scenario<00:13:48.699> can<00:13:48.910> happen<00:13:49.389> and<00:13:49.540> it<00:13:49.690> can<00:13:49.959> play<00:13:50.110> it 00:13:53.150 --> 00:13:53.160 align:start position:0% 00:13:53.160 --> 00:13:56.550 align:start position:0% may<00:13:54.160> be<00:13:54.220> not<00:13:54.459> an<00:13:54.610> animation<00:13:54.910> but<00:13:55.209> like<00:13:55.560> it 00:13:56.550 --> 00:13:56.560 align:start position:0% may be not an animation but like it 00:13:56.560 --> 00:13:58.710 align:start position:0% may be not an animation but like it should<00:13:57.190> look<00:13:57.310> like<00:13:57.370> somebody<00:13:58.089> attacking<00:13:58.569> you 00:13:58.710 --> 00:13:58.720 align:start position:0% should look like somebody attacking you 00:13:58.720 --> 00:14:01.199 align:start position:0% should look like somebody attacking you your<00:13:59.079> contract<00:13:59.620> that<00:14:00.370> would<00:14:00.579> make<00:14:00.910> the 00:14:01.199 --> 00:14:01.209 align:start position:0% your contract that would make the 00:14:01.209 --> 00:14:06.920 align:start position:0% your contract that would make the problem<00:14:01.470> much<00:14:02.470> more<00:14:03.240> easier<00:14:04.240> to<00:14:04.449> understand 00:14:06.920 --> 00:14:06.930 align:start position:0% problem much more easier to understand 00:14:06.930 --> 00:14:10.650 align:start position:0% problem much more easier to understand so<00:14:07.930> I<00:14:08.170> guess<00:14:08.440> if<00:14:08.740> stability<00:14:09.279> is<00:14:09.519> always<00:14:09.910> a<00:14:10.089> hard 00:14:10.650 --> 00:14:10.660 align:start position:0% so I guess if stability is always a hard 00:14:10.660 --> 00:14:13.079 align:start position:0% so I guess if stability is always a hard problem<00:14:10.810> right<00:14:11.319> and<00:14:11.889> that's<00:14:12.579> also<00:14:12.730> like<00:14:12.940> one 00:14:13.079 --> 00:14:13.089 align:start position:0% problem right and that's also like one 00:14:13.089 --> 00:14:14.579 align:start position:0% problem right and that's also like one of<00:14:13.180> the<00:14:13.300> motivation<00:14:13.839> that<00:14:13.990> why<00:14:14.170> we<00:14:14.350> build 00:14:14.579 --> 00:14:14.589 align:start position:0% of the motivation that why we build 00:14:14.589 --> 00:14:17.550 align:start position:0% of the motivation that why we build buoyant<00:14:15.100> e<00:14:15.220> the<00:14:16.209> smart<00:14:16.930> contract<00:14:17.050> analyzer 00:14:17.550 --> 00:14:17.560 align:start position:0% buoyant e the smart contract analyzer 00:14:17.560 --> 00:14:20.370 align:start position:0% buoyant e the smart contract analyzer based<00:14:17.949> on<00:14:18.190> symbolic<00:14:18.399> execution<00:14:19.019> so<00:14:20.019> the<00:14:20.139> idea 00:14:20.370 --> 00:14:20.380 align:start position:0% based on symbolic execution so the idea 00:14:20.380 --> 00:14:21.960 align:start position:0% based on symbolic execution so the idea here<00:14:20.410> is<00:14:20.620> that<00:14:20.649> you<00:14:20.949> know<00:14:21.069> user<00:14:21.550> they<00:14:21.699> do<00:14:21.760> not 00:14:21.960 --> 00:14:21.970 align:start position:0% here is that you know user they do not 00:14:21.970 --> 00:14:23.490 align:start position:0% here is that you know user they do not need<00:14:22.120> to<00:14:22.180> understand<00:14:22.720> like<00:14:22.930> how<00:14:23.110> authentic 00:14:23.490 --> 00:14:23.500 align:start position:0% need to understand like how authentic 00:14:23.500 --> 00:14:24.120 align:start position:0% need to understand like how authentic works 00:14:24.120 --> 00:14:24.130 align:start position:0% works 00:14:24.130 --> 00:14:25.559 align:start position:0% works they're<00:14:24.519> only<00:14:24.610> need<00:14:24.850> like<00:14:25.000> to<00:14:25.120> paste<00:14:25.360> the 00:14:25.559 --> 00:14:25.569 align:start position:0% they're only need like to paste the 00:14:25.569 --> 00:14:27.960 align:start position:0% they're only need like to paste the smart<00:14:25.839> contract<00:14:25.959> into<00:14:26.440> Oyen<00:14:26.829> T<00:14:27.010> or<00:14:27.279> into<00:14:27.699> the 00:14:27.960 --> 00:14:27.970 align:start position:0% smart contract into Oyen T or into the 00:14:27.970 --> 00:14:30.210 align:start position:0% smart contract into Oyen T or into the you<00:14:28.630> know<00:14:28.750> web<00:14:29.199> browser<00:14:29.440> and<00:14:29.769> they<00:14:29.980> click 00:14:30.210 --> 00:14:30.220 align:start position:0% you know web browser and they click 00:14:30.220 --> 00:14:32.340 align:start position:0% you know web browser and they click analyze<00:14:30.550> and<00:14:30.940> we<00:14:31.449> can<00:14:31.630> just<00:14:31.839> like<00:14:31.959> show<00:14:32.139> all 00:14:32.340 --> 00:14:32.350 align:start position:0% analyze and we can just like show all 00:14:32.350 --> 00:14:34.800 align:start position:0% analyze and we can just like show all the<00:14:32.470> possible<00:14:33.209> vulnerabilities<00:14:34.209> that 00:14:34.800 --> 00:14:34.810 align:start position:0% the possible vulnerabilities that 00:14:34.810 --> 00:14:38.600 align:start position:0% the possible vulnerabilities that orientation<00:14:35.170> can<00:14:35.680> figure<00:14:36.040> out<00:14:36.160> yeah<00:14:37.029> I 00:14:38.600 --> 00:14:38.610 align:start position:0% orientation can figure out yeah I 00:14:38.610 --> 00:14:40.920 align:start position:0% orientation can figure out yeah I personally<00:14:39.610> think<00:14:39.790> demand<00:14:40.269> sort<00:14:40.600> of<00:14:40.690> breeds 00:14:40.920 --> 00:14:40.930 align:start position:0% personally think demand sort of breeds 00:14:40.930 --> 00:14:43.350 align:start position:0% personally think demand sort of breeds progress<00:14:41.440> in<00:14:41.589> this<00:14:41.680> direction<00:14:41.970> and<00:14:42.970> we're 00:14:43.350 --> 00:14:43.360 align:start position:0% progress in this direction and we're 00:14:43.360 --> 00:14:44.910 align:start position:0% progress in this direction and we're sitting<00:14:43.569> in<00:14:43.750> a<00:14:43.810> room<00:14:43.959> of<00:14:44.199> some<00:14:44.500> extremely 00:14:44.910 --> 00:14:44.920 align:start position:0% sitting in a room of some extremely 00:14:44.920 --> 00:14:46.590 align:start position:0% sitting in a room of some extremely smart<00:14:45.250> and<00:14:45.430> talented<00:14:45.579> people<00:14:45.970> and<00:14:46.240> we've<00:14:46.360> seen 00:14:46.590 --> 00:14:46.600 align:start position:0% smart and talented people and we've seen 00:14:46.600 --> 00:14:48.059 align:start position:0% smart and talented people and we've seen some<00:14:46.779> projects<00:14:47.230> that<00:14:47.380> really<00:14:47.529> push<00:14:47.889> the 00:14:48.059 --> 00:14:48.069 align:start position:0% some projects that really push the 00:14:48.069 --> 00:14:51.090 align:start position:0% some projects that really push the envelope<00:14:48.100> in<00:14:48.670> a<00:14:48.730> number<00:14:48.970> of<00:14:49.060> spaces<00:14:49.300> and<00:14:50.100> while 00:14:51.090 --> 00:14:51.100 align:start position:0% envelope in a number of spaces and while 00:14:51.100 --> 00:14:52.439 align:start position:0% envelope in a number of spaces and while the<00:14:51.220> tools<00:14:51.459> are<00:14:51.639> hard<00:14:51.850> to<00:14:51.970> use<00:14:52.149> and<00:14:52.360> there 00:14:52.439 --> 00:14:52.449 align:start position:0% the tools are hard to use and there 00:14:52.449 --> 00:14:53.879 align:start position:0% the tools are hard to use and there certainly<00:14:52.720> could<00:14:52.959> be<00:14:53.110> improvements<00:14:53.680> made 00:14:53.879 --> 00:14:53.889 align:start position:0% certainly could be improvements made 00:14:53.889 --> 00:14:57.030 align:start position:0% certainly could be improvements made there<00:14:54.209> nothing<00:14:55.209> here<00:14:55.630> is<00:14:55.779> sort<00:14:56.019> of<00:14:56.079> magic<00:14:56.829> or 00:14:57.030 --> 00:14:57.040 align:start position:0% there nothing here is sort of magic or 00:14:57.040 --> 00:14:58.350 align:start position:0% there nothing here is sort of magic or anything<00:14:57.100> like<00:14:57.610> that<00:14:57.670> so<00:14:58.000> I<00:14:58.180> think 00:14:58.350 --> 00:14:58.360 align:start position:0% anything like that so I think 00:14:58.360 --> 00:15:00.389 align:start position:0% anything like that so I think sufficiently<00:14:59.050> motivated<00:14:59.680> developers<00:15:00.160> who 00:15:00.389 --> 00:15:00.399 align:start position:0% sufficiently motivated developers who 00:15:00.399 --> 00:15:01.949 align:start position:0% sufficiently motivated developers who are<00:15:00.430> incentivized<00:15:01.089> by<00:15:01.209> the<00:15:01.329> market<00:15:01.720> to 00:15:01.949 --> 00:15:01.959 align:start position:0% are incentivized by the market to 00:15:01.959 --> 00:15:04.290 align:start position:0% are incentivized by the market to develop<00:15:02.230> these<00:15:02.529> tools<00:15:02.800> is<00:15:03.760> really<00:15:03.819> what<00:15:04.209> we 00:15:04.290 --> 00:15:04.300 align:start position:0% develop these tools is really what we 00:15:04.300 --> 00:15:06.210 align:start position:0% develop these tools is really what we need<00:15:04.449> to<00:15:04.660> push<00:15:04.870> the<00:15:05.079> the<00:15:05.589> envelope<00:15:05.949> here 00:15:06.210 --> 00:15:06.220 align:start position:0% need to push the the envelope here 00:15:06.220 --> 00:15:08.370 align:start position:0% need to push the the envelope here another<00:15:07.149> thing<00:15:07.420> that<00:15:07.689> I<00:15:07.899> think<00:15:08.110> is<00:15:08.199> really 00:15:08.370 --> 00:15:08.380 align:start position:0% another thing that I think is really 00:15:08.380 --> 00:15:10.350 align:start position:0% another thing that I think is really helpful<00:15:08.709> and<00:15:09.040> I'd<00:15:09.579> like<00:15:09.759> to<00:15:09.970> especially 00:15:10.350 --> 00:15:10.360 align:start position:0% helpful and I'd like to especially 00:15:10.360 --> 00:15:11.999 align:start position:0% helpful and I'd like to especially congratulate<00:15:11.110> melon<00:15:11.350> port<00:15:11.560> for<00:15:11.709> taking<00:15:11.920> this 00:15:11.999 --> 00:15:12.009 align:start position:0% congratulate melon port for taking this 00:15:12.009 --> 00:15:14.519 align:start position:0% congratulate melon port for taking this approach<00:15:12.269> is<00:15:13.269> to<00:15:13.600> take<00:15:13.779> these<00:15:13.959> things<00:15:14.230> out<00:15:14.500> of 00:15:14.519 --> 00:15:14.529 align:start position:0% approach is to take these things out of 00:15:14.529 --> 00:15:17.160 align:start position:0% approach is to take these things out of academia<00:15:14.980> and<00:15:15.310> into<00:15:15.610> industry<00:15:16.000> and<00:15:16.029> use<00:15:16.930> them 00:15:17.160 --> 00:15:17.170 align:start position:0% academia and into industry and use them 00:15:17.170 --> 00:15:20.189 align:start position:0% academia and into industry and use them on<00:15:17.319> real<00:15:17.800> contracts<00:15:18.310> with<00:15:19.269> real<00:15:19.540> developers 00:15:20.189 --> 00:15:20.199 align:start position:0% on real contracts with real developers 00:15:20.199 --> 00:15:21.360 align:start position:0% on real contracts with real developers who<00:15:20.380> are<00:15:20.439> working<00:15:20.769> on<00:15:20.889> the<00:15:20.980> ground<00:15:21.160> in 00:15:21.360 --> 00:15:21.370 align:start position:0% who are working on the ground in 00:15:21.370 --> 00:15:24.300 align:start position:0% who are working on the ground in solidity<00:15:21.819> I<00:15:22.630> think<00:15:23.079> just<00:15:23.319> that<00:15:23.380> step<00:15:23.829> could<00:15:24.160> do 00:15:24.300 --> 00:15:24.310 align:start position:0% solidity I think just that step could do 00:15:24.310 --> 00:15:26.130 align:start position:0% solidity I think just that step could do a<00:15:24.339> lot<00:15:24.579> for<00:15:24.610> usability 00:15:26.130 --> 00:15:26.140 align:start position:0% a lot for usability 00:15:26.140 --> 00:15:27.900 align:start position:0% a lot for usability and<00:15:26.200> academics<00:15:26.980> are<00:15:27.100> not<00:15:27.220> really<00:15:27.520> the<00:15:27.700> the 00:15:27.900 --> 00:15:27.910 align:start position:0% and academics are not really the the 00:15:27.910 --> 00:15:29.340 align:start position:0% and academics are not really the the greatest<00:15:28.240> at<00:15:28.390> writing<00:15:28.690> super<00:15:28.990> useable 00:15:29.340 --> 00:15:29.350 align:start position:0% greatest at writing super useable 00:15:29.350 --> 00:15:32.490 align:start position:0% greatest at writing super useable systems<00:15:29.710> sometimes<00:15:30.190> so<00:15:30.960> more<00:15:31.960> more<00:15:32.290> broad 00:15:32.490 --> 00:15:32.500 align:start position:0% systems sometimes so more more broad 00:15:32.500 --> 00:15:36.840 align:start position:0% systems sometimes so more more broad participation<00:15:32.710> would<00:15:33.280> definitely<00:15:33.700> help<00:15:35.850> yeah 00:15:36.840 --> 00:15:36.850 align:start position:0% participation would definitely help yeah 00:15:36.850 --> 00:15:39.030 align:start position:0% participation would definitely help yeah if<00:15:36.970> they're<00:15:37.120> 13<00:15:37.540> that<00:15:37.690> in<00:15:38.230> just<00:15:38.380> 30<00:15:38.500> seconds<00:15:38.890> it 00:15:39.030 --> 00:15:39.040 align:start position:0% if they're 13 that in just 30 seconds it 00:15:39.040 --> 00:15:41.520 align:start position:0% if they're 13 that in just 30 seconds it but<00:15:39.760> yeah<00:15:39.880> definitely<00:15:40.090> the<00:15:40.540> the<00:15:41.110> approach 00:15:41.520 --> 00:15:41.530 align:start position:0% but yeah definitely the the approach 00:15:41.530 --> 00:15:43.560 align:start position:0% but yeah definitely the the approach that<00:15:41.560> that<00:15:42.250> mellon<00:15:42.550> port<00:15:42.760> is<00:15:42.850> taking<00:15:43.180> seems<00:15:43.420> to 00:15:43.560 --> 00:15:43.570 align:start position:0% that that mellon port is taking seems to 00:15:43.570 --> 00:15:46.230 align:start position:0% that that mellon port is taking seems to be<00:15:44.100> the<00:15:45.100> correct<00:15:45.310> one<00:15:45.520> just<00:15:45.790> make<00:15:45.910> the<00:15:46.060> tools 00:15:46.230 --> 00:15:46.240 align:start position:0% be the correct one just make the tools 00:15:46.240 --> 00:15:48.210 align:start position:0% be the correct one just make the tools usable<00:15:46.690> and<00:15:46.840> make<00:15:46.960> them<00:15:47.110> have<00:15:47.320> check<00:15:47.800> for<00:15:47.980> some 00:15:48.210 --> 00:15:48.220 align:start position:0% usable and make them have check for some 00:15:48.220 --> 00:15:51.200 align:start position:0% usable and make them have check for some some<00:15:49.090> specific<00:15:49.540> properties<00:15:49.770> automatically 00:15:51.200 --> 00:15:51.210 align:start position:0% some specific properties automatically 00:15:51.210 --> 00:15:53.760 align:start position:0% some specific properties automatically certainly<00:15:52.210> all<00:15:52.330> the<00:15:52.360> verification<00:15:53.320> tools<00:15:53.530> can 00:15:53.760 --> 00:15:53.770 align:start position:0% certainly all the verification tools can 00:15:53.770 --> 00:15:55.470 align:start position:0% certainly all the verification tools can be<00:15:53.890> instantiated<00:15:54.310> to<00:15:54.880> do<00:15:54.970> those<00:15:55.150> sorts<00:15:55.330> of 00:15:55.470 --> 00:15:55.480 align:start position:0% be instantiated to do those sorts of 00:15:55.480 --> 00:15:57.870 align:start position:0% be instantiated to do those sorts of things<00:15:55.690> but<00:15:56.040> you<00:15:57.040> know<00:15:57.130> it<00:15:57.220> takes<00:15:57.310> effort<00:15:57.550> and 00:15:57.870 --> 00:15:57.880 align:start position:0% things but you know it takes effort and 00:15:57.880 --> 00:15:59.190 align:start position:0% things but you know it takes effort and takes<00:15:58.030> developer<00:15:58.390> time<00:15:58.570> it<00:15:58.720> takes<00:15:58.900> people<00:15:59.050> who 00:15:59.190 --> 00:15:59.200 align:start position:0% takes developer time it takes people who 00:15:59.200 --> 00:16:00.890 align:start position:0% takes developer time it takes people who know<00:15:59.350> the<00:15:59.470> tools<00:15:59.680> to<00:15:59.860> do<00:15:59.950> that<00:15:59.980> instantiation 00:16:00.890 --> 00:16:00.900 align:start position:0% know the tools to do that instantiation 00:16:00.900 --> 00:16:03.060 align:start position:0% know the tools to do that instantiation and<00:16:01.900> that's<00:16:02.320> not<00:16:02.440> going<00:16:02.560> to<00:16:02.620> happen<00:16:02.770> overnight 00:16:03.060 --> 00:16:03.070 align:start position:0% and that's not going to happen overnight 00:16:03.070 --> 00:16:05.640 align:start position:0% and that's not going to happen overnight so<00:16:03.510> you<00:16:04.510> know<00:16:04.630> these<00:16:04.750> lighter-weight<00:16:05.140> methods 00:16:05.640 --> 00:16:05.650 align:start position:0% so you know these lighter-weight methods 00:16:05.650 --> 00:16:07.740 align:start position:0% so you know these lighter-weight methods like<00:16:05.980> fills<00:16:06.670> hydro<00:16:07.060> stuff<00:16:07.300> that's<00:16:07.510> really 00:16:07.740 --> 00:16:07.750 align:start position:0% like fills hydro stuff that's really 00:16:07.750 --> 00:16:10.290 align:start position:0% like fills hydro stuff that's really gonna<00:16:07.900> be<00:16:08.650> the<00:16:08.680> stopgap<00:16:09.280> until<00:16:09.490> we<00:16:09.850> can<00:16:10.090> have 00:16:10.290 --> 00:16:10.300 align:start position:0% gonna be the stopgap until we can have 00:16:10.300 --> 00:16:12.330 align:start position:0% gonna be the stopgap until we can have better<00:16:10.510> tooling<00:16:10.780> for<00:16:11.230> all<00:16:11.350> these<00:16:11.530> you<00:16:12.250> know 00:16:12.330 --> 00:16:12.340 align:start position:0% better tooling for all these you know 00:16:12.340 --> 00:16:20.250 align:start position:0% better tooling for all these you know high<00:16:12.490> assurance<00:16:12.610> tools<00:16:17.820> so<00:16:19.110> the<00:16:20.110> last 00:16:20.250 --> 00:16:20.260 align:start position:0% high assurance tools so the last 00:16:20.260 --> 00:16:22.170 align:start position:0% high assurance tools so the last question<00:16:20.410> from<00:16:20.740> from<00:16:21.190> me<00:16:21.280> and<00:16:21.460> then<00:16:21.610> opening 00:16:22.170 --> 00:16:22.180 align:start position:0% question from from me and then opening 00:16:22.180 --> 00:16:25.050 align:start position:0% question from from me and then opening it<00:16:22.270> up<00:16:22.330> to<00:16:22.540> the<00:16:22.690> audience<00:16:22.840> is<00:16:23.940> essentially<00:16:24.940> a 00:16:25.050 --> 00:16:25.060 align:start position:0% it up to the audience is essentially a 00:16:25.060 --> 00:16:30.960 align:start position:0% it up to the audience is essentially a shout<00:16:25.330> out<00:16:25.360> from<00:16:25.660> you<00:16:25.840> guys<00:16:25.990> so<00:16:29.520> but<00:16:30.520> what 00:16:30.960 --> 00:16:30.970 align:start position:0% shout out from you guys so but what 00:16:30.970 --> 00:16:32.340 align:start position:0% shout out from you guys so but what would<00:16:31.120> you<00:16:31.180> like<00:16:31.360> to<00:16:31.540> see<00:16:31.780> come<00:16:32.140> from 00:16:32.340 --> 00:16:32.350 align:start position:0% would you like to see come from 00:16:32.350 --> 00:16:34.230 align:start position:0% would you like to see come from different<00:16:32.560> ecosystem<00:16:33.250> players<00:16:33.460> so<00:16:33.760> from<00:16:33.940> from 00:16:34.230 --> 00:16:34.240 align:start position:0% different ecosystem players so from from 00:16:34.240 --> 00:16:37.320 align:start position:0% different ecosystem players so from from the<00:16:34.360> users<00:16:34.750> developers<00:16:35.710> investors<00:16:36.370> the 00:16:37.320 --> 00:16:37.330 align:start position:0% the users developers investors the 00:16:37.330 --> 00:16:40.050 align:start position:0% the users developers investors the project<00:16:37.690> leads<00:16:37.900> and<00:16:38.260> researchers<00:16:38.890> to<00:16:39.160> make 00:16:40.050 --> 00:16:40.060 align:start position:0% project leads and researchers to make 00:16:40.060 --> 00:16:45.390 align:start position:0% project leads and researchers to make formal<00:16:40.420> verification<00:16:41.040> mainstream<00:16:44.040> in<00:16:45.040> the 00:16:45.390 --> 00:16:45.400 align:start position:0% formal verification mainstream in the 00:16:45.400 --> 00:16:49.260 align:start position:0% formal verification mainstream in the current<00:16:46.260> ecosystem<00:16:47.260> I<00:16:47.500> think<00:16:47.980> it's<00:16:48.550> to<00:16:49.060> the 00:16:49.260 --> 00:16:49.270 align:start position:0% current ecosystem I think it's to the 00:16:49.270 --> 00:16:54.300 align:start position:0% current ecosystem I think it's to the users<00:16:50.730> responsibility<00:16:51.730> to<00:16:52.720> make<00:16:53.260> sure<00:16:53.310> that 00:16:54.300 --> 00:16:54.310 align:start position:0% users responsibility to make sure that 00:16:54.310 --> 00:16:57.600 align:start position:0% users responsibility to make sure that they<00:16:55.240> understand<00:16:56.110> the<00:16:56.560> contract<00:16:57.100> they<00:16:57.400> are 00:16:57.600 --> 00:16:57.610 align:start position:0% they understand the contract they are 00:16:57.610 --> 00:17:04.110 align:start position:0% they understand the contract they are interacting<00:16:58.560> with<00:17:00.540> some<00:17:01.540> people<00:17:02.970> people<00:17:03.970> are 00:17:04.110 --> 00:17:04.120 align:start position:0% interacting with some people people are 00:17:04.120 --> 00:17:07.500 align:start position:0% interacting with some people people are like<00:17:04.620> proposing<00:17:05.620> markets<00:17:06.160> for<00:17:06.490> audits<00:17:06.910> and<00:17:07.209> so 00:17:07.500 --> 00:17:07.510 align:start position:0% like proposing markets for audits and so 00:17:07.510 --> 00:17:12.630 align:start position:0% like proposing markets for audits and so on<00:17:07.690> but<00:17:07.900> it<00:17:08.079> is<00:17:08.310> not<00:17:09.310> working<00:17:10.030> yet<00:17:10.420> so<00:17:11.640> actually 00:17:12.630 --> 00:17:12.640 align:start position:0% on but it is not working yet so actually 00:17:12.640 --> 00:17:16.199 align:start position:0% on but it is not working yet so actually I<00:17:12.880> have<00:17:13.300> to<00:17:13.540> repeat<00:17:13.839> Martin<00:17:14.290> I<00:17:14.470> mean<00:17:14.970> it's<00:17:15.970> fair 00:17:16.199 --> 00:17:16.209 align:start position:0% I have to repeat Martin I mean it's fair 00:17:16.209 --> 00:17:19.319 align:start position:0% I have to repeat Martin I mean it's fair to<00:17:16.420> say<00:17:16.449> this<00:17:16.660> but<00:17:17.079> you<00:17:17.410> have<00:17:17.440> to<00:17:17.730> be<00:17:18.730> it<00:17:18.880> a<00:17:19.120> byte 00:17:19.319 --> 00:17:19.329 align:start position:0% to say this but you have to be it a byte 00:17:19.329 --> 00:17:19.860 align:start position:0% to say this but you have to be it a byte called 00:17:19.860 --> 00:17:19.870 align:start position:0% called 00:17:19.870 --> 00:17:23.490 align:start position:0% called learn<00:17:20.230> the<00:17:20.500> VM<00:17:20.920> in<00:17:21.670> order<00:17:22.030> to<00:17:22.209> make<00:17:22.390> sure<00:17:22.750> that 00:17:23.490 --> 00:17:23.500 align:start position:0% learn the VM in order to make sure that 00:17:23.500 --> 00:17:26.430 align:start position:0% learn the VM in order to make sure that you<00:17:23.709> are<00:17:23.890> interacting<00:17:24.220> with<00:17:25.290> busines<00:17:26.290> brew 00:17:26.430 --> 00:17:26.440 align:start position:0% you are interacting with busines brew 00:17:26.440 --> 00:17:30.330 align:start position:0% you are interacting with busines brew thing<00:17:28.170> it's<00:17:29.170> sort<00:17:29.410> of<00:17:29.530> Sadie's<00:17:29.860> but<00:17:30.100> it's 00:17:30.330 --> 00:17:30.340 align:start position:0% thing it's sort of Sadie's but it's 00:17:30.340 --> 00:17:33.930 align:start position:0% thing it's sort of Sadie's but it's something<00:17:30.940> like<00:17:31.210> that<00:17:31.420> currently<00:17:32.670> and<00:17:33.670> then 00:17:33.930 --> 00:17:33.940 align:start position:0% something like that currently and then 00:17:33.940 --> 00:17:37.290 align:start position:0% something like that currently and then yes<00:17:34.300> something<00:17:34.930> like<00:17:35.670> audit<00:17:36.670> market<00:17:37.060> with 00:17:37.290 --> 00:17:37.300 align:start position:0% yes something like audit market with 00:17:37.300 --> 00:17:38.900 align:start position:0% yes something like audit market with reputation<00:17:37.600> system 00:17:38.900 --> 00:17:38.910 align:start position:0% reputation system 00:17:38.910 --> 00:17:41.770 align:start position:0% reputation system something<00:17:39.150> like<00:17:39.300> that<00:17:39.510> very<00:17:39.870> gradually 00:17:41.770 --> 00:17:41.780 align:start position:0% something like that very gradually 00:17:41.780 --> 00:17:46.580 align:start position:0% something like that very gradually improve<00:17:42.780> the<00:17:42.990> situation<00:17:43.140> but<00:17:44.810> yeah<00:17:45.810> now<00:17:46.050> due 00:17:46.580 --> 00:17:46.590 align:start position:0% improve the situation but yeah now due 00:17:46.590 --> 00:17:50.030 align:start position:0% improve the situation but yeah now due diligence<00:17:47.100> is<00:17:47.430> required<00:17:48.030> for<00:17:48.630> all<00:17:48.930> parties<00:17:49.830> I 00:17:50.030 --> 00:17:50.040 align:start position:0% diligence is required for all parties I 00:17:50.040 --> 00:17:56.330 align:start position:0% diligence is required for all parties I believe<00:17:54.110> so<00:17:55.110> I<00:17:55.140> see<00:17:55.440> there<00:17:55.740> as<00:17:55.890> sort<00:17:56.130> of<00:17:56.160> being 00:17:56.330 --> 00:17:56.340 align:start position:0% believe so I see there as sort of being 00:17:56.340 --> 00:17:58.220 align:start position:0% believe so I see there as sort of being two<00:17:56.610> pushes<00:17:56.850> that<00:17:57.060> need<00:17:57.240> to<00:17:57.330> happen<00:17:57.480> one<00:17:58.200> of 00:17:58.220 --> 00:17:58.230 align:start position:0% two pushes that need to happen one of 00:17:58.230 --> 00:18:00.200 align:start position:0% two pushes that need to happen one of them<00:17:58.410> is<00:17:58.560> bottom<00:17:58.890> up<00:17:59.010> the<00:17:59.250> users<00:17:59.880> need<00:18:00.180> to 00:18:00.200 --> 00:18:00.210 align:start position:0% them is bottom up the users need to 00:18:00.210 --> 00:18:02.570 align:start position:0% them is bottom up the users need to really<00:18:00.540> start<00:18:00.750> demanding<00:18:01.050> that<00:18:01.620> if<00:18:01.920> there<00:18:02.430> are 00:18:02.570 --> 00:18:02.580 align:start position:0% really start demanding that if there are 00:18:02.580 --> 00:18:04.400 align:start position:0% really start demanding that if there are techniques<00:18:03.000> available<00:18:03.300> to<00:18:03.750> ensure<00:18:04.110> the 00:18:04.400 --> 00:18:04.410 align:start position:0% techniques available to ensure the 00:18:04.410 --> 00:18:05.540 align:start position:0% techniques available to ensure the correctness<00:18:04.710> of<00:18:04.890> that<00:18:04.950> kind<00:18:05.250> of<00:18:05.370> their 00:18:05.540 --> 00:18:05.550 align:start position:0% correctness of that kind of their 00:18:05.550 --> 00:18:07.610 align:start position:0% correctness of that kind of their contracts<00:18:05.970> they're<00:18:06.450> either<00:18:06.630> used<00:18:07.020> or<00:18:07.350> a<00:18:07.380> good 00:18:07.610 --> 00:18:07.620 align:start position:0% contracts they're either used or a good 00:18:07.620 --> 00:18:09.020 align:start position:0% contracts they're either used or a good justification<00:18:07.920> is<00:18:08.370> provided<00:18:08.790> for<00:18:08.910> why 00:18:09.020 --> 00:18:09.030 align:start position:0% justification is provided for why 00:18:09.030 --> 00:18:11.180 align:start position:0% justification is provided for why they're<00:18:09.180> not<00:18:09.300> used<00:18:09.540> We<00:18:10.290> certainly<00:18:10.440> have<00:18:10.710> a<00:18:10.920> few 00:18:11.180 --> 00:18:11.190 align:start position:0% they're not used We certainly have a few 00:18:11.190 --> 00:18:12.980 align:start position:0% they're not used We certainly have a few tools<00:18:11.430> right<00:18:11.700> now<00:18:11.730> we've<00:18:12.060> seen<00:18:12.300> presentations 00:18:12.980 --> 00:18:12.990 align:start position:0% tools right now we've seen presentations 00:18:12.990 --> 00:18:16.460 align:start position:0% tools right now we've seen presentations today<00:18:13.620> about<00:18:13.860> quite<00:18:14.190> a<00:18:14.250> few<00:18:14.310> of<00:18:14.550> them<00:18:15.050> so<00:18:16.050> so 00:18:16.460 --> 00:18:16.470 align:start position:0% today about quite a few of them so so 00:18:16.470 --> 00:18:17.990 align:start position:0% today about quite a few of them so so users<00:18:16.830> really<00:18:17.070> need<00:18:17.280> to<00:18:17.370> start<00:18:17.550> being<00:18:17.760> more 00:18:17.990 --> 00:18:18.000 align:start position:0% users really need to start being more 00:18:18.000 --> 00:18:19.400 align:start position:0% users really need to start being more selective<00:18:18.210> about<00:18:18.750> where<00:18:18.990> they<00:18:19.110> put<00:18:19.290> their 00:18:19.400 --> 00:18:19.410 align:start position:0% selective about where they put their 00:18:19.410 --> 00:18:21.800 align:start position:0% selective about where they put their money<00:18:19.620> and<00:18:20.250> well<00:18:20.610> sure<00:18:20.940> it's<00:18:21.150> tempting<00:18:21.480> to 00:18:21.800 --> 00:18:21.810 align:start position:0% money and well sure it's tempting to 00:18:21.810 --> 00:18:23.690 align:start position:0% money and well sure it's tempting to sort<00:18:21.990> of<00:18:22.050> buy<00:18:22.260> into<00:18:22.440> every<00:18:22.620> single<00:18:22.890> ICO<00:18:23.310> and 00:18:23.690 --> 00:18:23.700 align:start position:0% sort of buy into every single ICO and 00:18:23.700 --> 00:18:26.270 align:start position:0% sort of buy into every single ICO and flip<00:18:23.940> it<00:18:23.970> for<00:18:24.240> 2x<00:18:24.630> or<00:18:24.840> whatever<00:18:25.160> that's<00:18:26.160> not 00:18:26.270 --> 00:18:26.280 align:start position:0% flip it for 2x or whatever that's not 00:18:26.280 --> 00:18:28.490 align:start position:0% flip it for 2x or whatever that's not the<00:18:26.580> kind<00:18:26.790> of<00:18:26.940> space<00:18:27.270> that<00:18:27.440> sort<00:18:28.440> of 00:18:28.490 --> 00:18:28.500 align:start position:0% the kind of space that sort of 00:18:28.500 --> 00:18:31.520 align:start position:0% the kind of space that sort of incentivizes<00:18:29.400> and<00:18:29.580> fosters<00:18:30.080> rigorous<00:18:31.080> proper 00:18:31.520 --> 00:18:31.530 align:start position:0% incentivizes and fosters rigorous proper 00:18:31.530 --> 00:18:33.680 align:start position:0% incentivizes and fosters rigorous proper software<00:18:31.950> development<00:18:32.400> and<00:18:33.330> so<00:18:33.540> I<00:18:33.570> think 00:18:33.680 --> 00:18:33.690 align:start position:0% software development and so I think 00:18:33.690 --> 00:18:35.510 align:start position:0% software development and so I think users<00:18:34.050> and<00:18:34.350> investors<00:18:34.740> need<00:18:35.010> to<00:18:35.100> become<00:18:35.370> more 00:18:35.510 --> 00:18:35.520 align:start position:0% users and investors need to become more 00:18:35.520 --> 00:18:37.340 align:start position:0% users and investors need to become more selective<00:18:35.730> and<00:18:36.210> and<00:18:36.480> developers<00:18:37.110> need<00:18:37.320> to 00:18:37.340 --> 00:18:37.350 align:start position:0% selective and and developers need to 00:18:37.350 --> 00:18:40.100 align:start position:0% selective and and developers need to sort<00:18:37.650> of<00:18:37.740> enable<00:18:38.040> them<00:18:38.340> to<00:18:38.370> do<00:18:38.670> that<00:18:38.870> by<00:18:39.870> really 00:18:40.100 --> 00:18:40.110 align:start position:0% sort of enable them to do that by really 00:18:40.110 --> 00:18:42.920 align:start position:0% sort of enable them to do that by really going<00:18:41.010> through<00:18:41.190> the<00:18:41.310> processes<00:18:41.700> in<00:18:42.660> a<00:18:42.780> way 00:18:42.920 --> 00:18:42.930 align:start position:0% going through the processes in a way 00:18:42.930 --> 00:18:45.230 align:start position:0% going through the processes in a way that's<00:18:43.230> serious<00:18:44.070> and<00:18:44.430> in<00:18:44.580> a<00:18:44.640> way<00:18:44.760> that<00:18:44.940> they 00:18:45.230 --> 00:18:45.240 align:start position:0% that's serious and in a way that they 00:18:45.240 --> 00:18:47.390 align:start position:0% that's serious and in a way that they put<00:18:45.420> in<00:18:45.540> a<00:18:45.600> concerted<00:18:45.960> effort<00:18:46.200> to<00:18:46.650> get<00:18:47.280> the 00:18:47.390 --> 00:18:47.400 align:start position:0% put in a concerted effort to get the 00:18:47.400 --> 00:18:49.960 align:start position:0% put in a concerted effort to get the maximum<00:18:47.820> assurance<00:18:48.180> out<00:18:48.300> of<00:18:48.390> their<00:18:48.480> contracts 00:18:49.960 --> 00:18:49.970 align:start position:0% maximum assurance out of their contracts 00:18:49.970 --> 00:18:51.200 align:start position:0% maximum assurance out of their contracts Thanks 00:18:51.200 --> 00:18:51.210 align:start position:0% Thanks 00:18:51.210 --> 00:18:53.630 align:start position:0% Thanks yeah<00:18:51.720> kind<00:18:51.990> of<00:18:52.050> echoing<00:18:52.620> what<00:18:52.890> you<00:18:53.040> said<00:18:53.610> a 00:18:53.630 --> 00:18:53.640 align:start position:0% yeah kind of echoing what you said a 00:18:53.640 --> 00:18:55.040 align:start position:0% yeah kind of echoing what you said a little<00:18:53.760> bit<00:18:53.910> you<00:18:54.210> know<00:18:54.240> no<00:18:54.540> amount<00:18:54.780> of<00:18:54.870> money 00:18:55.040 --> 00:18:55.050 align:start position:0% little bit you know no amount of money 00:18:55.050 --> 00:18:56.780 align:start position:0% little bit you know no amount of money as<00:18:55.200> a<00:18:55.230> substitute<00:18:55.800> for<00:18:55.830> just<00:18:56.010> understanding 00:18:56.780 --> 00:18:56.790 align:start position:0% as a substitute for just understanding 00:18:56.790 --> 00:18:59.270 align:start position:0% as a substitute for just understanding right<00:18:57.180> so<00:18:57.450> at<00:18:58.290> some<00:18:58.440> point<00:18:58.710> you<00:18:58.800> just<00:18:58.830> have<00:18:59.040> to 00:18:59.270 --> 00:18:59.280 align:start position:0% right so at some point you just have to 00:18:59.280 --> 00:19:01.000 align:start position:0% right so at some point you just have to read<00:18:59.700> and<00:18:59.880> understand<00:19:00.270> the<00:19:00.360> bytecode<00:19:00.540> and 00:19:01.000 --> 00:19:01.010 align:start position:0% read and understand the bytecode and 00:19:01.010 --> 00:19:03.290 align:start position:0% read and understand the bytecode and understand<00:19:02.010> how<00:19:02.160> EVM<00:19:02.520> works<00:19:02.730> and<00:19:02.940> understand 00:19:03.290 --> 00:19:03.300 align:start position:0% understand how EVM works and understand 00:19:03.300 --> 00:19:05.030 align:start position:0% understand how EVM works and understand hustle<00:19:03.600> it<00:19:03.690> D<00:19:03.810> compiles<00:19:04.230> to<00:19:04.260> EVM<00:19:04.620> or<00:19:04.800> whatever 00:19:05.030 --> 00:19:05.040 align:start position:0% hustle it D compiles to EVM or whatever 00:19:05.040 --> 00:19:06.350 align:start position:0% hustle it D compiles to EVM or whatever tool<00:19:05.280> it<00:19:05.430> is<00:19:05.520> whatever<00:19:06.000> high<00:19:06.090> level 00:19:06.350 --> 00:19:06.360 align:start position:0% tool it is whatever high level 00:19:06.360 --> 00:19:07.940 align:start position:0% tool it is whatever high level programming<00:19:06.660> language<00:19:07.020> you're<00:19:07.140> using<00:19:07.200> how<00:19:07.830> it 00:19:07.940 --> 00:19:07.950 align:start position:0% programming language you're using how it 00:19:07.950 --> 00:19:09.650 align:start position:0% programming language you're using how it compiles<00:19:08.340> DBM<00:19:08.700> and<00:19:08.730> what<00:19:09.000> the<00:19:09.090> implications 00:19:09.650 --> 00:19:09.660 align:start position:0% compiles DBM and what the implications 00:19:09.660 --> 00:19:12.740 align:start position:0% compiles DBM and what the implications for<00:19:09.810> security<00:19:10.260> are<00:19:10.550> in<00:19:11.550> that<00:19:11.760> setting<00:19:12.090> and<00:19:12.240> you 00:19:12.740 --> 00:19:12.750 align:start position:0% for security are in that setting and you 00:19:12.750 --> 00:19:14.210 align:start position:0% for security are in that setting and you know<00:19:12.870> the<00:19:12.990> people<00:19:13.080> doing<00:19:13.380> security<00:19:13.800> audits 00:19:14.210 --> 00:19:14.220 align:start position:0% know the people doing security audits 00:19:14.220 --> 00:19:16.010 align:start position:0% know the people doing security audits they<00:19:14.670> understand<00:19:15.150> this<00:19:15.330> really<00:19:15.630> well<00:19:15.780> and 00:19:16.010 --> 00:19:16.020 align:start position:0% they understand this really well and 00:19:16.020 --> 00:19:18.050 align:start position:0% they understand this really well and they<00:19:16.470> like<00:19:17.280> they<00:19:17.400> were<00:19:17.490> saying<00:19:17.670> earlier<00:19:18.000> you 00:19:18.050 --> 00:19:18.060 align:start position:0% they like they were saying earlier you 00:19:18.060 --> 00:19:19.550 align:start position:0% they like they were saying earlier you know<00:19:18.300> they<00:19:18.450> just<00:19:18.630> read<00:19:18.810> the<00:19:18.900> code<00:19:19.080> and<00:19:19.110> read<00:19:19.470> it 00:19:19.550 --> 00:19:19.560 align:start position:0% know they just read the code and read it 00:19:19.560 --> 00:19:20.930 align:start position:0% know they just read the code and read it again<00:19:19.770> and<00:19:19.830> read<00:19:20.190> it<00:19:20.280> again<00:19:20.520> and<00:19:20.730> read<00:19:20.850> it 00:19:20.930 --> 00:19:20.940 align:start position:0% again and read it again and read it 00:19:20.940 --> 00:19:22.700 align:start position:0% again and read it again and read it again<00:19:21.030> you<00:19:21.480> know<00:19:21.570> there's<00:19:21.780> no<00:19:21.930> substitute<00:19:22.680> for 00:19:22.700 --> 00:19:22.710 align:start position:0% again you know there's no substitute for 00:19:22.710 --> 00:19:25.670 align:start position:0% again you know there's no substitute for just<00:19:22.980> putting<00:19:23.100> time<00:19:23.430> and<00:19:23.700> effort<00:19:24.030> into<00:19:24.680> you 00:19:25.670 --> 00:19:25.680 align:start position:0% just putting time and effort into you 00:19:25.680 --> 00:19:32.060 align:start position:0% just putting time and effort into you know<00:19:25.800> high<00:19:25.980> assurance<00:19:26.100> software<00:19:31.040> well<00:19:32.040> I 00:19:32.060 --> 00:19:32.070 align:start position:0% know high assurance software well I 00:19:32.070 --> 00:19:33.830 align:start position:0% know high assurance software well I guess<00:19:32.340> you<00:19:32.580> know<00:19:32.670> in<00:19:32.940> order<00:19:33.150> to<00:19:33.300> make<00:19:33.450> formal 00:19:33.830 --> 00:19:33.840 align:start position:0% guess you know in order to make formal 00:19:33.840 --> 00:19:36.890 align:start position:0% guess you know in order to make formal verification<00:19:34.760> popular<00:19:35.760> I<00:19:35.790> think<00:19:35.940> we<00:19:36.570> need<00:19:36.720> to 00:19:36.890 --> 00:19:36.900 align:start position:0% verification popular I think we need to 00:19:36.900 --> 00:19:41.270 align:start position:0% verification popular I think we need to adopt<00:19:37.740> this<00:19:37.830> first<00:19:38.220> right<00:19:38.810> so<00:19:39.810> I<00:19:40.080> mean<00:19:40.350> I<00:19:40.500> hope 00:19:41.270 --> 00:19:41.280 align:start position:0% adopt this first right so I mean I hope 00:19:41.280 --> 00:19:43.010 align:start position:0% adopt this first right so I mean I hope that<00:19:41.430> we<00:19:41.580> can<00:19:41.700> have<00:19:41.880> some<00:19:42.060> sort<00:19:42.210> of<00:19:42.330> like<00:19:42.510> ERC 00:19:43.010 --> 00:19:43.020 align:start position:0% that we can have some sort of like ERC 00:19:43.020 --> 00:19:45.650 align:start position:0% that we can have some sort of like ERC that<00:19:43.290> you<00:19:43.980> know<00:19:44.070> that<00:19:44.340> allows<00:19:45.180> you<00:19:45.570> know 00:19:45.650 --> 00:19:45.660 align:start position:0% that you know that allows you know 00:19:45.660 --> 00:19:47.540 align:start position:0% that you know that allows you know people<00:19:45.960> to<00:19:46.110> put<00:19:46.290> you<00:19:46.620> know<00:19:46.740> maybe<00:19:46.980> orientate 00:19:47.540 --> 00:19:47.550 align:start position:0% people to put you know maybe orientate 00:19:47.550 --> 00:19:50.000 align:start position:0% people to put you know maybe orientate half<00:19:47.790> Hydra<00:19:48.480> attack<00:19:48.600> or<00:19:49.110> you<00:19:49.170> know<00:19:49.470> KETV<00:19:49.920> on 00:19:50.000 --> 00:19:50.010 align:start position:0% half Hydra attack or you know KETV on 00:19:50.010 --> 00:19:52.700 align:start position:0% half Hydra attack or you know KETV on tap<00:19:50.250> into<00:19:50.880> every<00:19:51.060> single<00:19:51.390> smart<00:19:52.170> contractor 00:19:52.700 --> 00:19:52.710 align:start position:0% tap into every single smart contractor 00:19:52.710 --> 00:19:53.180 align:start position:0% tap into every single smart contractor has 00:19:53.180 --> 00:19:53.190 align:start position:0% has 00:19:53.190 --> 00:19:55.760 align:start position:0% has Ben<00:19:53.310> you<00:19:53.460> know<00:19:53.550> deploy<00:19:53.850> in<00:19:54.090> the<00:19:54.770> Italian 00:19:55.760 --> 00:19:55.770 align:start position:0% Ben you know deploy in the Italian 00:19:55.770 --> 00:20:02.120 align:start position:0% Ben you know deploy in the Italian blockchain<00:19:58.070> Thanks<00:20:00.530> so<00:20:01.530> anyone<00:20:01.800> from<00:20:01.980> the 00:20:02.120 --> 00:20:02.130 align:start position:0% blockchain Thanks so anyone from the 00:20:02.130 --> 00:20:03.110 align:start position:0% blockchain Thanks so anyone from the audience<00:20:02.400> would<00:20:02.580> like<00:20:02.700> to<00:20:02.760> ask<00:20:02.970> some 00:20:03.110 --> 00:20:03.120 align:start position:0% audience would like to ask some 00:20:03.120 --> 00:20:11.420 align:start position:0% audience would like to ask some questions<00:20:03.270> yes<00:20:09.530> maybe<00:20:10.530> it's<00:20:10.950> better<00:20:11.130> if 00:20:11.420 --> 00:20:11.430 align:start position:0% questions yes maybe it's better if 00:20:11.430 --> 00:20:14.240 align:start position:0% questions yes maybe it's better if people<00:20:12.180> with<00:20:12.360> questions<00:20:12.900> should<00:20:13.230> come<00:20:13.530> to<00:20:13.830> the 00:20:14.240 --> 00:20:14.250 align:start position:0% people with questions should come to the 00:20:14.250 --> 00:20:17.030 align:start position:0% people with questions should come to the front<00:20:15.080> that's<00:20:16.080> probably<00:20:16.410> a<00:20:16.470> good<00:20:16.560> idea<00:20:16.620> for 00:20:17.030 --> 00:20:17.040 align:start position:0% front that's probably a good idea for 00:20:17.040 --> 00:20:21.560 align:start position:0% front that's probably a good idea for the<00:20:17.160> next<00:20:17.280> person<00:20:19.460> so<00:20:20.460> from<00:20:21.090> an<00:20:21.210> artist 00:20:21.560 --> 00:20:21.570 align:start position:0% the next person so from an artist 00:20:21.570 --> 00:20:24.380 align:start position:0% the next person so from an artist standpoint<00:20:22.110> how<00:20:23.100> would<00:20:23.340> you<00:20:23.610> like<00:20:23.880> to<00:20:23.910> see 00:20:24.380 --> 00:20:24.390 align:start position:0% standpoint how would you like to see 00:20:24.390 --> 00:20:26.990 align:start position:0% standpoint how would you like to see people<00:20:25.170> who<00:20:25.290> provide<00:20:25.620> smart<00:20:26.130> contract<00:20:26.580> audits 00:20:26.990 --> 00:20:27.000 align:start position:0% people who provide smart contract audits 00:20:27.000 --> 00:20:29.450 align:start position:0% people who provide smart contract audits either<00:20:27.630> contributing<00:20:28.560> to<00:20:28.710> your<00:20:28.740> projects<00:20:29.310> or 00:20:29.450 --> 00:20:29.460 align:start position:0% either contributing to your projects or 00:20:29.460 --> 00:20:31.910 align:start position:0% either contributing to your projects or using<00:20:30.450> your<00:20:30.750> projects<00:20:31.200> I<00:20:31.290> assume<00:20:31.560> it's<00:20:31.740> sort 00:20:31.910 --> 00:20:31.920 align:start position:0% using your projects I assume it's sort 00:20:31.920 --> 00:20:34.340 align:start position:0% using your projects I assume it's sort of<00:20:32.090> maybe<00:20:33.090> one<00:20:33.300> or<00:20:33.450> the<00:20:33.540> other<00:20:33.660> but<00:20:33.930> maybe 00:20:34.340 --> 00:20:34.350 align:start position:0% of maybe one or the other but maybe 00:20:34.350 --> 00:20:37.820 align:start position:0% of maybe one or the other but maybe there's<00:20:34.590> both<00:20:34.830> for<00:20:35.310> us<00:20:35.430> right<00:20:35.670> now<00:20:36.800> does<00:20:37.800> that 00:20:37.820 --> 00:20:37.830 align:start position:0% there's both for us right now does that 00:20:37.830 --> 00:20:42.020 align:start position:0% there's both for us right now does that make<00:20:38.040> sense<00:20:38.210> yeah<00:20:39.350> I<00:20:40.350> do<00:20:40.770> do<00:20:41.310> some<00:20:41.730> smart 00:20:42.020 --> 00:20:42.030 align:start position:0% make sense yeah I do do some smart 00:20:42.030 --> 00:20:43.790 align:start position:0% make sense yeah I do do some smart contract<00:20:42.510> audits<00:20:42.840> and<00:20:43.020> I<00:20:43.110> would<00:20:43.230> say<00:20:43.410> ideally 00:20:43.790 --> 00:20:43.800 align:start position:0% contract audits and I would say ideally 00:20:43.800 --> 00:20:45.530 align:start position:0% contract audits and I would say ideally the<00:20:44.160> role<00:20:44.310> of<00:20:44.340> these<00:20:44.580> kinds<00:20:44.970> of<00:20:45.060> tools<00:20:45.240> in<00:20:45.480> the 00:20:45.530 --> 00:20:45.540 align:start position:0% the role of these kinds of tools in the 00:20:45.540 --> 00:20:47.480 align:start position:0% the role of these kinds of tools in the long<00:20:45.720> run<00:20:45.930> would<00:20:46.110> be<00:20:46.260> to<00:20:46.350> sort<00:20:46.530> of<00:20:46.650> put<00:20:46.980> most<00:20:47.190> of 00:20:47.480 --> 00:20:47.490 align:start position:0% long run would be to sort of put most of 00:20:47.490 --> 00:20:49.850 align:start position:0% long run would be to sort of put most of that<00:20:48.390> business<00:20:48.660> right<00:20:48.930> now<00:20:49.110> out<00:20:49.530> of<00:20:49.680> business 00:20:49.850 --> 00:20:49.860 align:start position:0% that business right now out of business 00:20:49.860 --> 00:20:51.470 align:start position:0% that business right now out of business to<00:20:50.190> an<00:20:50.280> extent<00:20:50.610> like<00:20:50.670> at<00:20:50.910> least<00:20:51.090> that's<00:20:51.300> my 00:20:51.470 --> 00:20:51.480 align:start position:0% to an extent like at least that's my 00:20:51.480 --> 00:20:54.350 align:start position:0% to an extent like at least that's my personal<00:20:51.870> go<00:20:52.020> with<00:20:52.200> it<00:20:52.380> in<00:20:53.190> all<00:20:53.640> my<00:20:53.850> audits<00:20:54.240> I 00:20:54.350 --> 00:20:54.360 align:start position:0% personal go with it in all my audits I 00:20:54.360 --> 00:20:56.090 align:start position:0% personal go with it in all my audits I always<00:20:54.720> make<00:20:55.050> recommendations<00:20:55.710> to<00:20:55.770> the<00:20:55.920> team 00:20:56.090 --> 00:20:56.100 align:start position:0% always make recommendations to the team 00:20:56.100 --> 00:20:57.380 align:start position:0% always make recommendations to the team about<00:20:56.400> which<00:20:56.700> tools<00:20:57.030> are<00:20:57.180> state-of-the-art 00:20:57.380 --> 00:20:57.390 align:start position:0% about which tools are state-of-the-art 00:20:57.390 --> 00:20:58.790 align:start position:0% about which tools are state-of-the-art and<00:20:57.810> what<00:20:57.900> they<00:20:58.020> should<00:20:58.200> be<00:20:58.320> running<00:20:58.560> on<00:20:58.680> their 00:20:58.790 --> 00:20:58.800 align:start position:0% and what they should be running on their 00:20:58.800 --> 00:21:02.330 align:start position:0% and what they should be running on their contracts<00:20:59.750> certainly<00:21:00.770> auditors<00:21:01.770> can<00:21:02.070> run 00:21:02.330 --> 00:21:02.340 align:start position:0% contracts certainly auditors can run 00:21:02.340 --> 00:21:04.160 align:start position:0% contracts certainly auditors can run these<00:21:02.490> tools<00:21:02.790> on<00:21:02.970> the<00:21:03.060> contracts<00:21:03.480> as<00:21:03.660> well<00:21:03.690> but 00:21:04.160 --> 00:21:04.170 align:start position:0% these tools on the contracts as well but 00:21:04.170 --> 00:21:05.540 align:start position:0% these tools on the contracts as well but at<00:21:04.290> the<00:21:04.410> end<00:21:04.440> of<00:21:04.650> the<00:21:04.740> day<00:21:04.890> my<00:21:05.130> personal 00:21:05.540 --> 00:21:05.550 align:start position:0% at the end of the day my personal 00:21:05.550 --> 00:21:06.560 align:start position:0% at the end of the day my personal opinion<00:21:05.880> is<00:21:06.030> that<00:21:06.180> it's<00:21:06.300> the<00:21:06.390> responsibility 00:21:06.560 --> 00:21:06.570 align:start position:0% opinion is that it's the responsibility 00:21:06.570 --> 00:21:10.250 align:start position:0% opinion is that it's the responsibility of<00:21:07.050> the<00:21:07.110> team<00:21:07.580> and<00:21:08.580> the<00:21:09.390> team<00:21:09.600> to<00:21:09.630> sort<00:21:09.960> of<00:21:10.050> seek 00:21:10.250 --> 00:21:10.260 align:start position:0% of the team and the team to sort of seek 00:21:10.260 --> 00:21:11.390 align:start position:0% of the team and the team to sort of seek help<00:21:10.470> when<00:21:10.680> they're<00:21:10.800> not<00:21:10.950> able<00:21:11.190> to<00:21:11.280> do 00:21:11.390 --> 00:21:11.400 align:start position:0% help when they're not able to do 00:21:11.400 --> 00:21:13.280 align:start position:0% help when they're not able to do something<00:21:11.730> like<00:21:11.820> this<00:21:12.050> especially<00:21:13.050> because 00:21:13.280 --> 00:21:13.290 align:start position:0% something like this especially because 00:21:13.290 --> 00:21:16.280 align:start position:0% something like this especially because you<00:21:14.070> know<00:21:14.190> most<00:21:14.730> teams<00:21:15.090> are<00:21:15.420> would<00:21:16.020> not<00:21:16.050> be 00:21:16.280 --> 00:21:16.290 align:start position:0% you know most teams are would not be 00:21:16.290 --> 00:21:18.560 align:start position:0% you know most teams are would not be willing<00:21:16.530> to<00:21:16.710> sort<00:21:17.100> of<00:21:17.160> pay<00:21:17.520> the<00:21:17.850> hourly<00:21:18.300> for<00:21:18.510> an 00:21:18.560 --> 00:21:18.570 align:start position:0% willing to sort of pay the hourly for an 00:21:18.570 --> 00:21:20.660 align:start position:0% willing to sort of pay the hourly for an auditor<00:21:18.900> to<00:21:19.140> run<00:21:19.320> security<00:21:19.980> on<00:21:20.160> their<00:21:20.280> code<00:21:20.490> or 00:21:20.660 --> 00:21:20.670 align:start position:0% auditor to run security on their code or 00:21:20.670 --> 00:21:21.650 align:start position:0% auditor to run security on their code or whatever<00:21:20.940> when<00:21:21.180> they<00:21:21.270> could<00:21:21.420> do<00:21:21.510> the<00:21:21.630> same 00:21:21.650 --> 00:21:21.660 align:start position:0% whatever when they could do the same 00:21:21.660 --> 00:21:23.870 align:start position:0% whatever when they could do the same thing<00:21:21.810> themselves<00:21:22.470> so<00:21:23.340> I<00:21:23.370> think<00:21:23.610> the<00:21:23.700> role<00:21:23.850> of 00:21:23.870 --> 00:21:23.880 align:start position:0% thing themselves so I think the role of 00:21:23.880 --> 00:21:25.790 align:start position:0% thing themselves so I think the role of auditors<00:21:24.450> to<00:21:24.870> answer<00:21:25.260> your<00:21:25.380> question<00:21:25.680> is<00:21:25.770> to 00:21:25.790 --> 00:21:25.800 align:start position:0% auditors to answer your question is to 00:21:25.800 --> 00:21:27.440 align:start position:0% auditors to answer your question is to sort<00:21:26.040> of<00:21:26.100> inform<00:21:26.580> the<00:21:26.760> team<00:21:26.940> about<00:21:27.240> what's 00:21:27.440 --> 00:21:27.450 align:start position:0% sort of inform the team about what's 00:21:27.450 --> 00:21:29.150 align:start position:0% sort of inform the team about what's available<00:21:27.570> and<00:21:28.140> what<00:21:28.350> they<00:21:28.530> think<00:21:28.590> could<00:21:29.010> be 00:21:29.150 --> 00:21:29.160 align:start position:0% available and what they think could be 00:21:29.160 --> 00:21:31.190 align:start position:0% available and what they think could be useful<00:21:29.280> for<00:21:29.520> the<00:21:29.700> contract<00:21:30.120> and<00:21:30.930> then<00:21:31.050> it's 00:21:31.190 --> 00:21:31.200 align:start position:0% useful for the contract and then it's 00:21:31.200 --> 00:21:32.930 align:start position:0% useful for the contract and then it's absolutely<00:21:31.710> the<00:21:31.740> team's<00:21:32.070> responsibility<00:21:32.490> to 00:21:32.930 --> 00:21:32.940 align:start position:0% absolutely the team's responsibility to 00:21:32.940 --> 00:21:35.380 align:start position:0% absolutely the team's responsibility to follow<00:21:33.120> up<00:21:33.360> on<00:21:33.480> that<00:21:33.720> and<00:21:33.900> put<00:21:33.960> the<00:21:34.200> time<00:21:34.470> in 00:21:35.380 --> 00:21:35.390 align:start position:0% follow up on that and put the time in 00:21:35.390 --> 00:21:37.880 align:start position:0% follow up on that and put the time in often<00:21:36.390> I<00:21:36.660> think<00:21:36.690> the<00:21:36.990> hardest<00:21:37.320> part<00:21:37.530> is<00:21:37.710> just 00:21:37.880 --> 00:21:37.890 align:start position:0% often I think the hardest part is just 00:21:37.890 --> 00:21:39.710 align:start position:0% often I think the hardest part is just the<00:21:38.010> spin<00:21:38.280> up<00:21:38.400> time<00:21:38.670> right<00:21:38.940> so<00:21:38.970> you<00:21:39.240> you<00:21:39.540> have 00:21:39.710 --> 00:21:39.720 align:start position:0% the spin up time right so you you have 00:21:39.720 --> 00:21:40.790 align:start position:0% the spin up time right so you you have some<00:21:39.900> new<00:21:40.050> tool<00:21:40.290> that<00:21:40.500> you're<00:21:40.590> trying<00:21:40.770> to 00:21:40.790 --> 00:21:40.800 align:start position:0% some new tool that you're trying to 00:21:40.800 --> 00:21:42.200 align:start position:0% some new tool that you're trying to bring<00:21:40.950> into<00:21:41.160> your<00:21:41.280> tool<00:21:41.430> chain<00:21:41.670> and<00:21:41.880> then<00:21:41.970> you 00:21:42.200 --> 00:21:42.210 align:start position:0% bring into your tool chain and then you 00:21:42.210 --> 00:21:43.400 align:start position:0% bring into your tool chain and then you know<00:21:42.360> it<00:21:42.450> maybe<00:21:42.600> takes<00:21:42.780> a<00:21:42.930> week<00:21:43.110> or<00:21:43.290> something 00:21:43.400 --> 00:21:43.410 align:start position:0% know it maybe takes a week or something 00:21:43.410 --> 00:21:45.560 align:start position:0% know it maybe takes a week or something to<00:21:43.800> get<00:21:44.040> it<00:21:44.160> fully<00:21:44.340> integrated<00:21:44.910> and<00:21:45.060> get<00:21:45.180> it<00:21:45.300> to 00:21:45.560 --> 00:21:45.570 align:start position:0% to get it fully integrated and get it to 00:21:45.570 --> 00:21:47.810 align:start position:0% to get it fully integrated and get it to be<00:21:45.690> seamless<00:21:45.930> but<00:21:46.410> once<00:21:47.070> you<00:21:47.190> have<00:21:47.340> that<00:21:47.460> spin 00:21:47.810 --> 00:21:47.820 align:start position:0% be seamless but once you have that spin 00:21:47.820 --> 00:21:49.400 align:start position:0% be seamless but once you have that spin up<00:21:47.940> time<00:21:48.150> taken<00:21:48.510> care<00:21:48.690> of<00:21:48.720> then<00:21:48.960> you<00:21:49.050> can<00:21:49.200> kind 00:21:49.400 --> 00:21:49.410 align:start position:0% up time taken care of then you can kind 00:21:49.410 --> 00:21:51.410 align:start position:0% up time taken care of then you can kind of<00:21:49.470> begin<00:21:49.620> to<00:21:49.830> make<00:21:49.980> incremental<00:21:50.400> progress<00:21:50.880> so 00:21:51.410 --> 00:21:51.420 align:start position:0% of begin to make incremental progress so 00:21:51.420 --> 00:21:53.660 align:start position:0% of begin to make incremental progress so what<00:21:52.020> I<00:21:52.050> would<00:21:52.170> like<00:21:52.350> to<00:21:52.470> see<00:21:52.620> is<00:21:52.770> people 00:21:53.660 --> 00:21:53.670 align:start position:0% what I would like to see is people 00:21:53.670 --> 00:21:55.250 align:start position:0% what I would like to see is people taking<00:21:54.000> the<00:21:54.180> case<00:21:54.360> semantics<00:21:54.840> and<00:21:54.930> making 00:21:55.250 --> 00:21:55.260 align:start position:0% taking the case semantics and making 00:21:55.260 --> 00:21:57.320 align:start position:0% taking the case semantics and making extensions<00:21:56.040> of<00:21:56.190> it<00:21:56.340> so<00:21:56.520> we<00:21:56.640> have<00:21:56.790> already 00:21:57.320 --> 00:21:57.330 align:start position:0% extensions of it so we have already 00:21:57.330 --> 00:21:59.990 align:start position:0% extensions of it so we have already several<00:21:57.960> extensions<00:21:58.380> one<00:21:58.830> is<00:21:59.160> a<00:21:59.220> small<00:21:59.730> gas 00:21:59.990 --> 00:22:00.000 align:start position:0% several extensions one is a small gas 00:22:00.000 --> 00:22:03.050 align:start position:0% several extensions one is a small gas analysis<00:22:00.510> tool<00:22:00.720> that's<00:22:00.960> not<00:22:01.760> very<00:22:02.760> feature 00:22:03.050 --> 00:22:03.060 align:start position:0% analysis tool that's not very feature 00:22:03.060 --> 00:22:05.150 align:start position:0% analysis tool that's not very feature full<00:22:03.360> or<00:22:03.630> very<00:22:03.870> complete<00:22:04.290> or<00:22:04.470> sound<00:22:04.770> it<00:22:04.980> just 00:22:05.150 --> 00:22:05.160 align:start position:0% full or very complete or sound it just 00:22:05.160 --> 00:22:06.320 align:start position:0% full or very complete or sound it just kind<00:22:05.340> of<00:22:05.370> gives<00:22:05.550> a<00:22:05.640> rough<00:22:05.760> estimate 00:22:06.320 --> 00:22:06.330 align:start position:0% kind of gives a rough estimate 00:22:06.330 --> 00:22:07.549 align:start position:0% kind of gives a rough estimate but<00:22:06.419> it'd<00:22:06.539> be<00:22:06.570> nice<00:22:06.779> to<00:22:06.990> kind<00:22:07.169> of<00:22:07.200> tighten<00:22:07.380> the 00:22:07.549 --> 00:22:07.559 align:start position:0% but it'd be nice to kind of tighten the 00:22:07.559 --> 00:22:10.519 align:start position:0% but it'd be nice to kind of tighten the screws<00:22:07.799> on<00:22:07.950> that<00:22:08.480> and<00:22:09.480> then<00:22:09.659> there's<00:22:09.929> another 00:22:10.519 --> 00:22:10.529 align:start position:0% screws on that and then there's another 00:22:10.529 --> 00:22:13.009 align:start position:0% screws on that and then there's another tool<00:22:11.250> called<00:22:11.820> EVM<00:22:12.210> prime<00:22:12.450> which<00:22:12.659> is<00:22:12.779> just<00:22:12.960> a 00:22:13.009 --> 00:22:13.019 align:start position:0% tool called EVM prime which is just a 00:22:13.019 --> 00:22:15.560 align:start position:0% tool called EVM prime which is just a small<00:22:13.140> extension<00:22:13.590> of<00:22:13.860> the<00:22:14.039> EVM<00:22:14.760> semantics<00:22:15.330> to 00:22:15.560 --> 00:22:15.570 align:start position:0% small extension of the EVM semantics to 00:22:15.570 --> 00:22:16.909 align:start position:0% small extension of the EVM semantics to a<00:22:15.600> higher-level<00:22:15.899> language<00:22:16.500> and<00:22:16.649> if<00:22:16.710> people 00:22:16.909 --> 00:22:16.919 align:start position:0% a higher-level language and if people 00:22:16.919 --> 00:22:18.080 align:start position:0% a higher-level language and if people wanted<00:22:17.100> to<00:22:17.159> hack<00:22:17.340> on<00:22:17.519> that<00:22:17.730> that<00:22:17.909> would<00:22:18.000> be 00:22:18.080 --> 00:22:18.090 align:start position:0% wanted to hack on that that would be 00:22:18.090 --> 00:22:19.549 align:start position:0% wanted to hack on that that would be really<00:22:18.179> cool<00:22:18.450> I'm<00:22:18.720> answering<00:22:19.049> specifically 00:22:19.549 --> 00:22:19.559 align:start position:0% really cool I'm answering specifically 00:22:19.559 --> 00:22:22.370 align:start position:0% really cool I'm answering specifically for<00:22:19.740> KTM<00:22:20.220> because<00:22:20.809> that's<00:22:21.809> you<00:22:22.169> know<00:22:22.260> the 00:22:22.370 --> 00:22:22.380 align:start position:0% for KTM because that's you know the 00:22:22.380 --> 00:22:24.529 align:start position:0% for KTM because that's you know the project<00:22:22.559> I'm<00:22:22.799> working<00:22:22.830> on<00:22:23.269> but<00:22:24.269> there's<00:22:24.419> all 00:22:24.529 --> 00:22:24.539 align:start position:0% project I'm working on but there's all 00:22:24.539 --> 00:22:25.909 align:start position:0% project I'm working on but there's all sorts<00:22:24.750> of<00:22:24.809> other<00:22:24.929> analysis<00:22:25.470> tools<00:22:25.679> you<00:22:25.799> can 00:22:25.909 --> 00:22:25.919 align:start position:0% sorts of other analysis tools you can 00:22:25.919 --> 00:22:28.009 align:start position:0% sorts of other analysis tools you can write<00:22:26.039> directly<00:22:26.340> in<00:22:26.610> K<00:22:26.880> itself<00:22:27.690> as<00:22:27.899> an 00:22:28.009 --> 00:22:28.019 align:start position:0% write directly in K itself as an 00:22:28.019 --> 00:22:29.419 align:start position:0% write directly in K itself as an extension<00:22:28.289> language<00:22:28.710> and<00:22:28.830> the<00:22:28.890> hard<00:22:29.070> part<00:22:29.220> is 00:22:29.419 --> 00:22:29.429 align:start position:0% extension language and the hard part is 00:22:29.429 --> 00:22:32.240 align:start position:0% extension language and the hard part is the<00:22:29.549> spin<00:22:29.760> up<00:22:29.850> time<00:22:30.059> on<00:22:30.240> K<00:22:30.510> of<00:22:30.750> course<00:22:31.440> but<00:22:31.769> you 00:22:32.240 --> 00:22:32.250 align:start position:0% the spin up time on K of course but you 00:22:32.250 --> 00:22:34.460 align:start position:0% the spin up time on K of course but you know<00:22:32.370> there's<00:22:32.730> no<00:22:32.909> there's<00:22:33.870> no<00:22:33.929> avoiding<00:22:34.200> now 00:22:34.460 --> 00:22:34.470 align:start position:0% know there's no there's no avoiding now 00:22:34.470 --> 00:22:37.940 align:start position:0% know there's no there's no avoiding now with<00:22:34.710> a<00:22:34.769> project<00:22:35.190> like<00:22:35.309> that<00:22:35.340> so<00:22:35.820> yeah<00:22:36.890> just<00:22:37.890> to 00:22:37.940 --> 00:22:37.950 align:start position:0% with a project like that so yeah just to 00:22:37.950 --> 00:22:40.639 align:start position:0% with a project like that so yeah just to butt<00:22:38.159> in<00:22:38.279> just<00:22:38.909> for<00:22:39.029> one<00:22:39.149> second<00:22:39.539> it<00:22:40.320> would<00:22:40.470> be 00:22:40.639 --> 00:22:40.649 align:start position:0% butt in just for one second it would be 00:22:40.649 --> 00:22:42.350 align:start position:0% butt in just for one second it would be really<00:22:40.769> nice<00:22:40.980> also<00:22:41.250> if<00:22:41.490> these<00:22:41.669> auditors<00:22:42.090> and 00:22:42.350 --> 00:22:42.360 align:start position:0% really nice also if these auditors and 00:22:42.360 --> 00:22:43.549 align:start position:0% really nice also if these auditors and these<00:22:42.450> teams<00:22:42.659> sort<00:22:42.899> of<00:22:42.990> complained<00:22:43.350> a<00:22:43.470> lot 00:22:43.549 --> 00:22:43.559 align:start position:0% these teams sort of complained a lot 00:22:43.559 --> 00:22:50.120 align:start position:0% these teams sort of complained a lot more<00:22:43.769> about<00:22:43.980> the<00:22:44.130> tools<00:22:47.240> yeah<00:22:48.350> so<00:22:49.350> so<00:22:49.590> far<00:22:49.860> most 00:22:50.120 --> 00:22:50.130 align:start position:0% more about the tools yeah so so far most 00:22:50.130 --> 00:22:53.360 align:start position:0% more about the tools yeah so so far most of<00:22:50.309> the<00:22:50.490> research<00:22:51.830> focused<00:22:52.830> around<00:22:53.159> either 00:22:53.360 --> 00:22:53.370 align:start position:0% of the research focused around either 00:22:53.370 --> 00:22:55.940 align:start position:0% of the research focused around either talk<00:22:53.789> or<00:22:54.029> Krauser<00:22:54.720> which<00:22:55.169> are<00:22:55.409> relatively 00:22:55.940 --> 00:22:55.950 align:start position:0% talk or Krauser which are relatively 00:22:55.950 --> 00:22:58.759 align:start position:0% talk or Krauser which are relatively smaller<00:22:56.490> size<00:22:56.880> and<00:22:57.179> they<00:22:57.659> off<00:22:57.840> also<00:22:58.590> it's 00:22:58.759 --> 00:22:58.769 align:start position:0% smaller size and they off also it's 00:22:58.769 --> 00:23:03.200 align:start position:0% smaller size and they off also it's quite<00:22:58.950> similar<00:22:59.370> but<00:23:00.299> as<00:23:01.100> more<00:23:02.100> more<00:23:02.549> companies 00:23:03.200 --> 00:23:03.210 align:start position:0% quite similar but as more more companies 00:23:03.210 --> 00:23:06.680 align:start position:0% quite similar but as more more companies start<00:23:04.200> delivering<00:23:05.190> the<00:23:05.580> product<00:23:06.029> which<00:23:06.450> they 00:23:06.680 --> 00:23:06.690 align:start position:0% start delivering the product which they 00:23:06.690 --> 00:23:10.009 align:start position:0% start delivering the product which they promised<00:23:07.139> today<00:23:07.799> based<00:23:08.519> on<00:23:08.669> the<00:23:08.820> funding<00:23:09.480> the 00:23:10.009 --> 00:23:10.019 align:start position:0% promised today based on the funding the 00:23:10.019 --> 00:23:11.600 align:start position:0% promised today based on the funding the sides<00:23:10.320> gonna<00:23:10.500> be<00:23:10.649> a<00:23:10.679> lot<00:23:10.919> bigger<00:23:11.159> and<00:23:11.309> the 00:23:11.600 --> 00:23:11.610 align:start position:0% sides gonna be a lot bigger and the 00:23:11.610 --> 00:23:14.269 align:start position:0% sides gonna be a lot bigger and the product<00:23:12.120> will<00:23:12.269> be<00:23:12.330> quite<00:23:12.840> diverse<00:23:13.320> what<00:23:14.010> would 00:23:14.269 --> 00:23:14.279 align:start position:0% product will be quite diverse what would 00:23:14.279 --> 00:23:15.799 align:start position:0% product will be quite diverse what would be<00:23:14.490> the<00:23:14.639> challenge<00:23:15.059> when<00:23:15.299> it<00:23:15.419> comes<00:23:15.630> to 00:23:15.799 --> 00:23:15.809 align:start position:0% be the challenge when it comes to 00:23:15.809 --> 00:23:18.860 align:start position:0% be the challenge when it comes to verifying<00:23:16.380> these<00:23:16.679> actual<00:23:17.610> product<00:23:18.059> rather 00:23:18.860 --> 00:23:18.870 align:start position:0% verifying these actual product rather 00:23:18.870 --> 00:23:23.029 align:start position:0% verifying these actual product rather than<00:23:18.990> I<00:23:19.350> talk<00:23:19.769> in<00:23:19.980> the<00:23:20.070> crowd<00:23:20.250> sales<00:23:22.039> this 00:23:23.029 --> 00:23:23.039 align:start position:0% than I talk in the crowd sales this 00:23:23.039 --> 00:23:29.659 align:start position:0% than I talk in the crowd sales this quick<00:23:23.370> answer<00:23:23.850> because<00:23:24.120> we<00:23:24.210> need<00:23:24.360> to<00:23:28.669> sorry 00:23:29.659 --> 00:23:29.669 align:start position:0% quick answer because we need to sorry 00:23:29.669 --> 00:23:31.220 align:start position:0% quick answer because we need to sorry the<00:23:29.820> question<00:23:29.970> was<00:23:30.149> what<00:23:30.419> are<00:23:30.450> the<00:23:30.659> challenges 00:23:31.220 --> 00:23:31.230 align:start position:0% the question was what are the challenges 00:23:31.230 --> 00:23:32.690 align:start position:0% the question was what are the challenges for<00:23:31.260> these<00:23:31.590> teams<00:23:31.860> that<00:23:32.010> are<00:23:32.250> using<00:23:32.610> these 00:23:32.690 --> 00:23:32.700 align:start position:0% for these teams that are using these 00:23:32.700 --> 00:23:37.250 align:start position:0% for these teams that are using these tools<00:23:33.000> mostly<00:23:35.480> it's<00:23:36.480> better<00:23:36.720> without<00:23:36.870> the<00:23:37.110> mic 00:23:37.250 --> 00:23:37.260 align:start position:0% tools mostly it's better without the mic 00:23:37.260 --> 00:23:53.350 align:start position:0% tools mostly it's better without the mic actually<00:23:37.620> I<00:23:37.679> think 00:23:53.350 --> 00:23:53.360 align:start position:0% 00:23:53.360 --> 00:23:55.880 align:start position:0% yeah<00:23:54.360> yeah<00:23:54.510> so<00:23:54.810> so<00:23:55.440> yeah<00:23:55.560> that's<00:23:55.740> a<00:23:55.800> great 00:23:55.880 --> 00:23:55.890 align:start position:0% yeah yeah so so yeah that's a great 00:23:55.890 --> 00:23:57.740 align:start position:0% yeah yeah so so yeah that's a great question<00:23:55.980> so<00:23:56.760> the<00:23:56.850> question<00:23:56.880> was<00:23:57.240> about<00:23:57.480> like 00:23:57.740 --> 00:23:57.750 align:start position:0% question so the question was about like 00:23:57.750 --> 00:23:59.420 align:start position:0% question so the question was about like most<00:23:57.990> of<00:23:58.140> the<00:23:58.230> verification<00:23:58.560> right<00:23:58.980> now<00:23:59.160> is 00:23:59.420 --> 00:23:59.430 align:start position:0% most of the verification right now is 00:23:59.430 --> 00:24:01.640 align:start position:0% most of the verification right now is tokens<00:24:00.030> or<00:24:00.180> crowd<00:24:00.420> sales<00:24:00.690> because<00:24:01.470> that's 00:24:01.640 --> 00:24:01.650 align:start position:0% tokens or crowd sales because that's 00:24:01.650 --> 00:24:02.810 align:start position:0% tokens or crowd sales because that's sort<00:24:01.830> of<00:24:01.860> what<00:24:02.010> everyone<00:24:02.250> is<00:24:02.310> doing<00:24:02.370> and<00:24:02.670> it's 00:24:02.810 --> 00:24:02.820 align:start position:0% sort of what everyone is doing and it's 00:24:02.820 --> 00:24:04.160 align:start position:0% sort of what everyone is doing and it's all<00:24:02.970> the<00:24:03.090> same<00:24:03.270> but<00:24:03.510> what<00:24:03.660> about<00:24:03.840> when<00:24:03.990> we<00:24:04.020> get 00:24:04.160 --> 00:24:04.170 align:start position:0% all the same but what about when we get 00:24:04.170 --> 00:24:06.710 align:start position:0% all the same but what about when we get more<00:24:04.350> complicated<00:24:04.740> contracts<00:24:05.400> I<00:24:06.150> personally 00:24:06.710 --> 00:24:06.720 align:start position:0% more complicated contracts I personally 00:24:06.720 --> 00:24:07.880 align:start position:0% more complicated contracts I personally think<00:24:06.900> people<00:24:07.170> are<00:24:07.260> always<00:24:07.470> going<00:24:07.590> to<00:24:07.650> sort<00:24:07.860> of 00:24:07.880 --> 00:24:07.890 align:start position:0% think people are always going to sort of 00:24:07.890 --> 00:24:09.800 align:start position:0% think people are always going to sort of push<00:24:08.130> the<00:24:08.250> envelope<00:24:08.280> and<00:24:08.880> do<00:24:09.210> things<00:24:09.570> that<00:24:09.690> are 00:24:09.800 --> 00:24:09.810 align:start position:0% push the envelope and do things that are 00:24:09.810 --> 00:24:11.360 align:start position:0% push the envelope and do things that are more<00:24:09.840> complicated<00:24:10.260> than<00:24:10.560> we<00:24:10.740> actually<00:24:10.860> can 00:24:11.360 --> 00:24:11.370 align:start position:0% more complicated than we actually can 00:24:11.370 --> 00:24:13.730 align:start position:0% more complicated than we actually can verify<00:24:11.750> and<00:24:12.750> I<00:24:12.810> think<00:24:13.020> that's<00:24:13.170> really<00:24:13.320> cool<00:24:13.590> to 00:24:13.730 --> 00:24:13.740 align:start position:0% verify and I think that's really cool to 00:24:13.740 --> 00:24:15.530 align:start position:0% verify and I think that's really cool to sort<00:24:13.920> of<00:24:13.980> feedback<00:24:14.220> in<00:24:14.550> but<00:24:15.210> the<00:24:15.390> more 00:24:15.530 --> 00:24:15.540 align:start position:0% sort of feedback in but the more 00:24:15.540 --> 00:24:17.090 align:start position:0% sort of feedback in but the more complicated<00:24:16.170> the<00:24:16.260> more<00:24:16.290> experimental<00:24:16.800> your 00:24:17.090 --> 00:24:17.100 align:start position:0% complicated the more experimental your 00:24:17.100 --> 00:24:18.380 align:start position:0% complicated the more experimental your contract<00:24:17.460> is<00:24:17.640> the<00:24:17.760> more<00:24:17.910> time<00:24:18.120> you're<00:24:18.300> going 00:24:18.380 --> 00:24:18.390 align:start position:0% contract is the more time you're going 00:24:18.390 --> 00:24:19.880 align:start position:0% contract is the more time you're going to<00:24:18.480> have<00:24:18.600> to<00:24:18.690> take<00:24:18.840> and<00:24:19.140> the<00:24:19.650> more<00:24:19.680> you're 00:24:19.880 --> 00:24:19.890 align:start position:0% to have to take and the more you're 00:24:19.890 --> 00:24:21.320 align:start position:0% to have to take and the more you're gonna<00:24:19.980> have<00:24:20.130> to<00:24:20.220> consult<00:24:20.520> experts<00:24:20.760> who<00:24:21.300> really 00:24:21.320 --> 00:24:21.330 align:start position:0% gonna have to consult experts who really 00:24:21.330 --> 00:24:22.460 align:start position:0% gonna have to consult experts who really know<00:24:21.690> how<00:24:21.840> to<00:24:21.900> write<00:24:22.110> like<00:24:22.290> new 00:24:22.460 --> 00:24:22.470 align:start position:0% know how to write like new 00:24:22.470 --> 00:24:24.200 align:start position:0% know how to write like new specifications<00:24:23.280> and<00:24:23.370> not<00:24:23.490> just<00:24:23.610> reuse<00:24:23.970> those 00:24:24.200 --> 00:24:24.210 align:start position:0% specifications and not just reuse those 00:24:24.210 --> 00:24:26.480 align:start position:0% specifications and not just reuse those same<00:24:24.480> old<00:24:24.510> building<00:24:24.960> blocks<00:24:25.200> in<00:24:26.010> the<00:24:26.130> old<00:24:26.310> ones 00:24:26.480 --> 00:24:26.490 align:start position:0% same old building blocks in the old ones 00:24:26.490 --> 00:24:32.090 align:start position:0% same old building blocks in the old ones I<00:24:26.960> I<00:24:27.960> think<00:24:28.380> auditing<00:24:30.050> make<00:24:31.050> finding<00:24:31.650> bugs<00:24:31.860> in 00:24:32.090 --> 00:24:32.100 align:start position:0% I I think auditing make finding bugs in 00:24:32.100 --> 00:24:35.590 align:start position:0% I I think auditing make finding bugs in the<00:24:32.280> contract<00:24:32.670> is<00:24:32.910> a<00:24:33.150> bad<00:24:33.420> game<00:24:33.840> to<00:24:34.260> play 00:24:35.590 --> 00:24:35.600 align:start position:0% the contract is a bad game to play 00:24:35.600 --> 00:24:39.080 align:start position:0% the contract is a bad game to play because<00:24:36.600> you<00:24:37.170> have<00:24:37.350> to<00:24:37.590> beat<00:24:38.070> the<00:24:38.580> best 00:24:39.080 --> 00:24:39.090 align:start position:0% because you have to beat the best 00:24:39.090 --> 00:24:46.460 align:start position:0% because you have to beat the best articles<00:24:40.010> in<00:24:41.010> the<00:24:41.190> world<00:24:42.500> so<00:24:45.170> going<00:24:46.170> forward 00:24:46.460 --> 00:24:46.470 align:start position:0% articles in the world so going forward 00:24:46.470 --> 00:24:49.790 align:start position:0% articles in the world so going forward if<00:24:46.650> you<00:24:46.920> try<00:24:47.250> more<00:24:48.020> complicated<00:24:49.020> stuff<00:24:49.290> you 00:24:49.790 --> 00:24:49.800 align:start position:0% if you try more complicated stuff you 00:24:49.800 --> 00:24:54.820 align:start position:0% if you try more complicated stuff you will<00:24:50.010> need<00:24:50.630> much<00:24:51.630> stronger<00:24:52.460> usable<00:24:53.460> - 00:24:54.820 --> 00:24:54.830 align:start position:0% will need much stronger usable - 00:24:54.830 --> 00:24:59.420 align:start position:0% will need much stronger usable - otherwise<00:24:55.830> um<00:24:56.690> so<00:24:57.690> I<00:24:57.930> mean<00:24:58.470> the<00:24:58.800> game<00:24:59.130> is<00:24:59.280> not 00:24:59.420 --> 00:24:59.430 align:start position:0% otherwise um so I mean the game is not 00:24:59.430 --> 00:25:02.710 align:start position:0% otherwise um so I mean the game is not fair<00:24:59.790> you<00:24:59.880> have<00:25:00.030> to<00:25:00.150> find<00:25:00.360> the<00:25:00.480> old<00:25:00.690> holes<00:25:01.610> and 00:25:02.710 --> 00:25:02.720 align:start position:0% fair you have to find the old holes and 00:25:02.720 --> 00:25:05.870 align:start position:0% fair you have to find the old holes and a<00:25:03.720> very<00:25:03.960> good<00:25:04.200> attacker<00:25:04.680> should<00:25:05.430> find<00:25:05.730> only 00:25:05.870 --> 00:25:05.880 align:start position:0% a very good attacker should find only 00:25:05.880 --> 00:25:09.110 align:start position:0% a very good attacker should find only one<00:25:06.060> go<00:25:06.420> one<00:25:06.750> poor<00:25:07.320> critical<00:25:08.130> vulnerability 00:25:09.110 --> 00:25:09.120 align:start position:0% one go one poor critical vulnerability 00:25:09.120 --> 00:25:11.540 align:start position:0% one go one poor critical vulnerability so<00:25:09.750> it's<00:25:09.900> very<00:25:10.110> skew<00:25:10.650> it's<00:25:10.890> a<00:25:11.130> very<00:25:11.310> very 00:25:11.540 --> 00:25:11.550 align:start position:0% so it's very skew it's a very very 00:25:11.550 --> 00:25:15.110 align:start position:0% so it's very skew it's a very very skewed<00:25:11.910> game<00:25:12.270> so<00:25:13.160> maybe<00:25:14.160> a<00:25:14.250> good<00:25:14.370> tooling<00:25:14.940> or 00:25:15.110 --> 00:25:15.120 align:start position:0% skewed game so maybe a good tooling or 00:25:15.120 --> 00:25:17.630 align:start position:0% skewed game so maybe a good tooling or maybe<00:25:15.420> a<00:25:15.540> good<00:25:15.780> game<00:25:16.080> like<00:25:16.260> Hydra<00:25:16.890> is 00:25:17.630 --> 00:25:17.640 align:start position:0% maybe a good game like Hydra is 00:25:17.640 --> 00:25:21.230 align:start position:0% maybe a good game like Hydra is necessary<00:25:18.320> but<00:25:19.320> I<00:25:19.590> think<00:25:20.160> we<00:25:20.550> are<00:25:20.700> kind<00:25:21.030> of 00:25:21.230 --> 00:25:21.240 align:start position:0% necessary but I think we are kind of 00:25:21.240 --> 00:25:25.340 align:start position:0% necessary but I think we are kind of ready<00:25:21.540> to<00:25:22.020> that<00:25:22.200> take<00:25:22.740> the<00:25:22.890> challenge<00:25:24.350> rights 00:25:25.340 --> 00:25:25.350 align:start position:0% ready to that take the challenge rights 00:25:25.350 --> 00:25:27.770 align:start position:0% ready to that take the challenge rights and<00:25:25.500> thanks<00:25:25.710> very<00:25:25.740> much<00:25:26.000> that<00:25:27.000> concludes<00:25:27.150> the 00:25:27.770 --> 00:25:27.780 align:start position:0% and thanks very much that concludes the 00:25:27.780 --> 00:25:29.900 align:start position:0% and thanks very much that concludes the panel<00:25:28.080> like<00:25:28.800> to<00:25:28.920> thank<00:25:29.250> all<00:25:29.370> the<00:25:29.490> panelists 00:25:29.900 --> 00:25:29.910 align:start position:0% panel like to thank all the panelists 00:25:29.910 --> 00:25:31.940 align:start position:0% panel like to thank all the panelists like<00:25:30.090> it's<00:25:30.240> a<00:25:30.300> huge<00:25:30.510> honor<00:25:30.720> to<00:25:31.050> share<00:25:31.740> the 00:25:31.940 --> 00:25:31.950 align:start position:0% like it's a huge honor to share the 00:25:31.950 --> 00:25:34.490 align:start position:0% like it's a huge honor to share the stage<00:25:31.980> with<00:25:32.220> some<00:25:33.060> of<00:25:33.180> the<00:25:33.510> best<00:25:33.960> researchers 00:25:34.490 --> 00:25:34.500 align:start position:0% stage with some of the best researchers 00:25:34.500 --> 00:25:38.510 align:start position:0% stage with some of the best researchers in<00:25:35.310> the<00:25:35.460> field<00:25:35.490> thanks<00:25:36.180> very<00:25:36.420> much 00:25:38.510 --> 00:25:38.520 align:start position:0% in the field thanks very much 00:25:38.520 --> 00:25:43.420 align:start position:0% in the field thanks very much [Applause] 00:25:43.420 --> 00:25:43.430 align:start position:0% [Applause] 00:25:43.430 --> 00:25:45.490 align:start position:0% [Applause] you