►
Description
Visit the https://archive.devcon.org/ to gain access to the entire library of Devcon talks with the ease of filtering, playlists, personalized suggestions, decentralized access on Swarm, IPFS and more.
https://archive.devcon.org/archive/watch/6/formal-methods-for-the-working-defi-dev/
Lecture notes: https://bit.ly/3RFwvBx
Runtime Verification is known for formal methods, but you don't need a PhD to make your code better by thinking like a prover. Here we want to show you how you as a developer or auditor can apply fairly simple mathematical thinking to make your code more robust and your security work simpler. By thinking “invariants first” you can get stronger tests, better docs, and reduce the risk of introducing bugs in your future coding.
Speaker(s): Rikard Hjort
Track: Security
Keywords: formal methods,invariants,mathematical thinking
Follow us: https://twitter.com/efdevcon, https://twitter.com/ethereum
Learn more about devcon: https://www.devcon.org/
Learn more about ethereum: https://ethereum.org/
Devcon is the Ethereum conference for developers, researchers, thinkers, and makers.
Devcon 6 was held in Bogotá, Colombia on Oct 11 - 14, 2022.
Devcon is organized and presented by the Ethereum Foundation, with the support of our sponsors. To find out more, please visit https://ethereum.foundation/
A
A
A
A
A
pointer
I
do
these
things
I'm
not
going
to
talk
about,
because
I
hope
dearly
that
if
you
hire
an
auditing
company,
you
have
good
tests,
they
run
they
pass.
You
have
integration
tests,
you
got
documentation
and
you
make
sure
that
your
devs
are
available
for
the
couple
of
weeks
that
you're
going
to
spend
on
an
audit
if,
in
case
a
question
comes
up,
those
are
the
basics
but
I
know
a
lot
of
teams
are
really
really
highly
skilled
and
they're
very
motivated,
and
they
want
to
do
more
if
they
can
so
well.
A
What
can
you
do?
What's?
What's
the
secret
sauce
to
getting
a
good
audit?
Actually,
what's
the
secret
sauce
of
the
Auditors
Auditors?
Like
us
different
noted
companies
do
different
things,
but
we
have
our
own
little
method
of
working
which
I'm
going
to
share
with
you
invariance
we
like
something
called
invariance.
Sometimes
you
call
them
Properties
or
property-based
tests,
or
whatever
your
favorite
equations
over
State
I,
usually
just
use
the
word
invariance
for
everything
they
help.
A
You
find
more
bugs
right,
better
docs
trust,
your
code
more,
they
help
Auditors
because
you
know
as
Auditors,
especially
we
we're
going
to
be
looking
at
invariants
and
trying
to
find
more
of
our
like
invariants
of
our
own.
Basically,
so
if
you
come
with
a
little
set
of
these,
that
you've
already
gone
over,
you've
done
some
of
our
work
for
us
and
we
can
focus
on
like
either
deeper
work
or
we
can
work
more
efficiently
and
get
you
done
faster.
A
So
we
want
you
to
come
up
with
invariants
if
you're
on
chain
code,
they're,
also
good
fuss
targets
we're
going
to
get
to
that.
They
also
one
thing
we
found
especially
developers.
They
can
tell
you
exactly
like.
Oh
you
have
to
go
to
this
function
and
this
function.
You
will
see
exactly
where
this
variable
get
updated
and
everything,
and
once
you
start
talking
about
invariants-
and
we
say
things
like
well,
just
a
sum
of
all
balances
always
match
the
total
balance
and
so
on.
A
A
A
If
that's
your,
that's
something
you
want
to
do
and
if
you
have
code
working
right
now,
if
you
have
a
laptop
up
like
you,
can
bring
up
your
own
code,
go
over
your
own
code
link
because
I'll
be
explaining
how
to
come
up
with
invariance.
If
something
comes
to
mind-
and
you
want
to
write
that
down,
please
do
that.
I'll
be
working
over
an
example
from
an
audit
we
did
a
while
ago.
A
So
if
you
don't
have
any
code
you're
working
on
right
now
or
you
just
want
to
follow,
follow
through
now
and
then
go
out
and
start
working
on
variants
on
your
own
after
this
session,
that's
fine,
too
I'll.
Also
it's
a
lot
to
cover
an
hour,
isn't
really
enough!
Anyone
here
interested,
we
can
just
just
grab
a
table,
I'm
happy
to
take
anyone
from
this
crowd
anywhere
and
just
keep
going
with
the
workshop.
A
I,
like
this
a
bit
too
much,
it
feels
almost
pathological
but
I
love
when
developers
come
up
with
invariants,
so
testing
versus
invariance
testing
is
I.
Guess
I
didn't
see
the
the
previous
talk,
but
I
think
he
was
talking
about
how
to
do
better
tests,
Tesla
sort
of
like
the
camping
knife.
It's
like.
If
you
know
what
you're
doing
you
can
use
it
for
almost
everything
and
you'll
get
out
of
most
things
by
just
doing
a
bunch
of
testing.
It's
our
first
and
most
robust
line
of
defense.
A
A
I
assume
you
do
unit
test
that
you
do
integration
tests,
you
try
deploying
on
test
Nets
and
so
on,
and
my
analogy
for
tests
is
sort
of
like
an
experiment,
right
you're,
trying
a
single
thing
you're
going
to
see
what
happens
if
I
do
exactly
this
call
or
I
do
this
little
sequence
of
calls
it's
great
and
we
often
like
especially
test
driven
developers
like
to
talk
about
testing.
As
you
know,
some
sort
of
silver
bullet,
or
even
if
they
say
it's
not,
then
you
can
kind
of
feel
like.
A
A
A
The
thing
is:
there's
very
few
resources
about
this
I
had
one
five
minute
talk
by
my
professor
when
I
started
college,
saying
like
here's,
how
I
run
over
code
in
my
head
and
I
think
that's
that's
the
end
of
it,
and
it
feels
like
reasoning
about
code
is
something
you
learned
from
experience.
It's
something
we're
always
doing
when
we're
debugging
doing
code
review,
doing
design
discussions,
we're
kind
of
like
simulating
things
in
our
head,
but
there's
not
much
resources
about
it.
No
one's
really
teaching
you
how
to
do
it.
A
A
This
is
meant
to
either
intimidate
you
or
titillate
you,
depending
on
what
your,
what
kind
of
person
you
are,
but
we're
doing
something:
that's
sort
of
analogous
to
math
proofs.
So
in
math
you
were
taught
both
like
Computing
answers,
like
figuring
something
specific
out,
but
also
how
to
do
proofs
how
to
make
sure
that
the
algorithm
that
I'm
doing
is
always
going
to
work
again.
A
It's
sort
of
like
the
analogy,
testing
versus
reasoning,
experiment
versus
Theory
reasoning
about
code
is
analogous,
but
proofs
before
anyone
say:
Curry
Howard,
like
I'm,
not
talking
about
something
like
that.
If
you're,
a
theoretical
computer
scientist
I'm
talking
about
something
very
straightforward,
that
I
think
anyone
who
has
taken
a
basic
code
boot
camp
should
be
able
to
do
and
just
like
proving,
there's
a
method.
There's
a
bit
of
artistry.
It's
not
always
straightforward.
I
can't
guarantee
you
that
your
proofs
will
work.
A
Even
if
your
theory
is
correct,
but
there's
a
structure
to
it,
you
don't
have
to
just
be
flailing
around
trying
to
prove
random
stuff,
and
with
that
we
get
to
the
actual
invariance.
What
is
an
invariant?
What
are
we
looking
for
and
what
are
we
trying
to
do
so?
This
is
very
small,
so
one
way
to
think
of
a
good
invariant,
it's
something
that
it's
obvious,
that
the
code
is
doing
or
should
be
doing
but
like
if
it
works
correctly.
A
A
Ideally,
it's
really
something
really
high
level
like
aliveness,
like
a
liveness
claim
that
you
know
this
contract
can
never
get
stuck
and
so
on,
but
to
be
completely
honest,
starting
with
really
simple.
Invariants
will
get
you
quite
far
most
of
the
time
and
we'll
do
a
very
simple
invariant
here
today
and
I
can
tell
you
from
experience
that
even
those
really
simple
invariants
that
aren't
like
super
high
level
claim
that
the
entire
protocol
is
perfectly
secure.
A
A
You
can
think
of
what's
the
code
behind
the
code,
because
the
code
is
very
exact,
it's
imperative
it
tells
the
computer
or,
like
the
evm,
exactly
how
to
do
every
little
step.
So
it's
not
it's
it's
imperative,
not
declarative
is
one
way
to
say
it
and
here's
your
chance
to
be
declarative.
You
say
something
like
you
know:
here's
the
equation
that
should
always
hold
I,
think
any
ERC
erc20
contract
should
have
this
property
right.
A
You
keep
track
of
the
total
balance,
you're
minting,
you're,
burning,
you're
transferring
and
we
just
kind
of
assume
or
like
we
hope,
or
we
might
be
very,
very
confident
that
the
total
balance
is
going
to
be
the
same
as
the
balances
in
each
individual
account
that
has
interacted
with
the
mapping
of
balances.
So
this
is
just
a
way
to
say,
take
all
the
balances
in
the
mapping
and
sum
them
up.
A
If
someone
knows
way
too
much
about
the
evm
like
I,
do
then
just
think
of
us
every
every
time
you
wrote
directly
into
a
mapping.
Technically,
the
mapping
contains
a
bunch
of
other
stuff,
but
don't
worry
about
that
and
again,
a
gradient
variant
is
something
that's
obvious
from
the
intended
business
logic
like
this,
like,
of
course,
you
know
the
total
balance
should
be
just
all
the
actual
balances
that
are
out
there,
but
it's
not
necessarily
obvious
from
the
code.
C
A
A
working
example,
if
you
want
to,
if
you
don't
have
any
code
of
your
own,
you
want
to
pull
up
and
follow
along
on
your
laptop.
You
can
go
to
GitHub
alchemics
Finance,
V2,
Foundry
repo.
It
should
be
pinned
at
the
top
we're
working
at
the
contract
Alchemist,
so
we're
going
to
be
like
Ctrl
fing
through
a
little
bit
of
it.
A
If
you
want
to
follow
along
properly
or
you
can
just
watch
the
slides
really
quickly,
this
is
sort
of
a
slightly
more
involved
version
of
the
the
sum
of
all
balances,
total
balance
invariant.
They
have
something
called
shares
that
they're
used
to
that.
They
use
to
make
sure
that
you
get
your.
You
know
your
your
yield
in
proportion
to
how
much
you
have
staked
essentially
and
then
for
every
specific
yield
token.
There
exists
a
total
shares,
valuable,
so
slightly
more
involved
than
this.
The
sum
of
all
balance.
A
This
is
total
total
balance,
invariant.
Here's
how
you
frame
it
as
the
mathematical
equation.
If
you
go
into
the
mapping
of
all
yield
tokens
where
that
contains
the
token
address
as
a
key
and
a
set
of
params,
that's
this
you'll
took
in
params.
If
you
go
into
param's
total
shares
that
should
be
equal
to
the
sum
over
all
the
accounts,
this
value
of
each
account.
A
That's
just
one
invariant
we
come
up
with.
We
proved
it
turned
out
helpful,
I'm,
not
sure
if
we
actually
find
any
found
any
bug
on
that
one.
But
you
know
we
do
find
bugs
on
those
kinds
of
things
quite
often,
but
the
question
is
like
so,
if
you're
sitting
here
with
your
own
code,
for
example,
or
you're
watching
this
later,
are
you
thinking
about
your
own
code?
How
do
you
come
up
with
good
invariants?
A
A
Second,
one
is
go
over
storage
variables.
Do
you
have
do
they
have
like
obvious
relationships?
This
was
a
good
example.
You
have
the
balances
you
have
the
total
balances,
of
course,
that
should
just
stick
out
as
a
sore
thumb
like
that's
these.
These
two
things
should
have
a
very
tight
relationship
between
them.
A
De-Optimizing
is
always
fun
like
you're
doing
a
lot
of
optimizations,
even
if
you're
not
doing
even
if
you're,
not
a
big
Optimizer
you're,
not
iterating
over
all
the
accounts
of
all
your
users,
for
example,
that's
the
sort
of
optimizations
as
solidity
developers
we
need
to
optimize,
but
what,
if
you
just
think,
I
don't
have
to
optimize
at
all?
You
write
the
code
as
you
would
in
a
dumb
Java
program,
and
then
you
just
State
the
invariant
say
like
well
this.
This
naive
implementation
and
this
optimize
implementation
are
identical.
A
A
These
these
two
variables
should
have
a
relationship
to
each
other
that
might
not
have
been
carried
over
to
your
code
comments,
those
things
you
should
go
to
invariants
and
you
can
also
work
from
unit
tests
like
replace
some
unit
test
values
and
start
thinking
about
what,
if
we
start
fussing
it,
what
if
we
use
symbolic
values,
what
properties
would
they
have
to
satisfy
and
then
just
try
to
State
them?
As
you
know,
equations
or
something
similar,
it
doesn't
have
to
be
a
mathematical
equation.
It
can
also
just
be
a
very
exact
description.
A
A
So
ghost
variables
are
just
a
way
to
introduce
variables
into
your
invariants
or
your
system,
descriptions
that
don't
exist
on
the
chain
or
that
you
don't
have
on
the
chain
so
impossible
to
compute
functions.
We've
seen
already
some
some
overall
balances.
You
could
think
of
that
as
sort
of
a
ghost
variable.
A
Another
one
is
like
well
total
deposited
ever,
for
example,
how
much
ether
has
this
contract
ever
received?
Maybe
you're
not
actually
tracking
that
you
can't
probably
actually
track
that
in
your
in
your
contract.
But
if
you're
just
reasoning
about
the
about
your
contract,
then
you
can
say
like
well
how
much
ether
has
ever
been
in
this
contract?
Make
that
a
variable-
and
you
studying
your
questions,
and
hopefully
you
may
decide
that
some
of
these
ghost
variables
actually
deserve
to
become
State
variables.
A
It
might
make
sense
to
actually
keep
track
of
these
on
chain.
The
way
we
do
with
totals,
even
if
it's
just
for
monitoring,
even
if
it's
just
a
little
view
function,
even
if
it
costs
a
little
bit
of
gas.
It's
going
to
help
you
reason
about
your
code,
monitor
your
code
and
like
make
sure
you
can
run
your
tests
on
on
chain
State
forever.
A
Here's
an
example
of
de-optimizing.
Just
to
give
you
a
quick
look
of
what
that
can
look
like
here's,
a
really
simple
optimized.
You
know
normally
optimized
piece
of
code.
When
you
give
rewards,
then
you
increment
the
total
reward
ever
variable.
That
should
be
a
semicolon
there
and
where
did
all
semicolons
go
must
have
done
a
search,
replace
oh
well,
because
what
happens
when
you
keep
copying
over
from
different
resources
and
then,
when
you
withdraw
rewards,
you
just
calculate
you
know.
A
Whatever
a
user
has
a
specific
stake
and
you
can
say
the
last
time
they're
reserved
they
received
a
reward.
You
calculate
how
much
reward
they've
earned
since
then,
then
you
update
some
variables
and
you
send
them
some
tokens.
The
really
dumb
way
to
do
this
is,
when
you
say,
give
rewards
you
just
iterate
over
all
the
users
and
you
give
them
a
bit
of
reward
and
then,
when
they
withdraw,
you
just
set
their
rewards
to
zero
and
you
send
the
tokens.
A
You
can't
do
that
right,
that's
not
really
possible,
and
if
you
do
that,
I
will
slap
your
fingers,
but
if
you
can
definitely
make
a
statement
like
hey,
these
things
will
give
the
exact
same
results
for
a
single
user
right.
If
we
call
to
give
rewards
with
a
certain
number
of
amounts
and
then
I
call
withdrawal,
rewards
I
should
receive
the
same
things
from
both
of
these
implementations.
A
So
make
sure
that
you,
you
know,
have
it
I,
don't
know
how
you
like
to
document
things.
If
you
like
to
do
it
in
your
codes,
you
have
to
be
new
code
comments
or
if
you
want
to
have
a
Google
doc
somewhere,
whichever
this,
but
but
this
like
you
could
have
a
few
pages
in
a
Google
document
that
say
like
hey
what,
if
we
implemented
like
this
here's,
our
actual
implementation.
These
should
be
equivalent
here's
you
know,
pen
and
paper
proof
showing
that
it
should
be
yeah
so
yeah
this.
A
Don't
go
deleting
all
your
semicolons,
like
all
the
experience
examples
here
are
illustrative:
it's
not
they're,
not
this
one
isn't
pulled
from
an
actual
deployed
code.
It's
just
you
know
a
quick
example
of
what
de-optimization
looks
like
or
I
could
say.
Oh
it's!
It's
pseudocode
like
because
some
of
you
might
be
riding
Viper
and
this
the
process
still
works
so,
okay.
Now
we
get
to
actually
proving
them.
So
you
come
up
with
something
that
you
say
like
well.
A
This
should
always
hold
over
my
contract
forever,
proving
I
had
a
math
teacher
who
said
like
well
proving
sounds
scary
like
oh,
it's
you,
you
just
need
to
convince
someone.
How
good
does
your
proof
need
to
be
well?
You're
gonna
have
to
show
it
to
someone.
If
that's
you,
if
that's
your
friend,
if
that's
nature
magazine,
then
you
know
whoever
you're
talking
to
you
need
to
convince
them.
That
yes,
I
know
like
my
argument
is
sound
and
it's
complete,
and
you
know
my
my
my
theorem
holds
right.
A
The
good
thing
about
code
is
that
it's
usually
boring
and
straightforward.
It's
pretty
mechanical
because
hopefully
the
code
is
pretty
straightforward
and
all
you
need
to
do
is
check
a
bunch
of
places
which
can
be
boring
but
straightforward.
Usually,
so
how
do
you
prevent
a
variant?
Well,
straightforward?
You
figure
out
where
are
all
the
variables
or
ghost
variables
that
are
ever
written
to?
Where
are
they
modified?
A
A
So
this
is
like
manual
verification
like,
of
course,
there's
still.
We
work
with
tools.
We
mechanize
things.
We
love
building
tools
to
do
these
things,
but
it's
actually
really
very
useful,
especially
for
smaller
contracts,
to
just
do
it
as
pen
and
paper
a
lot
of
times
so
don't
get
intimidated
when
I
say
like
just
write
it
down
like
write
it
down
into
document
and
follow
through
it's.
It
doesn't
actually
take
that
long.
Most
of
the
time,
then
you
check,
what's
called
a
base
case.
A
You
check
that
the
invariant
will
hold
from
the
start
in
the
Constructor,
the
initializer,
wherever
just
make
sure
that,
like
your
invariant,
isn't
invalidated
immediately
as
the
contract
is
deployed,
that's
usually
the
easy
part
and
then
the
hardest
part
is
the
inductive
case.
You
find
all
the
locations
that
you
noted
here
and
you
go
over
all
of
them.
A
You
can
assume,
as
you
go
into
the
the
contract,
that
that's
the
transaction
start
that
the
invariant
holds,
and
then
you
just
look
at
all
the
locations
that
modify
the
variables
you
do.
Some
symbolic
updates
just
say,
like
I'll
show
you
what
that
means
in
a
second
and
then
you
check
that
your
invariant
still
holds.
A
If
we
look
over,
the
contract,
I
usually
use
a
silver
Searcher
and
some
other
tools
just
look
get
an
initial
search
for,
where
are
all
the
places
where
these
variables
can
be
modified?
There
are
more
structured
ways
to
do
this,
but
just
use
the
fastest
make
sure
you
look
for
assembly
code,
because
you
know
it
can
modify
your
storage
variables
and
make
sure
you
find
all
the
relevant
locations.
A
I'll.
Also
look
in
the
contracts
you
inherit
from
because
you
know
modifications
can
happen
there
as
well
and
use
a
dependency
graph
tool
if
you
need
to.
In
this
case,
we
find
these
three
functions,
modify
our
total
shares
and
balances.
Add
yield
token
issue
shares
for
amount
and
burn
shares.
These
two
are
internal.
This
one's
external
I
can
just
tell
you
the
ad.
The
first
one
add
yield
token.
It's
fine.
It
just
sets
the
values
to
zero.
Constructor
and
initializer
doesn't
really
touch
any
of
this,
so
everything's
zero.
A
So
we
get
initially
zero
equals
zero,
because
the
total
shares
for
every
yield
token
starts
at
zero
and
all
the
balances
start
at
zero.
So
this
is
a
sum
of
zeros
and
we
get
zero
equals
zero.
That's
true,
so
the
invariant
holds
initially
and
then
we
go
and
find
the
issue
shares
for
amounts.
We
find
that
in
these
two
locations
are
variables
to
balances
and
total
shares
get
modified
technically.
It
also
makes
sense
to
reason
about
like
is
there?
Could
there
be
re-entrancing
here?
A
Actually
in
this
case,
that
wouldn't
matter,
are
there
many
different
paths
through
this
function?
No,
it's
a
very
straightforward
function,
technically,
there's
a
path
here,
but
it
doesn't
matter
for
us
because
we
always
only
the
only
relevant
changes
are
in
this
basic
block.
There's
failures.
But
if
this
function
fails,
then
you
know
State
doesn't
get
committed
and
still
fine.
So
we
find
that
we
add
a
number
of
shares
to
total
shares.
A
Read
very
carefully
accounts.
Recipient
balances.
Yield
token
shares,
yes,
heal
token
steel
talking
total
shares.
Yes,
yes,
okay,
we
just
add
shares
to
both
sides.
Note
that
we
don't
really
care
how
the
shares
were
computed
like
we.
This
might
be
an
external
call,
like
anything,
can
happen
here
it
doesn't
matter.
What
we
know
is
that
if
we
come
to
this
location
of
the
code-
and
we
go
through
this
line
and
this
line,
our
invariant
will
hold
once
we're
out
of
it.
A
This
one
has
left
us
an
exercise
to
the
reader.
It's
slightly
more,
not
challenging
it's
just
the
exact
same
thing,
but
I
mean
like
now:
we've
proven
this
invariant
and
it
may
Sun
sound
slightly
meaningless,
but
it's
sort
of
like
that
was
one
of
those
questions
that
come
up
as
you're.
Developing
hey
am
I
sure
that
well
total
shares
and
like
the
and
the
balances
they
should
always
match.
I
should
check
that
at
some
point
maybe
I
haven't
but
like
now
you
have
checked
it
and
you've
wrote
down
your
proof.
A
Hopefully,
and
now
you
know,
and
you
don't
have
to
worry
about
it,
that's
one
good
thing:
you
can
convince
everyone
that
the
invariance
holds
the
case
may
seem
trivial,
but
as
things
get
hairier
the
bugs
get
scarier
and
this
class
of
bugs
are
definitely
out
there.
People
do
forget
to
like
do
the
second
variable
update
I
mean
it
wouldn't
be
crazy
to
find
this
code
without
the
second
line.
A
Here
it
happens,
you
know
someone
slips
through
a
code
review
and
then
it
happens
and
now
you're
in
deep,
because
this
is
actually
used
to
calculate
rewards
and
if
this
line
was
missing,
you'd
be
in
deep
trouble
and
your
Auditors
would
find
it
and
report
it
a
critical
order,
ability
and
again
make
sure
you
save
yourself
some
somewhere
useful
somewhere.
You
can
find
it
somewhere.
You
can
show
your
colleagues,
so
you
don't
have
to
redo
your
work.
A
C
A
So
I
know
that
you're
all
hardcore
super
developers
and
your
code
is
not
always
this
straightforward.
So
what
you
do
then
failed
proofs
and
I
don't
mean
like.
If
you
find
that
the
proof
doesn't
hold,
then
you
know
you're
very
it's
invalidated
and
you
need
to
like
make
sure
that
you
know
figure
out
why
why
it
doesn't
work
and
fix
that
what
I
talk
about
here
is
fail.
Proofs
is
when
you
actually
fail
to
prove
it.
You
didn't
really
conclude
that
your
invarian
doesn't
hold
you're,
not
sure
it
holds.
A
A
So
here's
some
basic
tools
that
we
can
use
and
we
usually
recommend
like
if
we
can't
prove
if
we
can't
prove
an
invariant
and
we
really
try
to.
Then
we
usually
ask
you
like
hey:
can
you
make
this
a
bit
more
clear
because
we
haven't
been
able
to
convince
ourselves?
We
haven't
been
able
to
convince
you.
A
You
should
want
to
be
convinced
of
this
invariant,
and
until
that
happens,
we
should
make
sure
that
we
can
either
help
each
other
reason
through
the
code
or
we
can
make
the
code
more
easy
to
reason
about.
So
if
the
function's
logic
is
too
complex,
if
you
really
don't
want
to
refactor
one
thing
you
can
do,
is
you
can,
instead
of
giving
a
name
to
each
function,
you
give
a
name
to
each
basic
block,
as
does
everyone
know
what
I
mean
when
I
said
basic
block?
A
Okay
going
back,
so
a
basic
block
of
code
is
a
code
that
will
always
be
executed
together.
So,
for
example,
if
you
enter
this,
if
you
enter
this
function,
This
Can't
Fail,
there's
no
branching
here.
This
can't
fail.
There's
no
well!
This
can't
fail.
Actually
so,
but
if
we
okay-
if
we
ignore
reverting
failures
for
this
case-
which
we
can
because
you
know,
reverts
will
just
mean
that
nothing
happened.
A
These
three
lines
will
always
be
executed
together,
and
so
will
this
condition,
but
this
line
may
or
may
not
be
executed.
So
you
can
think
of
this
as
a
basic
block,
and
this
is
a
basic
block.
If
you
have
a
while
loop,
then
the
body
is
a
good
example
of
a
basic
block.
If
there's
no
more
branching
in
it.
Basically
anything
that's
like
you
can
treat
a
solid
chunk
of
code
that
will
always
be
executed
together
with
each
other.
A
If
you
had
thrown
this
line
into
here
or
like
another,
if
case,
then
it
would
not
be
in
the
same
basic
block
and
then
it
would
be
harder
to
reason
that
your
invariant
holds
so
yeah
I
mean
that's.
What
a
basic
block
is
a
single
piece
of
code
that
would
always
be
executed
together
and
if
you
have
really
complex
logic
and
your
functions
are
really
big,
you
might
want
us
instead
of
giving
labels
to
just
a
function.
A
What
we
find
sometimes,
is
that
you
will
only
like
the
variables
that
need
to
be
updated
together
are
updated
in
slightly
different
places,
and
then
we
get
an
argument
like
well.
You
know,
but
they
will
always
because
of
like
some
sort
of
reasoning
about
the
possible
execution
conditions.
They
will
still
always
be
executed
together.
Well,
why
don't
just
co-locate
them
put
them
right
after
one
another
to
make
it
easy
to
reason
about
them.
A
If
you
have
complex
arithmetic
expressions
with
rounding,
ignore
that
for
now
treat
numbers
as
real
numbers,
don't
worry
about
rounding
at
all.
You
can
do
rounding
error.
Analysis
separately,
write
your
stuff
as
functions.
Imagine
it's
all
real
numbers
make
sure
you're
invariant
holds
and
then
you
do
rounding
error
analysis.
We
did
a
talk
on
that
yesterday,
I'm
sure
you
can
find
the
link
in
the
Devcon
videos
about
how
to
do
rounding
error
analysis
to
make
sure
you're
contracts
are
safe.
A
A
This
function
modifies
all
these
storage
variables
if
it
doesn't
modify
any
one
of
the
ones
you
care
about,
then
you're,
fine,
if
it
modifies
one
of
the
ones
in
your
invariant,
but
not
one
of
the
others,
then
you
know
look
out,
but
it's
just
a
good
way
to
build
up
your
code
with
comments
that
will
make
it
easier
to
reason
about
in
a
structured
way.
If
you
see
doing
this
more
and
more
again,
did
you
check
everything,
Imports
inheritance,
both
up
and
down
inline
assembly?
A
There's
a
bunch
of
places
where
you
can
have
storage
modifications
that
you
weren't
thinking
about
control
effing
does
is
not
enough
and
if
the
code
keeps
changing,
if
you're
doing
this
as
you're
prototyping
you're
doing
it
wrong.
This
is
like
once
you've
done
a
proof
and
you
checked
everything
and
your
code
changes.
You
will
need
to
recheck
your
proof.
So
this
is
very
much
something
you
will
do
towards
the
end.
A
D
A
A
That's
going
to
take
me
four
days
and
like,
but
you
already
checked
I'm
like
well,
you
changed
the
code,
it's
like
that's
sort
of
the
negotiation
with
with
the
client,
and
it
also
kind
of
emphasizes
that
you
do
need
to
freeze
your
code
as
much
as
possible
like
so
again,
if
you,
if
you
doc,
if
you
document
your
proofs
really
well
and
they
don't
refactor
everything
and
change
the
entire
design,
then
change
like
looking
over
the
proof
should
be
pretty
straightforward.
If
you're
used
to
it,
you
can
kind
of
work
from
the
diff.
A
Yeah
I
mean
there's
a
feedback
loop
here
as
well.
Right
I
mean
if
you,
if
you
write
down
your
framing
conditions,
put
them
in
the
function
and
then
you
can
make
sure
that
the
client
knows
to
respect
them
or,
like
you
know,
up
again
update
their
framing
conditions,
and
so
one
beautiful
thing
about
this
way
of
working
that
we
found
is
a
lot
of
our
clients,
get
trained
to
do
this
more
and
more
themselves.
A
They
start
producing
better
code,
it's
more
readable,
it's
it's
not
always
less
complex,
but
like
the
important
things
are
more
co-located
and
so
on.
So
I
would
say
if
you
personally,
if
clients
keep
changing
the
code
like
make
sure
that
they
understand
that,
there's
a
cost
to
that.
If
they
still
want
to
do
it,
of
course,
they
can
do
it,
but
also
help
them
to
train
them
to
be
better
at
when
they
do
that.
A
They
also
make
sure
that
the
proofs
that
you
produced
or
that
they
produce
that
they
have
are
also
kept
up
to
date.
Right
yeah
I,
like
that,
it's
a
co-location
sort
of
like
imagine
like
if
you
I,
don't
know.
If
anyone
writes
Java
or
C
or
JavaScript,
imagine
if
you
use
one
of
the
basic
data
structures
like
hash
tables
or
something,
and
you
manually
had
to
manage
the
number
of
items
you
imagine
how
to
manage
all
the
internal
variables.
A
This
is
sort
of
the
kind
of
encapsulation
I
know
people,
don't
always
love
using
libraries
for
different
reasons.
You
know
gas,
optimizes
and
so
on,
but
try
to
make
sure
that
you're
your
your
code
behaves
more
like
it,
like
you
know,
the
all
the
things
that
are
relevant
to
this
little
data
structure
updated
in
the
same
place.
A
For
a
baseball,
I
mean
it's
just
the
same
thing
right
like
in
like,
if
you
let's
say
that
this
was
a
really
complex
function
and
there's
a
bunch
of
code
here
and
a
bunch
of
code
here
with
and
there's
a
bunch
of
different
paths
through
this
function.
Right
I
would
name
this
basic
block.
Whatever
basic
block
these
contain,
I
would
name
that
something
and
then,
instead
of
checking
every
function
instead
of
going
over
over
every
function
and
prove
this
I
would
just
prove
it
over.
A
As
we
go
into
this
look
when
we
are
here
assume
the
invariant
holds
after
the
basic
block,
which
I
know
will
be
executed
together,
I
can
show
that
it
holds
and
then
for
every
basic
block.
You
just
go
well
in
this
basic
block:
it's
not
modified,
so
if
hold
four,
then
it
holds
after
this.
The
basic
blocks
appear
if
it
gets
modified
before,
if
it's
it
doesn't
get
modified,
so
it
still
holds
right.
So
it's
sort
of
like
you.
A
Instead
of
showing
that
the
invariance
hold
over
each
function,
you
do
it
over
the
basic
block
and
you
give
them
a
name
or
something,
and
if,
for
some
reason
this
was
down
here
one
of
the
updates
we're
down
here,
then
that's
a
good
reason
to
move
it
up
so
that
they're
in
the
same
place,
because
that
will
make
you
reason.
It's
a
lot
harder
to
reason
about
it
if
they're
in
the
different
basic
blocks.
So
you
have
to
think
about
everything
that
happens
between
there.
But
if
you
co-locate
them,
then
it's
a
lot
easier.
G
A
Just
much
Harrier
proof
to
make
like
it's
just
like,
if
you
really
need
to
do
like
consider,
if
you
really
need
to
do
that,
if
you
really
need
to
do
it
that
way,
then
you
do
need
to
treat
the
entire
thing
as
one
block
and
reason
about
all
the
possible
paths
between
I'm
a
little
short
on
time.
If
I
want
to
get
through
this,
so
we
do
have
a
minute
10
minutes
of
questions
at
the
end
right.
So
if.
H
H
That
you
generate-
and
you
increase
one
by
one-
this
ID
will
eventually
overflow
and
you
can.
You
cannot
prove
that
it
will
never
overflow,
but
it
will
require
millions
of
transactions.
So
in
practice
the
you
you
should
not
you,
you
can
prove
it,
but
it
will
be,
never
reachable.
So
what
is
what
is
your
view
on
this?
You.
A
State
your
assumptions
you
make
the
assumption
that
there
will
never
be
two
to
the
power
256
transactions
on
the
ethereum
blockchain
and
you
move
on
with
your
day.
That's
it
all
right.
It's
like
the
the
counter
in
open
sampling
contracts
can
be
unchecked
on
its
increment
because
it
will
never
update.
It
will
never
overflow.
If
you
know
what
I'm
talking
about.
If
you
don't
then
doesn't
matter
so
I
I
just
need
to
move
on.
A
So
if
it's,
if
you're
having
a
lot
of
trouble,
look
at
the
environment,
that's
giving
you
trouble
pick
one
function,
look
at
all
the
relevant
variables
and
try
to
group
them.
You
may
have
to
create
a
few
different
paths.
Use
helper
functions
like
you
know
this
one's
really
good
the
they
had
the
burn,
shares
and
issue
shares.
I
think
that
might
have
been
in
our
recommendations
like
well.
These
things
will
have
to
be
up
there
together.
A
Let's
make
sure
they're
updated
in
a
single
place
where
all
the
relevant
things
to
burning
shares
happen
together.
Right,
don't
do
it
all
in
you
know
all
over
the
code,
if
you
can
avoid
it
remember.
This
is
what
you
need
to
show.
The
invariant
holds
at
construction
time
and
it's
not
initialization,
and
if
the
invariant
holds
at
the
beginning
of
a
basic
block,
it
holds
at
the
end
of
the
basic
block
through
that
for
all
the
blocks,
then
the
variant
holds
anyone
who's
likes
discrete
math.
A
This
is
an
induction
proof,
we're
security
Auditors.
We
have
slightly
different
priorities,
sometimes
from
developers.
So
like
we
kind
of
security,
is
the
most
important
thing.
Simplicity
is
the
second
most
important
thing
it
can
depend,
but,
like
the
thing
is,
Simplicity
is
so
tied
into
security
that
we
really
care
about
Simplicity
and
we'd.
Rather,
have
you
skip
a
neat
bit
of
functionality?
If
it
just
makes
things
too
complex,
and
then
you
know
save
that
for
version
two
or
something
or
an
extension
and
optimizations
are
the
least
important
thing.
A
I
know
that
doesn't
resonate
with
everyone,
but
if
these
things
are
so
much
more
important
to
you
than
keeping
things
simple
and
having
make
it
being
easy
to
reason
about
security,
what
you
can
do
again,
it's
just
it's
a
lot
of
work,
but
then
again
you
should
probably
spend
you
know.
10
times
more
time
on
securing
your
smart
contract
code
than
you
spend
on
writing
it.
So
it
might
be
worth
it.
A
Do
you
want
to
talk
about
invariances,
test
targets
we
like
to
use
Foundry?
You
can
take
your
invariance
and
just
create
a
bunch
of
tests
to
just
test
those
as
properties
like
you.
You
take
the
variant
we
had
here
and
you
just
there.
You
go
and
you
run
a
test
that
just
does
a
bunch
of
different
operations
and
it
interacts
with
your
protocol
in
a
bunch
of
different
ways
and
at
the
end
it
checks
your
property.
A
That's
pretty
straightforward,
a
really
cool
thing
you
can
do
if
you
could
instrument
your
testing
to
just
you
know
at
the
end
of
every
test,
you're
running
check
your
invariant
like
make
sure
your
advantages
always
holds
everywhere.
It
can
be
hairier.
There's
things
I'm
going
to
show
you
one
trick
to
do
it.
It's
not
it's
not
the
most
elegant
way,
but
it's
the
most
simplest
that
will
get
you
going
quickly.
A
Here's
a
dead,
simple
idea.
If
we
take
the
contract
we
just
had
and
we
just
wrap
it.
So
we
take
all
the
functions
that
affect
user
accounts,
so
we
make
sure
we
keep
track
of
all
the
users
we
have.
So
we
can
do
the
sum
overall
to
balance
this
thing
and
then
we
just
whenever
there's
an
interaction
we
make
sure
we
add
that
user
to
the
set.
A
Then
we
do
the
regular
update
and
then
at
the
end
of
every
function
we
check
our
invariance
and
we
do
this
for
all
the
Contra
or
all
the
relevant
functions
in
the
contract
and
checking
the
invariance
is
just
checking
well,
you
know.
So
once
we
have
this
one's
called
A2,
so
checking
A2
is
just
doing
this
thing,
we're
summing
over
all
the
balances
and
then
we
make
sure
that
matches
the
total
shares.
A
So
now,
you're
checking
your
invariant
at
the
like
in
each
and
every
interaction
you're
doing
with
your
contract
again
I
mean
I'm
sure
a
bunch
of
You
Are
cool
hackers,
and
you
could
do
this
with
if
you
get
the
name
of
The
Foundry
op
code.
But
you
know
if
you
can
update
the
the
evm
code
of
the
contract
in
place,
to
do
this
in
a
cooler
way
and
in
a
more
robust
way,
but
this
will
get
you
going
pretty
quickly
so
yeah.
A
Basically,
your
job
is
to
update
ghost
variables
the
variables
that
you
have
in
storage.
You
can
always
check
your
ghost
variables.
You
need
to
keep
track
of
with
a
wrapper.
This
might
also
convince
you
that
some
of
your
ghost
variables
should
be
actual
variables.
Maybe
it's
maybe
it
makes
sense
to
keep
track
of
a
set
of
all
your
users
in
your
code.
I,
don't
know
it's
a
trade-off.
You
have
to
make,
and
finally
I
just
want
to
mention-
you
can
also
use
this
for
monitoring.
I.
Think
someone
mentioned
it.
A
There's
two
approaches
to
monitoring.
Roughly
one
of
them
is
just
doing
it
on
chain
like
make
sure
check
your.
If
you
find
some
important
variants
that
you
can
check
on
chain,
you
can
put
them
in
requires
in
a
search
clause
and
then,
if
something,
if
for
some
reason
at
the
end
of
a
transaction,
they
are
violated.
You
bail,
you
stop
the
protocol,
that's
good,
because
you
can
halt
the
contract
before
bad
things
happen.
You
can't.
I
A
One's
going
to
be
able
to
mess
with
your
toll
shares
and
like
steal,
a
bunch
of
yield
that
way,
it
is
pretty
scary,
though,
because
it
can
can
cause
liveness
bugs
you
don't
want
your
contract
to
end
up
in
a
state
where
it
can
never
proceed
and
now
all
the
funds
are
stuck.
So
you
know
talk
to
your
auditor.
A
It's
like
talking
to
your
doctor,
like
you
know,
we're
we're
here,
have
them
on
speed,
dial,
ask
like
I'm,
not
sure
about
this,
but
I
have
this
little
thing
in
my
code
and
like
they
might
say,
that's
fine
or
they
might
say,
come
right
in
drop
everything
you're
doing
and
let's
talk
about
this
and
you
know
obviously
gas
costs.
You
have
to
put
the
gas
cost
on
all
the
users
or
you
can
do
off-shade
monitoring
a
poor
man's
monitor
we'll
get
to
that.
But
you
can,
you
know,
deploy
it
later.
A
Even
if
you
already
have
a
protocol
up
and
running,
you
can
still
deploy
some
off
chain
monitoring.
He
can't
call
us
live
in
his
bugs.
Obviously
what
do
you
do
if
you
detect
a
failure?
Maybe
it's
all
regulates,
your
variant
got
violated,
someone
stole
all
your
money
and
it
may
not
prevent
tax
that
you
know
happen
in
a
single
block.
Someone
uses
flashbots,
it
violates
some
invariants
and
now
you
know
the
damage
is
already
done
before
your
Sentinels
can
come
in
and
halt.
Your
protocol.
A
After
that
well
well,
first
I
should
mention
what
can
you
do
next?
Well,
you
can
keep
finding
invariants,
you
can
add
more
document
them
share
them
with
your
Auditors
share
them.
With
your
with
your
users,
you
probably
have
a
bunch
of
white
hat
users.
Hopefully
that
can.
If
you
make
bold
statements,
they
will
take
that
as
a
challenge
to
go
out
and
try
to
find
violations
of
them
and
the
good
thing
is.
A
You
can
kind
of
keep
doing
this
long
after
deployment
finding
finding
good
invariance
making
that
will
improve
your
documentation
and
they
will
improve
your
monitoring.
So
you
know
security
doesn't
end
when
you
deploy
another
thing
I
want
to
mention.
Is
we
like
symbolic
execution
with,
like
formal
verification,
so
we're
working
pretty
hard
on
making
sure
that
if
you
write
your
invariance
in
Foundry
and
you
fuss
over
them,
you
can
try
as
many
million
inputs
as
you
want.
We
also
have
a
tool
that
will
let
you
run
it
symbolically.
A
So
try
it
on
all
inputs,
there's
a
bunch
of
trade-offs.
You
should
do
fussing
first,
because
it's
fast,
you
can
write
your
test
using
solidity
same
thing,
because
you
know
we
used
to
found
your
chest
anyway,
you're
limited
to
what
you
can
express
in
solidity,
whereas
with
our
KVM
Foundry
implementation,
you
can
kind
of
use
all
of
matching
logic
and
not
all
a
matching
line,
but
a
lot
of
matching
logic.
It's
a
it's
a
nice
logic.
Fussing
is
extremely
fast.
This
symbolic
execution
is
pretty
slow.
A
It's
getting
faster,
my
CTO
is
looking
at
me.
I
might
have
called
it
as
orange,
but
it's
turning
more
and
more
yellow
doesn't
require
any
human
intervention.
This
often
requires
human
intervention,
because
a
symbolic
execution
or
engine
or
a
prover
might
not
be
able
to
complete.
It
might
not
be
able
to
say
yes,
I
proved
it
or
no
I
found
a
counter
example.
It
might
say:
C3
can't
handle
this
query.
So
you're
gonna
have
to
help
me
out
here
and
that
can
require
some
expert
human
intervention.
A
Symbolic
inputs
are
100
and
100
input
coverage,
you're
testing
every
possible
value.
So
if
you
prove
your
invariance
with
KVM
and
Foundry,
then
you've
they're
proven
this
was
contentions.
Yesterday,
the
idea
of
false
passes
and
false
negatives
I
think
it's
unfair
to
say
that
you
have
false
negatives
with
fussing
because
well
it's
not
like
Foundry
comes
in
or
a
echidna
comes
and
says
like.
Oh
actually,
we
didn't
find
anything.
So
therefore,
it's
safe,
but
the
problem
is
sometimes
that's
what
developers
or
users
think.
A
So
that's
why
you
can
think
of
that
as
a
false
positive.
You
can't
really
have
or
a
false
negative.
You
can't
really
have
a
false,
negative
or
false
posture
with
symbolic
execution.
Either
we
prove
that
this
doesn't
hold
or
we
prove
that
it
holds
either
your
invariance
is
correct
or
it's
not
or
you
get
stuck
and
you
need
a
human
and
then
you
need
to
do
some
things
that
are
easy
to
try
hard
to
master
easy
to.
A
Try
means
that
you
can
get
in
on
our
Alpha
release
and
do
it
hard
to
master
means.
You
might
have
to
call
us
and
we'll
help
you
and
we're
happy
to
help
you
along
here's.
What
it
can
look
like.
You
know
Forge
tests
will
run
the
standard
256
tests
for
you.
You
can
make
turn
this
up
to
as
many
million
as
you
want
with
KVM
Foundry.
A
This
is
a
example
from
rolls
talk
yesterday,
KVM
was
able
to
prove
that
a
specific
invariant
just
held
that
was
written
initially
as
a
Foundry
test
again
go
and
look
at
his
video.
If
you
want
to
check
that
out,
I
would
be
remiss
if
I
didn't
mention
that
we
are
starting
a
research
branch
and
runtime
verification.
So
if
anyone's
research
minded
or
just
curious,
please
go
to
research.rontimereification.com.
We
have
a
bunch
of
research
challenges
there.
A
I
think
that's
what
I
got.
We
do
have
10
minutes
for
questions.
I
was
promised
so
I've
seen
a
few
hints
again
if
someone
wants
to
like
try
this
right
now,
like
pull
up
some
of
your
code,
try
to
find
some
few,
a
few
invariants
I'll
just
do
a
little
train
out
of
here
and
we'll
find
a
table
somewhere
and
sit
down
and
work
for
as
long
as
we
have
to.
A
If
you
go
home-
and
you
do
this
later,
write
me
at
Twitter
or
at
runtime
verification.com,
you
can
always
reach
out
to
us
at
Discord
we're
happy
to
help.
This
is
a
past
talk.
The
video
should
come
soon
so
check
that
out
as
well.
It's
important
to
what
what
you'll
be
doing,
because,
eventually
your
environment
will
contain
a
division
and
then
all
bets
are
off
and
you
need
to
know
what
you're
doing
cool.
J
Yeah,
so
the
idea
that
you
can
do
pen
and
paper
proofs
as
a
really
you
know
robust
method,
is
new
to
me.
I
guess
my
question
is:
it
might
be
a
bit
vague
but
like?
How
do
you
think
of
the
risk
of
let's
say
I
take
that
seriously
and
I
write.
My
proof
I
convince
my
team
member.
How
do
you
think
about
the
risk
that
we've
still
missed?
Something?
A
The
good
thing
is
that
if
they
do
then
I
mean
we'll.
If,
if
you
write
invarians
and
like
hey,
we
have
a
proof.
We
will
also
check
the
proof.
Like
I
mean
we're
part
of
the
audit
yeah
we're
the
ACM
Journal
you're
submitting
to
or
like
you
know,
we'll
make
sure
that
you're
reasoning
is
out
because,
like
oh
that's
a
good
invariant,
we
trust
you
guys,
but
let's
double
check
right,
ask
for
pen
and
paper
versus.
So
this
is
still
formal
verification.
A
Someone
says,
like
someone
said
like:
oh,
it's
not
formal
verification,
because
it's
a
pen
and
paper
now
it
is
formal
verification.
It's
not
mechanized.
For
my
verification,
you
wouldn't
take
a
math
paper
and
say:
oh,
it's
not
a
formal
proof,
because
it's
in
English,
like
it's
still
formal
proof,
it's
about
how
you
reason
and
how
good
you
are
at
formal
reasoning.
A
K
K
The
mic
just
go.
Okay,
so
obviously,
like
part
of
the
limitations
of
of
defining
invariance
would
be
like.
If
it's
a
house
and
the
invariant
there's
no
Thief
can
go
through
the
front
door
or
come
out.
If
you
somehow
got
in
right.
Let's
say
that's
the
invariant
right,
so
obviously
the
limitation
would
be
that
you
know
we
sort
of
like
didn't,
define
that
oh
there's
also
a
window,
you
know
or
they're.
You
know
there
were
roof
tiles
or
there
was
something
to
that
effect.
A
Well,
I
so
I
mean
to
to
work
with
your
analogy.
What
you
do
is
something
like
instead
of
saying
the
thief
can't
go
through
the
front
door.
It's
like
what
do
you
care
about
the
thief
can't
get
in
the
house
and
then
you
have
to
say
what
are
all
the
ways
to
get
in
that,
like
you
know,
is
there
a
whole
like
what
can
happen?
Is
there
a
hole
in
the
walls
and
where
is
there
a
window?
Can
you
get
in
from
the
roof?
It's
sort
of
the
same
thing
here.
A
It's
like
one
thing
we
do.
A
lot
is
like
a
really
good
starting
nodded
with
is.
Where
are
all
the
places
where
any
token
transfers
happen?
Those
are
a
great
place
to
work
backwards
from
because
you
know,
and
then
there's
always
inline
assembly.
But
let's,
let's
forget
that
for
now,
but
just
look
at
all
the
places
where
tokens
or
ether
change
his
hands
and
then
look,
then
you
can
start
looking
like
well.
A
If
we
cover
all
the
paths
that
can
reach
those
locations
and
those
are
all
safe,
then
we're
safe
and
then
you
know,
of
course,
like
you
know
what
what,
if
the
token
can
do,
weird
things
if
it
like
can
block
use
or
something
something
you
need
to
keep
in
mind,
but
yeah
that
that's
sort
of
the
approach
right
like
find
like
well
take
the
floor
of
the
house.
That's
the
thing
that
this
thief
can
never
reach
and
then,
like
exhaustively
enumerate
all
the
way
someone
can
reach
the
floor
of
your
house.
I
guess.
A
L
Have
Mike
so
in
the
example
you
showed
where
you
talked
about
basic
blocks,
my
reaction
was
like
and
and
reasoning
about,
invariance
before
and
after
they're,
not
as
it's
written
they're
not
necessarily
accessible
to
us
to
to
like
it's,
not
maybe
we
instrument
it
but
yeah
I
can't
really
get
in
there
easily,
with
the
tools.
I
have
in
my
hand,
I
by
hand
like
Forge
and
say:
okay.
L
This
is
an
invariant
that
holds
over
this
if
statement
or
like
the
Block
in
there.
So
so
I'm
curious,
like
you
know
how,
if
there
is
a
way
I'm
missing
and
then
this
this
also
maybe
part
two
is
like.
Does
verifiable
code
look
different
than
like
readable
code
and
testable
code,
because,
if
I'm
to
I
imagine
pulling
this
out
into
a
lot
of
helper
functions?
That's
not
my
preference
in
this
case,
so
I
I'd
like
to
hear
your
thoughts
on
that.
A
A
A
Ask
for
the
readable
or
I'd
say
that
I
say
they
all
come
together,
pretty
well
in
the
sense
that
you
don't
have
to
have
small
helper
functions
all
over,
but
like
like
I
I
again.
The
data
structure
example
right
like
if
you
think
of
your
Java
hash
map
as
a
single
entity,
make
sure
that,
like
it
might
be
a
good
idea
to
have
like
you
know
the
updates
or
deletions
from
from
that
just
be
co-located
and
might
as
well
probably
be
a
function
right.
So
and
it's
not
about
going
crazy.
A
I
wouldn't
say
like
break
these
out
too
in
in
a
helper
function
like
we
have
Burns,
and
we
have
the
issues
like
that's
fine.
It's
only
two
places
verifiable
code
and
testable
well
testable
code,
especially
now,
if
you're
using
Foundry,
testable
code
kind
of
requires
you
to
put
everything
public,
which
you
know
is
a
bunch
of
costs
that
you
might
not
want
to
pay,
but
verifiable
code.
I'd
say
now.
It
just
really
relies
on
this.
A
That
you
have
all
the
relevant
changes
to
things
that
have
a
clear
relationship
are
co-located,
whether
that's
in
functions
or
anywhere
else,
and
you
know
right
right,
a
bunch
of
inline
comments
that
say,
like
you
know
how
yours
back
in
this
environment
and
so
on.
I'd,
say
that
the
the
enemy
of
this
is
maintainable
code.
That's
why
it's
like
the
good
thing
here
is
like
well
things.
A
M
I
actually
have
a
follow-on
question
to
that
right
here
in
the
back
hi
yeah
you,
you
said
that
you
should
be
doing
these
proofs
only
during
the
or
when
the
code
is
frozen,
because
you
can,
you
don't
have
to
be
redoing
your
changes
over
and
over
right,
which
is
right.
You're,
like
you,
don't
have
to
be
redoing
this
work,
but
it's
you
have
something
to
mechanize
the
invariant
checking
you
can
do
it.
M
You
know
not
only
with
changes,
but
you
can
also
get
valuable
feedback
during
the
development
cycle
right
so,
and
that
has
other
benefits
too.
That
you
sort
of
alluded
to
in
your
symbolic
execution
is
that
you
don't
have
to
rely
on
the
fact
that
you
have
to
manually
look
at
all
the
places
where
storage
is
updated.
M
You
don't
have
to
worry
about
the
fact
that
you
made
a
delegate
call
into
a
library
and
oops,
actually
that
Library
had
an
inline
assembly
blocked
as
a
secretly
changing
that
all
gets
sort
of
handled
for
you
automatically
during
mechanized,
proving
so
I
I,
just
I,
I,
guess
I
quibble
with
what
you've
said
there
that
you
should
only
be
doing
your
invariant
proofs.
You
should
probably
be
doing
it
much
more
frequently.
Yeah.
A
I
mean
I'm
I'm
more
talking
from
experience
like
it's,
it's
like
I
would
say.
Like
start
writing
in
variants
like
as
soon
as
you
hit
your
docs,
like
you
know,
you're
doing
your
design
start.
Writing
your
variants,
keep
them
up
to
date
in
the
code.
Realistically,
that
doesn't
happen
as
much
as
I'd
like.
If
you
want
to
be
a
unicorn
and
do
that
I
love
you
but
like
I
know
most
people
here
won't
do
it
that
that's
sort
of
what
I
was
I
was
getting
at
and
especially
like
yeah.
A
If
you
do
your
instrumented
tests,
then
you
know
go
right
ahead.
It's
also
like
from
experience.
Sometimes
the
signs
change
enough
during
the
process
that
maybe
teams
don't
want
to
invest
all
that
time
in,
because
these
instrumental
tests
can
take
a
while
to
do
as
well.
If
you
want
to
have
some
examples,
go
to
that
alchemics
V2,
Foundry
repo.
It's
called
that
because
we're
working
on
setting
up
founder
tests
sort
of
like
this,
but
like
even
even
more
powerful
and
extensive.
A
So
you
can
see
some
of
the
work
that
goes
into
doing
like
full
Foundry
checking
of
a
bunch
of
different
invariants,
but
the
all
the
variants
came
from
an
audit
where
we
found
them
and
wrote
like
formal
English
proofs
of
Lucas
over
there
actually
did
than
that.
So
it's
yes,
this
paper
and
a
bunch
of
other
things
in
our
Publications
are
actually
really
good
resources.
A
If
you
just
want
more
examples
of
this,
this
entire
section,
where
we
just
go
over
like
10
different
invariants
and
give
formal
fairly
formal
proofs
or
hand
waves
about
why
each
of
them
holds
so
it's
a
great
place
to
go
and
see
more
examples.
There's
also
links.
If
you
go
again
to
the
beginning
in
the
the
lecture
notes
or
slightly
more
extensive,
there
should
be
links
in
there.
I
A
kind
of
a
follow-up
on
that
it
strikes
me
that
some
of
this
could
be
related
to
behavior,
driven
development.
I,
don't
know
if
I
haven't
really
seen
this
in
the
solidity
web
3
world,
but
you
know
think
of
like
a
tdd
loop
but
then
zoom
out.
So
instead
of
writing
a
failing
unit
test
red
green
refactor,
Loop
you're,
doing
a
red
green
refactor
loop
at
like
app
or
protocol
functionality
level.
I
So,
instead
of
like
the
standard,
arrange
act,
assert
way
that
we
might
set
up
a
unit
test
in
Behavior
driven
development,
they
call
it
given
when
then
so.
Given
some
background,
when
some
action
gets
taken,
then
I
expect
these
assertions
at
the
end
and
I
think
it
could
fit
well
with,
like
trust,
threat.
I
Modeling
like
actors,
assets
actions,
I
was
just
curious
if
you've
seen
that,
because
when
we're
doing
bdd
and
I'm
trying
it
out
on
a
solidity
project,
you
got
to
keep
those
green
and
so
I
wonder
if
there's
a
way
to
kind
of
Drive.
Some
of
your
development
within
variants
that
you
use
in
the
bdd
world
you
use
cucumber,
which
is
like
runnable
English
language,
so
I
I
thought
that
might
be
a
pattern.
I
don't
know
if
you've
seen
that
no.
I
E
Hello,
I
just
wanted
to
make
one
clarification
that
the
inductive
proof
at
the
function
level
is
what
you
need
to
perform
to
get
the
invariant
to
hold,
but
the
basic
block
level
is
easier.
That's
why
it's
presented
as
an
alternative.
So
if
you
can
show
it
at
the
basic
block
level,
then
it
holds
at
the
function
level,
not
necessarily
the
other
way
around.
So
if
you
can't
show
it
at
the
basic
block
level,
try
it
at
the
function
level
still
might
hold
so.
A
So
KVM
doesn't
actually
work
over
Viper,
so
the
thing
is
like
well.
The
the
thing
we're
developed
now
works
over
Foundry
and
Foundry
works
over
solidity,
but
I
mean
there's
nothing
stopping
you
from
setting
up
your
own
little
pipeline
where
you
build
your
contracts
in
Viper
test
them
in
solidity
with
Foundry
or
just
you
know,
hack
on
Foundry,
to
make
it
include
a
Viper
compiler
and
then
do
the
same
things,
because
you
know
it.
A
Yeah
actually
check
out
the
the
alchemix
paper
for
a
good
like
run
through
of
so
there's
a
section
at
the
beginning.
That
lists
some
variants
in
the
section.
At
the
end,
that
proves
the
variants
and
in
between
are
just
all
like
the
you
know,
findings
reports
with
mechanized
proofs
I,
don't
we
I
mean
we
have
a
bunch
of
like
tested
come
talk
to
us
like
depends
on.
Like
your
background
on
where
you
want
to
start.