Yes, so hello everyone, I'm happy to be there and at the end of the first day, I've
been a spectator to talk to you about formal verification, it's a technique to analyze
code and to make a full coverage by making a mathematical analysis of a code, so we'll
present you what it is in the big lines on how we can apply it, so MGM and I'm worked
in the formal methods for maybe 10 or 15 years, since as a PhD student and after I've
studied formal and agency to do formal verification, especially for the blockchain industry,
so the motivation of formal methods is to go beyond testing, because even if testing is a very
effective full effective in practice, we know we can always miss bugs, because it cannot cover
all the scenarios, especially user can be very creative, as well as attackers, so we
use this, for example, from a digital, seeing that testing can show the presence of bugs,
but it cannot show that there are no bugs remaining, so it's been a few bugs, but because
the big loss, so one of the things I often quoted is the bug of Iron 5, with a wall
rocket explaining due to a bug, so there are domains where a single bug can cause loss of
material or even loss of life, for example in trains or cars, for what we want to have
mitodology at our reliable to find all the bugs, also there's a geopolitics, so all the
pay agencies in the world they want to find the reliability to be able to attack over states, for
example, the most recent, maybe Maduro, Maduro was taken by the US, they made an attack on the
ground, but also a cyber attack to get the power lines, so it shows that if you're a president,
you are concerned by the security and the government who invest more in protecting their systems,
in the blockchain world, there's a North Korea that is expected to be behind a lot of big
attacks, and they have, of course, great means to find all the bugs, and no big ripe coding wave,
with a lot of people producing more and more code, and it's very hard to make sure that everything
is correct, and in particular, they are good at writing code, but to make sure that everything is
correct, it's a much harder because of a still-educination, and today there are no, there are a lot of
offers to find bugs automatically with agents, especially the cyber security, but we see that
varsity, the kind of bugs that they cannot find will Iably, like access control errors,
for bad, it means that we need to better run more systematic tools, so for more
verification, it's a mathematical method to ensure that a program is bug free for any possible input,
so I don't know if some of you are familiar with the subject,
but when I first saw it, I find bad surprising for many reasons, first of all, we say bug free,
while we have the habit of seeing that a code is never 100% safe, but actually for
programming languages, when we think about that, it's a fully deterministic, when we go down to
the definition, it's 0-1-1, because the code will always return the same result every time we
run it, at least when it's sequential code, why not having an idea that a code can be perfect,
but we can prove that a code is a well-eback free, so the big drawback, of course, is that it's
bug free or safe for given specifications, so we need to write a formal definition of what is considered
as a bug or not a bug or a feature. Second surprise, maybe it's mathematical, so we are used to do
math on a number of matrices or geometry, but there are also formulas to reason about code,
to say what is a loop function, and this is a theory that is also behind the work of
compilers to make sure that when we go from a long graduate of a top, don't do the assembly,
we propagate the evaluation rules, it's quite interesting, and the third surprise is that we can
cover all the all-in boots, even if in general there are infinitely many, or an exponential number,
and this is because we are doing mathematical reasoning, we reason about a sense of value,
what can be an infinite aim, so we can cover much more entries, and we are testing
your testing test, for example, so we will directly show what is a concrete example of
formal verification in the rock language, which was a previously named code,
so for formal verification there are many different technologies, but all of them,
we rely on some languages, but are related to programming languages, but a bit different,
and especially more strict, and in rock, it's a language similar to a camel or a bit similar to
the worst, as well, you can define a list, which is equivalent here for an enamine in rust,
seeing that a list is a new type, which is polymorphic in A, and for two cases, the case where the list is
empty, and the case where we have a head of a list on the rest of a list, and we can fill the
linked list like that, so we have a small programming language, we can define functions,
for example, to define the length of a list, we do much like in a in rust, and we can iterate,
seeing that the list of Lyam Tiles, the length of the Lyam Tiles is 0, and when we have one
more element, we take S, that is a successor for plus 1, so we compute one plus 1 plus 1 for
all the elements of a list, and we have a lens, we can define other functions like for an
but here the concatenation of to list, and the new thing that is not very programming languages,
is that we can also stay properties, for example here we stay for any list L1 and L2,
the length of concatenation is the sum of the length, it's quite a simple property,
but with testing, we call only observe this property on a few examples,
where we can actually cover all possible lists, and how do we do that, that we have also
a part of a language, that is very to white mathematical proof, and we will do a reasoning about
the code, with a few ingredients, I can verify any, almost any kind of program, so the first thing
we do is that we consider any list L1 and L2, we have a pre-saysing anything,
it's just a variable names, how we can talk about any list, and after we use the
induction principle, so in the same way that when we return on integers, we can do proof by
inducing that we show the case 0, and the case n plus 1, assuming that the case n is okay,
it's principal, it can be realized also to list where we return about the list is empty,
or the case where the list is a head element followed by the rest of the list, and when the list is
empty, we can do, we can evaluate this expression, and we will return 0 on both sides, so we use
a flexibility, say value of the equality is trivial, because it's a same thing on both sides,
and for the induction case, we will have, but we have this equality for the rest of the list,
and using this equality with the rewriting, we get back to the fact that the two sides are
equal, and when we do cure this, the root system will check that our proof is actually correct,
so the system is search, but if we make any mistake in the proof,
or if the statement is not correct, we will never be able to wish to be n,
and there is a small kernel, but people have been working on to make sure that there are no
venerabilities or no bells meet, and to give a view also in a text editor, so it's very small,
but generally you have your proof, you have a green portion, which is what is validated,
you want to make the green go to the end of a file, and on the other side, you get what are your current hypothesis,
and what is your current target, and you want to make sure that your target is smaller,
smaller until it's obvious, so it's feels like a game, to find the white command to reduce the
target goal until it's correct and everything is green,
and who is using that, so there are many critical industries, like spacing industry, transport,
defense, and also finance, especially blockchain, where the vulnerability can enable to still a lot of
money very quickly, because it's not regulated, it's not centralized, so,
but actually, even for those critical industries, the use is rather limited, and the main reason is the cost,
and some estimates that it's 10 times more expensive to formally verify the code,
than to white it, I think it greatly depends on the domain and the scope of verification,
but the hopes is that we've a technical progress that are always going on,
active with search project, and also with the help of AI, we can automate as much as possible
the boring stuff, and especially in our role of vibrating the idea of writing code by starting from
a spec, I think it's kind of a new trend, to be able to manage more code when it's
the twiten by a human anymore, maybe a form of verification will be more popular,
and in case of a property that we check on the code,
first property we check is that there are no one time errors, so it means that there is no
panic or segmentation fault, for example, and after another interesting one is that there are
no restrictions, so that when you make an optimization of an existing code, you always get the
same result for the same inputs, the functional correctness means that you show that your code
behaves like reference simplifying implementation describing what it's supposed to do,
and after you can create business rules also about a specific two-year domain,
say that, for example, a user that is not admin is not supposed to access to certain set of values
or things like that, and you need to define your business logic rules correctly,
but you know, let's see, we attack surface is smaller when all of the code,
there are many, many methods, it's a big bit of spectrum,
it can start with phasing test and a property best test, and go up to the CRM Prover,
a full form of verification approach, and even in the form of verification itself,
there are many different tools, I think the two main categories are automated proofers and interactive
proofers, we have a difference, it's when to have the right-hand specification,
is the tool to automatically show that it's correct, or is it waiting for interaction with you
to have some hints, so the automated proofers are typically less expressive and for a full
menu, interactive ones, but interactive ones are also more complex, but it's comfortable to know
that you will never be stuck when you use interactive proofers such as the Rock language,
what I have shown, and I hope also that with AI it will be simpler,
because since the indirect proof of a language AI can talk with systems,
it has been a few investments like Armonic,
in the logical intelligence recently, and this domain to use LLMs to talk to interactive proofers,
the main languages are Rock, I was the one of the first one,
Lina Agban, derivatives of Th objective-language, so they the word aforean language.
So 11, 11,Müzik of coding, so we're chasing the first three move,
so we're chasing the second, mission, nothing of that.
So the first two moves, where we call atonement,
the first time someone achieved to make
a long-dike el culus extension.
So minimal long-range, that is mixing well,
programs and proofs in a way that things are.
That you cannot make longer proofs and still
white code.
It's quite a good achievement where it was discovered.
So it's both programming language.
Like we have seen on the master language at the same time.
So it means you can write proofs about your code,
to show property that are always true programs.
And you can even use it to be over where one,
to write code, but it's generating proofs.
So you can make decisions, procedures.
So I have, for example, to be able to compute
the vendor properties to our false.
So you can use it both ways, very elegant,
and there is a feature of dependent types,
meaning that, for example, in C,
when you have a certain size, you need to have the size
that is almost always a constant, but there
can be any expressions.
And it will type check that, and you
can be able to mix types and values freely.
And in practice, to use such systems,
we always have two steps.
One is the translation from your programs,
two formal systems.
And after that, writing the specification
and making the verification, the two steps are
about a similar level of complexity, we'll see.
The lightweight approach will do the translation
from a global risk response program,
a link, a counter, to the Rob system by hand.
So this is convenient because it's very fast,
but you can mix some details.
Typically, here, the integers are 60 for bytes.
So it means you have a overflow.
And in this translation, it's a simplified,
we use an abundant integer, but it can still
be relevant to capture the main business logic
and verify the main properties of some programs.
If we want the full analysis of some code capturing
all the details, like integers, size under everything,
making sure we do not make any typo,
we need a transpiler from the programming languages,
to the formal systems.
So for me, we have developed a few transpilers
for various languages, with OKML as well,
to the ROG system, taking the same examples,
the generated code is much longer and a little horizontal.
It can fit a bit.
After inside the ROG system, we can prove
that it's equivalent to this code, but it's similar
to the ROG on the one, and the right type for the 64 byte,
a 64 bits integer, and we can prove
a property that the max values in the ROG
are going to go down, as we show the expected from this.
We have every incandone, so that way,
we can have a fairly up-tarier risk-odd for up-tarier
properties.
On the last project we have made, we have to
verify the ROG circuit, cryptographic programs,
and the implementation of the Ethereum virtual machine,
for solidity smart contracts, that is a whiter in the rest.
So we have everything is open source.
We have a web-ish things on our GitHub,
and with the document also on our blog,
we'll invite you to test, and for 2026,
so my wish is that with the AI,
we'll be able to see much border use of formal verification,
so it will be nice, maybe, to achieve
their findings, some open source projects,
but are heavily used, like the TABS system,
or the next commands, as well,
making the use of formal verification,
more important in our enterprise projects.
So I think that because, by cutting,
really hard to know whether the code is secure or not,
there are ways to do laterate formal verification,
to verify, for example, the control rules of software.
Or maybe one other way to make the right-cutting scale,
it would be good enough, safety.
So we'll see, at the end of here.
And yes, yes, thanks.
Catch you next time.
Thank you.
Yeah.
I can just get some sleep from here?
I got very logged, although it was very insightful,
and I was incompetent, in my perspective.
I'm simply falling for someone,
but it is to experience a complicated and long-セ 애� page
You have a full set of files when you then point for proof that a regularity test would be the more advanced way to test the performance test.
Yes.
And I just have a little bit of information.
And for me, the faster questions of proof can be learned in this case.
I guess I can move a bit of this slide.
But I also can make good points for you to write.
Yes.
We work this way.
We sell this as a service as a service company.
It's a solution to space for it.
Otherwise, I think that for for more language, even if you use automated proofers,
you can still need to learn how to use them.
Yes.
For automated proofers, you will need to learn how to split your specification in a piece that can be verified automatically.
So I think it's kind of like learning about front end when you are back end or things like about necessarily text time.
We have a catalogue of software that when writing the proof inside is an extraction.
Yes.
You get some feedback.
You mean like some guides?
For example, showcase.
I think the biggest showcase was the Tesas project.
Translating the core of the Tesas blockchain.
It was one of the lines of OKML to work and then sharing parts of it.
So we didn't find really a lot of bugs because it was already heavily.
Yes.
One quick question here at the back.
Actually, hopefully very far it's a translation of pro practice.
This was the same question for the whole language.
Yes.
But we have not very far did.
One of the reasons is that for most of the language, we do not have a formal specification of the language itself.
And also it's quite difficult to do.
But we try to minimize the translation for example for rest to rock.
We take the processing tax free and directly import it one to one.
And after we define the semantics through this in rock.
So we have no logic to be able to stress as much as possible translation.
Yeah.
Yes.
So we have not verified the problem in floods.
I think so.
Some libraries formalizing clear how floods behave.
Some projects have been done.
Some projects have been done about floods.
But I think in general, people do not use floods for critical code.
We will just assume that it computes something but we.
Yeah.
Thank you.