Formal Methods for Security: Model Checking and Proofs

Testing and code review sample a handful of behaviours, while the security failures that hurt most often hide in rare interleavings, protocol corner cases and policy combinations nobody thought to test. Formal methods use mathematical models and machine-checked reasoning to cover every behaviour of a model, not just the ones a test suite happens to exercise. They are no longer confined to research: verified cryptographic code ships in Firefox and the Linux kernel, TLA+ has found data-loss bugs in cloud storage designs, and automated reasoning evaluates cloud access policies millions of times a day. This guide explains the main techniques, where they pay off in security, how to read a proof claim critically, and how a security team can adopt them without a dedicated research group. It is written for security architects, engineering leads and identity teams, and it goes deeper than the Security Architecture Review Guide, which it complements.

Key takeaways

Formal methods check all behaviours of a model. Model checkers explore every reachable state up to a bound, and theorem provers prove properties for all inputs, which is why they find bugs that survive review and months of testing.
Most organisations should consume formal methods before producing them. Choosing verified components (cryptographic libraries, kernels, policy engines) and using automated policy reasoning tools gives most of the value with little specialist effort.
Policy reasoning is the identity team's entry point. SMT-based analysis of IAM policies can prove that no policy grants public access or that a change adds no new access, which is exactly the question NHI permission reviews struggle to answer.
A proof is only as good as its model and assumptions. Verified code can still be undermined by an incomplete specification, unverified boot or assembly code, hardware behaviour or side channels.
Specify designs early. A short TLA+ or protocol model written before implementation is cheap, and AWS engineers reported useful results within two to three weeks of starting to learn TLA+.

What formal methods are

A formal method has three parts: a precise model of the system (a specification, a protocol model, a policy translated into logic), a precise statement of the property that should hold (no secret leaks, no two nodes both believe they are leader, no principal outside the organisation can read the bucket), and a tool that checks the property against the model mechanically. CyBOK treats this as its own knowledge area, Formal Methods for Security, within the Systems Security group.

Technique	What it does	Example tools	Typical security use	Effort
Specification and model checking	Explores every reachable state of a design model and reports a counterexample trace if a property fails	TLA+ with the TLC model checker; PlusCal for an algorithm-like syntax	Distributed protocols, replication, failover, lock and lease designs, key rotation workflows	Days to weeks per design
Interactive theorem proving	Proves properties for all inputs with machine-checked proofs	TLAPS (TLA+ proof system), Isabelle/HOL, Coq/Rocq, Lean, F*	Kernels, cryptographic libraries, authorisation language semantics	Months to years; specialist skills
Symbolic protocol verification	Models a protocol and an attacker who controls the network, then proves secrecy or authentication properties or finds attacks	Tamarin, ProVerif	Authentication and key exchange protocols (TLS 1.3, 5G-AKA, Noise, EMV)	Weeks per protocol
SMT-based automated reasoning	Translates a policy or program fragment into logic and asks a solver whether any input violates a property	Zelkova (AWS), Z3 and cvc5 solvers, Cedar analysis	Access policy checks, configuration verification, change impact (does this change grant new access?)	Push-button once built
Verified implementation and extraction	Code proven correct against a specification, then compiled to C or assembly	HACL* (F* to C), Vale and EverCrypt	Cryptographic primitives used by browsers, kernels and VPNs	Consumed as a library

Model checking answers "is there any sequence of steps, within these bounds, that breaks the property?" Theorem proving answers "does the property hold for every case, with no bounds?" SMT-based reasoning sits in between: it is fully automatic for the restricted languages it supports, such as access policies, and returns either a proof or a concrete counterexample.

Where formal methods pay off in security

Problem area	Why testing struggles	Method	Documented example
Distributed system designs	Failures interleave with normal processing in an astronomical number of orders	TLA+ model checking	AWS used TLA+ on DynamoDB and S3 designs; one DynamoDB data-loss bug needed a 35-step trace and had passed design review, code review and testing
Authentication and key exchange protocols	Attacks depend on an adversary combining messages across sessions	Symbolic verification	Tamarin was used in the analysis or development of TLS 1.3, 5G-AKA, Noise, EMV and Apple iMessage
Cryptographic code	Bugs appear on rare inputs (carry propagation, edge values) and timing leaks are invisible to functional tests	Verified implementation	HACL* is written in F* and compiled to C; code from the project is used in Firefox NSS, the Linux kernel, mbedTLS and WireGuard
Operating system kernels and separation	Whole classes of memory bugs and information flows	Interactive theorem proving	seL4's proofs run from specification down to binary code and cover properties from functional correctness to absence of information leakage
Access policies	Policies combine wildcards, conditions, deny statements and resource policies; reviewers cannot enumerate all requests	SMT-based reasoning	Zelkova encodes AWS policy semantics into SMT and is invoked many millions of times daily (FMCAD 2018 paper)
Authorisation languages	Evaluation errors or type confusion in the policy engine itself	Proofs plus differential testing	Cedar's validator was modelled in Lean, validation soundness was proved, and the Rust implementation is differentially tested against the Lean model

Automated reasoning over IAM policies: the NHI angle

Non-human identities carry most cloud permissions, and their policies are written by automation, copied between environments and rarely reviewed line by line. The questions reviewers need answered are semantic: can anything outside the organisation assume this role, does this pipeline change grant new actions, can this service account write to production buckets? Automated reasoning answers those questions exactly for the policy language it models.

External access: AWS IAM Access Analyzer generates a finding for each resource-based policy that grants access to a principal outside the zone of trust (the account or organisation you choose). Sharing inside the zone is treated as safe and produces no finding. AWS documents that its internal access analysis uses automated reasoning to evaluate all IAM policies.
Change checks: custom policy checks compare or constrain policies before deployment. CheckNoNewAccess reports whether an updated policy grants new access compared with the existing version; CheckAccessNotGranted confirms that named actions are not allowed; CheckNoPublicAccess checks whether a resource policy can grant public access for a resource type. They run from the console, CLI and API, so they can gate pull requests for infrastructure as code. AWS charges per check.
Policy languages built for analysis: Cedar was designed so that validation is provably sound against a schema. Its documentation still lists errors validation does not prevent, such as integer overflow and missing entities, which is a good example of a proof claim stated with its limits. See the Policy-as-Code for Authorisation Guide.
How to use it for NHIs: write a small set of invariants for machine identities (no workload role trusts a principal outside the organisation; no CI role can modify IAM; no service account can read the secrets path of another tenant) and run them on every change, not only in quarterly reviews. See the IAM Access Analyzer Guide and the Least Privilege Techniques Guide.

The limit is the model boundary. Policy reasoning tells you what the policies permit; it does not tell you whether a leaked key is being used, whether a role is used at all, or whether an application enforces its own checks correctly. Pair it with unused-access analysis and runtime detection.

Reading a proof claim critically

"Formally verified" is a precise claim about a specific property, model and set of assumptions. Before relying on it, find out what each of those is.

Question	Why it matters	Example
What property was proved?	Functional correctness, memory safety, secrecy and constant-time execution are different claims	A correct cipher implementation can still leak keys through timing if secret independence was not part of the proof
What was verified: design, source or binary?	Compilers and build steps can introduce differences	seL4 proofs extend to binary code; most design-level TLA+ work verifies the model only
What is assumed?	Unverified parts are where residual risk lives	seL4 lists assembly code, boot code, the machine interface, hardware and DMA as assumptions outside the proofs
Which configuration and platform?	Proofs often cover a specific architecture and configuration	seL4 announced its security proofs complete on AArch64 in August 2026; other architectures have different coverage
Does the model match reality?	A model that leaves out a failure mode cannot find bugs in it	The AWS authors note that TLA+ verifies the model, not the executable code, and does not address emergent performance problems such as retry storms
What is the maintenance status?	Research code may not be production-supported	The HACL* site describes the projects as ongoing research and asks integrators to contact the maintainers first

Choosing an approach

Small organisation, no specialists: consume. Prefer verified or formally analysed components where they exist, turn on cloud policy reasoning tools, and ask suppliers what was verified and under which assumptions.
Platform or SaaS engineering team: add policy invariants as code to CI and write TLA+ models for the few designs where a bug means data loss or cross-tenant access: replication, failover, leader election, key rotation and token revocation flows.
Protocol or cryptography owner: if you design a new authentication or key exchange protocol, model it in Tamarin or ProVerif before release. Do not design custom protocols where a standard one with published analysis exists.
High-assurance product (defence, critical infrastructure, separation kernels): theorem proving and verified components are justified, and procurement or certification may expect formal design evidence. See the Common Criteria Evaluation Guide.

The deciding factors are the cost of a bug (data loss, cross-tenant exposure, key compromise), whether the component is concurrent or adversarial, and how stable it is. Formal effort is wasted on code that changes weekly and whose failures are cheap; it is well spent on a small, stable core that everything else trusts.

Adopting formal methods step by step

Pick one high-value target: a design that has already produced a subtle incident, or the policy set for your most privileged machine identities.
Write the property in plain language first: "no production role trusts an external account", "a revoked token is never accepted after propagation completes". Unclear properties are the most common reason models produce nothing useful.
Start with push-button tools: enable policy analysis and run change checks on infrastructure-as-code pull requests in report-only mode, then make failures blocking once false alarms are understood.
Model one design in TLA+ or PlusCal: keep the model small, check it with TLC at small bounds, and inject known bugs to confirm the model can find them.
Keep models with the code: store specifications in the same repository, review them with design changes, and rerun checks in CI.
Record assumptions: document what the model leaves out and cover those areas with testing, fuzzing and review.
Roll back safely: if a blocking policy check stalls delivery, return it to report-only while the invariant is corrected, rather than deleting it.

Measuring value

Coverage: percentage of privileged NHI policies covered by automated invariants run on every change.
Prevented changes: number of pull requests blocked by policy checks for new or external access, and how many were genuine issues.
Design defects found before code: counterexamples found in models of critical designs, compared with defects found later in testing or production.
Verified dependency share: proportion of cryptographic operations served by verified or formally analysed libraries.
Model freshness: percentage of specifications updated within one release of the design they describe.

Framework mapping

Framework	Reference	Relevance
NIST SP 800-53 Rev. 5	SA-17 Developer Security and Privacy Architecture and Design, with SA-17(1) Formal Policy Model and SA-17(3) Formal Correspondence	Explicit control enhancements for formal models of security policy and correspondence between specification and design
NIST SP 800-53 Rev. 5	SA-8 Security and Privacy Engineering Principles; SA-11 Developer Testing and Evaluation; AC-6 Least Privilege	Engineering assurance; policy reasoning as evidence of least privilege
NIST CSF 2.0	PR.PS-06 Secure software development practices; ID.RA-01 Vulnerabilities identified	Formal checks as part of the development lifecycle and vulnerability identification
CyBOK 1.1	Formal Methods for Security knowledge area	Body of knowledge reference for the techniques on this page

Common failure patterns

Proving the wrong property: the model is checked thoroughly against a property that does not capture the real security goal, for example authentication without freshness, so replay remains possible.
Treating "verified" as "secure": relying on a verified component while ignoring its stated assumptions, configuration requirements or unverified boot and hardware layers.
Models that drift: a specification written once for a design review and never updated, so the code moves on and the model describes a system that no longer exists.
Policy checks outside the pipeline: running policy analysis as a quarterly report rather than on every change, so over-permissive NHI policies run in production for months before anyone sees the finding.
Wrong zone of trust: configuring external-access analysis at account level when sharing should be judged at organisation level, or the reverse, producing either noise or blind spots.
Too big a first project: attempting a full proof of a large system, stalling, and concluding formal methods do not work, when a small model of the riskiest design would have found real bugs.

Practitioner checklist

List the components whose failure means data loss, key compromise or cross-tenant access, and rank them for formal analysis.
Prefer verified or formally analysed cryptographic libraries and record which are in use.
Enable cloud policy analysis with the correct zone of trust, and review findings for machine identities first.
Write 5-10 policy invariants for NHIs and run them as change checks on every infrastructure-as-code pull request.
Model at least one critical distributed design in TLA+ or PlusCal and keep the model in the repository.
For any custom authentication or key exchange protocol, require symbolic analysis before release.
For every "formally verified" supplier claim, record the property, the level (design, source, binary) and the assumptions.
Cover assumptions and unmodelled areas with fuzzing, testing and review.

Formal Methods for Security Guide: Model Checking, Proofs and Policy Reasoning