WEBVTT
Kind: captions
Language: en

00:00:04.609 --> 00:00:08.270 align:start position:0%
 
hi<00:00:05.609><c> my</c><00:00:06.390><c> name</c><00:00:06.540><c> is</c><00:00:06.599><c> Lee</c><00:00:06.750><c> Joon</c><00:00:06.930><c> Park</c><00:00:07.319><c> I'm</c><00:00:07.589><c> going</c><00:00:08.189><c> to</c>

00:00:08.270 --> 00:00:08.280 align:start position:0%
hi my name is Lee Joon Park I'm going to
 

00:00:08.280 --> 00:00:12.890 align:start position:0%
hi my name is Lee Joon Park I'm going to
talk<00:00:08.460><c> about</c><00:00:08.610><c> the</c><00:00:09.209><c> K</c><00:00:09.510><c> beacon</c><00:00:10.200><c> chain</c><00:00:10.760><c> so</c><00:00:11.760><c> so</c><00:00:12.629><c> far</c>

00:00:12.890 --> 00:00:12.900 align:start position:0%
talk about the K beacon chain so so far
 

00:00:12.900 --> 00:00:15.709 align:start position:0%
talk about the K beacon chain so so far
people<00:00:13.500><c> were</c><00:00:13.980><c> talking</c><00:00:14.250><c> about</c><00:00:14.490><c> how</c><00:00:14.969><c> to</c><00:00:15.029><c> and</c>

00:00:15.709 --> 00:00:15.719 align:start position:0%
people were talking about how to and
 

00:00:15.719 --> 00:00:19.730 align:start position:0%
people were talking about how to and
what<00:00:16.439><c> they</c><00:00:16.770><c> implement</c><00:00:17.900><c> the</c><00:00:18.900><c> clients</c><00:00:19.470><c> and</c>

00:00:19.730 --> 00:00:19.740 align:start position:0%
what they implement the clients and
 

00:00:19.740 --> 00:00:23.749 align:start position:0%
what they implement the clients and
network<00:00:21.410><c> but</c><00:00:22.410><c> now</c><00:00:22.919><c> I'm</c><00:00:23.220><c> going</c><00:00:23.460><c> to</c><00:00:23.519><c> talk</c><00:00:23.669><c> about</c>

00:00:23.749 --> 00:00:23.759 align:start position:0%
network but now I'm going to talk about
 

00:00:23.759 --> 00:00:25.189 align:start position:0%
network but now I'm going to talk about
a<00:00:23.849><c> little</c><00:00:24.060><c> bit</c><00:00:24.150><c> different</c><00:00:24.570><c> which</c><00:00:24.779><c> is</c><00:00:24.810><c> about</c>

00:00:25.189 --> 00:00:25.199 align:start position:0%
a little bit different which is about
 

00:00:25.199 --> 00:00:28.179 align:start position:0%
a little bit different which is about
how<00:00:25.470><c> to</c><00:00:25.529><c> formally</c><00:00:26.310><c> verify</c><00:00:26.820><c> the</c><00:00:27.390><c> beacon</c><00:00:27.689><c> chain</c>

00:00:28.179 --> 00:00:28.189 align:start position:0%
how to formally verify the beacon chain
 

00:00:28.189 --> 00:00:32.380 align:start position:0%
how to formally verify the beacon chain
especially<00:00:29.189><c> state</c><00:00:29.730><c> transition</c><00:00:30.300><c> function</c><00:00:30.739><c> so</c>

00:00:32.380 --> 00:00:32.390 align:start position:0%
especially state transition function so
 

00:00:32.390 --> 00:00:35.300 align:start position:0%
especially state transition function so
before<00:00:33.390><c> we</c><00:00:33.570><c> go</c><00:00:33.750><c> this</c><00:00:34.410><c> is</c><00:00:34.500><c> our</c><00:00:34.590><c> awesome</c><00:00:34.920><c> team</c>

00:00:35.300 --> 00:00:35.310 align:start position:0%
before we go this is our awesome team
 

00:00:35.310 --> 00:00:38.960 align:start position:0%
before we go this is our awesome team
that<00:00:36.000><c> this</c><00:00:36.180><c> project</c><00:00:36.690><c> we</c><00:00:37.500><c> all</c><00:00:37.770><c> at</c><00:00:38.130><c> Iran</c><00:00:38.790><c> time</c>

00:00:38.960 --> 00:00:38.970 align:start position:0%
that this project we all at Iran time
 

00:00:38.970 --> 00:00:41.900 align:start position:0%
that this project we all at Iran time
verification<00:00:39.570><c> do</c><00:00:40.440><c> form</c><00:00:40.740><c> a</c><00:00:40.800><c> verification</c><00:00:41.100><c> for</c>

00:00:41.900 --> 00:00:41.910 align:start position:0%
verification do form a verification for
 

00:00:41.910 --> 00:00:44.540 align:start position:0%
verification do form a verification for
any<00:00:42.090><c> safety</c><00:00:42.750><c> critical</c><00:00:42.960><c> systems</c><00:00:43.320><c> like</c><00:00:43.920><c> smart</c>

00:00:44.540 --> 00:00:44.550 align:start position:0%
any safety critical systems like smart
 

00:00:44.550 --> 00:00:48.350 align:start position:0%
any safety critical systems like smart
contract<00:00:45.110><c> consensus</c><00:00:46.110><c> algorithm</c><00:00:46.580><c> and</c><00:00:47.580><c> now</c><00:00:47.940><c> we</c>

00:00:48.350 --> 00:00:48.360 align:start position:0%
contract consensus algorithm and now we
 

00:00:48.360 --> 00:00:50.510 align:start position:0%
contract consensus algorithm and now we
are<00:00:48.570><c> really</c><00:00:48.750><c> excited</c><00:00:48.930><c> to</c><00:00:49.290><c> work</c><00:00:49.920><c> on</c><00:00:50.070><c> this</c><00:00:50.130><c> form</c>

00:00:50.510 --> 00:00:50.520 align:start position:0%
are really excited to work on this form
 

00:00:50.520 --> 00:00:52.600 align:start position:0%
are really excited to work on this form
verification<00:00:51.150><c> of</c><00:00:51.240><c> the</c><00:00:51.810><c> beacon</c><00:00:52.080><c> chain</c>

00:00:52.600 --> 00:00:52.610 align:start position:0%
verification of the beacon chain
 

00:00:52.610 --> 00:01:00.650 align:start position:0%
verification of the beacon chain
implementation<00:00:53.610><c> so</c><00:00:58.340><c> the</c><00:00:59.340><c> K</c><00:00:59.700><c> beacon</c><00:01:00.030><c> chain</c><00:01:00.270><c> is</c>

00:01:00.650 --> 00:01:00.660 align:start position:0%
implementation so the K beacon chain is
 

00:01:00.660 --> 00:01:05.960 align:start position:0%
implementation so the K beacon chain is
a<00:01:01.560><c> an</c><00:01:02.210><c> executable</c><00:01:03.470><c> formal</c><00:01:04.470><c> model</c><00:01:04.890><c> of</c><00:01:05.129><c> the</c>

00:01:05.960 --> 00:01:05.970 align:start position:0%
a an executable formal model of the
 

00:01:05.970 --> 00:01:08.060 align:start position:0%
a an executable formal model of the
beacon<00:01:06.299><c> chain</c><00:01:06.540><c> written</c><00:01:07.500><c> in</c><00:01:07.619><c> the</c><00:01:07.740><c> formal</c>

00:01:08.060 --> 00:01:08.070 align:start position:0%
beacon chain written in the formal
 

00:01:08.070 --> 00:01:12.320 align:start position:0%
beacon chain written in the formal
language<00:01:08.159><c> called</c><00:01:08.820><c> K</c><00:01:10.700><c> for</c><00:01:11.700><c> the</c><00:01:11.790><c> purpose</c><00:01:12.120><c> of</c>

00:01:12.320 --> 00:01:12.330 align:start position:0%
language called K for the purpose of
 

00:01:12.330 --> 00:01:14.990 align:start position:0%
language called K for the purpose of
verifying<00:01:12.960><c> the</c><00:01:13.680><c> important</c><00:01:14.190><c> properties</c><00:01:14.700><c> which</c>

00:01:14.990 --> 00:01:15.000 align:start position:0%
verifying the important properties which
 

00:01:15.000 --> 00:01:18.110 align:start position:0%
verifying the important properties which
has<00:01:15.360><c> called</c><00:01:15.659><c> this</c><00:01:16.460><c> accountable</c><00:01:17.460><c> safety</c><00:01:17.880><c> and</c>

00:01:18.110 --> 00:01:18.120 align:start position:0%
has called this accountable safety and
 

00:01:18.120 --> 00:01:19.550 align:start position:0%
has called this accountable safety and
plus<00:01:18.870><c> or</c><00:01:19.080><c> liveness</c>

00:01:19.550 --> 00:01:19.560 align:start position:0%
plus or liveness
 

00:01:19.560 --> 00:01:23.210 align:start position:0%
plus or liveness
of<00:01:19.740><c> the</c><00:01:20.370><c> beacon</c><00:01:20.700><c> chain</c><00:01:20.880><c> implementation</c><00:01:22.220><c> how</c>

00:01:23.210 --> 00:01:23.220 align:start position:0%
of the beacon chain implementation how
 

00:01:23.220 --> 00:01:27.219 align:start position:0%
of the beacon chain implementation how
many<00:01:23.400><c> those</c><00:01:23.940><c> of</c><00:01:24.090><c> you</c><00:01:24.240><c> know</c><00:01:24.450><c> the</c><00:01:24.659><c> K</c><00:01:24.900><c> language</c><00:01:25.770><c> oh</c>

00:01:27.219 --> 00:01:27.229 align:start position:0%
many those of you know the K language oh
 

00:01:27.229 --> 00:01:30.080 align:start position:0%
many those of you know the K language oh
okay<00:01:28.260><c> awesome</c><00:01:28.590><c> so</c><00:01:29.190><c> those</c><00:01:29.520><c> of</c><00:01:29.550><c> you</c><00:01:29.760><c> don't</c><00:01:29.970><c> know</c>

00:01:30.080 --> 00:01:30.090 align:start position:0%
okay awesome so those of you don't know
 

00:01:30.090 --> 00:01:34.690 align:start position:0%
okay awesome so those of you don't know
about<00:01:30.210><c> the</c><00:01:30.390><c> K</c><00:01:30.830><c> the</c><00:01:31.830><c> K</c><00:01:32.070><c> is</c><00:01:32.340><c> a</c><00:01:32.670><c> formal</c><00:01:33.380><c> language</c>

00:01:34.690 --> 00:01:34.700 align:start position:0%
about the K the K is a formal language
 

00:01:34.700 --> 00:01:39.100 align:start position:0%
about the K the K is a formal language
in<00:01:35.700><c> which</c><00:01:36.479><c> we</c><00:01:37.110><c> actually</c><00:01:37.590><c> specify</c><00:01:37.920><c> the</c><00:01:38.190><c> EDM</c>

00:01:39.100 --> 00:01:39.110 align:start position:0%
in which we actually specify the EDM
 

00:01:39.110 --> 00:01:43.039 align:start position:0%
in which we actually specify the EDM
semantics<00:01:40.110><c> called</c><00:01:40.680><c> ke</c><00:01:41.040><c> VM</c><00:01:41.520><c> which</c><00:01:41.820><c> we</c><00:01:42.360><c> use</c><00:01:42.630><c> to</c>

00:01:43.039 --> 00:01:43.049 align:start position:0%
semantics called ke VM which we use to
 

00:01:43.049 --> 00:01:46.130 align:start position:0%
semantics called ke VM which we use to
verify<00:01:43.190><c> many</c><00:01:44.190><c> high-profile</c><00:01:44.909><c> smart</c><00:01:45.630><c> contract</c>

00:01:46.130 --> 00:01:46.140 align:start position:0%
verify many high-profile smart contract
 

00:01:46.140 --> 00:01:50.500 align:start position:0%
verify many high-profile smart contract
using<00:01:46.350><c> that</c><00:01:46.650><c> KBM</c><00:01:48.110><c> specification</c><00:01:49.110><c> so</c>

00:01:50.500 --> 00:01:50.510 align:start position:0%
using that KBM specification so
 

00:01:50.510 --> 00:01:53.480 align:start position:0%
using that KBM specification so
including<00:01:51.510><c> the</c><00:01:51.690><c> recently</c><00:01:52.229><c> we</c><00:01:52.530><c> verified</c><00:01:53.190><c> the</c><00:01:53.460><c> e</c>

00:01:53.480 --> 00:01:53.490 align:start position:0%
including the recently we verified the e
 

00:01:53.490 --> 00:01:55.609 align:start position:0%
including the recently we verified the e
2.0<00:01:54.240><c> the</c><00:01:54.270><c> party</c><00:01:54.659><c> contract</c><00:01:55.080><c> as</c><00:01:55.170><c> well</c><00:01:55.380><c> using</c>

00:01:55.609 --> 00:01:55.619 align:start position:0%
2.0 the party contract as well using
 

00:01:55.619 --> 00:01:58.640 align:start position:0%
2.0 the party contract as well using
that<00:01:55.740><c> so</c><00:01:56.340><c> k</c><00:01:56.520><c> is</c><00:01:56.549><c> kind</c><00:01:56.909><c> of</c><00:01:57.119><c> really</c><00:01:57.690><c> like</c><00:01:57.720><c> formal</c>

00:01:58.640 --> 00:01:58.650 align:start position:0%
that so k is kind of really like formal
 

00:01:58.650 --> 00:02:02.780 align:start position:0%
that so k is kind of really like formal
language<00:01:59.010><c> you</c><00:01:59.460><c> can</c><00:01:59.670><c> use</c><00:02:00.049><c> any</c><00:02:01.049><c> formal</c><00:02:01.409><c> thing</c><00:02:02.369><c> in</c>

00:02:02.780 --> 00:02:02.790 align:start position:0%
language you can use any formal thing in
 

00:02:02.790 --> 00:02:06.410 align:start position:0%
language you can use any formal thing in
this<00:02:03.270><c> domain</c><00:02:03.979><c> so</c><00:02:04.979><c> let</c><00:02:05.580><c> me</c><00:02:05.640><c> go</c><00:02:05.760><c> to</c><00:02:05.790><c> some</c><00:02:06.270><c> big</c>

00:02:06.410 --> 00:02:06.420 align:start position:0%
this domain so let me go to some big
 

00:02:06.420 --> 00:02:09.979 align:start position:0%
this domain so let me go to some big
picture<00:02:06.810><c> about</c><00:02:07.110><c> what</c><00:02:07.799><c> we</c><00:02:08.640><c> where</c><00:02:09.330><c> we</c><00:02:09.360><c> are</c><00:02:09.689><c> and</c>

00:02:09.979 --> 00:02:09.989 align:start position:0%
picture about what we where we are and
 

00:02:09.989 --> 00:02:14.750 align:start position:0%
picture about what we where we are and
what<00:02:10.860><c> we</c><00:02:11.039><c> are</c><00:02:11.159><c> going</c><00:02:11.340><c> to</c><00:02:11.459><c> do</c><00:02:11.640><c> next</c><00:02:11.879><c> so</c><00:02:13.520><c> we</c><00:02:14.520><c> have</c>

00:02:14.750 --> 00:02:14.760 align:start position:0%
what we are going to do next so we have
 

00:02:14.760 --> 00:02:18.470 align:start position:0%
what we are going to do next so we have
the<00:02:15.720><c> K</c><00:02:16.349><c> Deacon</c><00:02:16.650><c> chain</c><00:02:16.890><c> is</c><00:02:17.190><c> a</c><00:02:17.250><c> formal</c><00:02:17.700><c> model</c>

00:02:18.470 --> 00:02:18.480 align:start position:0%
the K Deacon chain is a formal model
 

00:02:18.480 --> 00:02:23.440 align:start position:0%
the K Deacon chain is a formal model
which<00:02:19.280><c> actually</c><00:02:20.280><c> formalize</c><00:02:21.050><c> the</c><00:02:22.050><c> Python</c>

00:02:23.440 --> 00:02:23.450 align:start position:0%
which actually formalize the Python
 

00:02:23.450 --> 00:02:26.540 align:start position:0%
which actually formalize the Python
former<00:02:24.450><c> spec</c><00:02:24.810><c> of</c><00:02:24.989><c> the</c><00:02:25.080><c> beacon</c><00:02:25.349><c> chain</c><00:02:25.590><c> so</c><00:02:26.519><c> we</c>

00:02:26.540 --> 00:02:26.550 align:start position:0%
former spec of the beacon chain so we
 

00:02:26.550 --> 00:02:29.089 align:start position:0%
former spec of the beacon chain so we
faithfully<00:02:27.420><c> formalized</c><00:02:27.900><c> to</c><00:02:28.530><c> whatever</c><00:02:28.739><c> the</c>

00:02:29.089 --> 00:02:29.099 align:start position:0%
faithfully formalized to whatever the
 

00:02:29.099 --> 00:02:32.420 align:start position:0%
faithfully formalized to whatever the
the<00:02:29.790><c> pythons</c><00:02:30.209><c> back</c><00:02:30.480><c> into</c><00:02:31.019><c> our</c><00:02:31.410><c> K</c><00:02:32.010><c> formal</c>

00:02:32.420 --> 00:02:32.430 align:start position:0%
the pythons back into our K formal
 

00:02:32.430 --> 00:02:33.050 align:start position:0%
the pythons back into our K formal
language

00:02:33.050 --> 00:02:33.060 align:start position:0%
language
 

00:02:33.060 --> 00:02:35.720 align:start position:0%
language
and<00:02:33.150><c> that</c><00:02:34.110><c> we</c><00:02:34.230><c> have</c><00:02:34.379><c> a</c><00:02:34.410><c> de</c><00:02:34.560><c> formal</c><00:02:34.890><c> model</c><00:02:35.220><c> and</c>

00:02:35.720 --> 00:02:35.730 align:start position:0%
and that we have a de formal model and
 

00:02:35.730 --> 00:02:38.540 align:start position:0%
and that we have a de formal model and
as<00:02:36.630><c> I</c><00:02:36.720><c> said</c><00:02:37.050><c> the</c><00:02:37.440><c> the</c><00:02:37.830><c> one</c><00:02:37.980><c> of</c><00:02:38.010><c> the</c><00:02:38.160><c> benefit</c><00:02:38.519><c> of</c>

00:02:38.540 --> 00:02:38.550 align:start position:0%
as I said the the one of the benefit of
 

00:02:38.550 --> 00:02:41.150 align:start position:0%
as I said the the one of the benefit of
using<00:02:38.819><c> K</c><00:02:39.120><c> language</c><00:02:39.569><c> is</c><00:02:39.750><c> that</c><00:02:40.040><c> anything</c><00:02:41.040><c> is</c>

00:02:41.150 --> 00:02:41.160 align:start position:0%
using K language is that anything is
 

00:02:41.160 --> 00:02:43.580 align:start position:0%
using K language is that anything is
modeled<00:02:41.610><c> in</c><00:02:41.790><c> the</c><00:02:41.819><c> K</c><00:02:42.090><c> language</c><00:02:42.540><c> is</c><00:02:42.810><c> executable</c>

00:02:43.580 --> 00:02:43.590 align:start position:0%
modeled in the K language is executable
 

00:02:43.590 --> 00:02:45.830 align:start position:0%
modeled in the K language is executable
which<00:02:44.130><c> means</c><00:02:44.459><c> that</c><00:02:44.730><c> it's</c><00:02:44.880><c> not</c><00:02:44.940><c> just</c><00:02:45.209><c> more</c><00:02:45.690><c> than</c>

00:02:45.830 --> 00:02:45.840 align:start position:0%
which means that it's not just more than
 

00:02:45.840 --> 00:02:48.289 align:start position:0%
which means that it's not just more than
the<00:02:45.989><c> paper</c><00:02:46.200><c> just</c><00:02:46.590><c> you</c><00:02:46.739><c> can</c><00:02:46.890><c> actually</c><00:02:47.430><c> execute</c>

00:02:48.289 --> 00:02:48.299 align:start position:0%
the paper just you can actually execute
 

00:02:48.299 --> 00:02:50.449 align:start position:0%
the paper just you can actually execute
and<00:02:48.690><c> you</c><00:02:48.780><c> run</c><00:02:49.110><c> this</c><00:02:49.290><c> model</c><00:02:49.799><c> so</c><00:02:50.280><c> you</c><00:02:50.340><c> can</c>

00:02:50.449 --> 00:02:50.459 align:start position:0%
and you run this model so you can
 

00:02:50.459 --> 00:02:52.400 align:start position:0%
and you run this model so you can
actually<00:02:50.580><c> even</c><00:02:50.760><c> test</c><00:02:51.209><c> so</c><00:02:51.989><c> what</c><00:02:52.170><c> you</c><00:02:52.260><c> are</c><00:02:52.290><c> doing</c>

00:02:52.400 --> 00:02:52.410 align:start position:0%
actually even test so what you are doing
 

00:02:52.410 --> 00:02:55.940 align:start position:0%
actually even test so what you are doing
what<00:02:52.860><c> we've</c><00:02:53.670><c> done</c><00:02:53.819><c> so</c><00:02:54.030><c> far</c><00:02:54.060><c> is</c><00:02:54.390><c> we</c><00:02:55.049><c> write</c><00:02:55.769><c> down</c>

00:02:55.940 --> 00:02:55.950 align:start position:0%
what we've done so far is we write down
 

00:02:55.950 --> 00:02:58.699 align:start position:0%
what we've done so far is we write down
this<00:02:56.069><c> model</c><00:02:56.549><c> we</c><00:02:57.299><c> want</c><00:02:57.569><c> the</c><00:02:57.660><c> exactly</c><00:02:58.079><c> same</c><00:02:58.200><c> test</c>

00:02:58.699 --> 00:02:58.709 align:start position:0%
this model we want the exactly same test
 

00:02:58.709 --> 00:03:01.220 align:start position:0%
this model we want the exactly same test
the<00:02:59.250><c> conformance</c><00:02:59.670><c> test</c><00:02:59.880><c> suite</c><00:03:00.150><c> you</c><00:03:00.480><c> run</c><00:03:00.810><c> in</c>

00:03:01.220 --> 00:03:01.230 align:start position:0%
the conformance test suite you run in
 

00:03:01.230 --> 00:03:03.110 align:start position:0%
the conformance test suite you run in
the<00:03:01.380><c> clients</c><00:03:01.980><c> to</c><00:03:02.160><c> make</c><00:03:02.310><c> sure</c><00:03:02.519><c> that</c><00:03:02.730><c> you</c><00:03:02.910><c> all</c>

00:03:03.110 --> 00:03:03.120 align:start position:0%
the clients to make sure that you all
 

00:03:03.120 --> 00:03:04.370 align:start position:0%
the clients to make sure that you all
agree<00:03:03.810><c> on</c><00:03:03.959><c> that</c>

00:03:04.370 --> 00:03:04.380 align:start position:0%
agree on that
 

00:03:04.380 --> 00:03:06.680 align:start position:0%
agree on that
so<00:03:04.590><c> we</c><00:03:04.680><c> run</c><00:03:04.799><c> the</c><00:03:04.829><c> same</c><00:03:05.069><c> test</c><00:03:05.400><c> and</c><00:03:05.760><c> and</c><00:03:06.060><c> and</c><00:03:06.299><c> we</c>

00:03:06.680 --> 00:03:06.690 align:start position:0%
so we run the same test and and and we
 

00:03:06.690 --> 00:03:09.080 align:start position:0%
so we run the same test and and and we
make<00:03:06.870><c> sure</c><00:03:06.989><c> the</c><00:03:07.110><c> oil</c><00:03:07.140><c> Pat</c><00:03:07.560><c> test</c><00:03:07.920><c> passed</c><00:03:08.250><c> so</c><00:03:08.970><c> we</c>

00:03:09.080 --> 00:03:09.090 align:start position:0%
make sure the oil Pat test passed so we
 

00:03:09.090 --> 00:03:13.160 align:start position:0%
make sure the oil Pat test passed so we
were<00:03:09.299><c> very</c><00:03:09.569><c> high</c><00:03:10.410><c> confident</c><00:03:11.010><c> that</c><00:03:11.280><c> our</c><00:03:12.170><c> model</c>

00:03:13.160 --> 00:03:13.170 align:start position:0%
were very high confident that our model
 

00:03:13.170 --> 00:03:15.289 align:start position:0%
were very high confident that our model
actually<00:03:13.380><c> faithfully</c><00:03:14.190><c> captures</c><00:03:14.760><c> whatever</c>

00:03:15.289 --> 00:03:15.299 align:start position:0%
actually faithfully captures whatever
 

00:03:15.299 --> 00:03:21.319 align:start position:0%
actually faithfully captures whatever
the<00:03:16.459><c> spec</c><00:03:17.459><c> and</c><00:03:17.760><c> also</c><00:03:18.360><c> implementation</c><00:03:20.030><c> so</c><00:03:21.030><c> I</c>

00:03:21.319 --> 00:03:21.329 align:start position:0%
the spec and also implementation so I
 

00:03:21.329 --> 00:03:24.199 align:start position:0%
the spec and also implementation so I
will<00:03:21.829><c> get</c><00:03:22.829><c> to</c><00:03:22.920><c> that</c><00:03:22.950><c> how</c><00:03:23.340><c> what</c><00:03:23.639><c> it</c><00:03:23.760><c> looks</c><00:03:23.970><c> like</c>

00:03:24.199 --> 00:03:24.209 align:start position:0%
will get to that how what it looks like
 

00:03:24.209 --> 00:03:30.020 align:start position:0%
will get to that how what it looks like
the<00:03:24.630><c> KA</c><00:03:25.380><c> we</c><00:03:25.590><c> can</c><00:03:25.739><c> change</c><00:03:25.920><c> model</c><00:03:26.190><c> is</c><00:03:26.639><c> but</c><00:03:28.220><c> so</c><00:03:29.220><c> but</c>

00:03:30.020 --> 00:03:30.030 align:start position:0%
the KA we can change model is but so but
 

00:03:30.030 --> 00:03:32.270 align:start position:0%
the KA we can change model is but so but
right<00:03:30.359><c> now</c><00:03:30.569><c> we</c><00:03:30.630><c> finish</c><00:03:31.290><c> the</c><00:03:31.500><c> akkada</c><00:03:31.859><c> content</c>

00:03:32.270 --> 00:03:32.280 align:start position:0%
right now we finish the akkada content
 

00:03:32.280 --> 00:03:34.699 align:start position:0%
right now we finish the akkada content
model<00:03:32.609><c> and</c><00:03:32.819><c> the</c><00:03:33.150><c> next</c><00:03:33.600><c> thing</c><00:03:33.810><c> we</c><00:03:33.989><c> want</c><00:03:34.470><c> to</c><00:03:34.500><c> do</c>

00:03:34.699 --> 00:03:34.709 align:start position:0%
model and the next thing we want to do
 

00:03:34.709 --> 00:03:37.729 align:start position:0%
model and the next thing we want to do
is<00:03:34.980><c> using</c><00:03:35.549><c> that</c><00:03:35.760><c> model</c><00:03:35.970><c> to</c><00:03:36.359><c> prove</c><00:03:37.260><c> the</c><00:03:37.500><c> safety</c>

00:03:37.729 --> 00:03:37.739 align:start position:0%
is using that model to prove the safety
 

00:03:37.739 --> 00:03:40.449 align:start position:0%
is using that model to prove the safety
and<00:03:37.950><c> lightness</c><00:03:38.370><c> groups</c><00:03:38.700><c> on</c><00:03:38.970><c> that</c><00:03:39.569><c> model</c><00:03:39.780><c> and</c>

00:03:40.449 --> 00:03:40.459 align:start position:0%
and lightness groups on that model and
 

00:03:40.459 --> 00:03:43.640 align:start position:0%
and lightness groups on that model and
once<00:03:41.459><c> we've</c><00:03:41.700><c> done</c><00:03:41.730><c> these</c><00:03:42.090><c> things</c><00:03:42.380><c> we</c><00:03:43.380><c> really</c>

00:03:43.640 --> 00:03:43.650 align:start position:0%
once we've done these things we really
 

00:03:43.650 --> 00:03:45.800 align:start position:0%
once we've done these things we really
have<00:03:43.799><c> a</c><00:03:43.829><c> high</c><00:03:44.069><c> confident</c><00:03:44.670><c> that</c><00:03:44.910><c> your</c><00:03:45.359><c> actual</c>

00:03:45.800 --> 00:03:45.810 align:start position:0%
have a high confident that your actual
 

00:03:45.810 --> 00:03:48.349 align:start position:0%
have a high confident that your actual
client<00:03:46.170><c> implementation</c><00:03:46.889><c> also</c><00:03:47.299><c> satisfy</c><00:03:48.299><c> this</c>

00:03:48.349 --> 00:03:48.359 align:start position:0%
client implementation also satisfy this
 

00:03:48.359 --> 00:03:50.930 align:start position:0%
client implementation also satisfy this
nice<00:03:48.810><c> two</c><00:03:49.109><c> properties</c><00:03:49.500><c> as</c><00:03:49.920><c> long</c><00:03:50.609><c> as</c><00:03:50.760><c> you</c>

00:03:50.930 --> 00:03:50.940 align:start position:0%
nice two properties as long as you
 

00:03:50.940 --> 00:03:57.379 align:start position:0%
nice two properties as long as you
follow<00:03:51.209><c> the</c><00:03:51.389><c> word</c><00:03:51.690><c> of</c><00:03:51.810><c> the</c><00:03:51.930><c> spec</c><00:03:55.430><c> is</c><00:03:56.430><c> that</c><00:03:56.609><c> any</c>

00:03:57.379 --> 00:03:57.389 align:start position:0%
follow the word of the spec is that any
 

00:03:57.389 --> 00:04:06.410 align:start position:0%
follow the word of the spec is that any
question<00:03:57.810><c> at</c><00:03:58.680><c> this</c><00:03:58.799><c> point</c><00:04:02.030><c> okay</c><00:04:04.280><c> so</c><00:04:05.280><c> now</c><00:04:06.000><c> I'm</c>

00:04:06.410 --> 00:04:06.420 align:start position:0%
question at this point okay so now I'm
 

00:04:06.420 --> 00:04:08.809 align:start position:0%
question at this point okay so now I'm
going<00:04:07.079><c> to</c><00:04:07.139><c> show</c><00:04:07.349><c> you</c><00:04:07.410><c> how</c><00:04:07.680><c> these</c><00:04:07.920><c> formal</c><00:04:08.489><c> model</c>

00:04:08.809 --> 00:04:08.819 align:start position:0%
going to show you how these formal model
 

00:04:08.819 --> 00:04:16.449 align:start position:0%
going to show you how these formal model
looks<00:04:09.060><c> like</c><00:04:10.609><c> so</c><00:04:13.160><c> we</c><00:04:14.160><c> actually</c><00:04:15.049><c> decided</c><00:04:16.049><c> to</c>

00:04:16.449 --> 00:04:16.459 align:start position:0%
looks like so we actually decided to
 

00:04:16.459 --> 00:04:20.960 align:start position:0%
looks like so we actually decided to
have<00:04:17.459><c> release</c><00:04:18.560><c> the</c><00:04:19.560><c> model</c><00:04:19.919><c> that</c><00:04:20.099><c> very</c><00:04:20.700><c> similar</c>

00:04:20.960 --> 00:04:20.970 align:start position:0%
have release the model that very similar
 

00:04:20.970 --> 00:04:25.129 align:start position:0%
have release the model that very similar
to<00:04:21.750><c> the</c><00:04:21.979><c> spec</c><00:04:22.979><c> to</c><00:04:23.700><c> minimize</c><00:04:24.180><c> the</c><00:04:24.690><c> potential</c>

00:04:25.129 --> 00:04:25.139 align:start position:0%
to the spec to minimize the potential
 

00:04:25.139 --> 00:04:28.490 align:start position:0%
to the spec to minimize the potential
mistakes<00:04:25.550><c> that</c><00:04:26.550><c> made</c><00:04:26.820><c> we</c><00:04:27.210><c> write</c><00:04:28.140><c> down</c><00:04:28.349><c> this</c>

00:04:28.490 --> 00:04:28.500 align:start position:0%
mistakes that made we write down this
 

00:04:28.500 --> 00:04:31.010 align:start position:0%
mistakes that made we write down this
phone<00:04:28.710><c> model</c><00:04:29.130><c> the</c><00:04:29.580><c> reason</c><00:04:29.849><c> that</c><00:04:30.180><c> this</c><00:04:30.599><c> because</c>

00:04:31.010 --> 00:04:31.020 align:start position:0%
phone model the reason that this because
 

00:04:31.020 --> 00:04:32.060 align:start position:0%
phone model the reason that this because
we<00:04:31.260><c> this</c>

00:04:32.060 --> 00:04:32.070 align:start position:0%
we this
 

00:04:32.070 --> 00:04:35.060 align:start position:0%
we this
is<00:04:32.160><c> important</c><00:04:32.580><c> because</c><00:04:32.700><c> if</c><00:04:33.690><c> our</c><00:04:34.230><c> formal</c><00:04:34.680><c> model</c>

00:04:35.060 --> 00:04:35.070 align:start position:0%
is important because if our formal model
 

00:04:35.070 --> 00:04:38.330 align:start position:0%
is important because if our formal model
has<00:04:35.370><c> some</c><00:04:35.570><c> mean</c><00:04:36.570><c> differences</c><00:04:37.260><c> from</c><00:04:37.890><c> whatever</c>

00:04:38.330 --> 00:04:38.340 align:start position:0%
has some mean differences from whatever
 

00:04:38.340 --> 00:04:41.330 align:start position:0%
has some mean differences from whatever
spec<00:04:38.850><c> or</c><00:04:39.000><c> implementations</c><00:04:40.160><c> even</c><00:04:41.160><c> if</c><00:04:41.250><c> you</c>

00:04:41.330 --> 00:04:41.340 align:start position:0%
spec or implementations even if you
 

00:04:41.340 --> 00:04:43.460 align:start position:0%
spec or implementations even if you
prove<00:04:41.580><c> these</c><00:04:41.790><c> things</c><00:04:42.060><c> they</c><00:04:42.750><c> meant</c><00:04:42.990><c> may</c><00:04:43.260><c> not</c>

00:04:43.460 --> 00:04:43.470 align:start position:0%
prove these things they meant may not
 

00:04:43.470 --> 00:04:45.350 align:start position:0%
prove these things they meant may not
hold<00:04:43.680><c> in</c><00:04:44.010><c> the</c><00:04:44.100><c> actual</c><00:04:44.340><c> implementation</c><00:04:44.490><c> unless</c>

00:04:45.350 --> 00:04:45.360 align:start position:0%
hold in the actual implementation unless
 

00:04:45.360 --> 00:04:47.720 align:start position:0%
hold in the actual implementation unless
we<00:04:45.600><c> verify</c><00:04:46.020><c> again</c><00:04:46.380><c> same</c><00:04:46.650><c> thing</c><00:04:46.710><c> over</c><00:04:47.070><c> those</c>

00:04:47.720 --> 00:04:47.730 align:start position:0%
we verify again same thing over those
 

00:04:47.730 --> 00:04:52.300 align:start position:0%
we verify again same thing over those
implementation<00:04:48.630><c> as</c><00:04:49.730><c> the</c><00:04:50.730><c> what</c><00:04:51.240><c> are</c><00:04:51.510><c> the</c>

00:04:52.300 --> 00:04:52.310 align:start position:0%
implementation as the what are the
 

00:04:52.310 --> 00:04:58.400 align:start position:0%
implementation as the what are the
lighthouse<00:04:53.310><c> as</c><00:04:54.270><c> I</c><00:04:54.390><c> said</c><00:04:54.630><c> right</c><00:04:54.990><c> so</c><00:04:57.410><c> we</c>

00:04:58.400 --> 00:04:58.410 align:start position:0%
lighthouse as I said right so we
 

00:04:58.410 --> 00:05:00.740 align:start position:0%
lighthouse as I said right so we
actually<00:04:58.590><c> have</c><00:04:58.920><c> very</c><00:04:59.130><c> similar</c><00:04:59.570><c> formal</c><00:05:00.570><c> motor</c>

00:05:00.740 --> 00:05:00.750 align:start position:0%
actually have very similar formal motor
 

00:05:00.750 --> 00:05:03.740 align:start position:0%
actually have very similar formal motor
that<00:05:01.230><c> looks</c><00:05:01.710><c> like</c><00:05:02.180><c> almost</c><00:05:03.180><c> one-to-one</c>

00:05:03.740 --> 00:05:03.750 align:start position:0%
that looks like almost one-to-one
 

00:05:03.750 --> 00:05:06.860 align:start position:0%
that looks like almost one-to-one
correspondence<00:05:04.050><c> to</c><00:05:04.650><c> the</c><00:05:04.920><c> spec</c><00:05:05.430><c> so</c><00:05:06.270><c> I</c><00:05:06.300><c> will</c>

00:05:06.860 --> 00:05:06.870 align:start position:0%
correspondence to the spec so I will
 

00:05:06.870 --> 00:05:08.960 align:start position:0%
correspondence to the spec so I will
give<00:05:07.020><c> you</c><00:05:07.140><c> some</c><00:05:07.350><c> example</c><00:05:07.830><c> huh</c><00:05:07.890><c> looks</c><00:05:08.100><c> like</c><00:05:08.340><c> so</c>

00:05:08.960 --> 00:05:08.970 align:start position:0%
give you some example huh looks like so
 

00:05:08.970 --> 00:05:10.990 align:start position:0%
give you some example huh looks like so
here<00:05:09.300><c> the</c><00:05:09.450><c> left-hand</c><00:05:09.810><c> side</c><00:05:10.020><c> we</c><00:05:10.350><c> have</c><00:05:10.500><c> a</c><00:05:10.530><c> Python</c>

00:05:10.990 --> 00:05:11.000 align:start position:0%
here the left-hand side we have a Python
 

00:05:11.000 --> 00:05:14.030 align:start position:0%
here the left-hand side we have a Python
spec<00:05:12.000><c> especially</c><00:05:12.840><c> for</c><00:05:13.050><c> the</c><00:05:13.380><c> beacon</c><00:05:13.770><c> change</c>

00:05:14.030 --> 00:05:14.040 align:start position:0%
spec especially for the beacon change
 

00:05:14.040 --> 00:05:16.910 align:start position:0%
spec especially for the beacon change
state<00:05:14.490><c> definition</c><00:05:15.410><c> so</c><00:05:16.410><c> here</c><00:05:16.530><c> you</c><00:05:16.680><c> can</c><00:05:16.830><c> change</c>

00:05:16.910 --> 00:05:16.920 align:start position:0%
state definition so here you can change
 

00:05:16.920 --> 00:05:19.010 align:start position:0%
state definition so here you can change
the<00:05:17.040><c> definition</c><00:05:17.580><c> the</c><00:05:17.970><c> user</c><00:05:18.450><c> Python</c><00:05:18.900><c> data</c>

00:05:19.010 --> 00:05:19.020 align:start position:0%
the definition the user Python data
 

00:05:19.020 --> 00:05:22.090 align:start position:0%
the definition the user Python data
structure<00:05:19.350><c> there</c><00:05:19.980><c> are</c><00:05:20.040><c> many</c><00:05:20.220><c> things</c><00:05:20.910><c> here</c><00:05:21.300><c> and</c>

00:05:22.090 --> 00:05:22.100 align:start position:0%
structure there are many things here and
 

00:05:22.100 --> 00:05:25.340 align:start position:0%
structure there are many things here and
the<00:05:23.100><c> right-hand</c><00:05:23.460><c> side</c><00:05:23.550><c> is</c><00:05:23.850><c> our</c><00:05:24.000><c> K</c><00:05:24.330><c> called</c><00:05:24.960><c> K</c>

00:05:25.340 --> 00:05:25.350 align:start position:0%
the right-hand side is our K called K
 

00:05:25.350 --> 00:05:26.690 align:start position:0%
the right-hand side is our K called K
configuration<00:05:26.070><c> which</c><00:05:26.220><c> is</c><00:05:26.370><c> a</c><00:05:26.400><c> mathematical</c>

00:05:26.690 --> 00:05:26.700 align:start position:0%
configuration which is a mathematical
 

00:05:26.700 --> 00:05:29.990 align:start position:0%
configuration which is a mathematical
object<00:05:27.600><c> of</c><00:05:28.170><c> the</c><00:05:28.410><c> same</c><00:05:28.650><c> exact</c><00:05:29.430><c> beacon</c><00:05:29.790><c> change</c>

00:05:29.990 --> 00:05:30.000 align:start position:0%
object of the same exact beacon change
 

00:05:30.000 --> 00:05:33.290 align:start position:0%
object of the same exact beacon change
state<00:05:30.300><c> and</c><00:05:30.600><c> we</c><00:05:31.290><c> have</c><00:05:31.800><c> really</c><00:05:32.310><c> similar</c>

00:05:33.290 --> 00:05:33.300 align:start position:0%
state and we have really similar
 

00:05:33.300 --> 00:05:36.950 align:start position:0%
state and we have really similar
structure<00:05:34.020><c> that</c><00:05:34.890><c> you</c><00:05:35.670><c> can</c><00:05:35.790><c> even</c><00:05:36.030><c> follow</c><00:05:36.330><c> the</c><00:05:36.570><c> H</c>

00:05:36.950 --> 00:05:36.960 align:start position:0%
structure that you can even follow the H
 

00:05:36.960 --> 00:05:41.420 align:start position:0%
structure that you can even follow the H
want<00:05:37.320><c> one</c><00:05:37.590><c> line</c><00:05:38.540><c> drawing</c><00:05:39.540><c> the</c><00:05:39.780><c> slot</c><00:05:40.410><c> same</c><00:05:41.160><c> it's</c>

00:05:41.420 --> 00:05:41.430 align:start position:0%
want one line drawing the slot same it's
 

00:05:41.430 --> 00:05:44.330 align:start position:0%
want one line drawing the slot same it's
one<00:05:41.700><c> data</c><00:05:41.940><c> and</c><00:05:42.270><c> so</c><00:05:42.690><c> on</c><00:05:42.780><c> is</c><00:05:42.900><c> force</c><00:05:43.170><c> so</c><00:05:44.010><c> make</c><00:05:44.190><c> sure</c>

00:05:44.330 --> 00:05:44.340 align:start position:0%
one data and so on is force so make sure
 

00:05:44.340 --> 00:05:46.370 align:start position:0%
one data and so on is force so make sure
that<00:05:44.520><c> they</c><00:05:44.790><c> are</c><00:05:44.910><c> very</c><00:05:44.940><c> similar</c><00:05:45.300><c> and</c><00:05:46.110><c> make</c><00:05:46.260><c> sure</c>

00:05:46.370 --> 00:05:46.380 align:start position:0%
that they are very similar and make sure
 

00:05:46.380 --> 00:05:49.100 align:start position:0%
that they are very similar and make sure
that<00:05:46.560><c> you're</c><00:05:46.950><c> not</c><00:05:47.460><c> missing</c><00:05:47.730><c> any</c><00:05:48.110><c> important</c>

00:05:49.100 --> 00:05:49.110 align:start position:0%
that you're not missing any important
 

00:05:49.110 --> 00:05:52.820 align:start position:0%
that you're not missing any important
thing<00:05:49.320><c> that's</c><00:05:49.920><c> the</c><00:05:50.070><c> one</c><00:05:50.220><c> thing</c><00:05:51.170><c> next</c><00:05:52.170><c> thing</c><00:05:52.530><c> is</c>

00:05:52.820 --> 00:05:52.830 align:start position:0%
thing that's the one thing next thing is
 

00:05:52.830 --> 00:05:54.830 align:start position:0%
thing that's the one thing next thing is
we<00:05:53.490><c> have</c><00:05:53.580><c> a</c><00:05:53.610><c> bunch</c><00:05:53.820><c> of</c><00:05:54.000><c> the</c><00:05:54.150><c> functions</c><00:05:54.600><c> in</c><00:05:54.810><c> the</c>

00:05:54.830 --> 00:05:54.840 align:start position:0%
we have a bunch of the functions in the
 

00:05:54.840 --> 00:05:57.260 align:start position:0%
we have a bunch of the functions in the
Python<00:05:55.110><c> specs</c><00:05:55.620><c> right</c><00:05:55.920><c> so</c><00:05:56.190><c> each</c><00:05:56.430><c> function</c><00:05:57.000><c> we</c>

00:05:57.260 --> 00:05:57.270 align:start position:0%
Python specs right so each function we
 

00:05:57.270 --> 00:06:01.580 align:start position:0%
Python specs right so each function we
have<00:05:58.490><c> K</c><00:05:59.490><c> called</c><00:06:00.360><c> rules</c><00:06:00.690><c> so</c><00:06:01.140><c> you</c><00:06:01.170><c> can</c><00:06:01.410><c> think</c>

00:06:01.580 --> 00:06:01.590 align:start position:0%
have K called rules so you can think
 

00:06:01.590 --> 00:06:03.500 align:start position:0%
have K called rules so you can think
about<00:06:01.650><c> rule</c><00:06:02.010><c> as</c><00:06:02.160><c> a</c><00:06:02.190><c> like</c><00:06:02.520><c> function</c><00:06:03.000><c> the</c><00:06:03.090><c> Python</c>

00:06:03.500 --> 00:06:03.510 align:start position:0%
about rule as a like function the Python
 

00:06:03.510 --> 00:06:05.780 align:start position:0%
about rule as a like function the Python
so<00:06:04.230><c> in</c><00:06:04.680><c> the</c><00:06:04.800><c> function</c><00:06:05.190><c> we</c><00:06:05.280><c> have</c><00:06:05.460><c> left</c><00:06:05.670><c> hand</c>

00:06:05.780 --> 00:06:05.790 align:start position:0%
so in the function we have left hand
 

00:06:05.790 --> 00:06:09.170 align:start position:0%
so in the function we have left hand
side<00:06:06.000><c> is</c><00:06:06.450><c> called</c><00:06:06.950><c> process</c><00:06:07.950><c> app</c><00:06:08.160><c> o</c><00:06:08.430><c> we</c><00:06:08.970><c> have</c>

00:06:09.170 --> 00:06:09.180 align:start position:0%
side is called process app o we have
 

00:06:09.180 --> 00:06:11.240 align:start position:0%
side is called process app o we have
like<00:06:09.660><c> called</c><00:06:10.020><c> a</c><00:06:10.080><c> bunch</c><00:06:10.230><c> of</c><00:06:10.380><c> function</c><00:06:11.130><c> in</c>

00:06:11.240 --> 00:06:11.250 align:start position:0%
like called a bunch of function in
 

00:06:11.250 --> 00:06:14.210 align:start position:0%
like called a bunch of function in
sequence<00:06:11.690><c> and</c><00:06:12.690><c> then</c><00:06:12.870><c> in</c><00:06:12.990><c> the</c><00:06:13.080><c> K</c><00:06:13.290><c> model</c><00:06:13.830><c> we</c><00:06:13.980><c> have</c>

00:06:14.210 --> 00:06:14.220 align:start position:0%
sequence and then in the K model we have
 

00:06:14.220 --> 00:06:17.600 align:start position:0%
sequence and then in the K model we have
same<00:06:15.030><c> thing</c><00:06:15.360><c> we</c><00:06:16.020><c> these</c><00:06:16.590><c> curly</c><00:06:17.070><c> arrow</c><00:06:17.400><c> means</c>

00:06:17.600 --> 00:06:17.610 align:start position:0%
same thing we these curly arrow means
 

00:06:17.610 --> 00:06:20.000 align:start position:0%
same thing we these curly arrow means
that<00:06:17.970><c> it</c><00:06:18.210><c> calls</c><00:06:18.750><c> followed</c><00:06:19.230><c> by</c><00:06:19.350><c> these</c><00:06:19.770><c> and</c>

00:06:20.000 --> 00:06:20.010 align:start position:0%
that it calls followed by these and
 

00:06:20.010 --> 00:06:22.190 align:start position:0%
that it calls followed by these and
followed<00:06:20.220><c> by</c><00:06:20.370><c> that</c><00:06:20.580><c> so</c><00:06:21.360><c> you</c><00:06:21.780><c> can</c><00:06:21.930><c> see</c><00:06:22.050><c> also</c>

00:06:22.190 --> 00:06:22.200 align:start position:0%
followed by that so you can see also
 

00:06:22.200 --> 00:06:24.260 align:start position:0%
followed by that so you can see also
very<00:06:22.530><c> similar</c><00:06:22.740><c> the</c><00:06:23.370><c> only</c><00:06:23.400><c> difference</c><00:06:23.580><c> is</c><00:06:24.030><c> made</c>

00:06:24.260 --> 00:06:24.270 align:start position:0%
very similar the only difference is made
 

00:06:24.270 --> 00:06:26.380 align:start position:0%
very similar the only difference is made
is<00:06:24.510><c> they</c><00:06:24.900><c> have</c><00:06:25.140><c> what</c><00:06:25.350><c> this</c><00:06:25.470><c> state</c><00:06:25.830><c> is</c>

00:06:26.380 --> 00:06:26.390 align:start position:0%
is they have what this state is
 

00:06:26.390 --> 00:06:28.880 align:start position:0%
is they have what this state is
explicitly<00:06:27.390><c> mention</c><00:06:27.750><c> is</c><00:06:27.870><c> here</c><00:06:28.230><c> and</c><00:06:28.440><c> no</c><00:06:28.650><c> state</c>

00:06:28.880 --> 00:06:28.890 align:start position:0%
explicitly mention is here and no state
 

00:06:28.890 --> 00:06:31.310 align:start position:0%
explicitly mention is here and no state
mentioned<00:06:29.250><c> that</c><00:06:29.420><c> many</c><00:06:30.420><c> because</c><00:06:30.570><c> that</c><00:06:31.050><c> state</c>

00:06:31.310 --> 00:06:31.320 align:start position:0%
mentioned that many because that state
 

00:06:31.320 --> 00:06:33.650 align:start position:0%
mentioned that many because that state
actually<00:06:31.710><c> it's</c><00:06:31.800><c> already</c><00:06:32.220><c> global</c><00:06:32.880><c> which</c><00:06:33.450><c> can</c>

00:06:33.650 --> 00:06:33.660 align:start position:0%
actually it's already global which can
 

00:06:33.660 --> 00:06:36.770 align:start position:0%
actually it's already global which can
be<00:06:33.780><c> accessed</c><00:06:34.470><c> accessed</c><00:06:35.330><c> which</c><00:06:36.330><c> is</c><00:06:36.480><c> in</c><00:06:36.600><c> the</c>

00:06:36.770 --> 00:06:36.780 align:start position:0%
be accessed accessed which is in the
 

00:06:36.780 --> 00:06:39.770 align:start position:0%
be accessed accessed which is in the
next<00:06:37.020><c> example</c><00:06:37.290><c> so</c><00:06:38.250><c> for</c><00:06:38.820><c> example</c><00:06:39.210><c> if</c><00:06:39.390><c> your</c>

00:06:39.770 --> 00:06:39.780 align:start position:0%
next example so for example if your
 

00:06:39.780 --> 00:06:43.310 align:start position:0%
next example so for example if your
function<00:06:40.460><c> access</c><00:06:41.460><c> any</c><00:06:41.730><c> state</c><00:06:42.150><c> like</c><00:06:42.720><c> state</c>

00:06:43.310 --> 00:06:43.320 align:start position:0%
function access any state like state
 

00:06:43.320 --> 00:06:46.189 align:start position:0%
function access any state like state
that<00:06:43.650><c> slot</c><00:06:44.360><c> in</c><00:06:45.360><c> our</c><00:06:45.540><c> K</c><00:06:45.780><c> mode</c>

00:06:46.189 --> 00:06:46.199 align:start position:0%
that slot in our K mode
 

00:06:46.199 --> 00:06:48.850 align:start position:0%
that slot in our K mode
we<00:06:46.379><c> can</c><00:06:46.529><c> simply</c><00:06:47.009><c> mention</c><00:06:47.460><c> those</c><00:06:47.669><c> slot</c><00:06:48.180><c> this</c>

00:06:48.850 --> 00:06:48.860 align:start position:0%
we can simply mention those slot this
 

00:06:48.860 --> 00:06:53.119 align:start position:0%
we can simply mention those slot this
called<00:06:49.860><c> configuration</c><00:06:51.169><c> you</c><00:06:52.169><c> just</c><00:06:52.409><c> mentioned</c>

00:06:53.119 --> 00:06:53.129 align:start position:0%
called configuration you just mentioned
 

00:06:53.129 --> 00:06:55.129 align:start position:0%
called configuration you just mentioned
that<00:06:53.159><c> that</c><00:06:53.520><c> means</c><00:06:53.699><c> you</c><00:06:53.879><c> just</c><00:06:54.029><c> match</c><00:06:54.389><c> that</c><00:06:54.749><c> so</c>

00:06:55.129 --> 00:06:55.139 align:start position:0%
that that means you just match that so
 

00:06:55.139 --> 00:06:57.110 align:start position:0%
that that means you just match that so
match<00:06:55.409><c> the</c><00:06:55.680><c> current</c><00:06:56.039><c> state</c><00:06:56.460><c> and</c><00:06:56.789><c> then</c><00:06:56.939><c> you</c><00:06:56.999><c> can</c>

00:06:57.110 --> 00:06:57.120 align:start position:0%
match the current state and then you can
 

00:06:57.120 --> 00:06:59.689 align:start position:0%
match the current state and then you can
just<00:06:57.270><c> use</c><00:06:57.689><c> that</c><00:06:57.930><c> whatever</c><00:06:58.800><c> match</c><00:06:59.069><c> there</c><00:06:59.430><c> in</c>

00:06:59.689 --> 00:06:59.699 align:start position:0%
just use that whatever match there in
 

00:06:59.699 --> 00:07:03.769 align:start position:0%
just use that whatever match there in
your<00:07:00.949><c> like</c><00:07:01.949><c> function</c><00:07:02.279><c> body</c><00:07:02.719><c> instead</c><00:07:03.719><c> of</c>

00:07:03.769 --> 00:07:03.779 align:start position:0%
your like function body instead of
 

00:07:03.779 --> 00:07:05.659 align:start position:0%
your like function body instead of
static<00:07:04.020><c> say</c><00:07:04.590><c> that</c><00:07:04.770><c> slot</c><00:07:05.099><c> can</c><00:07:05.310><c> just</c><00:07:05.460><c> mention</c>

00:07:05.659 --> 00:07:05.669 align:start position:0%
static say that slot can just mention
 

00:07:05.669 --> 00:07:12.529 align:start position:0%
static say that slot can just mention
the<00:07:05.999><c> state</c><00:07:06.840><c> slot</c><00:07:09.800><c> and</c><00:07:10.909><c> then</c><00:07:11.909><c> if</c><00:07:12.180><c> you</c><00:07:12.300><c> have</c><00:07:12.389><c> any</c>

00:07:12.529 --> 00:07:12.539 align:start position:0%
the state slot and then if you have any
 

00:07:12.539 --> 00:07:14.839 align:start position:0%
the state slot and then if you have any
if<00:07:12.810><c> statement</c><00:07:13.469><c> I</c><00:07:13.529><c> like</c><00:07:13.680><c> assault</c><00:07:14.069><c> which</c><00:07:14.400><c> can</c><00:07:14.669><c> be</c>

00:07:14.839 --> 00:07:14.849 align:start position:0%
if statement I like assault which can be
 

00:07:14.849 --> 00:07:18.890 align:start position:0%
if statement I like assault which can be
described<00:07:15.360><c> as</c><00:07:15.479><c> our</c><00:07:15.689><c> requires</c><00:07:16.229><c> clothes</c><00:07:17.189><c> so</c><00:07:17.999><c> it</c>

00:07:18.890 --> 00:07:18.900 align:start position:0%
described as our requires clothes so it
 

00:07:18.900 --> 00:07:20.239 align:start position:0%
described as our requires clothes so it
pretty<00:07:19.229><c> much</c><00:07:19.379><c> very</c><00:07:19.589><c> similar</c><00:07:19.620><c> you</c><00:07:19.949><c> can</c><00:07:20.009><c> see</c>

00:07:20.239 --> 00:07:20.249 align:start position:0%
pretty much very similar you can see
 

00:07:20.249 --> 00:07:24.409 align:start position:0%
pretty much very similar you can see
this<00:07:20.400><c> right</c><00:07:21.379><c> so</c><00:07:22.379><c> one</c><00:07:23.189><c> thing</c><00:07:23.370><c> is</c><00:07:23.400><c> like</c><00:07:23.759><c> former</c>

00:07:24.409 --> 00:07:24.419 align:start position:0%
this right so one thing is like former
 

00:07:24.419 --> 00:07:27.110 align:start position:0%
this right so one thing is like former
motor<00:07:24.629><c> is</c><00:07:24.779><c> not</c><00:07:24.960><c> really</c><00:07:25.169><c> like</c><00:07:25.909><c> different</c><00:07:26.909><c> thing</c>

00:07:27.110 --> 00:07:27.120 align:start position:0%
motor is not really like different thing
 

00:07:27.120 --> 00:07:30.909 align:start position:0%
motor is not really like different thing
or<00:07:27.270><c> like</c><00:07:27.949><c> things</c><00:07:28.949><c> you</c><00:07:29.189><c> can</c><00:07:29.339><c> even</c><00:07:29.669><c> write</c><00:07:29.819><c> it</c>

00:07:30.909 --> 00:07:30.919 align:start position:0%
or like things you can even write it
 

00:07:30.919 --> 00:07:35.239 align:start position:0%
or like things you can even write it
from<00:07:31.919><c> in</c><00:07:32.550><c> okay</c><00:07:33.330><c> as</c><00:07:33.960><c> long</c><00:07:34.650><c> as</c><00:07:34.770><c> you</c><00:07:34.889><c> know</c><00:07:35.039><c> how</c><00:07:35.219><c> to</c>

00:07:35.239 --> 00:07:35.249 align:start position:0%
from in okay as long as you know how to
 

00:07:35.249 --> 00:07:37.850 align:start position:0%
from in okay as long as you know how to
write<00:07:35.639><c> our</c><00:07:35.789><c> interpreter</c><00:07:36.210><c> or</c><00:07:36.599><c> writing</c><00:07:37.050><c> the</c><00:07:37.199><c> -</c>

00:07:37.850 --> 00:07:37.860 align:start position:0%
write our interpreter or writing the -
 

00:07:37.860 --> 00:07:42.140 align:start position:0%
write our interpreter or writing the -
code<00:07:38.779><c> so</c><00:07:39.779><c> that's</c><00:07:40.199><c> that</c><00:07:40.650><c> but</c><00:07:41.159><c> the</c><00:07:41.639><c> there</c><00:07:42.060><c> are</c>

00:07:42.140 --> 00:07:42.150 align:start position:0%
code so that's that but the there are
 

00:07:42.150 --> 00:07:43.790 align:start position:0%
code so that's that but the there are
some<00:07:42.240><c> exception</c><00:07:42.689><c> that</c><00:07:42.930><c> we</c><00:07:43.229><c> are</c><00:07:43.349><c> not</c><00:07:43.499><c> really</c>

00:07:43.790 --> 00:07:43.800 align:start position:0%
some exception that we are not really
 

00:07:43.800 --> 00:07:48.050 align:start position:0%
some exception that we are not really
similar<00:07:45.050><c> in</c><00:07:46.050><c> the</c><00:07:46.620><c> case</c><00:07:46.830><c> that</c><00:07:47.039><c> we</c><00:07:47.159><c> have</c><00:07:47.370><c> Python</c>

00:07:48.050 --> 00:07:48.060 align:start position:0%
similar in the case that we have Python
 

00:07:48.060 --> 00:07:50.350 align:start position:0%
similar in the case that we have Python
list<00:07:48.449><c> comprehension</c><00:07:48.810><c> so</c><00:07:49.650><c> in</c><00:07:49.710><c> this</c><00:07:49.830><c> case</c><00:07:50.099><c> this</c>

00:07:50.350 --> 00:07:50.360 align:start position:0%
list comprehension so in this case this
 

00:07:50.360 --> 00:07:53.029 align:start position:0%
list comprehension so in this case this
we<00:07:51.360><c> have</c><00:07:51.569><c> these</c><00:07:51.719><c> matching</c><00:07:52.680><c> target</c>

00:07:53.029 --> 00:07:53.039 align:start position:0%
we have these matching target
 

00:07:53.039 --> 00:07:55.300 align:start position:0%
we have these matching target
attestation<00:07:53.460><c> which</c><00:07:53.699><c> simply</c><00:07:54.629><c> filtering</c><00:07:54.930><c> out</c>

00:07:55.300 --> 00:07:55.310 align:start position:0%
attestation which simply filtering out
 

00:07:55.310 --> 00:07:58.429 align:start position:0%
attestation which simply filtering out
whatever<00:07:56.310><c> the</c><00:07:56.550><c> target</c><00:07:56.759><c> is</c><00:07:56.969><c> not</c><00:07:57.149><c> matched</c><00:07:57.439><c> and</c>

00:07:58.429 --> 00:07:58.439 align:start position:0%
whatever the target is not matched and
 

00:07:58.439 --> 00:07:59.719 align:start position:0%
whatever the target is not matched and
then<00:07:58.589><c> Python</c><00:07:58.979><c> using</c><00:07:59.310><c> this</c><00:07:59.399><c> list</c>

00:07:59.719 --> 00:07:59.729 align:start position:0%
then Python using this list
 

00:07:59.729 --> 00:08:01.249 align:start position:0%
then Python using this list
comprehension<00:08:00.120><c> which</c><00:08:00.449><c> is</c><00:08:00.569><c> really</c><00:08:00.899><c> succeed</c>

00:08:01.249 --> 00:08:01.259 align:start position:0%
comprehension which is really succeed
 

00:08:01.259 --> 00:08:05.719 align:start position:0%
comprehension which is really succeed
and<00:08:01.529><c> is</c><00:08:02.189><c> to</c><00:08:02.399><c> read</c><00:08:02.810><c> but</c><00:08:03.810><c> we</c><00:08:04.020><c> decided</c><00:08:04.860><c> to</c><00:08:05.099><c> not</c>

00:08:05.719 --> 00:08:05.729 align:start position:0%
and is to read but we decided to not
 

00:08:05.729 --> 00:08:07.730 align:start position:0%
and is to read but we decided to not
using<00:08:06.149><c> these</c><00:08:06.270><c> risk</c><00:08:06.779><c> comprehension</c><00:08:07.289><c> and</c>

00:08:07.730 --> 00:08:07.740 align:start position:0%
using these risk comprehension and
 

00:08:07.740 --> 00:08:10.040 align:start position:0%
using these risk comprehension and
similar<00:08:08.129><c> syntax</c><00:08:08.370><c> because</c><00:08:08.669><c> we</c><00:08:09.330><c> think</c><00:08:09.719><c> that</c>

00:08:10.040 --> 00:08:10.050 align:start position:0%
similar syntax because we think that
 

00:08:10.050 --> 00:08:12.170 align:start position:0%
similar syntax because we think that
it's<00:08:10.349><c> more</c><00:08:10.770><c> eat</c><00:08:11.039><c> I</c><00:08:11.219><c> mean</c><00:08:11.399><c> it's</c><00:08:11.699><c> better</c><00:08:11.909><c> to</c>

00:08:12.170 --> 00:08:12.180 align:start position:0%
it's more eat I mean it's better to
 

00:08:12.180 --> 00:08:14.329 align:start position:0%
it's more eat I mean it's better to
explicitly<00:08:12.839><c> specify</c><00:08:13.409><c> what's</c><00:08:13.680><c> going</c><00:08:13.949><c> on</c><00:08:14.099><c> here</c>

00:08:14.329 --> 00:08:14.339 align:start position:0%
explicitly specify what's going on here
 

00:08:14.339 --> 00:08:16.700 align:start position:0%
explicitly specify what's going on here
using<00:08:14.789><c> the</c><00:08:14.939><c> traditional</c><00:08:15.599><c> iteration</c><00:08:16.439><c> approach</c>

00:08:16.700 --> 00:08:16.710 align:start position:0%
using the traditional iteration approach
 

00:08:16.710 --> 00:08:22.040 align:start position:0%
using the traditional iteration approach
so<00:08:17.460><c> we</c><00:08:17.610><c> have</c><00:08:17.819><c> like</c><00:08:20.180><c> defining</c><00:08:21.180><c> filter</c><00:08:21.629><c> function</c>

00:08:22.040 --> 00:08:22.050 align:start position:0%
so we have like defining filter function
 

00:08:22.050 --> 00:08:23.929 align:start position:0%
so we have like defining filter function
and<00:08:22.199><c> filter</c><00:08:22.469><c> function</c><00:08:22.830><c> is</c><00:08:22.919><c> simply</c><00:08:23.219><c> trade</c><00:08:23.699><c> each</c>

00:08:23.929 --> 00:08:23.939 align:start position:0%
and filter function is simply trade each
 

00:08:23.939 --> 00:08:27.619 align:start position:0%
and filter function is simply trade each
data<00:08:24.870><c> station</c><00:08:25.050><c> list</c><00:08:25.349><c> and</c><00:08:25.680><c> then</c><00:08:25.879><c> if</c><00:08:26.879><c> the</c>

00:08:27.619 --> 00:08:27.629 align:start position:0%
data station list and then if the
 

00:08:27.629 --> 00:08:29.269 align:start position:0%
data station list and then if the
targets<00:08:27.990><c> match</c><00:08:28.229><c> then</c><00:08:28.499><c> it</c><00:08:28.620><c> include</c><00:08:28.919><c> otherwise</c>

00:08:29.269 --> 00:08:29.279 align:start position:0%
targets match then it include otherwise
 

00:08:29.279 --> 00:08:33.740 align:start position:0%
targets match then it include otherwise
our<00:08:30.120><c> filtering</c><00:08:30.479><c> out</c><00:08:31.669><c> so</c><00:08:32.669><c> this</c><00:08:33.240><c> is</c><00:08:33.419><c> kind</c><00:08:33.630><c> of</c>

00:08:33.740 --> 00:08:33.750 align:start position:0%
our filtering out so this is kind of
 

00:08:33.750 --> 00:08:36.139 align:start position:0%
our filtering out so this is kind of
exception<00:08:34.169><c> that</c><00:08:34.349><c> the</c><00:08:34.890><c> two</c><00:08:35.310><c> models</c><00:08:35.760><c> are</c><00:08:35.909><c> a</c>

00:08:36.139 --> 00:08:36.149 align:start position:0%
exception that the two models are a
 

00:08:36.149 --> 00:08:37.519 align:start position:0%
exception that the two models are a
little<00:08:36.300><c> bit</c><00:08:36.510><c> different</c><00:08:36.930><c> but</c><00:08:37.050><c> is</c><00:08:37.169><c> but</c>

00:08:37.519 --> 00:08:37.529 align:start position:0%
little bit different but is but
 

00:08:37.529 --> 00:08:44.089 align:start position:0%
little bit different but is but
essentially<00:08:37.949><c> they</c><00:08:38.039><c> are</c><00:08:38.130><c> same</c><00:08:39.199><c> so</c><00:08:41.750><c> that</c><00:08:42.750><c> is</c><00:08:43.139><c> how</c>

00:08:44.089 --> 00:08:44.099 align:start position:0%
essentially they are same so that is how
 

00:08:44.099 --> 00:08:48.439 align:start position:0%
essentially they are same so that is how
this<00:08:44.639><c> former</c><00:08:45.180><c> model</c><00:08:45.300><c> looks</c><00:08:45.660><c> like</c><00:08:45.959><c> and</c><00:08:46.230><c> then</c><00:08:47.449><c> we</c>

00:08:48.439 --> 00:08:48.449 align:start position:0%
this former model looks like and then we
 

00:08:48.449 --> 00:08:50.240 align:start position:0%
this former model looks like and then we
already<00:08:48.720><c> have</c><00:08:48.870><c> a</c><00:08:48.899><c> good</c><00:08:49.139><c> competence</c><00:08:49.649><c> that</c><00:08:49.769><c> I</c>

00:08:50.240 --> 00:08:50.250 align:start position:0%
already have a good competence that I
 

00:08:50.250 --> 00:08:52.100 align:start position:0%
already have a good competence that I
mean<00:08:50.610><c> these</c><00:08:50.880><c> two</c><00:08:51.089><c> are</c><00:08:51.209><c> very</c><00:08:51.360><c> similar</c><00:08:51.600><c> but</c><00:08:51.930><c> you</c>

00:08:52.100 --> 00:08:52.110 align:start position:0%
mean these two are very similar but you
 

00:08:52.110 --> 00:08:54.319 align:start position:0%
mean these two are very similar but you
want<00:08:52.230><c> to</c><00:08:52.290><c> do</c><00:08:52.410><c> more</c><00:08:52.589><c> so</c><00:08:52.860><c> as</c><00:08:52.949><c> I</c><00:08:53.069><c> said</c><00:08:53.370><c> we</c><00:08:53.730><c> run</c><00:08:54.120><c> all</c>

00:08:54.319 --> 00:08:54.329 align:start position:0%
want to do more so as I said we run all
 

00:08:54.329 --> 00:08:55.639 align:start position:0%
want to do more so as I said we run all
the<00:08:54.449><c> tests</c><00:08:54.690><c> and</c><00:08:54.959><c> make</c><00:08:55.050><c> sure</c><00:08:55.170><c> the</c><00:08:55.290><c> whole</c><00:08:55.380><c> test</c>

00:08:55.639 --> 00:08:55.649 align:start position:0%
the tests and make sure the whole test
 

00:08:55.649 --> 00:08:59.900 align:start position:0%
the tests and make sure the whole test
passed<00:08:56.420><c> but</c><00:08:57.560><c> in</c><00:08:58.560><c> allusion</c><00:08:59.100><c> to</c><00:08:59.130><c> their</c>

00:08:59.900 --> 00:08:59.910 align:start position:0%
passed but in allusion to their
 

00:08:59.910 --> 00:09:03.350 align:start position:0%
passed but in allusion to their
was<00:09:00.360><c> the</c><00:09:00.570><c> measure</c><00:09:00.810><c> the</c><00:09:01.590><c> test</c><00:09:02.370><c> coverage</c><00:09:02.940><c> which</c>

00:09:03.350 --> 00:09:03.360 align:start position:0%
was the measure the test coverage which
 

00:09:03.360 --> 00:09:06.290 align:start position:0%
was the measure the test coverage which
means<00:09:03.690><c> that</c><00:09:03.990><c> how</c><00:09:04.830><c> many</c><00:09:05.010><c> out</c><00:09:05.130><c> for</c><00:09:05.370><c> me</c><00:09:05.820><c> how</c><00:09:06.180><c> much</c>

00:09:06.290 --> 00:09:06.300 align:start position:0%
means that how many out for me how much
 

00:09:06.300 --> 00:09:07.370 align:start position:0%
means that how many out for me how much
part<00:09:06.630><c> of</c><00:09:06.720><c> for</c><00:09:06.900><c> more</c><00:09:07.020><c> more</c><00:09:07.170><c> that</c><00:09:07.290><c> actually</c>

00:09:07.370 --> 00:09:07.380 align:start position:0%
part of for more more that actually
 

00:09:07.380 --> 00:09:09.770 align:start position:0%
part of for more more that actually
exercise<00:09:07.950><c> by</c><00:09:08.310><c> those</c><00:09:08.490><c> tests</c><00:09:08.820><c> and</c><00:09:09.120><c> you</c><00:09:09.660><c> know</c>

00:09:09.770 --> 00:09:09.780 align:start position:0%
exercise by those tests and you know
 

00:09:09.780 --> 00:09:11.540 align:start position:0%
exercise by those tests and you know
what<00:09:09.870><c> actually</c><00:09:10.170><c> your</c><00:09:10.650><c> life</c><00:09:10.860><c> we</c><00:09:11.160><c> found</c><00:09:11.400><c> it</c>

00:09:11.540 --> 00:09:11.550 align:start position:0%
what actually your life we found it
 

00:09:11.550 --> 00:09:15.100 align:start position:0%
what actually your life we found it
actually<00:09:11.640><c> to</c><00:09:11.820><c> some</c><00:09:11.970><c> test</c><00:09:12.210><c> amidst</c><00:09:12.890><c> for</c><00:09:13.890><c> example</c>

00:09:15.100 --> 00:09:15.110 align:start position:0%
actually to some test amidst for example
 

00:09:15.110 --> 00:09:18.770 align:start position:0%
actually to some test amidst for example
just<00:09:16.190><c> program</c><00:09:17.190><c> I</c><00:09:17.370><c> mean</c><00:09:17.520><c> same</c><00:09:17.820><c> thing</c><00:09:18.210><c> example</c><00:09:18.690><c> I</c>

00:09:18.770 --> 00:09:18.780 align:start position:0%
just program I mean same thing example I
 

00:09:18.780 --> 00:09:24.160 align:start position:0%
just program I mean same thing example I
sorry<00:09:19.290><c> this</c><00:09:19.560><c> one</c><00:09:21.140><c> so</c><00:09:22.140><c> that</c><00:09:22.350><c> is</c><00:09:22.590><c> Python</c>

00:09:24.160 --> 00:09:24.170 align:start position:0%
sorry this one so that is Python
 

00:09:24.170 --> 00:09:30.770 align:start position:0%
sorry this one so that is Python
coverage<00:09:25.170><c> to</c><00:09:25.740><c> report</c><00:09:26.600><c> where</c><00:09:29.030><c> you</c><00:09:30.030><c> have</c><00:09:30.600><c> this</c>

00:09:30.770 --> 00:09:30.780 align:start position:0%
coverage to report where you have this
 

00:09:30.780 --> 00:09:32.930 align:start position:0%
coverage to report where you have this
list<00:09:31.020><c> comprehension</c><00:09:31.440><c> and</c><00:09:31.920><c> then</c><00:09:32.460><c> this</c><00:09:32.640><c> this</c>

00:09:32.930 --> 00:09:32.940 align:start position:0%
list comprehension and then this this
 

00:09:32.940 --> 00:09:35.270 align:start position:0%
list comprehension and then this this
comprehension<00:09:33.390><c> can</c><00:09:33.660><c> be</c><00:09:33.870><c> I</c><00:09:34.140><c> mean</c><00:09:34.530><c> you</c><00:09:35.070><c> have</c><00:09:35.190><c> a</c>

00:09:35.270 --> 00:09:35.280 align:start position:0%
comprehension can be I mean you have a
 

00:09:35.280 --> 00:09:37.850 align:start position:0%
comprehension can be I mean you have a
full<00:09:35.580><c> wondered</c><00:09:36.510><c> person</c><00:09:36.870><c> state</c><00:09:37.200><c> coverage</c><00:09:37.740><c> if</c>

00:09:37.850 --> 00:09:37.860 align:start position:0%
full wondered person state coverage if
 

00:09:37.860 --> 00:09:40.970 align:start position:0%
full wondered person state coverage if
you've<00:09:37.980><c> only</c><00:09:38.130><c> one</c><00:09:38.640><c> single</c><00:09:39.350><c> test</c><00:09:40.350><c> because</c><00:09:40.740><c> it's</c>

00:09:40.970 --> 00:09:40.980 align:start position:0%
you've only one single test because it's
 

00:09:40.980 --> 00:09:42.970 align:start position:0%
you've only one single test because it's
single<00:09:41.160><c> line</c><00:09:41.460><c> whatever</c><00:09:42.210><c> you</c><00:09:42.360><c> have</c><00:09:42.450><c> one</c><00:09:42.600><c> test</c>

00:09:42.970 --> 00:09:42.980 align:start position:0%
single line whatever you have one test
 

00:09:42.980 --> 00:09:46.550 align:start position:0%
single line whatever you have one test
it<00:09:43.980><c> just</c><00:09:44.280><c> executed</c><00:09:44.820><c> and</c><00:09:45.000><c> you</c><00:09:45.240><c> just</c><00:09:45.450><c> it</c><00:09:46.290><c> cover</c>

00:09:46.550 --> 00:09:46.560 align:start position:0%
it just executed and you just it cover
 

00:09:46.560 --> 00:09:49.040 align:start position:0%
it just executed and you just it cover
but<00:09:47.250><c> but</c><00:09:47.520><c> but</c><00:09:47.790><c> the</c><00:09:48.030><c> things</c><00:09:48.240><c> that</c><00:09:48.510><c> this</c><00:09:48.900><c> is</c>

00:09:49.040 --> 00:09:49.050 align:start position:0%
but but but the things that this is
 

00:09:49.050 --> 00:09:50.630 align:start position:0%
but but but the things that this is
filtering<00:09:49.410><c> function</c><00:09:49.650><c> so</c><00:09:50.280><c> you</c><00:09:50.340><c> need</c><00:09:50.460><c> to</c><00:09:50.550><c> have</c>

00:09:50.630 --> 00:09:50.640 align:start position:0%
filtering function so you need to have
 

00:09:50.640 --> 00:09:52.220 align:start position:0%
filtering function so you need to have
at<00:09:50.790><c> least</c><00:09:50.910><c> few</c><00:09:51.270><c> tests</c><00:09:51.540><c> like</c><00:09:51.810><c> whether</c>

00:09:52.220 --> 00:09:52.230 align:start position:0%
at least few tests like whether
 

00:09:52.230 --> 00:09:54.350 align:start position:0%
at least few tests like whether
filtering<00:09:52.740><c> whether</c><00:09:53.370><c> is</c><00:09:53.580><c> filtering</c><00:09:53.910><c> out</c><00:09:54.090><c> I</c>

00:09:54.350 --> 00:09:54.360 align:start position:0%
filtering whether is filtering out I
 

00:09:54.360 --> 00:09:56.900 align:start position:0%
filtering whether is filtering out I
mean<00:09:54.900><c> some</c><00:09:55.440><c> every</c><00:09:56.010><c> elements</c><00:09:56.430><c> or</c><00:09:56.520><c> filtering</c>

00:09:56.900 --> 00:09:56.910 align:start position:0%
mean some every elements or filtering
 

00:09:56.910 --> 00:09:59.200 align:start position:0%
mean some every elements or filtering
out<00:09:57.000><c> in</c><00:09:57.120><c> some</c><00:09:57.330><c> other</c><00:09:57.480><c> element</c><00:09:57.840><c> or</c><00:09:57.990><c> nothing</c><00:09:58.320><c> so</c>

00:09:59.200 --> 00:09:59.210 align:start position:0%
out in some other element or nothing so
 

00:09:59.210 --> 00:10:01.490 align:start position:0%
out in some other element or nothing so
since<00:10:00.210><c> we</c><00:10:00.450><c> already</c><00:10:00.570><c> specified</c><00:10:01.080><c> that</c>

00:10:01.490 --> 00:10:01.500 align:start position:0%
since we already specified that
 

00:10:01.500 --> 00:10:05.420 align:start position:0%
since we already specified that
explicitly<00:10:02.660><c> those</c><00:10:03.660><c> iteration</c><00:10:04.200><c> we</c><00:10:05.040><c> found</c><00:10:05.250><c> that</c>

00:10:05.420 --> 00:10:05.430 align:start position:0%
explicitly those iteration we found that
 

00:10:05.430 --> 00:10:12.050 align:start position:0%
explicitly those iteration we found that
existing<00:10:05.910><c> tests</c><00:10:06.150><c> only</c><00:10:07.700><c> test</c><00:10:10.580><c> none</c><00:10:11.580><c> of</c><00:10:11.700><c> them</c><00:10:11.910><c> is</c>

00:10:12.050 --> 00:10:12.060 align:start position:0%
existing tests only test none of them is
 

00:10:12.060 --> 00:10:13.580 align:start position:0%
existing tests only test none of them is
filtered<00:10:12.360><c> out</c><00:10:12.480><c> everything</c><00:10:13.110><c> is</c><00:10:13.230><c> just</c><00:10:13.320><c> all</c>

00:10:13.580 --> 00:10:13.590 align:start position:0%
filtered out everything is just all
 

00:10:13.590 --> 00:10:15.260 align:start position:0%
filtered out everything is just all
targets<00:10:14.070><c> matched</c><00:10:14.280><c> so</c><00:10:14.670><c> we</c><00:10:14.790><c> found</c><00:10:15.030><c> that</c>

00:10:15.260 --> 00:10:15.270 align:start position:0%
targets matched so we found that
 

00:10:15.270 --> 00:10:17.930 align:start position:0%
targets matched so we found that
something<00:10:16.050><c> isn't</c><00:10:16.320><c> filtering</c><00:10:17.070><c> out</c><00:10:17.220><c> case</c><00:10:17.610><c> is</c>

00:10:17.930 --> 00:10:17.940 align:start position:0%
something isn't filtering out case is
 

00:10:17.940 --> 00:10:21.950 align:start position:0%
something isn't filtering out case is
not<00:10:19.340><c> covered</c><00:10:20.340><c> so</c><00:10:20.670><c> we</c><00:10:20.880><c> wrote</c><00:10:21.630><c> down</c><00:10:21.810><c> each</c>

00:10:21.950 --> 00:10:21.960 align:start position:0%
not covered so we wrote down each
 

00:10:21.960 --> 00:10:24.350 align:start position:0%
not covered so we wrote down each
additional<00:10:22.620><c> test</c><00:10:22.890><c> so</c><00:10:23.490><c> we</c><00:10:23.850><c> found</c><00:10:24.240><c> another</c>

00:10:24.350 --> 00:10:24.360 align:start position:0%
additional test so we found another
 

00:10:24.360 --> 00:10:27.080 align:start position:0%
additional test so we found another
similar<00:10:25.350><c> the</c><00:10:25.560><c> missing</c><00:10:25.830><c> test</c><00:10:26.070><c> and</c><00:10:26.340><c> we</c><00:10:26.640><c> propose</c>

00:10:27.080 --> 00:10:27.090 align:start position:0%
similar the missing test and we propose
 

00:10:27.090 --> 00:10:31.070 align:start position:0%
similar the missing test and we propose
and<00:10:27.360><c> write</c><00:10:28.350><c> more</c><00:10:28.860><c> tests</c><00:10:29.160><c> and</c><00:10:29.820><c> I</c><00:10:30.750><c> think</c><00:10:30.990><c> which</c>

00:10:31.070 --> 00:10:31.080 align:start position:0%
and write more tests and I think which
 

00:10:31.080 --> 00:10:33.670 align:start position:0%
and write more tests and I think which
that<00:10:31.410><c> will</c><00:10:31.620><c> be</c><00:10:31.940><c> including</c><00:10:32.940><c> the</c><00:10:33.000><c> next</c><00:10:33.240><c> release</c>

00:10:33.670 --> 00:10:33.680 align:start position:0%
that will be including the next release
 

00:10:33.680 --> 00:10:36.470 align:start position:0%
that will be including the next release
so<00:10:34.680><c> yeah</c><00:10:35.040><c> we</c><00:10:35.250><c> not</c><00:10:35.460><c> only</c><00:10:35.490><c> have</c><00:10:35.790><c> a</c><00:10:35.820><c> formal</c><00:10:36.150><c> model</c>

00:10:36.470 --> 00:10:36.480 align:start position:0%
so yeah we not only have a formal model
 

00:10:36.480 --> 00:10:39.050 align:start position:0%
so yeah we not only have a formal model
but<00:10:36.570><c> also</c><00:10:36.600><c> we</c><00:10:36.960><c> hope</c><00:10:37.670><c> improving</c><00:10:38.670><c> the</c><00:10:38.790><c> test</c>

00:10:39.050 --> 00:10:39.060 align:start position:0%
but also we hope improving the test
 

00:10:39.060 --> 00:10:45.170 align:start position:0%
but also we hope improving the test
suite<00:10:40.280><c> so</c><00:10:41.280><c> that's</c><00:10:42.210><c> what</c><00:10:43.020><c> we</c><00:10:43.230><c> have</c><00:10:43.440><c> so</c><00:10:43.680><c> far</c><00:10:44.180><c> we</c>

00:10:45.170 --> 00:10:45.180 align:start position:0%
suite so that's what we have so far we
 

00:10:45.180 --> 00:10:48.050 align:start position:0%
suite so that's what we have so far we
have<00:10:45.300><c> a</c><00:10:45.500><c> former</c><00:10:46.500><c> model</c><00:10:46.700><c> which</c><00:10:47.700><c> is</c><00:10:47.850><c> very</c>

00:10:48.050 --> 00:10:48.060 align:start position:0%
have a former model which is very
 

00:10:48.060 --> 00:10:50.630 align:start position:0%
have a former model which is very
similar<00:10:48.300><c> to</c><00:10:48.450><c> the</c><00:10:49.140><c> specification</c><00:10:50.130><c> Python</c>

00:10:50.630 --> 00:10:50.640 align:start position:0%
similar to the specification Python
 

00:10:50.640 --> 00:10:53.420 align:start position:0%
similar to the specification Python
specification<00:10:51.210><c> it</c><00:10:52.080><c> passed</c><00:10:52.680><c> all</c><00:10:52.890><c> the</c><00:10:53.010><c> tests</c>

00:10:53.420 --> 00:10:53.430 align:start position:0%
specification it passed all the tests
 

00:10:53.430 --> 00:10:54.980 align:start position:0%
specification it passed all the tests
so<00:10:53.700><c> we</c><00:10:53.760><c> have</c><00:10:53.850><c> a</c><00:10:53.910><c> very</c><00:10:54.120><c> high</c><00:10:54.300><c> confident</c><00:10:54.780><c> that</c>

00:10:54.980 --> 00:10:54.990 align:start position:0%
so we have a very high confident that
 

00:10:54.990 --> 00:10:58.610 align:start position:0%
so we have a very high confident that
that<00:10:55.940><c> captures</c><00:10:56.940><c> whatever</c><00:10:57.750><c> spec</c><00:10:58.410><c> and</c>

00:10:58.610 --> 00:10:58.620 align:start position:0%
that captures whatever spec and
 

00:10:58.620 --> 00:11:01.670 align:start position:0%
that captures whatever spec and
implementation<00:10:59.450><c> and</c><00:11:00.450><c> then</c><00:11:00.810><c> our</c><00:11:00.990><c> next</c><00:11:01.200><c> goal</c><00:11:01.470><c> as</c>

00:11:01.670 --> 00:11:01.680 align:start position:0%
implementation and then our next goal as
 

00:11:01.680 --> 00:11:04.010 align:start position:0%
implementation and then our next goal as
I<00:11:01.830><c> said</c><00:11:02.100><c> is</c><00:11:02.340><c> to</c><00:11:02.610><c> now</c><00:11:02.850><c> prove</c><00:11:03.300><c> the</c><00:11:03.570><c> safety</c><00:11:03.780><c> and</c>

00:11:04.010 --> 00:11:04.020 align:start position:0%
I said is to now prove the safety and
 

00:11:04.020 --> 00:11:07.040 align:start position:0%
I said is to now prove the safety and
lightness<00:11:04.470><c> in</c><00:11:04.740><c> that</c><00:11:05.700><c> model</c><00:11:06.210><c> and</c><00:11:06.360><c> the</c><00:11:06.750><c> monster</c>

00:11:07.040 --> 00:11:07.050 align:start position:0%
lightness in that model and the monster
 

00:11:07.050 --> 00:11:08.810 align:start position:0%
lightness in that model and the monster
have<00:11:07.140><c> dead</c><00:11:07.380><c> we</c><00:11:07.830><c> are</c><00:11:07.950><c> very</c><00:11:08.130><c> high</c><00:11:08.280><c> confident</c>

00:11:08.810 --> 00:11:08.820 align:start position:0%
have dead we are very high confident
 

00:11:08.820 --> 00:11:11.990 align:start position:0%
have dead we are very high confident
that<00:11:09.150><c> clients</c><00:11:10.080><c> are</c><00:11:10.290><c> secure</c><00:11:10.980><c> I</c><00:11:11.130><c> mean</c><00:11:11.339><c> safe</c><00:11:11.700><c> and</c>

00:11:11.990 --> 00:11:12.000 align:start position:0%
that clients are secure I mean safe and
 

00:11:12.000 --> 00:11:13.740 align:start position:0%
that clients are secure I mean safe and
life

00:11:13.740 --> 00:11:13.750 align:start position:0%
life
 

00:11:13.750 --> 00:11:17.430 align:start position:0%
life
thank<00:11:14.750><c> you</c>

00:11:17.430 --> 00:11:17.440 align:start position:0%
 
 

00:11:17.440 --> 00:11:26.540 align:start position:0%
 
[Applause]

00:11:26.540 --> 00:11:26.550 align:start position:0%
 
 

00:11:26.550 --> 00:11:28.610 align:start position:0%
 
you