WEBVTT Kind: captions Language: en 00:00:07.420 --> 00:00:19.270 align:start position:0% you 00:00:19.270 --> 00:00:19.280 align:start position:0% 00:00:19.280 --> 00:00:23.510 align:start position:0% hello<00:00:20.280> hello<00:00:20.610> oh<00:00:20.820> thank<00:00:21.390> you<00:00:21.450> very<00:00:21.630> much<00:00:22.400> it<00:00:23.400> is 00:00:23.510 --> 00:00:23.520 align:start position:0% hello hello oh thank you very much it is 00:00:23.520 --> 00:00:27.080 align:start position:0% hello hello oh thank you very much it is an<00:00:23.610> honor<00:00:23.760> to<00:00:23.880> be<00:00:24.060> here<00:00:24.090> and<00:00:24.540> I<00:00:25.400> have<00:00:26.400> a<00:00:26.640> part<00:00:27.060> of 00:00:27.080 --> 00:00:27.090 align:start position:0% an honor to be here and I have a part of 00:00:27.090 --> 00:00:31.340 align:start position:0% an honor to be here and I have a part of me<00:00:27.240> I<00:00:27.450> have<00:00:28.020> to<00:00:28.200> second<00:00:28.970> yo<00:00:29.970> yo<00:00:30.300> chewy<00:00:30.540> your 00:00:31.340 --> 00:00:31.350 align:start position:0% me I have to second yo yo chewy your 00:00:31.350 --> 00:00:35.090 align:start position:0% me I have to second yo yo chewy your shoe<00:00:31.530> ease<00:00:32.150> statement<00:00:33.150> that<00:00:33.690> this<00:00:33.960> is<00:00:34.170> a<00:00:34.199> dream 00:00:35.090 --> 00:00:35.100 align:start position:0% shoe ease statement that this is a dream 00:00:35.100 --> 00:00:37.580 align:start position:0% shoe ease statement that this is a dream for<00:00:35.879> a<00:00:35.940> formal<00:00:36.300> verification<00:00:36.480> engineer<00:00:37.110> I 00:00:37.580 --> 00:00:37.590 align:start position:0% for a formal verification engineer I 00:00:37.590 --> 00:00:41.180 align:start position:0% for a formal verification engineer I mean<00:00:37.949> the<00:00:38.580> amount<00:00:39.180> of<00:00:39.270> interest<00:00:39.770> in<00:00:40.770> the<00:00:40.980> room 00:00:41.180 --> 00:00:41.190 align:start position:0% mean the amount of interest in the room 00:00:41.190 --> 00:00:44.689 align:start position:0% mean the amount of interest in the room in<00:00:41.750> this<00:00:42.750> beautiful<00:00:43.020> field<00:00:43.530> that<00:00:43.920> those<00:00:44.400> of<00:00:44.580> us 00:00:44.689 --> 00:00:44.699 align:start position:0% in this beautiful field that those of us 00:00:44.699 --> 00:00:47.680 align:start position:0% in this beautiful field that those of us who<00:00:44.910> have<00:00:45.650> you<00:00:46.650> know<00:00:46.680> devoted<00:00:47.159> a<00:00:47.220> lot<00:00:47.339> of<00:00:47.489> our 00:00:47.680 --> 00:00:47.690 align:start position:0% who have you know devoted a lot of our 00:00:47.690 --> 00:00:52.369 align:start position:0% who have you know devoted a lot of our professional<00:00:48.690> and<00:00:49.879> you<00:00:50.879> say<00:00:51.170> personal<00:00:52.170> lives 00:00:52.369 --> 00:00:52.379 align:start position:0% professional and you say personal lives 00:00:52.379 --> 00:00:54.560 align:start position:0% professional and you say personal lives too<00:00:52.650> it's<00:00:53.550> amazing<00:00:54.030> to<00:00:54.059> see<00:00:54.300> so<00:00:54.330> much 00:00:54.560 --> 00:00:54.570 align:start position:0% too it's amazing to see so much 00:00:54.570 --> 00:01:01.160 align:start position:0% too it's amazing to see so much enthusiasm<00:00:54.780> so<00:00:55.470> I<00:00:56.269> feel<00:00:57.269> very<00:00:57.300> fortunate<00:01:00.170> to 00:01:01.160 --> 00:01:01.170 align:start position:0% enthusiasm so I feel very fortunate to 00:01:01.170 --> 00:01:03.530 align:start position:0% enthusiasm so I feel very fortunate to be<00:01:01.290> a<00:01:01.320> part<00:01:01.379> of<00:01:01.589> this<00:01:01.739> group<00:01:02.070> we're<00:01:02.970> such<00:01:03.180> great 00:01:03.530 --> 00:01:03.540 align:start position:0% be a part of this group we're such great 00:01:03.540 --> 00:01:05.660 align:start position:0% be a part of this group we're such great work<00:01:03.750> and<00:01:04.019> awareness<00:01:04.470> is<00:01:04.949> happening<00:01:05.519> around 00:01:05.660 --> 00:01:05.670 align:start position:0% work and awareness is happening around 00:01:05.670 --> 00:01:08.060 align:start position:0% work and awareness is happening around formal<00:01:06.510> verification<00:01:06.630> static<00:01:07.470> analysis<00:01:07.920> and 00:01:08.060 --> 00:01:08.070 align:start position:0% formal verification static analysis and 00:01:08.070 --> 00:01:10.760 align:start position:0% formal verification static analysis and so<00:01:08.159> on<00:01:08.420> so<00:01:09.420> I'm<00:01:09.750> very<00:01:09.840> excited<00:01:10.080> today<00:01:10.590> to 00:01:10.760 --> 00:01:10.770 align:start position:0% so on so I'm very excited today to 00:01:10.770 --> 00:01:13.850 align:start position:0% so on so I'm very excited today to launch<00:01:11.159> our<00:01:11.670> a<00:01:12.330> mantra<00:01:12.780> contracts<00:01:13.260> platform 00:01:13.850 --> 00:01:13.860 align:start position:0% launch our a mantra contracts platform 00:01:13.860 --> 00:01:16.670 align:start position:0% launch our a mantra contracts platform which<00:01:14.310> is<00:01:14.549> formal<00:01:15.450> verification<00:01:15.600> in<00:01:16.290> the 00:01:16.670 --> 00:01:16.680 align:start position:0% which is formal verification in the 00:01:16.680 --> 00:01:19.760 align:start position:0% which is formal verification in the cloud<00:01:16.950> for<00:01:17.340> smart<00:01:17.970> contracts<00:01:18.770> initially 00:01:19.760 --> 00:01:19.770 align:start position:0% cloud for smart contracts initially 00:01:19.770 --> 00:01:22.190 align:start position:0% cloud for smart contracts initially targeted<00:01:19.950> for<00:01:20.430> etherium<00:01:20.850> so<00:01:21.510> what<00:01:21.750> powers<00:01:22.170> a 00:01:22.190 --> 00:01:22.200 align:start position:0% targeted for etherium so what powers a 00:01:22.200 --> 00:01:24.830 align:start position:0% targeted for etherium so what powers a mantra<00:01:22.680> contracts<00:01:23.160> is<00:01:23.940> our<00:01:24.420> formal 00:01:24.830 --> 00:01:24.840 align:start position:0% mantra contracts is our formal 00:01:24.840 --> 00:01:26.990 align:start position:0% mantra contracts is our formal verification<00:01:25.100> engine<00:01:26.100> that<00:01:26.610> will<00:01:26.730> talk<00:01:26.880> to 00:01:26.990 --> 00:01:27.000 align:start position:0% verification engine that will talk to 00:01:27.000 --> 00:01:28.850 align:start position:0% verification engine that will talk to you<00:01:27.090> about<00:01:27.180> call<00:01:27.480> Timandra<00:01:27.930> but<00:01:28.590> what<00:01:28.740> we've 00:01:28.850 --> 00:01:28.860 align:start position:0% you about call Timandra but what we've 00:01:28.860 --> 00:01:31.070 align:start position:0% you about call Timandra but what we've done<00:01:29.100> is<00:01:29.430> we've<00:01:29.700> taken<00:01:29.730> the<00:01:30.210> etherium<00:01:30.690> virtual 00:01:31.070 --> 00:01:31.080 align:start position:0% done is we've taken the etherium virtual 00:01:31.080 --> 00:01:33.530 align:start position:0% done is we've taken the etherium virtual machine<00:01:31.470> and<00:01:31.700> formalized<00:01:32.700> it<00:01:33.030> within<00:01:33.330> a 00:01:33.530 --> 00:01:33.540 align:start position:0% machine and formalized it within a 00:01:33.540 --> 00:01:35.900 align:start position:0% machine and formalized it within a mantra<00:01:33.960> given<00:01:34.590> a<00:01:34.680> full<00:01:34.980> bit<00:01:35.370> precise 00:01:35.900 --> 00:01:35.910 align:start position:0% mantra given a full bit precise 00:01:35.910 --> 00:01:39.320 align:start position:0% mantra given a full bit precise operational<00:01:36.900> semantics<00:01:37.470> to<00:01:38.070> the<00:01:38.730> instruction 00:01:39.320 --> 00:01:39.330 align:start position:0% operational semantics to the instruction 00:01:39.330 --> 00:01:41.360 align:start position:0% operational semantics to the instruction set<00:01:39.690> of<00:01:39.870> the<00:01:39.960> etherium<00:01:40.380> virtual<00:01:40.710> machine<00:01:41.010> and 00:01:41.360 --> 00:01:41.370 align:start position:0% set of the etherium virtual machine and 00:01:41.370 --> 00:01:43.670 align:start position:0% set of the etherium virtual machine and then<00:01:42.000> from<00:01:42.300> that<00:01:42.360> we're<00:01:42.990> able<00:01:43.140> to<00:01:43.350> build<00:01:43.530> a 00:01:43.670 --> 00:01:43.680 align:start position:0% then from that we're able to build a 00:01:43.680 --> 00:01:45.650 align:start position:0% then from that we're able to build a stack<00:01:43.920> of<00:01:43.950> tools<00:01:44.400> that<00:01:44.820> work<00:01:45.330> at<00:01:45.510> many 00:01:45.650 --> 00:01:45.660 align:start position:0% stack of tools that work at many 00:01:45.660 --> 00:01:47.780 align:start position:0% stack of tools that work at many different<00:01:45.720> levels<00:01:46.100> powered<00:01:47.100> by<00:01:47.130> techniques 00:01:47.780 --> 00:01:47.790 align:start position:0% different levels powered by techniques 00:01:47.790 --> 00:01:50.270 align:start position:0% different levels powered by techniques such<00:01:48.060> as<00:01:48.120> symbolic<00:01:48.630> execution<00:01:49.280> something 00:01:50.270 --> 00:01:50.280 align:start position:0% such as symbolic execution something 00:01:50.280 --> 00:01:52.010 align:start position:0% such as symbolic execution something called<00:01:50.430> principal<00:01:50.760> region<00:01:51.270> decomposition 00:01:52.010 --> 00:01:52.020 align:start position:0% called principal region decomposition 00:01:52.020 --> 00:01:54.170 align:start position:0% called principal region decomposition and<00:01:52.200> ultimately<00:01:53.040> both<00:01:53.310> automated<00:01:54.000> an 00:01:54.170 --> 00:01:54.180 align:start position:0% and ultimately both automated an 00:01:54.180 --> 00:01:57.320 align:start position:0% and ultimately both automated an interactive<00:01:54.900> proof<00:01:55.850> so<00:01:56.850> I'll<00:01:57.090> walk<00:01:57.240> you 00:01:57.320 --> 00:01:57.330 align:start position:0% interactive proof so I'll walk you 00:01:57.330 --> 00:01:59.090 align:start position:0% interactive proof so I'll walk you through<00:01:57.480> many<00:01:57.630> details<00:01:58.020> show<00:01:58.800> some<00:01:58.950> examples 00:01:59.090 --> 00:01:59.100 align:start position:0% through many details show some examples 00:01:59.100 --> 00:02:01.520 align:start position:0% through many details show some examples and<00:01:59.760> then<00:02:00.120> I<00:02:00.480> hope<00:02:00.690> we<00:02:00.810> can<00:02:00.960> do<00:02:01.050> lots<00:02:01.200> of<00:02:01.320> demos 00:02:01.520 --> 00:02:01.530 align:start position:0% and then I hope we can do lots of demos 00:02:01.530 --> 00:02:03.890 align:start position:0% and then I hope we can do lots of demos because<00:02:02.070> there<00:02:02.190> isn't<00:02:02.400> that<00:02:02.430> much<00:02:02.610> time<00:02:02.900> but 00:02:03.890 --> 00:02:03.900 align:start position:0% because there isn't that much time but 00:02:03.900 --> 00:02:05.990 align:start position:0% because there isn't that much time but please<00:02:04.050> find<00:02:04.380> me<00:02:04.530> if<00:02:04.890> you're<00:02:05.400> interested<00:02:05.430> in 00:02:05.990 --> 00:02:06.000 align:start position:0% please find me if you're interested in 00:02:06.000 --> 00:02:09.830 align:start position:0% please find me if you're interested in sign<00:02:06.240> up<00:02:06.420> so<00:02:07.409> before<00:02:08.340> I<00:02:08.849> get<00:02:09.149> started<00:02:09.179> I<00:02:09.690> want 00:02:09.830 --> 00:02:09.840 align:start position:0% sign up so before I get started I want 00:02:09.840 --> 00:02:12.500 align:start position:0% sign up so before I get started I want to<00:02:09.989> show<00:02:10.110> a<00:02:10.140> two<00:02:10.440> minute<00:02:10.619> video<00:02:10.830> that<00:02:11.510> give 00:02:12.500 --> 00:02:12.510 align:start position:0% to show a two minute video that give 00:02:12.510 --> 00:02:13.910 align:start position:0% to show a two minute video that give some<00:02:12.750> background<00:02:12.930> on<00:02:13.290> what<00:02:13.470> we<00:02:13.620> do<00:02:13.800> at 00:02:13.910 --> 00:02:13.920 align:start position:0% some background on what we do at 00:02:13.920 --> 00:02:15.710 align:start position:0% some background on what we do at aesthetic<00:02:14.340> integration<00:02:14.849> and<00:02:15.090> really<00:02:15.540> how<00:02:15.659> we 00:02:15.710 --> 00:02:15.720 align:start position:0% aesthetic integration and really how we 00:02:15.720 --> 00:02:18.380 align:start position:0% aesthetic integration and really how we got<00:02:15.959> here<00:02:16.040> so<00:02:17.040> now<00:02:17.220> I<00:02:17.550> will<00:02:17.819> hand<00:02:18.000> over<00:02:18.120> to 00:02:18.380 --> 00:02:18.390 align:start position:0% got here so now I will hand over to 00:02:18.390 --> 00:02:20.570 align:start position:0% got here so now I will hand over to Hudson<00:02:18.810> because<00:02:19.140> I<00:02:19.230> think<00:02:19.440> he<00:02:19.830> has<00:02:19.980> to<00:02:20.159> man<00:02:20.370> the 00:02:20.570 --> 00:02:20.580 align:start position:0% Hudson because I think he has to man the 00:02:20.580 --> 00:02:25.270 align:start position:0% Hudson because I think he has to man the sound<00:02:23.329> thank<00:02:24.329> you 00:02:25.270 --> 00:02:25.280 align:start position:0% sound thank you 00:02:25.280 --> 00:02:26.830 align:start position:0% sound thank you what's<00:02:25.640> plaguing<00:02:25.910> today's<00:02:26.360> electronic 00:02:26.830 --> 00:02:26.840 align:start position:0% what's plaguing today's electronic 00:02:26.840 --> 00:02:29.680 align:start position:0% what's plaguing today's electronic financial<00:02:27.470> markets<00:02:27.819> the<00:02:28.819> world<00:02:29.000> economy<00:02:29.270> is 00:02:29.680 --> 00:02:29.690 align:start position:0% financial markets the world economy is 00:02:29.690 --> 00:02:31.630 align:start position:0% financial markets the world economy is built<00:02:29.900> on<00:02:30.110> a<00:02:30.140> staggeringly<00:02:30.560> complex<00:02:31.310> tangle 00:02:31.630 --> 00:02:31.640 align:start position:0% built on a staggeringly complex tangle 00:02:31.640 --> 00:02:34.210 align:start position:0% built on a staggeringly complex tangle of<00:02:31.910> algorithms<00:02:32.680> competitive<00:02:33.680> pressures<00:02:34.069> and 00:02:34.210 --> 00:02:34.220 align:start position:0% of algorithms competitive pressures and 00:02:34.220 --> 00:02:36.160 align:start position:0% of algorithms competitive pressures and economic<00:02:34.940> recession<00:02:35.450> have<00:02:35.569> contributed<00:02:35.900> to 00:02:36.160 --> 00:02:36.170 align:start position:0% economic recession have contributed to 00:02:36.170 --> 00:02:38.850 align:start position:0% economic recession have contributed to increasingly<00:02:36.860> opaque<00:02:37.310> and<00:02:37.550> unstable<00:02:37.910> markets 00:02:38.850 --> 00:02:38.860 align:start position:0% increasingly opaque and unstable markets 00:02:38.860 --> 00:02:41.260 align:start position:0% increasingly opaque and unstable markets the<00:02:39.860> effects<00:02:40.160> of<00:02:40.310> glitches<00:02:40.610> and<00:02:40.970> unfair 00:02:41.260 --> 00:02:41.270 align:start position:0% the effects of glitches and unfair 00:02:41.270 --> 00:02:43.690 align:start position:0% the effects of glitches and unfair advantages<00:02:41.780> can<00:02:42.050> be<00:02:42.170> devastating<00:02:42.700> cratering 00:02:43.690 --> 00:02:43.700 align:start position:0% advantages can be devastating cratering 00:02:43.700 --> 00:02:45.100 align:start position:0% advantages can be devastating cratering the<00:02:43.819> confidence<00:02:44.300> of<00:02:44.420> investors<00:02:44.510> and 00:02:45.100 --> 00:02:45.110 align:start position:0% the confidence of investors and 00:02:45.110 --> 00:02:47.820 align:start position:0% the confidence of investors and ultimately<00:02:45.860> hurting<00:02:46.430> the<00:02:46.520> general<00:02:46.850> public 00:02:47.820 --> 00:02:47.830 align:start position:0% ultimately hurting the general public 00:02:47.830 --> 00:02:50.050 align:start position:0% ultimately hurting the general public regulators<00:02:48.830> and<00:02:48.980> the<00:02:49.280> industry<00:02:49.550> have<00:02:49.850> worked 00:02:50.050 --> 00:02:50.060 align:start position:0% regulators and the industry have worked 00:02:50.060 --> 00:02:52.479 align:start position:0% regulators and the industry have worked tirelessly<00:02:50.390> to<00:02:50.810> define<00:02:51.290> what<00:02:51.319> safe<00:02:51.860> and<00:02:52.100> fair 00:02:52.479 --> 00:02:52.489 align:start position:0% tirelessly to define what safe and fair 00:02:52.489 --> 00:02:55.240 align:start position:0% tirelessly to define what safe and fair markets<00:02:52.970> are<00:02:53.290> what's<00:02:54.290> been<00:02:54.440> missing<00:02:54.620> is<00:02:54.950> a<00:02:55.010> way 00:02:55.240 --> 00:02:55.250 align:start position:0% markets are what's been missing is a way 00:02:55.250 --> 00:02:56.949 align:start position:0% markets are what's been missing is a way to<00:02:55.310> analyze<00:02:55.670> and<00:02:56.060> regulate<00:02:56.420> all<00:02:56.600> of<00:02:56.900> the 00:02:56.949 --> 00:02:56.959 align:start position:0% to analyze and regulate all of the 00:02:56.959 --> 00:02:59.650 align:start position:0% to analyze and regulate all of the algorithms<00:02:57.590> underlying<00:02:58.100> the<00:02:59.000> solution<00:02:59.480> is 00:02:59.650 --> 00:02:59.660 align:start position:0% algorithms underlying the solution is 00:02:59.660 --> 00:03:02.080 align:start position:0% algorithms underlying the solution is formal<00:03:00.110> verification<00:03:00.519> the<00:03:01.519> science<00:03:01.940> of 00:03:02.080 --> 00:03:02.090 align:start position:0% formal verification the science of 00:03:02.090 --> 00:03:05.080 align:start position:0% formal verification the science of correct<00:03:02.600> algorithms<00:03:03.250> other<00:03:04.250> safety<00:03:04.700> critical 00:03:05.080 --> 00:03:05.090 align:start position:0% correct algorithms other safety critical 00:03:05.090 --> 00:03:07.420 align:start position:0% correct algorithms other safety critical industries<00:03:05.450> already<00:03:06.350> rely<00:03:06.680> on<00:03:06.920> formal 00:03:07.420 --> 00:03:07.430 align:start position:0% industries already rely on formal 00:03:07.430 --> 00:03:09.430 align:start position:0% industries already rely on formal verification<00:03:07.550> to<00:03:08.480> make<00:03:08.630> their<00:03:08.840> algorithms 00:03:09.430 --> 00:03:09.440 align:start position:0% verification to make their algorithms 00:03:09.440 --> 00:03:12.490 align:start position:0% verification to make their algorithms say<00:03:09.650> the<00:03:10.580> mandra<00:03:11.090> by<00:03:11.480> aesthetic<00:03:11.930> integration 00:03:12.490 --> 00:03:12.500 align:start position:0% say the mandra by aesthetic integration 00:03:12.500 --> 00:03:14.250 align:start position:0% say the mandra by aesthetic integration is<00:03:12.650> the<00:03:12.830> world's<00:03:13.130> first<00:03:13.400> formal<00:03:14.000> verification 00:03:14.250 --> 00:03:14.260 align:start position:0% is the world's first formal verification 00:03:14.260 --> 00:03:18.070 align:start position:0% is the world's first formal verification solution<00:03:15.260> for<00:03:15.530> financial<00:03:16.069> markets<00:03:17.080> consider 00:03:18.070 --> 00:03:18.080 align:start position:0% solution for financial markets consider 00:03:18.080 --> 00:03:20.530 align:start position:0% solution for financial markets consider the<00:03:18.230> building<00:03:18.560> of<00:03:18.650> a<00:03:18.709> bridge<00:03:18.950> a<00:03:19.239> design<00:03:20.239> flaw 00:03:20.530 --> 00:03:20.540 align:start position:0% the building of a bridge a design flaw 00:03:20.540 --> 00:03:23.290 align:start position:0% the building of a bridge a design flaw may<00:03:20.900> be<00:03:20.959> catastrophic<00:03:21.760> to<00:03:22.760> make<00:03:22.910> it<00:03:23.060> safe 00:03:23.290 --> 00:03:23.300 align:start position:0% may be catastrophic to make it safe 00:03:23.300 --> 00:03:25.390 align:start position:0% may be catastrophic to make it safe engineers<00:03:23.780> use<00:03:24.230> powerful<00:03:24.650> computer<00:03:25.250> aided 00:03:25.390 --> 00:03:25.400 align:start position:0% engineers use powerful computer aided 00:03:25.400 --> 00:03:27.910 align:start position:0% engineers use powerful computer aided design<00:03:25.610> tools<00:03:26.150> which<00:03:26.600> analyze<00:03:27.080> designs<00:03:27.560> for 00:03:27.910 --> 00:03:27.920 align:start position:0% design tools which analyze designs for 00:03:27.920 --> 00:03:30.120 align:start position:0% design tools which analyze designs for safety<00:03:28.340> automatically 00:03:30.120 --> 00:03:30.130 align:start position:0% safety automatically 00:03:30.130 --> 00:03:32.820 align:start position:0% safety automatically powered<00:03:30.940> by<00:03:30.970> latest<00:03:31.570> advances<00:03:32.200> in<00:03:32.200> artificial 00:03:32.820 --> 00:03:32.830 align:start position:0% powered by latest advances in artificial 00:03:32.830 --> 00:03:34.740 align:start position:0% powered by latest advances in artificial intelligence<00:03:33.100> computer<00:03:34.060> science<00:03:34.570> and 00:03:34.740 --> 00:03:34.750 align:start position:0% intelligence computer science and 00:03:34.750 --> 00:03:36.390 align:start position:0% intelligence computer science and mathematics<00:03:34.930> a<00:03:35.530> mantra<00:03:36.100> brings 00:03:36.390 --> 00:03:36.400 align:start position:0% mathematics a mantra brings 00:03:36.400 --> 00:03:38.430 align:start position:0% mathematics a mantra brings unprecedented<00:03:36.760> rigor<00:03:37.420> to<00:03:37.720> the<00:03:37.840> electronic 00:03:38.430 --> 00:03:38.440 align:start position:0% unprecedented rigor to the electronic 00:03:38.440 --> 00:03:40.770 align:start position:0% unprecedented rigor to the electronic financial<00:03:38.890> markets<00:03:39.310> analyzing<00:03:40.270> the<00:03:40.360> safety 00:03:40.770 --> 00:03:40.780 align:start position:0% financial markets analyzing the safety 00:03:40.780 --> 00:03:42.960 align:start position:0% financial markets analyzing the safety and<00:03:40.930> fairness<00:03:41.650> of<00:03:41.800> algorithms<00:03:42.340> before 00:03:42.960 --> 00:03:42.970 align:start position:0% and fairness of algorithms before 00:03:42.970 --> 00:03:45.750 align:start position:0% and fairness of algorithms before they're<00:03:43.210> deployed<00:03:44.190> financial<00:03:45.190> algorithms 00:03:45.750 --> 00:03:45.760 align:start position:0% they're deployed financial algorithms 00:03:45.760 --> 00:03:48.360 align:start position:0% they're deployed financial algorithms are<00:03:45.910> unfathomably<00:03:46.600> complex<00:03:47.080> they<00:03:47.830> can<00:03:47.980> be<00:03:48.130> in 00:03:48.360 --> 00:03:48.370 align:start position:0% are unfathomably complex they can be in 00:03:48.370 --> 00:03:50.280 align:start position:0% are unfathomably complex they can be in a<00:03:48.460> virtually<00:03:48.880> infinite<00:03:49.060> number<00:03:49.690> of<00:03:49.720> possible 00:03:50.280 --> 00:03:50.290 align:start position:0% a virtually infinite number of possible 00:03:50.290 --> 00:03:54.170 align:start position:0% a virtually infinite number of possible states<00:03:50.910> examining<00:03:51.910> 100<00:03:52.590> 1000<00:03:53.590> were<00:03:53.740> even 00:03:54.170 --> 00:03:54.180 align:start position:0% states examining 100 1000 were even 00:03:54.180 --> 00:03:57.750 align:start position:0% states examining 100 1000 were even 100,000<00:03:55.180> test<00:03:55.390> cases<00:03:55.630> isn't<00:03:56.410> enough<00:03:56.620> we<00:03:57.550> must 00:03:57.750 --> 00:03:57.760 align:start position:0% 100,000 test cases isn't enough we must 00:03:57.760 --> 00:03:59.700 align:start position:0% 100,000 test cases isn't enough we must consider<00:03:57.910> every<00:03:58.630> possible<00:03:59.080> case<00:03:59.320> to<00:03:59.560> answer 00:03:59.700 --> 00:03:59.710 align:start position:0% consider every possible case to answer 00:03:59.710 --> 00:04:02.400 align:start position:0% consider every possible case to answer definitively<00:04:00.330> what<00:04:01.330> can<00:04:01.690> possibly<00:04:01.900> go<00:04:02.290> wrong 00:04:02.400 --> 00:04:02.410 align:start position:0% definitively what can possibly go wrong 00:04:02.410 --> 00:04:05.670 align:start position:0% definitively what can possibly go wrong a<00:04:02.940> mandra<00:04:03.940> allows<00:04:04.300> designers<00:04:04.570> and<00:04:05.140> regulators 00:04:05.670 --> 00:04:05.680 align:start position:0% a mandra allows designers and regulators 00:04:05.680 --> 00:04:07.800 align:start position:0% a mandra allows designers and regulators to<00:04:05.710> fix<00:04:06.160> breaches<00:04:06.610> of<00:04:06.640> safety<00:04:07.150> and<00:04:07.270> fairness 00:04:07.800 --> 00:04:07.810 align:start position:0% to fix breaches of safety and fairness 00:04:07.810 --> 00:04:11.310 align:start position:0% to fix breaches of safety and fairness before<00:04:08.590> they<00:04:08.740> affect<00:04:09.070> markets<00:04:10.020> let's<00:04:11.020> build 00:04:11.310 --> 00:04:11.320 align:start position:0% before they affect markets let's build 00:04:11.320 --> 00:04:13.440 align:start position:0% before they affect markets let's build safer<00:04:11.860> more<00:04:12.340> reliable<00:04:12.400> and<00:04:13.030> regulatory 00:04:13.440 --> 00:04:13.450 align:start position:0% safer more reliable and regulatory 00:04:13.450 --> 00:04:15.510 align:start position:0% safer more reliable and regulatory compliance<00:04:14.260> systems<00:04:14.650> that<00:04:14.890> all<00:04:15.130> of<00:04:15.310> us<00:04:15.400> can 00:04:15.510 --> 00:04:15.520 align:start position:0% compliance systems that all of us can 00:04:15.520 --> 00:04:18.500 align:start position:0% compliance systems that all of us can trust<00:04:15.880> saving<00:04:16.690> everyone<00:04:17.170> time<00:04:17.590> and<00:04:17.830> money<00:04:17.950> a 00:04:18.500 --> 00:04:18.510 align:start position:0% trust saving everyone time and money a 00:04:18.510 --> 00:04:21.570 align:start position:0% trust saving everyone time and money a mandra<00:04:19.510> by<00:04:19.870> aesthetic<00:04:20.350> integration<00:04:20.920> the 00:04:21.570 --> 00:04:21.580 align:start position:0% mandra by aesthetic integration the 00:04:21.580 --> 00:04:27.270 align:start position:0% mandra by aesthetic integration the logic<00:04:21.820> of<00:04:22.150> financial<00:04:22.810> risk<00:04:25.830> alright<00:04:26.830> thank 00:04:27.270 --> 00:04:27.280 align:start position:0% logic of financial risk alright thank 00:04:27.280 --> 00:04:32.490 align:start position:0% logic of financial risk alright thank you<00:04:27.690> very<00:04:28.690> much<00:04:30.270> so<00:04:31.270> just<00:04:32.170> a<00:04:32.260> bit<00:04:32.380> of 00:04:32.490 --> 00:04:32.500 align:start position:0% you very much so just a bit of 00:04:32.500 --> 00:04:35.010 align:start position:0% you very much so just a bit of background<00:04:33.060> we<00:04:34.060> are<00:04:34.150> aesthetic<00:04:34.510> integration 00:04:35.010 --> 00:04:35.020 align:start position:0% background we are aesthetic integration 00:04:35.020 --> 00:04:37.470 align:start position:0% background we are aesthetic integration and<00:04:35.170> our<00:04:35.950> work<00:04:36.220> before<00:04:36.640> etherium<00:04:37.090> and<00:04:37.270> you 00:04:37.470 --> 00:04:37.480 align:start position:0% and our work before etherium and you 00:04:37.480 --> 00:04:39.260 align:start position:0% and our work before etherium and you know<00:04:37.570> also<00:04:37.810> worth<00:04:38.080> that<00:04:38.290> continues 00:04:39.260 --> 00:04:39.270 align:start position:0% know also worth that continues 00:04:39.270 --> 00:04:42.600 align:start position:0% know also worth that continues vehemently<00:04:40.270> has<00:04:41.260> mostly<00:04:41.650> been<00:04:41.770> with 00:04:42.600 --> 00:04:42.610 align:start position:0% vehemently has mostly been with 00:04:42.610 --> 00:04:45.360 align:start position:0% vehemently has mostly been with financial<00:04:43.030> algorithms<00:04:43.660> like<00:04:44.650> dark<00:04:45.070> pools 00:04:45.360 --> 00:04:45.370 align:start position:0% financial algorithms like dark pools 00:04:45.370 --> 00:04:48.350 align:start position:0% financial algorithms like dark pools matching<00:04:46.180> logics<00:04:46.570> exchange<00:04:47.440> matching<00:04:47.890> logics 00:04:48.350 --> 00:04:48.360 align:start position:0% matching logics exchange matching logics 00:04:48.360 --> 00:04:50.550 align:start position:0% matching logics exchange matching logics connectivity<00:04:49.360> layers<00:04:49.600> for<00:04:50.020> instance<00:04:50.350> between 00:04:50.550 --> 00:04:50.560 align:start position:0% connectivity layers for instance between 00:04:50.560 --> 00:04:54.090 align:start position:0% connectivity layers for instance between venues<00:04:51.490> and<00:04:51.910> different<00:04:52.150> trading<00:04:52.330> systems<00:04:53.100> so 00:04:54.090 --> 00:04:54.100 align:start position:0% venues and different trading systems so 00:04:54.100 --> 00:04:56.130 align:start position:0% venues and different trading systems so we<00:04:54.790> have<00:04:54.880> worked<00:04:55.060> with<00:04:55.210> a<00:04:55.240> number<00:04:55.330> of<00:04:55.600> top 00:04:56.130 --> 00:04:56.140 align:start position:0% we have worked with a number of top 00:04:56.140 --> 00:04:58.320 align:start position:0% we have worked with a number of top investment<00:04:56.560> banks<00:04:56.710> on<00:04:57.160> formally<00:04:57.790> verifying 00:04:58.320 --> 00:04:58.330 align:start position:0% investment banks on formally verifying 00:04:58.330 --> 00:05:00.210 align:start position:0% investment banks on formally verifying regulatory<00:04:59.110> properties<00:04:59.620> of<00:04:59.800> their<00:04:59.890> core 00:05:00.210 --> 00:05:00.220 align:start position:0% regulatory properties of their core 00:05:00.220 --> 00:05:03.090 align:start position:0% regulatory properties of their core infrastructure<00:05:00.820> algorithms<00:05:01.750> last<00:05:02.740> year 00:05:03.090 --> 00:05:03.100 align:start position:0% infrastructure algorithms last year 00:05:03.100 --> 00:05:05.490 align:start position:0% infrastructure algorithms last year after<00:05:03.640> DEFCON<00:05:04.240> 1<00:05:04.480> something<00:05:04.960> very<00:05:05.170> exciting 00:05:05.490 --> 00:05:05.500 align:start position:0% after DEFCON 1 something very exciting 00:05:05.500 --> 00:05:08.130 align:start position:0% after DEFCON 1 something very exciting that<00:05:05.800> has<00:05:05.950> really<00:05:06.160> been<00:05:06.670> a<00:05:06.700> huge<00:05:06.940> catalyst<00:05:07.480> for 00:05:08.130 --> 00:05:08.140 align:start position:0% that has really been a huge catalyst for 00:05:08.140 --> 00:05:11.490 align:start position:0% that has really been a huge catalyst for us<00:05:08.290> in<00:05:09.070> growth<00:05:09.370> is<00:05:09.690> we<00:05:10.690> won<00:05:10.930> something<00:05:11.260> called 00:05:11.490 --> 00:05:11.500 align:start position:0% us in growth is we won something called 00:05:11.500 --> 00:05:13.950 align:start position:0% us in growth is we won something called the<00:05:11.590> UBS<00:05:12.010> future<00:05:12.460> of<00:05:12.580> Finance<00:05:12.970> challenge<00:05:13.510> so 00:05:13.950 --> 00:05:13.960 align:start position:0% the UBS future of Finance challenge so 00:05:13.960 --> 00:05:15.870 align:start position:0% the UBS future of Finance challenge so this<00:05:14.110> was<00:05:14.290> a<00:05:14.320> global<00:05:14.830> competition<00:05:15.220> between 00:05:15.870 --> 00:05:15.880 align:start position:0% this was a global competition between 00:05:15.880 --> 00:05:20.490 align:start position:0% this was a global competition between 620<00:05:16.870> companies<00:05:17.290> 52<00:05:18.070> countries<00:05:18.280> and<00:05:19.380> we<00:05:20.380> ended 00:05:20.490 --> 00:05:20.500 align:start position:0% 620 companies 52 countries and we ended 00:05:20.500 --> 00:05:22.560 align:start position:0% 620 companies 52 countries and we ended up<00:05:20.620> winning<00:05:20.770> the<00:05:20.980> whole<00:05:21.070> thing<00:05:21.130> and<00:05:21.580> I<00:05:22.330> think<00:05:22.510> a 00:05:22.560 --> 00:05:22.570 align:start position:0% up winning the whole thing and I think a 00:05:22.570 --> 00:05:25.380 align:start position:0% up winning the whole thing and I think a major<00:05:22.900> reason<00:05:23.140> was<00:05:23.500> we<00:05:24.250> took<00:05:24.460> the<00:05:25.030> design<00:05:25.360> of 00:05:25.380 --> 00:05:25.390 align:start position:0% major reason was we took the design of 00:05:25.390 --> 00:05:27.930 align:start position:0% major reason was we took the design of UBS<00:05:25.810> is<00:05:25.990> dark<00:05:26.230> pool<00:05:26.470> and<00:05:26.740> actually<00:05:27.490> analyzed 00:05:27.930 --> 00:05:27.940 align:start position:0% UBS is dark pool and actually analyzed 00:05:27.940 --> 00:05:30.180 align:start position:0% UBS is dark pool and actually analyzed it<00:05:28.120> for<00:05:28.300> regulatory<00:05:28.570> properties<00:05:29.260> showed<00:05:29.980> how 00:05:30.180 --> 00:05:30.190 align:start position:0% it for regulatory properties showed how 00:05:30.190 --> 00:05:32.310 align:start position:0% it for regulatory properties showed how certain<00:05:30.640> issues<00:05:31.150> that<00:05:31.510> were<00:05:31.720> settled<00:05:32.200> with 00:05:32.310 --> 00:05:32.320 align:start position:0% certain issues that were settled with 00:05:32.320 --> 00:05:35.380 align:start position:0% certain issues that were settled with the<00:05:32.350> SEC<00:05:32.980> could<00:05:33.580> be<00:05:33.670> found<00:05:33.820> automatically 00:05:35.380 --> 00:05:35.390 align:start position:0% the SEC could be found automatically 00:05:35.390 --> 00:05:38.850 align:start position:0% the SEC could be found automatically and<00:05:35.620> many<00:05:36.620> related<00:05:36.860> things<00:05:37.160> so<00:05:37.790> also<00:05:38.090> at<00:05:38.570> the 00:05:38.850 --> 00:05:38.860 align:start position:0% and many related things so also at the 00:05:38.860 --> 00:05:43.060 align:start position:0% and many related things so also at the sort<00:05:39.860> of<00:05:39.950> middle<00:05:40.430> of<00:05:40.900> the<00:05:41.900> summer<00:05:42.320> a<00:05:42.740> little 00:05:43.060 --> 00:05:43.070 align:start position:0% sort of middle of the summer a little 00:05:43.070 --> 00:05:45.370 align:start position:0% sort of middle of the summer a little bit<00:05:43.160> before<00:05:43.490> we<00:05:43.730> finished<00:05:44.270> what<00:05:44.990> is<00:05:45.080> to<00:05:45.290> our 00:05:45.370 --> 00:05:45.380 align:start position:0% bit before we finished what is to our 00:05:45.380 --> 00:05:46.930 align:start position:0% bit before we finished what is to our knowledge<00:05:45.500> as<00:05:45.830> the<00:05:45.950> world's<00:05:46.250> first<00:05:46.400> formally 00:05:46.930 --> 00:05:46.940 align:start position:0% knowledge as the world's first formally 00:05:46.940 --> 00:05:49.030 align:start position:0% knowledge as the world's first formally verified<00:05:46.970> dark<00:05:47.600> pool<00:05:47.810> design<00:05:48.140> for<00:05:48.830> a<00:05:48.860> major 00:05:49.030 --> 00:05:49.040 align:start position:0% verified dark pool design for a major 00:05:49.040 --> 00:05:51.280 align:start position:0% verified dark pool design for a major investment<00:05:49.490> bank<00:05:49.760> where<00:05:50.000> we<00:05:50.150> of<00:05:50.360> course<00:05:50.780> in 00:05:51.280 --> 00:05:51.290 align:start position:0% investment bank where we of course in 00:05:51.290 --> 00:05:54.130 align:start position:0% investment bank where we of course in the<00:05:51.410> process<00:05:52.420> fixing<00:05:53.420> many<00:05:53.570> aspects<00:05:53.960> of<00:05:54.020> their 00:05:54.130 --> 00:05:54.140 align:start position:0% the process fixing many aspects of their 00:05:54.140 --> 00:05:57.610 align:start position:0% the process fixing many aspects of their system<00:05:54.560> were<00:05:54.920> able<00:05:55.250> to<00:05:55.400> prove<00:05:55.990> 114<00:05:56.990> fairness 00:05:57.610 --> 00:05:57.620 align:start position:0% system were able to prove 114 fairness 00:05:57.620 --> 00:05:59.260 align:start position:0% system were able to prove 114 fairness and<00:05:57.740> safety<00:05:58.070> properties<00:05:58.490> ultimately<00:05:59.000> about 00:05:59.260 --> 00:05:59.270 align:start position:0% and safety properties ultimately about 00:05:59.270 --> 00:06:02.530 align:start position:0% and safety properties ultimately about their<00:05:59.750> collection<00:06:00.230> of<00:06:00.350> order<00:06:00.530> types<00:06:01.030> and<00:06:02.030> we 00:06:02.530 --> 00:06:02.540 align:start position:0% their collection of order types and we 00:06:02.540 --> 00:06:04.570 align:start position:0% their collection of order types and we recently<00:06:02.720> closed<00:06:03.170> our<00:06:03.350> seed<00:06:03.590> round<00:06:03.770> backed<00:06:04.430> by 00:06:04.570 --> 00:06:04.580 align:start position:0% recently closed our seed round backed by 00:06:04.580 --> 00:06:06.430 align:start position:0% recently closed our seed round backed by Google's<00:06:05.270> chief<00:06:05.330> business<00:06:05.630> officer<00:06:05.900> Philip 00:06:06.430 --> 00:06:06.440 align:start position:0% Google's chief business officer Philip 00:06:06.440 --> 00:06:08.380 align:start position:0% Google's chief business officer Philip Schindler<00:06:06.770> which<00:06:07.610> is<00:06:07.730> leading<00:06:07.880> to<00:06:08.000> some<00:06:08.240> very 00:06:08.380 --> 00:06:08.390 align:start position:0% Schindler which is leading to some very 00:06:08.390 --> 00:06:10.150 align:start position:0% Schindler which is leading to some very exciting<00:06:08.660> things<00:06:09.020> of<00:06:09.260> getting<00:06:09.860> formal 00:06:10.150 --> 00:06:10.160 align:start position:0% exciting things of getting formal 00:06:10.160 --> 00:06:11.770 align:start position:0% exciting things of getting formal verification<00:06:10.310> out<00:06:10.910> to<00:06:11.090> the<00:06:11.210> masses<00:06:11.360> and 00:06:11.770 --> 00:06:11.780 align:start position:0% verification out to the masses and 00:06:11.780 --> 00:06:14.080 align:start position:0% verification out to the masses and democratizing<00:06:12.620> this<00:06:12.740> technology<00:06:13.310> that<00:06:13.940> has 00:06:14.080 --> 00:06:14.090 align:start position:0% democratizing this technology that has 00:06:14.090 --> 00:06:16.240 align:start position:0% democratizing this technology that has up<00:06:14.240> to<00:06:14.270> now<00:06:14.420> been<00:06:14.780> quite<00:06:15.290> arcane<00:06:15.710> in<00:06:15.920> many<00:06:16.070> ways 00:06:16.240 --> 00:06:16.250 align:start position:0% up to now been quite arcane in many ways 00:06:16.250 --> 00:06:19.090 align:start position:0% up to now been quite arcane in many ways so<00:06:17.120> my<00:06:17.240> co-founder<00:06:17.720> Dennis<00:06:18.020> he<00:06:18.740> was<00:06:18.860> head<00:06:19.070> of 00:06:19.090 --> 00:06:19.100 align:start position:0% so my co-founder Dennis he was head of 00:06:19.100 --> 00:06:20.710 align:start position:0% so my co-founder Dennis he was head of the<00:06:19.280> central<00:06:19.520> risk<00:06:19.760> trading<00:06:20.180> desk<00:06:20.390> at 00:06:20.710 --> 00:06:20.720 align:start position:0% the central risk trading desk at 00:06:20.720 --> 00:06:23.620 align:start position:0% the central risk trading desk at deutsche<00:06:21.140> before<00:06:21.530> we<00:06:21.680> founded<00:06:22.100> a<00:06:22.370> I<00:06:22.610> and<00:06:23.030> my 00:06:23.620 --> 00:06:23.630 align:start position:0% deutsche before we founded a I and my 00:06:23.630 --> 00:06:25.960 align:start position:0% deutsche before we founded a I and my background<00:06:23.840> so<00:06:24.290> I<00:06:24.320> did<00:06:24.710> my<00:06:24.830> PhD<00:06:24.890> in<00:06:25.580> formal 00:06:25.960 --> 00:06:25.970 align:start position:0% background so I did my PhD in formal 00:06:25.970 --> 00:06:28.750 align:start position:0% background so I did my PhD in formal verification<00:06:26.060> at<00:06:26.720> Edinboro<00:06:27.110> a<00:06:27.530> lot<00:06:28.490> of<00:06:28.610> what<00:06:28.730> I 00:06:28.750 --> 00:06:28.760 align:start position:0% verification at Edinboro a lot of what I 00:06:28.760 --> 00:06:30.850 align:start position:0% verification at Edinboro a lot of what I did<00:06:29.030> was<00:06:29.240> around<00:06:29.570> something<00:06:30.080> called<00:06:30.350> an<00:06:30.470> smt 00:06:30.850 --> 00:06:30.860 align:start position:0% did was around something called an smt 00:06:30.860 --> 00:06:32.680 align:start position:0% did was around something called an smt solver<00:06:31.280> called<00:06:31.730> said<00:06:31.940> three<00:06:32.270> so<00:06:32.630> I 00:06:32.680 --> 00:06:32.690 align:start position:0% solver called said three so I 00:06:32.690 --> 00:06:33.910 align:start position:0% solver called said three so I co-authored<00:06:32.900> a<00:06:33.320> lot<00:06:33.440> of<00:06:33.560> the<00:06:33.650> core 00:06:33.910 --> 00:06:33.920 align:start position:0% co-authored a lot of the core 00:06:33.920 --> 00:06:35.680 align:start position:0% co-authored a lot of the core mathematics<00:06:34.460> of<00:06:34.550> Zed<00:06:34.820> three<00:06:35.090> nonlinear 00:06:35.680 --> 00:06:35.690 align:start position:0% mathematics of Zed three nonlinear 00:06:35.690 --> 00:06:38.290 align:start position:0% mathematics of Zed three nonlinear decision<00:06:35.930> procedures<00:06:36.490> and<00:06:37.490> then<00:06:37.790> went<00:06:38.030> down 00:06:38.290 --> 00:06:38.300 align:start position:0% decision procedures and then went down 00:06:38.300 --> 00:06:40.180 align:start position:0% decision procedures and then went down to<00:06:38.330> Cambridge<00:06:38.690> as<00:06:38.810> a<00:06:38.840> postdoc<00:06:39.290> working<00:06:40.070> on 00:06:40.180 --> 00:06:40.190 align:start position:0% to Cambridge as a postdoc working on 00:06:40.190 --> 00:06:41.950 align:start position:0% to Cambridge as a postdoc working on safety<00:06:41.060> and<00:06:41.090> fairness<00:06:41.480> of<00:06:41.600> collision 00:06:41.950 --> 00:06:41.960 align:start position:0% safety and fairness of collision 00:06:41.960 --> 00:06:44.320 align:start position:0% safety and fairness of collision avoidance<00:06:42.290> algorithms<00:06:42.860> and<00:06:43.700> then<00:06:44.240> we 00:06:44.320 --> 00:06:44.330 align:start position:0% avoidance algorithms and then we 00:06:44.330 --> 00:06:45.610 align:start position:0% avoidance algorithms and then we realized<00:06:44.630> we<00:06:44.780> could<00:06:44.900> apply<00:06:45.110> many<00:06:45.410> of<00:06:45.530> these 00:06:45.610 --> 00:06:45.620 align:start position:0% realized we could apply many of these 00:06:45.620 --> 00:06:47.490 align:start position:0% realized we could apply many of these same<00:06:45.830> techniques<00:06:46.040> to<00:06:46.430> financial<00:06:46.850> algorithms 00:06:47.490 --> 00:06:47.500 align:start position:0% same techniques to financial algorithms 00:06:47.500 --> 00:06:50.200 align:start position:0% same techniques to financial algorithms so<00:06:48.500> we<00:06:48.620> all<00:06:48.710> know<00:06:48.890> the<00:06:49.040> problems<00:06:49.520> that<00:06:49.850> are 00:06:50.200 --> 00:06:50.210 align:start position:0% so we all know the problems that are 00:06:50.210 --> 00:06:52.060 align:start position:0% so we all know the problems that are motivating<00:06:50.450> formal<00:06:51.230> verification<00:06:51.350> being 00:06:52.060 --> 00:06:52.070 align:start position:0% motivating formal verification being 00:06:52.070 --> 00:06:54.580 align:start position:0% motivating formal verification being taken<00:06:52.460> up<00:06:52.580> in<00:06:52.760> our<00:06:53.030> community<00:06:53.510> so<00:06:54.410> I<00:06:54.440> don't 00:06:54.580 --> 00:06:54.590 align:start position:0% taken up in our community so I don't 00:06:54.590 --> 00:06:57.190 align:start position:0% taken up in our community so I don't need<00:06:54.740> to<00:06:54.860> belabor<00:06:55.280> those<00:06:55.610> but<00:06:56.510> there<00:06:56.930> are<00:06:57.050> some 00:06:57.190 --> 00:06:57.200 align:start position:0% need to belabor those but there are some 00:06:57.200 --> 00:06:58.390 align:start position:0% need to belabor those but there are some other<00:06:57.350> aspects<00:06:57.860> that<00:06:57.920> haven't<00:06:58.340> been 00:06:58.390 --> 00:06:58.400 align:start position:0% other aspects that haven't been 00:06:58.400 --> 00:07:01.300 align:start position:0% other aspects that haven't been mentioned<00:06:58.850> at<00:06:59.270> least<00:06:59.450> that<00:06:59.630> I've<00:06:59.720> seen<00:07:00.020> and<00:07:00.310> in 00:07:01.300 --> 00:07:01.310 align:start position:0% mentioned at least that I've seen and in 00:07:01.310 --> 00:07:03.610 align:start position:0% mentioned at least that I've seen and in addition<00:07:01.520> to<00:07:02.060> the<00:07:02.660> need<00:07:02.900> for<00:07:03.140> automated 00:07:03.610 --> 00:07:03.620 align:start position:0% addition to the need for automated 00:07:03.620 --> 00:07:05.380 align:start position:0% addition to the need for automated auditing<00:07:04.040> tools<00:07:04.310> around<00:07:04.700> correctness 00:07:05.380 --> 00:07:05.390 align:start position:0% auditing tools around correctness 00:07:05.390 --> 00:07:08.380 align:start position:0% auditing tools around correctness fairness<00:07:06.140> and<00:07:06.290> safety<00:07:06.770> of<00:07:07.580> course<00:07:07.850> mitigating 00:07:08.380 --> 00:07:08.390 align:start position:0% fairness and safety of course mitigating 00:07:08.390 --> 00:07:11.160 align:start position:0% fairness and safety of course mitigating subtle<00:07:09.140> bugs<00:07:09.320> and<00:07:09.680> so<00:07:09.800> on<00:07:09.980> we<00:07:10.760> also<00:07:10.940> need 00:07:11.160 --> 00:07:11.170 align:start position:0% subtle bugs and so on we also need 00:07:11.170 --> 00:07:13.540 align:start position:0% subtle bugs and so on we also need fundamentally<00:07:12.170> robust<00:07:12.710> tools<00:07:13.040> for<00:07:13.400> risk 00:07:13.540 --> 00:07:13.550 align:start position:0% fundamentally robust tools for risk 00:07:13.550 --> 00:07:15.910 align:start position:0% fundamentally robust tools for risk management<00:07:13.690> so<00:07:14.690> I'm<00:07:14.810> talking<00:07:15.200> here<00:07:15.230> for<00:07:15.680> you 00:07:15.910 --> 00:07:15.920 align:start position:0% management so I'm talking here for you 00:07:15.920 --> 00:07:17.500 align:start position:0% management so I'm talking here for you know<00:07:16.040> those<00:07:16.220> of<00:07:16.370> you<00:07:16.520> at<00:07:16.730> an<00:07:17.240> investment 00:07:17.500 --> 00:07:17.510 align:start position:0% know those of you at an investment 00:07:17.510 --> 00:07:20.110 align:start position:0% know those of you at an investment banking<00:07:18.050> where<00:07:18.650> you<00:07:18.980> have<00:07:19.160> exposure<00:07:19.550> you<00:07:20.030> know 00:07:20.110 --> 00:07:20.120 align:start position:0% banking where you have exposure you know 00:07:20.120 --> 00:07:22.840 align:start position:0% banking where you have exposure you know imagine<00:07:20.680> an<00:07:21.680> investment<00:07:22.220> bank<00:07:22.370> goes<00:07:22.580> all-in 00:07:22.840 --> 00:07:22.850 align:start position:0% imagine an investment bank goes all-in 00:07:22.850 --> 00:07:25.930 align:start position:0% imagine an investment bank goes all-in on<00:07:23.390> etherium<00:07:24.260> and<00:07:24.500> five<00:07:25.130> years<00:07:25.370> from<00:07:25.490> now<00:07:25.610> has 00:07:25.930 --> 00:07:25.940 align:start position:0% on etherium and five years from now has 00:07:25.940 --> 00:07:27.790 align:start position:0% on etherium and five years from now has a<00:07:25.970> hundred<00:07:26.330> thousand<00:07:26.780> smart<00:07:27.080> contracts<00:07:27.530> in<00:07:27.710> a 00:07:27.790 --> 00:07:27.800 align:start position:0% a hundred thousand smart contracts in a 00:07:27.800 --> 00:07:30.850 align:start position:0% a hundred thousand smart contracts in a portfolio<00:07:28.420> what<00:07:29.420> is<00:07:29.540> their<00:07:29.720> exposure<00:07:30.110> how<00:07:30.800> do 00:07:30.850 --> 00:07:30.860 align:start position:0% portfolio what is their exposure how do 00:07:30.860 --> 00:07:33.220 align:start position:0% portfolio what is their exposure how do you<00:07:30.980> calculate<00:07:31.190> risk<00:07:31.760> how<00:07:32.300> do<00:07:32.360> you<00:07:32.450> price<00:07:32.840> for 00:07:33.220 --> 00:07:33.230 align:start position:0% you calculate risk how do you price for 00:07:33.230 --> 00:07:34.660 align:start position:0% you calculate risk how do you price for instance<00:07:33.560> derivatives<00:07:34.220> and<00:07:34.400> structured 00:07:34.660 --> 00:07:34.670 align:start position:0% instance derivatives and structured 00:07:34.670 --> 00:07:36.460 align:start position:0% instance derivatives and structured products<00:07:35.210> that<00:07:35.720> are<00:07:35.840> expressed<00:07:36.140> as 00:07:36.460 --> 00:07:36.470 align:start position:0% products that are expressed as 00:07:36.470 --> 00:07:39.310 align:start position:0% products that are expressed as ultimately<00:07:36.980> athyrium<00:07:37.490> by<00:07:37.640> code<00:07:37.880> and<00:07:38.840> that's 00:07:39.310 --> 00:07:39.320 align:start position:0% ultimately athyrium by code and that's 00:07:39.320 --> 00:07:40.870 align:start position:0% ultimately athyrium by code and that's another<00:07:39.560> place<00:07:39.860> where<00:07:40.070> we<00:07:40.250> see<00:07:40.460> formal 00:07:40.870 --> 00:07:40.880 align:start position:0% another place where we see formal 00:07:40.880 --> 00:07:43.180 align:start position:0% another place where we see formal verification<00:07:41.000> as<00:07:41.690> being<00:07:41.960> utterly<00:07:42.200> crucial<00:07:42.680> so 00:07:43.180 --> 00:07:43.190 align:start position:0% verification as being utterly crucial so 00:07:43.190 --> 00:07:45.040 align:start position:0% verification as being utterly crucial so some<00:07:43.790> of<00:07:43.820> the<00:07:44.000> things<00:07:44.210> we're<00:07:44.360> building<00:07:44.660> on<00:07:44.780> top 00:07:45.040 --> 00:07:45.050 align:start position:0% some of the things we're building on top 00:07:45.050 --> 00:07:46.519 align:start position:0% some of the things we're building on top of<00:07:45.260> our<00:07:45.350> formalized<00:07:45.920> EDM 00:07:46.519 --> 00:07:46.529 align:start position:0% of our formalized EDM 00:07:46.529 --> 00:07:49.309 align:start position:0% of our formalized EDM in<00:07:46.769> a<00:07:46.949> mantra<00:07:47.339> are<00:07:47.879> around<00:07:48.269> exactly<00:07:48.839> this<00:07:49.019> risk 00:07:49.309 --> 00:07:49.319 align:start position:0% in a mantra are around exactly this risk 00:07:49.319 --> 00:07:51.469 align:start position:0% in a mantra are around exactly this risk management<00:07:49.859> calculating<00:07:50.789> Greeks<00:07:51.029> and<00:07:51.239> market 00:07:51.469 --> 00:07:51.479 align:start position:0% management calculating Greeks and market 00:07:51.479 --> 00:07:53.119 align:start position:0% management calculating Greeks and market exposure<00:07:51.779> linked<00:07:52.439> directly<00:07:52.589> to<00:07:52.889> the 00:07:53.119 --> 00:07:53.129 align:start position:0% exposure linked directly to the 00:07:53.129 --> 00:07:56.229 align:start position:0% exposure linked directly to the semantics<00:07:53.669> of<00:07:53.669> the<00:07:53.849> bytecode<00:07:54.349> so<00:07:55.349> mandra 00:07:56.229 --> 00:07:56.239 align:start position:0% semantics of the bytecode so mandra 00:07:56.239 --> 00:07:58.009 align:start position:0% semantics of the bytecode so mandra leverages<00:07:57.239> a<00:07:57.449> number<00:07:57.719> of<00:07:57.839> recent 00:07:58.009 --> 00:07:58.019 align:start position:0% leverages a number of recent 00:07:58.019 --> 00:08:00.859 align:start position:0% leverages a number of recent breakthroughs<00:07:58.649> in<00:07:58.679> formal<00:07:59.219> verification<00:07:59.869> smt 00:08:00.859 --> 00:08:00.869 align:start position:0% breakthroughs in formal verification smt 00:08:00.869 --> 00:08:02.629 align:start position:0% breakthroughs in formal verification smt which<00:08:01.289> is<00:08:01.469> powerful<00:08:01.979> automated<00:08:02.129> proof 00:08:02.629 --> 00:08:02.639 align:start position:0% which is powerful automated proof 00:08:02.639 --> 00:08:05.089 align:start position:0% which is powerful automated proof techniques<00:08:03.089> combining<00:08:04.049> SAT<00:08:04.289> solvers<00:08:04.769> what 00:08:05.089 --> 00:08:05.099 align:start position:0% techniques combining SAT solvers what 00:08:05.099 --> 00:08:07.369 align:start position:0% techniques combining SAT solvers what really<00:08:05.459> powers<00:08:05.939> formal<00:08:06.659> verification<00:08:06.779> for 00:08:07.369 --> 00:08:07.379 align:start position:0% really powers formal verification for 00:08:07.379 --> 00:08:10.129 align:start position:0% really powers formal verification for hardware<00:08:07.769> combining<00:08:08.759> those<00:08:08.879> techniques<00:08:09.359> with 00:08:10.129 --> 00:08:10.139 align:start position:0% hardware combining those techniques with 00:08:10.139 --> 00:08:12.559 align:start position:0% hardware combining those techniques with richer<00:08:10.669> mathematical<00:08:11.669> theories<00:08:11.999> things<00:08:12.359> like 00:08:12.559 --> 00:08:12.569 align:start position:0% richer mathematical theories things like 00:08:12.569 --> 00:08:14.749 align:start position:0% richer mathematical theories things like reasoning<00:08:13.289> about<00:08:13.409> arrays<00:08:13.739> and<00:08:14.159> bit<00:08:14.369> vectors 00:08:14.749 --> 00:08:14.759 align:start position:0% reasoning about arrays and bit vectors 00:08:14.759 --> 00:08:17.179 align:start position:0% reasoning about arrays and bit vectors and<00:08:15.119> nonlinear<00:08:16.079> and<00:08:16.259> linear<00:08:16.499> inequalities 00:08:17.179 --> 00:08:17.189 align:start position:0% and nonlinear and linear inequalities 00:08:17.189 --> 00:08:20.329 align:start position:0% and nonlinear and linear inequalities and<00:08:17.339> so<00:08:17.489> on<00:08:18.769> model-based<00:08:19.769> automated 00:08:20.329 --> 00:08:20.339 align:start position:0% and so on model-based automated 00:08:20.339 --> 00:08:22.609 align:start position:0% and so on model-based automated induction<00:08:20.639> plays<00:08:21.059> a<00:08:21.089> huge<00:08:21.329> role<00:08:21.449> so<00:08:22.349> when<00:08:22.499> you 00:08:22.609 --> 00:08:22.619 align:start position:0% induction plays a huge role so when you 00:08:22.619 --> 00:08:25.339 align:start position:0% induction plays a huge role so when you have<00:08:22.799> algorithms<00:08:23.489> that<00:08:24.089> ultimately<00:08:24.599> iterate 00:08:25.339 --> 00:08:25.349 align:start position:0% have algorithms that ultimately iterate 00:08:25.349 --> 00:08:28.419 align:start position:0% have algorithms that ultimately iterate or<00:08:25.619> you<00:08:26.429> know<00:08:26.549> when<00:08:26.729> it<00:08:26.849> when<00:08:26.999> expressed<00:08:27.419> in<00:08:27.569> a 00:08:28.419 --> 00:08:28.429 align:start position:0% or you know when it when expressed in a 00:08:28.429 --> 00:08:32.389 align:start position:0% or you know when it when expressed in a logic<00:08:29.429> may<00:08:30.359> be<00:08:30.629> expressed<00:08:30.899> as<00:08:31.109> recursion<00:08:31.649> you 00:08:32.389 --> 00:08:32.399 align:start position:0% logic may be expressed as recursion you 00:08:32.399 --> 00:08:33.739 align:start position:0% logic may be expressed as recursion you typically<00:08:32.699> need<00:08:32.789> to<00:08:33.029> prove<00:08:33.209> theorems<00:08:33.569> by 00:08:33.739 --> 00:08:33.749 align:start position:0% typically need to prove theorems by 00:08:33.749 --> 00:08:37.369 align:start position:0% typically need to prove theorems by induction<00:08:34.050> either<00:08:34.709> by<00:08:35.479> techniques<00:08:36.479> like<00:08:36.689> you 00:08:37.369 --> 00:08:37.379 align:start position:0% induction either by techniques like you 00:08:37.379 --> 00:08:39.769 align:start position:0% induction either by techniques like you know<00:08:37.499> writing<00:08:37.919> out<00:08:38.189> inductive<00:08:38.699> invariants<00:08:39.300> as 00:08:39.769 --> 00:08:39.779 align:start position:0% know writing out inductive invariants as 00:08:39.779 --> 00:08:41.899 align:start position:0% know writing out inductive invariants as we<00:08:40.019> saw<00:08:40.229> with<00:08:40.829> the<00:08:40.979> work<00:08:41.099> of<00:08:41.249> Christian<00:08:41.639> and 00:08:41.899 --> 00:08:41.909 align:start position:0% we saw with the work of Christian and 00:08:41.909 --> 00:08:44.960 align:start position:0% we saw with the work of Christian and your<00:08:42.300> Chewie<00:08:42.479> with<00:08:42.689> y3<00:08:43.139> or<00:08:43.949> with<00:08:44.579> proving 00:08:44.960 --> 00:08:44.970 align:start position:0% your Chewie with y3 or with proving 00:08:44.970 --> 00:08:46.970 align:start position:0% your Chewie with y3 or with proving inductive<00:08:45.389> limos<00:08:45.779> that<00:08:46.199> then<00:08:46.379> get<00:08:46.529> used<00:08:46.769> for 00:08:46.970 --> 00:08:46.980 align:start position:0% inductive limos that then get used for 00:08:46.980 --> 00:08:48.679 align:start position:0% inductive limos that then get used for instance<00:08:47.220> as<00:08:47.339> rewrite<00:08:47.639> rules<00:08:47.879> these<00:08:48.540> are<00:08:48.629> all 00:08:48.679 --> 00:08:48.689 align:start position:0% instance as rewrite rules these are all 00:08:48.689 --> 00:08:50.590 align:start position:0% instance as rewrite rules these are all bread<00:08:48.959> and<00:08:49.079> butter<00:08:49.230> for<00:08:49.319> formal<00:08:50.129> verification 00:08:50.590 --> 00:08:50.600 align:start position:0% bread and butter for formal verification 00:08:50.600 --> 00:08:53.660 align:start position:0% bread and butter for formal verification but<00:08:51.600> we<00:08:52.139> now<00:08:52.259> have<00:08:52.500> much<00:08:52.889> more<00:08:53.040> powerful<00:08:53.339> tools 00:08:53.660 --> 00:08:53.670 align:start position:0% but we now have much more powerful tools 00:08:53.670 --> 00:08:55.879 align:start position:0% but we now have much more powerful tools for<00:08:54.029> for<00:08:54.509> instance<00:08:54.809> using<00:08:55.079> counter<00:08:55.410> examples 00:08:55.879 --> 00:08:55.889 align:start position:0% for for instance using counter examples 00:08:55.889 --> 00:08:58.069 align:start position:0% for for instance using counter examples to<00:08:56.370> help<00:08:56.399> us<00:08:56.730> guide<00:08:56.970> the<00:08:57.269> way<00:08:57.389> we<00:08:57.569> inductively 00:08:58.069 --> 00:08:58.079 align:start position:0% to help us guide the way we inductively 00:08:58.079 --> 00:08:59.780 align:start position:0% to help us guide the way we inductively generalize<00:08:58.649> which<00:08:59.160> is<00:08:59.309> something<00:08:59.399> you<00:08:59.610> often 00:08:59.780 --> 00:08:59.790 align:start position:0% generalize which is something you often 00:08:59.790 --> 00:09:01.639 align:start position:0% generalize which is something you often need<00:08:59.939> to<00:09:00.149> do<00:09:00.269> when<00:09:00.899> proving<00:09:01.230> theorems<00:09:01.379> by 00:09:01.639 --> 00:09:01.649 align:start position:0% need to do when proving theorems by 00:09:01.649 --> 00:09:03.740 align:start position:0% need to do when proving theorems by induction<00:09:01.949> but<00:09:02.850> fundamentally<00:09:03.480> what<00:09:03.629> we're 00:09:03.740 --> 00:09:03.750 align:start position:0% induction but fundamentally what we're 00:09:03.750 --> 00:09:06.439 align:start position:0% induction but fundamentally what we're doing<00:09:04.019> with<00:09:04.230> the<00:09:04.350> Amanda<00:09:04.740> cloud<00:09:04.980> is<00:09:05.449> aiming<00:09:06.449> to 00:09:06.439 --> 00:09:06.449 align:start position:0% doing with the Amanda cloud is aiming to 00:09:06.449 --> 00:09:08.360 align:start position:0% doing with the Amanda cloud is aiming to really<00:09:06.839> democratize<00:09:07.559> access<00:09:07.589> to<00:09:08.250> these 00:09:08.360 --> 00:09:08.370 align:start position:0% really democratize access to these 00:09:08.370 --> 00:09:10.549 align:start position:0% really democratize access to these techniques<00:09:08.759> and<00:09:09.059> make<00:09:09.360> them<00:09:09.540> usable<00:09:09.809> to 00:09:10.549 --> 00:09:10.559 align:start position:0% techniques and make them usable to 00:09:10.559 --> 00:09:12.920 align:start position:0% techniques and make them usable to developers<00:09:11.069> and<00:09:11.279> non<00:09:11.370> developers<00:09:11.879> alike<00:09:12.000> we 00:09:12.920 --> 00:09:12.930 align:start position:0% developers and non developers alike we 00:09:12.930 --> 00:09:14.840 align:start position:0% developers and non developers alike we all<00:09:13.050> need<00:09:13.319> them<00:09:13.529> and<00:09:14.100> need<00:09:14.309> them<00:09:14.430> to<00:09:14.550> be<00:09:14.670> easy 00:09:14.840 --> 00:09:14.850 align:start position:0% all need them and need them to be easy 00:09:14.850 --> 00:09:18.860 align:start position:0% all need them and need them to be easy so<00:09:16.040> fundamentally<00:09:17.040> you<00:09:17.850> give<00:09:18.000> a<00:09:18.029> mantra<00:09:18.569> to 00:09:18.860 --> 00:09:18.870 align:start position:0% so fundamentally you give a mantra to 00:09:18.870 --> 00:09:21.860 align:start position:0% so fundamentally you give a mantra to things<00:09:19.170> a<00:09:19.439> smart<00:09:19.829> contract<00:09:20.750> let's<00:09:21.750> say 00:09:21.860 --> 00:09:21.870 align:start position:0% things a smart contract let's say 00:09:21.870 --> 00:09:23.449 align:start position:0% things a smart contract let's say expressed<00:09:22.290> as<00:09:22.439> a<00:09:22.470> theory<00:09:22.740> and<00:09:22.860> byte<00:09:23.040> code<00:09:23.250> for 00:09:23.449 --> 00:09:23.459 align:start position:0% expressed as a theory and byte code for 00:09:23.459 --> 00:09:25.220 align:start position:0% expressed as a theory and byte code for instance<00:09:23.759> and<00:09:23.970> a<00:09:24.329> property<00:09:24.750> you<00:09:24.899> wish<00:09:25.050> to 00:09:25.220 --> 00:09:25.230 align:start position:0% instance and a property you wish to 00:09:25.230 --> 00:09:27.350 align:start position:0% instance and a property you wish to verify<00:09:25.649> and<00:09:25.920> a<00:09:26.250> mantra<00:09:26.550> will<00:09:26.730> work<00:09:26.939> to<00:09:27.209> either 00:09:27.350 --> 00:09:27.360 align:start position:0% verify and a mantra will work to either 00:09:27.360 --> 00:09:29.809 align:start position:0% verify and a mantra will work to either give<00:09:27.779> you<00:09:27.809> a<00:09:27.930> proof<00:09:28.199> of<00:09:28.379> that<00:09:28.470> property<00:09:28.819> or 00:09:29.809 --> 00:09:29.819 align:start position:0% give you a proof of that property or 00:09:29.819 --> 00:09:32.629 align:start position:0% give you a proof of that property or work<00:09:30.600> to<00:09:30.779> show<00:09:30.929> you<00:09:30.990> a<00:09:31.110> counter<00:09:31.470> example<00:09:31.639> where 00:09:32.629 --> 00:09:32.639 align:start position:0% work to show you a counter example where 00:09:32.639 --> 00:09:35.809 align:start position:0% work to show you a counter example where a<00:09:32.670> property<00:09:33.120> fails<00:09:33.329> and<00:09:34.069> then<00:09:35.069> there's<00:09:35.279> I'll 00:09:35.809 --> 00:09:35.819 align:start position:0% a property fails and then there's I'll 00:09:35.819 --> 00:09:37.460 align:start position:0% a property fails and then there's I'll show<00:09:35.970> you<00:09:36.029> many<00:09:36.209> ways<00:09:36.779> that<00:09:37.079> you<00:09:37.110> can<00:09:37.319> get 00:09:37.460 --> 00:09:37.470 align:start position:0% show you many ways that you can get 00:09:37.470 --> 00:09:38.840 align:start position:0% show you many ways that you can get involved<00:09:37.709> in<00:09:38.009> that<00:09:38.100> process<00:09:38.370> and 00:09:38.840 --> 00:09:38.850 align:start position:0% involved in that process and 00:09:38.850 --> 00:09:41.360 align:start position:0% involved in that process and interactively<00:09:39.420> work<00:09:39.660> with<00:09:39.809> the<00:09:39.899> mantra<00:09:40.259> so<00:09:41.069> a 00:09:41.360 --> 00:09:41.370 align:start position:0% interactively work with the mantra so a 00:09:41.370 --> 00:09:44.449 align:start position:0% interactively work with the mantra so a mantra<00:09:42.089> is<00:09:42.660> a<00:09:43.079> programming<00:09:43.889> language<00:09:43.920> a 00:09:44.449 --> 00:09:44.459 align:start position:0% mantra is a programming language a 00:09:44.459 --> 00:09:46.340 align:start position:0% mantra is a programming language a mathematical<00:09:45.389> logic<00:09:45.509> and<00:09:45.870> a<00:09:45.929> reasoning 00:09:46.340 --> 00:09:46.350 align:start position:0% mathematical logic and a reasoning 00:09:46.350 --> 00:09:48.079 align:start position:0% mathematical logic and a reasoning engine<00:09:46.589> all<00:09:46.740> in<00:09:46.889> one<00:09:47.129> it's<00:09:47.429> a<00:09:47.579> formalized 00:09:48.079 --> 00:09:48.089 align:start position:0% engine all in one it's a formalized 00:09:48.089 --> 00:09:49.939 align:start position:0% engine all in one it's a formalized subset<00:09:48.600> of<00:09:48.629> a<00:09:48.870> functional<00:09:49.319> language<00:09:49.620> called<00:09:49.860> o 00:09:49.939 --> 00:09:49.949 align:start position:0% subset of a functional language called o 00:09:49.949 --> 00:09:53.419 align:start position:0% subset of a functional language called o camel<00:09:51.110> crucially<00:09:52.110> when<00:09:52.559> designing<00:09:52.860> a<00:09:53.040> mantra 00:09:53.419 --> 00:09:53.429 align:start position:0% camel crucially when designing a mantra 00:09:53.429 --> 00:09:54.829 align:start position:0% camel crucially when designing a mantra you<00:09:53.550> know<00:09:53.639> we<00:09:53.759> set<00:09:53.939> out<00:09:54.029> to<00:09:54.059> design<00:09:54.420> our<00:09:54.449> dream 00:09:54.829 --> 00:09:54.839 align:start position:0% you know we set out to design our dream 00:09:54.839 --> 00:09:56.689 align:start position:0% you know we set out to design our dream formal<00:09:55.230> verification<00:09:55.350> system<00:09:56.129> and<00:09:56.279> one<00:09:56.670> of 00:09:56.689 --> 00:09:56.699 align:start position:0% formal verification system and one of 00:09:56.699 --> 00:09:58.040 align:start position:0% formal verification system and one of the<00:09:56.819> most<00:09:56.970> important<00:09:57.389> things<00:09:57.569> is<00:09:57.779> having 00:09:58.040 --> 00:09:58.050 align:start position:0% the most important things is having 00:09:58.050 --> 00:09:59.319 align:start position:0% the most important things is having first-class<00:09:58.470> counter<00:09:58.949> exam 00:09:59.319 --> 00:09:59.329 align:start position:0% first-class counter exam 00:09:59.329 --> 00:10:02.439 align:start position:0% first-class counter exam so<00:10:00.079> in<00:10:00.709> a<00:10:00.860> mantra<00:10:01.189> we're<00:10:01.369> always<00:10:01.670> working<00:10:02.119> to 00:10:02.439 --> 00:10:02.449 align:start position:0% so in a mantra we're always working to 00:10:02.449 --> 00:10:03.939 align:start position:0% so in a mantra we're always working to find<00:10:02.720> counter-examples<00:10:03.259> to<00:10:03.739> false 00:10:03.939 --> 00:10:03.949 align:start position:0% find counter-examples to false 00:10:03.949 --> 00:10:06.069 align:start position:0% find counter-examples to false conjectures<00:10:04.549> and<00:10:04.759> actually<00:10:05.509> reflect<00:10:05.929> those 00:10:06.069 --> 00:10:06.079 align:start position:0% conjectures and actually reflect those 00:10:06.079 --> 00:10:08.199 align:start position:0% conjectures and actually reflect those into<00:10:06.379> the<00:10:06.410> runtime<00:10:06.949> and<00:10:07.129> into<00:10:07.309> the<00:10:07.429> logic<00:10:07.790> so 00:10:08.199 --> 00:10:08.209 align:start position:0% into the runtime and into the logic so 00:10:08.209 --> 00:10:09.879 align:start position:0% into the runtime and into the logic so that<00:10:08.360> you<00:10:08.420> can<00:10:08.569> compute<00:10:08.929> with<00:10:09.049> them<00:10:09.230> which<00:10:09.860> is 00:10:09.879 --> 00:10:09.889 align:start position:0% that you can compute with them which is 00:10:09.889 --> 00:10:12.879 align:start position:0% that you can compute with them which is which<00:10:10.279> is<00:10:10.309> really<00:10:10.549> crucial<00:10:10.759> so<00:10:11.689> there's<00:10:12.139> see<00:10:12.860> I 00:10:12.879 --> 00:10:12.889 align:start position:0% which is really crucial so there's see I 00:10:12.889 --> 00:10:15.400 align:start position:0% which is really crucial so there's see I really<00:10:13.129> don't<00:10:13.309> have<00:10:13.429> much<00:10:13.459> time<00:10:13.790> so<00:10:14.089> I<00:10:14.869> want<00:10:15.319> to 00:10:15.400 --> 00:10:15.410 align:start position:0% really don't have much time so I want to 00:10:15.410 --> 00:10:18.160 align:start position:0% really don't have much time so I want to just<00:10:15.589> show<00:10:15.649> you<00:10:16.449> probably<00:10:17.449> impossible<00:10:17.749> to 00:10:18.160 --> 00:10:18.170 align:start position:0% just show you probably impossible to 00:10:18.170 --> 00:10:20.889 align:start position:0% just show you probably impossible to read<00:10:18.350> but<00:10:18.949> this<00:10:19.730> is<00:10:19.999> a<00:10:20.029> little<00:10:20.449> bit<00:10:20.569> of<00:10:20.629> a<00:10:20.720> walk 00:10:20.889 --> 00:10:20.899 align:start position:0% read but this is a little bit of a walk 00:10:20.899 --> 00:10:22.720 align:start position:0% read but this is a little bit of a walk through<00:10:21.170> of<00:10:21.199> our<00:10:21.439> formalized<00:10:22.040> to<00:10:22.369> theorem 00:10:22.720 --> 00:10:22.730 align:start position:0% through of our formalized to theorem 00:10:22.730 --> 00:10:24.850 align:start position:0% through of our formalized to theorem virtual<00:10:23.089> machine<00:10:23.420> and<00:10:23.449> a<00:10:23.720> mantra<00:10:24.110> and<00:10:24.319> the<00:10:24.769> way 00:10:24.850 --> 00:10:24.860 align:start position:0% virtual machine and a mantra and the way 00:10:24.860 --> 00:10:26.559 align:start position:0% virtual machine and a mantra and the way you<00:10:24.920> formalize<00:10:25.429> this<00:10:25.699> because<00:10:26.119> a<00:10:26.149> mantra<00:10:26.509> is 00:10:26.559 --> 00:10:26.569 align:start position:0% you formalize this because a mantra is 00:10:26.569 --> 00:10:28.900 align:start position:0% you formalize this because a mantra is logic<00:10:27.019> is<00:10:27.170> also<00:10:27.559> an<00:10:27.709> executable<00:10:28.279> programming 00:10:28.900 --> 00:10:28.910 align:start position:0% logic is also an executable programming 00:10:28.910 --> 00:10:30.879 align:start position:0% logic is also an executable programming language<00:10:29.209> you<00:10:29.899> actually<00:10:30.079> just<00:10:30.319> feel<00:10:30.739> like 00:10:30.879 --> 00:10:30.889 align:start position:0% language you actually just feel like 00:10:30.889 --> 00:10:32.919 align:start position:0% language you actually just feel like you're<00:10:31.069> writing<00:10:31.519> a<00:10:31.670> simulator<00:10:32.269> for<00:10:32.809> the 00:10:32.919 --> 00:10:32.929 align:start position:0% you're writing a simulator for the 00:10:32.929 --> 00:10:35.100 align:start position:0% you're writing a simulator for the virtual<00:10:33.290> machine<00:10:33.439> writing<00:10:34.189> an<00:10:34.279> interpreter 00:10:35.100 --> 00:10:35.110 align:start position:0% virtual machine writing an interpreter 00:10:35.110 --> 00:10:37.660 align:start position:0% virtual machine writing an interpreter defining<00:10:36.110> precisely<00:10:36.499> the<00:10:36.799> memory<00:10:37.100> model<00:10:37.519> the 00:10:37.660 --> 00:10:37.670 align:start position:0% defining precisely the memory model the 00:10:37.670 --> 00:10:40.150 align:start position:0% defining precisely the memory model the storage<00:10:38.029> model<00:10:38.480> all<00:10:39.379> of<00:10:39.619> the<00:10:39.739> instructions 00:10:40.150 --> 00:10:40.160 align:start position:0% storage model all of the instructions 00:10:40.160 --> 00:10:42.999 align:start position:0% storage model all of the instructions and<00:10:40.670> how<00:10:41.449> those<00:10:41.629> operate<00:10:42.199> on<00:10:42.350> the<00:10:42.470> state<00:10:42.739> and 00:10:42.999 --> 00:10:43.009 align:start position:0% and how those operate on the state and 00:10:43.009 --> 00:10:44.530 align:start position:0% and how those operate on the state and then<00:10:43.429> ultimately<00:10:43.519> there's<00:10:44.089> a<00:10:44.149> top-level 00:10:44.530 --> 00:10:44.540 align:start position:0% then ultimately there's a top-level 00:10:44.540 --> 00:10:46.509 align:start position:0% then ultimately there's a top-level state<00:10:44.899> transition<00:10:45.439> function<00:10:45.470> and<00:10:46.040> then 00:10:46.509 --> 00:10:46.519 align:start position:0% state transition function and then 00:10:46.519 --> 00:10:49.419 align:start position:0% state transition function and then finally<00:10:46.970> that's<00:10:47.149> iterated<00:10:47.689> right<00:10:48.309> until<00:10:49.309> you 00:10:49.419 --> 00:10:49.429 align:start position:0% finally that's iterated right until you 00:10:49.429 --> 00:10:51.669 align:start position:0% finally that's iterated right until you run<00:10:49.519> out<00:10:49.579> of<00:10:49.699> gas<00:10:49.879> or<00:10:50.119> reach<00:10:50.689> an<00:10:51.199> exceptional 00:10:51.669 --> 00:10:51.679 align:start position:0% run out of gas or reach an exceptional 00:10:51.679 --> 00:10:54.369 align:start position:0% run out of gas or reach an exceptional halting<00:10:51.980> state<00:10:52.220> or<00:10:52.519> you<00:10:52.730> halt<00:10:53.569> in<00:10:53.869> a<00:10:54.019> nice<00:10:54.170> way 00:10:54.369 --> 00:10:54.379 align:start position:0% halting state or you halt in a nice way 00:10:54.379 --> 00:10:57.879 align:start position:0% halting state or you halt in a nice way so<00:10:55.249> in<00:10:55.639> a<00:10:55.790> mantra<00:10:56.179> by<00:10:56.899> the<00:10:56.959> way<00:10:57.139> we<00:10:57.860> are 00:10:57.879 --> 00:10:57.889 align:start position:0% so in a mantra by the way we are 00:10:57.889 --> 00:11:01.329 align:start position:0% so in a mantra by the way we are releasing<00:10:58.399> our<00:10:58.850> EVM<00:10:59.389> model<00:10:59.829> under<00:11:00.829> a<00:11:00.889> patchy<00:11:01.069> 2 00:11:01.329 --> 00:11:01.339 align:start position:0% releasing our EVM model under a patchy 2 00:11:01.339 --> 00:11:03.519 align:start position:0% releasing our EVM model under a patchy 2 point<00:11:01.610> 0<00:11:01.730> and<00:11:01.939> so<00:11:02.209> our<00:11:02.420> hope<00:11:02.660> is<00:11:02.869> that<00:11:02.899> the 00:11:03.519 --> 00:11:03.529 align:start position:0% point 0 and so our hope is that the 00:11:03.529 --> 00:11:05.679 align:start position:0% point 0 and so our hope is that the community<00:11:03.949> will<00:11:04.129> manage<00:11:04.879> this<00:11:05.119> port<00:11:05.540> it<00:11:05.660> to 00:11:05.679 --> 00:11:05.689 align:start position:0% community will manage this port it to 00:11:05.689 --> 00:11:08.769 align:start position:0% community will manage this port it to other<00:11:05.989> systems<00:11:06.459> and<00:11:07.459> it<00:11:08.329> can<00:11:08.480> be<00:11:08.600> something 00:11:08.769 --> 00:11:08.779 align:start position:0% other systems and it can be something 00:11:08.779 --> 00:11:11.019 align:start position:0% other systems and it can be something that<00:11:08.929> evolves<00:11:09.230> as<00:11:09.709> the<00:11:09.980> you<00:11:10.369> know<00:11:10.489> design<00:11:10.879> of 00:11:11.019 --> 00:11:11.029 align:start position:0% that evolves as the you know design of 00:11:11.029 --> 00:11:13.269 align:start position:0% that evolves as the you know design of etherium<00:11:11.389> evolves<00:11:11.919> but<00:11:12.919> what<00:11:13.009> I'm<00:11:13.100> showing 00:11:13.269 --> 00:11:13.279 align:start position:0% etherium evolves but what I'm showing 00:11:13.279 --> 00:11:15.100 align:start position:0% etherium evolves but what I'm showing you<00:11:13.429> here<00:11:13.519> now<00:11:13.910> this<00:11:14.119> is<00:11:14.299> a<00:11:14.329> very<00:11:14.629> very<00:11:14.809> low 00:11:15.100 --> 00:11:15.110 align:start position:0% you here now this is a very very low 00:11:15.110 --> 00:11:17.350 align:start position:0% you here now this is a very very low level<00:11:15.350> interface<00:11:15.639> but<00:11:16.639> I've<00:11:16.759> loaded<00:11:16.939> into<00:11:17.239> a 00:11:17.350 --> 00:11:17.360 align:start position:0% level interface but I've loaded into a 00:11:17.360 --> 00:11:19.449 align:start position:0% level interface but I've loaded into a mantra<00:11:17.809> the<00:11:18.110> model<00:11:18.499> of<00:11:18.589> the<00:11:18.709> etherium<00:11:19.129> virtual 00:11:19.449 --> 00:11:19.459 align:start position:0% mantra the model of the etherium virtual 00:11:19.459 --> 00:11:21.460 align:start position:0% mantra the model of the etherium virtual machine<00:11:19.790> I've<00:11:20.029> also<00:11:20.629> loaded<00:11:21.139> in<00:11:21.259> some 00:11:21.460 --> 00:11:21.470 align:start position:0% machine I've also loaded in some 00:11:21.470 --> 00:11:24.069 align:start position:0% machine I've also loaded in some bytecode<00:11:21.939> those<00:11:22.939> are<00:11:23.089> now<00:11:23.209> in<00:11:23.480> the<00:11:23.660> runtime 00:11:24.069 --> 00:11:24.079 align:start position:0% bytecode those are now in the runtime 00:11:24.079 --> 00:11:26.739 align:start position:0% bytecode those are now in the runtime those<00:11:24.470> of<00:11:24.619> you<00:11:24.709> who<00:11:24.739> know<00:11:25.040> o<00:11:25.279> camel<00:11:26.029> will<00:11:26.569> see 00:11:26.739 --> 00:11:26.749 align:start position:0% those of you who know o camel will see 00:11:26.749 --> 00:11:28.359 align:start position:0% those of you who know o camel will see that<00:11:26.899> this<00:11:27.049> looks<00:11:27.529> just<00:11:27.769> like<00:11:27.919> you're<00:11:28.100> at<00:11:28.160> a<00:11:28.189> no 00:11:28.359 --> 00:11:28.369 align:start position:0% that this looks just like you're at a no 00:11:28.369 --> 00:11:31.449 align:start position:0% that this looks just like you're at a no camel<00:11:28.939> top-level<00:11:29.419> read<00:11:29.839> eval<00:11:29.929> print<00:11:30.049> loop<00:11:30.459> but 00:11:31.449 --> 00:11:31.459 align:start position:0% camel top-level read eval print loop but 00:11:31.459 --> 00:11:32.979 align:start position:0% camel top-level read eval print loop but actually<00:11:31.790> everything<00:11:32.299> you<00:11:32.389> write<00:11:32.600> in<00:11:32.869> this 00:11:32.979 --> 00:11:32.989 align:start position:0% actually everything you write in this 00:11:32.989 --> 00:11:34.720 align:start position:0% actually everything you write in this language<00:11:33.379> is<00:11:33.529> also<00:11:34.100> reflected<00:11:34.339> into 00:11:34.720 --> 00:11:34.730 align:start position:0% language is also reflected into 00:11:34.730 --> 00:11:36.909 align:start position:0% language is also reflected into mathematics<00:11:35.629> and<00:11:35.899> you<00:11:36.350> can<00:11:36.499> then<00:11:36.619> reason 00:11:36.909 --> 00:11:36.919 align:start position:0% mathematics and you can then reason 00:11:36.919 --> 00:11:39.909 align:start position:0% mathematics and you can then reason about<00:11:37.069> it<00:11:37.249> so<00:11:38.059> I'm<00:11:38.269> now<00:11:38.449> asking<00:11:38.779> a<00:11:39.410> mantra<00:11:39.739> here 00:11:39.909 --> 00:11:39.919 align:start position:0% about it so I'm now asking a mantra here 00:11:39.919 --> 00:11:42.989 align:start position:0% about it so I'm now asking a mantra here to<00:11:40.519> decompose<00:11:41.119> the<00:11:41.419> state<00:11:41.689> space<00:11:41.899> of 00:11:42.989 --> 00:11:42.999 align:start position:0% to decompose the state space of 00:11:42.999 --> 00:11:45.150 align:start position:0% to decompose the state space of effectively<00:11:43.999> the<00:11:44.329> virtual<00:11:44.720> machine 00:11:45.150 --> 00:11:45.160 align:start position:0% effectively the virtual machine 00:11:45.160 --> 00:11:47.229 align:start position:0% effectively the virtual machine interpreter<00:11:46.160> running<00:11:46.549> that<00:11:46.699> piece<00:11:46.910> of<00:11:46.939> byte 00:11:47.229 --> 00:11:47.239 align:start position:0% interpreter running that piece of byte 00:11:47.239 --> 00:11:49.479 align:start position:0% interpreter running that piece of byte code<00:11:47.449> and<00:11:47.749> what's<00:11:48.379> this<00:11:48.529> what<00:11:48.949> this<00:11:49.069> is<00:11:49.279> doing 00:11:49.479 --> 00:11:49.489 align:start position:0% code and what's this what this is doing 00:11:49.489 --> 00:11:51.220 align:start position:0% code and what's this what this is doing it's<00:11:49.819> ultimately<00:11:50.419> using<00:11:50.839> something<00:11:51.049> called 00:11:51.220 --> 00:11:51.230 align:start position:0% it's ultimately using something called 00:11:51.230 --> 00:11:53.559 align:start position:0% it's ultimately using something called symbolic<00:11:51.739> execution<00:11:51.860> under<00:11:52.610> the<00:11:52.699> hood<00:11:52.850> but 00:11:53.559 --> 00:11:53.569 align:start position:0% symbolic execution under the hood but 00:11:53.569 --> 00:11:55.030 align:start position:0% symbolic execution under the hood but it's<00:11:53.720> telling<00:11:54.079> me<00:11:54.199> the<00:11:54.319> possible<00:11:54.889> behaviors 00:11:55.030 --> 00:11:55.040 align:start position:0% it's telling me the possible behaviors 00:11:55.040 --> 00:11:57.340 align:start position:0% it's telling me the possible behaviors of<00:11:55.639> this<00:11:55.790> piece<00:11:55.970> of<00:11:56.119> bytecode<00:11:56.509> with<00:11:56.839> respect 00:11:57.340 --> 00:11:57.350 align:start position:0% of this piece of bytecode with respect 00:11:57.350 --> 00:11:58.780 align:start position:0% of this piece of bytecode with respect to<00:11:57.499> the<00:11:57.619> actual<00:11:58.009> semantics<00:11:58.610> of<00:11:58.730> the 00:11:58.780 --> 00:11:58.790 align:start position:0% to the actual semantics of the 00:11:58.790 --> 00:12:01.059 align:start position:0% to the actual semantics of the instructions<00:11:59.329> so<00:12:00.110> this<00:12:00.290> tells<00:12:00.529> me<00:12:00.769> that 00:12:01.059 --> 00:12:01.069 align:start position:0% instructions so this tells me that 00:12:01.069 --> 00:12:02.499 align:start position:0% instructions so this tells me that actually<00:12:01.249> this<00:12:01.549> piece<00:12:01.759> of<00:12:01.910> byte<00:12:02.059> code<00:12:02.299> which 00:12:02.499 --> 00:12:02.509 align:start position:0% actually this piece of byte code which 00:12:02.509 --> 00:12:04.840 align:start position:0% actually this piece of byte code which is<00:12:02.660> for<00:12:02.869> a<00:12:02.899> simple<00:12:03.439> name<00:12:03.589> registry<00:12:04.129> it<00:12:04.610> only 00:12:04.840 --> 00:12:04.850 align:start position:0% is for a simple name registry it only 00:12:04.850 --> 00:12:07.449 align:start position:0% is for a simple name registry it only has<00:12:05.089> two<00:12:05.419> possible<00:12:05.660> behaviors<00:12:06.230> with<00:12:07.100> respect 00:12:07.449 --> 00:12:07.459 align:start position:0% has two possible behaviors with respect 00:12:07.459 --> 00:12:10.029 align:start position:0% has two possible behaviors with respect to<00:12:07.549> arbitrary<00:12:08.119> symbolic<00:12:08.689> storage<00:12:09.079> and<00:12:09.319> one 00:12:10.029 --> 00:12:10.039 align:start position:0% to arbitrary symbolic storage and one 00:12:10.039 --> 00:12:12.579 align:start position:0% to arbitrary symbolic storage and one behavior<00:12:10.549> it<00:12:10.759> would<00:12:10.910> go<00:12:11.059> tour<00:12:11.439> execute<00:12:12.439> at 00:12:12.579 --> 00:12:12.589 align:start position:0% behavior it would go tour execute at 00:12:12.589 --> 00:12:13.049 align:start position:0% behavior it would go tour execute at program 00:12:13.049 --> 00:12:13.059 align:start position:0% program 00:12:13.059 --> 00:12:15.199 align:start position:0% program counter<00:12:13.269> 17<00:12:13.749> if<00:12:14.049> it<00:12:14.169> doesn't<00:12:14.559> run<00:12:14.619> out<00:12:14.739> of<00:12:14.799> gas 00:12:15.199 --> 00:12:15.209 align:start position:0% counter 17 if it doesn't run out of gas 00:12:15.209 --> 00:12:17.849 align:start position:0% counter 17 if it doesn't run out of gas and<00:12:16.209> it<00:12:16.569> would<00:12:16.659> update<00:12:16.839> the<00:12:17.109> storage<00:12:17.469> in<00:12:17.739> the 00:12:17.849 --> 00:12:17.859 align:start position:0% and it would update the storage in the 00:12:17.859 --> 00:12:20.999 align:start position:0% and it would update the storage in the other<00:12:18.039> behavior<00:12:18.779> it's<00:12:19.779> I<00:12:20.109> believe<00:12:20.649> would<00:12:20.799> halt 00:12:20.999 --> 00:12:21.009 align:start position:0% other behavior it's I believe would halt 00:12:21.009 --> 00:12:23.359 align:start position:0% other behavior it's I believe would halt you<00:12:21.369> just<00:12:21.639> told<00:12:21.789> me<00:12:21.879> it<00:12:22.329> would<00:12:22.479> halt<00:12:22.659> at<00:12:22.809> eight 00:12:23.359 --> 00:12:23.369 align:start position:0% you just told me it would halt at eight 00:12:23.369 --> 00:12:26.129 align:start position:0% you just told me it would halt at eight and<00:12:24.369> would<00:12:25.059> not<00:12:25.149> update<00:12:25.479> the<00:12:25.629> storage<00:12:25.959> for 00:12:26.129 --> 00:12:26.139 align:start position:0% and would not update the storage for 00:12:26.139 --> 00:12:29.849 align:start position:0% and would not update the storage for instance<00:12:26.439> so<00:12:27.339> now<00:12:27.579> I'm<00:12:27.999> actually<00:12:28.629> let<00:12:29.589> me<00:12:29.679> see 00:12:29.849 --> 00:12:29.859 align:start position:0% instance so now I'm actually let me see 00:12:29.859 --> 00:12:31.439 align:start position:0% instance so now I'm actually let me see if<00:12:29.949> I<00:12:30.009> could<00:12:30.069> pause<00:12:30.339> this<00:12:30.519> for<00:12:30.759> a<00:12:30.789> second<00:12:31.179> and 00:12:31.439 --> 00:12:31.449 align:start position:0% if I could pause this for a second and 00:12:31.449 --> 00:12:33.389 align:start position:0% if I could pause this for a second and we<00:12:31.539> have<00:12:31.689> two<00:12:31.899> minutes<00:12:32.199> you<00:12:32.859> can't<00:12:33.069> read<00:12:33.249> it 00:12:33.389 --> 00:12:33.399 align:start position:0% we have two minutes you can't read it 00:12:33.399 --> 00:12:35.159 align:start position:0% we have two minutes you can't read it unfortunately<00:12:34.119> but<00:12:34.419> these<00:12:34.629> are<00:12:34.779> theorem 00:12:35.159 --> 00:12:35.169 align:start position:0% unfortunately but these are theorem 00:12:35.169 --> 00:12:37.319 align:start position:0% unfortunately but these are theorem statements<00:12:35.679> about<00:12:36.279> the<00:12:36.339> execution<00:12:37.149> of<00:12:37.209> this 00:12:37.319 --> 00:12:37.329 align:start position:0% statements about the execution of this 00:12:37.329 --> 00:12:39.449 align:start position:0% statements about the execution of this bytecode<00:12:37.599> so<00:12:38.349> these<00:12:38.499> are<00:12:38.649> the<00:12:38.679> formal<00:12:39.129> specs 00:12:39.449 --> 00:12:39.459 align:start position:0% bytecode so these are the formal specs 00:12:39.459 --> 00:12:41.099 align:start position:0% bytecode so these are the formal specs of<00:12:39.699> how<00:12:39.879> this<00:12:40.059> name<00:12:40.299> registry<00:12:40.719> should<00:12:40.929> work 00:12:41.099 --> 00:12:41.109 align:start position:0% of how this name registry should work 00:12:41.109 --> 00:12:43.199 align:start position:0% of how this name registry should work and<00:12:41.379> we're<00:12:41.949> asking<00:12:42.279> a<00:12:42.369> mantra<00:12:42.669> to<00:12:42.789> prove<00:12:43.029> those 00:12:43.199 --> 00:12:43.209 align:start position:0% and we're asking a mantra to prove those 00:12:43.209 --> 00:12:45.649 align:start position:0% and we're asking a mantra to prove those for<00:12:43.509> us<00:12:43.659> and<00:12:43.869> it<00:12:44.139> does<00:12:44.379> which<00:12:45.129> is<00:12:45.309> great 00:12:45.649 --> 00:12:45.659 align:start position:0% for us and it does which is great 00:12:45.659 --> 00:12:47.819 align:start position:0% for us and it does which is great directly<00:12:46.659> about<00:12:46.899> the<00:12:47.229> meaning<00:12:47.499> of<00:12:47.679> the 00:12:47.819 --> 00:12:47.829 align:start position:0% directly about the meaning of the 00:12:47.829 --> 00:12:49.619 align:start position:0% directly about the meaning of the bytecode<00:12:48.009> so<00:12:48.429> not<00:12:48.579> at<00:12:48.729> a<00:12:48.789> higher<00:12:48.939> level<00:12:48.969> but 00:12:49.619 --> 00:12:49.629 align:start position:0% bytecode so not at a higher level but 00:12:49.629 --> 00:12:51.119 align:start position:0% bytecode so not at a higher level but really<00:12:49.929> at<00:12:50.049> the<00:12:50.139> actual<00:12:50.439> byte<00:12:50.679> code<00:12:50.859> that<00:12:51.009> will 00:12:51.119 --> 00:12:51.129 align:start position:0% really at the actual byte code that will 00:12:51.129 --> 00:12:53.939 align:start position:0% really at the actual byte code that will be<00:12:51.399> executed<00:12:51.519> on<00:12:52.059> the<00:12:52.089> EVM<00:12:52.629> and<00:12:52.959> now<00:12:53.739> we're 00:12:53.939 --> 00:12:53.949 align:start position:0% be executed on the EVM and now we're 00:12:53.949 --> 00:12:56.039 align:start position:0% be executed on the EVM and now we're asking<00:12:54.279> it<00:12:54.369> to<00:12:54.429> prove<00:12:54.669> some<00:12:54.879> things<00:12:55.089> that<00:12:55.869> have 00:12:56.039 --> 00:12:56.049 align:start position:0% asking it to prove some things that have 00:12:56.049 --> 00:12:58.469 align:start position:0% asking it to prove some things that have mistakes<00:12:56.469> and<00:12:56.739> what<00:12:57.459> happens<00:12:57.819> is<00:12:57.999> in<00:12:58.239> this 00:12:58.469 --> 00:12:58.479 align:start position:0% mistakes and what happens is in this 00:12:58.479 --> 00:13:00.899 align:start position:0% mistakes and what happens is in this case<00:12:58.719> we<00:12:59.589> can<00:12:59.739> ask<00:12:59.859> him<00:12:59.979> andhra<00:13:00.279> to<00:13:00.459> show<00:13:00.699> us 00:13:00.899 --> 00:13:00.909 align:start position:0% case we can ask him andhra to show us 00:13:00.909 --> 00:13:03.209 align:start position:0% case we can ask him andhra to show us where<00:13:01.389> it's<00:13:01.569> proof<00:13:01.839> attempt<00:13:02.199> failed<00:13:02.529> and<00:13:02.859> then 00:13:03.209 --> 00:13:03.219 align:start position:0% where it's proof attempt failed and then 00:13:03.219 --> 00:13:04.799 align:start position:0% where it's proof attempt failed and then we<00:13:03.309> can<00:13:03.459> ask<00:13:03.609> a<00:13:03.699> mantra<00:13:03.969> to<00:13:04.089> also<00:13:04.329> mine<00:13:04.569> that 00:13:04.799 --> 00:13:04.809 align:start position:0% we can ask a mantra to also mine that 00:13:04.809 --> 00:13:06.869 align:start position:0% we can ask a mantra to also mine that for<00:13:05.049> counter<00:13:05.469> examples<00:13:05.889> but<00:13:06.459> these<00:13:06.549> are<00:13:06.699> very 00:13:06.869 --> 00:13:06.879 align:start position:0% for counter examples but these are very 00:13:06.879 --> 00:13:08.729 align:start position:0% for counter examples but these are very useful<00:13:07.089> for<00:13:07.329> understanding<00:13:07.659> these<00:13:08.379> what<00:13:08.649> we 00:13:08.729 --> 00:13:08.739 align:start position:0% useful for understanding these what we 00:13:08.739 --> 00:13:10.709 align:start position:0% useful for understanding these what we call<00:13:08.769> sub<00:13:09.189> goals<00:13:09.339> for<00:13:09.939> understanding<00:13:10.539> why 00:13:10.709 --> 00:13:10.719 align:start position:0% call sub goals for understanding why 00:13:10.719 --> 00:13:13.859 align:start position:0% call sub goals for understanding why something<00:13:11.319> isn't<00:13:11.439> true<00:13:11.739> so<00:13:11.979> I<00:13:12.909> don't<00:13:13.749> have 00:13:13.859 --> 00:13:13.869 align:start position:0% something isn't true so I don't have 00:13:13.869 --> 00:13:15.869 align:start position:0% something isn't true so I don't have time<00:13:14.049> to<00:13:14.199> go<00:13:14.229> through<00:13:14.349> this<00:13:14.649> this<00:13:15.369> is<00:13:15.549> a<00:13:15.579> higher 00:13:15.869 --> 00:13:15.879 align:start position:0% time to go through this this is a higher 00:13:15.879 --> 00:13:19.799 align:start position:0% time to go through this this is a higher level<00:13:16.359> so<00:13:16.899> we<00:13:17.409> have<00:13:17.589> a<00:13:18.369> higher<00:13:19.059> level<00:13:19.449> language 00:13:19.799 --> 00:13:19.809 align:start position:0% level so we have a higher level language 00:13:19.809 --> 00:13:22.679 align:start position:0% level so we have a higher level language that<00:13:20.439> is<00:13:20.559> a<00:13:20.589> subset<00:13:21.129> of<00:13:21.369> Madra<00:13:22.089> subset<00:13:22.509> of<00:13:22.539> o 00:13:22.679 --> 00:13:22.689 align:start position:0% that is a subset of Madra subset of o 00:13:22.689 --> 00:13:25.499 align:start position:0% that is a subset of Madra subset of o camel<00:13:23.049> that<00:13:23.679> we<00:13:23.949> can<00:13:24.099> compile<00:13:24.489> to<00:13:24.789> the<00:13:24.879> EVM<00:13:25.299> and 00:13:25.499 --> 00:13:25.509 align:start position:0% camel that we can compile to the EVM and 00:13:25.509 --> 00:13:27.029 align:start position:0% camel that we can compile to the EVM and so<00:13:25.869> one<00:13:26.019> of<00:13:26.049> the<00:13:26.169> things<00:13:26.199> we're<00:13:26.499> working<00:13:26.529> on<00:13:26.919> is 00:13:27.029 --> 00:13:27.039 align:start position:0% so one of the things we're working on is 00:13:27.039 --> 00:13:28.769 align:start position:0% so one of the things we're working on is proving<00:13:27.399> the<00:13:27.489> correctness<00:13:27.879> of<00:13:27.939> that<00:13:28.239> compiler 00:13:28.769 --> 00:13:28.779 align:start position:0% proving the correctness of that compiler 00:13:28.779 --> 00:13:31.229 align:start position:0% proving the correctness of that compiler with<00:13:29.229> respect<00:13:29.739> to<00:13:29.889> the<00:13:30.009> EVM<00:13:30.369> semantics<00:13:30.879> so 00:13:31.229 --> 00:13:31.239 align:start position:0% with respect to the EVM semantics so 00:13:31.239 --> 00:13:32.459 align:start position:0% with respect to the EVM semantics so hopefully<00:13:31.599> we'll<00:13:31.749> finish<00:13:31.929> that<00:13:32.169> by<00:13:32.319> the<00:13:32.379> end 00:13:32.459 --> 00:13:32.469 align:start position:0% hopefully we'll finish that by the end 00:13:32.469 --> 00:13:35.269 align:start position:0% hopefully we'll finish that by the end of<00:13:32.619> the<00:13:32.739> year<00:13:33.239> but<00:13:34.239> I<00:13:34.449> wanted<00:13:34.719> to<00:13:34.779> show<00:13:34.869> you 00:13:35.269 --> 00:13:35.279 align:start position:0% of the year but I wanted to show you 00:13:35.279 --> 00:13:38.009 align:start position:0% of the year but I wanted to show you these<00:13:36.279> region<00:13:36.759> decompositions<00:13:37.479> like<00:13:37.719> I<00:13:37.869> did 00:13:38.009 --> 00:13:38.019 align:start position:0% these region decompositions like I did 00:13:38.019 --> 00:13:39.749 align:start position:0% these region decompositions like I did of<00:13:38.139> the<00:13:38.289> possible<00:13:38.859> behaviors<00:13:39.009> of<00:13:39.459> that<00:13:39.579> piece 00:13:39.749 --> 00:13:39.759 align:start position:0% of the possible behaviors of that piece 00:13:39.759 --> 00:13:42.929 align:start position:0% of the possible behaviors of that piece of<00:13:39.789> by<00:13:39.999> code<00:13:40.349> we<00:13:41.349> can<00:13:41.769> scale<00:13:42.009> this<00:13:42.249> to<00:13:42.549> you<00:13:42.849> know 00:13:42.929 --> 00:13:42.939 align:start position:0% of by code we can scale this to you know 00:13:42.939 --> 00:13:46.289 align:start position:0% of by code we can scale this to you know very<00:13:43.149> complex<00:13:43.539> algorithms<00:13:44.079> so<00:13:44.739> this<00:13:45.039> is<00:13:45.299> smart 00:13:46.289 --> 00:13:46.299 align:start position:0% very complex algorithms so this is smart 00:13:46.299 --> 00:13:49.229 align:start position:0% very complex algorithms so this is smart contract<00:13:46.869> encoding<00:13:48.089> effectively<00:13:49.089> the 00:13:49.229 --> 00:13:49.239 align:start position:0% contract encoding effectively the 00:13:49.239 --> 00:13:51.509 align:start position:0% contract encoding effectively the matching<00:13:49.659> logic<00:13:50.079> pricing<00:13:50.679> function<00:13:51.099> for<00:13:51.429> an 00:13:51.509 --> 00:13:51.519 align:start position:0% matching logic pricing function for an 00:13:51.519 --> 00:13:53.579 align:start position:0% matching logic pricing function for an exchange<00:13:51.759> and<00:13:52.299> we<00:13:52.809> asked<00:13:52.989> Timandra<00:13:53.409> to 00:13:53.579 --> 00:13:53.589 align:start position:0% exchange and we asked Timandra to 00:13:53.589 --> 00:13:55.709 align:start position:0% exchange and we asked Timandra to decompose<00:13:54.129> it<00:13:54.369> state<00:13:54.639> space<00:13:54.939> it<00:13:55.299> told<00:13:55.569> us 00:13:55.709 --> 00:13:55.719 align:start position:0% decompose it state space it told us 00:13:55.719 --> 00:13:58.019 align:start position:0% decompose it state space it told us there's<00:13:55.959> actually<00:13:56.289> only<00:13:56.669> 107<00:13:57.669> different 00:13:58.019 --> 00:13:58.029 align:start position:0% there's actually only 107 different 00:13:58.029 --> 00:14:00.419 align:start position:0% there's actually only 107 different possible<00:13:58.419> behaviors<00:13:58.569> and<00:13:59.079> now<00:13:59.739> I<00:13:59.769> can<00:14:00.249> go 00:14:00.419 --> 00:14:00.429 align:start position:0% possible behaviors and now I can go 00:14:00.429 --> 00:14:02.159 align:start position:0% possible behaviors and now I can go through<00:14:00.729> and<00:14:00.759> we<00:14:01.059> have<00:14:01.509> this<00:14:01.659> hierarchical 00:14:02.159 --> 00:14:02.169 align:start position:0% through and we have this hierarchical 00:14:02.169 --> 00:14:04.529 align:start position:0% through and we have this hierarchical tree<00:14:02.499> representation<00:14:02.979> as<00:14:03.489> a<00:14:03.549> Peroni<00:14:03.999> diagram 00:14:04.529 --> 00:14:04.539 align:start position:0% tree representation as a Peroni diagram 00:14:04.539 --> 00:14:06.419 align:start position:0% tree representation as a Peroni diagram that's<00:14:04.779> interactive<00:14:05.289> you<00:14:05.829> can<00:14:05.979> go<00:14:06.129> and 00:14:06.419 --> 00:14:06.429 align:start position:0% that's interactive you can go and 00:14:06.429 --> 00:14:08.549 align:start position:0% that's interactive you can go and experiment<00:14:07.269> and<00:14:07.389> see<00:14:07.959> what<00:14:08.349> are<00:14:08.439> the 00:14:08.549 --> 00:14:08.559 align:start position:0% experiment and see what are the 00:14:08.559 --> 00:14:10.709 align:start position:0% experiment and see what are the different<00:14:08.949> symbolic<00:14:09.429> behaviors<00:14:09.939> of<00:14:10.149> this 00:14:10.709 --> 00:14:10.719 align:start position:0% different symbolic behaviors of this 00:14:10.719 --> 00:14:12.869 align:start position:0% different symbolic behaviors of this function<00:14:11.049> with<00:14:11.589> a<00:14:11.619> map<00:14:11.949> to<00:14:11.979> its<00:14:12.369> state<00:14:12.579> space 00:14:12.869 --> 00:14:12.879 align:start position:0% function with a map to its state space 00:14:12.879 --> 00:14:14.879 align:start position:0% function with a map to its state space and<00:14:13.119> we're<00:14:13.749> getting<00:14:14.019> on<00:14:14.139> the<00:14:14.229> right<00:14:14.409> you<00:14:14.679> can't 00:14:14.879 --> 00:14:14.889 align:start position:0% and we're getting on the right you can't 00:14:14.889 --> 00:14:16.799 align:start position:0% and we're getting on the right you can't read<00:14:15.279> them<00:14:15.429> unfortunately<00:14:15.759> but<00:14:16.059> constraints 00:14:16.799 --> 00:14:16.809 align:start position:0% read them unfortunately but constraints 00:14:16.809 --> 00:14:19.619 align:start position:0% read them unfortunately but constraints on<00:14:16.989> the<00:14:17.649> input<00:14:17.829> that<00:14:18.459> would<00:14:18.579> cause<00:14:18.819> a<00:14:19.209> certain 00:14:19.619 --> 00:14:19.629 align:start position:0% on the input that would cause a certain 00:14:19.629 --> 00:14:21.599 align:start position:0% on the input that would cause a certain output<00:14:19.809> and<00:14:20.739> these<00:14:20.889> are<00:14:21.009> all<00:14:21.129> expressed 00:14:21.599 --> 00:14:21.609 align:start position:0% output and these are all expressed 00:14:21.609 --> 00:14:23.369 align:start position:0% output and these are all expressed symbolically<00:14:22.089> and<00:14:22.299> so<00:14:22.599> now<00:14:22.720> we<00:14:22.779> know<00:14:22.899> even 00:14:23.369 --> 00:14:23.379 align:start position:0% symbolically and so now we know even 00:14:23.379 --> 00:14:25.269 align:start position:0% symbolically and so now we know even though<00:14:23.470> this<00:14:23.589> has<00:14:23.769> an<00:14:23.979> infinite<00:14:24.489> state<00:14:24.819> space 00:14:25.269 --> 00:14:25.279 align:start position:0% though this has an infinite state space 00:14:25.279 --> 00:14:29.720 align:start position:0% though this has an infinite state space the<00:14:26.279> system<00:14:26.639> itself<00:14:27.019> only<00:14:28.019> has<00:14:28.410> 107<00:14:29.279> possible 00:14:29.720 --> 00:14:29.730 align:start position:0% the system itself only has 107 possible 00:14:29.730 --> 00:14:32.449 align:start position:0% the system itself only has 107 possible symbolic<00:14:30.149> behaviors<00:14:30.570> so<00:14:31.440> we<00:14:32.160> have<00:14:32.279> a<00:14:32.310> new 00:14:32.449 --> 00:14:32.459 align:start position:0% symbolic behaviors so we have a new 00:14:32.459 --> 00:14:34.220 align:start position:0% symbolic behaviors so we have a new website<00:14:32.610> that<00:14:33.029> launches<00:14:33.389> today<00:14:33.570> you<00:14:33.750> can<00:14:34.079> go 00:14:34.220 --> 00:14:34.230 align:start position:0% website that launches today you can go 00:14:34.230 --> 00:14:39.710 align:start position:0% website that launches today you can go to<00:14:34.290> its<00:14:35.089> wwm<00:14:36.089> Andre<00:14:36.420> I<00:14:36.720> and<00:14:37.220> it<00:14:38.220> is<00:14:38.540> if<00:14:39.540> you 00:14:39.710 --> 00:14:39.720 align:start position:0% to its wwm Andre I and it is if you 00:14:39.720 --> 00:14:41.329 align:start position:0% to its wwm Andre I and it is if you click<00:14:39.899> on<00:14:39.990> image<00:14:40.320> or<00:14:40.440> contracts<00:14:40.860> you<00:14:41.010> can<00:14:41.130> sign 00:14:41.329 --> 00:14:41.339 align:start position:0% click on image or contracts you can sign 00:14:41.339 --> 00:14:42.590 align:start position:0% click on image or contracts you can sign up<00:14:41.519> and<00:14:41.670> we're<00:14:41.820> adding<00:14:42.060> a<00:14:42.120> certain<00:14:42.389> number<00:14:42.480> of 00:14:42.590 --> 00:14:42.600 align:start position:0% up and we're adding a certain number of 00:14:42.600 --> 00:14:45.050 align:start position:0% up and we're adding a certain number of people<00:14:42.930> each<00:14:43.079> week<00:14:43.320> as<00:14:43.529> we<00:14:43.860> scale<00:14:44.100> up<00:14:44.160> but 00:14:45.050 --> 00:14:45.060 align:start position:0% people each week as we scale up but 00:14:45.060 --> 00:14:46.610 align:start position:0% people each week as we scale up but effectively<00:14:45.449> it's<00:14:45.660> a<00:14:45.779> mandra<00:14:46.110> now<00:14:46.260> in<00:14:46.470> the 00:14:46.610 --> 00:14:46.620 align:start position:0% effectively it's a mandra now in the 00:14:46.620 --> 00:14:48.889 align:start position:0% effectively it's a mandra now in the cloud<00:14:46.889> running<00:14:47.820> in<00:14:47.910> google<00:14:48.240> cloud<00:14:48.449> with 00:14:48.889 --> 00:14:48.899 align:start position:0% cloud running in google cloud with 00:14:48.899 --> 00:14:51.590 align:start position:0% cloud running in google cloud with something<00:14:49.230> called<00:14:49.350> codenvy<00:14:50.240> which<00:14:51.240> uses 00:14:51.590 --> 00:14:51.600 align:start position:0% something called codenvy which uses 00:14:51.600 --> 00:14:55.370 align:start position:0% something called codenvy which uses eclipse<00:14:51.959> che<00:14:52.320> and<00:14:53.180> number<00:14:54.180> of<00:14:54.240> things<00:14:54.449> to<00:14:55.079> spin 00:14:55.370 --> 00:14:55.380 align:start position:0% eclipse che and number of things to spin 00:14:55.380 --> 00:14:57.050 align:start position:0% eclipse che and number of things to spin up<00:14:55.410> docker<00:14:55.680> containers<00:14:56.250> for<00:14:56.399> you<00:14:56.579> and<00:14:56.820> have<00:14:57.000> a 00:14:57.050 --> 00:14:57.060 align:start position:0% up docker containers for you and have a 00:14:57.060 --> 00:14:59.660 align:start position:0% up docker containers for you and have a mantra<00:14:57.449> so<00:14:57.899> I<00:14:57.930> see<00:14:58.139> I'm<00:14:58.260> out<00:14:58.470> of<00:14:58.500> time<00:14:58.800> but 00:14:59.660 --> 00:14:59.670 align:start position:0% mantra so I see I'm out of time but 00:14:59.670 --> 00:15:02.569 align:start position:0% mantra so I see I'm out of time but anyways<00:15:00.570> we<00:15:00.810> are<00:15:00.930> building<00:15:01.320> the<00:15:01.589> stack<00:15:01.920> also 00:15:02.569 --> 00:15:02.579 align:start position:0% anyways we are building the stack also 00:15:02.579 --> 00:15:05.889 align:start position:0% anyways we are building the stack also with<00:15:02.699> a<00:15:02.730> smart<00:15:03.060> contract<00:15:03.480> auditing<00:15:03.899> API<00:15:04.519> and 00:15:05.889 --> 00:15:05.899 align:start position:0% with a smart contract auditing API and 00:15:05.899 --> 00:15:08.300 align:start position:0% with a smart contract auditing API and finally<00:15:06.899> thanks<00:15:07.290> to<00:15:07.320> our<00:15:07.529> incredible<00:15:08.040> team 00:15:08.300 --> 00:15:08.310 align:start position:0% finally thanks to our incredible team 00:15:08.310 --> 00:15:10.370 align:start position:0% finally thanks to our incredible team and<00:15:08.610> I<00:15:08.730> hope<00:15:08.880> all<00:15:09.000> of<00:15:09.060> you<00:15:09.269> will<00:15:09.510> get<00:15:09.899> involved 00:15:10.370 --> 00:15:10.380 align:start position:0% and I hope all of you will get involved 00:15:10.380 --> 00:15:12.590 align:start position:0% and I hope all of you will get involved and<00:15:10.680> the<00:15:11.220> community<00:15:11.639> can<00:15:11.820> can<00:15:12.240> really<00:15:12.449> make 00:15:12.590 --> 00:15:12.600 align:start position:0% and the community can can really make 00:15:12.600 --> 00:15:15.350 align:start position:0% and the community can can really make use<00:15:12.750> of<00:15:12.810> the<00:15:12.990> mantra<00:15:13.350> and<00:15:14.279> join<00:15:14.850> us<00:15:15.029> at<00:15:15.269> a 00:15:15.350 --> 00:15:15.360 align:start position:0% use of the mantra and join us at a 00:15:15.360 --> 00:15:26.449 align:start position:0% use of the mantra and join us at a Monterey<00:15:15.630> I<00:15:16.010> thank<00:15:17.010> you<00:15:17.100> thank<00:15:17.610> you<00:15:22.670> now<00:15:23.670> Oh