Summary
Even though a real quantum processor is not there yet, there are already algorithms and programming languages dedicated to quantum computing, as well as proposals for verifying their properties.
Similarly, massively distributed applications among untrusted actors (blockchains and smart contracts) pose interesting problems in terms of verification.
A few references
- Palina Tolmach et al. A Survey of Smart Contract Formal Specification and Verification
- Luís Pedro Arrojado da Horta et al. WhylSon: Proving your Michelson Smart Contracts in Why3. In 2nd International Workshop on Formal Methods for Blockchains. 2020
- Zeinab Nehai, François Bobot. Deductive Proof of Industrial Smart Contracts Using Why3. In 1st International Workshop on Formal Methods for Blockchains. 2019
- Sylvain Conchon, Alexandrina Korneva, Fatiha Zaïdi Verifying Smart Contracts with Cubicle. In 1st International Workshop on Formal Methods for Blockchains. 2019
- Christophe Chareton et al. Qbricks: formal verification in quantum computing. In 1st International Workshop on Programming Languages for Quantum Computing. 2020