In this blog post, we present a short introduction to Rocq, a formal verification system, as a summary of the guide Rocq in a Hurry from Yves Bertot of the Rocq team.| formal.land
Here we present the beginning of our work to develop a formal verification tool for LLZK from Veridise, a new language designed to implement zero-knowledge circuits. The zero-knowledge technology is how future versions of Ethereum are planned to be implemented.| formal.land
In this blog post, we present how we specify and verify the implementation of the ADD instruction of the EVM virtual machine in Rust.| formal.land
Here, we present our beginning work of translating part of the OpenVM code to the proof assistant Rocq. The aim is to experiment around the formal verification of the zero-knowledge circuits of this zkVM based on the Plonky3 library. One of the aims of the zkVMs is to increase the scalability of the blockchains by packing many transactions in a single zk proof.| formal.land
This blog post provides a review of the existing literature on agent-based systems for automated theorem proving, while presenting a general approach to the problem. Additionally, it serves as an informal specification outlining the requirements for a future system we intend to develop.| formal.land
We want to write a series of blog posts about our efforts to use LLMs to formally verify code faster with the Rocq/Coq theorem prover. Here, we present an experiment consisting of writing all that we are doing so that we can document our reasoning and help LLMs to pick up human techniques.| formal.land