Candidate Profile

Runtime Verification specializes in cybersecurity and formal verification of software systems, providing the highest level of assurance for the correctness of smart contracts and other critical infrastructure. Runtime Verification is committed to applying its expertise to the Arbitrum Security Council. Our team is well-versed in responding to and mitigating vulnerabilities in distributed systems, and we are eager to support Arbitrum in its mission to maintain a secure and resilient ecosystem.

Runtime Verification’s motivation to join the Arbitrum Security Council stems from our dedication to making blockchain ecosystems mature and reliable security-wise. As a key player in blockchain formal verification, we see the Security Council as a vital mechanism for quickly addressing and resolving any potential vulnerabilities in Arbitrum’s infrastructure. By joining the council, we aim to contribute our expertise and help protect Arbitrum's ecosystem from any critical security risks that require swift, decisive action.

• Runtime Verification has been a trusted security and formal verification partner across multiple leading L1s, L2s and other blockchain protocols and dApps, including Ethereum, Polkadot, Uniswap, Optimism, Lido, Morpho, EigenLayer and many others.
• Our company has developed multiple open-source security testing and formal verification tools like Kontrol, which enables formal verification of smart contracts, helping projects like Arbitrum ensure that critical properties hold as expected. The complete list of tools we’ve developed can be found on our GitHub: https://github.com/runtimeverification
• We have worked with various high-profile blockchain protocols that are actively operating on Arbitrum, like Synonym Finance and Alchemix to ensure that their dApps are secure, rigorously tested, and maintain the highest level of correctness. The complete list of projects we worked with can be found here: https://github.com/runtimeverification/publications
• Our team includes top experts and PhDs in formal methods, symbolic execution, and cybersecurity, with deep experience in handling complex, security-critical blockchain systems. You can see our team here: https://runtimeverification.com/team

Runtime Verification works with several prominent blockchain projects, including Ethereum, EigenLayer, Polkadot, Optimism, and Arbitrum itself. There are no conflicts of interest related to this application.