[pjmlp]

Rust safety with runtime dependencies, Vec bounds checking, Arc and Rc datatypes.

Ada with SPARK 2014 formal proofs, for your other part of the remark.