> Ferrous Systems and AdaCore are.. joining forces to develop Ferrocene - a safety-qualified Rust toolchain, which is aimed at supporting the needs of various regulated markets, such as automotive, avionics, space, and railway.. qualifying the Ferrocene Rust compiler according to various safety standards.. [including] development and qualification of the necessary dynamic and static analysis tools.. our long-term commitment to Rust and Ada extends to developers who will be using both languages at the same time. We are looking at interoperability between them - including, in particular, the idea of developing bi-directional binding generators.
Nvidia uses Ada/SPARK for formally-verified security firmware on RISC-V cores on GPUs [1] and SPDM attestation of devices like GPUs and Infiniband NICs [2].
> Ferrous Systems and AdaCore are.. joining forces to develop Ferrocene - a safety-qualified Rust toolchain, which is aimed at supporting the needs of various regulated markets, such as automotive, avionics, space, and railway.. qualifying the Ferrocene Rust compiler according to various safety standards.. [including] development and qualification of the necessary dynamic and static analysis tools.. our long-term commitment to Rust and Ada extends to developers who will be using both languages at the same time. We are looking at interoperability between them - including, in particular, the idea of developing bi-directional binding generators.
Nvidia uses Ada/SPARK for formally-verified security firmware on RISC-V cores on GPUs [1] and SPDM attestation of devices like GPUs and Infiniband NICs [2].
[1] https://blog.adacore.com/when-formal-verification-with-spark... & https://static.sched.com/hosted_files/riscvsummit2024/fe/Key...
[2] https://www.adacore.com/papers/nvidia-using-recordflux-and-s... & https://docs.nvidia.com/networking/display/nvidiadeviceattes...