Blockchain Advisory Services
“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:
Blockchain advisory team members
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ș 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'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 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 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 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 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 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.