DARPA COOP BAA: What Anchors “If and Only If the Device Physics Is Correct”

Date: August 29, 2026 · Author: Dmitrii Zatona  · Updated: September 29, 2026

TL;DR

• DARPA’s 2024 COOP broad agency announcement sought tools to guarantee that software runs correctly if and only if the device physics is correct, combining formal methods with physical side-channels (Sections 1 and 2).
• The announcement defines correct software through an oracle; neither it, nor the 51-question FAQ, nor the Proposers Day slides defines when device physics is correct (Sections 2 and 4).
• Asked whether the accuracy target covers the gap between the physical world and its formal model, the FAQ referred the question to each proposer’s threat models and assumptions (Section 4).
• The texts define a proof as an independently verifiable argument and require formal verification of the detection target, without selecting the artifact that carries the guarantee or naming its checker (Sections 3 and 4).
• Three awards followed in 2024, their current performance periods ended between March and June 2026, and as of September 29, 2026 DARPA’s program page lists the program as complete (Sections 5 and 6).
• The article evaluates neither the program nor its performers; it claims only that the reviewed texts and standards leave the guarantee’s anchor, artifact, and transfer unchosen (Section 8).

DARPA’s Continuous-correctness On Opaque Processors program, COOP, was built around a sentence of unusual logical form. Its broad agency announcement (BAA), HR001124S0016, published in March 2024, seeks tools to guarantee “that software is running correctly if and only if the device physics is correct.” A biconditional binds a statement about software to a statement about physics in both directions. The BAA gives the left side an operational definition: a computation is correct if its output equals that of an oracle. The right side has none in any of the three DARPA texts reviewed here, which are the BAA, a 51-question FAQ, and the Proposers Day slides.

The slides’ own premise speaks of physics being stable, not correct. When a proposer asked whether the headline accuracy metric covers the gap between the physical world and its formal model, the FAQ answered that the metric “is based on the threat models and assumptions in each proposer’s technical proposal.” This article takes the guarantee apart into three questions: what anchors it, which artifact carries it, and who checks it. A BAA may delegate all three to proposers, and nothing below evaluates the program, its performers, or its outcome.

1. What was published

The primary text is BAA HR001124S0016 , “Continuous-correctness On Opaque Processors (COOP) Program.” It is a 17-page announcement from DARPA’s Microsystems Technology Office, posted to SAM.gov on March 13, 2024. The technical point of contact is Dr. Lok Yan, Program Manager, and the notice’s contact is a BAA coordinator mailbox.

The program it describes is a 36-month, two-phase effort: an 18-month base phase and an 18-month option phase. Two more priced options cover fabrication. One is a 6-month detailed-design option to tapeout; the other is a 7-month fabrication and packaging option, exercised only after the first. Multiple awards were anticipated, as procurement contracts or Other Transactions.

The schedule ran quickly. A Proposers Day was held on March 18, 2024 in Arlington, Virginia, announced separately as DARPA-SN-24-41 . Abstracts were due March 28, question submittal closed May 3, and proposals were due at 4:00 PM ET on May 13, 2024. The notice was last updated on May 7, 2024 and archived on June 12, 2024.

Three DARPA-authored documents carry the program’s public technical content, and they differ in standing. The binding text is the BAA alone. The Proposers Day deck says so itself: “Only the information/instructions in the BAA counts,” and any FAQ answer that differs from the BAA is to be “made formal by an amendment to the BAA.” The SAM.gov notice description restates the central sentence, hyphenated there as “if-and-only-if.”

The FAQ and the 58-slide Proposers Day deck record DARPA’s stated positions, but they explain rather than bind. The FAQ grew across three releases, of March 26, April 9, and May 7, 2024, which carry questions 1 to 35, 1 to 45, and 1 to 51. Statements below of the form “the requirement says” rest on the BAA. The FAQ and slides appear with their own modality, and no claim below rests on them alone.

This is the sixth teardown in a series; the previous one, NIST NCCoE DevSecOps Live Document: What Does the Attestation Attest?, asked who selects the signed policy under which per-stage supply-chain evidence composes.

2. What the requirement says

The central sentence appears in the BAA’s background section (p. 3), and the SAM.gov description restates it:

“The COOP program seeks to develop tools and techniques to continuously guarantee that software is running correctly if and only if the device physics is correct. COOP combines formal methods and side-channels to unify computer science and physics.”

The sentence is asymmetric before any companion document is opened. The left side, software running correctly, is defined operationally two pages later. The right side, the device physics being correct, is defined nowhere in the BAA, and a full-text reading of the FAQ and the slides finds no definition there either. The three texts never state what would make device physics incorrect, or who would determine that it was. A biconditional guarantee has two sides, and the published texts build a floor under one of them.

The left side’s definition sits in BAA §1.3.1 (p. 5):

“In COOP, a computation has integrity (i.e., it is correct) if, given an input, the output is equal to that of an oracle. The oracle can be the same computation executed in a golden processor, a formal specification, or others if defended in the proposal. Proposals must clearly and succinctly describe the chosen oracle.”

The BAA defines the oracle itself as “an abstract entity used in formal methods to represent the axiomatic source of correct answers” (p. 4). Proposals must describe “why the oracle is realistic,” along with mitigations for when it is proven wrong. The word-level definition of “correct” is marked informal: a computation is correct “if the output is as expected (both in time and value),” and “Strong proposals will formalize this definition” (p. 3). The title concept is informal too, with errors identified and corrected “within program metrics” (p. 3).

The technical objective connects the two sides by removing the usual ladder of assumptions. The BAA describes proofs for mission critical software (MCS) that assume a correct operating system, which assumes a correct instruction set, and so on down to device physics. It then states the objective (p. 5):

“The COOP program seeks to demonstrate a formal link between MCS and physics without having to compose proofs or assume correctness across all layers.”

The architecture is named in one sentence: “The COOP solution is a reference monitor,” defined as “a trusted entity that enforces control boundaries by completely mediating accesses” (p. 4). The trust structure is given as an example partition that proposals may refine. For an interposer-style embodiment, the opaque processor and non-mission-critical software are untrusted. The mission critical software, the COOP solution, and other components are trusted, but “trusted does not mean error free” (p. 6). Proposals “should refine the threat model,” so the partition is a worked example rather than a fixed program model.

The quantitative targets in Table 1 (p. 5) are program goals, not results:

The accuracy figure carries the BAA’s one mandate of formal verification. Its note equates the target to a 30-bit guarantee, “the probability of not identifying an error is 1/2^30,” and states: “This will be formally verified.” The false-positive and false-negative rows carry a different note: “Assessed using IV&V designed test cases.”

One vocabulary fact frames what follows. A full-text reading of the BAA finds no occurrence of “attestation,” “evidence,” “certificate,” “remote,” or “root of trust.” The BAA names its solution class, a reference monitor, but that definition describes what the solution does, not what its output artifact is or who checks it. The BAA’s only statement about the form of that artifact is a one-line definition (p. 4): “Proof: An independently verifiable argument using mathematics.”

3. What anchors a guarantee: three questions

A continuous correctness guarantee of the published shape has to answer three questions: what it is anchored to, in which artifact it exists, and who checks that artifact. The three texts answer them to different depths. The object model in this section is an organizing abstraction assembled from the texts; no reviewed document draws it, and it does not describe a required COOP architecture.

The diagram’s chain is an inference from the BAA’s definitions (pp. 3 to 5) and FAQ answers 16, 35, 38, 40, and 44, not something the BAA defines.

3.1 The semantic anchor

For the biconditional to be a checkable object, a chain has to hold end to end. The deployed physical execution is observed through physical measurement channels. Those observations relate to a formal model of the device’s physics, which relates in turn to an oracle that defines correct output. The texts fix real points on this chain.

Side-channels, the program’s term, are defined as “physical manifestations of software running on hardware” (p. 4). The FAQ rules out a purely digital approach (Q35). Digital channels alone do “not link software with physics,” so a solution must sense through at least one physical channel. Q38 and Q40 exclude a golden processor that executes the mission software in place of the opaque processor, because “real-world oracles do not exist.” Running a portion of the mission software on a trusted processor as part of a formal verification setup is in scope.

The subject the guarantee monitors is therefore the deployed execution on the opaque processor, which no reference re-execution may replace; that is an inference from Q38 and Q40. Q44 adds a background assumption. Opaque components are deterministic even when they err, whether the cause is a bug or an adversary: “Deterministic does not mean correct and on time.” The slides state the premise in their own words: “Device physics is stable.” They add that guarantees built on device physics are stable in turn.

None of the three texts supplies the anchor’s semantics. The phrase “device physics is correct” appears in the BAA’s central sentence and the notice description, and no reviewed text defines it. The slides speak of stability, and the FAQ, asked directly (Q16, quoted in Section 4.2), refers the question to each proposer’s threat model.

3.2 The artifact

A guarantee has to live in some artifact, and the candidate forms differ in kind. A static proof about the design is verified once. A per-execution certificate is generated as the software runs. A runtime monitor’s verdict is consumed as a signal.

The BAA gives the one-line proof definition and schedules formal models and specifications as early milestones. It mandates that the 30-bit detection figure “will be formally verified.” It does not state in which of these forms the guarantee exists, in what proof system the verification happens, or what a consumer of the artifact would hold. The probabilistic detection metric and the reference-monitor framing together suggest a runtime verdict backed by a design-time formal argument. That reading is an inference from Table 1’s note and the reference-monitor definition; no text states it.

3.3 The verifier and the transfer

External checking is present in the BAA. An independent verification and validation (IV&V) team evaluates solutions against the metrics and designs the false-positive and false-negative test cases. Phase II hardware is “delivered to IV&V to verify the results.” Proposers should expect to develop formal models “for external (e.g., IV&V and research community) scrutiny and verification” (pp. 10 to 11).

The texts do not name a concrete proof checker: which machine or party checks the independently verifiable argument, under what trust and identity model. The slides pose that question back to proposers, in a backup-slide checklist on the formally verified metric. It includes “Consider how the guarantees can be proven” and “Consider who can verify proofs.”

Beyond the program’s own loop there is a further step that the BAA never set as a task. That step is an operational transfer of the guarantee to a downstream relying party: a developer handing it to an operator, or an operator to an auditor. This is not an underdetermination of the requirement. It is a design choice left open for any reader who would use a COOP-style guarantee outside the program and IV&V context, and Section 8 surveys what the released standards offer that reader.

4. What the guarantee leaves undefined

The guarantee is undefined at both of its ends. On the anchor side, the texts name the condition without defining it and send the model-versus-world question to each proposal; on the artifact side, they select no form for the guarantee, and metrics stand in for it during the program. Each point below is stated with the documents’ own words as the boundary.

4.1 The right side of the biconditional has no program-level semantics

“Device physics is correct” is the condition on which the entire guarantee is predicated, and none of the three texts defines it. The BAA grounds the program’s plausibility in physics: “Reliability physics is grounded in mathematics” and can serve as a stable basis for formal analysis (p. 4). That sentence describes physics as a basis for analysis. It does not say what it means for a particular deployed device’s physics to be correct or incorrect.

The slides never use the phrase; their premise, quoted in Section 3.1, speaks of stability. Neither the FAQ nor the slides restates the biconditional at all. In the reviewed texts, the condition that gives the guarantee its shape is a name without a definition.

4.2 The model-versus-world question went to the proposer’s threat model

A proposer asked the question directly, in FAQ Q16, which is an explanatory record rather than binding text:

“Question #16: Question about the 99.9999…% accuracy: is it with respect to a physical model that has been fed to a formal method tool, or it is with respect to the physical world? In other words, is the gap between the physical world and its formal model included in the 99.99%?”

The FAQ’s answer reads:

“Answer #16: The metric is based on the threat models and assumptions in each proposer’s technical proposal. Please also see the Phase I (Base) paragraph in the ‘Program Structure’ section of the BAA.”

Elsewhere (Q42) the FAQ states what a threat model must contain: the needed properties, the assumptions including the oracle, and a list of trusted and untrusted components that “helps set the boundaries to which the proposed approach is valid.” The answer names where the assumptions live. It does not state whether the gap is inside or outside the metric.

Read together, the two answers support an inference from Q16 and Q42. The semantics of the anchor come from each proposal’s own models and assumptions, within the constraints the BAA does set: the metrics, the physical-channel requirement, and the boundaries a threat model must state. The BAA directs each proposal to describe its own oracle and threat model, and no program text supplies a common definition for “device physics is correct.” Two conforming proposals could therefore anchor that phrase to different formal models with different validity boundaries.

The BAA delegates this to proposers by design. The narrow, documented point is that Q16 does not determine whether the model-versus-world gap is inside the metric, and no reviewed text determines it elsewhere.

4.3 The artifact of the guarantee is never selected

Section 3.2 laid out the candidate forms, and the texts choose none. The one-line proof definition fits all of them. The sentence “This will be formally verified” attaches to the 30-bit metric without naming the proof system, the checker, or the party performing the verification.

The scheduled deliverables are models, specifications, software, and hardware, flowing under contract to the Government and IV&V. The vocabulary that would pin an artifact form (attestation, evidence, certificate) is absent from the BAA. The one named solution class, the reference monitor, is defined by what it mediates rather than by what it emits. The FAQ and the slides add no form; the slides add the open question of who verifies.

4.4 Three metrics, kept separate

The 99.9999999% figure is an error-detection accuracy, a bound on the probability of not identifying an error. Per Q16, it is relative to each proposer’s threat models and assumptions. It is a stated program target, not a demonstrated property, and it is not an end-to-end statement about the biconditional. Nothing in the texts extends the 30-bit figure across the model-versus-world gap, whose treatment Q16 leaves open.

The false-positive and false-negative targets are distinct quantities, as the FAQ states in Q32: “The accuracy and FP/FN metrics are different.” Their denominators are unspecified. Asked what countable entity the percentages are calculated against (Q31) and what base error rate they assume (Q30), the FAQ refers both questions to Q13. Q13 states only that these metrics are “assessed using IV&V designed test cases.”

The overhead target’s dimension (time, power, or area) was asked in the first FAQ release (Q7), and the answer asked the proposer to clarify and resubmit. The slides bound overhead only as “compared to processor’s native performance.”

The texts therefore keep three kinds of target apart. One is a detection bound that the BAA states will be formally verified, based per Q16 on each proposer’s threat models and assumptions. Two are operational rates measured by IV&V tests whose denominators the public texts do not fix. The last is an overhead multiple whose unit is not stated.

The diagram’s split between the program loop the BAA describes and the three unselected steps is an inference from the BAA’s deliverables and IV&V passages and slide 56, not something the BAA defines.

5. Scale

Money comes first, with one figure per award and a label. As recorded on USAspending on September 29, 2026, the obligated amounts are $12,622,799 to Galois (HR001125C0300 ), $1,211,181 to Peraton Labs (HR001125C0305 ), and $1,042,067 to Vanderbilt University (HR001124C0520 ). Announced values and contract ceilings are different figures with different meanings, and they appear in Section 6 with their own labels. No arithmetic is performed on any of these numbers, and the program’s quantitative targets are in Section 2 as stated goals.

The peer-reviewed context for the prior class of work, physical-channel malware detection built on machine learning, is systematized in a 2024 SoK paper at HASP  by Cathis et al., “Power Side-Channel Malware Detection.” It finds that prior works target single-core platforms executing one task at a time, and that existing methods “can be easily evaded in a multi-core setup.” It also finds that those works often reframe security problems as classic machine-learning problems, at the cost of information loss or stronger assumptions. Few if any prior works release their datasets. Instruction-level detection is reported on microcontroller-grade devices, while detectors on more complex devices characterize higher-level activities.

Two caveats bound the relevance of this literature. It is not a measurement of COOP, and it implies nothing about the achievability of COOP’s formal approaches, which belong to a different class of technique. The BAA itself draws the distinction (p. 9). It states that traditional approaches using single side-channel probes and machine learning are unable to “provably isolate the errors at the fine granularities needed to achieve COOP goals.”

On the formal-methods side, one primary document sizes the layer COOP addresses. The BAA’s footnote on proof tractability cites the seL4 proof FAQ. The seL4 project’s assumptions page  states that its functional-correctness proof assumes the hardware “is assumed not to be tampered with, and working as the formal model predicts.” That assumption sits at the boundary between model and device, the boundary the COOP sentence names.

6. The notice and award record

The procurement chain is given here as documents only, with only the connections the documents draw. The BAA was posted on March 13, 2024. The notice was updated on March 26 and April 9 with FAQ releases and slides, and on May 7, 2024 with the final FAQ. Responses closed on May 13, and the notice was archived on June 12, 2024. A SAM.gov search for HR001124S0016 on September 29, 2026 returns five notices: the Proposers Day special notice, the BAA, and three award notices.

The three awards follow, with announced values from the SAM.gov award notices and ceilings from USAspending, each labeled. Obligated amounts are in Section 5.

• Vanderbilt University, HR001124C0520 , awarded September 30, 2024; announced value $5,380,677; base-and-all-options value $5,380,677. The period of performance ran from September 30, 2024 to a current end date of March 30, 2026, and the USAspending record lists a potential end date of September 30, 2027.
• Galois, Inc., HR001125C0300 , awarded October 16, 2024; announced value $26,407,821; base-and-all-options value $52,815,642. The period of performance ran from October 16, 2024 to June 11, 2026.
• Peraton Labs Inc., HR001125C0305 , awarded November 5, 2024; announced value $2,809,522; base-and-all-options value $1,211,181.03 on the USAspending record. The period of performance ran from November 5, 2024 to June 30, 2026.

All three USAspending contract records carry HR001124S0016 as the solicitation identifier. The current periods of performance ended after roughly 18 to 20 months, between March and June 2026. As of September 29, 2026, no reviewed document states whether any options were exercised, and the records do not label their end dates as option decisions.

The darpa.mil program page  states, as of September 29, 2026: “This program is now complete.” It attributes the program to the Multi X Office, a name from DARPA’s reorganization, and names no program manager; the page’s earlier wording was not retrievable for comparison. No causal statement connects any link of this chain to any other beyond what the documents say.

7. Who would build it

The BAA anticipated multiple awards and made Associate Contractor Agreements mandatory across them: “The success of COOP hinges upon continuous collaboration across COOP performers” (p. 16). It also expected publication restrictions. Program goals were not expected to be achievable as fundamental research, and awardees were expected to seek DARPA permission before publishing program results. The same document states a strong desire for Unlimited Rights or Government Purpose Rights and encourages open-source licensing.

The documented record names three performers, listed in Section 6. Galois’s public record is the most specific. Its January 30, 2025 announcement  names the project “HEIMDALLR (Hybrid Electromagnetic side-channel and Interactive-proof Methods to Detect and Amend LogicaL Rifts).” It lists eight partners: MIT, NYU, Ohio State, Carnegie Mellon, Battelle, Niobium Microsystems, Riscure (a part of Keysight Technologies), and Ansys.

The HEIMDALLR project page , marked approved for public release, lists team members by name and role. It describes a trusted-hardware component the page calls the “HEIMDALLR InterProcessor (HIP).” A news page on peraton.com republishes trade coverage of the awards; it is secondary and is not relied on here. Neither Peraton Labs nor Vanderbilt has a project page in the record reviewed on September 29, 2026.

The public record has limits that can be stated with a date. As of September 29, 2026, searches of the GaloisInc GitHub organization and of arXiv, by program name and by project name, found no code repositories or preprints linked to COOP or HEIMDALLR. That is a statement about those searches on that date, not a claim that no such artifacts exist. The BAA’s own expectation of publication restrictions is a documented feature of the program’s design. The public record does not distribute roles within any performer’s solution.

8. What does not exist as a standard

A reader who wanted to hand a COOP-style guarantee, continuous, physically grounded, and formally argued, to an external verifying party would need a released format for it. The survey below asks what the released specifications offer that reader. Each row is bounded to the version it names.

Two positive findings come first. Runtime-extendable measurement registers, TDX RTMRs and CCA realm extensible measurements, are the closest released mechanism. They let evidence be appended during execution, although each entry still means that an object was measured, not that execution was correct.

Carriers for application-defined data also exist. A TDX quote binds 64 bytes of TD-supplied REPORTDATA, and EAT admits proprietary and future standardized claims, so a COOP-style statement could already ride inside existing envelopes. The extension points through which such a claim could be standardized exist as well, in EAT’s claim registry and CoRIM’s profiles, with CoRIM still a draft. What is missing is standardized semantics for the claim such an artifact would carry.

On the monitor side, formally verified runtime monitors exist in peer-reviewed research. Finkbeiner et al. (RV 2020) , for one, compile stream-based monitor specifications to Rust code whose functional correctness and termination a verification toolkit proves automatically. Among the standards in this table, IEEE 1012-2024 and ASTM F3269-21 come nearest, and neither defines runtime monitors with formal guarantees.

The bounded negation follows, with its corpus stated. The released specifications reviewed here are RATS RFC 9334, EAT RFC 9711, TPM 2.0 Library Version 185, TCG D-RTM 1.0.0, Linux IMA, Intel TDX DCAP, seL4’s published proofs and assumptions, CompCert 3.18, the RISC-V Sail model, ISO/IEC 17825:2024, FIPS 140-3, IEEE 1012-2024, and ASTM F3269-21; the drafts reviewed are CoRIM -11 and the Arm CCA token Internet-Draft -04. As of September 29, 2026, none of them defines the standardized claim that would make such an artifact meaningful to an external verifying party. That claim would bind physical measurement to execution correctness, with continuity semantics and an appraisal policy.

A carrier for application-defined data exists in this set, and the standardized claim to put in it does not. The attestation formats listed convey measurements and identity at or up to a point in time. The formal-verification entries condition on the hardware matching their models. The physical-testing standards assess modules and designs at validation or evaluation time. For the chain the COOP sentence names, from physical reality to formal model to correctness oracle, held continuously, the reviewed set defines no standardized claim with those semantics.

The COOP sentence of March 2024 seeks a guarantee that software runs correctly if and only if the device physics is correct. The texts around it define the left side through an oracle and leave the right side undefined. They answer the one direct question about the model-versus-world gap by pointing to each proposer’s threat model, and they define the guarantee’s artifact in one line. In the documents reviewed here, whoever gives the guarantee decides what it is anchored to and in what form it could reach a party outside the program. This article does not claim that any performer’s solution lacks such an anchor, or that the program fell short of its goals.

I work on verifiable data structures for evidence chains in an adjacent area, and that work is separate from this analysis. More write-ups are on the engineering blog.

If a system must show an outside party that its hardware executed as specified, deciding what that runtime guarantee claims and how it is checked is contract work I take on.