{"id":"d286a890-1895-447e-934f-09c9b95ef968","arxiv_id":"2508.20411","paper_version":1,"verdict":"REJECT","confidence":"HIGH","novelty_score":4.0,"correctness_risk":"high","formal_verification":"none","parameter_count":0,"one_line_summary":"An architecture that places a digitally signed, tamper-proof rule checker between an AI and its actuators is claimed to guarantee safety, but the proof assumes the very rules it must supply.","lead":"The paper proposes an external guard layer, called GAI, that sits between an AI and the machinery it controls and checks every command against pre-signed safety rules. It claims this cryptographic and trusted-computing barrier can make AI behavior provably safe even against a superintelligent, malicious AI.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The formal proof is vacuous: the 'provable safety' conclusion (S9/Eq. 17) is just assumption H3 (Eq. 1) restated, and S9 is self-referential and type-ill-formed; the proof cannot establish safety beyond assuming it.","rationale":"I read the paper in good faith: the GAI architecture is a concrete engineering proposal, and the components—REM, digital signatures, TPM-based boot, OS-level access control—are real and mostly mature. As a defense-in-depth system conditional on a complete and correct rule set, it is plausible and could be useful. The problem is the paper's central claim of provable safety under an extreme threat model. That claim is not supported because the formal proof assumes exactly the property it claims to prove. H3 in Eq. (1) is the assertion that there exists a rule set qr such that rectification always produces an acceptable command. After a chain of cryptographic-integrity steps (which are valid but only establish that the loaded REM is the genuine REM and the loaded rule is the signed rule), S9 concludes that the executed command is acceptable. This is H3 with a different name for the rectification function. The proof adds nothing about whether such a rule set can actually be written; it merely pushes the burden onto an assumption the authors themselves acknowledge is 'not a technical issue' (Sec. V-C, P2). The formal proof is additionally defective: S9 cites itself, and the equality in Eq. (17) is ill-typed (command = set). The reader's weakest_assumption identifies the same core issue—H3 is the load-bearing premise. My stress-test sharpens this: the proof is not merely conditional on an unverified premise; it is logically circular, so the 'provable' adjective is unjustified. The experimental results (Table II, signature tampering, eBPF access control) demonstrate textbook enforcement and integrity mechanisms, not resistance to a maximally adversarial AI trying to bypass them while the rule set is inadequate. They also do not test the rule set's completeness, which would be impossible in general. Given all this, the reader's REJECT verdict stands. I would express no opinion on whether the engineering components are useful; the concern is specifically that the central safety guarantee is assumed, not proven.","tokens_in":19118,"tokens_out":3437,"duration_ms":38961,"concrete_test":"Formalize the derivation S1–S9 in a proof assistant (e.g., Coq) with explicit types: c:Cmd, s:State, qr:Rule, rectify: Cmd→Rule→State→Cmd, AcceptableCommand: State→Set Cmd, mREM: Cmd→Rule→State→Cmd. Attempt to prove ∀s c, mREM(c,r,s) = AcceptableCommand(s). The proof will either require postulating Eq. (1) as an axiom—making the theorem a restatement of H3—or fail at type-checking because the left side is a command and the right side is a set. As a supplementary check, substitute an intentionally unsafe rule set (e.g., a rule that accepts every command) and rerun the proof; if the 'safety' theorem still holds, the formal system cannot certify rule adequacy.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is 'provable safety under extreme threat models,' but the formal proof in Sec. VI-C reduces to assumption H3. H3 is formalized as Eq. (1): ∃qr∈R, ∀c∈C, rectify(c,qr,s)∈AcceptableCommand(s). This is exactly the desired safety guarantee—every command becomes acceptable after rectification. The succeeding steps only show that, under the signature/TPM assumptions, the loaded mREM equals REM and the loaded rule r equals qr (S2, S4), so mREM(c,r,s)=rectify(c,qr,s) (S7, S8). Then S9 concludes mREM(c,r,s)=AcceptableCommand(s), which is precisely H3 with 'rectify(c,qr,s)' replaced by 'mREM(c,r,s)'. No new property is derived; the proof is circular. Moreover, S9 is internally invalid: it cites 'S9 and H3' (itself, likely a typo for S8), and it equates a command—an element of C—with AcceptableCommand(s), which is a set of commands. This is a type error in the formalization, not a cosmetic issue. The extensive cryptographic/TPM analysis only establishes authenticity and integrity of the REM and rules; it cannot distinguish a safe rule set from an unsafe one. Thus, even if every attack path P1–P9 is blocked, the 'safety' property is assumed, not proved. This is the load-bearing gap behind the paper's headline claim.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a Governable AI (GAI) architecture in which a deterministic Rule Enforcement Module (REM) sits between an AI system and its actuators, applies human-authored governance rules to every command, and is protected by a 'Governable Secure Super-Platform' (GSSP) based on TPMs, digital signatures, and OS-level access control. The paper identifies nine attack paths, claims each is blocked, and gives an informal formal proof in Sec. VI purporting to show that every command reaching the actuator is acceptable. It also reports a prototype using GPT-4o-mini on grid path-planning and Linux IMA/eBPF demonstrations. The headline claim is that GAI provides provable, non-bypassable, tamper-resistant safety against an omniscient, maximally adversarial AI.","tokens_in":19475,"tokens_out":6426,"duration_ms":75347,"significance":"The architectural idea of separating a powerful, potentially untrusted AI from a small, deterministic, rule-based enforcement component is a reasonable engineering direction, and the paper usefully enumerates attack surfaces and demonstrates concrete integrity-enforcement mechanisms. If the formal claim were established, the paper would be important. However, the central proof does not establish safety: the desired property is already assumed in H3, and the cryptographic steps only establish authenticity/integrity of the loaded code and rules, not semantic safety. The trusted-computing self-protection premise is asserted rather than proved. The experiments, while relevant as a proof-of-concept, do not exercise the advertised extreme threat model. As submitted, the paper's main contribution—'provable safety'—is not sustained.","major_comments":[{"comment":"The formal proof is circular. Eq. (1) formalizes H3 as ∃qr∈R, ∀c∈C: rectify(c,qr,s)∈AcceptableCommand(s), which is already the target safety property. S9 then concludes ∀s∈S, ∀c∈C: mREM(c,r,s)=AcceptableCommand(s). Since S7 and S8 only use signature verification to establish mREM=REM and r=qr, they substitute the loaded module/rule into Eq. (1); no new property is derived. S9 also cites 'S9 and H3' (self-reference, presumably S8) and equates a command with a set of commands—a type error. Additional cryptography cannot repair this gap, because signatures do not constrain the semantics of the signed rule set. This is the load-bearing issue behind the paper's 'provable safety' claim.","section":"Sec. VI-C, Eq. (1), Eq. (17) (S9)"},{"comment":"The blocking of P6, and transitively P3/P4/P5/P7/P8, rests on the assertion that the trusted computing platform 'is also capable of protecting itself under assumption H2.' No mechanism or proof is supplied for this claim, and H2 explicitly includes software-level attacks targeting hardware. Real-world TPMs, secure boot implementations, and trusted-computing stacks have been compromised through software and firmware vectors; the paper cites no evidence that its platform is immune under its adversarial model. Since P4 and P7 are reduced to P6, the non-bypassability and tamper-resistance guarantees inherit this unproved premise.","section":"Sec. V-C, P6; Sec. III-A, H2"},{"comment":"The paper itself states in the P2 discussion that whether governance rules are comprehensive 'is not a technical issue and is beyond the scope of this paper' and treats it as an assumption. But H3—there exists a rule set such that every rectified command is acceptable in every state—is exactly the safety conclusion. Signature checking can only ensure that the loaded rule is the signed rule, not that the signed rule is safe. Thus the architecture delivers integrity and authenticity hardening, not provable safety. The concluding assertion that every output command 'can be ensured' acceptable is valid only conditional on H3, which is equivalent to the target property.","section":"Sec. III-A, H3; Sec. V-C, P2"},{"comment":"The formalization of hash collision resistance as ∀x,y: hash(x)=hash(y) ↔ x=y is not a true property of cryptographic hash functions; it asserts injectivity, which is impossible for a fixed-length hash on a larger input domain. S1 uses this equivalence to infer x1=x2 from equality of hashes. Even if this were repaired as a probabilistic statement, the resulting step would still establish only that the signed and loaded objects are equal, not that they are safe. As written, the formal derivation contains a further logical error.","section":"Sec. VI-A, Eq. (4); Sec. VI-C, S1"},{"comment":"The experiments do not exercise the extreme threat model advertised in the paper. Table II measures a benign GPT-4o-mini planner on 3×3/5×5/7×7 grids, where REM feedback enables replanning; this demonstrates a guardrail for a helpful planner, not defense against an omniscient, actively evasive attacker. The eBPF demo in Sec. VII-F shows one unauthorized open of /dev/secur_ctrl returning EPERM; it does not demonstrate that all possible bypass paths are closed. These results therefore provide engineering illustration, not evidence for the paper's central security guarantee.","section":"Sec. VII-C, Table II; Sec. VII-F"}],"minor_comments":[{"comment":"The quantifier over s is missing: as written, s is free, so the formula is a predicate over s rather than a closed assumption.","section":"Sec. VI-C, Eq. (1)"},{"comment":"The step says 'Based on S9 and H3'; this should presumably be S8. Also, mREM(c,r,s) is a command, while AcceptableCommand(s) is a set; the conclusion should be ∈, not =.","section":"Sec. VI-C, S9"},{"comment":"S7 and S8 cite 'P6' and 'P7' as if they were formal propositions, but P6/P7 are attack-path labels from Sec. V. The proof does not connect the informal blocking claims to the formal derivation.","section":"Sec. VI-C, S7/S8"},{"comment":"Some citations do not match the text: '[8]' is Fidon et al., not Li et al.; '[22]' is Kieseberg et al., not Amodei et al. The intended Amodei et al. reference appears to be missing.","section":"Sec. II-A, references"},{"comment":"Numerous typos and proofreading errors occur, e.g., 'etsablishes' (Sec. IV-A), 'architectuure' (Sec. V-C), 'comninantion' (Sec. II-B), 'futher' (Sec. IV-E), and 'formal proofed' (Sec. V-C).","section":"Throughout"}],"recommendation":"reject","confidential_remarks":"The reader's report correctly identifies the central circularity: H3 is the entire safety property, and the formal proof does not go beyond it. I agree with the reject recommendation. The paper might be reconsidered if substantially rewritten as an engineering architecture proposal that claims integrity hardening and rule enforcement under explicitly acknowledged rule-completeness assumptions, without the 'provable safety' framing. I would not invite a revision until that reframing is made."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Thanks for sharing the reader report. I read the paper and agree with the REJECT verdict, but there are some things in its favor before I get to the reasons.\n\nWhat's actually new is the packaging. The REM as a deterministic command-validation chokepoint, signed rule files, TPM-secured loading, and the governance-technical decoupling—each component is mature, but the assembly into an external AI safety layer is not something I've seen in exactly this form. The decoupling idea, where governance people write rules without engineers, is worth taking seriously as a design principle. The paper is also honest about its load-bearing assumption: H3 says 'humans can write a complete and correct rule set,' and the authors explicitly call it out and say rule completeness is outside the technical scope. The attack-surface enumeration is systematic, and the experiments, though small, do demonstrate that the standard mechanisms work as advertised: signing, IMA/EVM enforcement, and eBPF/LSM port blocking. No tricks there.\n\nThe soft spot is the formal proof, and it's load-bearing. The stress-test note is right: S9 concludes exactly what H3 postulates. Eq. (1) says there exists qr such that rectify(c,qr,s) is in AcceptableCommand(s). After S2 and S4 establish that the loaded module is REM and the loaded rule is qr, S9 restates that as mREM(c,r,s) = AcceptableCommand(s). That's not a theorem; it's H3 in new notation. On top of that, S9 is formally ill-typed—it says a command equals a set—and its citation 'based on S9 and H3' is self-referential, likely a typo for S8, but the kind of thing that tells you the proof was never checked. The crypto and TPM steps only buy authenticity and integrity of the loaded code and rules; they cannot buy safety of the rules themselves. Secondary issue: the attack-path blocking leans on 'the trusted computing platform can protect itself under H2' (P6). That's asserted, not argued, and TPM/OS self-protection has a contested history.\n\nWhere does that leave it? As an engineering proposal conditional on H3, GAI is a plausible defense-in-depth layer. As a proof of provable safety under an extreme threat model, it fails. The gap between the headline and the result is exactly what the formal proof was supposed to close. This paper is for anyone working on external enforcement, sandboxing, or command filtering for AI. The architecture discussion is useful, and the formal proof is a good teaching example of a circular argument. I'd send it to a serious referee because the topic matters and the flaws are fixable by reframing the work as 'integrity-hardened enforcement of human-provided rules,' which is an honest contribution. As is, reject.","headline":"Useful architectural packaging undone by a circular formal proof: the 'provable safety' conclusion restates assumption H3, so the headline overclaims even though the engineering is a defensible defense-in-depth proposal.","tokens_in":19941,"tokens_out":2574,"would_cite":false,"duration_ms":30455,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper claims that a deterministic rule-checking module between an AI and its actuators, protected by digital signatures and trusted hardware, can guarantee that every executed command is safe even against an omniscient, maliciously moti","keywords":["AI safety","Governable AI","rule enforcement","trusted computing","cryptographic signatures","threat model","superintelligent AI","formal proof"],"falsifier":"Red-team a GAI prototype with full source knowledge and software-only access: any success in placing an unrectified command on an actuator port falsifies the non-bypassability claim (H2/P6). Separately, domain experts can falsify the rule-completeness premise by exhibiting one reachable state where the rule set admits a rectified command that still causes harm.","tokens_in":18987,"feed_emoji":"🔐","tokens_out":10785,"duration_ms":111012,"temperature":0.7,"pith_summary":"This paper argues that safety for advanced AI should be enforced from the outside rather than requested from the inside. It proposes Governable AI (GAI): a deterministic rule-checking module (REM) placed between the AI and the physical systems it controls, which verifies or repairs every command against human-authored governance rules, plus a trusted-computing layer that makes the module non-bypassable, tamper-resistant, and unforgeable. Alignment, model hardening, and human oversight, the authors argue, cannot guarantee safety against an AI that is maximally malicious and far more intelligent than its builders, whereas cryptographic signatures are hard to break regardless of attacker intelligence. If the proof holds, the safety question shifts from the AI's intentions to the quality of the human rule set. A prototype on grid-world path planning raises command compliance from as low as 10 percent to 100 percent when the REM is inserted between the AI and the actuators.","feed_headline":"No AI, however intelligent, can bypass this command gate","feed_subtitle":"Paper proves every AI command can be rectified to obey human rules — if the rules cover every situation.","key_machinery":"The load-bearing mechanism is the signature-verified execution chain: REM logic implemented as side-effect-free pure functions, governance rules as signed data, and a TPM-rooted secure boot that validates OS, REM, and rules before any of them run. The proof turns on two identities — verify(sign(x, prv), pub) = x (CT2) and hash collision-freeness (CT3) — which force the executed module and the loaded rules to equal the originals that humans signed; definition L1 then identifies the REM's behavior with the rectify function; and H3 asserts that rectify's output is always acceptable. Every safety guarantee pivots on the key pair and the boot chain that keep those identities intact.","core_discovery":"The paper claims that no matter how capable or malicious an AI is, the commands it can execute can be made provably safe by interposing a small, deterministic Rule Enforcement Module (REM) between the AI and the actuators. The REM checks each command against signed governance rules and, on failure, transforms it into a rule-compliant alternative, including no-op. A Governable Secure Super-Platform wraps the REM in a TPM-based trusted boot chain, verifies signatures of REM code and rules before loading, keeps keys in tamper-resistant chips, and gives actuator access to the REM alone. The proof chains these links: signature correctness and hash collision resistance force the executed REM and l","pith_inferences":["The paper converts AI safety into a rule-authoring problem and explicitly leaves rule completeness out of scope (H3); if a complete rule set cannot be written for an open-ended domain, the cryptographic guarantee still holds but the safety that matters depends entirely on rule quality.","A natural stress test the paper never runs: a full-knowledge red team attacking a GAI prototype through software and network paths only, measuring how close real TPM and OS stacks come to the assumed self-defense (H2).","The decoupling of rules from platform suggests a concrete near-term pilot: regulators authoring machine-checkable rules directly into REM rule sets for high-risk systems, making safety review a governance ceremony rather than a vendor engineering task.","Editorial note on the proof text: step S9 in Sec. VI-C reads 'Based on S9 and H3' where the intended antecedent is the previous step, S8; reindexing the derivation removes the slip without changing the conclusion."],"forward_implications":["AI behavior at the actuator is capped by a safety floor that does not depend on the AI's honesty, alignment, or competence.","Safety updates become policy acts: new rules can be drafted and signed by non-technical authorities and loaded without rewriting the AI or the REM software.","The same verified REM engine can be reused across domains, since governance rules are data rather than code.","Existing safety methods (alignment, hardening, kill switches) are repositioned as upper-bound optimizers inside a hardened boundary, not as the last line of defense.","A formal guarantee of command acceptability is achieved under the paper's extreme threat model (omniscient, maximally adversarial AI), provided its premises hold."],"supporting_citations":[{"why":"supplies the TPM hardware root of trust on which the GSSP's tamper-resistance claims are built","marker":"[25]"},{"why":"describes the secure boot chain that validates OS and REM, backing the blocking of attack paths P4-P6","marker":"[26]"},{"why":"gives the UF-CMA unforgeability result for Ed25519 that underpins the claim that signatures cannot be forged","marker":"[43]"},{"why":"supports the claim that a TPM-based trusted boot can keep the controller OS uncompromised","marker":"[24]"},{"why":"cited to argue the REM's bounded input space can be exhaustively verified against implementation bugs (P1)","marker":"[27]"},{"why":"the prior 'control problem is unsolvable' position that the paper's external-enforcement claim is framed against","marker":"[13]"},{"why":"the key-management standard behind the claim that private keys never leave the cryptographic chip (P9)","marker":"[44]"},{"why":"the PKCS#11 hardware interface used for the USB-key signature terminals that protect P9","marker":"[46]"},{"why":"a mature, audited rule engine offered as evidence that an industrial-grade REM is feasible","marker":"[32]"}],"fun_headline_variants":["Even superintelligent AI can't bypass this crypto rule gate","Provable AI safety: crypto gate blocks every unsafe command","Governable AI: provable crypto gate for human rules","Crypto rule gate: provable AI safety under extreme threat models","Crypto gate provably forces AI commands to obey human rules"],"cache_read_input_tokens":2688,"weakest_assumption_plain":"The load-bearing premise is H3: that people can write a rule set such that, in every reachable state, every command the REM lets through is acceptable — the paper concedes it treats rule completeness as an assumption 'beyond the scope' of the technical proof, and if even one situation is missing from the rules, the guarantee inherits that gap.","fun_headline_variants_meta":{"raw":{"variants":["Even superintelligent AI can't bypass this crypto rule gate","Provable AI safety: crypto gate blocks every unsafe command","Governable AI: provable crypto gate for human rules","Crypto rule gate: provable AI safety under extreme threat models","Crypto gate provably forces AI commands to obey human rules"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.002466,"raw_usage":{"total_tokens":9327,"prompt_tokens":789,"completion_tokens":8538,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":533,"completion_tokens_details":{"reasoning_tokens":8453}},"tokens_in":533,"tokens_out":8538,"duration_ms":64918,"temperature":1.0,"reasoning_tokens":8453,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-05T15:05:12.428232+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Red-team a GAI prototype with full source knowledge and software-only access: any success in placing an unrectified command on an actuator port falsifies the non-bypassability claim (H2/P6). Separately, domain experts can falsify the rule-completeness premise by exhibiting one reachable state where the rule set admits a rectified command that still causes harm.","supporting_citations":[{"cited_title":"Trusted platform module,","cited_arxiv_id":null,"evidence_quote":"supplies the TPM hardware root of trust on which the GSSP's tamper-resistance claims are built"},{"cited_title":"Research on trusted com- puting and its development,","cited_arxiv_id":null,"evidence_quote":"describes the secure boot chain that validates OS and REM, backing the blocking of attack paths P4-P6"},{"cited_title":"High-speed high-security signatures,","cited_arxiv_id":null,"evidence_quote":"gives the UF-CMA unforgeability result for Ed25519 that underpins the claim that signatures cannot be forged"},{"cited_title":"Design and implementation of trusted boot based on a new trusted computing dual- architecture,","cited_arxiv_id":null,"evidence_quote":"supports the claim that a TPM-based trusted boot can keep the controller OS uncompromised"},{"cited_title":"An extensive investigation of condition reachability using cbmc: Study on negative results,","cited_arxiv_id":null,"evidence_quote":"cited to argue the REM's bounded input space can be exhaustively verified against implementation bugs (P1)"},{"cited_title":"On controllability of artificial intelli- gence,","cited_arxiv_id":null,"evidence_quote":"the prior 'control problem is unsolvable' position that the paper's external-enforcement claim is framed against"},{"cited_title":"Nist special publication 800-57 part 1, revision 4,","cited_arxiv_id":null,"evidence_quote":"the key-management standard behind the claim that private keys never leave the cryptographic chip (P9)"},{"cited_title":"On the security of pkcs# 11,","cited_arxiv_id":null,"evidence_quote":"the PKCS#11 hardware interface used for the USB-key signature terminals that protect P9"},{"cited_title":"Clips user’s guide,","cited_arxiv_id":null,"evidence_quote":"a mature, audited rule engine offered as evidence that an industrial-grade REM is feasible"}],"review_version":1}