Musab A. Alturki, PhD

Musab A. Alturki, PhD

Senior Research Engineer @ Runtime Verification Inc. working on formal modeling and verification of blockchain and distributed systems

Two Papers Presented at FMBC’19

less than 1 minute read

Published:

We have two papers presented today at the 1st Workshop on Formal Methods for Blockchains, hosted by the 3rd Formal Methods World Congress on October 11, 2019 in Porto, Portugal:

  • “Towards a Verified Model of the Algorand Consensus Protocol in Coq” Musab A. Alturki, Jing Chen, Victor Luchangco, Brandon Moore, Karl Palmskog, Lucas Pena, and Grigore Rosu
  • “Statistical Model Checking of RANDAO’s Resilience to Pre-computed Reveal Strategies”. Musab A. Alturki and Grigore Rosu

More details about these papers can be found in the Publications page.

You May Also Enjoy

Best Practices For Securing Algorand Smart Contracts

less than 1 minute read

Published:

Smart contracts are the backbone of decentralized applications in Algorand. Ensuring their security against attacks and the safety of funds they maintain is critical to the success of these applications. In this talk, we give an overview of our world-class security auditing services at Runtime Verification, and reflect on our experiences auditing TEAL smart contracts in Algorand. We highlight some common programming pitfalls and provide some recommendations for best practices when developing TEAL smart contracts.

Added support for TEAL 5 in Tealer

less than 1 minute read

Published:

Tealer is a static analysis tool developed by Trail of Bits for analyzing the structure of smart contracts written in TEAL. I have added to Tealer support for the new features introduced in TEAL 5, including inner transactions.

Runtime Verification Audits Tinyman

less than 1 minute read

Published:

Runtime Verification announced Tinyman’s audit completioni, which was an effort I’ve had the pleasure of leading. Tinyman is a new project under development that focuses on bringing a decentralized trading protocol to the Algorand ecosystem and its community.