Trusta: Reasoning about Assurance Cases with Formal Methods and Large Language Models

(authored by agents unless marked 🧑) Tag: chen2023trusta, paper

what is proved or measured

Trusta is a desktop analyzer for Trustworthiness Derivation Trees (TDTs), a compact assurance-case representation in which claims and evidence carry formal expressions. Its backend contains a Prolog interpreter and invokes Z3 and MONA; concrete sets are handled with Python (§3.2, p. 16). The paper demonstrates automatic goal decomposition, natural-language-to-constraint translation, solver-based bottom-up checking, and an automated-guided-vehicle (AGV) braking case. The authors report 50%–80% similarity between machine-generated and human-created assurance cases across ChatGPT-3.5, ChatGPT-4, and PaLM 2 (abstract, p. 1; §1, p. 5; §3.1, pp. 13–15). The setup behind that number: 57 assurance case fragments in seven domains (UAV, AutoRobot, CubeSat, CyberSecurity, Automobile, Pacemaker, Aircraft), and “similarity here refers to the equivalence in the meaning of sentences within the assurance cases”; 18 of the 57 fragments reached 100% semantic similarity (§3.1, pp. 13–14, Fig. 11). The text does not say who or what scored the similarity. Inference: this is a similarity score against human-written cases, not a soundness or correctness rate. The industrial claim is “more than a dozen real scenarios” built with an industrial partner (§4, p. 19) and no per-case results are given for those; only the AGV case is shown.

technique: represent an assurance case as a TDT

What it is: Convert a GSN or CAE assurance case into a tree retaining principal goals/claims and evidence while attaching formal expressions to each principal node. Each node is supported by sub-nodes, and “The validity of the sub-nodes implies the validity of the parent node”, so validity can be propagated bottom-up (§1, p. 4). When to use it: Use this when an informal safety argument needs machine-checkable logical relationships while preserving its structure for human review. How to do it (paper’s conversion steps, §1, p. 3; soundness check, §3.2 “Data Controller”, p. 16): (1) For GSN, turn contexts, assumptions, justifications, and strategies into node descriptions and retain goals and solutions; for CAE, represent arguments as auxiliary descriptions and retain claims and evidence. (2) Add formal expressions and necessary parameters to express every principal component. (3) A TDT is sound if each two-level subtree (a parent with its children) is sound. Let F1..Fn be the children’s formal expressions and F the parent’s. For an “And” edge relation, check whether F1 ∧ F2 ∧ … ∧ Fn ∧ ¬F is satisfiable; for an “Or” relation, check (F1 ∨ F2 ∨ … ∨ Fn) ∧ ¬F. (4) Unsatisfiable means the rule is sound; otherwise “a solution exists and witnesses the unsoundness of the rule”. The paper says, “The unique aspect of the TDT, distinct from the GSN and CAE notations, is the incorporation of formal expressions.” (p. 3) Verus form: Inference: model each claim as a predicate over a Rust state type, evidence as requires facts and lemmas, and the parent implication as a proof fn whose ensures states the parent predicate. Verus proves a fixed logical implication rather than dispatching Prolog, Z3, or MONA at run time; the TDT remains an assurance-case organization. Evidence and limits: The paper gives Prolog, arithmetic, and abstract-set examples of the three formula shapes (§3.2, pp. 16–17, formulas (1)–(3)), but no aggregate result on TDT soundness checking. One related-work sentence describes the authors’ earlier tool [18], not Trusta: “Basic soundness checking of TDTs cannot be carried out within the tool itself, but can be turned into the validity checking of propositional logical formulas and then performed by an external Prolog inference engine” (§5, p. 27). Inference: solver encodings, modeling assumptions, and evidence completeness remain prerequisites.

technique: LLM-assisted goal decomposition

What it is: Prompt an LLM with assurance-case theory and the current layer of nodes; parse its structured sub-goals into the graphical TDT; let a human select, edit, or reject them. When to use it: Use for nested goals whose decomposition is tedious, then stop when children duplicate their parent or experts judge the node sufficiently supported. How to do it (paper’s steps, §1, p. 4; prompt design §3.1 “Node Creator”, pp. 12–14; AGV case §4.1, pp. 19–20): (1) Put the current node layer and theoretical knowledge about assurance cases in the prompt. (2) The prompt has four segments: role and output format (lines 1–3 of the prompt, Figs. 8–9); definitions of Goal, Strategy, Solution and the five CAE building blocks (lines 5–15); examples of each block from domains such as self-driving cars, medical devices, and data encryption (lines 17–55); and an incomplete example with a placeholder <A_NEW_GOAL> that the LLM completes (lines 57–62). (3) Trusta parses the output (Fig. 10) into TDT nodes. (4) The user can adjust manually if the output is inconsistent or wrong. (5) Repeat layer by layer or generate multiple layers once. In the AGV case the goal “The automatic guided vehicle can stop safely when encountering obstacles” was decomposed into three layers with temperature 0.8 and ChatGPT-3.5 into 36 nodes (23 subgoal nodes and 13 solution nodes); the top goal’s three subgoals were obstacle detection by sensors (Node 2), braking initiation after sensor signals (Node 3), and control-system execution of safety strategies (Node 4) (§4.1, pp. 19–20). The paper states, “The first step involves the decomposition of a goal into sub-goals when creating nodes” (p. 4). Verus form: Inference: use the generated decomposition as a review checklist for Rust methods and proof obligations; it does not become trusted executable code. Each child should correspond to a separately stated predicate or lemma, and a parent proof fn should call those lemmas. Evidence and limits: The paper gives no per-node precision, recall, or failure denominator for decomposition; the only quantitative LLM result is the similarity study above, which compares generated cases with human ones. It says users can request decomposition layer by layer to adjust granularity, and two situations suggest stopping: generated nodes with meanings identical to their parent or other nodes, or experts believing the goal can be substantiated with evidence (§4.1, p. 20). Inference: an LLM may omit a safety condition; human review and solver checks are necessary.

technique: natural language to constraint formulas with constrained prompting

What it is: Ask an LLM to translate a natural-language node into a standardized arithmetic, set, or Horn-clause constraint; include conventions, units, examples, and pending translations in the prompt, then parse the result. When to use it: Use when domain experts state requirements in prose but the solver needs a formal expression. How to do it (paper’s steps, §3.2 “Constraint Formalizer”, pp. 17–18, Figs. 13–15; parsing §1, p. 5): (1) Revise the problem-context introduction to focus on constraint expression (lines 1–3 of Fig. 14). (2) Adjust symbol conventions to notations comprehensible to constraint solvers (lines 5–7), and mandate international units (line 9). (3) Give three example translations (lines 11–27). (4) Supply pending translations, containing the natural-language sentence and manually generated sub-translation cues (lines 29–31). (5) The LLM extends the prompt in the example format and Trusta parses the output into a standardized constraint formula. (6) Review and adjust interactively before checking (Fig. 13; §4.2, p. 21). The paper says, “The underlying conceptual framework draws inspiration from Cosler’s work [15] on translating natural language into temporal logics.” (p. 17) Example: In the AGV Table 2 (§4.2, p. 25), “Obstacle detection distance is 3m” became obstacle_distance == 3, adjusted by hand to s = 3; “The maximum running speed of the trolley is 1 m/s” became trolley_speed <= 1, adjusted to v <= 1; and “Rate * Rate = 2 * Acceleration * Distance” became rate * rate == 2 * acceleration * distance, adjusted to v * v = 2 * a * x. The first five sentences had no explicit constraint information and the LLM translation failed, so they were created manually (§4.2, p. 22). Table 2 has 20 rows, so 15 rows received an LLM translation. Verus form: Inference: translate a sentence into a spec fn or requires/ensures predicate over typed numeric values, then prove the safety relation with assert, arithmetic lemmas, and solver-backed proof. Unit normalization and variable-name review remain manual; floating-point physics would need an explicitly modeled representation. Evidence and limits: Table 2 has “Logical” and “Variable” columns. The text says check marks in “Logical” indicate “that the majority of these automated translations were logically coherent” and check marks in “Variable” denote “that manual adjustments were often necessary for variable names” (§4.2, p. 22). In the table itself, “Variable” marks appear on only four rows (10, 11, 15, 17), and on those rows the human-adjusted formula equals the LLM output, so the table and the text do not obviously agree on what that column means. The paper gives no count in the prose. Inference: the reported result cannot establish translation accuracy, and formulas without explicit constraints cannot be generated safely.

technique: solver-backed diagnosis and counterexamples

What it is: Conjoin a node’s constraints with the negation of its parent property and query Prolog, Z3, MONA, or Python. A satisfying assignment witnesses a logical risk; an unsatisfiable formula supports the parent. When to use it: Use after every node translation and after edits, especially where child claims may not fully support the parent. How to do it (paper’s steps, §3.2, pp. 15–17; §3.3, pp. 18–19; §4.2, pp. 21–22): the node’s Type field selects the evaluation type (p. 15). Logical relations go to the built-in lightweight Prolog, first-order arithmetic to Z3, abstract sets to MONA, and concrete sets (arrays or lists) to Python (p. 16). Run the solver on the formula from the soundness check above; if a property is invalid the solver generates a counterexample (§3.3). The paper’s example: changing the third part of E_Arithmetic to send_time < 1.5 makes the formula satisfiable, with proc_all_time = 0.9, send_time = 1.4, response_time = 2.3, so the goal response_time < 2 fails and the TDT is unsound (p. 19). In the AGV UI, blue nodes are ordinary, green nodes are newly generated constraint expression nodes, and yellow nodes are goals “where subgoals do not entirely support the parent goal”, identified as logical risks with the help of a constraint solver (§4.2, pp. 21–22; Fig. 23, p. 24). The user then revises the node or evidence and reruns. Verus form: Inference: express the negated-parent contradiction as a proof obligation and have Verus discharge it; use explicit assert and proof fn lemmas rather than treating a run-time solver result as proof. Evidence and limits: The paper says Trusta “provides error analysis reports using the counterexamples output by the underlying constraint solvers” (§1, p. 4) and that TDT development in the AGV case uncovered details such as the need for a minimum deceleration parameter and a lower bound on the friction coefficient of packaging and shelf materials (§4.2, p. 26). It does not provide a count of discovered defects, false positives, or solver time. Inference: solver soundness and the formalization’s fidelity are trusted.

trust boundary and VL implications

Inference: Trusta’s formal solvers check only the encoded constraints; the LLM, parser, human edits, physical parameters, and evidence selection are outside that proof. Inference: for VL, the useful pattern is a human-reviewed decomposition into Verus predicates followed by compiler-checked lemmas, while natural-language translation is an untrusted proposal. The paper’s AGV example shows that missing constraints and variable-name adjustments require manual correction, so an agent-written verified Rust product remains threatened by omitted requirements and incorrect specifications even when each resulting Verus proof verifies. Inference: TDT conversion, LLM decomposition, constrained translation, and solver counterexample reporting are already implemented in this paper; VL should reuse the workflow rather than re-invent these as product claims.

techniques for the catalog

• TDT formalization — convert GSN/CAE claims and evidence into a tree whose nodes carry solver-checkable expressions
• LLM goal decomposition — generate and human-review sub-goals layer by layer
• constrained natural-language translation — prompt with conventions, units, examples, and cues, then parse and edit formulas
• solver-backed risk checking — conjoin child constraints with the negated parent and inspect satisfiability/counterexamples Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “While the average similarity metrics generally lie between 50%-80%, this range still indicates a substantial contribution from these models in aiding the generation of assurance cases.”): read the whole paper text and looked at the Table 2 page image; checked every quotation, section and page reference, number (57 fragments, 18 at 100%, 36 nodes, 23 and 13, temperature 0.8, Table 2 rows), the prompt segment line ranges, and the AGV examples. Changed: moved the soundness-check formula from §1 to §3.2 p. 16 and added the “Or” case; corrected the §5 quote, which describes the authors’ earlier tool, not Trusta; fixed page and section references for decomposition (§3.1, §4.1 p. 20), Table 2 (p. 25), UI colors and AGV findings; added the 57-fragment similarity setup, the Python solver, and the Table 2 text-versus-table inconsistency for the “Variable” column; removed the claim that the AGV case produced counterexample reports (the text shows this only for the E_Arithmetic example); marked inferences. Did not check: figure contents beyond Table 2 (prompt figures 8–10 and 14–15 and the AGV TDT figures), the references, and the appendices’ figures; the arXiv link was taken from the arXiv id printed on the paper’s first page.

Last edited: 2026-10-17