Semi-Formal Development: The Cardano Wallet
2018年 6月 4日 17 分で読めます
Please note: this post originally appeared on the Well-Typed blog.
TL;DR: A combination of formal modelling and testing using QuickCheck is a powerful tool in the design and implementation of high assurance software. Consistency of the model can be checked by testing invariants, and the real implementation can be tested by comparing it against the model.
As part of our consulting work for IOHK, Well-Typed have been working with IOHK on the design and implementation of the new version of the Cardano cryptocurrency wallet. As a crucial component of this process, we have written a semi-formal specification of the wallet: a mathematical model of the wallet along with…
Writing a High-Assurance Blockchain Implementation
Guest blog from Edsko de Vries, who is working on the high assurance implementation of the Ouroboros blockchain protocol
2017年 11月 3日 9 分で読めます
Writing a High-Assurance Blockchain Implementation - Input Output
In our previous blog post Cryptocurrencies need a safeguard to prevent another DAO disaster we discussed the need for high assurance development of cryptocurrencies and their underlying blockchain protocols. We also sketched one way in which one might go about this, but we did not give much detail. In this follow-up blog post we delve into computer science theory a bit more…
最新の記事
Input | Output chief scientist receives prestigious Lovelace computing award 筆者： Fergie Miller
3 December 2024
Delivering change in Ethiopia: lessons and reflections 筆者： Staff Writer
28 November 2024
Applying formal methods at Input | Output: real-world examples 筆者： James Chapman
26 November 2024