[berkeleynerd]

Is there an effort to provide formal verification features for a safe subset of the D language similar to ADA’s SPARK and related tooling?

[DoingIsLearning]

There is a D subset:

https://dlang.org/articles/safed.html

But nothing like Ada SPARK provability stuff, I don't think.