Des membres de la Ethereum Foundation, George Kadianakis et Kev Wedderburn, ont publié un article intitulé « Ethereum TCB, Part One: Clients » sur le Forum de recherche Ethereum. D’après Foresight News, l’article définit la base de calcul de confiance (trusted computing base) comme l’ensemble des composants, spécifications, outils et hypothèses qui sont considérés comme dignes de confiance plutôt que prouvés, et examine comment le TCB du client Ethereum pourrait diminuer à mesure que la vérification formelle devient plus courante.

L’article plaide en faveur de la séparation des logiciels en modules « purs » faciles à vérifier, tels que la cryptographie et le SSZ, et en modules « sales » difficiles à vérifier, avec des effets de bord, tels que le réseau. Il indique que les modules sales doivent être traités comme non fiables, tandis que la vérification doit se concentrer sur les modules purs et repousser autant que possible la limite vérifiée vers la logique d’analyse du réseau, de la diffusion (gossip) et de la synchronisation.

L’article distingue également l’écriture de spécifications et la preuve de propriétés dans Lean4, ainsi que la preuve qu’une implémentation correspond à une spécification. Il présente plusieurs approches, notamment la traduction d’implémentations Rust vers Lean4, le traducteur et le compilateur Rust restant inclus dans le TCB ; l’écriture de modules dans Lean4 et leur extraction vers C ; la construction de clients directement dans Lean4 ; l’utilisation d’un assembleur RISC-V pour contourner les compilateurs conventionnels, tandis que le modèle ISA demeure dans le TCB ; ou l’utilisation d’un compilateur vérifié.