V for Verification
summary
A unified verification-as-a-service runs a language- and blockchain-agnostic pipeline that takes code plus optional V specification language assertions, executes multiple formal-methods tools, and reports which specs are proved or violated with concrete counterexamples. The service already uncovers real defects—flash-loan vulnerabilities in DApps and soundness bugs in zero-knowledge proofs—and supports an LTL-style temporal logic. Roadmap includes an upgraded VAS release and ZK-focused tools: a circuit vulnerability detector and a tool to prove circuit functional correctness.
AI-written summary · about
related talks
50mTrust but Verify: Scaling Deductive Verification with Abstract Interpretation
01h 00mCooperative Verification: Towards Reliable Safety-Critical Systems
14mRich Specifications for Ethereum Smart Contract Verification
25mvlayer Workshop
17mVEP: A Two-stage Verification Toolchain for Full eBPF Programmability
41mThe Future Is Trustless: How ZkVMS And ZkTLS Transform Bug
01h 04mSoftware Verification meets Real-World Cryptography
23mGradual Verification for Smart Contracts