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

arXiv: https://arxiv.org/abs/2309.12941 · HTML: https://mlsanity.com/paper/2309.12941/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning for agents, planning and code, one of 17 directions in LLM reasoning.
- Builds on 5 of its 54 references that are in the map.
- First posted on arXiv 22 Sep 2023.

## Placed in

- LLM reasoning / [Reasoning for agents, planning and code](https://mlsanity.com/lr/reasoning-for-agents-planning-and-code/)

## Builds on (most cited first, 5 of 5)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Evolution of Semantic Similarity -- A Survey](https://mlsanity.com/paper/2004.13820/) (2020)
- [nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models](https://mlsanity.com/paper/2303.04864/) (2023)
- [Integration of Formal Proof into Unified Assurance Cases with Isabelle/SACM](https://mlsanity.com/paper/2009.12154/) (2020)
- [Enhancing Covid-19 Decision-Making by Creating an Assurance Case for Simulation Models](https://mlsanity.com/paper/2005.08381/) (2020)

## Built on by (most cited first, 3 of 3)

- [Fine-Tuning Language Models Using Formal Methods Feedback](https://mlsanity.com/paper/2310.18239/) (2023)
- [An Agentic RAG and Evaluation Framework for Assurance Case Generation: Industrial Use Case for the EU Cyber Resilience Act Compliance](https://mlsanity.com/paper/2608.19509/) (2026)
- [Context operations to architecture modelling output from large language models and evaluation criteria for their use in systems engineering design](https://mlsanity.com/paper/2609.10132/) (2026)

## Abstract (arXiv)

Assurance cases can be used to argue for the safety of products in safety engineering. In safety-critical areas, the construction of assurance cases is indispensable. Trustworthiness Derivation Trees (TDTs) enhance assurance cases by incorporating formal methods, rendering it possible for automatic reasoning about assurance cases. We present Trustworthiness Derivation Tree Analyzer (Trusta), a desktop application designed to automatically construct and verify TDTs. The tool has a built-in Prolog interpreter in its backend, and is supported by the constraint solvers Z3 and MONA. Therefore, it can solve constraints about logical formulas involving arithmetic, sets, Horn clauses etc. Trusta also utilizes large language models to make the creation and evaluation of assurance cases more convenient. It allows for interactive human examination and modification. We evaluated top language models like ChatGPT-3.5, ChatGPT-4, and PaLM 2 for generating assurance cases. Our tests showed a 50%-80% similarity between machine-generated and human-created cases. In addition, Trusta can extract formal constraints from text in natural languages, facilitating an easier interpretation and validation process. This extraction is subject to human review and correction, blending the best of automated efficiency with human insight. To our knowledge, this marks the first integration of large language models in automatic creating and reasoning about assurance cases, bringing a novel approach to a traditional challenge. Through several industrial case studies, Trusta has proven to quickly find some subtle issues that are typically missed in manual inspection, demonstrating its practical value in enhancing the assurance case development process.