Spécification et vérification d'un client léger Blockchain

Cette séance de cours couvre la conception, la mise en œuvre et la vérification formelle des systèmes distribués, en se concentrant sur les systèmes et organisations distribués vérifiables. Les sujets abordés incluent Tendermint, IBC, Apalache, les contraintes clients légères, la preuve de participation, la vérification de bloc, les rôles clients légers et les cas d'utilisation du client léger dans IBC. La séance de cours traite également de la spécification TLA +, de l'outil de vérification Stainless, de la vérification du noyau du client léger, de la vérification formelle du noyau du client léger et du processus de développement avec vérification formelle. Le présentateur met l'accent sur l'approche du développement piloté par la vérification, l'interopérabilité de la mise en œuvre, les stratégies de test, la programmation de la version N, les statistiques de mise en œuvre et de vérification, les limites et les conclusions.