Zcash adopte la vérification formelle pour la mise à niveau Ironwood

2 min de lecture

Les développeurs de Zcash sont passés à la vérification formelle pour la mise à niveau du réseau Ironwood après qu’un défaut comptable récemment divulgué dans le pool Orchard a révélé les limites des audits conventionnels. Le défaut, découvert par Taylor Hornby, chercheur chez Shielded Labs, a été corrigé avant toute exploitation connue. L’équipe indique que la contrefaçon indétectable provient de défauts de spécification ou d’hypothèses cryptographiques, et non de bogues d’implémentation, et concentre les preuves sur la spécification cryptographique d’Ironwood en utilisant le vérificateur de théorèmes Lean avec des contributeurs de zkSecurity et du Zcash Open Development Lab. Ironwood fermera le pool blindé ancien, lancera un remplacement corrigé et utilisera une migration par tourniquet pour démontrer l’intégrité de l’offre lorsqu’il s’activera en juillet 2026.

Ironwood va vérifier formellement les spécifications pour prévenir toute contrefaçon indétectable.