2-day, interactive online event with talks & workshops feat. all things Solidity - live from https://interspace.solidity-summit.ethereum.org

Franziska Heintel welcomes us to The Solidity Summit for April 2020 and gives us a quick overview of how to use the technology.

Chris gives us a quick tour of the roadmap for Solidity Summit for 2020.

Solc-verify is a source-level formal verification tool for Soldity smart contracts, developed in collaboration with SRI International. Solc-verify takes smart contracts written in Solidity and discharges verification conditions using modular program analysis and SMT solvers. Built on top of the Solidity compiler, solc-verify reasons at the level of the contract source code. This enables solc-verify to effectively reason about high-level functional properties while modeling low-level language semantics (e.g., the memory model) precisely. The contract properties, such as contract invariants, loop invariants, function pre- and post-conditions and fine grained access control can be provided as in-code annotations by the developer. This enables automated, yet user-friendly formal verification for smart contracts.

Learn about the K's background and the Solidity semantics in the K framework.

We will describe a platform for formally verifying smart contract correctness that can be integrated in CI/CD. Smart contracts and their invariants are converted into SMT formulas and the SMT solvers automatically identify vulnerabilities or generate mathematical proofs of correctness. We describe our experience applying this technology in the development phase and present bugs found and smart contracts verified. Our hope is that this SaaS technology can speed up the development process. The secret sauce for integrating in the CI/CD is that the invariants are reusable across different versions of the code, and targeting the low level EVM bytecode. This raises various technical challenges both at the conceptual level of the specification and at the technical level.

"dType is a decentralized & distributed type system for interoperable protocols.
ChainLens: Lens implementation for Ethereum as a browser and fine-grained search for smart contracts with a distributed database cache of types, functions, ABIs, code sources, and other metadata information. Available as a Remix IDE plugin, interoperable with other plugins.

Solidity is a relatively young language in a rapidly evolving space. The challenges it faces changed over time, greatly influencing the language design. In this brief talk, we examine the current language design processes in place and compare it against other models (i.e. language design committees).

"Yul+ is an extension to Yul, an intermediate language for the Ethereum Virtual Machine. It adds several quality of language features such as enums, constants, memory structures and injected methods. Our talk will go over the motivations, objectives and the features that Yul+ brings to the Ethereum ecosystem.

1) Yul overview, what we liked and what we needed
2) Motivations for an extension language
3) Objectives for a new language
4) Yul+ feature overview
5) Roadmap and future language exploration"

Learn more about the evolution and current state of the SOLL compiler project, which builds compiler front ends for YUL and Solidity, and backends for Ewasm and EVM. This talk includes a report on the technical progress made so far as well as future roadmaps and collaborations. It also discussed the web-based IDE developed for Solidity that allows fast dapp development and deployment on Ethereum compatible blockchains.