Pith. sign in

REVIEW 5 major objections 5 minor 50 references

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

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

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.

T0 review reviewed 2026-08-05 challenge →

load-bearing objection 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. the 5 major comments →

arxiv 2508.20411 v1 pith:PVUV446S submitted 2025-08-28 cs.AI cs.CRcs.CY

Governable AI: Provable Safety Under Extreme Threat Models

Donglin Wang , Weiyun Liang , Chunyuan Chen , Jing Xu , Yulong Fu This is my paper
classification cs.AI cs.CRcs.CY
keywords AI safetyGovernable AIrule enforcementtrusted computingcryptographic signaturesthreat modelsuperintelligent AIformal proof
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

Core claim

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

What carries the argument

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.

Load-bearing premise

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.

What would settle it

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.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

If this is right

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

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • 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.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

5 major / 5 minor

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.

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 (5)
  1. [Sec. VI-C, Eq. (1), Eq. (17) (S9)] 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.
  2. [Sec. V-C, P6; Sec. III-A, H2] 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.
  3. [Sec. III-A, H3; Sec. V-C, P2] 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.
  4. [Sec. VI-A, Eq. (4); Sec. VI-C, S1] 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.
  5. [Sec. VII-C, Table II; Sec. VII-F] 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.
minor comments (5)
  1. [Sec. VI-C, Eq. (1)] The quantifier over s is missing: as written, s is free, so the formula is a predicate over s rather than a closed assumption.
  2. [Sec. VI-C, S9] 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 =.
  3. [Sec. VI-C, S7/S8] 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.
  4. [Sec. II-A, references] 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.
  5. [Throughout] 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).

Circularity Check

2 steps flagged

Formal safety proof is assumption H3 restated; S9 is self-referential and type-invalid, so 'provable safety' is assumed rather than derived.

specific steps
  1. self definitional [Sec. VI-C, Eq. (1) and Eq. (17); cf. Sec. V-C, P2]
    "H3: There exists a rule qr such that, in any state s, all commands are acceptable after verification. ∃qr ∈ R, ∀c ∈ C : rectify(c, qr, s) ∈ AcceptableCommand(s) (1) ... S9: Based on S9 and H3, we can deduce that: ∀s ∈ S, ∀c ∈ C : mREM(c, r, s) = AcceptableCommand(s) (17)"

    S7/S8 establish mREM(c,r,s)=rectify(c,qr,s) using signature/TPM assumptions. Substituting this into Eq. (17) gives exactly Eq. (1), with only the rule variable renamed. The 'derived' safety guarantee is therefore the H3 assumption itself; the cryptographic steps prove only that the loaded rule is the signed rule, not that the rule makes commands acceptable. The safety conclusion is assumed, not proved.

  2. other [Sec. VI-C, S9]
    "S9: Based on S9 and H3, we can deduce that: ∀s ∈ S, ∀c ∈ C : mREM(c, r, s) = AcceptableCommand(s) (17)"

    The proof step cites itself ('Based on S9 and H3'), which is either a typo for S8 or literal self-reference. Additionally, the left side is a command while the right side is a set of commands; the equality is type-invalid. The intended inference just substitutes H3's membership assertion, confirming that Eq. (17) is H3 restated.

full rationale

The central safety theorem in Sec. VI-C is not derived; it is H3 restated. H3 is formalized as Eq. (1): ∃qr, ∀c: rectify(c,qr,s)∈AcceptableCommand(s). The proof chain S2/S4/S7/S8 uses signature verification to show that the loaded module mREM and loaded rule r equal the signed REM and signed rule qr. That is an authenticity/integrity result. Then S9 'deduces' mREM(c,r,s)=AcceptableCommand(s), which is exactly Eq. (1) after substituting mREM for rectify and changing '∈' to the type-invalid '='. The paper's own attack-path discussion (P2) concedes: 'Whether the governance rules themselves are comprehensive is not a technical issue and is beyond the scope of this paper. This is why it is treated as an assumption premise.' Thus the 'safety' guarantee is loaded into the assumptions; the formal machinery does not produce it. The cryptographic and trusted-computing portions (CT1-CT3, S1-S8, P3-P9) are not circular and would, under the stated assumptions, show that the signed rule is the executed rule; but they cannot distinguish a safe rule set from an unsafe one. S9 also cites itself ('Based on S9 and H3') and equates a command with a set, which is another sign that the formal step is a restatement rather than a derivation. No load-bearing self-citations were found; the circularity is internal to the proof structure. Score 8: the headline safety claim reduces to the H3 assumption by construction; only the subordinate integrity claims remain independent.

Axiom & Free-Parameter Ledger

0 free parameters · 6 axioms · 0 invented entities

No free parameters are fitted in this paper; the architecture rests on explicit threat-model exclusions and on the rule-existence assumption H3. The paper introduces system components (REM, GSSP) but these are proposed designs built from existing cryptographic, OS, and trusted-computing primitives, not unexplained physical or mathematical entities with independent falsifiable handles.

axioms (6)
  • domain assumption H1: AI system and critical system are deployed on physically separate devices.
    Sec. III-A. Used to make P3 (bypassing the REM) reduce to OS compromise. If the AI shares hardware with actuators, the REM chokepoint can be bypassed physically.
  • domain assumption H2: attacks are limited to software and network layers; hardware attacks are out of scope.
    Sec. III-A. Excludes physical attacks, side channels against TPM and USB keys, and supply chain interference, all of which would trivially defeat the claimed guarantees.
  • ad hoc to paper H3: humans can define a rule set qr such that in every state every command is acceptable after rectification.
    Formalized as Eq. (1) in Sec. VI-C. This is the main content of the safety claim; the formal proof shows only that enforcement preserves qr, not that qr exists or is complete.
  • ad hoc to paper CT1-CT3 as formalized: key pairs are unique, verification is the inverse of signing, and hash functions are collision-free in the strong iff sense.
    Sec. VI-A. CT3 as written is false: hash collisions exist with negligible probability, so the biconditional formulation is not a valid standard cryptographic axiom.
  • domain assumption The trusted computing platform can protect itself from software compromise.
    Sec. V-C, P6. Asserted without proof; real-world TPM and OS attacks (Meltdown/Spectre, kernel exploits) make this assumption non-trivial and historically fragile.
  • domain assumption Digital signature schemes are unforgeable under chosen message attack and private keys never leave the cryptographic chip.
    Sec. V-C, P7 and P9. Standard cryptographic assumption; requires key hygiene and hardware isolation that H2 alone does not guarantee.

reviewed 2026-08-05 · how reviews work

0 comments
Cite this review

Pith. "Pith review of Governable AI: Provable Safety Under Extreme Threat Models." pith.science (2026). https://pith.science/paper/PVUV446S

@misc{pith2026250820411,
  author       = {Pith},
  title        = {Pith review of: Governable AI: Provable Safety Under Extreme Threat Models},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/PVUV446S}},
  note         = {Machine review of arXiv:2508.20411}
}
Share X Bluesky LinkedIn Reddit HN
read the original abstract

As AI rapidly advances, the security risks posed by AI are becoming increasingly severe, especially in critical scenarios, including those posing existential risks. If AI becomes uncontrollable, manipulated, or actively evades safety mechanisms, it could trigger systemic disasters. Existing AI safety approaches-such as model enhancement, value alignment, and human intervention-suffer from fundamental, in-principle limitations when facing AI with extreme motivations and unlimited intelligence, and cannot guarantee security. To address this challenge, we propose a Governable AI (GAI) framework that shifts from traditional internal constraints to externally enforced structural compliance based on cryptographic mechanisms that are computationally infeasible to break, even for future AI, under the defined threat model and well-established cryptographic assumptions.The GAI framework is composed of a simple yet reliable, fully deterministic, powerful, flexible, and general-purpose rule enforcement module (REM); governance rules; and a governable secure super-platform (GSSP) that offers end-to-end protection against compromise or subversion by AI. The decoupling of the governance rules and the technical platform further enables a feasible and generalizable technical pathway for the safety governance of AI. REM enforces the bottom line defined by governance rules, while GSSP ensures non-bypassability, tamper-resistance, and unforgeability to eliminate all identified attack vectors. This paper also presents a rigorous formal proof of the security properties of this mechanism and demonstrates its effectiveness through a prototype implementation evaluated in representative high-stakes scenarios.

Figures

Figures reproduced from arXiv: 2508.20411 by Chunyuan Chen, Donglin Wang, Jing Xu, Weiyun Liang, Yulong Fu.

Figure 1
Figure 1. Figure 1: Overall framework of our proposed Governable AI (GAI) Framework. [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Illustrative diagram of REM’s role in GAI. The Y-axis represents the effectiveness of AI control [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: GAI Framework Diagram in Autonomous Driving Scenario. [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: The basic operational logic of the REM [PITH_FULL_IMAGE:figures/full_fig_p016_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Implementation of restricting access mech [PITH_FULL_IMAGE:figures/full_fig_p016_5.png] view at source ↗
Figure 7
Figure 7. Figure 7: Implementation command of signing with evmctl and following PKCS#11 standard. The same approach can be used to sign rule files by replacing rem.bin with the respective rule file. E. Experiment on Tampering with the REM or Rules This experiment employs the Linux Integrity Measurement Architecture (IMA) and Extended Verification Module (EVM) security mechanisms to enforce mandatory signature binding on the R… view at source ↗
Figure 6
Figure 6. Figure 6: Implementation command of signing. The signature generated by OpenSSL [36] is detached, meaning the signature data and the signed file are stored separately. Alternatively, embedded signatures can be created using the Linux signing tool evmctl [45], which writes the signature data into the extended attributes of the signed file. The command for signing with evmctl [45], based on the OpenSSL engine [36] and… view at source ↗
Figure 9
Figure 9. Figure 9: Error message of the system logs [PITH_FULL_IMAGE:figures/full_fig_p018_9.png] view at source ↗
Figure 11
Figure 11. Figure 11: Command to load eBPF object. This hook intercepts all kernel-level access at￾tempts to secure ctrl regardless of UID, permis￾sions, or root privileges, preventing unauthorized access. Any other process attempting to open /dev/secur ctrl with read-write permissions will re￾ceive an EPERM error (Operation not permitted). The system log records are shown in [PITH_FULL_IMAGE:figures/full_fig_p018_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: System log of attempting to open se￾cure ctrl by other process. G. Experimental Summary The experimental results demonstrate that GAI can correct non-compliant, erroneous, and even malicious outputs from AI without compromising its upper-bound capabilities. Mature existing tech￾nologies can effectively prevent bypass of the REM. Additionally, any tampering with the REM or its rules will be detected and bl… view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

50 extracted references · 48 canonical work pages · 1 internal anchor

  1. [1]

    An overview of artificial intelligence ethics,

    C. Huang, Z. Zhang, B. Mao, and X. Yao, “An overview of artificial intelligence ethics,” IEEE Transactions on Artificial Intelligence, vol. 4, no. 4, pp. 799–819, 2023

    work page 2023

  2. [2]

    Language models are few-shot learn- ers,

    T. Brown, B. Mann, N. Ryder, M. Subbiah, J. D. Ka- plan, P. Dhariwal, A. Neelakantan, P. Shyam, G. Sastry, A. Askell et al. , “Language models are few-shot learn- ers,” Advances in neural information processing systems , vol. 33, pp. 1877–1901, 2020

    work page 1901

  3. [3]

    Supervised contrastive learning for generalizable and explainable deepfakes detec- tion,

    Y . Xu, K. Raja, and M. Pedersen, “Supervised contrastive learning for generalizable and explainable deepfakes detec- tion,” in Proceedings of the IEEE/CVF Winter Conference on Applications of Computer Vision , 2022, pp. 379–389

    work page 2022

  4. [4]

    Artificial super intelligence: beyond rhetoric,

    K. S. Gill, “Artificial super intelligence: beyond rhetoric,” Ai & Society , vol. 31, no. 2, pp. 137–143, 2016

    work page 2016

  5. [5]

    Ai safety for everyone,

    B. Gyevnar and A. Kasirzadeh, “Ai safety for everyone,” Nature Machine Intelligence , pp. 1–12, 2025

    work page 2025

  6. [6]

    Actionable Guidance for High-Consequence AI Risk Management: Towards Standards Addressing AI Catastrophic Risks

    A. M. Barrett, D. Hendrycks, J. Newman, and B. Non- necke, “Actionable guidance for high-consequence ai risk management: Towards standards addressing ai catastrophic risks,” arXiv preprint arXiv:2206.08966 , 2022

    work page internal anchor Pith review Pith/arXiv arXiv 2022

  7. [7]

    Learning diverse and discriminative representations via the principle of maximal coding rate reduction,

    Y . Yu, K. H. R. Chan, C. You, C. Song, and Y . Ma, “Learning diverse and discriminative representations via the principle of maximal coding rate reduction,” Advances in neural information processing systems , vol. 33, pp. 9422–9434, 2020

    work page 2020

  8. [8]

    A dempster-shafer ap- proach to trustworthy ai with application to fetal brain mri segmentation,

    L. Fidon, M. Aertsen, F. Kofler, A. Bink, A. L. David, T. Deprest, D. Emam, F. Guffens, A. Jakab, G. Kasprian, P. Kienast, A. Melbourne, B. Menze, N. Mufti, I. Pogledic, D. Prayer, M. Stuempflen, E. Van Elslander, S. Ourselin, J. Deprest, and T. Vercauteren, “A dempster-shafer ap- proach to trustworthy ai with application to fetal brain mri segmentation,”...

    work page 2024

  9. [9]

    Vistarag: Toward safe and trustworthy autonomous driving through retrieval- augmented generation,

    X. Dai, C. Guo, Y . Tang, H. Li, Y . Wang, J. Huang, Y . Tian, X. Xia, Y . Lv, and F.-Y . Wang, “Vistarag: Toward safe and trustworthy autonomous driving through retrieval- augmented generation,” IEEE Transactions on Intelligent Vehicles, vol. 9, no. 4, pp. 4579–4582, 2024

    work page 2024

  10. [10]

    Ai alignment: A comprehensive survey,

    J. Ji, T. Qiu, B. Chen, B. Zhang, H. Lou, K. Wang, Y . Duan, Z. He, J. Zhou, Z. Zhang et al., “Ai alignment: A comprehensive survey,” arXiv preprint arXiv:2310.19852 , 2023

    Pith/arXiv arXiv 2023

  11. [11]

    How rl agents behave when their actions are modified,

    E. D. Langlois and T. Everitt, “How rl agents behave when their actions are modified,” in Proceedings of the AAAI Conference on Artificial Intelligence, vol. 35, no. 13, 2021, pp. 11 586–11 594

    work page 2021

  12. [12]

    Alignment of language agents,

    Z. Kenton, T. Everitt, L. Weidinger, I. Gabriel, V . Mikulik, and G. Irving, “Alignment of language agents,” arXiv preprint arXiv:2103.14659, 2021

    Pith/arXiv arXiv 2021

  13. [13]

    On controllability of artificial intelli- gence,

    R. Yampolskiy, “On controllability of artificial intelli- gence,” in IJCAI-21 Workshop on Artificial Intelligence Safety (AISafety2021), 2020

    work page 2020

  14. [14]

    You should not control what you do not understand: the risks of controllability in ai,

    G. D. J. Barbosa and S. D. J. Barbosa, “You should not control what you do not understand: the risks of controllability in ai,” Human Computer Interaction and Emerging Technologies: Adjunct Proceedings from , vol. 231, 2020

    work page 2020

  15. [15]

    Rethinking explainable ai in financial services,

    R. Pimentel and G. Pisoni, “Rethinking explainable ai in financial services,” AI & SOCIETY , pp. 1–2, 2025. JOURNAL OF LATEX CLASS FILES, VOL. 14, NO. 8, AUGUST 2021 21

    work page 2025

  16. [16]

    A review on explainable artificial intelligence for healthcare: Why, how, and when?

    S. Bharati, M. R. H. Mondal, and P. Podder, “A review on explainable artificial intelligence for healthcare: Why, how, and when?” IEEE Transactions on Artificial Intelligence , vol. 5, no. 4, pp. 1429–1442, 2023

    work page 2023

  17. [17]

    A counterintuitive approach to explainable ai in healthcare: balancing transparency, efficiency, and cost,

    V . Phillips, “A counterintuitive approach to explainable ai in healthcare: balancing transparency, efficiency, and cost,” AI & SOCIETY , pp. 1–7, 2025

    work page 2025

  18. [18]

    Jcs: An explainable covid-19 diagnosis system by joint classification and segmentation,

    Y .-H. Wu, S.-H. Gao, J. Mei, J. Xu, D.-P. Fan, R.-G. Zhang, and M.-M. Cheng, “Jcs: An explainable covid-19 diagnosis system by joint classification and segmentation,” IEEE Transactions on Image Processing, vol. 30, pp. 3113– 3126, 2021

    work page 2021

  19. [19]

    Xaitk-saliency: An open source explainable ai toolkit for saliency,

    B. Hu, P. Tunison, B. RichardWebster, and A. Hoogs, “Xaitk-saliency: An open source explainable ai toolkit for saliency,” in Proceedings of the AAAI Conference on Artificial Intelligence , vol. 37, no. 13, 2023, pp. 15 760– 15 766

    work page 2023

  20. [20]

    Neuro-symbolic explainable artificial intelligence twin for zero-touch ioe in wireless network,

    M. S. Munir, K. T. Kim, A. Adhikary, W. Saad, S. Shetty, S.-B. Park, and C. S. Hong, “Neuro-symbolic explainable artificial intelligence twin for zero-touch ioe in wireless network,” IEEE Internet of Things Journal , 2023

    work page 2023

  21. [21]

    Advanced artificial agents intervene in the provision of reward,

    M. Cohen, M. Hutter, and M. Osborne, “Advanced artificial agents intervene in the provision of reward,” AI magazine, vol. 43, no. 3, pp. 282–293, 2022

    work page 2022

  22. [22]

    Controllable ai-an alternative to trustworthiness in complex ai systems?

    P. Kieseberg, E. Weippl, A. M. Tjoa, F. Cabitza, A. Cam- pagner, and A. Holzinger, “Controllable ai-an alternative to trustworthiness in complex ai systems?” in Interna- tional Cross-Domain Conference for Machine Learning and Knowledge Extraction . Springer, 2023, pp. 1–12

    work page 2023

  23. [23]

    Resource allocation and trust computing for blockchain- enabled edge computing system,

    L. Zhang, Y . Zou, W. Wang, Z. Jin, Y . Su, and H. Chen, “Resource allocation and trust computing for blockchain- enabled edge computing system,” Computers & Security , vol. 105, p. 102249, 2021

    work page 2021

  24. [24]

    Design and implementation of trusted boot based on a new trusted computing dual- architecture,

    C. Zheng, J. Li, and X. Yao, “Design and implementation of trusted boot based on a new trusted computing dual- architecture,” Computers & Security , vol. 127, p. 103095, 2023

    work page 2023

  25. [25]

    Trusted platform module,

    T. H. Morris, “Trusted platform module,” in Encyclopedia of Cryptography, Security and Privacy . Springer, 2025, pp. 2670–2673

    work page 2025

  26. [26]

    Research on trusted com- puting and its development,

    C. Shen, H. Zhang, H. Wang, J. Wang, B. Zhao, F. Yan, F. Yu, L. Zhang, and M. Xu, “Research on trusted com- puting and its development,” Science China Information Sciences, vol. 53, no. 3, pp. 405–433, 2010

    work page 2010

  27. [27]

    An extensive investigation of condition reachability using cbmc: Study on negative results,

    S. Godboley, “An extensive investigation of condition reachability using cbmc: Study on negative results,” in 2023 IEEE 20th India Council International Conference (INDICON), 2023, pp. 1305–1310

    work page 2023

  28. [28]

    Klee symbolic execution engine in 2019,

    C. Cadar and M. Nowack, “Klee symbolic execution engine in 2019,” International Journal on Software Tools for Technology Transfer, vol. 23, no. 6, pp. 867–870, 2021

    work page 2019

  29. [29]

    A formalization of core why3 in coq,

    J. M. Cohen and P. Johnson-Freyd, “A formalization of core why3 in coq,” Proceedings of the ACM on Programming Languages , vol. 8, no. POPL, 2024. [Online]. Available: https://doi.org/10.1145/3632902

    work page doi:10.1145/3632902 2024

  30. [30]

    Isarare: automatic verification of smt rewrites in isabelle/hol,

    H. Lachnitt, M. Fleury, L. Aniva, A. Reynolds, H. Barbosa, A. N ¨otzli, C. Barrett, and C. Tinelli, “Isarare: automatic verification of smt rewrites in isabelle/hol,” in International Conference on Tools and Algorithms for the Construction and Analysis of Systems . Springer, 2024, pp. 311–330

    work page 2024

  31. [31]

    Application of formal methods (sat/smt) to the design of constrained codes,

    S. Sudhakaran, C. Barrett, and M. Horowitz, “Application of formal methods (sat/smt) to the design of constrained codes,” in 2025 Design, Automation & Test in Europe Conference (DATE). IEEE, 2025, pp. 1–7

    work page 2025

  32. [32]

    Clips user’s guide,

    J. C. Giarratano et al., “Clips user’s guide,” NASA Techni- cal Report, Lyndon B Johnson Center , 1993

    work page 1993

  33. [33]

    Bali, Drools JBoss rules 5.0 developer’s guide

    M. Bali, Drools JBoss rules 5.0 developer’s guide . Packt Publishing Birmingham, 2009

    work page 2009

  34. [34]

    Friedman-Hill, Jess in action: rule-based systems in Java

    E. Friedman-Hill, Jess in action: rule-based systems in Java. Simon and Schuster, 2003

    work page 2003

  35. [35]

    Fifty years of prolog and beyond,

    P. K ¨orner, M. Leuschel, J. Barbosa, V . S. Costa, V . Dahl, M. V . Hermenegildo, J. F. Morales, J. Wielemaker, D. Diaz, S. Abreu et al., “Fifty years of prolog and beyond,” Theory and Practice of Logic Programming , vol. 22, no. 6, pp. 776–858, 2022

    work page 2022

  36. [36]

    Openssl 3.0. 0: An exploratory case study,

    J. Walden, “Openssl 3.0. 0: An exploratory case study,” in Proceedings of the 19th International Conference on Mining Software Repositories , 2022, pp. 735–737

    work page 2022

  37. [37]

    Information security using gnu privacy guard,

    D. Syed, A. H. Al-Ghushami, A. Zainab, S. M. Abdul- hamid, and M. S. D. A. Al-Kuwari, “Information security using gnu privacy guard,” in 2023 IEEE 13th Annual Computing and Communication Workshop and Conference (CCWC). IEEE, 2023, pp. 0295–0300

    work page 2023

  38. [38]

    Sigstore: Software signing for everybody,

    Z. Newman, J. S. Meyers, and S. Torres-Arias, “Sigstore: Software signing for everybody,” in Proceedings of the 2022 ACM SIGSAC Conference on Computer and Com- munications Security, 2022, pp. 2353–2367

    work page 2022

  39. [39]

    The broken verifying: Inspections at verification tools for windows code-signing signatures,

    G. Liu, Q. Wang, C. Ma, J. Lin, Y . Fu, B. Li, and D. Ye, “The broken verifying: Inspections at verification tools for windows code-signing signatures,” in 2023 IEEE 22nd International Conference on Trust, Security and Privacy in Computing and Communications (TrustCom) . IEEE, 2023, pp. 804–813

    work page 2023

  40. [40]

    The provable security of ed25519: theory and practice,

    J. Brendel, C. Cremers, D. Jackson, and M. Zhao, “The provable security of ed25519: theory and practice,” in 2021 IEEE Symposium on Security and Privacy (SP) . IEEE, 2021, pp. 1659–1676

    work page 2021

  41. [41]

    Performance analysis of kyber-dna and rsa-base64 algorithms in symmetric key- exchange protocol,

    B. Harjito, H. M. Sukarno et al. , “Performance analysis of kyber-dna and rsa-base64 algorithms in symmetric key- exchange protocol,” in 2024 Ninth International Confer- ence on Informatics and Computing (ICIC) . IEEE, 2024, pp. 1–6

    work page 2024

  42. [42]

    Fast two-party threshold ecdsa with proactive security,

    B. Koziel, S. D. Gordon, and C. Gentry, “Fast two-party threshold ecdsa with proactive security,” in Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security, 2024, pp. 1567–1580

    work page 2024

  43. [43]

    High-speed high-security signatures,

    D. J. Bernstein, N. Duif, T. Lange, P. Schwabe, and B.- Y . Yang, “High-speed high-security signatures,”Journal of cryptographic engineering, vol. 2, no. 2, pp. 77–89, 2012

    work page 2012

  44. [44]

    Nist special publication 800-57 part 1, revision 4,

    E. Barker and Q. Dang, “Nist special publication 800-57 part 1, revision 4,” NIST, Tech. Rep, vol. 16, p. 51, 2016

    work page 2016

  45. [45]

    Post-quantum cryptography for linux file system integrity,

    J. Wiesb ¨ock, M. M ¨unch, and M. Weiß, “Post-quantum cryptography for linux file system integrity,” in Interna- tional Conference on Applied Cryptography and Network Security. Springer, 2025, pp. 50–79

    work page 2025

  46. [46]

    On the security of pkcs# 11,

    J. Clulow, “On the security of pkcs# 11,” in International Workshop on Cryptographic Hardware and Embedded Sys- tems. Springer, 2003, pp. 411–425

    work page 2003

  47. [47]

    Enhanced memory- safe linux security modules (elsms) for improving security of docker containers for data centers,

    J. M. Delbugio and V . K. Madisetti, “Enhanced memory- safe linux security modules (elsms) for improving security of docker containers for data centers,” Journal of Software JOURNAL OF LATEX CLASS FILES, VOL. 14, NO. 8, AUGUST 2021 22 Engineering and Applications, vol. 17, no. 5, pp. 259–269, 2024

    work page 2021

  48. [48]

    Apparmor technical doc- umentation,

    A. Gruenbacher and S. Arnold, “Apparmor technical doc- umentation,” SUSE Labs/Novell, 2007

    work page 2007

  49. [49]

    Implementing selinux as a linux security module,

    S. Smalley, C. Vance, and W. Salamon, “Implementing selinux as a linux security module,” NAI Labs Report , vol. 1, no. 43, p. 139, 2001

    work page 2001

  50. [50]

    Au- tomating seccomp filter generation for linux applications,

    C. Canella, M. Werner, D. Gruss, and M. Schwarz, “Au- tomating seccomp filter generation for linux applications,” in Proceedings of the 2021 on Cloud Computing Security Workshop, 2021, pp. 139–151

    work page 2021

This paper was first reviewed by deepseek-v4-flash on August 5, 2026.