[Music]
hello thank you so my name is
aov um the slides ah here the slides um
happy to be here actually this is work
done by myself uh tan hran who's also
here in the room uh EUR C Thomas P who
is also here and Roberto saltin and
we're happy to have done this work
supported by serum fun found so if you
look at consensus ethereum consensus uh
you probably see a lot of algorithms
starting as Casper Gasper now we have
single slot finality and recently on the
Block we have uh three slot finality you
can check uh the recent report uh by
Franchesco Roberto tanhai and Luca and
if you look into into these things uh
you will see that there are a lot of
definitions I cannot explain all of you
uh all these definitions to you you will
see that there are chain blocks slots uh
checkpoints Justified checkpoints
finalized checkpoints votes by
validators FFG votes uh that connect
these checkpoints and so on so forth so
these are not simple
algorithms so in our work we don't uh we
don't have uh basically time budget to
to do everything so we focus on
accountable safety which
means roughly speaking that if if you
have a fork in consensus we should be
able to identify at least oneir of the
uh validators that are
basically uh that produce this fork and
they should be slashed so we focus on
accountable safety here how would we be
able to check that these protocols uh
namely three uh three slot finality
satisfy accountable safety well in
science fiction solution when it's all
good uh we would take the code in Python
we'll take the executable spec in Python
produce some examples maybe to convince
ourselves that it kind of works but also
would we would also produce an automatic
proof of accountable safety
unfortunately that's a bit of Science
Fiction nowadays there are no of
the-shelf solutions that would take
executable python spec and reason about
such complex algorithms as
consensus so what we have been doing in
this project we actually
uh VI writing uh specifications in
temperal logic factions that's a
language invented by Les Lampard some
time ago for reason about concurrent and
distributed
systems um and we did we did produce
specifications by hand because there are
no tools that would be able to do it
although we have been thinking how we
could automate that so basically the
first specification we wrote was just
two complex for the model Checkers uh we
greatly produced obstructions using this
specification
and essentially produced like four
levels of obstructions here so the model
Checker could handle uh the complexity
of the algorithm in the end we used the
model check palache which uh is
offloading the verification task to the
smt solver Z3 and in addition to that as
things were a bit slow we also wrote a
specification in alloy which is also a
well-known model Checker that is backed
by aat solver and in addition to that we
wrote uh smt constraints
in uh CVC 5 using the theory of finite
sets and cardinalities so we kind of did
a lot of experiments here to check
accountable safety on the different uh
using different
tools so as I told you model checking uh
could help you how can it help you the
first thing where it can help you is
actually you can qu for interest in
States if you have a large protocol it's
not easy to produce examples and that's
what model checking is good about for
instance here I'm just writing an
invariant saying there are no two
conflicting blocks basically there is no
fork and challenge the model Checker
with this false invariant then the model
Checker comes back in several minutes
and shows me an example so actually
these tools uh work uh as a good
communication tool for protocol
designers he is an example of such an
execution you don't have to read it it's
just laan but it's machine readable and
it's an actual execution in in this
specification so the second thing where
this tools can help you is to show some
properties uh not for all kinds of uh
values but for small scopes for small
parameters for instance here we have
experiments for five blocks seven
checkpoints 24 vots and as you can see
when we increase the parameter space the
tools uh slow down
dramatically however we have some
evidence uh that these properties hold
true at least for the small parameters
and that's again fast feedback that you
can get without proven things in heavy
tools so to come to the summary of of
our work we believe that mche can
actually helps in ensuring correctness
of protocols uh we still need humans in
the loops unfortunately we still need us
basically to construct this abstractions
and
specifications uh tune in for the
upcoming technical report we are going
to publish all of it and you'll see it
and thank you eum foundation for giving
us a grant thanks a lot
thank you
Igor does anybody have any
question okay
okay I think it was very clear nobody
has any re
you have to quick and come back again
at
okay okay if there are no more questions
just thank you for thank
you we will