Certus

A Domain Specific Language for Confidence Assessment in Assurance Cases

Certus is a DSL for modelling and evaluating confidence in assurance cases — structured arguments used in safety, security, and dependability engineering (e.g., GSN, CAE, or Eliminative Argumentation). Rather than requiring precise numerical inputs, Certus lets practitioners express confidence using natural, linguistically meaningful terms such as “high” or “very high”, grounded in fuzzy set theory.

Certus is introduced in the following paper, freely accessible on arXiv:

S. Diemert and J. H. Weber, “Certus: A Domain Specific Language for Confidence Assessment in Assurance Cases,” SAFECOMP 2025 Workshops. arXiv:2505.01894

---

Canonical Confidence Levels

Certus provides nine built-in confidence levels, ordered from lowest to highest belief. Each maps to a fuzzy set defined over the belief domain [−1, 1], where −1 represents complete disbelief, 0 represents uncertainty, and +1 represents complete belief.

Keyword	Meaning	Fuzzy Set (approx.)
reject	Complete rejection	point mass at −1
vopp	Very opposed	peaked around −0.75
opp	Opposed	trap(−0.9, −0.8, −0.5, −0.4)
skep	Skeptical	trap(−0.6, −0.5, −0.2, −0.1)
uncert	Uncertain (neutral)	trap(−0.3, −0.2, 0.2, 0.3)
low	Low confidence	trap(0.1, 0.2, 0.5, 0.6)
high	High confidence	trap(0.4, 0.5, 0.8, 0.9)
vhigh	Very high confidence	peaked around 0.75
certain	Complete certainty	point mass at +1

Comparisons between canonical sets (e.g., >=, >) follow this ordering.

---

Language Reference

Direct Assignment

The simplest Certus expression directly assigns a confidence level to a node:

G1 is high;

You can also propagate confidence from a child node:

G0 is G1;

---

Cases Expression

The cases expression provides conditional confidence propagation. Each branch specifies a condition over child node valuations and the resulting confidence if that condition holds. Branches are evaluated top-to-bottom; the first matching branch wins. An otherwise clause provides the default.

G0 is cases
    G1 >= high  && G2 >= high  -> vhigh,
    G1 >= low   && G2 >= low   -> low,
    otherwise uncert

Conditions support && (and), || (or), and NOT, with parentheses for grouping:

G0 is cases
    NOT (G1 >= low)              -> reject,
    G1 >= vhigh || G2 >= vhigh   -> certain,
    G1 >= high  && G2 >= high    -> vhigh,
    otherwise uncert

Comparisons can be made against canonical set names or against other child node identifiers:

G0 is cases
    G1 >= G2  -> high,
    otherwise low

---

Set Operations

Two confidence sets can be combined using intersection (intersect) and union (union):

G0 is G1 intersect G2;   -- more conservative valuation
G0 is G1 union G2;       -- more liberal valuation

Operations can be composed and parenthesised:

G0 is (G1 union G2) intersect G3;

---

Aggregate Macros

Certus provides built-in macros for common aggregation patterns over multiple child nodes:

G0 is min(G1, G2, G3);   -- weakest-link: lowest confidence
G0 is max(G1, G2, G3);   -- best-case: highest confidence
G0 is fuse(G1, G2);      -- evidence fusion (Dempster-Shafer style)

Macro arguments can be canonical set names or arbitrarily nested set expressions:

G0 is min(G1 union G2, G3);   -- G1∨G2 vs G3, take the lower
G0 is max(vhigh, high);        -- evaluates to vhigh

Strict and eliminative variants of min, max, and fuse are also available (e.g., minStrict, maxEliminative, fuseStrict).

---

Custom Fuzzy Sets

You can define custom confidence levels using trapezoidal fuzzy sets with the with ... as ... end syntax. Parameters define the trapezoid trap(left_foot, left_shoulder, right_shoulder, right_foot) over [−1, 1]:

with myConf as trap(0.3, 0.5, 0.7, 0.9) end

G0 is cases
    G1 >= myConf -> certain,
    otherwise low

Custom sets can be used anywhere a canonical set name is expected.

---

Indicators

Certus supports conditioning confidence on external indicators — runtime values or categories passed into the evaluation context. Indicator names are prefixed with $.

Indicators can be numeric values with numeric comparisons:

G0 is cases
    $score >= 0.8  -> vhigh,
    $score >= 0.5  -> high,
    otherwise low

Or they can be categorical (testing membership in a named category):

G0 is cases
    $indicator is DANGER -> opp,
    G1 >= high           -> vhigh,
    otherwise uncert

You can also test whether an artifact indicator is present using has @name:

G0 is cases
    has @report  -> high,
    otherwise low

---

TypeScript API

A TypeScript implementation of the Certus evaluator is available as the certus-ts npm package.

Installation

npm install certus-ts

Quick Start

import { CertusEvaluator, CertusContext, NodeType } from 'certus-ts';

const ctx = new CertusContext();
const evaluator = new CertusEvaluator();

// Define the argument structure and child valuations
ctx.setRoot("G0");
ctx.addChild("G1", NodeType.CLAIM, ctx.getNamedSet("high"));
ctx.addChild("G2", NodeType.CLAIM, ctx.getNamedSet("vhigh"));

// Evaluate a confidence expression
const expr = `G0 is cases
    G1 >= high && G2 >= vhigh -> certain,
    G1 >= low  && G2 >= low   -> low,
    otherwise uncert`;

evaluator.evaluate(expr, ctx);

console.log(ctx.getSyntaxErrors());      // []
console.log(ctx.getEvaluationErrors()); // []
console.log(ctx.getRoot().valuation.name); // "certain"

Set Operations in Code

// Intersect and union of named sets
evaluator.evaluate("G0 is G1 intersect G2;", ctx);

// Aggregate macros
evaluator.evaluate("G0 is min(G1, G2, G3);", ctx);
evaluator.evaluate("G0 is max(G1, G2, G3);", ctx);

// Custom fuzzy sets
evaluator.evaluate("G0 is trap(0.3, 0.5, 0.7, 0.9);", ctx);

---

Formal Semantics

Formal semantics for Certus are specified in the Lean4 theorem prover. The Lean4 source is available in the semantics/ directory of this repository.

---

Implementations in Tools

Tools that have incorporated Certus include:

• Socrates — Assurance Case Editor

---

Citations

If you use Certus in academic or industrial work, please cite:

S. Diemert and J. H. Weber, “Certus: A Domain Specific Language for Confidence Assessment in Assurance Cases,” in Computer Safety, Reliability, and Security. SAFECOMP 2025 Workshops, Cham: Springer Nature Switzerland, 2025, pp. 211–225. doi: 10.1007/978-3-032-02018-5_16.

Related works:

S. Diemert, C. Shortt, and J. H. Weber, “How do practitioners gain confidence in assurance cases?” Information and Software Technology, vol. 185, p. 107767, Sept. 2025. doi: 10.1016/j.infsof.2025.107767.

B. Herd, J. Kelly, J.-V. Zacchi, C. Heinzemann, and S. Diemert, “Integrating Defeaters into Subjective Logic-based Quantitative Assurance Arguments,” presented at EDCC, Lisbon, Portugal, 2025.

S. Diemert, L. Millet, J. Joyce, and J. H. Weber, “Including Defeaters in Quantitative Confidence Assessments for Assurance Cases,” in Computer Safety, Reliability, and Security. SAFECOMP 2024 Workshops, Cham: Springer Nature Switzerland, 2024, pp. 239–250. doi: 10.1007/978-3-031-68738-9_18.

---

Credits

Certus was developed by Simon Diemert at the University of Victoria (Canada) as part of his PhD research, under the supervision of Dr. Jens H. Weber. Development was supported by the Natural Sciences and Engineering Research Council of Canada (NSERC).

Certus is open source, available under the MIT License.