La piattaforma
Ogni applicazione svolge una parte del lavoro — e passa le sue evidenze alla successiva. Usale insieme, o una alla volta.
Panoramica della piattaformaScopri come funziona il cicloOrchestrazione
DjiniousEngineeringOrchestrazioneProgettazione e dimostrazione
DjiniousLabModellazione e simulazione
DjiniousWorkshopIntegrazione di sistema
DjiniousSafeCodice certificabileOperatività
DjiniousCCOperatività e SCADADjiniousEngineeringOrchestrazioneDjiniousLabModellazione e simulazioneDjiniousWorkshopIntegrazione di sistemaDjiniousSafeCodice certificabile
DjiniousWorldRepliche 3D
DjiniousMapGIS ad agentiDjiniousCCOperatività e SCADA
DjiniousDataBase di conoscenza
DjiniousWorkflowAutomazione ad agenti
DjiniousSafeCodice certificabileDjiniousSafe è una toolchain per costruire funzioni di sicurezza a norma IEC 61508 SIL 4: specificale formalmente in Lean 4, dimostra le loro proprietà di sicurezza con il kernel Lean e genera Rust no_std, privo di panic — con un certificato verificato dalla macchina per ogni build che il codice spedito equivale alla specifica, e tracciabilità completa dai requisiti ai teoremi.
DjiniousSafe
Cos’è
Una pipeline di generazione di codice di sicurezza da Lean a Rust. Valida i requisiti, esporta IR verificato da Lean, genera Rust ristretto, esegue gate di equivalenza e back-to-back, e scrive un bundle di evidenze di audit per le build accettate. Le build fallite sono fail-closed.
Scrivi funzioni di sicurezza come macchine a stati, transizioni con guardia, dataflow booleano e a virgola fissa — e dimostra proprietà di sicurezza (invarianti, raggiungibilità dello stato sicuro) con il kernel Lean.
Lean 4Due generatori progettati in modo indipendente, uno in Rust, uno in Lean, dalla stessa specifica. I loro output devono essere strutturalmente identici — qualsiasi divergenza fa fallire la build.
sgen-a · sgen-bOgni build ri-analizza il testo Rust emesso e il kernel Lean verifica un nuovo certificato che sia semanticamente uguale alla specifica. Ciò che è dimostrato è ciò che spedisci.
Certificato del kernelZero heap, privo di panic, nessun unsafe, loop con limiti costanti, aritmetica satura — pronto per il compilatore qualificato Ferrocene.
#![no_std]Requisito → teorema Lean → simbolo Rust → vettore di test. Il testo del requisito fissato con hash trasforma l'impatto di una modifica in un errore di build.
Matrice di tracciabilitàLarghezze, scalatura e saturazione esplicite — più assenza di overflow verificata dal kernel e obblighi di esattezza su ogni costante.
Q-formatDentro al prodotto
Ogni schermata qui sotto è il prodotto in esecuzione.
01 · Fail-closed ovunque
Una build esegue i propri gate in un ordine fisso e ogni gate aggiunge una riga alle evidenze. Dimostrazioni, equivalenza dei generatori, certificato, matrice di tracciabilità e test back-to-back sono tutti gate rigidi: il primo fallimento interrompe la build, con l'errore registrato come dettaglio della riga fallita — e nessun gate successivo viene eseguito.
02 · I generatori non sono mai considerati affidabili
Il testo Rust viene prodotto due volte, in modo indipendente: sgen-a abbassa l'IR esportato in Rust; sgen-b stampa direttamente dalla funzione di sicurezza elaborata in Lean. Il gate equiv richiede identità dell'AST, il gate reprint identità byte per byte — un difetto deve verificarsi in modo identico in entrambe le toolchain per passare.
03 · Funzioni di sicurezza di riferimento
L'esempio voter porta nove funzioni di sicurezza di riferimento dal requisito al codice certificato: un voter 2oo3, uno scatto con latching, un limitatore di rate, un monitor di soglia con isteresi, un blocco di guadagno, un blocco statistico, un blocco di rapporto punto per punto, un interblocco di pressione e un misuratore di portata con limite IEEE-754 f32 — ciascuno spedito con un certificato di equivalenza verificato dal kernel.
DjiniousSafe
04 · Riproduzione on-target
I vettori di riferimento lato Lean — prodotti incrociati ai limiti, sequenze LCG a 8 × 32 passi e, per le funzioni con limiti in virgola mobile, sonde f32 incluse NaN, ±inf, ±0 e pareggi di arrotondamento — vengono riprodotti contro il codice compilato sull'host. Quando è configurato un target, gli stessi vettori vengono riprodotti sotto QEMU su thumbv7em-none-eabihf, con lo SHA-256 di ogni ELF riprodotto fissato nelle evidenze.
IA e agenti
djsafe serve incapsula la pipeline esistente senza duplicare il comportamento della build: i comandi CLI locali restano la fonte di verità, e il servizio espone le stesse operazioni tramite una Provider API pronta per gli agenti e un endpoint MCP.
Capacità, identità e un documento OpenAPI, con build e clean come operazioni idempotenti.
Le stesse operazioni come strumenti MCP, così un agente può scoprirle e invocarle.
Scopri le capacità prima di invocare le operazioni, tieni i token fuori dai log e dai riassunti, riporta i gate falliti in modo abbastanza letterale da diagnosticare la build, e chiedi conferma prima di distribuire.
Funzionalità
Una sola CLI, djsafe, orchestra un workspace di crate piccoli e monofunzione e un pacchetto Lean.
Semantica di sicurezza, specifiche e codice di esportazione in Lean: il DSL, l'assenza di overflow sugli intervalli, il ponte di accuratezza macchina, il generatore lato Lean e l'esportazione dei vettori back-to-back.
Analisi e hashing del modello dei requisiti — SHA-256 per requisito su testo normalizzato negli spazi bianchi.
L'IR di sicurezza tipizzato esportato da Lean e fissato con hash su entrambi i lati.
Generatore Rust A, che abbassa l'IR esportato.
Il parser e il printer del Rust ristretto dietro la legge di canonicità byte.
Il gate di equivalenza dei generatori: identità dell'AST o la build fallisce.
Generazione del certificato: un termine Lean ricostruito dall'artefatto analizzato, verificato dal kernel.
Generazione della matrice di tracciabilità in JSON, CSV e HTML, con rifiuto di requisiti orfani, riferimenti sconosciuti e funzioni non tracciate per nome.
CLI, orchestrazione della pipeline, servizio HTTP e comandi client remoto — build e clean in locale o sul servizio distribuito.
Una skill per agenti IA per operare il servizio distribuito.
Fiducia
Nessun singolo componente è considerato affidabile per un'affermazione che non sia verificata incrociando un percorso strutturalmente diverso. Ogni affermazione portante può essere riderivata da un valutatore senza fidarsi del rapporto della pipeline stessa.
Ogni affermazione semantica si riduce a dimostrazioni verificate dal kernel. Un audit degli assiomi mostra che i certificati dipendono solo dagli assiomi standard di Lean — nessun sorry, nessun native_decide, nessun assioma personalizzato.
Lean 4.15.0Rifissa una specifica con un tuo terzo hash indipendente, riesegui un certificato attraverso il kernel, riesegui l'intera build e confronta le evidenze, riproduci a mano un binario on-target, e fai transitare un artefatto spedito andata e ritorno attraverso il parser e il printer.
Le build del codice generato possono essere puntate a Ferrocene tramite la configurazione [toolchain]; l'identità del compilatore viene registrata in ogni bundle di evidenze. L'identità non è qualificazione, e le evidenze lo dichiarano.
FerroceneLa validità dei requisiti resta una revisione umana. Nessuna affermazione riguarda tempistiche, WCET, limiti dello stack o ingombro di memoria. QEMU valida il codice macchina cross-compilato e la libcore del target, non il silicio fisico.
Nel filo digitale
DjiniousSafe svolge la propria parte del ciclo di ingegneria e trasmette le proprie evidenze — e funziona altrettanto bene anche da sola.
DjiniousSafeCodice certificabileConsegna
DjiniousEngineeringUn bundle di evidenze per ogni build — certificati, matrice di tracciabilità, log delle dimostrazioni e risultati back-to-back — per il safety case del progetto.DjiniousWorkshopModuli Rust no_std certificati e il loro runner per il target, pronti per essere integrati sui banchi di prova.Da sola, DjiniousSafe è una toolchain a riga di comando: punta djsafe su un progetto di requisiti e specifiche Lean, e restituisce Rust embedded certificato con le sue evidenze — oppure il gate che lo ha rifiutato.
Casi d’uso
2 casi documentati.
Controllo embedded safety-criticalNove funzioni di sicurezza, dal requisito YAML al Rust embedded certificatoIl progetto di riferimento del voter porta nove funzioni di sicurezza — voto, latching, limitazione di slew rate, monitoraggio del trip, interblocchi e un misuratore di flusso con un confine in virgola mobile — attraverso tutti e tredici i gate, e riproduce ognuna su un Cortex-M4F emulato.DjiniousSafe
Generazione di codice embeddedModello → firmware RustDal design basato su modello al codice distribuibile, alla maniera Rust-first — un autopilota progettato come schemi a blocchi, generato in codice Rust #![no_std], dimostrato equivalente al modello, cross-compilato per un target Cortex-M, e attestato per la provenienza.
DjiniousLabDjiniousSafePrenota una demo
Guarda una funzione di sicurezza andare dal requisito al Rust embedded certificato — e osserva la build rifiutare quando deve.
Lungo il filo
DjiniousEngineeringOrchestrazioneL’ingegnere di sistema IA: prende in carico l’incarico e porta l’intero progetto attraverso un System Ledger tracciabile.
DjiniousWorkshopIntegrazione di sistemaComponenti collegati in un sistema completo e chiusi in anello tramite la fisica GPU in NVIDIA Isaac Sim.
DjiniousLabModellazione e simulazioneModelli di sistema multi-dominio, repliche digitali e una cassetta degli attrezzi matematica, guidati dall’IA.
DjiniousWorkflowAutomazione ad agentiAutomazione a grafo a cui ogni fase può ricorrere: costruisci un processo, eseguilo, osservalo e sottoponilo ad audit.
Djinious
