Safety-critical embedded controlEngineering methods

Nine safety functions, from YAML requirement to certified embedded Rust

The voter reference project takes nine safety functions — voting, latching, slew limiting, trip monitoring, interlocks and a flow gauge with a floating-point boundary — through all thirteen gates, and replays every one on an emulated Cortex-M4F.

DjiniousSafeCertifiable code

Generated Rust for the 2oo3 voter step, traced to REQ-SF-001, beside the Lean certificate for the rate limiter with its wfAll, structEqExact and step-equivalence theorems.

safety functions: 9safety functionsREQ-SF-001 to REQ-SF-016
gates passed: 13gates passedBUILD ACCEPTED
on-target cases for flow_gauge: 406on-target cases for flow_gauge0 failed · 78 float cases
differences between two builds: 0differences between two buildsevidence.json, ELF hashes included

The project

examples/voter is a complete djsafe project: a requirements file, the Lean specifications it points at, and a target section naming thumbv7em-none-eabihf on the netduinoplus2 QEMU machine. It is the project an external assessor is handed together with one evidence bundle.

Each requirement says, in plain text, what the function shall do — “The voter output shall be true if and only if at least two of the three input channels are true” — and its whitespace-normalised text is hash-pinned in the evidence, so a change of wording is a change the build can see.

What the nine functions cover

Safety logic

2oo3 voting logic and a latching trip that stays true once triggered.

REQ-SF-001 · 002

Fixed-point control

A slew limiter clamped to ±100 per step within [−1000, 1000], a two-state trip monitor with hysteresis, and a Q4 gain block.

REQ-SF-010 · 011 · 012

Division, roots and wide arithmetic

Averages, ratios, square roots, vector magnitudes and modulo counters, including wide i64 arithmetic — certified panic-free.

REQ-SF-013 · 014

Mixed inputs

A pressure interlock that trips on enable at ≥ 3000 and clears on reset below 2500, with latched worst-case pressure and a safety margin.

REQ-SF-015

A floating-point boundary

A flow gauge whose sensor value enters as an IEEE-754 f32 through a certified integer-only conversion to Q4, and whose margin leaves as an exactly converted f32 — fixed-point core unchanged.

REQ-SF-016

One build, gate by gate

Requirements and proofs
The requirements parse with unique IDs; the whole Lean package — specs, semantics library, every theorem — elaborates and kernel-checks.
Fresh export
Every Lean-derived artifact is regenerated from the just-checked modules, and a function that is not well-formed is refused at export.
Hash-pinned hand-offs
The IR, the spec sources and the semantics library are hashed by Lean and by Rust, and the two must agree.
Traceability
Every requirement is satisfied by some function, and every function cites only known requirements.
Two generators, one program
“9 functions AST-identical across sgen-a and sgen-b”, then byte-canonical across both.
Certificates
Per function, five theorems about the artifact as parsed back from the shipped bytes, checked by the Lean kernel.
Replay
Lean reference vectors against the compiled code on the host, then per function on the emulated target, each ELF hashed.
Evidence
Certificates, trace matrix, back-to-back manifest and on-target transcript assembled into one bundle.

Checked by someone other than the pipeline

The evidence guide gives an assessor five procedures that do not depend on the pipeline’s own report, each executed as written. For flow_gauge: a third SHA-256 of the spec source matches both recorded hashes and the certificate header; the certificate re-runs through the kernel with exit 0 and depends only on propext and Quot.sound; and the hand-replayed ELF prints “B2BT flow_gauge cases=406 failed=0 float_cases=78” with a hash equal to the one in the evidence.

The guide is as explicit about limits: requirements validity stays a human review, no claim concerns timing or stack bounds, and QEMU is not silicon.