EthSystems completa la verifica formale del privacy pool, coprendo il bytecode di Sepolia

L'agenzia di tecnologia della privacy di Ethereum, EthSystems, ha annunciato di aver completato la verifica formale del suo privacy pool, coprendo l'intera gamma dalla specifica scritta al bytecode sulla rete di test Sepolia. Durante il processo di verifica sono stati utilizzati diversi strumenti: modelli, circuiti e hash utilizzano Lean, i contratti utilizzano Halmos e Kontrol, i portafogli utilizzano Aeneas e Verus, e i validatori e il deployment sono stati verificati tramite ricostruzione byte per byte. Il double spending e la conservazione del valore sono stati verificati dalla macchina dei teoremi Lean. Durante la verifica sono stati riscontrati 6 problemi, di cui 3 riguardano gli strumenti di verifica stessi. Il team ha anche elencato le assunzioni su cui si fa ancora affidamento, tra cui l'assenza di collisioni negli hash, il rifiuto delle prove falsificate da parte dei validatori e la coerenza del comportamento dei contratti con il modello.

Questo contenuto è fornito a solo scopo informativo generale e non costituisce consulenza finanziaria, di investimento, legale o fiscale. Qualsiasi evento, ricompensa, promozione online o informazione correlata menzionata nel presente documento non deve essere considerata una raccomandazione, una sollecitazione o un invito ad acquistare, vendere, fare trading o altrimenti negoziare criptovalute. Le criptovalute sono altamente volatili e possono comportare perdite. La disponibilità dei servizi, dei prodotti e degli eventi correlati di WEEX può variare a seconda della regione. È tua responsabilità assicurarti che la tua partecipazione sia conforme alle leggi e ai regolamenti locali applicabili.