High Assurance Cryptographic Software and Smart Contracts

What was the project about?

Cryptographic Software drives the internet, web3 and many other service and trillions of kroner depend on it working correctly. But bugs in cryptographic implementations opens up to the possibility to `print money’ (create crypto-coins) or steal hundreds of billions of kroners from smart contracts (small programs running on a blockchain). This is why high assurance cryptographic software (HACS) is used in prominent projects, like the major browsers and the Linux kernel. ​

HACS is an emerging research field between academia and industry and it was the aim of the partners in this project to advance HACS, specifically for applications in Fintech (blockchain), but also more widely to work on formal methods for the rust programming language.

Several private partners contributed to the project and advanced HACS by:​

  • Contributing to the open source library​ (like hacspec and libcrux)
  • Developing a framework to ensure the quality of rust computer programs​
  • Developing joint best practices for certified smart contracts, especially focusing on the rust language​

Concordium and Partisia is planning to switch to these new libraries and the partners plan to continue their collaboration as they expect, that HACS will become more and more important as regulation around security by design catches up (e.g. CRA, EUCC, The Data Act for Smart Contracts).

The project was led by Bas Spitters, Associate Professor at Aarhus University and lead of the Concordium Blockchain Research Center at Aarhus University (CoBRA). He is internationally recognized for his research in the verification of blockchain technologies.

Host Institution(s):

Aarhus University​

Principal Investigators:

Bas Spitters​


Concordium, Partisia and Cryspen​


200.000 DKK

Project Period


Project outcomes


​Contributions to the libcrux library can be found on Github. Find here

Presentation of work at the Real World Cryptography 2023 Conference (Barbosa et al.). Find here

Presentation: Specifying Smart Contract with Hax and ConCert (Hansen and Spitters, 2024) Find here

Additional background material

Blogpost about the introduction of hax. Find here

In the news


No items found.