2026-04-08·8 min read·sota.io team

EU Cyber Resilience Act 2027: Why Formal Verification Is the Right Tool for CRA Compliance

The EU Cyber Resilience Act — Regulation (EU) 2024/2847 — entered into force on 10 December 2024. It applies to every product with digital elements placed on the EU market: connected devices, software components, firmware, APIs, mobile apps, desktop applications. If your software is sold or distributed in the EU, the CRA applies to you.

The enforcement timeline has two critical dates:

11 September 2026: Articles 14 and 15 apply — vulnerability disclosure obligations and security incident reporting begin.
11 December 2027: Full compliance required — essential cybersecurity requirements (Annex I) apply to all products.

With September 2026 now five months away, vulnerability disclosure obligations are the immediate concern for most software teams. December 2027 is the larger structural deadline — and it is a design requirement, not a documentation checkbox.

Annex I, Part I of the CRA requires that products with digital elements are "designed, developed and produced to ensure an appropriate level of cybersecurity based on the risks." The first specific requirement: they must be "delivered without any known exploitable vulnerabilities."

That phrase — "without any known exploitable vulnerabilities" — is where formal verification becomes the correct tool. Here is why.

What CRA Annex I Actually Requires

Annex I of the CRA is divided into two parts: security requirements for the product itself (Part I) and security requirements for vulnerability handling (Part II).

Part I — Product security requirements include:

Delivered without known exploitable vulnerabilities
Security by default configuration
Protection of confidentiality and integrity of stored, transmitted, and processed data
Protection against unauthorised access, including authentication and access control
Protection of availability of essential functions (denial of service resistance)
Minimisation of attack surface
Ability to receive security updates

Part II — Vulnerability handling requirements include:

Identify and document vulnerabilities throughout the product lifecycle (Art. 14: starting September 2026)
Address vulnerabilities without undue delay
Apply security updates for the expected product lifetime
Disclose vulnerabilities to ENISA within 24 hours of learning of active exploitation

The Part I requirements are the ones that demand formal verification. Specifically: "delivered without any known exploitable vulnerabilities" and "minimisation of attack surface" cannot be satisfied by testing alone.

The Testing Problem

Testing finds vulnerabilities you have found. A penetration test, a fuzz campaign, a CVE scan — these tell you about vulnerabilities your testing process discovered. They cannot tell you about the vulnerabilities your testing process did not discover.

CRA Annex I does not say "delivered without any vulnerabilities discovered in your test suite." It says "without any known exploitable vulnerabilities" — and the burden of knowing is on the manufacturer.

The two most common causes of exploitable software vulnerabilities are memory safety errors and authentication logic errors. Both are tractable targets for formal verification:

Vulnerability class	Testing coverage	Formal verification coverage
Buffer overflow	Finds some instances in tests	Proves absence across all inputs
Use-after-free	Finds some instances in tests	Proves ownership invariants hold
Integer overflow leading to buffer over-read	Rarely caught by tests	Provably absent with contracts
Authentication bypass via state machine error	Depends on test coverage of state space	TLA+ exhaustively checks all states
Null dereference	Finds some instances in tests	VeriFast/Frama-C prove absence
Race conditions in concurrent code	Highly non-deterministic, hard to reproduce	TLA+ / CBMC prove absence

Formal verification does not replace penetration testing. It addresses the class of vulnerabilities that testing structurally cannot eliminate — which is exactly what CRA Annex I requires you to address.

The Tools: Formal Verification for CRA Compliance

These are production-deployed EU-origin tools used in automotive, avionics, medical devices, and nuclear systems. They are actively maintained by EU research institutions.

VeriFast (KU Leuven 🇧🇪, Frank Piessens)

VeriFast is a modular program verifier for C and Java, developed at KU Leuven in Belgium. It uses separation logic to reason about heap memory — proving that a C program cannot perform buffer overflows, use-after-free operations, or double-frees for any input satisfying the preconditions.

/*@ requires chars(buf, n, _) &*& n >= 0 &*& count <= n;
  @ ensures  chars(buf, n, _);
  @*/
void safe_fill(char *buf, int n, int count, char val) {
  for (int i = 0; i < count; i++)
    //@ loop_invariant 0 <= i &*& i <= count &*& chars(buf + i, n - i, _);
    buf[i] = val;
}

VeriFast proves that safe_fill never writes outside the bounds of buf for any value of count ≤ n. This directly satisfies CRA Annex I Part I requirement 1 — "delivered without any known exploitable vulnerabilities" — for the buffer overflow class.

CRA relevance: Memory safety proofs eliminate the most common class of CWE vulnerabilities (CWE-119, CWE-125, CWE-787) that CRA Annex I targets.

Frama-C (CEA/INRIA 🇫🇷, Saclay and Paris)

Frama-C is a C code analysis and verification framework developed by CEA (Commissariat à l'énergie atomique) and INRIA. Its WP plugin uses weakest precondition calculus to verify ACSL (ANSI/ISO C Specification Language) annotations against C implementations.

Airbus uses Frama-C for avionics software verification at DO-178C Level A. The tool is developed and maintained entirely by French public research organisations.

/*@ requires \valid(input) && \valid(output);
  @ requires size > 0 && size <= MAX_PACKET_SIZE;
  @ ensures  \valid(output + (0 .. size-1));
  @ assigns  output[0 .. size-1];
  @*/
void process_packet(const uint8_t *input, uint8_t *output, size_t size) {
  for (size_t i = 0; i < size; i++)
    output[i] = transform(input[i]);
}

The \valid predicate and assignment clause formally document that process_packet only writes to the declared output range — no buffer overruns, no out-of-bounds writes, regardless of input.

CRA relevance: Frama-C's WP plugin produces formal proofs that specific vulnerability classes (buffer overflows, out-of-bounds accesses, uninitialised reads) are absent from C code — essential for network-facing components subject to CRA Part I requirements 1, 3, and 6.

CBMC (Daniel Kroening 🇬🇧, Oxford / ETH Zürich)

CBMC (C Bounded Model Checker) is an automatic verification tool for C and C++ programs, developed at Oxford and ETH Zürich. It translates C code and safety properties into SAT/SMT problems, then uses a solver to either prove the property holds or produce a counterexample.

CBMC is particularly effective for finding integer overflow vulnerabilities, which are a common source of memory corruption exploits:

cbmc packet_parser.c \
  --property "no-integer-overflow" \
  --property "no-buffer-overflow" \
  --unwind 16
# → VERIFICATION SUCCESSFUL (or produces a counterexample trace)

CBMC is integrated into industrial verification workflows at Arm, AWS (for verifying C-based cryptographic code), and European automotive suppliers.

CRA relevance: CBMC directly checks for the vulnerability classes that CRA Annex I targets — buffer overflows, integer overflows leading to memory corruption — and produces machine-checkable proof results that can be stored as compliance documentation.

SPARK Ada (AdaCore 🇫🇷, Paris)

SPARK is a formally-verifiable subset of Ada, developed by AdaCore (Paris, founded 1994). Every function carries contracts — preconditions, postconditions, loop invariants — verified by GNATprove, which produces formal proofs using Why3 and Alt-Ergo.

SPARK Ada is the standard verification language for systems where compliance demands are even stricter than the CRA:

Aviation: DO-178C Level A
Railway: EN 50128 SIL 3/4
Automotive: ISO 26262 ASIL-D
Medical devices: IEC 62304
Nuclear: IEC 61513

For connected products subject to CRA — firmware, IoT devices, embedded controllers — SPARK provides a complete verification environment:

function Parse_Length (Packet : Bytes; Max : Positive) return Natural
  with Pre  => Packet'Length >= 2 and Max <= Packet'Length,
       Post => Parse_Length'Result <= Max
is
  Raw : Natural := Natural (Packet (Packet'First)) * 256
                 + Natural (Packet (Packet'First + 1));
begin
  return Natural'Min (Raw, Max);
end Parse_Length;

GNATprove verifies that Parse_Length always returns a value ≤ Max — eliminating the class of length-field parsing vulnerabilities that historically underlie many buffer overflow exploits in network protocols.

CRA relevance: SPARK's contract verification is the most complete industrial solution for Annex I Part I requirements 1 (no known exploitable vulnerabilities), 3 (data integrity), and 4 (access control) in embedded and firmware contexts.

TLA+ (Leslie Lamport, Microsoft Research)

TLA+ is a specification language for modelling concurrent and distributed systems. The TLC model checker exhaustively explores all reachable states of a protocol specification, proving that safety properties hold in all executions.

For CRA compliance, TLA+ addresses a vulnerability class that memory-level tools do not: authentication and session management logic errors. These are typically state machine errors — sequences of valid operations that, combined in an unexpected order, reach an unauthorised state.

---- MODULE AuthProtocol ----
VARIABLES state, token, authenticated

TypeInvariant ==
  state \in {"initial", "challenged", "authenticated", "revoked"}

SecurityProperty ==
  \* A revoked session can never reach authenticated state again
  [] (state = "revoked" => [] ~(state = "authenticated"))
====

TLA+ can prove that your authentication protocol never allows a revoked session to re-authenticate — regardless of the order, timing, or concurrency of operations. This directly addresses CRA Annex I requirement 4 (authentication and access control) and requirement 7 (minimisation of attack surface through correct state machine design).

CRA relevance: Proves authentication protocol correctness across all reachable states — the class of logic errors that penetration testing rarely finds but that account for a significant fraction of CVEs.

CPAchecker (TU Munich 🇩🇪, Dirk Beyer)

CPAchecker is a software verification platform developed at TU Munich. It implements Configurable Program Analysis — a framework that allows different verification algorithms (k-induction, predicate abstraction, symbolic execution) to be combined for a given verification goal.

CPAchecker has won the International Competition on Software Verification (SV-COMP) multiple times and is used for verifying Linux kernel drivers and automotive software.

cpachecker \
  -config config/sv-comp23--memorysafety.properties \
  -spec ../properties/memsafety.prp \
  network_driver.c
# → Verification result: TRUE (no memory safety violations found)

CRA relevance: CPAchecker's memory safety configuration directly addresses CRA Annex I Part I requirements — producing a verification result that can be stored as compliance documentation for embedded network drivers, firmware, and system software.

Mapping CRA Annex I to Formal Verification Tools

CRA Annex I Requirement	Tool	What It Proves
Part I.1: No known exploitable vulnerabilities	VeriFast, Frama-C, CBMC, CPAchecker	Memory safety: buffer overflows, use-after-free, integer overflows absent for all inputs
Part I.3: Data confidentiality and integrity	SPARK Ada, F* / EverCrypt	Cryptographic implementation correctness; data handling contracts hold
Part I.4: Authentication and access control	TLA+	Authentication protocol correct in all reachable states; no bypass possible
Part I.5: DoS resistance	TLA+	Resource allocation never leads to starvation or livelock under adversarial input
Part I.7: Minimise attack surface	Frama-C (WP), CBMC	Attack surface characterised by proof — no unspecified behaviours reachable
Part II.1: Identify vulnerabilities (Art. 14, Sep 2026)	All tools	Proof artifacts serve as structured vulnerability analysis documentation

The September 2026 Obligation: Vulnerability Identification Documentation

Article 14 of the CRA requires manufacturers to "identify and document vulnerabilities" in their products — starting September 2026. This is a documentation obligation: you must maintain a structured record of vulnerabilities identified throughout the product lifecycle, and report actively exploited vulnerabilities to ENISA within 24 hours.

Formal verification directly generates the documentation Art. 14 requires. When VeriFast proves that your C code contains no buffer overflows, that proof artifact — the annotated source, the proof check result, the specification — is a structured record of one class of vulnerabilities being absent. When CBMC returns VERIFICATION SUCCESSFUL for integer overflow checks, that result is a reproducible, machine-verifiable document.

This is more defensible than penetration test reports, which are point-in-time assessments. Formal verification results are reproducible against any version of the codebase — you can regenerate the proof for a new commit and confirm the property still holds.

Running CRA Compliance Pipelines on EU-Native Infrastructure

CRA compliance documentation — proof artifacts, verification results, vulnerability reports — is security-sensitive data. Storing it on US-headquartered infrastructure creates a structural exposure under the US CLOUD Act: a US company can be compelled to produce your vulnerability documentation under US law, without your knowledge and without going through EU mutual legal assistance procedures.

Running your formal verification CI/CD pipelines on EU-native infrastructure eliminates this exposure. The verification toolchain, the proof artifacts, the source code they verify, and the compliance documentation all remain under EU jurisdiction — no CLOUD Act risk.

# Deploy a VeriFast verification pipeline to EU infrastructure
sota deploy
# → VeriFast 21.04 container running on EU servers
# → Proof artifacts stored in managed EU PostgreSQL
# → CBMC results logged with commit hash + timestamp
# → Frama-C WP results stored alongside source snapshots
# → Full chain of custody under EU jurisdiction

sota.io is a German-incorporated PaaS running exclusively on EU infrastructure. Deploy any verification toolchain — VeriFast, Frama-C, CBMC, SPARK Ada, TLA+ — as containerised CI/CD pipelines, with managed PostgreSQL for storing proof artifacts and compliance records. GDPR-compliant by design, free tier available.

December 2027: What Full CRA Compliance Requires

By December 2027, all products with digital elements placed on the EU market must satisfy Annex I in full. For software products, this means:

Security by design documented. A technical file (Art. 31) demonstrating that the product was designed to meet Annex I requirements. Formal verification specifications and proof artifacts are the strongest possible evidence.
No known exploitable vulnerabilities at time of release. A verification toolchain integrated into CI/CD that checks each release against memory safety, authentication logic, and protocol correctness properties.
Vulnerability disclosure infrastructure operational. A coordinated vulnerability disclosure policy, a contact point for security researchers, and a pipeline for ENISA reporting — all active since September 2026.
Security update mechanism. For connected products, a means of delivering security patches for the expected operational lifetime.

For teams building software today — particularly teams building network-connected products, IoT firmware, APIs, or infrastructure software — the critical action is to start integrating formal verification into the development process now, not in 2027. Formal verification specifications are architectural commitments; they cannot be retrofitted to code written without them.

Where to Start

The most tractable entry point for CRA compliance is to apply formal verification to the security-critical surfaces of your product:

Network input parsing (VeriFast or Frama-C): Prove that all network-received data is handled within bounds before processing. Eliminates the largest class of remote exploitation vectors.
Authentication state machine (TLA+): Prove that your session management, token validation, and access control logic are correct across all possible request orderings.
Cryptographic implementation (EverCrypt or SPARK Ada): If you implement any cryptographic primitives, replace them with formally-verified alternatives. The EverCrypt library provides FIPS-validated, F*-verified implementations of AES-GCM, ChaCha20-Poly1305, and SHA-2/3.
Integer arithmetic in parsers and protocol handlers (CBMC or CPAchecker): Run bounded model checking on any code that performs arithmetic on externally-supplied values — sizes, lengths, indices.