alpha0 sp. z o. o. is implementing project FENG.02.12-IP.02-0481/26, co-financed by European Funds, entitled “Preparation of a Eurogrant application planned under the Horizon Europe programme”.

What is the purpose of the project?

The project aims to prepare and submit a Eurogrant proposal under Horizon Europe in the HORIZON-CL3-2026-02-CS-ECCC-03 call, “Advanced cryptographic schemes and High-Assurance high-speed cryptographic implementations”. The project will produce the application documentation, while external contractors will prepare the specialised analyses required to establish the assumptions for the planned R&D work and its commercialisation.

What will the planned Eurogrant cover?

The planned Eurogrant will develop the concept, reference architecture and demonstrator of a “Formal Verification System for Post-Quantum Cryptography Software”. The solution will describe security requirements, automatically assess code correctness and produce machine-checkable evidence of conformity. The proposal will be submitted by a consortium coordinated by alpha0 sp. z o. o., together with two identified international consortium members. The planned Eurogrant duration is 36 months.

What is the purpose of the planned R&D work?

The R&D work will develop a new methodology, a unified language for specifying cryptographic requirements, and an environment for formally verifying implementations and usage of the ML-KEM and ML-DSA algorithms. The work will cover correct key and parameter use, integration and configuration error detection, and security evidence generation. A demonstrator will be designed and evaluated in laboratory conditions, measuring verification effectiveness, repeatability and computational and timing overhead.

Scope of the planned Eurogrant

The planned Eurogrant will in particular involve:

• developing a formal security-requirements model for post-quantum cryptography implementations, including key usage, algorithm parameters, error handling and secret storage;
• developing a unified specification language for expressing cryptographic code correctness and security requirements;
• defining formal verification rules for implementations and usage of ML-KEM and ML-DSA;
• combining automated code analysis with formal methods and machine-checkable correctness evidence;
• developing methods for detecting integration, configuration and migration errors when moving from classical to post-quantum cryptography;
• improving HACS tools and defining how to integrate them into software design, development, review and update workflows;
• building a demonstrator with an integration interface, verification rules, example specifications, reporting and evidence-package generation;
• evaluating the demonstrator in use cases involving secure connections, software-component signatures and protected updates;
• validating the solution on correct and deliberately flawed implementations, measuring nonconformity detection, performance and repeatability.

What will the planned Eurogrant deliver?

The planned Eurogrant is expected to deliver a formal model of security requirements, a unified specification language, a verification-rule set, a software demonstrator and examples of machine-checkable correctness proofs. It will also deliver an assessment methodology, validation reports, technical documentation and deployment guidance to support the secure use of post-quantum cryptography.

What will the project deliver?

The project will prepare and submit a Eurogrant proposal under Horizon Europe in compliance with the requirements of the specified call, together with application documentation and specialised analyses performed by external contractors. Proposal preparation will also include necessary translations, expert consultations and any required supplements.

The direct beneficiary of these results will be alpha0 sp. z o. o., which will use the documentation to apply, as consortium coordinator, for R&D funding for a formal verification system for post-quantum cryptography software.

Project funding