La plateforme
Chaque application prend en charge une partie du travail — et transmet ses preuves à la suivante. Utilisez-les ensemble, ou une à la fois.
Vue d’ensemble de la plateformeVoir comment la boucle fonctionneOrchestration
DjiniousEngineeringOrchestrationConception et preuve
DjiniousLabModélisation et simulation
DjiniousWorkshopIntégration système
DjiniousSafeCode certifiableExploitation
DjiniousCCExploitation et SCADADjiniousEngineeringOrchestrationDjiniousLabModélisation et simulationDjiniousWorkshopIntégration systèmeDjiniousSafeCode certifiable
DjiniousWorldRépliques 3D
DjiniousMapSIG agentiqueDjiniousCCExploitation et SCADA
DjiniousDataBase de connaissances
DjiniousWorkflowAutomatisation agentique
DjiniousSafeCode certifiableDjiniousSafe est une chaîne d’outils pour construire des fonctions de sécurité conformes à l’IEC 61508 SIL 4 : spécifiez-les formellement en Lean 4, prouvez leurs propriétés de sécurité avec le noyau Lean, et générez du Rust no_std, sans panic — avec, à chaque build, un certificat vérifié par machine attestant que le code livré équivaut à la spécification, et une traçabilité complète des exigences jusqu’aux théorèmes.
DjiniousSafe
Ce que c’est
Un pipeline de génération de code de sécurité de Lean vers Rust. Il valide les exigences, exporte l’IR vérifiée par Lean, génère du Rust restreint, effectue les jalons d’équivalence et de comparaison croisée (back-to-back), et écrit un dossier de preuves d’audit pour les builds acceptés. Les builds en échec sont à sécurité positive.
Écrivez des fonctions de sécurité sous forme de machines à états, de transitions gardées, de flux de données booléens et à virgule fixe — et prouvez des propriétés de sécurité (invariants, atteignabilité d’un état sûr) avec le noyau Lean.
Lean 4Deux générateurs conçus indépendamment, l’un en Rust, l’autre en Lean, à partir de la même spécification. Leurs sorties doivent être structurellement identiques — toute divergence fait échouer le build.
sgen-a · sgen-bChaque build reparcourt le texte Rust émis, et le noyau Lean vérifie un certificat neuf attestant qu’il est sémantiquement équivalent à la spécification. Ce qui est prouvé est ce qui part en production.
Certificat du noyauAucun tas, sans panic, sans unsafe, boucles bornées par des constantes, arithmétique saturante — prêt pour le compilateur qualifié Ferrocene.
#![no_std]Exigence → théorème Lean → symbole Rust → vecteur de test. Le texte de l’exigence figé par hachage transforme tout impact de changement en erreur de build.
Matrice de traçabilitéLargeurs, mise à l’échelle et saturation explicites — ainsi que l’absence de dépassement et les obligations d’exactitude sur chaque constante, vérifiées par le noyau.
Q-formatDans le produit
Chaque capture ci-dessous est le produit en fonctionnement.
01 · Sécurité positive partout
Un build exécute ses jalons dans un ordre fixe, et chaque jalon ajoute une ligne aux preuves. Les preuves, l’équivalence des générateurs, le certificat, la matrice de traçabilité et les tests de comparaison croisée sont tous des jalons stricts : le premier échec interrompt le build, l’erreur étant consignée comme détail de la ligne en échec — et aucun jalon suivant ne s’exécute.
02 · Les générateurs ne sont jamais crus sur parole
Le texte Rust est produit deux fois, indépendamment : sgen-a abaisse l’IR exportée en Rust ; sgen-b l’imprime directement depuis la fonction de sécurité élaborée en Lean. Le jalon d’équivalence exige une identité d’AST, le jalon de réimpression une identité au byte près — un défaut doit se produire de façon identique dans les deux chaînes d’outils pour passer.
03 · Fonctions de sécurité de référence
L’exemple voter porte neuf fonctions de sécurité de référence, de l’exigence jusqu’au code certifié : un voteur 2oo3, un déclenchement à verrouillage, un limiteur de débit, un moniteur de seuil à hystérésis, un bloc de gain, un bloc statistique, un bloc de rapport point à point, un interverrouillage de pression et une jauge de débit avec une limite f32 IEEE-754 — chacun livré avec un certificat d’équivalence vérifié par le noyau.
DjiniousSafe
04 · Relecture sur cible
Les vecteurs de référence côté Lean — produits croisés de bornes, séquences LCG de 8 × 32 pas et, pour les fonctions à bornes flottantes, des sondes f32 incluant NaN, ±inf, ±0 et les égalités d’arrondi — sont rejoués sur le code compilé, sur l’hôte. Quand une cible est configurée, les mêmes vecteurs sont rejoués sous QEMU sur thumbv7em-none-eabihf, avec le SHA-256 de chaque ELF rejoué figé dans les preuves.
IA et agents
djsafe serve encapsule le pipeline existant sans dupliquer le comportement de build : les commandes CLI locales restent la source de vérité, et le service expose ces mêmes opérations via une API fournisseur prête pour les agents et un point de terminaison MCP.
Capacités, identité et un document OpenAPI, avec build et clean comme opérations idempotentes.
Les mêmes opérations sous forme d’outils MCP, pour qu’un agent puisse les découvrir et les invoquer.
Découvrez les capacités avant d’invoquer des opérations, gardez les jetons hors des journaux et des résumés, rapportez les jalons en échec de façon assez littérale pour diagnostiquer le build, et demandez avant de déployer.
Capacités
Un seul CLI, djsafe, orchestre un espace de travail de petites crates à usage unique et un package Lean.
Sémantique de sécurité, spécifications et code d’export en Lean : le DSL, l’absence de dépassement par intervalles, le pont de précision machine, le générateur côté Lean et l’export des vecteurs de comparaison croisée.
Analyse et hachage du modèle d’exigences — SHA-256 par exigence sur un texte normalisé au niveau des espaces.
L’IR de sécurité typée exportée depuis Lean et figée par hachage des deux côtés.
Générateur Rust A, abaissant l’IR exportée.
L’analyseur et l’imprimeur de Rust restreint derrière la règle de canonicité au byte près.
Le jalon d’équivalence des générateurs : identité d’AST, sinon le build échoue.
Génération de certificat : un terme Lean reconstruit à partir de l’artefact analysé, vérifié par le noyau.
Génération de la matrice de traçabilité en JSON, CSV et HTML, rejetant nommément les exigences orphelines, les références inconnues et les fonctions non tracées.
CLI, orchestration du pipeline, service HTTP et commandes client distant — build et clean en local ou sur le service déployé.
Une compétence pour agent IA permettant d’exploiter le service déployé.
Confiance
Aucun composant seul n’est cru sur parole pour une affirmation qui n’est pas recoupée par un chemin structurellement différent. Toute affirmation porteuse peut être redérivée par un évaluateur sans se fier au rapport du pipeline lui-même.
Toute affirmation sémantique se ramène à des preuves vérifiées par le noyau. Un audit des axiomes montre que les certificats ne dépendent que des axiomes standard de Lean — pas de sorry, pas de native_decide, pas d’axiome personnalisé.
Lean 4.15.0Refigez une spécification avec votre propre tierce empreinte, repassez un certificat par le noyau, relancez tout le build et comparez les preuves, rejouez un binaire sur cible à la main, et faites transiter un artefact livré par l’analyseur puis l’imprimeur.
Les builds de code généré peuvent être dirigés vers Ferrocene via la configuration [toolchain] ; l’identité du compilateur est consignée dans chaque dossier de preuves. L’identité n’est pas une qualification, et les preuves le disent explicitement.
FerroceneLa validité des exigences reste une revue humaine. Aucune affirmation ne concerne le temps d’exécution, le WCET, les bornes de pile ou l’empreinte mémoire. QEMU valide le code machine compilé de façon croisée et la libcore cible, pas le silicium physique.
Dans le fil numérique
DjiniousSafe assure sa part de la boucle d’ingénierie et transmet ses preuves — et fonctionne tout aussi bien seule.
DjiniousSafeCode certifiableLivre
DjiniousEngineeringUn dossier de preuves par build — certificats, matrice de traçabilité, journaux de preuve et résultats de comparaison croisée — pour le dossier de sécurité du projet.DjiniousWorkshopDes modules Rust no_std certifiés et leur exécuteur cible, prêts à intégrer sur les bancs de test.À elle seule, DjiniousSafe est une chaîne d’outils en ligne de commande : pointez djsafe vers un projet d’exigences et de spécifications Lean, et il renvoie du Rust embarqué certifié avec ses preuves — ou le jalon qui l’a refusé.
Cas d’usage
2 cas documentés.
Commande embarquée critique pour la sécuritéNeuf fonctions de sécurité, de l’exigence YAML au Rust embarqué certifiéLe projet de référence du voteur fait passer neuf fonctions de sécurité — vote, verrouillage, limitation de pente, surveillance de déclenchement, verrouillages de sécurité et une jauge de débit avec une frontière en virgule flottante — à travers les treize jalons, et rejoue chacune sur un Cortex-M4F émulé.DjiniousSafe
Génération de code embarquéModèle → firmware RustDe la conception orientée modèle au code déployable, à la manière Rust d’abord — un pilote automatique conçu sous forme de schémas-blocs, généré en code Rust #![no_std], prouvé équivalent au modèle, compilé de manière croisée pour une cible Cortex-M, et attesté en provenance.
DjiniousLabDjiniousSafeRéserver une démo
Voyez une fonction de sécurité passer de l’exigence au Rust embarqué certifié — et regardez le build refuser quand il le doit.
Le long du fil numérique
DjiniousEngineeringOrchestrationL’ingénieur système IA : il prend la mission et porte tout le projet à travers un System Ledger traçable.
DjiniousWorkshopIntégration systèmeDes composants câblés en un système complet et bouclé grâce à la physique GPU dans NVIDIA Isaac Sim.
DjiniousLabModélisation et simulationDes modèles système multidomaines, des répliques numériques et une boîte à outils mathématique, pilotés par l’IA.
DjiniousWorkflowAutomatisation agentiqueUne automatisation en graphe que chaque étape peut solliciter : construisez un processus, exécutez-le, surveillez-le et auditez-le.
Djinious
