ZK-circuits are part of the Zero-Knowledge Proof process which allows one party to prove the truth of a statement to another party without disclosing any information about it. We use extractions from different zk-circuit Domain Specific Languages (DSLs) into Lean 4 proof assistant to verify zk-circuit properties formally.
EVM-based smart contract verification involves using formal methods to prove the correctness, security, and adherence to formal specifications of an EVM smart contract.
Starknet smart contract verification involves using formal methods to prove the correctness, security, and adherence to formal specifications of a Starknet smart contract.
RISC Zero is building the RISC Zero zero-knowledge virtual machine (zkVM) as a major step toward improving the security and trustworthiness of distributed applications.
Nethermind recently partnered with RISC Zero to develop tooling that formally verify their zk-circuit against the RISC-V semantics.
We offer a range of formal verification and specification categories, with varying levels of security. Our team will guide you to a formal verification and specification service that best suits your projects needs.
StarkWare is using STARK proofs to bringing scalability, security and privacy to a blockchain near you.
zkLend is a protocol combining zk-rollup scalability, superior transaction speed, and cost-savings with Ethereum's security.
We recognize that applications of formal verification within the web3 ecosystem are rapidly evolving, and we are interested in exploring any proposals you may have.
If you have formal verification needs outside of the Starknet ecosystem, get in touch and let's discuss what we can do for you.