you
hello hello oh thank you very much it is
an honor to be here and I have a part of
me I have to second yo yo chewy your
shoe ease statement that this is a dream
for a formal verification engineer I
mean the amount of interest in the room
in this beautiful field that those of us
who have you know devoted a lot of our
professional and you say personal lives
too it's amazing to see so much
enthusiasm so I feel very fortunate to
be a part of this group we're such great
work and awareness is happening around
formal verification static analysis and
so on so I'm very excited today to
launch our a mantra contracts platform
which is formal verification in the
cloud for smart contracts initially
targeted for etherium so what powers a
mantra contracts is our formal
verification engine that will talk to
you about call Timandra but what we've
done is we've taken the etherium virtual
machine and formalized it within a
mantra given a full bit precise
operational semantics to the instruction
set of the etherium virtual machine and
then from that we're able to build a
stack of tools that work at many
different levels powered by techniques
such as symbolic execution something
called principal region decomposition
and ultimately both automated an
interactive proof so I'll walk you
through many details show some examples
and then I hope we can do lots of demos
because there isn't that much time but
please find me if you're interested in
sign up so before I get started I want
to show a two minute video that give
some background on what we do at
aesthetic integration and really how we
got here so now I will hand over to
Hudson because I think he has to man the
sound thank you
what's plaguing today's electronic
financial markets the world economy is
built on a staggeringly complex tangle
of algorithms competitive pressures and
economic recession have contributed to
increasingly opaque and unstable markets
the effects of glitches and unfair
advantages can be devastating cratering
the confidence of investors and
ultimately hurting the general public
regulators and the industry have worked
tirelessly to define what safe and fair
markets are what's been missing is a way
to analyze and regulate all of the
algorithms underlying the solution is
formal verification the science of
correct algorithms other safety critical
industries already rely on formal
verification to make their algorithms
say the mandra by aesthetic integration
is the world's first formal verification
solution for financial markets consider
the building of a bridge a design flaw
may be catastrophic to make it safe
engineers use powerful computer aided
design tools which analyze designs for
safety automatically
powered by latest advances in artificial
intelligence computer science and
mathematics a mantra brings
unprecedented rigor to the electronic
financial markets analyzing the safety
and fairness of algorithms before
they're deployed financial algorithms
are unfathomably complex they can be in
a virtually infinite number of possible
states examining 100 1000 were even
100,000 test cases isn't enough we must
consider every possible case to answer
definitively what can possibly go wrong
a mandra allows designers and regulators
to fix breaches of safety and fairness
before they affect markets let's build
safer more reliable and regulatory
compliance systems that all of us can
trust saving everyone time and money a
mandra by aesthetic integration the
logic of financial risk alright thank
you very much so just a bit of
background we are aesthetic integration
and our work before etherium and you
know also worth that continues
vehemently has mostly been with
financial algorithms like dark pools
matching logics exchange matching logics
connectivity layers for instance between
venues and different trading systems so
we have worked with a number of top
investment banks on formally verifying
regulatory properties of their core
infrastructure algorithms last year
after DEFCON 1 something very exciting
that has really been a huge catalyst for
us in growth is we won something called
the UBS future of Finance challenge so
this was a global competition between
620 companies 52 countries and we ended
up winning the whole thing and I think a
major reason was we took the design of
UBS is dark pool and actually analyzed
it for regulatory properties showed how
certain issues that were settled with
the SEC could be found automatically
and many related things so also at the
sort of middle of the summer a little
bit before we finished what is to our
knowledge as the world's first formally
verified dark pool design for a major
investment bank where we of course in
the process fixing many aspects of their
system were able to prove 114 fairness
and safety properties ultimately about
their collection of order types and we
recently closed our seed round backed by
Google's chief business officer Philip
Schindler which is leading to some very
exciting things of getting formal
verification out to the masses and
democratizing this technology that has
up to now been quite arcane in many ways
so my co-founder Dennis he was head of
the central risk trading desk at
deutsche before we founded a I and my
background so I did my PhD in formal
verification at Edinboro a lot of what I
did was around something called an smt
solver called said three so I
co-authored a lot of the core
mathematics of Zed three nonlinear
decision procedures and then went down
to Cambridge as a postdoc working on
safety and fairness of collision
avoidance algorithms and then we
realized we could apply many of these
same techniques to financial algorithms
so we all know the problems that are
motivating formal verification being
taken up in our community so I don't
need to belabor those but there are some
other aspects that haven't been
mentioned at least that I've seen and in
addition to the need for automated
auditing tools around correctness
fairness and safety of course mitigating
subtle bugs and so on we also need
fundamentally robust tools for risk
management so I'm talking here for you
know those of you at an investment
banking where you have exposure you know
imagine an investment bank goes all-in
on etherium and five years from now has
a hundred thousand smart contracts in a
portfolio what is their exposure how do
you calculate risk how do you price for
instance derivatives and structured
products that are expressed as
ultimately athyrium by code and that's
another place where we see formal
verification as being utterly crucial so
some of the things we're building on top
of our formalized EDM
in a mantra are around exactly this risk
management calculating Greeks and market
exposure linked directly to the
semantics of the bytecode so mandra
leverages a number of recent
breakthroughs in formal verification smt
which is powerful automated proof
techniques combining SAT solvers what
really powers formal verification for
hardware combining those techniques with
richer mathematical theories things like
reasoning about arrays and bit vectors
and nonlinear and linear inequalities
and so on model-based automated
induction plays a huge role so when you
have algorithms that ultimately iterate
or you know when it when expressed in a
logic may be expressed as recursion you
typically need to prove theorems by
induction either by techniques like you
know writing out inductive invariants as
we saw with the work of Christian and
your Chewie with y3 or with proving
inductive limos that then get used for
instance as rewrite rules these are all
bread and butter for formal verification
but we now have much more powerful tools
for for instance using counter examples
to help us guide the way we inductively
generalize which is something you often
need to do when proving theorems by
induction but fundamentally what we're
doing with the Amanda cloud is aiming to
really democratize access to these
techniques and make them usable to
developers and non developers alike we
all need them and need them to be easy
so fundamentally you give a mantra to
things a smart contract let's say
expressed as a theory and byte code for
instance and a property you wish to
verify and a mantra will work to either
give you a proof of that property or
work to show you a counter example where
a property fails and then there's I'll
show you many ways that you can get
involved in that process and
interactively work with the mantra so a
mantra is a programming language a
mathematical logic and a reasoning
engine all in one it's a formalized
subset of a functional language called o
camel crucially when designing a mantra
you know we set out to design our dream
formal verification system and one of
the most important things is having
first-class counter exam
so in a mantra we're always working to
find counter-examples to false
conjectures and actually reflect those
into the runtime and into the logic so
that you can compute with them which is
which is really crucial so there's see I
really don't have much time so I want to
just show you probably impossible to
read but this is a little bit of a walk
through of our formalized to theorem
virtual machine and a mantra and the way
you formalize this because a mantra is
logic is also an executable programming
language you actually just feel like
you're writing a simulator for the
virtual machine writing an interpreter
defining precisely the memory model the
storage model all of the instructions
and how those operate on the state and
then ultimately there's a top-level
state transition function and then
finally that's iterated right until you
run out of gas or reach an exceptional
halting state or you halt in a nice way
so in a mantra by the way we are
releasing our EVM model under a patchy 2
point 0 and so our hope is that the
community will manage this port it to
other systems and it can be something
that evolves as the you know design of
etherium evolves but what I'm showing
you here now this is a very very low
level interface but I've loaded into a
mantra the model of the etherium virtual
machine I've also loaded in some
bytecode those are now in the runtime
those of you who know o camel will see
that this looks just like you're at a no
camel top-level read eval print loop but
actually everything you write in this
language is also reflected into
mathematics and you can then reason
about it so I'm now asking a mantra here
to decompose the state space of
effectively the virtual machine
interpreter running that piece of byte
code and what's this what this is doing
it's ultimately using something called
symbolic execution under the hood but
it's telling me the possible behaviors
of this piece of bytecode with respect
to the actual semantics of the
instructions so this tells me that
actually this piece of byte code which
is for a simple name registry it only
has two possible behaviors with respect
to arbitrary symbolic storage and one
behavior it would go tour execute at
program
counter 17 if it doesn't run out of gas
and it would update the storage in the
other behavior it's I believe would halt
you just told me it would halt at eight
and would not update the storage for
instance so now I'm actually let me see
if I could pause this for a second and
we have two minutes you can't read it
unfortunately but these are theorem
statements about the execution of this
bytecode so these are the formal specs
of how this name registry should work
and we're asking a mantra to prove those
for us and it does which is great
directly about the meaning of the
bytecode so not at a higher level but
really at the actual byte code that will
be executed on the EVM and now we're
asking it to prove some things that have
mistakes and what happens is in this
case we can ask him andhra to show us
where it's proof attempt failed and then
we can ask a mantra to also mine that
for counter examples but these are very
useful for understanding these what we
call sub goals for understanding why
something isn't true so I don't have
time to go through this this is a higher
level so we have a higher level language
that is a subset of Madra subset of o
camel that we can compile to the EVM and
so one of the things we're working on is
proving the correctness of that compiler
with respect to the EVM semantics so
hopefully we'll finish that by the end
of the year but I wanted to show you
these region decompositions like I did
of the possible behaviors of that piece
of by code we can scale this to you know
very complex algorithms so this is smart
contract encoding effectively the
matching logic pricing function for an
exchange and we asked Timandra to
decompose it state space it told us
there's actually only 107 different
possible behaviors and now I can go
through and we have this hierarchical
tree representation as a Peroni diagram
that's interactive you can go and
experiment and see what are the
different symbolic behaviors of this
function with a map to its state space
and we're getting on the right you can't
read them unfortunately but constraints
on the input that would cause a certain
output and these are all expressed
symbolically and so now we know even
though this has an infinite state space
the system itself only has 107 possible
symbolic behaviors so we have a new
website that launches today you can go
to its wwm Andre I and it is if you
click on image or contracts you can sign
up and we're adding a certain number of
people each week as we scale up but
effectively it's a mandra now in the
cloud running in google cloud with
something called codenvy which uses
eclipse che and number of things to spin
up docker containers for you and have a
mantra so I see I'm out of time but
anyways we are building the stack also
with a smart contract auditing API and
finally thanks to our incredible team
and I hope all of you will get involved
and the community can can really make
use of the mantra and join us at a
Monterey I thank you thank you now Oh