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

Date: August 29, 2026 · Author: Dmitrii Zatona 

In March 2024, DARPA’s Microsystems Technology Office published a broad agency announcement built around a sentence of unusual logical form. The Continuous-correctness On Opaque Processors program, BAA HR001124S0016, seeks tools and techniques “to continuously guarantee that software is running correctly if and only if the device physics is correct.” A biconditional is a strong thing to promise: it 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 — and seeks to demonstrate “a formal link between MCS and physics without having to compose proofs or assume correctness across all layers,” MCS being the BAA’s abbreviation for mission critical software. The right side is different. Across the three DARPA-authored texts reviewed here — the BAA, a fifty-one-question FAQ, and the Proposers Day slide deck — the phrase “device physics is correct” is never defined; the slides’ own premise predicates on physics being stable, not correct; and when a proposer asked whether the headline accuracy metric covers the gap between the physical world and its formal model, the FAQ’s answer — explanatory, not binding — was that the metric “is based on the threat models and assumptions in each proposer’s technical proposal,” an answer that names where the assumptions live without resolving whether the gap is included. This article reads the three texts closely, lays out the chain a guarantee of this shape would have to be anchored to, and identifies what the texts define, what they delegate, and what a reader who wanted to rely on the guarantee outside the program’s own evaluation loop would have to decide.

One caveat governs everything below. A BAA is a solicitation, not a specification: its definitions section marks its central terms as informal and expressly delegates their formalization to proposers, which is a legitimate design for a research solicitation. And the program’s record now has an end as well as a beginning: three awards were made in fall 2024; current periods of performance ended after roughly 18–20 months (March–June 2026; Vanderbilt’s record separately lists a potential end date of 2027-09-30), and darpa.mil states the program is complete as of 2026-08-29; no reviewed document states whether any options were exercised. Nothing here evaluates the program, its performers, or its outcome. The subject is the published text of a guarantee — what it anchors, and what it leaves to whoever gives it.

1. What was published

The primary text is BAA HR001124S0016 , “Continuous-correctness On Opaque Processors (COOP) Program,” a 17-page initial 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; the notice’s contact is a BAA coordinator mailbox. The program it describes is a 36-month, two-phase effort — an 18-month Phase I base and an 18-month Phase II option — plus two priced fabrication options: a 6-month detailed-design option to tapeout, and a 7-month fabrication and packaging option available only after the first. Award instruments: procurement contracts or Other Transactions, multiple awards anticipated.

The schedule ran quickly. A Proposers Day was held March 18, 2024 in Arlington, Virginia (announced separately as DARPA-SN-24-41 ); abstracts were due March 28; question submittal closed May 3; proposals were due May 13, 2024 at 4:00 PM ET. The SAM.gov notice was last updated May 7, 2024 and has been inactive since June 12, 2024.

Three DARPA-authored documents carry the program’s public technical content, and they are not equal in standing. The binding text is the BAA alone — the Proposers Day deck says so itself: “Only the information/instructions in the BAA counts,” with any diverging FAQ answer to be “made formal by an amendment to the BAA.” The SAM.gov notice description is the primary notice record, and it reproduces the central sentence (“if-and-only-if,” hyphenated there). The FAQ — 51 question-and-answer pairs in the final May 7, 2024 file, read here as cumulative across its three releases on internal evidence (continuous numbering under a single header, Proposers-Day-era questions at the low end; the exact batch boundaries are an inference, not an observation) — and the 58-slide Proposers Day deck are primary records of DARPA’s stated positions, but explanatory. Statements below of the form “the requirement says” rest on the BAA; the FAQ and slides appear with their own modality, and no load-bearing claim in this article rests on them alone.

As of August 29, 2026, the darpa.mil program page  states, verbatim: “This program is now complete.” The current page attributes the program to the post-reorganization “Multi X Office” and names no program manager; the page’s pre-reorganization wording was not retrievable for comparison. The award record behind that status is in Section 6, stated as documents only.

Method note: this is the sixth teardown in a series — the first  asked whether a named primitive exists on the shelf, the second  which assurance tier a notice’s words select, the third  where a platform boundary sits, the fourth  which operational choices a traceability sentence leaves open, the fifth  who chooses the signed cross-stage policy under which evidence composes. This one asks what anchors the guarantee itself — physical reality, formal model, correctness oracle — because here the right side of the biconditional has no program-level definition, and the one direct question about the model-versus-world gap was answered by pointing to each proposer’s threat model; the who-verifies and who-receives questions that also arise belong to the same class the fifth article examined, and are treated as secondary here.

2. What the requirement says

The central sentence appears in the BAA’s background section (p. 3), and the SAM.gov description reproduces 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 underdetermination this article is about is visible in the sentence’s own asymmetry, before any companion document is opened. The left side — software running correctly — is operationally defined two pages later. The right side — the device physics being correct — is defined nowhere in the BAA, and, on full-text reading, nowhere in the FAQ or the slides; 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 (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 oracle itself is defined as “an abstract entity used in formal methods to represent the axiomatic source of correct answers,” with proposals required to describe “why the oracle is realistic, and mitigations for if and when the oracle is proven wrong in the future” (p. 4). The word-level definition of “correct” is explicitly informal — “a computation is correct if the output is as expected (both in time and value). Strong proposals will formalize this definition” (p. 3) — as is the title concept: “Continuous-correctness: Informally, errors are identified and corrected within program metrics. Correctness is guaranteed over time” (p. 3).

The technical objective connects the two sides by removing the usual ladder. The BAA describes the layered-assumption problem — “Formal proofs for MCS might assume that the operating system is correct, proofs for operating systems might assume that the processor instruction set architecture is correct… and so on until the proof chain reaches the physical realities of device physics” — and 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” — “a trusted entity that enforces control boundaries by completely mediating accesses” (p. 4). The trust structure is given as an example partition, expressly refinable: for an interposer-style embodiment, the opaque processor and non-mission-critical software are untrusted, while the mission critical software, the COOP solution, and other system components and peripherals “are considered trusted. However, it is important to highlight that trusted does not mean error free” (p. 6). Proposals “should refine the threat model to include enhancing or relaxing the requirements to meet the needs of the proposed approach” (p. 6) — the partition is a worked example, not a fixed program model.

The quantitative targets (Table 1, p. 5), stated here as the BAA states them — program goals, not results:

The accuracy figure carries the BAA’s one mandate of formal verification: “Equivalent to at least 30-bits guarantee that computation is correct; the probability of not identifying an error is 1/2^30. 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, verified by full-text reading and load-bearing for everything that follows: the words “attestation” and “evidence” do not occur anywhere in the BAA; neither do “certificate,” “remote,” or “root of trust.” The BAA does name its solution class — “a reference monitor” — but that definition describes what the solution does (mediates accesses), not what the guarantee’s output artifact is or who checks it. The BAA’s only statement about the form of that artifact is a definition one line long (p. 4): “Proof: An independently verifiable argument using mathematics.”

3. What anchors a guarantee: three questions

The object model in this section is this article’s organizing abstraction — an incomplete one, marked (I) here and on both diagrams. No reviewed document draws it, and it is not a description of a required COOP architecture. It exists to make the texts’ choices legible: a continuous correctness guarantee of the published shape has to answer three questions, and the three texts answer them to different depths.

(a) The semantic anchor. For the biconditional to be a checkable object, a chain has to hold end to end: the deployed physical execution, observed through physical measurement channels, related to a formal model of the device’s physics, related 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), and the FAQ’s direct prohibition of a technical approach (Q35) states that digital channels alone are disallowed because they do “not link software with physics”: the solution must include sensing through at least one genuinely physical channel. FAQ Q38 and Q40 exclude a “golden processor” that executes the mission software in place of the opaque processor — “real-world oracles do not exist,” the FAQ states — while permitting a portion of the mission software to run on a trusted processor in a formal-verification setup, and an abstract-machine golden processor for reasoning; so — an inference (I) from those answers — the subject the guarantee monitors is the deployed execution on the opaque processor, which no reference re-execution may replace. FAQ Q44 supplies a load-bearing background assumption: opaque components — whose erroneous behavior, per the FAQ, may result from a bug or an adversary — are deterministic — “Deterministic does not mean correct and on time.” And the slides state the premise in their own words: “Device physics is stable. If software can be guaranteed continuously-correct using device physics, then software’s continuous-correctness guarantees are stable.” What no text supplies is the anchor’s semantics: the phrase “device physics is correct” appears in the BAA’s central sentence and the notice description, and in no reviewed text is it defined — the slides predicate on stable, the FAQ, asked directly (Q16, quoted in Section 4), refers the question to each proposer’s threat model.

(b) The artifact. A guarantee has to live in some artifact, and the candidate forms differ in kind: a static proof about the design, verified once; a per-execution certificate, generated as the software runs; a runtime monitor’s verdict, consumed as a signal. The BAA’s texts give the one-line “Proof” definition, schedule “formal models and specifications” for error isolation and correction as the early milestones, and mandate that the 30-bit detection figure “will be formally verified” — without stating in which of these forms the guarantee exists, in what proof system the verification happens, or what a consumer of the artifact would hold in hand. (I) The probabilistic detection metric together with the reference-monitor framing reads most naturally as a runtime verdict backed by a design-time formal argument — an inference from Table 1’s note and the reference-monitor definition, not a statement any text makes.

(c) The verifier, and the transfer. External checking is present in the BAA, and it is worth stating precisely because the presence is real: an independent verification and validation team evaluates solutions against the metrics and designs the false-positive/false-negative test cases; Phase II hardware is “delivered to IV&V to verify the results”; and proposers “should anticipate having to develop formal models of the problem sets and solutions for external (e.g., IV&V and research community) scrutiny and verification” (p. 10). What the texts do not name is a concrete proof-checker — which machine or party checks the “independently verifiable argument,” under what trust and identity model. The slides pose exactly this to proposers, in a backup-slide checklist on the formally verified metric: “Consider how the problem is formalized… Consider what assumptions are needed… Consider how the guarantees can be proven… Consider who can verify proofs.” And beyond the program’s own loop, there is a further step the BAA never set as a task and this article does not read into it: an operational transfer of the guarantee to a downstream relying party — a developer handing it to an operator, an operator to an auditor. That is not an underdetermination of the requirement; it is a design choice left open for any reader who would want to use a COOP-style guarantee outside the program and IV&V context, and Section 8 surveys what the shelf offers such a reader.

4. Four gaps

The gaps below are stated against the documents, with each document’s 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 the rigorous, stable, and tautological basis for formal analysis” (p. 4) — but that sentence describes physics as a basis for analysis, not what it means for a particular deployed device’s physics to be correct or incorrect. The slides never use the phrase; their premise, quoted above, predicates on stability. Neither the FAQ nor the slides restates the biconditional at all. The condition that gives the guarantee its shape is, in the reviewed texts, a name without a definition.

4.2 The one direct question about the model-versus-world gap was answered by pointing to the proposer’s threat model. A proposer asked it exactly (FAQ Q16 — explanatory record, not 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%?

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.”

The FAQ states elsewhere (Q42) what a threat model must contain — the assumptions, the oracle, and the trusted/untrusted component list 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. Reading these two answers together, an interpretation this article marks (I): 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, the boundaries a threat model must state) — because 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. For a research solicitation, delegating this is a coherent choice; 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(b) laid out the candidate forms; the texts choose none. The one-line “Proof” definition is compatible with 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 — a contractual flow to the Government and IV&V — and the vocabulary that would pin an artifact form (“attestation,” “evidence,” “certificate”) is absent from the BAA entirely, while the one named solution class — the reference monitor — is defined by what it mediates, not by what it emits. The FAQ and slides do not add a form; the slides add the open question of who verifies.

4.4 The metrics are three different quantities, and the texts leave them separate. The 99.9999999% figure is an error-detection accuracy — “the probability of not identifying an error is 1/2^30” — and, per Q16, it is relative to each proposer’s threat model 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 unresolved. The false-positive and false-negative targets are distinct quantities — the FAQ says so flatly (Q32: “The accuracy and FP/FN metrics are different”) — and their denominators are unspecified: asked what the countable entity behind the percentages is (Q31) and what base error rate they assume (Q30), the FAQ refers both questions to Q13, which states only that the rates are “assessed using IV&V designed test cases.” The overhead target’s dimension — time, power, area — was asked (Q7) and returned unanswered; the slides bound it only as “compared to processor’s native performance.” A reader should therefore hold the three apart: a detection bound the BAA states will be formally verified, based — per Q16 — on each proposer’s threat models and assumptions; two operational rates measured by IV&V tests whose denominators the public texts do not fix; and an overhead multiple whose unit is not stated.

5. Scale

Money first, one figure per award, labeled: the obligated amounts recorded on USAspending as of August 29, 2026 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 appear in Section 6 with their own labels. No arithmetic is performed on any of these numbers. The program’s quantitative targets are in Section 2, as stated goals.

The peer-reviewed context for the prior class of work — physical-channel integrity monitoring built on machine learning — is systematized in a 2024 SoK at HASP  (Cathis et al., “Power Side-Channel Malware Detection”). Its findings about that corpus: prior works target single-core platforms executing one task at a time and “can be easily evaded in a multi-core setup”; the field tends to reframe security problems as classic machine-learning problems at a cost the paper describes in terms of information loss and stronger assumptions; rigorous public datasets are lacking; and instruction-level detection is reported only for constrained MCU-class devices. The systems in that literature report their own figures — a power-channel malware detector at 94% or better on known and 85% or better on unknown malware for embedded medical devices, an electromagnetic control-flow monitor for PLCs at a reported 98.9% — with training tied to the monitored target in each case — per-device for the medical-device detector, per-controller-and-program for the PLC monitor. Two caveats bound the relevance of all of this. First, it is not a measurement of COOP and carries no implication about the achievability of COOP’s formal, non-ML approaches — the figures describe a different class of techniques. Second, the BAA itself draws the distinction: “Traditional approaches that use single side-channel probes and machine learning to characterize high-level MCS functions in real-time are unable to provably isolate the errors at the fine granularities needed to achieve COOP goals” (p. 9). The BAA distinguishes its sought approaches from the single-probe, machine-learning approaches it describes.

On the formal-methods side, one primary document sizes the layer COOP addresses. The BAA’s own 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.” seL4’s published proof and assumptions pages state, in the project’s own words, the assumption at the boundary between model and device — the boundary the COOP sentence names.

6. The record

The procurement chain, documents only, with only the connections the documents draw. The BAA posted March 13, 2024; the notice was updated March 26 and April 9 (Q&A releases and slides), and May 7, 2024 (final FAQ); responses closed May 13; the notice has been inactive since June 12, 2024. In the SAM.gov search run on August 29, 2026, HR001124S0016 returns exactly five notices — the Proposers Day special notice, the BAA, and three award notices; no other award notices exist under this BAA.

The three awards, 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. Period of performance September 30, 2024 to a current end date of March 30, 2026, with a potential end date of September 30, 2027 on the USAspending record.
• Galois, Inc., HR001125C0300 , awarded October 16, 2024; announced value $26,407,821; base-and-all-options value $52,815,642. Period of performance 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. Period of performance November 5, 2024 to June 30, 2026.

All three USAspending contract records carry HR001124S0016 as the solicitation identifier. The darpa.mil program page  states, as of August 29, 2026: “This program is now complete.” Restating the bounded formulation from Section 1: the current periods of performance ended after roughly 18–20 months (March–June 2026; Vanderbilt’s record separately lists a potential end date of 2027-09-30), and darpa.mil states the program is complete as of 2026-08-29; no reviewed document states whether any options were exercised. No causal statement connects any link of this chain to any other beyond what the documents themselves say.

7. Who would build it

What was requested: the BAA anticipated multiple awards and made Associate Contractor Agreements mandatory across all of them — “The success of COOP hinges upon continuous collaboration across COOP performers” (p. 16). It also stated an expectation of publication restrictions: program goals were anticipated not to be achievable as fundamental research, with awardees expected to seek DARPA permission before publishing program results — alongside, in the same document, a strongly stated desire for Unlimited Rights or Government Purpose Rights and encouragement of open-source licensing.

What is documented: three performers, named above. 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)” and 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 — names three team members, David Archer, Johanna Zimmerman, and Ben Hamlin, in the roles the page itself lists, and describes a trusted-hardware component the page calls the “HEIMDALLR InterProcessor (HIP).” A news page on peraton.com carries republished 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 reviewed record.

What is not in the public record: as of August 29, 2026, in the corpus searched — the GaloisInc GitHub organization, arXiv, and web search by program name and award numbers (HR001124S0016, HR001125C0300 and variants) — no public code repositories, peer-reviewed papers, preprints, or recorded talks documentably linked to COOP or HEIMDALLR were found beyond the two Galois pages above. That is a statement about those searches on that date, not a claim that no such artifacts exist; the BAA’s own publication-restriction expectation is a documented feature of the program’s design. The public record does not distribute roles within any performer’s solution, and this article does not either.

8. What does not exist as a standard

If a reader wanted to take a COOP-style guarantee — continuous, physically grounded, formally argued — and hand it to an external verifying party, what does the shelf offer? The survey below names the versions the reviewed sources stated when accessed on August 29, 2026; where a link cannot be pinned to an immutable edition, the bounded claims hold for the linked page as read on that date:

Two positive findings keep the table honest. First, runtime-extendable measurement registers — TDX RTMRs, CCA REMs — are the closest released mechanism: they let evidence be appended during execution, though each entry’s semantics remain “this object was measured,” not “execution was correct.” Second, carriers for application-defined data already exist — an SGX or TDX quote binds 64 bytes of application- or 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 also exist — EAT’s open claim registry, CoRIM’s profiles (CoRIM itself still a draft) — what does not exist is standardized semantics for the claim such an artifact would carry. And on the monitor side, runtime verification with formally verified monitors exists as peer-reviewed research, not as an ISO/IEC or IEEE standard: as of August 29, 2026, in the corpus searched (ISO catalog, IEEE standards listings, RV literature venues), no standard was found that defines runtime monitors with formal guarantees; IEEE 1012 and ASTM F3269-21 are the nearest published documents, and neither does.

The bounded negation, then, with its corpus stated: among the released specifications reviewed here — RATS RFC 9334, EAT RFC 9711, TPM 2.0 v184, TCG D-RTM 1.0, Linux IMA, Intel SGX/TDX DCAP, Arm CCA RMM v1.0-rel0, seL4’s published proofs and assumptions, CompCert 3.17, the RISC-V Sail model, ISO/IEC 17825:2024, FIPS 140-3, IEEE 1012, ASTM F3269-21 — none defines the standardized claim that would make such an artifact meaningful to an external verifying party: a claim whose semantics bind physical measurement to execution correctness, with continuity semantics and an appraisal policy. A carrier for application-defined data exists on this shelf; the standardized claim to put in it does not. The listed attestation formats convey measurements and identity at or up to a point in time, and several can also carry application-supplied data whose meaning the specifications leave to the application; the formal-verification entries listed condition on the hardware matching their models; the physical-testing standards listed assess modules and designs at validation or evaluation time. For the chain the COOP sentence names — physical reality to formal model to correctness oracle, held continuously — no standardized claim with those semantics is defined among this reviewed set. I work on verifiable data structures for evidence chains in an adjacent area, and that work is separate from this analysis.

The sentence has been on the record since March 2024: correctly, if and only if the device physics is correct. The texts around it define the left side through an oracle, decline to define the right side, answer the one direct question about the model-versus-world gap by pointing to each proposer’s threat model, and describe the guarantee’s artifact in a six-word definition after its label. On the (I) reading this article has marked throughout, what the guarantee is anchored to — and in what form it could ever leave the building — is, in the documents reviewed here, left to whoever gives it.

If you are building a response to this document and the provenance or attestation piece has to be designed and built, that is contract work I take on.