formalland.bsky.social
Formal verification for everyday-life applications
We use math to ensure your code has no vulnerabilities
For Rust, Solidity, zk circuits. We use Rocq.
https://formal.land/
72 posts
38 followers
28 following
Regular Contributor
Active Commenter
comment in response to
post
Thanks for the notice! Happy to contribute to making zero-knowledge really safe, and happy to discuss if you have questions!
comment in response to
post
github.com/formal-land/...
Our first target is Plonky3-like circuits, with the verification of the Blake3 AIR primitive. 🔍
Feel free to chat with us if you have needs! 📢
comment in response to
post
This is what we propose with our "coq-of-solidity" tool github.com/formal-land/... 👀
If you need help to run it or want us to verify your smart contract is free of vulnerabilities, please contact us! 💌
comment in response to
post
This truly means the ability to write software without bugs! 🎉🎉🎉
To make the bridge between programming languages like Solidity and formal languages like Rocq we need a translator (or compiler) to translate Solidity to the Rocq format.
comment in response to
post
On the other side, formal languages like Rocq are designed to express software specifications, like "the smart contract can never end up in a situation where the funds are blocked", and verify them on *all* possible inputs.
This process is called formal verification. ✅
comment in response to
post
Solidity is the language used to write smart contracts on Ethereum and compatible blockchains. These are rather short programs (< 5,000 lines) with high security risks. 🥷
Smart contracts handle real money, and a single bug often means the loss of millions of dollars! 💸
comment in response to
post
The link to the program: csd.ens.psl.eu?ai-and-maths
comment in response to
post
It will also make sure that refactoring or protocol upgrades do not break anything in the EVM semantics. We have designed our system so that we can follow the code changes as much as possible.
comment in response to
post
The end goal will be to show that the Rust implementation of the EVM is equivalent to a native Rocq implementation that another team is doing.
We are not yet there, but hopefully, it will be the case in some months!
comment in response to
post
In particular, we need to define or axiomatize the typing of all the dependencies, as well as the trait structure, which is generally quite verbose.
comment in response to
post
We are at 33%, still far from completion, but many instructions are similar!
The "coq-of-rust" translator gives us a first representation of the code in Rocq, but then we need to show that a typing of the translated code exists, which can require a bit of work.
comment in response to
post
For the curious, this is represented in the THIR intermediate language of the Rust compiler asPointerCoercion expressions doc.rust-lang.org/beta/nightly...
There are many kinds of coercion. The one we are interested in is `PointerCoercion::Unsize`.
comment in response to
post
Link to impredicative Set's page: github.com/rocq-prover/...
comment in response to
post
Mathematicians hate impredicative sets for this last fact; for example, Lean does not have this feature, and it has to be explicitly enabled in Rocq!
But it opens as many doors as it closes, and we do not need these axioms for program reasoning! 💥
comment in response to
post
- You get a nice (the nicest?) representation of binders using existential types, for example, to implement lambda calculus using native functions
- You become incompatible with the choice and excluded-middle axioms
comment in response to
post
- You can reason with the same typing rule as programming languages for polymorphic code (can be emulated with universe polymorphism also)
- You can represent existential types (like "dyn" in Rust) of arbitrary depth (cannot be emulated with universe polymorphism)
comment in response to
post
The link to the project: github.com/formal-land/...
Reach out to us if you are interested! Our email is on our homepage.
comment in response to
post
- Hacker News: news.ycombinator.com/item?id=4336...
- Lobsters: lobste.rs/s/lomwgf
comment in response to
post
We focus on the formal verification of Rust / Solidity systems to make critical code bug-free. If you have any needs, contact us!
comment in response to
post
A difficulty is that top-level elements are in the HIR AST of Rust, while expanded types are in THIR. Our error was in handling the back-and-forth between these two structures.
Fortunately, as we are verifying more code, we make `coq-of-rust` more reliable and add more examples in our CI!
comment in response to
post
The fix is in the pull request github.com/formal-land/... in the file `top_level.rs` that handles the translation of top-level elements such as trait implementations.
comment in response to
post
with the type `core::fmt::Error` added to the list of polymorphic types for the `M.IsTraitInstance` predicate.
We also added support for `const` parameters for traits that are rarely used but still occurred in one of the codes we looked at.
comment in response to
post
```coq
Axiom Implements :
M.IsTraitInstance
"core::cmp::PartialEq"
(* Trait polymorphic consts *) []
(* Trait polymorphic types *) [ Ty.path "core::fmt::Error" ]
Self
(* Instance *) [ ("eq", InstanceField.Method eq) ].
```
comment in response to
post
for the instance of `PartialEq` for the type `core::fmt::Error`, resulting in proofs where we are stuck with inconsistent definitions.
After our fix, we correctly get:
comment in response to
post
```coq
Definition Self : Ty.t := Ty.path "core::fmt::Error".
(* ... *)
Axiom Implements :
M.IsTraitInstance
"core::cmp::PartialEq"
(* Trait polymorphic consts *) []
(* Trait polymorphic types *) []
Self
(* Instance *) [ ("eq", InstanceField.Method eq) ].
```
comment in response to
post
The trait `PartialEq`, which is implemented by many types through the corresponding `derive` macro, takes as a parameter the generic type `Rhs` with `Self` as a default type.
Previously, when translating to Rocq an implementation of this trait, we were not showing this implicit parameter:
comment in response to
post
Here is a case where this applies:
```rust
pub trait PartialEq<Rhs: ?Sized = Self> {
// Required method
fn eq(&self, other: &Rhs) -> bool;
// Provided method
fn ne(&self, other: &Rhs) -> bool { ... }
}
```