“Building on the blockchain” — be it smart contracts, tokens, protocols, or virtual machines — is challenging. We’ve been there. Now we’d like to share our experiences and offer our expertise via an advisory service we call “RV office hours”. During your office hours you will receive targeted advice from an RV senior engineer on the verification topic of your choice. Look at it as an affordable way to reduce existing tech debt and frustration or prevent its accumulation from the beginning.
Contact us if you need advice before starting with any type of blockchain project:
Smart Contracts — There are things you should know before you have your contract audited or formally verified. In fact, there are details you should know even before you write your smart contract. Feel free to read more about our approach. You can also check out our public reports and the collected list of known smart contract vulnerabilities.
Consensus Protocols— Our approach to protocol verificationis centered around formal methods. First, we build formal specifications of the protocol’s design and its properties. Second, we mathematically verify that protocol’s design meets its expected requirements. We developed formal models of Casper 1 | 2 | 3 and Algorand 1 | 2 | 3 | 4.
Virtual Machines — In partnership with blockchain research firm, IOHK, we designed and developed IELE, a new virtual machine that represents an evolution of sorts of the Ethereum virtual machine (EVM). It leverages the KEVM project, which successfully demonstrated that a K formal specification can automatically generate a "fast enough" VM.
Tokens — For the Ethereum ecosystem we specified ERC20-K and ERC777-K, the mathematically rigorous formalization of the ERC20 and ERC777 token standards. These formalizations facilitate formal verification of token implementations.
Formalized Languages — Developing formal analysis tools for a programming language takes a substantial amount of work. The K Framework consists of several language-independent program analysis tools automatically derived from a formal definition of the target language’s syntax and semantics. If you need help formalizing your language in K, take a look at a few examples that have been successfully formalized: C, Java, JavaScript, PHP, Python, EVM, IELE.
Musab A. Alturki is a Senior Research Engineer working on formally specifying and verifying blockchain and distributed systems. Before joining Runtime Verification, he was a Visiting Research Scholar at the University of Pennsylvania from 2017-2018, working on formal modeling and analysis of cyber-physical systems security. Before that, between 2011-2017, he was an Assistant Professor in Computer Science at King Fahd University of Petroleum and Minerals (KFUPM), Dhahran, Saudi Arabia. He received his Ph.D. in Computer Science from the University of Illinois at Urbana-Champaign (UIUC) in 2011. His research interests are in the applications of formal methods to distributed systems. He was a recipient of the prestigious King Abdullah Scholar Award for scientific excellence in 2008.
Denis Bogdănaș
Research Collaborator
Denis Bogdănaș completed his Ph.D. at the University of Iasi, Romania, where he formalized the first complete semantics of Java, using the K framework. In 2014 he did an internship at UIUC, where he met Grigore and the K team. Prior to his Ph.D. studies, he was a Java and C# software engineer for five years. Before joining RV, Denis was a postdoc at Oregon State University, where he worked on software analysis tools for Android security.
Xiaohong Chen
ZK Research Lead
Xiaohong Chen's main research interest includes formal methods and programming languages, in particular, formal specification, zero knowledge, and verification and program logics. Xiaohong believes that programming languages and programs should have formal specifications, and verification techniques should be made language-independent. He finished his Ph.D at the University of Illinois at Urbana-Champaign. Before that he obtained a Bachelor's degree in Mathematics from Peking University, China.
Everett Hildenbrandt
CTO
Everett Hildenbrandt is a formal modeling engineer and product owner at RV. His interests include automated system analysis via symbolic model checking, rigorous software development via carefully designed development practices, and applying these techniques to the software used in the other sciences (eg. physics, biology). He strongly believes that programming languages and system description languages should not be put together in an ad-hoc manner, rather they should be carefully designed using state of the art language-building tools.
Brandon Moore
Formal Verification Engineer
Brandon Moore completed his Ph.D. at UIUC, working with Grigore to develop formal verification techniques which require only a language definition to verify programs against specific implementations or versions of a programming language. He uses proof assistants like Coq, Isabelle and Agda, on a regular basis, and thinks that proofs by coinduction are beautiful and elegant. Before UIUC he worked at Yahoo! Inc. on latency-critical servers. Brandon received his B.S. in computer science and in mathematics at Caltech.
Daejun Park
Research Collaborator
Daejun Park is a Senior Blockchain Security Engineer at a16z crypto, developing formal methods and tools for web3 security to help portfolio companies in particular and the web3 community in general to raise their security bar. Prior to joining a16z crypto, he was a Director of Formal Verification at Runtime Verification, where he led a team of formal verification engineers and security auditors for smart contracts and consensus protocols. Early in his career, he was a founding member of another tech startup Sparrow, where he designed and implemented static program analysis tools that detect memory safety errors for embedded systems software. He received a Ph.D. in Computer Science from the University of Illinois at Urbana-Champaign, and his B.S. and M.S. degrees from Seoul National University. His work on language-parametric program verification received the Distinguished Paper Award at OOPSLA'16.
Grigore Roșu
Founder & CEO
Grigore Roșu is a Computer Science professor at the University of Illinois at Urbana-Champaign (UIUC), where he leads the Formal Systems Laboratory (FSL). Previously, he was a scientist at NASA, where he coined the term runtime verification with his colleagues. He is interested in programming languages, formal methods, and software engineering, and especially in how to combine these to increase the safety, security, and dependability of computing systems. He was offered the NSF CAREER award, the UIUC outstanding junior award, the Dean's award for excellence in research, and several best paper awards. Grigore got his Ph.D. from the University of California at San Diego.
Yi Zhang
Software Engineer
Yi Zhang is interested in runtime verification and programming languages. He worked on DARPA HACMS, where his mission was to generate efficient monitors for cyber physical systems. He worked as a summer intern at Google in 2016 and 2017. In 2016, he joined the Laser team at Google and worked on Protocol Buffer instrumentation. In 2017, he joined the YouTube team and used TensorFlow to cluster regression testing reports. His goal at RV is to formalize the semantics of programming languages and virtual machines for smart contracts to execute on the blockchain, and use such semantics to verify smart contracts. In addition to his full time work at RV, Yi is wrapping up his Ph.D. at UIUC in formal semantics-based program verification.
