Specification and Verification of a Blockchain Light Client

This lecture covers the design, implementation, and formal verification of distributed systems, focusing on verifiable distributed systems and organizations. Topics include Tendermint, IBC, Apalache, light client constraints, proof of stake, block verification, light client roles, and the use cases of the light client in IBC. The lecture also discusses the TLA+ specification, Stainless verification tool, light client core verification, formal verification of the light client core, and the development process with formal verification. The presenter emphasizes the Verification Driven Development approach, interoperability of the implementation, testing strategies, N-version programming, implementation and verification statistics, limitations, and conclusions.

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related lectures (3)

Related concepts (63)

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to u

Proof of stake

Proof-of-stake (PoS) protocols are a class of consensus mechanisms for blockchains that work by selecting validators in proportion to their quantity of holdings in the associated cryptocurrency. This is done to avoid the computational cost of proof-of-work (POW) schemes. The first functioning use of PoS for cryptocurrency was Peercoin in 2012, although the scheme, on the surface, still resembled a POW. For a blockchain transaction to be recognized, it must be appended to the blockchain.

Proof of work

Proof of work (PoW) is a form of cryptographic proof in which one party (the prover) proves to others (the verifiers) that a certain amount of a specific computational effort has been expended. Verifiers can subsequently confirm this expenditure with minimal effort on their part. The concept was invented by Moni Naor and Cynthia Dwork in 1993 as a way to deter denial-of-service attacks and other service abuses such as spam on a network by requiring some work from a service requester, usually meaning processing time by a computer.

Test-driven development

Test-driven development (TDD) is a software development process relying on software requirements being converted to test cases before software is fully developed, and tracking all software development by repeatedly testing the software against all test cases. This is as opposed to software being developed first and test cases created later. Software engineer Kent Beck, who is credited with having developed or "rediscovered" the technique, stated in 2003 that TDD encourages simple designs and inspires confidence.

Proof of space

Proof of space (PoS) is a type of consensus algorithm achieved by demonstrating one's legitimate interest in a service (such as sending an email) by allocating a non-trivial amount of memory or disk space to solve a challenge presented by the service provider. The concept was formulated in 2013 by Dziembowski et al. and (with a different formulation) by Ateniese et al.. Proofs of space are very similar to proofs of work (PoW), except that instead of computation, storage is used to earn cryptocurrency.

Acceptance test-driven development

Acceptance test–driven development (ATDD) is a development methodology based on communication between the business customers, the developers, and the testers. ATDD encompasses many of the same practices as specification by example (SBE), behavior-driven development (BDD), example-driven development (EDD), and support-driven development also called story test–driven development (SDD). All these processes aid developers and testers in understanding the customer's needs prior to implementation and allow customers to be able to converse in their own domain language.

Blockchain Basics: Financial Applications FIN-413: Financial applications of blockchains and distributed ledgers

Delves into blockchain basics and financial applications, covering hash puzzles, Merkle trees, proof of stake, and smart contracts.

Limitations of Bitcoin and Increasing TPS CS-438: Decentralized systems engineering

Discusses the limitations of Bitcoin and ways to increase transaction processing speed.

Ethereum Consensus Protocols: Security and Attacks

Explores Ethereum consensus protocols, vulnerabilities, and solutions for ledger system security.