It's a directive that happens to be placed at the tail end of a comment. Reading the documentation the doc comment stops being a comment-proper with the first @-directive, after that it's a list of directives. SPARK started in comments, ACSL is placed in specially marked comments. SPARK 2014 moved into Ada proper using Ada 2012 features (aspects). The difference between SPARK 2014's annotation and this is basically, are the annotations above the function or after the function declaration?

It is different yes, having read a good amount of it by now I find it work's pretty well in practice. It means you can incrementally adopt them if you like and code with or without them looks quite similar assuming you documented your code, the function signatures look the same as well which I appreciate.