We have CTO of Ren, Loong Wang, on to educate us on their token transfer protocol. Ren is building a system that allows a user to transfer a token from one change to another, without the drawbacks found in techniques like atomic swaps. They have a network of "dark nodes" which run on their virtual machine, RenVM, to computer across the transactions and share data over the network. Interesting technology with many use cases!

Links

• https://renproject.io/
• https://twitter.com/bzlwang

Donate

• https://donate.hashingitout.stream

Champion of decentralization, Zaki Manian, rejoins us for updates on Cosmos since their Mainnet launch. We dive into the design principles of Cosmos, their consensus mechanisms, incentivisation model, and how to integrate your decentralized application into the Cosmos Network. We also learn more about who is currently using Cosmos and how, what Zaki and Cosmos will be speaking on at NYC Blockchain Week events, as well as how Cosmos differentiates itself from other technologies being produced. Riveting as always!

Show Links:

• MIT talk about launch
• cosmos
• Zaki's Twitter

We bring you another brilliant mind on the show for this episode! Russell O'Connor, developer of Blockstream's Simplicity programming language for Bitcoin, dives deep into formal verification topics. We learn about the language design principles driving Simplicity, how formal verification plays an integral role in making the language suitable for securely automating Bitcoin transactions, and the challenges in creating a smart contract script for Bitcoin. We get a glimpse into the future of blockchain automation, and he elucidates what is being done right and what could be done better in blockchain platforms to place security first in smart contract design.

Links

• Simplicity's Github
• Simplicity Publication -- PLAS 2017
• Simplicity presentation -- BPASE 2018 (slides)
• Illustration of formal verification using Simplicity -- Scale by the Bay 2018 (slides)
• Enhancing Bitcoin Transactions with Covenants -- The Financial Crypography 2017 Workshop
• Andrew Appel's Verified Software Toolchain for formal verification of C
• The Coq proof assistant
• Mooly Sagiv's Modularity for Decidability: Implementing and Semi-Automatically Verifying Distributed Systems

We are excited to have the Kadena team back on with an update. The erudite Stuart Popejoy and brilliant Emily Pillmore speak more on Pact, the smart contract language with built-in formal verification used in the Kadena Chainweb. We learn more about formal verification: what it means, how it works, and a bit of its limitations. They also give us an update on Chainweb itself and talk us through some of the challenges since we last spoke... AND their innovated solutions to those challenges!

Links:

• http://kadena.io
• https://kadena.io/en/resources/
• https://twitter.com/kadena_io
• https://twitter.com/sirlensalot
• https://twitter.com/emi1ypi
• EVM is fundamentally unsafe
• Turing Complete vs Turing Incomplete

Sponsorship:

We'd like to thank our sponsor for this episode Trail of Bits for supporting us. Now go sign up for automatic github-integrated smart contract security at www.crytic.io !