You may be using an older version of scribble. Earlier scribble allowed annotations without a leading # - e.g. invariant x > 0; instead of #invariant x > 0. However we found that since some of the keywords we use (e.g. invariant and define ) can occur in normal docstrings, sometimes scribble can get confused and try and treat something that is not an annotation as an annotation. To solve this problem we made the # required. So try to upgrade scribble to the latest version, and make sure all your annotations start with #.