well thank you very much it's a pleasure
to be here and grant passmore in my
co-founder dennis ignite ovitch here in
the audience thank you to a italic for
the invitation so we're going to talk to
you today about our formal verification
platform and mandra and a particular
something we're calling a mantra
contracts which is the application of a
mantra to etherium smart contracts both
to analyze smart contracts reason about
them be able to prove properties of them
compute proofs and counter examples and
then on top of that to actually do risk
management so I'll tell you what I mean
but for those and investment banking we
mean you no compute Greeks and so on so
let me start with a video that gives you
a background on what we're doing at
aesthetic integration see if the sound
I'll start it over here we go
yes thought was the best of an issue
Paris
I made it
alright so that gave you a bit of an
overview of what we're doing at
aesthetic integration the big idea is
we're bringing the hard science of
formal verification techniques that are
relied upon already in safety-critical
industries like avionics and hardware
design finally to finance so that
financial algorithms things like dark
pool matching logics exchange matching
logics market making algorithm smart
order routers the type of algorithm that
is really at the heart of our global
financial infrastructure so that they
can actually be analyzed rigorously and
reasoned about so a bit of our
background so Dennis formerly was the
head of the central risk trading desk at
Deutsche roughly I believe nine years at
Deutsche by the way we were undergrad
roommates in Texas and then as Dennis
went to Wall Street I went to academia
did my PhD in formal verification in
particular the real loud to break
geometry for reasoning about autopilot
algorithms and being able to prove
safety properties of autopilot
algorithms in avionics in now and
self-driving cars and ended up as a
postdoc at Cambridge well Dennis was
working at Deutsche and we realized we
were working in many ways on some of the
same problems he had very complex
trading algorithms that constantly
everyone was worried you know if we
commit a line of code is this change all
of a sudden going to cause us to violate
a regulation and it's very hard to get
right if you think of modern market
microstructure something like in
exchange trading than you in the US for
instance it may have upwards of 20 30 40
different order types in each of those
order types effectively it's a way of
packaging risk it's a programming
language and as you introduce new order
types it's very difficult by hand to
understand what can possibly go wrong
so when it comes to smart contracts
really we have the same issues so if i
come to you and say look I promise you
know this piece of bytecode really
implements fair escrow please send me
your assets how do you know likewise if
I say I promise this implements a swap
that we've agreed upon how do you know
you can't ultimately trust the result or
the design of a given smart contract
without reasoning about it without
proving theorems about it's possible
behavior so what we've done is we've
taken our mantra engine which I'll tell
you about for reasoning about financial
algorithms and now we've adapted it in
effectively two different ways i'll tell
you about one that's reasoning about a
high-level language that can be compiled
down to a theorem bytecode and the other
that effectively is doing something
called verified d compilation that takes
etherium bytecode d compiles it to IML
or high-level functional language that's
actually a formalized subset of o camel
if you know camel allows you to reason
about it and push the proofs back down
to be proofs about bytecode so okay
that's reasoning about individual
contracts but as I mentioned fundamental
importance as you know a bank who's a
pioneer right now with let's say
athyrium is there looking down the road
three years from now what happens when
they have a portfolio of 100,000 smart
contracts right you have to do risk
management in the large you have to
compute Greeks and to do that you have
to reason about the code so you must
have effectively formal semantics that
ultimately is mechanized for reasoning
about your smart contracts so let me
tell you a bit about how a mantra is
used currently so our biggest focus has
been something we call a mantra venues
and this is using a mantra to formally
analyze the matching logics behind
trading venues things like stock
exchanges and dark pools so you may have
heard about many glitches in the past
few years for instance bats failed
trading its own IPO of course famous
Nasdaq Nasdaq glitch with Facebook night
capital goldman sachs alphabet trading
glitch these
happen all the time and finance and
fundamentally what's been missing is a
way to reason about the algorithms in
advance of their deployment so a mantra
venues is now currently get use at top
five global investment banks effectively
to take what is classically an
imprecisely described algorithm their
collection of matching logic that is
usually described say in some collection
of PDFs you know there there is
classically no formal spec of how these
things are supposed to work but it's
actually taking those ambiguous sort of
in precise specs making them precise in
a mantra reasoning about fairness and
safety properties and then using a
mantra to vet their high-performance
production systems to ensure that the
production systems really correspond to
verified specifications so there's also
some exciting developments we have in
the regulatory space so just to say we
came out of stealth mode with this an
april and the sec brought us to
washington DC to the sec headquarters to
teach them about a mantra for two days
and some exciting developments will be
announced soon on a mantra in the
regulatory space but fundamentally
regulators face the same issues someone
comes to them and says I'd like to add
this new order type to my trading venue
ensure for me that you know this is
allowed and the SEC then has to process
these things and you know so so does the
FCA and other global regulators and it's
virtually impossible to do by hand
without formal verification so what is a
mantra I'm going to give you very
low-level demos of a mantra this is a
very technical audience so i want you to
see really in action and i want to talk
to you a bit about the automated
reasoning and mathematical logic that's
under the hood but fundamentally it's
three things in one it's a programming
language so it's a formalized subset of
o camel if you're familiar with o camel
in the ml family of languages functional
language it's a mathematical logic so
fundamentally every data type definition
or every program they
to find every function you define in a
mantra is automatically transformed into
an axiomatic representation that then a
mantras reasoning engine reasons about
so you write code and questions that you
would like to ask a mantra about your
code in a mantra works to produce proofs
or counter examples using many different
types of decision procedures and I'll
talk to you more about them so that's
the big idea what I just outlined
effectively you give a mantra your
financial algorithm or your smart
contract and ask them onto a question
you know is there a potential glitch of
this class or does this do some concrete
form of unfair trading for instance is
there some sequence of messages that
could be sent to this trading venue that
could allow someone to jump the queue
right and ultimately you get out either
that the algorithm is verified with a
mathematical proof that can be
independently vetted or you get a
counter example so that's that's the big
idea pushing pushing these questions
into what are called decidable fragments
so that this is automatic so let me show
you a very simple example here we have
on the left if you can read it a
summation function just in a mantra so
you may this is just summing up the
numbers from 0 to n the natural numbers
and it's a program so on the right we're
just computing with it right we can
compute some 5 some of 100 but you may
remember this possibly apocryphal story
of Gauss's a six-year-old proving
actually that the sum of in you know
some of 0 up to n is equal to n times n
plus 1 over 2 so we can not only define
programs but we can write verification
goals and what we've done here is we've
asked Timandra tactical part of me to
actually verify this statement on the
left to verify we named it Gauss we
asked amarjit to prove for every
possible input in if n is greater than
or equal to 0 then the sum of n is n
times n plus 1 over 2 so Ahmad rhythm
goes and does a proof by induction and
etc we can see a trace of that proof
great proof by induction as you might do
by hand and ultimately has to do some
symbolic rewriting
that proof can be exported can be
verified by an open source proof checker
so you don't have to trust it but now
what happens more often of course is we
have bugs in our code so instead here
I've swapped a plus for a minus right
and I'm asking a mantra instead to prove
that some event is equal to something
really that it's not equal to and a
mantra comes back and gives me a counter
example so that's a super simple example
but let me show you something more
complex so I believe I don't have too
much time but for instance here's an
example where I'm effectively defining
algebraic data types and I'm asking a
moderate to compute some complex counter
examples for me and again you know it
comes back and always the counter
examples it gives me those are valid IML
they're valid o camel objects they can
be reflected into the language and
computed with so the same idea now can
actually be scaled to reason about
financial algorithms so for instance we
can take the design of a dark pool which
I have on the left here fairly complex
matching logic this is of a global
investment bank top five investment
banks dark pool and now we can reason
about it so by the way this is all based
on publicly available information don't
worry so now for a sense i can ask a
mantra yeah is the order ranking
function transitive right so that's
something we really care about a
fairness property so i can ask them on
through this question it has a model of
the matching logic on the right that's
also a high-performance simulator and a
mantra comes back and synthesizes for me
a counter example so now i have concrete
values of different orders effectively
that could exist in the book of this
dark pool where the ranking function
violates transitivity so that's the main
idea proofs and counter examples so let
me quickly cut to the chase for athyrium
so what we've done here is we've taken a
mantra and we've adapted it so that in
IML in this fragment of o campbell you
can directly write smart contracts so
there's many things to talk to you about
how we actually do the compilation so
right now we actually compile
effectively your customized smart
contract code via serpent we compile it
first to serpent and we have different
encoding mechanisms for how we encode
algebraic data types recursively but now
we have this smart contract let's say
for a crowdfunding example and now we
can ask a monitor to reason about it so
for instance we just had a mantra prove
that in this smart contract you
effectively can't jump the queue in a
certain sense and then we ask another
question effectively that we will always
get our money back if we come in after a
certain time out and a modular computes
for us a counter example where that
fails so that's the big idea I think I
need to end here but we have these
different modes effectively you can go
IML directly to bytecode by a serpent
reason about your IML or we can use our
etherium to IML verified decompiler so
sign up please if you'd like to join the
private alpha and thank you very much
okay okay oh ok well that's okay I mean
if there's any questions okay yes so are
you saying we can write smart contracts
in oh come in I exactly in IML so I ml
it's not all evoke camel but it's you
know polymorphic hemming milner fragment
of o camel for instance it doesn't
support exceptions so that's a that's a
fundamental difference but instead of
exceptions you use you know things like
option types yeah but yes that is pretty
awesome oh thank you but part of me it's
not it's not so effectively we have a
reasoning as a service API we have an
online web interface and we have an open
source proof checker so you can always
you don't have to trust the proofs the
hard part is finding the proofs you know
the easy part is checking the proofs so
currently it's not open source though
I'm sure we'll open source pieces of it
over time
do you mean use a mantra to reason about
a mantra yeah yeah it's a great question
so there's there's you know sort of
architecture of a mantra there's some
bootstrapping in a mantra that is not
written in a mantra that's written in
let's say raw Oh camel see but then most
of a mantra actually is written in a
mantra after this bootstrapping so we've
actually done some self verifications I
mean you know you always have these
fundamental meta mathematical results
that if you want to prove ultimately
consistency of your own system you
effectively need to add you know
something like trans finite induction up
to a larger ordinal so actually a mantra
is logic it's related to a logic called
primitive recursive arithmetic of Scala
but it's typed and but then we have
transplant out induction up to an
ordinal called epsilon zero so basically
that means we can you know synthesized
in do termination proofs of functions
that you know effectively recurse in
some complex ways but so what you would
have to do because we already have that
strong ordinal in the logic you'd have
to add a transaction principle up to a
bigger ordinal but you can you know so
proof theorists have have isolated
effectively the ordinal analysis of
theories like this so you could do it
and actually try to prove soundness
properties of a mandra as a whole but
one of our really driving philosophies
has been we always just want our proofs
to be independently checkable as well so
when we produce a proof object
ultimately you can use a simple checker
to check that proof object or if we
produce a counter example it's an
explicit you know value of a given type
that you can run your system on so in
either case you don't have to trust us
but we have a lot of ideas where you
know we would love to talk to members of
the community who are interested a lot
of ideas of effectively attaching this
type of evidence directly to smart
contracts different ways that we can you
know actually have an API where you can
easily query what is known about this
contract what's been proved about it
what's been disproved also you know
there are times you need to prove limos
before a mantra will you know actually
prove your main theorem
you know happens all the time for let's
say you know very deep properties and
there we imagined you could have you
know sort of bounties where you want to
give someone you know some some number
of credits if they prove this limo for
you that you relied upon so there's lots
of cool things I think we can do
community wise flash crashes are either
generated by fat fingers or like
downward spirals we're algorithms are
forced to sell because other algorithms
are selling and so you just get this
very very quick negative spiral down
like how Adam Andhra help in either of
those two cases oh great question I mean
fundamentally there's a number of
answers so if you look at what has
happened so first of all flash crashes
happen a lot more often than you know we
hear about in the press right these
happened at a micro level happened at a
micro level it is not uncommon and a lot
of work has been done effectively having
things like risk specialized risk gates
specialized circuit breakers that are
effectively you know trying to act as an
arbiter to make sure that things don't
get out of control so first in some of
our clients now the first thing they
actually do is they use a mantra to
reason about their risk a component
before they go in reason let's say they
have an order router before they start
to reason about best execution of their
routing they may use a mantra first to
prove that their risk a component which
is just this last piece that that it
effectively won't let something crazy
out the door so you can effectively
incrementally verify the circuit
breakers these risks gates get those
safe first and then start to verify more
pieces that are you know more
algorithmically interesting so did that
answer your question okay thank you very
much
thank you