Formal Land: formal verification services for cryptography and ZK
=================================================================

Formal Land verifies circuits, Rust and Solidity in Rocq. Garden proves determinism, functional correctness and completeness of Circom and Plonky3 circuits, rocq-of-llzk connects it to Veridise's LLZK, and rocq-of-rust and rocq-of-solidity cover the code around a ZK system. Clients include the Ethereum Foundation (CompPoly, revm), Sui, Aleph Zero and Tezos.

Website: https://formal.land
Headquarters: Paris, France
Focus: Rocq verification: Garden (circuits), rocq-of-rust, rocq-of-solidity, rocq-of-llzk
Index position: #5 of 11
Services: Circuit verification in Rocq via Garden and LLZK | Rust verification via rocq-of-rust | Solidity verifier and contract verification via rocq-of-solidity
Tools: Garden, LLZK, Rocq (formerly Coq)
Evidence: https://github.com/formal-land/garden | https://formal.land

Source page: https://sorryfree.com/firms/formal-land/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13