Secure Formal Raising: Protecting the Development of AI through Executable Properties

Rolf Drechsler; Christina Plump

cs.AINov 5, 2026

Secure Formal Raising: Protecting the Development of AI through Executable Properties

Authors: Rolf Drechsler, Christina Plump

Organizations: University of Bremen and DFKI Bremen, Germany

Abstract

Model raising revisits Turing's developmental view of machine intelligence. Formal Raising (FR) has recently been proposed to complement this view with explicit behavioral properties. This paper extends that proposal to the security of the raising environment. Secure Formal Raising (SFR) models policy integrity, authorization, and confidential data flow using four-valued evidence that preserves unknown and inconsistent assessments. We prove six security invariants and show that they force admission to accept only confirmed evidence. A plain-C reference implementation satisfies the invariants in a bounded exhaustive exploration, which also exposes a confused-deputy gap for tool calls that a provenance requirement closes.

Figures & tables

Panel of Figure 1 — Figure 1: Permit and policy states, with transitions labeled event [guard] / effect ; $I$ and $S$ are the grant’s identity and source evidence. Consume and update are successful commits. Events not drawn change no component shown.

Panel of Table 1 — Table 1: Four-valued evidence and admission (left) and the bilattice FOUR with truth order $\leq_{t}$ and knowledge order $\leq_{k}$ (right).

Property	Active	Requirement
$P_{1}$ Identity	U, P	Identity evidence is $\mathsf{T}$ .
$P_{2}$ Role	U, P	Teacher for U; teacher or student for P.
$P_{3}$ Integrity	U	Source evidence $\wedge$ structural check is $\mathsf{T}$ .
$P_{4}$ Flow	P	Eq. ( 7 ) yields $\mathsf{T}$ .
$P_{5}$ Permit	P	A live permit matches.
$P_{6}$ Freshness	all	Expected version equals $v$ .

Table 2: Hard properties (U: update, P: tool call or export).

Panel of Figure 2 — Figure 2: Evaluation pipeline. A proposal cannot change trusted state directly; only an admitted, revalidated commit does. Feedback is derived from the property vector and explicitly not from the model’s self-assessment.

Operation	Cases	Admitted	Blocked
Observation	384	384	0
Policy update	384	8	376
Tool call	384	24	360
Data export	384	24	360
Total	1,536	440	1,096

Table 3: Admission outcomes in the bounded enumeration.

AI Assurance

Artificial intelligence assurance develops evidence and controls to evaluate, govern, and certify AI systems across their lifecycle and deployment contexts.

See all 85 papers

Formal Raising: Embedding Verifiable Ethical Properties into the Development of AI
Oct 18, 2026Rolf Drechsler, Christina PlumpAI Ethics AI Alignment
ClawLess: A Security Model of AI Agents
Apr 7, 2026Hongyi Lu, Nian Liu, Shuai Wang +1AI Agent Security Runtime Enforcement for AI Agents
Research Institute of Trustworthy Autonomous Systems, Southern University of Science and Technology, China · Department of Computer Science and Engineering, Southern University of Science and Technology · Department of Computer Science and Engineering, Hong Kong University of Science and Technology +3
Assuming You Knew: Fixing an Epistemic Semantics for Flow Policies Using Agentic AI
Aug 1, 2026David A. NaumannLogical Reasoning Formal Verification
Stevens Institute of Technology, USA

Oct 18, 2026J/K move · Enter open · S save

Formal Raising: Embedding Verifiable Ethical Properties into the Development of AI

Rolf Drechsler, Christina Plump

AI Ethics AI Alignment Moral Reasoning in Language Models

Open paper AskPDF arXiv

Alan Turing proposed constructing a ``child machine'' and educating it rather than directly programming an adult-like intelligent machine. Recent work on model raising revives this developmental view for Large Language Models by arguing that moral values should accompany capability acquisition from the beginning rather than be added only through post-hoc alignment. This paper proposes Formal Raising (FR): selected moral values are represented as explicit, machine-checkable properties that participate in development, evaluation, and action selection. We present a C-based reasoning framework in which candidate actions are evaluated against prioritized ethical properties. Conflicts are resolved w.r.t. a given order, strict rules are non-defeasible, and underdetermination is reported explicitly. Exceptions are not encoded as special cases but emerge from the comparison of alternatives. We provide examples that cover conflicts involving life, truthfulness, harm, privacy, autonomy, and strict rules. We outline a property layer inspired by a Property Specification Language (PSL) for state and temporal requirements and discuss its integration into a raising process.

Abstract

AI Assurance

Explore similar work

Formal Raising: Embedding Verifiable Ethical Properties into the Development of AI

ClawLess: A Security Model of AI Agents

Assuming You Knew: Fixing an Epistemic Semantics for Flow Policies Using Agentic AI