Hacker News Reader

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?

There is a D subset:

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