Skip to content
Nenkin
Sign inStart free trial

EAL7: Formally Verified Design and Tested

EAL7 is the highest assurance level defined by Common Criteria (ISO/IEC 15408-3). It requires formal mathematical verification that the TOE design implements the security policy, and applies only to TOEs that are small and simple enough for such proof to be feasible.

Explore NenkinTracker to find certified products and compare their assurance levels, including EAL7.

Key facts

  • Assurance families covered: adds ADV_FSP.6 (formal functional specification), ADV_TDS.6 (formal TOE design), ADV_SPM.1 (formal security policy model), ADV_INT.3, ATE_DPT.4 (testing: implementation representation), AVA_VAN.5 over EAL6.
  • Typical product categories: small, security-critical components such as cryptographic kernels, separation kernels, and very focused embedded trust anchors.
  • Relative cost/time: extreme; formal methods work is measured in years of specialist effort.
  • Attack potential resisted: High.

What this level tests

Evaluators check a formal functional specification (ADV_FSP.6), a formal TOE design (ADV_TDS.6), and a formal security policy model (ADV_SPM.1), together with formal correspondence between them. Testing reaches the implementation representation (ATE_DPT.4). Vulnerability analysis remains at AVA_VAN.5 with High attack potential.

Because EAL7 assurance depends on complete formal verification, TOE scope is deliberately minimized. A typical EAL7 TOE covers a small, well-defined module, not an entire product family.

Typical product categories

EAL7 evaluations are very rare. They appear for small, formally tractable components such as separation kernels and focused cryptographic TOEs. Vendors usually ship a larger product in which an EAL7 TOE is embedded; the certificate applies to the TOE boundary, not the whole system.

Common misconceptions

EAL is an assurance level, not a security-strength rating. EAL7 means the TOE has been formally proven to implement a specific security policy under the assumptions of the Security Target. It does not mean the product is “unbreakable”. It means that, within the Security Target’s scope and assumptions, the design has been mathematically verified to implement the modeled policy. Flaws in the model, or outside the TOE boundary, are not covered.

Very few products reach EAL7. The overwhelming majority of high-assurance commercial certifications stop at EAL5+/VAN.5 or EAL6. EAL7 is specialized and often tied to defense, aerospace, or critical infrastructure programmes that mandate formal methods.

Comparison to adjacent levels

  • vs. EAL6: EAL7 replaces semiformal artifacts with formal ones across the functional specification, TOE design, and correspondence: the substantive leap is full mathematical verification.
  • vs. EAL beyond 7: CC defines no level above EAL7. Assurance higher than EAL7 is not expressible in the standard.

See the EAL Levels overview and the glossary for SAR vocabulary.

Frequently asked questions

What is EAL7?
EAL7 is the highest Evaluation Assurance Level defined by Common Criteria (ISO/IEC 15408-3). It requires a formal functional specification (ADV_FSP.6), a formal TOE design (ADV_TDS.6), and a formal security policy model (ADV_SPM.1), together with formal mathematical correspondence between them. Testing reaches the implementation representation (ATE_DPT.4) and vulnerability analysis stays at AVA_VAN.5 with High attack potential.
Why is EAL7 so rare?
EAL7 requires complete formal mathematical verification that the design implements the security policy. Formal methods work is measured in years of specialist effort and only feasible for small, simple TOEs. The overwhelming majority of high-assurance commercial certifications stop at EAL5+/AVA_VAN.5 or EAL6. EAL7 evaluations are usually tied to defense, aerospace, or critical infrastructure programmes that explicitly mandate formal methods.
What products are typically certified at EAL7?
EAL7 evaluations target small, formally tractable components such as separation kernels, focused cryptographic TOEs, and very narrow embedded trust anchors. Vendors usually ship a larger product in which an EAL7 TOE is embedded; the certificate applies to the TOE boundary, not the whole system. Examples are typically drawn from defense and high-integrity systems rather than general commercial IT.
Does EAL7 use formal methods?
Yes. Formal methods are the defining characteristic of EAL7. Evaluators check a formal functional specification, a formal TOE design, and a formal security policy model, and verify that mathematical correspondence between them holds. This goes beyond the semiformal notation of EAL5 and the partial formality of EAL6 (where only the policy model is formal). EAL7 is the only level where the full design chain must be formally verified.
Why are EAL7 TOEs small?
Formal mathematical verification scales poorly with complexity. Proving that a design implements a security policy requires a model small enough for the proof to be tractable and reviewable. For this reason, EAL7 TOEs are deliberately scoped to a minimal security-critical core, such as a separation kernel or cryptographic primitive, rather than a full product. Larger functionality is left outside the TOE boundary.
Is there an EAL above 7?
No. Common Criteria defines no assurance level above EAL7. Assurance higher than EAL7 is not expressible in the standard. Higher confidence in a specific deployment can come from combining EAL7 with additional measures such as operational monitoring, formal verification of components outside the TOE boundary, or independent code audit, but these sit outside the EAL ladder rather than extending it.
  • EAL1: Functionally TestedEAL1 is the lowest Common Criteria assurance level: independent confirmation that a product behaves as documented. Suitable when threats are low and trust in the vendor is adequate.
  • EAL2: Structurally TestedEAL2 is the workhorse Common Criteria assurance level: a high-level design review with independent vulnerability analysis, and the CCRA mutual-recognition cap for non-cPP evaluations.
  • EAL3: Methodically Tested and CheckedEAL3 extends EAL2 with development environment security controls, systematic life-cycle definition, and deeper test coverage. Less common than EAL2 or EAL4 in practice.
  • EAL4: Methodically Designed, Tested, and ReviewedEAL4 is the highest assurance level generally achievable on commercial products without re-engineering for assurance. Standard for smart cards, HSMs, and many government-used products.