Detecting Inconsistencies in Arm CCA's Formally Verified Specification

Formal verification proves a system correct only relative to its specification, so if the specification itself contains a contradiction the proof is worthless and a "verified" system can still be insecure — yet giant, fast-changing specifications like Arm's confidential-computing firmware standard are validated by hand, and often before any implementation exists to test against; this paper (Samsung Research and Georgia Tech — Changho Choi, Xiang Cheng, Bokdeuk Jeong, Taesoo Kim) presents Scope, which treats the specification as the sole ground truth, translates it into a machine-checkable model and uses an SMT solver to find where the specification contradicts its own summary tables, uncovering 35 previously unknown bugs in Arm CCA's RMM specification, all confirmed by Arm.

The argument in one glance

Problem

A formal proof is only as trustworthy as the specification it is proved against

Formal verification is prized because it uses mathematics to prove a system correct, and it is sometimes treated as a silver bullet for building bug-free software — operating system kernels, file systems, hypervisors, and compilers have all been verified this way. But there is a catch that undercuts the whole promise: a proof only shows that an implementation matches its specification. If the specification itself is wrong — if it contains a contradiction or a subtly missing rule — then the proof can still succeed while the system it describes is broken or insecure, giving a dangerous illusion of safety. This is not hypothetical: a formally verified smart contract paid a one-million-dollar bug bounty for a critical vulnerability that traced back to a flawed invariant in its specification. The problem is getting worse as specifications grow. A particularly high-stakes example is Arm's Confidential Compute Architecture (CCA), whose Realm Management Monitor (RMM) firmware specification defines the trusted computing base for confidential computing on Arm — the foundation every security guarantee rests on. That specification is hundreds of pages, is authored and revised by a team of engineers, and is developed before any implementation exists (Arm mandates the spec first). So the very document that everything depends on is the hardest to check, and mistakes in it are exactly the mistakes that matter most.
What people did

Prove properties of the specification, or test it against an implementation

Two established approaches try to make specifications trustworthy. One is to formally prove properties of the specification itself, building machine-checked proofs about it. The other is to test the specification against a reference implementation, checking that they agree on many inputs. Both have been applied to architecture specifications, including Arm's.
Why it fell short

Proofs are hard to maintain, and testing needs an implementation that may not exist

Neither approach fits the reality of a document like the RMM specification. Formally proving properties of the specification is powerful but brittle to change: every time the architects add a feature or revise an interface — which happens frequently — the proofs must be laboriously updated, so the effort does not keep pace with the document. Testing the specification against an implementation assumes an implementation exists, but Arm's design process deliberately writes the specification before any code, so there is nothing to test against for new features. On top of these, there is no ready-made set of rules for what counts as a specification bug: the CCA threat model is complex, the security requirements are intricate, and a human would have to invent, by hand, the criteria for spotting a contradiction buried across hundreds of pages describing dozens of interface commands. And large language models, the obvious modern shortcut, turn out to be imprecise at this — they flag many things that are not real bugs. What was missing was an automated way to validate a specification using nothing but the specification itself, precise enough to be useful and cheap enough to re-run on every update.
This paper's idea

Treat the specification as ground truth and check it against its own summaries

Scope is an automated system that finds inconsistencies in a specification by combining formal modeling with rule-based checking, and its guiding insight is simple: if two statements in the same document contradict each other, at least one is wrong. Every part of a specification is meant to be accurate and consistent, so combining them should never produce a contradiction — and specifications conveniently contain a condensed statement of how the architects intend the system to behave, in the form of summarized tables and figures. Scope treats the specification as the sole ground truth (no implementation needed) and checks whether the detailed text agrees with those summaries. Concretely, it parses the RMM specification's formal content — written in Arm's Architecture Specification Language (ASL) — from the PDF, and translates it into Verus, a formal-verification framework, reconstructing a machine-checkable RMM model (using uninterpreted functions for helper predicates, a capability previously available only inside Arm). It then turns the summarized tables into proof queries and uses an SMT solver to check whether the model's ABI semantics for success conditions, failure conditions, dependency rules, and state transitions actually match those summaries; any failed assertion is a reported inconsistency. It also applies heuristic rules tailored to the specification (for example, that a command's recorded footprint must include everything its success conditions modify) to catch structural bugs. Applied to the RMM specification, Scope uncovered 35 previously unknown inconsistencies — some persisting up to 33 months, including security-critical flaws in ABI semantics and missing state transitions — all confirmed by Arm, and it improved inconsistency-detection precision by 7 to 40 times over leading large language models.

Why this problem is worth solving

The specification is the anchor for every formal guarantee, so a flaw there can silently negate an enormous amount of verification effort, and nowhere more so than in a security foundation.

The entire value of formal verification is that it reduces trust in a large, complex implementation to trust in a smaller, precise specification: prove the code matches the spec, and you are done. But that argument only holds if the spec is right. A contradiction or omission in the specification is invisible to the proof — the proof happily certifies that the implementation matches a broken description, and the resulting system can be exploitable while appearing bulletproof. This inverts the usual intuition that a verified system is safe. For something like Arm CCA’s RMM, the stakes are maximal: the RMM specification defines the trusted computing base of confidential computing on Arm, the layer whose correctness underpins the isolation guarantees that protect sensitive workloads in data centers. A subtle bug in that specification is not a local defect; it is a crack in the foundation that everything above inherits. So making the specification itself trustworthy is not a refinement of verification — it is the precondition for verification to mean anything at all.

What makes it hard is precisely the setting where it matters: a huge, evolving specification with no implementation and no rulebook for bugs.

Three properties of the RMM specification defeat the standard playbook. First, there is no implementation to compare against, by design — Arm writes the specification before the code, so testing-based validation has nothing to test. Second, the specification changes frequently, adding features and new interface commands, so any validation that requires heavy manual re-proving falls behind almost immediately; whatever checks it must be automated and cheap to re-run. Third, there is no predefined notion of what a specification bug even looks like: the document spans hundreds of pages of interface commands, state machines, and dependencies, and the CCA threat model is complex enough that a human cannot easily enumerate the consistency rules that ought to hold. Together these rule out proving properties by hand (too costly to maintain), testing against an implementation (none exists), and even naive use of language models (too imprecise to trust). The opening Scope exploits is that the specification is redundant in a useful way: it states the same behavior twice, once in detailed per-command semantics and once in summarized tables and figures, and those two must agree. Turning that redundancy into an automatic, precise check is the problem.

What people did before, and where it broke

Formally prove properties of the specification. Build machine-checked proofs that the specification satisfies desired invariants. Where it broke. The proofs are hard to maintain: every frequent design change forces a laborious re-proof, so the effort cannot keep pace with an evolving specification.
Test the specification against a reference implementation. Run both on many inputs and check they agree. Where it broke. It requires an implementation, but Arm mandates writing the specification before any code, so for new features there is nothing to test against.
Rely on human review across hundreds of pages. Have engineers read the specification and spot contradictions. Where it broke. The document is huge, authored by many people, and full of hard-to-trace dependencies, so inconsistencies from divergent interpretations slip through and persist for months or years.
Ask a large language model to find inconsistencies. Feed the specification to a modern LLM and let it flag bugs. Where it broke. The LLMs are imprecise here — they report many things that are not real bugs — so their low precision makes their output expensive to sift.
The gap. No automated method validated a specification using only the specification itself, precisely enough to be trusted and cheaply enough to re-run on every update.

How Scope works

Checking a specification against its own summaries with a solver

↓ →
new
↓ →
new
↓ →
new
↓ →
new
↓ →
new

The idea

Find bugs by checking two descriptions of the same thing for agreement. Scope’s engine is a consistency check: the specification describes each command’s behavior in detail and also summarizes it in tables, and any disagreement between the two exposes a bug in at least one of them. Locating defects by cross-checking two accounts that are supposed to match and flagging exactly where they diverge is the same undertaking the work on automatically locating inconsistent instructions between a real machine and its model (Examiner) covered elsewhere on this site pursues, turning a mismatch between two views into a precise bug report. Scope applies this within a single specification, playing the detailed semantics against the architects’ summarized view.

Turn an informal artifact into a formal model a solver can reason about. To check the specification mechanically, Scope translates its ASL text into a Verus model and hands the resulting logical conditions to an SMT solver, so contradictions become failed proofs rather than things a human must spot. Rendering a program or artifact into a precise, machine-verifiable form so an automated checker can prove or refute properties of it is the same principle the work on lightweight modular verification for WebAssembly-to-native compilation covered elsewhere on this site is built on, letting a formal tool do the reasoning a person cannot do reliably at scale. Scope builds such a model of the RMM specification, complete with uninterpreted functions, so the SMT solver can decide consistency automatically.

Guard the trusted foundation of confidential computing. The reason Scope targets the RMM specification is that it is the trusted computing base of Arm CCA — the piece whose correctness the whole confidential-computing security model depends on. Hardening the small, critical core that isolates and protects sensitive workloads, so that a flaw there cannot undermine everything above it, is the same idea the work on scalable and efficient I/O protection for trusted execution environments (SIOPMP) covered elsewhere on this site develops, fortifying the base that a confidential system stands on. Scope contributes the correctness side of that base, catching the specification bugs that would otherwise become security holes in the very layer meant to enforce isolation.

Following one inconsistency through Scope

Catching a contradiction in an ABI command

A trace, drawn from the paper, of how Scope finds an inconsistency in the RMM specification.

Step 1 of 5

Scope extracts an interface command from the specification

From the PDF, Scope parses an ABI command (for example, RMI_DATA_DESTROY) together with its failure and success conditions, which are written in Arm's Architecture Specification Language.

No implementation is consulted; the specification text is the only source.

Why it works

Using the spec as sole ground truth removes the need for an implementation. Testing-based validation has nothing to run when code does not yet exist → but Scope checks the specification against itself → so it can validate a specification written before any implementation.
Redundancy in the document turns bug-finding into a contradiction check. The specification states each behavior twice, in detail and in summary → and those two must agree → so a solver can find inconsistencies by detecting where they contradict.
A formal model plus an SMT solver makes the checking automatic. Consistency across hundreds of pages is beyond reliable human review → but translating ASL to Verus gives a model an SMT solver can reason over → so contradictions surface as failed proofs, not missed by a tired reader.
Rule-based heuristics catch what the solver does not. Some bugs are structural, not logical contradictions → but tailored rules (like footprint-must-match-modifications) check those directly → so Scope covers missing footprints, undefined outputs, and similar defects too.
Full automation keeps validation in step with the specification. Manual proofs fall behind frequent revisions → but Scope’s pipeline re-runs over each parsed update → so ongoing changes are validated continuously rather than drifting out of check.

What it costs (trade-offs and scope)

Not everything is automatic; some manual effort remains. Scope automatically processes the formal Interface and Types content (a majority of the pages), but the Usage part’s diagrams and descriptive text must be translated into queries by hand, and small patches are applied to fix type errors during model generation — so a human is still in the loop for part of the specification.
It detects contradictions, not all bugs. Scope finds where the detailed semantics disagree with the summaries or violate its rules; a specification that is internally self-consistent but wrong in a way that both the detail and the summaries share would not be flagged, so consistency is necessary but not sufficient for correctness.
Coverage and precision are strong but not complete. Scope reaches a majority of the interface commands and far higher precision than large language models (about 62 percent versus at best 8 percent for the LLMs), but that precision means reported inconsistencies still need human confirmation, and some subtle issues (like the ordering of failure conditions, or checking all page-table entries rather than one) are outside its current reach.
Uninterpreted functions can cause false positives. Because Scope models helper predicates as uninterpreted functions, it can occasionally report a false inconsistency when one function’s meaning is actually subsumed by another’s, which the abstraction does not capture.
It is tailored to the RMM specification’s structure. The method relies on the specification using ASL and on the presence of summarized tables and figures as an oracle; applying Scope to other specifications would require adapting the parser and the rules, even though the underlying idea is general.

The evaluation

Validating the Arm CCA RMM specification

Property	Prove properties / test vs implementation	LLM-based tools	Scope
Needs an implementation
Keeps up with frequent updates
Detection precision
ABI coverage
Bugs found in the RMM spec

A comparison of ways to validate the Arm CCA RMM specification. By treating the specification as the sole ground truth, translating it into a Verus model, and using an SMT solver to check the detailed ABI semantics against the summarized tables (plus rule-based checks), Scope needs no implementation, keeps pace with frequent updates, and reaches far higher precision than large language models — uncovering 35 previously unknown inconsistencies, all confirmed by Arm.Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

This explainer is based on the paper’s full text (the authors’ copy hosted at Georgia Tech, of the ASPLOS 2026 paper). The system described is the paper’s: Scope is an automated tool that detects specification inconsistencies by combining formal modeling with rule-based consistency checking, treating the specification as the sole ground truth rather than relying on an implementation. It parses the RMM specification (written in Arm’s Architecture Specification Language) from PDF, translates it into a machine-verifiable model in Verus using uninterpreted functions, and uses SMT solvers to detect inconsistencies between the detailed ABI semantics and the specification’s summarized tables and figures, across success and failure conditions, dependency rules, and state transitions; it also applies heuristic rules (such as footprint-versus-success-condition checks). Applied to the Realm Management Monitor specification for Arm’s Confidential Compute Architecture, the paper reports uncovering 35 previously unknown inconsistencies — some persisting up to 33 months, including security-critical flaws in ABI semantics and missing state transitions — all confirmed by Arm, and reports improving inconsistency-detection precision from about 8 percent (best evaluated LLM) to about 62 percent (a 7 to 40 times improvement over evaluated LLMs including GPT-o1, LLaMA 3.1, GPT-4o, and Claude 3.7) with coverage of about 72.8 percent of ABIs. The reported comparisons are the paper’s own measurements under its evaluation setup. Exact translation rules, the model, the consistency rules, benchmark details, and full results should be read from the paper.

Background

Why trusting a proof means trusting everything it stands on

It helps to see Scope within a recurring humility in formal methods: a proof is only ever as strong as its assumptions, and the assumptions live in the specification, the model, and the tools — which are themselves written by people and can be wrong. History is full of verified systems whose bugs hid not in the proved code but in the unproved edges: an incorrect specification, an over-strong axiom, a vacuous invariant that made a theorem true by making it say nothing. As verification reaches larger and more security-critical systems, the specification becomes both more valuable and more likely to harbor such flaws, because it grows to hundreds of pages maintained by many hands. Confidential computing sharpens the stakes, because its whole promise is that a small, trusted core can protect sensitive data even from a compromised operating system or hypervisor, so a defect in the core’s definition is a defect in the protection itself. Much of the field’s progress therefore comes from turning attention back onto the foundations — validating the specifications, models, and mechanisms that proofs and protections rest on, rather than only the code above them. The wider push to automatically validate security-critical designs before they ship, rather than trusting them by assumption, is the same terrain the work on automated design-time testing of secure speculation countermeasures (Amulet) covered elsewhere on this site occupies, catching flaws in a defense while it is still on the drawing board. Scope’s contribution is to show that a specification can be made to check itself, catching the foundational bugs that would otherwise pass silently through every proof built on top.

If you remember only three things

1. Formal verification proves a system correct only relative to its specification, so a contradiction or omission in the specification invalidates the proof and can leave a "verified" system insecure while looking safe — a real risk, as when a verified smart contract lost a one-million-dollar bounty to a specification-rooted flaw. Validating a specification like Arm CCA's RMM (the trusted computing base of confidential computing on Arm) is hard because it is written before any implementation exists, changes frequently, and has no predefined rules for what counts as a bug across hundreds of pages.
2. Scope treats the specification as the sole ground truth and exploits its redundancy: the detailed per-command semantics and the summarized tables both describe the same behavior, so they must agree. It parses the RMM specification's ASL content from PDF, translates it into a machine-checkable Verus model (with uninterpreted functions), and uses SMT solvers to check whether the ABI semantics for success and failure conditions, dependencies, and state transitions match the summarized tables — reporting any contradiction. It adds heuristic rules (like requiring a command's footprint to list everything its success conditions modify) to catch structural bugs.
3. Applied to the RMM specification, Scope uncovered 35 previously unknown inconsistencies — some persisting up to 33 months, including security-critical ABI-semantics flaws and missing state transitions — all confirmed by Arm, and improved detection precision by 7 to 40 times over leading large language models (about 62 percent versus at best 8 percent) with about 72.8 percent ABI coverage. The trade-offs: part of the specification (diagrams, descriptive text) still needs manual translation, it finds contradictions rather than all bugs, reported inconsistencies need human confirmation, uninterpreted functions can cause occasional false positives, and it is tailored to the RMM specification's ASL-and-tables structure.

Check yourself

Check your understanding

1. Why can a system be formally verified and yet still be insecure?
2. What is the key insight Scope exploits to find bugs using only the specification?
3. How does Scope turn this consistency check into something automatic?
4. Predict: Arm releases a new revision of the RMM specification adding several new interface commands, before any implementation of them exists. How does Scope handle this, compared to prior approaches?

Sources

The paper is “Detecting Inconsistencies in Arm CCA’s Formally Verified Specification” by Changho Choi, Xiang Cheng, Bokdeuk Jeong, and Taesoo Kim (Samsung Research and the Georgia Institute of Technology), published at ASPLOS 2026, DOI 10.1145/3779212.3790152 (pages 583 to 601). It is licensed CC BY-NC-ND, with an author copy hosted at Georgia Tech and the source code open at github.com/islet-project/scope.

This explainer is written from the paper’s full text (the authors’ hosted copy). Scope is an automated system that identifies specification inconsistencies by combining formal modeling with rule-based consistency checking, treating the specification as the sole ground truth rather than relying on an implementation. It translates the specification (written in Arm’s Architecture Specification Language, parsed from PDF) into a machine-verifiable model using Verus and SMT solvers, then detects inconsistencies in success and failure conditions, dependency rules, and state transitions between the detailed ABI semantics and the specification’s summarized tables and figures, and applies heuristic rules tailored to the specification. Applied to the Realm Management Monitor specification for Arm’s Confidential Compute Architecture, Scope uncovered 35 previously unknown inconsistencies — including security-critical flaws in ABI semantics and missing state transitions, some persisting up to 33 months — all confirmed by Arm. The paper reports that Scope improves inconsistency-detection precision by 7 times over GPT-o1 and up to 40 times over leading chat models (LLaMA 3.1, GPT-4o, Claude 3.7), from about 8 percent to about 62 percent, with about 72.8 percent ABI coverage. Numbers and comparisons are the paper’s own; exact rules, the model, and full results should be confirmed in the paper.