.svg){kind=icon}
Now hiring!
•
We are excited to announce the release of the first version of Clear, a formal verification framework for programs written in Solidity (or any programming language that compiles Yul)!
Clear allows you to define the expected behaviour of any Yul program and prove that the code conforms to it.
For support or questions about Clear or other Formal Verification services, reach out to Julian.
Clear extracts Yul smart contracts into an embedding in the Lean proof assistant, allowing users to write computer-checkable proofs of correctness for the extracted contracts.
Unlike existing automated theorem-proving-based formal verification frameworks for smart contracts, Clear requires more human intervention. However, it allows virtually any correctness argument expressible on paper to be computer-checked. Clear leverages the power of Mathlib’s extensive collection of formalized mathematics and proof automation and domain-specific automation from the Clear framework. Nevertheless, as Gödel’s incompleteness theorems states, there will always be statements that are unprovable within any sufficiently powerful proof system, including Lean’s type system — hence the asterisk in the title!
This should unlock the ability to verify the correctness of complex smart contracts. We intend to demonstrate its power in a first instance by leveraging it to verify complex properties of numerical approximation algorithms used in DeFi and on-chain ZK verifiers.
To further solidify Clear’s trust base, we have received a grant from the Ethereum Foundation to test our semantics against the Ethereum conformance test suite and to extend our model to be fully compliant with the Cancun schedule.
We will release this model as a public good in the near future.
The Clear framework contains a verification condition (VC) generator, that, given a Yul program, can extract it into the Lean proof assistant. It automatically cuts the program up into blocks, which can easily be reasoned about, and derives simplified descriptions of the semantics of these blocks.
A formal description of the intended behaviour of the extracted Yul, as well as a third ingredient that is not an input for the automated approaches described above, a proof that the program does in fact conform to the behaviour you described, can be inserted into the generated Lean files. The Clear framework facilitates writing these proofs by providing a library of theorems and automation. The proofs can then be checked using the Lean compiler. The authoritative proof-checking kernel of Lean is relatively small and currently believed not to contain any bugs as of the publication of this blog, which would accept a proof of a false proposition. Still, for the sake of transparency, it is important to emphasize that there is still a trust base merely assumed to be correct, from which we are deducing the correctness of everything else.
Unlike automated theorem proving-based methodologies, the Clear framework requires sacrificing some time to write these proofs, in exchange for several significant advantages:
Henceforth, things get technical. (Sorry.)
Please note that this post is not meant to be an introduction to theorem proving and/or Lean. We assume some familiarity with proof assistants, but we normally keep it very lightweight on Lean specifics. One can consult the official Lean documentation to begin the journey.
The Clear framework consists of multiple components for reasoning about Yul programs. We can loosely split it into three parts:
The Clear framework workflow to verify that an initial input Yul program satisfies a given specification looks like this:
We will explore each of these components using a simple running example.
Clear makes certain assumptions about the structure of the Yul code it receives as input. The following arguments to solc will generate Yul satisfying these assumptions:
.svg)
.svg)
.svg)
.svg)
.svg)
.svg){kind=icon}
.svg)
.svg)
.svg)
.svg)
.svg)
.svg)
.svg)
.svg)
solc --optimize --ir-optimized --yul-optimizations 'hxor'
Consider the following Yul program:
function mulk(x, k) -> y {
let y := 0
for {} 1 {k := sub(k, 1)} {
if eq(k, 0) {
break
}
y := addk(y, x)
}
}
The function mulk computes x * k by repeating the addition of x k times.
One can read addk as the primop add; the naming scheme gives away its nature. We use a user-defined function here rather than a primop to demonstrate Clear’s composability and abstraction capability, as touched on above. We will elaborate further on this later. Finally, we use a conditional break within the loop rather than using an appropriate loop condition to demonstrate Clear’s ability to handle arbitrary control flow.
As mentioned above, Clear requires three user inputs to formally verify a program:
That said, there are some nuances to this. Initially, one only needs the input program. From there on, Clear will help. To follow along with the example, start here.
Running
vc peano.yul
yields the following folder structure:
Generated/peano/Peano
Common
if_6183625948864629624.lean
if_6183625948864629624_gen.lean
if_6183625948864629624_user.lean
for_4806375509446804985.lean
for_4806375509446804985_gen.lean
for_4806375509446804985_user.lean
for_84821961910748561.lean -- dependency
for_84821961910748561_gen.lean -- dependency
for_84821961910748561_user.lean -- dependency
mulk_gen.lean
mulk_user.lean
mulk.lean
addk_gen.lean -- dependency
addk_user.lean -- dependency
addk.lean -- dependency
For the overall superstructure, we have the Generated file followed by the name of the corresponding Yul file and then the name of the contract itself. Furthermore, one can in addition get a Common subfolder containing blocks of the original program that represent parts of the code, chiefly blocks encapsulating control flow, that have been abstracted over — in other words, Clear chops up your program to pieces and generates plumbing to ensure that the composition of the pieces constitute the original program. Abstraction, ease of reasoning, and component reuse are the primary reasons, e.g. if this very same if block were to occur anywhere else in the contract, it would simply refer to this file (Of course, identical blocks of code have identical behaviour. There is a caveat here pertaining to potentially differing preconditions, however, both will be derivable from the block’s weakest precondition), but the piece-wise reasoning also happens to be crucial for the performance and scaling of the framework.
Considering we also use addk, a custom function, we get a couple of dependencies, marked as such, that we are safe to ignore. There are essentially three kinds of files for each elementary block of code X:
Files in the generated family contain the encoding of the program in Yul, called X (We embed the Yul syntax within Lean; as such, the translation function is the identity), in addition to code-specific reasoning done by Clear. These autogenerated files contain the generated verification condition for the corresponding block of code named X_concrete_of_code which also happens to represent a proof that executing the block of code does indeed yield this verification condition. Some constructs such as for generate analogous stuff for each of their parts individually, but the specifics here are not all too important as we normally simply unfold these and forget about their existence altogether — furthermore, the initial proof templates already conveniently contain these unfolds to save you some precious keystrokes.
Files in the glue family contain both the statement and the proof that executing your Yul program conforms to the specification you wrote. They differ slightly based on whether they represent control flow or functions, but conceptually they can be thought of as statements of the form:
lemma X_abs_of_code {s₀ s₉ : State} {fuel : Nat} :
exec fuel X s₀ = s₉ → Spec A_X s₀ s₉ :=
λ _ h ↦ X_abs_of_concrete (X_concrete_of_code.2 h)
In other words, regardless of what the initial state s₀ is, if executing the program X from this state yields the final state s₉, then s₀ and s₉ are A_X-related, or, simply put, the specification A_X holds. Ignore the fuel, it is only needed for technical reasons. Proofs of these statements are constructed by composing two implications. The first one bridges the gap between the code and the verification condition, which uses the ingredients of the gen file. The other one links the verification condition to the abstract specification, both of which need to be provided by the user in the user file family.
Files in the user family are the main point of interface between the Clear framework and the user. They therefore require additional attention. In this example, we have 3 (three) kinds of abstractions; ifs, for, and functions. The only remaining kind not present in this example is switch, but its behaviour follows trivially as it is modeled as a sequence of ifs.
Inspecting the if_6183625948854629624 user file from above, one can immediately notice that we had to apologise to Lean not once, but twice. These sorries are holes that the user needs to fill in. In the if case, we need to provide a specification for the if.
To express the semantics of breaking out of the immediate enclosing loop, we will use setBreak. Furthermore, for accessing a variable “k” in a state s we use the syntax s[“k”]!. As a general theme, Clear comes equipped with utilities for common operations one might generally wish to express about Yul programs; do not worry however, Yul is tiny and there are very few instances with seemingly arbitrary functions being used. We then have the following definition with the corresponding sorry replaced by a natural specification:
def A_if_6183625948864629624 (s₀ s₉ : State) : Prop := s₉ = if s₀["k"]! = 0 then setBreak s₀ else s₀
It is worth pointing out here that specifications can contain any valid Lean, i.e. pretty much anything. In other words, there are no limitations on what program properties can be expressed, which is often not the case with soft formal methods approaches. The specifications we use here are what we consider most natural for the program under scrutiny, but we encourage you to experiment.
When using Clear, it is important to note that, while specifications cannot be wrong, they can very easily not represent what you think they do represent, which can render them toothless as they underspecify important behaviour. This is best demonstrated on a simple example. One could specify that a sorting function returns a sequence that is sorted, i.e. every (i+1)th element in the output is greater than or equal to the previous element. Unfortunately, we can prove that the constant function that discards its input and returns an empty sequence conforms to this specification — yet this is not what we want, it is just what we specified. With more complex behaviour, it can be extremely tricky to carefully formally state what properties are actually important. As a matter of fact, it is often the case that getting the specifications right is the difficult part of the entire process of formal verification; writing the proofs is, in a sense, secondary.
Back to the example! The lemma above, named with a prefix A_ standing for ‘’Abstract’’, describes the relationship between the input state s₀ and the output state s₉ such that the if behaves as the identity function if looking up “k” in the initial state is not zero and otherwise it updates the state using setBreak.
Now we address the second sorry. This time we need to prove that the verification condition bestowed upon us by the vc implies the specification we defined above. The name uses the Lean convention for implications, i.e. conclusion_of_assumption, in our case the conclusion being that the abstract specification holds and the assumption is that the verification condition holds.
We replace this sorry with a proof of the property:
lemma if_6183625948864629624_abs_of_concrete {s₀ s₉ : State} :
Spec if_6183625948864629624_concrete_of_code s₀ s₉ →
Spec A_if_6183625948864629624 s₀ s₉ := by
unfold if_6183625948864629624_concrete_of_code A_if_6183625948864629624
aesop_spec
As a rule of thumb, most of these proofs begin by unfolding the relevant abstractions, as these are proofs related directly to the properties we defined. This is just about the only time one will need to use the names, and it is always quite clear what these names are. As such, we shall no longer elaborate on what certain definitions and lemmas are named and why.
The rest of the proof now follows and is highly specific based on what is being proved about what programs. However, Clear tries to help as much as it can. This is achieved by a combination of lemmas and tactics for the kinds of patterns that normally arise, such as handling variable store in the presence of various assignment patterns. This particular property is so easy to prove that it is done completely automatically by aesop_spec, which can be viewed as a general-purpose clean-up tactic for proof states containing verification conditions generated by the VC. Neat!
Note that this is a prime example of extensible custom automation, which we use extensively in Clear. We intend to extend the automation considerably in future iterations of the tool.
While the little if above could certainly be attacked by automated approaches, our seemingly trivial for is a different kind of beast entirely and we are already getting into territory where a majority of automated proving tools would start to struggle. The reason for this is quite simple — for loops require inductive reasoning, which has broken many a tooth of automatic approaches to software verification.
We have to repent for all kinds of things when it comes to loops. First of all, we have a cluster of four specifications that correspond with the behaviour of particular parts of a for loop construct. First, we describe its termination condition; in our case:
def ACond_for_4806375509446804985 (s : State) : Literal := 1
Thus, an infinite loop. Worth noting Literals here can be a proxy for whatever boolean condition one’s heart desires, given we have access to the state s. E.g. s[“x”]! for the condition x. It is worth noting here that the initial release of Clear does not support loop conditions that contain side-effecting expressions even though the semantics of Yul permit this. For practical examples, this restriction is rarely ever relevant.
Then we describe the behaviour of the block that is run after every iteration of the body. The syntax s〚“x”↦42〛 is used to express the notion of assigning the value 42 to “x” in the state s.
def APost_for_4806375509446804985 (s₀ s₉ : State) : Prop :=
s₉ = s₀〚"k"↦ (s₀["k"]!) - 1〛
This basically means that k is decremented by one after every time a loop runs its body once. Easy.
Now we need to describe the way that the loop body behaves:
def ABody_for_4806375509446804985 (s₀ s₉ : State) : Prop :=
s₉ = if s₀["k"]! = 0 then setBreak s₀ else s₀〚"y"↦(s₀["y"]!) + (s₀["x"]!)
This specification captures the intent that either “k” is zero in which case we break outside of the loop, or it is not zero in which case we increment “y” by “x”. Very simple.
The last specification we need to feed Clear is pertaining to the entire loop and can be viewed as the loop invariant. We use isPure to express that the EVM state remains unmodified. Furthermore, we use isOk to designate that we can continue execution as normal from the final state — in other words, that e.g. no control flow needs to be handled for immediate execution after the loop. We have some plans to improve the UX here so that these technical details that do not matter most of the time are opaque, but it has not been a priority for now.
ef AFor_for_4806375509446804985 (s₀ s₉ : State) : Prop :=
(s₉["y"]!) = (s₀["y"]!) + (s₀["x"]!) * (s₀["k"]!) ∧ isPure s₀ s₉ ∧ s₉.isOk
This loop invariant says that regardless of how many iterations the loop makes, it will always be the case that y will be equal to y + x * k. As will be shown shortly, not only is this loop invariant preserved by the loop, it is also strong enough to prove the behaviour of the overall enclosing function.
We are finally done with the specifications. The astute reader may have noticed that while Yul semantics allow for loops to have a block to run before the loop construct is executed, we somehow do not say anything at all about its behaviour. This is because these can be hoisted outside of the loop constructs and pre-evaluated before the loop is entered, thus making the reasoning about loops ever so slightly easier (This is one of the assumptions we make that are easily broken if the solc optimisation pass is skipped).
Until now, we have been at liberty to claim whatever we wanted. This is very powerful when it comes to stating desirable properties about our code, but with great power comes great responsibility. We now need to fill in a couple of sorries to convince Clear that our claims actually follow from the Yul code in question.
For the condition, we have:
lemma for_4806375509446804985_cond_abs_of_code {s₀ fuel} :
eval fuel for_4806375509446804985_cond s₀ =
(s₀, ACond_for_4806375509446804985 s₀) := by
unfold ACond_for_4806375509446804985
aesop_spec
Pretend that the fuel argument is not there. It has no bearing on high-level reasoning and it is a technicality that we will eventually make completely opaque. Note that aesop_spec does the job again, as the condition is very simple.
The post is still simple enough, let us throw an aesop_spec at it and see what happens:
def for_4806375509446804985_concrete_of_post_abs {s₀ s₉ : State} :
Spec for_4806375509446804985_post_concrete_of_code s₀ s₉ →
Spec APost_for_4806375509446804985 s₀ s₉ := by
unfold for_4806375509446804985_post_concrete_of_code APost_for_4806375509446804985 Spec
aesop_spec
It works; glorious!
The body code and its specification are a little bit more involved, let us see what happens once it meets the mighty aesop_spec.
def for_4806375509446804985_concrete_of_body_abs {s₀ s₉ : State} :
Spec for_4806375509446804985_body_concrete_of_code s₀ s₉ →
Spec ABody_for_4806375509446804985 s₀ s₉ := by
unfold for_4806375509446804985_body_concrete_of_code ABody_for_4806375509446804985 A_if_6183625948864629624 Spec
aesop_spec
Well, turns out it still works.
How about the proof obligation that the loop invariant is preserved in case the boolean test is false and thus the loop does not execute:
lemma AZero_for_4806375509446804985 : ∀ s₀, isOk s₀ →
ACond_for_4806375509446804985 (s₀.mkOk) = 0 →
AFor_for_4806375509446804985 s₀ s₀ := by
unfold ACond_for_4806375509446804985
aesop_spec
No problem.
This is getting a bit boring, so we will speed up. The lemmas AContinue_for_4806375509446804985, ABreak_for_4806375509446804985 and ALeave_for_4806375509446804985 describe the behaviour of the loop in case continue, break and leave occur respectively. They are all discharged by aesop_spec.
There are some parallels to be drawn here between interactive approaches like using Clear and automated approaches — essentially, the easy stuff that the latter can resolve can oftentimes be also done automatically even in the context of the former. However, the fundamental difference is that we now also have the option to address the difficult bits that a fully automated approach would choke on. Please note that this comparison is somewhat crude and conceptual; there are ways to tweak some automated approaches to guide them towards solutions to more difficult problems, just like there are ways to expand the automation available in interactive approaches. This discussion is outside of the scope of this blog post.
The last remaining lemma is the most difficult of them all and pertains to the preservation of the loop invariant in case the body is executed, i.e. the boolean test condition is true. This is not a Lean tutorial, but we will point out how we utilise certain custom tactics to help us reason about Yul programs. One can safely almost ignore the isOutOfFuel bit, it is a technical detail that we will make completely opaque soon enough. It suffices to know that Lean will sometimes ask you to show that some state is not out of fuel and then you use aesop_spec and call it a day. To reinforce understanding, we encourage you to open the proofs that follow henceforth in the Lean interactive mode to see the effects of the tactics we use.
lemma AOk_for_4806375509446804985 :
∀ s₀ s₂ s₄ s₅, isOk s₀ → isOk s₂ → ¬ isOutOfFuel s₅ →
¬ ACond_for_4806375509446804985 s₀ = 0 →
ABody_for_4806375509446804985 s₀ s₂ →
APost_for_4806375509446804985 s₂ s₄ →
Spec AFor_for_4806375509446804985 s₄ s₅ →
AFor_for_4806375509446804985 s₀ s₅
:= by
unfold AFor_for_4806375509446804985 APost_for_4806375509446804985 ABody_for_4806375509446804985
intros s₀ s₂ s₄ s₅ h₁ h₂ h₃ h₄ h₅ h₆ h₇
rcases s₄ with ⟨evm, vs⟩ | _ | v <;> [skip; aesop_spec; skip]
· clr_spec at h₇
split_ands <;> [rw [h₆] at h₇; aesop_spec; tauto]
· split_ifs at h₅
· aesop_spec
· simp only [h₇, h₅] at *
clr_varstore
ring
· have : isOk (s₂⟦"k"↦s₂["k"]! - 1⟧) := by aesop
simp [h₆.symm] at this
A few noteworthy things. The superstructure of the proof is such that we do case-by-case analysis on the state s₄ to inspect its behaviour when:
s₀⟦”y” ↦ s₀[“y”]! + (s₀[“x”]!)⟧⟦”k” ↦ s₀⟦”y” ↦ s₀[“y”]! + (s₀[“x”]!)⟧[“k”]!-1⟧[“y”]! +
(s₀⟦”y” ↦ s₀[“y”]! + (s₀[“x”]!)⟧⟦”k” ↦ s₀⟦”y” ↦ s₀[“y”]! + (s₀[“x”]!)⟧[“k”]!-1⟧[“x”]!) *
(s₀⟦”y” ↦ s₀[“y”]! + (s₀[“x”]!)⟧⟦”k” ↦ s₀⟦”y” ↦ s₀[“y”]! + (s₀[“x”]!)⟧[“k”]!-1⟧[“k”]!) =
s₀[“y”]! + (s₀[“x”]!) * (s₀[“k”]!)
Clear to the rescue! Invoking clr_varstore yields:
s₀[“y”]!+(s₀[“x”]!) + (s₀[“x”]!)*(s₀[“k”]!-1) = s₀[“y”]!+(s₀[“x”]!)*(s₀[“k”]!)
This is an expression that is true in this ring of fixed width integers and so we can use Lean’s existing ring tactic to immediately discharge the goal.
Something amazing happened here. Note that by explaining the semantics of Yul in abstract terms, we can leverage existing work, such as the ring tactic, to reason about these programs. This makes Clear extremely powerful.
Note further that we use addk here, which is also a custom function. Its specification simply says that the initial state is the same as the final state except y happens to contain the sum of the functions arguments. As such, when reasoning about this for, once we encounter the line y := addk (y , x), we can leverage the abstraction capability of Clear and in fact consider any function for which we can prove the same specification, i.e. behaves the same in the ways we care about. In this case, for example, the primitive operation add would do just fine. We encourage you to make this change for yourself and observe its effects on this example.
With all the setup out of the way, we are left with mulk and its two sorries in dire need of filling, first of which being the specification.
def A_mulk (y : Identifier) (x k : Literal) (s₀ s₉ : State) : Prop :=
s₉ = s₀⟦y ↦ (x * k)⟧
We choose a straightforward description saying that the initial state is the same as the resulting state except y contains x * k. Now all that is left is to prove is the fact that the specification above follows from the verification condition. We do it thusly:
lemma mulk_abs_of_concrete {s₀ s₉ : State} {y x k} :
Spec (mulk_concrete_of_code.1 y x k) s₀ s₉ →
Spec (A_mulk y x k) s₀ s₉ := by
unfold mulk_concrete_of_code A_mulk AFor_for_4806375509446804985
rcases s₀ with ⟨evm, varstore⟩ | _ | _ <;> [simp only; aesop_spec; aesop_spec]
apply spec_eq
rintro h ⟨h₁, ⟨ss, h₂⟩⟩
clr_funargs at ss
clr_spec at ss
aesop_spec
congr
aesop_spec
First of all, note that this proof should be trivial at a high level once we know the behaviour of the loop, as mulk pretty much is the loop and a tiny bit of initialisation. As such, any logical steps that we have to take are introduced by the way that we encode Yul in Clear. Therefore, the proof itself mostly focuses on reasoning about the model itself — and Clear had better help with this. And it does!
We will go line by line as this is a good place to explain when to use which Clear tactic, which the proof is pretty much exclusively comprised of. Line 5 analyses the initial state s₀ and immediately uses aesop_spec to discharge the easy cases that account for stray control flow and the omnipresent outOfFuel nonsense. As such, we are left in a state where the execution continues — here lines 6 and 7 use some basic Lean to clean up the proof state so that we are left to prove exactly the specification we entered, except we already know that the state is Ok. The clr_funargs tactic on line 8 applies the effects of calling a function to the variable store. In general, whenever you see initcall and you know that the state is Ok, it is a good idea to throw clr_funargs at it. Now we see a Spec wrapping our relational specification in the assumption ss, so as per line 9, we use clr_spec to extract the underlying relation.
Now the proof state might look a bit tricky for one unfamiliar with the specifics of the underlying model — we have some reviveJump, setStore, and isOutOfFuel lying around. Clearly these have nothing to do with the semantics of the program and are artifacts of the way that we encode things in Clear. One can view reviveJump as a means to restore the state of a program to some previously remembered one, which normally happens when control flow occurs. setStore is an override on the variable store — this is sometimes necessary, for example when a function returns and kills its scope. Some of the time, invoking aesop_spec (line 10) performs the reasoning necessary to leave you with a statement expressed in terms of constructs you are likely to be more familiar with. Some of the time, however, aesop_spec leaves you with a couple dozen goals to prove. If this happens, we recommend you instead formulate a simpler property that you need to progress the proof and prove it with aesop_spec. In other words, using aesop_spec as an intermediate tactic that does not prove your goal right away is potentially dangerous. After the dust settles, we are thus left to prove the following:
Ok a varstore⟦y ↦
(Ok evm Inhabited.default⟦”k” ↦ k⟧⟦”x” ↦ x⟧⟦”y”↦0⟧[“x”]!) *
(Ok evm Inhabited.default⟦”k” ↦ k⟧⟦”x” ↦ x⟧⟦”y” ↦ 0⟧[“k”]!)⟧ =
Ok evm varstore⟦y ↦ x * k⟧
We see that we are trying to retrieve “x” and “k” from the variable store that has been changed by the semantics of the program; as a rule of thumb, hit convoluted variable store operations with clr_varstore and you will get back a normal form. In this case, after line 11 we are left to prove:
Ok a varstore⟦y ↦ x * k⟧ = Ok evm varstore⟦y ↦ x * k⟧
The name a is ever so slightly awkward here — currently, the aesop_spec tactic cannot be fed custom names to use for various terms it introduces; of course, one is free to perform the rename manually, but it is unnecessary for this simple example. Anyway, the congr on line 12 leaves us with the goal a = evm, i.e. an equality between two EVM states. Considering we have not used any operations that manipulate the underlying state, the problem should be quite trivial; and it is. The aesop_spec on line 13 finishes the proof.
Aaaaaand we’re done! The _usr file family has been filled; the specs have been formulated and the proofs have been constructed. As the glue file mulk.lean says, we now know that the mulk program conforms to the A_mulk specification.
In summary, Clear is a tool that lets you take any Yul program, state its expected behaviour, and prove that the code conforms thereto. Clear first translates your program to an abstract representation and gives you a proof of consistency of this translation. This gives you a simpler initial abstract object as your starting point to subsequently construct a proof that the required behaviour, i.e. the specification, follows therefrom. The process of proving is further simplified by Clear facilitating access to custom Lean tactics, i.e. automation procedures. These address certain repeating patterns that often arise when reasoning about Yul programs, such as various variable store shuffling operations — this allows you to automatically prove simpler statements about your programs, allowing you to focus on high-level ideas of your proofs.
Nethermind Security has been awarded a grant to continue our work on Clear and the goals of this grant form a large part of the near-future work. To name a few goodies that are coming soon:
Some other projects that we hope to work on to contribute to the security of the Ethereum ecosystem:
An important part of learning how to use Clear is to learn how to use Lean, as we make extensive use of its powerful capabilities. First of all, Lean checks the underlying proofs for us. Furthermore, we have access to the entirety of Lean libraries, such as Mathlib or Batteries; these contain mechanisation of mathematical and computer scientific concepts that often come in handy when reasoning about programs — for example, we used the ring tactic to prove certain integer properties. Custom tactics such as clr_varstore that are available in Clear have been created by utilising the very powerful Lean metaprogramming framework. The ability to add arbitrary automation is very useful and we will continue to both refine the existing tactics in addition to adding new ones, based on the patterns we identify in daily usage of the tool. Lastly, we use Lean’s extensible parser to encode Yul directly within Lean, which makes interfacing frictionless.
For any support or questions, email Julian Sutherland.
.svg)
The simplest solutions to the hardest
problems in blockchain
Nethermind © 2024
.png)
.png)
%20(1).png)
.png)
