That's basically SPARK (the Ada subset) but with c-like syntax (more or less).

I see minor differences; however, the author does nothing to highlight them. That's the number one thing that any new language should show when it's trying to fit into a niche that a language already exists for: What makes this language different?