Established 2026 · Cayman Islands
Building the infrastructure to make formal verification the universal standard for critical software.
The Thesis
Testing can demonstrate the presence of bugs, but never their absence. Formal verification produces mathematical proof that software behaves correctly across all inputs, all states, all execution paths.
The software industry has accepted a fundamental limitation for decades. We are building the infrastructure to remove it—making exhaustive, machine-checked proof as accessible as writing a unit test.
Software that is proven correct before it ships, not discovered incorrect after deployment.
A neutral foundation stewarding verified tools as public goods across the entire software ecosystem.
Eliminating the PhD requirement. Automated proof generation that any developer can use.
(* Compiler correctness for Vyper → EVM *) Theorem compile_correct: ∀ (src : vyper_program) (evm : evm_bytecode) (state : execution_state), compile src = Ok evm ⊢ semantics_vyper src state = semantics_evm evm state (* Corollary: no reachable state violates safety *) Theorem no_exploit_path: ∀exploit_state. reachable evm exploit_state ⇒ ¬violates_safety exploit_state Proof ... QED
→ AI-generated code is accelerating total software output—and total risk surface. → $2.2B lost to smart contract exploits in 2024 alone. → Regulatory forcing functions: EU AI Act, MiCA, FDA SaMD. → Verification cost down from $1,000/line to near-zero.
Foundation Mission
The Foundation for Verified Software operates as a neutral institutional home for formal verification research, open tools, and the ecosystems that depend on them. We are the academic and public-interest counterpart to commercial verification efforts.
Advancing the science of formal verification—from proof automation and compiler verification to program logics for new languages and paradigms.
Stewarding verified compilers, proof assistants, and formal semantics as permanent public goods—free for researchers, implementable by industry.
Grants, fellowships, and partnerships that bring formal verification within reach for developers building in security-critical domains.
Current Projects
The Team
Lead maintainer of the Vyper smart contract language. Deep expertise in compiler architecture, programming language theory, and formal semantics for high-assurance systems.
Former DeepMind researcher and co-creator of CakeML, the world's first machine-verified ML compiler. HOL4 core contributor and principal architect of Verifereum.
Author of CoqHammer, the leading automated proof tactic for Coq. Expert in proof automation, first-order logic, and making formal verification accessible to non-specialists.
Supported as critical infrastructure for the decentralized ecosystem.
Get Involved
We work with protocols, research institutions, enterprises, and individuals who share the conviction that software correctness is not optional. Whether you're a potential design partner, funder, researcher, or collaborator—we want to hear from you.