Send in your ideas. Deadline October 1, 2024
Theme fund: NGI Assure
Start: 2022-04

Dual-level Specification Inference

Make formal verification more practical with dual-level Specification Inference

While formal verification of smart contracts gains traction, writing formal specifications can be equally if not more costly than writing code. Spec^2 is a specification inference framework that aims to automatically deduce a high-quality set of specs based on the code only. The inferred specs include both per-transaction pre-post conditions (low-level specs) and invariants on the blockchain-backed storage (high-level specs). Furthermore, the inferred specs should be similar to what experts might develop manually and can be easily examined by people without formal verification training. The funding from NLnet and NGI Assure will be used to prototype Spec^2 against the Move language and infer specifications for Move-based smart contracts.

  • The project's own website:

Run by CISPA Helmholtz Center for Information Security

Logo NLnet: abstract logo of four people seen from above Logo NGI Assure: letterlogo shaped like a tag

This project was funded through the NGI Assure Fund, a fund established by NLnet with financial support from the European Commission's Next Generation Internet programme, under the aegis of DG Communications Networks, Content and Technology under grant agreement No 957073.