Djinious
A constrained Lean 4 safety DSL
Author safety functions as state machines, guarded transitions, boolean and fixed-point dataflow — and prove safety properties (invariants, safe-state reachability) with the Lean kernel.
Lean 4
DjiniousSafeCertifiable codeWhat is provedis what ships.
The proven-code toolchain · IEC 61508 · SIL 4Prove
DjiniousSafe is a toolchain for building safety functions to IEC 61508 SIL 4: specify them formally in Lean 4, prove their safety properties with the Lean kernel, and generate no_std, panic-free Rust — with a per-build, machine-checked certificate that the shipped code equals the spec, and complete traceability from requirements to theorems.
DjiniousSafe
- fail-closed gates per build
- 13fail-closed gates per buildthe first failure aborts the build
- diverse generators
- 2diverse generatorsone in Rust, one in Lean — outputs byte-identical
- kernel-checked theorems per function
- 5kernel-checked theorems per functionre-proved from the emitted code on every build
- reference safety functions
- 9reference safety functionscertified end to end in examples/voter
What it is
Generate embedded Rust that provably implements its formal spec
A Lean-to-Rust safety code generation pipeline. It validates requirements, exports Lean-checked IR, generates restricted Rust, performs equivalence and back-to-back gates, and writes an audit evidence bundle for accepted builds. Failed builds are fail-closed.
Dual-channel diverse generation
Two independently designed generators, one in Rust, one in Lean, from the same specification. Their outputs must be structurally identical — any divergence fails the build.
sgen-a · sgen-bTranslation validation
Every build re-parses the emitted Rust text and the Lean kernel checks a fresh certificate that it is semantically equal to the spec. What is proved is what ships.
Kernel certificateRestricted-Rust output
Zero heap, panic-free, no unsafe, constant-bounded loops, saturating arithmetic — ready for the Ferrocene qualified compiler.
#![no_std]Bidirectional, machine-checked traceability
Requirement → Lean theorem → Rust symbol → test vector. Hash-pinned requirement text turns change impact into a build error.
Trace matrixQ-format fixed-point arithmetic
Explicit widths, scaling and saturation — plus kernel-checked overflow-freedom and exactness obligations on every constant.
Q-formatInside the product
See it working.
Every capture below is the running product.
01 · Fail-closed everywhere
Thirteen gates, and the first failure stops the build
A build runs its gates in a fixed order and every gate appends a row to the evidence. Proofs, generator equivalence, certificate, trace matrix and back-to-back tests are all hard gates: the first failure aborts the build, with the error recorded as the failed row’s detail — and no later gate runs.
- requirements · lean-proofs · export-fresh · ir-load · trace
- generate · equiv · reprint · certificate
- b2b-host · no_std-check · b2b-target · evidence-finalize
- b2b-target runs only when a [target] is configured — otherwise it is absent from the evidence, not marked skipped
02 · Generators are never trusted
The same program, written twice, by two toolchains
The Rust text is produced twice, independently: sgen-a lowers the exported IR in Rust; sgen-b prints directly from the elaborated safety function in Lean. The equiv gate requires AST identity, the reprint gate byte-identity — a defect must occur identically in both toolchains to pass.
- Every cross-language hash is computed twice — by a Lean SHA-256 implementation and by the Rust sha2 crate — and both are recorded
- The shipped artifact must be byte-canonical: print(parse(bytes)) == bytes
- Certificates are built from the emitted code itself, never from generator state
03 · Reference safety functions
From YAML requirement to certified no_std Rust
The voter example carries nine reference safety functions from requirement to certified code: a 2oo3 voter, a latching trip, a rate limiter, a threshold monitor with hysteresis, a gain block, a statistics block, a dot-ratio block, a pressure interlock and a flow gauge with an IEEE-754 f32 boundary — each shipped with a kernel-checked equivalence certificate.
- Every generated file carries its // TRACE: requirement line
- Per function, the certificate proves well-formedness, exact structural equality and step-for-step simulation of the spec
- div, rem, sqrt and wide i64 arithmetic certified panic-free
DjiniousSafe
04 · On-target replay
Back-to-back on the host, and on an emulated Cortex-M4F
Lean-side reference vectors — boundary cross-products, 8 × 32-step LCG sequences and, for float-boundary functions, f32 probes including NaN, ±inf, ±0 and rounding ties — are replayed against the compiled code on the host. When a target is configured, the same vectors replay under QEMU on thumbv7em-none-eabihf, with the SHA-256 of each replayed ELF pinned in the evidence.
- A fixed vector seed, so every count is deterministic
- Count-equality between host and target: no partial credit, no missing function
- Building twice with unchanged sources and environment gave zero differences in evidence.json, ELF hashes included
AI & agents
Agents call the same pipeline you do
djsafe serve wraps the existing pipeline without duplicating build behaviour: local CLI commands remain the source of truth, and the service exposes those same operations over an agent-ready Provider API and an MCP endpoint.
Provider API
Capabilities, identity and an OpenAPI document, with build and clean as idempotent operations.
MCP endpoint
The same operations as MCP tools, so an agent can discover and invoke them.
Rules for agents
Discover capabilities before invoking operations, keep tokens out of logs and summaries, report failing gates verbatim enough to diagnose the build, and ask before deploying.
Capabilities
The toolchain, crate by crate
One CLI, djsafe, orchestrates a workspace of small, single-purpose crates and a Lean package.
Specification and proof3 capabilities
leansafe
Lean safety semantics, specs and export code: the DSL, interval overflow-freedom, the machine-accuracy bridge, the Lean-side generator and the back-to-back vector export.
req-model
Requirements model parsing and hashing — per-requirement SHA-256 over whitespace-normalised text.
safe-ir
The typed safety IR exported from Lean and hash-pinned on both sides.
Generation and gates5 capabilities
sgen-a
Rust generator A, lowering the exported IR.
rrust-syntax
The restricted-Rust parser and printer behind the byte-canonicality law.
equiv-gate
The generator equivalence gate: AST identity or the build fails.
cert-gen
Certificate generation: a Lean term rebuilt from the parsed artifact, checked by the kernel.
trace
Trace matrix generation in JSON, CSV and HTML, rejecting orphan requirements, unknown references and untraced functions by name.
Operation2 capabilities
djsafe
CLI, pipeline orchestration, HTTP service and remote client commands — build and clean locally or on the deployed service.
djinious-safe-service skill
An AI-agent skill for operating the deployed service.
Trust
A bounded trust base — and honest limits
No single component is trusted for a claim that is not cross-checked through a structurally different path. Every load-bearing claim can be re-derived by an assessor without trusting the pipeline’s own report.
The Lean kernel is the root of trust
Every semantic claim reduces to kernel-checked proofs. An axiom audit shows the certificates depend only on Lean’s standard axioms — no sorry, no native_decide, no custom axioms.
Lean 4.15.0Independent verification playbook
Re-pin a spec with your own third hash, re-run a certificate through the kernel, re-run the whole build and diff the evidence, replay an on-target binary by hand, and round-trip a shipped artifact through the parser and printer.
Ready for a qualified compiler
The generated-code builds can be pointed at Ferrocene through the [toolchain] configuration; the compiler’s identity is recorded in every evidence bundle. Identity is not qualification, and the evidence says so.
FerroceneWhat is not claimed
Requirements validity remains a human review. No claim concerns timing, WCET, stack bounds or memory footprint. QEMU validates cross-compiled machine code and target libcore, not physical silicon.
In the digital thread
What it takes in. What it hands on.
DjiniousSafe does its part of the engineering loop and passes its evidence along — and it works just as well on its own.
DjiniousSafeCertifiable codeOn its own
On its own, DjiniousSafe is a command-line toolchain: point djsafe at a project of requirements and Lean specifications, and it returns certified embedded Rust with its evidence — or the gate that refused it.
Use cases
DjiniousSafe in use.
2 worked cases.
Safety-critical embedded controlNine safety functions, from YAML requirement to certified embedded RustThe 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.DjiniousSafe
Embedded code generationModel → Rust firmwareModel-based design to deployable code, the Rust-first way — an autopilot designed as block diagrams, code-generated to #![no_std] Rust, proven equivalent to the model, cross-compiled to a Cortex-M target, and attested for provenance.
DjiniousLabDjiniousSafeBook a demo
See it on your problem.
See a safety function go from requirement to certified embedded Rust — and watch the build refuse when it should.
- Writing a safety function and its properties in the Lean 4 safety DSL
- A full djsafe build through all thirteen gates, to BUILD ACCEPTED
- Tampering with a generated artifact and watching the certificate gate reject it
- Reading the evidence bundle: trace matrix, certificates, back-to-back and on-target replay
- Toolchain choices, the trust base, and what the evidence does not claim
Along the thread
Works well with
DjiniousEngineeringOrchestrationThe AI systems engineer: it takes the assignment and carries the whole project through a traceable System Ledger.
DjiniousWorkshopSystem integrationComponents wired into a complete system and closed through GPU physics in NVIDIA Isaac Sim.
DjiniousLabModelling & simulationMulti-domain system models, digital replicas and a mathematical toolbox, driven by AI.
DjiniousWorkflowAgent automationGraph automation any stage can call on: build a process, run it, watch it and audit it.