diff --git a/Source/DafnyCore/AST/Attributes.cs b/Source/DafnyCore/AST/Attributes.cs
index e3f44389b65..925f51258b5 100644
--- a/Source/DafnyCore/AST/Attributes.cs
+++ b/Source/DafnyCore/AST/Attributes.cs
@@ -15,6 +15,31 @@ public static bool IsExplicitAxiom(this IAttributeBearingDeclaration me) =>
     Attributes.Contains(me.Attributes, "axiom");
 }
 
+// Syntax of a formal of a built-in @-attribute
+// To create one, prefer using the chaining BuiltInAtAttributeSyntax.WithArg()
+public record BuiltInAtAttributeArgSyntax(
+  String ArgName,
+  Type ArgType, // If null, it means it's not resolved (@Induction and @Trigger)
+  Expression DefaultValue) {
+  public Formal ToFormal() {
+    Contract.Assert(ArgType != null);
+    return new Formal(Token.NoToken, ArgName, ArgType, true, false,
+      DefaultValue);
+  }
+}
+
+// Syntax for a built-in @-attribute.
+// To create such an attribute, use the Attributes.B() helper
+public record BuiltInAtAttributeSyntax(
+  string Name,
+  List<BuiltInAtAttributeArgSyntax> Args) {
+  public BuiltInAtAttributeSyntax WithArg(String argName, Type argType, Expression defaultValue = null) {
+    var c = new List<BuiltInAtAttributeArgSyntax>(Args) {
+      new(argName, argType, defaultValue) };
+    return this with { Args = c };
+  }
+}
+
 public class Attributes : TokenNode {
   [ContractInvariantMethod]
   void ObjectInvariant() {
@@ -37,6 +62,7 @@ void ObjectInvariant() {
   public Attributes(string name, [Captured] List<Expression> args, Attributes prev) {
     Contract.Requires(name != null);
     Contract.Requires(cce.NonNullElements(args));
+    Contract.Requires(name != UserSuppliedAtAttribute.AtName || this is UserSuppliedAtAttribute);
     Name = name;
     Args = args;
     Prev = prev;
@@ -207,6 +233,196 @@ public static bool ContainsMatchingValue(Attributes attrs, string nm, ref object
       : new List<Node> { Prev });
 
   public override IEnumerable<INode> PreResolveChildren => Children;
+
+
+  private static string TupleItem0Name => "0";
+  // Helper to create a built-in @-attribute
+  static BuiltInAtAttributeSyntax B(string name) {
+    return new BuiltInAtAttributeSyntax(
+      name, new List<BuiltInAtAttributeArgSyntax>());
+  }
+
+  // Helper to create an old-style attribute
+  private static Attributes A(string name, params Expression[] args) {
+    return new Attributes(name, args.ToList(), null);
+  }
+
+  // Helper to create an old-style attribute with only one argument
+  private static Attributes A1(string name, ActualBindings bindings) {
+    if (Get(bindings, 0, out var expr) && expr != null) {
+      return A(name, expr);
+    }
+
+    return A(name);
+  }
+
+  // Given a user-supplied @-attribute, expand it if recognized as builtin to an old-style attribute
+  // or mark i as not built-in for later resolution
+  public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttribute atAttribute) {
+    var toMatch = atAttribute.Arg;
+    var name = atAttribute.UserSuppliedName;
+    var bindings = atAttribute.UserSuppliedPreResolveBindings;
+
+    if (name == null) {
+      program.Reporter.Error(MessageSource.Resolver, atAttribute.RangeToken, "@-Attribute not recognized: " + atAttribute.ToString());
+      return null;
+    }
+
+    if (!TryGetBuiltinAtAttribute(name, out var builtinSyntax) || builtinSyntax == null) {
+      atAttribute.Builtin = false; // Will be resolved after
+      return null;
+    }
+
+    if (name != "Induction" && name != "Trigger") {
+      var formals = builtinSyntax.Args.Select(arg => arg.ToFormal()).ToArray();
+      ResolveLikeDatatypeConstructor(program, formals, name, toMatch.tok, bindings);
+    } // For @Induction and @Trigger, resolution is done in the generated version of the attributes
+
+    atAttribute.Builtin = true;
+    atAttribute.Arg.Type = Type.Int; // Dummy type to avoid crashes
+
+    switch (name) {
+      case "Compile": {
+          return A1("compile", bindings);
+        }
+      case "Fuel": {
+          if (Get(bindings, 0, out var lowFuel) && lowFuel != null) {
+            if (Get(bindings, 1, out var highFuel) && highFuel != null) {
+              if (Get(bindings, 2, out var functionName) && IsStringNotEmpty(functionName)) {
+                return A("fuel", functionName, lowFuel, highFuel);
+              }
+
+              return A("fuel", lowFuel, highFuel);
+            }
+
+            return A("fuel", lowFuel);
+          }
+
+          return A("fuel");
+        }
+      case "Induction": {
+          return A("induction", bindings.ArgumentBindings.Select(binding => binding.Actual).ToArray());
+        }
+      case "IsolateAssertions": {
+          return A("isolate_assertions");
+        }
+      case "Options": {
+          return A1("options", bindings);
+        }
+      default: {
+          throw new Exception("@-Attribute added to Attributes.BuiltinAtAttributes needs to be handled here");
+        }
+    }
+  }
+
+  // List of built-in @-attributes with their definitions.
+  // This list could be obtained from parsing and resolving a .Dfy file
+  // but for now it's good enough.
+  public static readonly List<BuiltInAtAttributeSyntax> BuiltinAtAttributes = new() {
+    B("Compile").WithArg(TupleItem0Name, Type.Bool, DefaultBool(true)),
+    B("Fuel")
+      .WithArg("low", Type.Int, DefaultInt(1))
+      .WithArg("high", Type.Int, DefaultInt(2))
+      .WithArg("functionName", Type.ResolvedString(), DefaultString("")),
+    B("Induction"), // Resolution is different
+    B("IsolateAssertions"),
+    B("Options").WithArg(TupleItem0Name, Type.ResolvedString()),
+  };
+
+  ////// Helpers to create default values for the @-attribute definitions above //////
+
+  public static LiteralExpr DefaultString(string value) {
+    return Expression.CreateStringLiteral(Token.NoToken, value);
+  }
+
+  public static LiteralExpr DefaultBool(bool value) {
+    return Expression.CreateBoolLiteral(Token.NoToken, value);
+  }
+
+  public static LiteralExpr DefaultInt(int value) {
+    return Expression.CreateIntLiteralNonnegative(Token.NoToken, value);
+  }
+
+  private static bool IsStringNotEmpty(Expression value) {
+    return value is StringLiteralExpr { Value: string and not "" };
+  }
+
+  // Given resolved bindings, gets the i-th argument according to the
+  // declaration formals order
+  private static bool Get(ActualBindings bindings, int i, out Expression expr) {
+    if (bindings.Arguments.Count < i + 1) {
+      expr = null;
+      return false;
+    }
+
+    expr = bindings.Arguments[i];
+    return true;
+  }
+
+  // Resolves bindings given a list of datatype constructor-like formals,
+  // obtained from built-in @-attribute definitions
+  private static void ResolveLikeDatatypeConstructor(
+    Program program, Formal[] formals, string attrName,
+    IToken attrsTok, ActualBindings bindings) {
+    var datatypeName = new Name(RangeToken.NoToken, attrName);
+    var datatypeCtor = new DatatypeCtor(RangeToken.NoToken, datatypeName, false, formals.ToList(), null);
+    var resolutionContext = new ResolutionContext(new NoContext(program.DefaultModuleDef), false); ;
+    var typeMap = new Dictionary<TypeParameter, Type>();
+    var resolver = new ModuleResolver(new ProgramResolver(program), program.Options);
+    resolver.reporter = program.Reporter;
+    resolver.moduleInfo = resolver.ProgramResolver.SystemModuleManager.systemNameInfo;
+    resolver.ResolveActualParameters(bindings, formals.ToList(), attrsTok,
+      datatypeCtor, resolutionContext, typeMap, null);
+    resolver.FillInDefaultValueExpressions();
+    resolver.SolveAllTypeConstraints();
+  }
+
+  // Recovers a built-in @-Attribute if it exists
+  public static bool TryGetBuiltinAtAttribute(string name, out BuiltInAtAttributeSyntax builtinAtAttribute) {
+    return BuiltInAtAttributeDictionary.TryGetValue(name, out builtinAtAttribute);
+  }
+
+  // Builtin @-attributes dictionary based on the sequence of definitions of @-attributes
+  public static Dictionary<string, BuiltInAtAttributeSyntax> BuiltInAtAttributeDictionary =
+    BuiltinAtAttributes.ToDictionary(b => {
+      if (b.Name.Contains("_") || b.Name.Contains("-") || Char.IsLower(b.Name[0])) {
+        throw new Exception("Builtin @-attributes are PascalCase for consistency");
+      }
+      return b.Name;
+    }, b => b);
+
+  // Overridable method to clone the attribute as if the new attribute was placed after "prev" in the source code
+  public virtual Attributes CloneAfter(Attributes prev) {
+    return new Attributes(Name, Args, prev);
+  }
+
+  //////// Helpers for parsing attributes //////////////////
+
+  // Returns the memory location's attributes content and set the memory location to null (no attributes)
+  public static Attributes Consume(ref Attributes tmpStack) {
+    var result = tmpStack;
+    tmpStack = null;
+    return result;
+  }
+
+  // Empties the first attribute memory location while prepending its attributes to the second attribute memory location, in the same order
+  public static void MergeInto(ref Attributes tmpStack, ref Attributes attributesStack) {
+    MergeIntoReadonly(tmpStack, ref attributesStack);
+    tmpStack = null;
+  }
+
+  // Prepends the attributes tmpStack before the attributes contained in the memory location attributesStack 
+  private static void MergeIntoReadonly(Attributes tmpStack, ref Attributes attributesStack) {
+    if (tmpStack == null) {
+      return;
+    }
+    if (attributesStack == null) {
+      attributesStack = tmpStack;
+      return;
+    }
+    MergeIntoReadonly(tmpStack.Prev, ref attributesStack);
+    attributesStack = tmpStack.CloneAfter(attributesStack);
+  }
 }
 
 public static class AttributesExtensions {
@@ -221,6 +437,7 @@ public static IEnumerable<Attributes> AsEnumerable(this Attributes attr) {
   }
 }
 
+// {:..} Attributes parsed are built using this class
 public class UserSuppliedAttributes : Attributes {
   public readonly IToken OpenBrace;
   public readonly IToken CloseBrace;
@@ -237,11 +454,80 @@ public UserSuppliedAttributes(IToken tok, IToken openBrace, IToken closeBrace, L
   }
 }
 
+// @-Attributes parsed are built using this class
+public class UserSuppliedAtAttribute : Attributes {
+  public static readonly string AtName = "@";
+  public readonly IToken AtSign;
+  public bool Builtin;  // set to true to indicate it was recognized as a builtin attribute
+  // Otherwise it's a user-defined one and Arg needs to be fully resolved
+  public UserSuppliedAtAttribute(IToken tok, Expression arg, Attributes prev)
+    : base(AtName, new List<Expression>() { arg }, prev) {
+    Contract.Requires(tok != null);
+    this.tok = tok;
+    this.AtSign = tok;
+  }
+
+  public Expression Arg => Args[0];
+
+  public override Attributes CloneAfter(Attributes prev) {
+    return new UserSuppliedAtAttribute(AtSign, Args[0], prev);
+  }
+
+  // Name of this @-Attribute, which is the part right after the @
+  public string UserSuppliedName =>
+    GetName(this);
+
+  // Pre-resolved bindings of this @-Attribute
+  public ActualBindings UserSuppliedPreResolveBindings =>
+    GetPreResolveBindings(this);
+
+  // Pre-resolved arguments of this @-Attributes. The order is the one provided by the user,
+  // not by any binding. Used for 
+  public IEnumerable<Expression> UserSuppliedPreResolveArguments =>
+    GetPreResolveArguments(this);
+
+  // Gets the name of an @-attribute. Attributes might be applied.
+  public static string GetName(Attributes a) {
+    if (a is UserSuppliedAtAttribute { Arg: ApplySuffix { Lhs: NameSegment { Name: var name } } }) {
+      return name;
+    }
+    if (a is UserSuppliedAtAttribute { Arg: NameSegment { Name: var singleName } }) {
+      return singleName;
+    }
+
+    return null;
+  }
+
+  // Gets the pre-resolved bindings of an @-Attribute.
+  // Returns an empty bindings if it's anything else
+  public static ActualBindings GetPreResolveBindings(Attributes a) {
+    if (a is UserSuppliedAtAttribute { Arg: ApplySuffix { Bindings: var bindings } }) {
+      return bindings;
+    }
+    return new ActualBindings(new List<ActualBinding>());
+  }
+
+  // Gets the list of pre-resolved arguments of an @-Attribute, and an empty list otherwise
+  public static IEnumerable<Expression> GetPreResolveArguments(Attributes a) {
+    if (a is UserSuppliedAtAttribute { UserSuppliedPreResolveBindings: var bindings }) {
+      return bindings.ArgumentBindings.Select(arg => arg.Actual);
+    }
+
+    return new List<Expression>();
+  }
+
+  // Gets the list of pre-resolved arguments of an @-Attribute, and the list of arguments
+  // for any other kind of attributes. Used for example to extract module options for parsing.
+  public static IEnumerable<Expression> GetUserSuppliedArguments(Attributes a) {
+    return a is UserSuppliedAtAttribute { UserSuppliedPreResolveArguments: var arguments } ? arguments : a.Args;
+  }
+}
+
 /// <summary>
 /// A class implementing this interface is one that can carry attributes.
 /// </summary>
 public interface IAttributeBearingDeclaration {
-  Attributes Attributes { get; }
+  Attributes Attributes { get; internal set; }
 }
 
 public static class AttributeBearingDeclarationExtensions {
diff --git a/Source/DafnyCore/AST/Cloner.cs b/Source/DafnyCore/AST/Cloner.cs
index d42e6358abc..66ff187b38a 100644
--- a/Source/DafnyCore/AST/Cloner.cs
+++ b/Source/DafnyCore/AST/Cloner.cs
@@ -334,10 +334,11 @@ public Attributes CloneAttributes(Attributes attrs) {
       } else if (!CloneResolvedFields && attrs.Name.StartsWith("_")) {
         // skip this attribute, since it would have been produced during resolution
         return CloneAttributes(attrs.Prev);
-      } else if (attrs is UserSuppliedAttributes) {
-        var usa = (UserSuppliedAttributes)attrs;
+      } else if (attrs is UserSuppliedAttributes usa) {
         return new UserSuppliedAttributes(Tok(usa.tok), Tok(usa.OpenBrace), Tok(usa.CloseBrace),
           attrs.Args.ConvertAll(CloneExpr), CloneAttributes(attrs.Prev));
+      } else if (attrs is UserSuppliedAtAttribute usaa) {
+        return new UserSuppliedAtAttribute(Tok(usaa.tok), CloneExpr(usaa.Arg), CloneAttributes(usaa.Prev));
       } else {
         return new Attributes(attrs.Name, attrs.Args.ConvertAll(CloneExpr), CloneAttributes(attrs.Prev));
       }
diff --git a/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs b/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs
index 0abfc1614cd..b137babd8de 100644
--- a/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs
+++ b/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs
@@ -40,7 +40,10 @@ void ObjectInvariant() {
   }
 
   public Attributes Attributes;
-  Attributes IAttributeBearingDeclaration.Attributes => Attributes;
+  Attributes IAttributeBearingDeclaration.Attributes {
+    get => Attributes;
+    set => Attributes = value;
+  }
 
   [FilledInDuringResolution] public List<BoundedPool> Bounds;
   // invariant Bounds == null || Bounds.Count == BoundVars.Count;
diff --git a/Source/DafnyCore/AST/Expressions/Expression.cs b/Source/DafnyCore/AST/Expressions/Expression.cs
index 7b4f54224e3..eef5c6e69d2 100644
--- a/Source/DafnyCore/AST/Expressions/Expression.cs
+++ b/Source/DafnyCore/AST/Expressions/Expression.cs
@@ -390,10 +390,21 @@ public static Expression CreateDecrement(Expression e, int n, Type ty = null) {
     if (n == 0) {
       return e;
     }
-    var nn = CreateIntLiteral(e.tok, n, ty);
+    var nn = CreateIntLiteralNonnegative(e.tok, n, ty);
     return CreateSubtract(e, nn);
   }
 
+  /// <summary>
+  /// Create a resolved expression of the form "n" when n is nonnegative
+  /// </summary>
+  public static LiteralExpr CreateIntLiteralNonnegative(IToken tok, int n, Type ty = null) {
+    Contract.Requires(tok != null);
+    Contract.Requires(0 <= n);
+    var nn = new LiteralExpr(tok, n);
+    nn.Type = ty ?? Type.Int;
+    return nn;
+  }
+
   /// <summary>
   /// Create a resolved expression of the form "n"
   /// </summary>
@@ -401,11 +412,9 @@ public static Expression CreateIntLiteral(IToken tok, int n, Type ty = null) {
     Contract.Requires(tok != null);
     Contract.Requires(n != int.MinValue);
     if (0 <= n) {
-      var nn = new LiteralExpr(tok, n);
-      nn.Type = ty ?? Type.Int;
-      return nn;
+      return CreateIntLiteralNonnegative(tok, n, ty);
     } else {
-      return CreateDecrement(CreateIntLiteral(tok, 0, ty), -n, ty);
+      return CreateDecrement(CreateIntLiteralNonnegative(tok, 0, ty), -n, ty);
     }
   }
 
diff --git a/Source/DafnyCore/AST/Grammar/ParseErrors.cs b/Source/DafnyCore/AST/Grammar/ParseErrors.cs
index 8e666089d15..898e1161766 100644
--- a/Source/DafnyCore/AST/Grammar/ParseErrors.cs
+++ b/Source/DafnyCore/AST/Grammar/ParseErrors.cs
@@ -11,6 +11,7 @@ public class ParseErrors {
   public enum ErrorId {
     // ReSharper disable once InconsistentNaming
     none,
+    p_extra_attributes,
     p_duplicate_modifier,
     p_abstract_not_allowed,
     p_no_ghost_for_by_method,
@@ -144,7 +145,9 @@ public enum ErrorId {
   }
 
   static ParseErrors() {
-
+    Add(ErrorId.p_extra_attributes,
+      @"
+@-attributes are not supported here".TrimStart(), Remove(true, "Remove this @-attribute"));
     Add(ErrorId.p_duplicate_modifier,
       @"
 No Dafny modifier, such as [`abstract`, `static`, `ghost`](https://dafny.org/latest/DafnyRef/DafnyRef#sec-declaration-modifiers) may be repeated
diff --git a/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs b/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs
index 783e1716810..2284767b3e3 100644
--- a/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs
+++ b/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs
@@ -25,6 +25,14 @@ public Parser(DafnyOptions options, Scanner/*!*/ scanner, Errors/*!*/ errors, Ca
     theModule = new FileModuleDefinition(scanner.FirstToken);
   }
 
+  public void MergeInto(ref Attributes attrsStack, ref Attributes attrsTarget) {
+    Attributes.MergeInto(ref attrsStack, ref attrsTarget);
+  }
+
+  public Attributes Consume(ref Attributes attrs) {
+    return Attributes.Consume(ref attrs);
+  }
+
   bool IsReveal(IToken nextToken) => la.kind == _reveal || (la.kind == _hide && nextToken.kind is _star or _ident);
 
   bool IsIdentifier(int kind) {
@@ -458,6 +466,30 @@ bool IsGenericInstantiation(bool inExpressionContext) {
         return false;
     }
   }
+
+  // Returns true if the parser can parse an heap-referencing @-call
+  // The reason to do this is that expressions can be prefixed by @-Attributes,
+  // so the rule to distinguish them is that an @-call of the form name@label(args),
+  // the @ must be next to the name. Otherwise an attribute is parsed.
+  // Indeed 'name' could be the last expression of an ensures clause, and the attribute
+  // could belong to the next method declaration otherwise.
+  bool IsAtCall() {
+    IToken pt = la;
+    if (pt.val != "@") {
+      return false;
+    }
+    // If it's the beginning of the file, or the previous token is on a different line or separated by a space, it's not an At-call. Must be an attribute
+    var isFirstToken = pt.Prev == null;
+    var spaceExistsSincePreviousToken =
+      !isFirstToken &&
+      (pt.Prev.line != pt.line || pt.Prev.col + pt.Prev.val.Length + pt.TrailingTrivia.Trim().Length < pt.col - pt.LeadingTrivia.Trim().Length);
+    if (isFirstToken || spaceExistsSincePreviousToken) {
+      return false;
+    }
+
+    return true;
+  }
+
   /* Returns true if the next thing is of the form:
    *     "<" Type { "," Type } ">"
    */
@@ -608,7 +640,7 @@ int StringToInt(string s, int defaultValue, string errString, IToken tok) {
   int anonymousIds = 0;
 
   /// <summary>
-  /// Holds the modifiers given for a declaration
+  /// Holds the modifiers and attributes given for a declaration
   ///
   /// Not all modifiers are applicable to all kinds of declarations.
   /// Errors are given when a modify does not apply.
@@ -627,6 +659,7 @@ class DeclModifierData {
     public bool IsOpaque;
     public IToken OpaqueToken;
     public IToken FirstToken;
+    public Attributes Attributes = null;
   }
 
   private ModuleKindEnum GetModuleKind(DeclModifierData mods) {
@@ -644,6 +677,16 @@ private ModuleKindEnum GetModuleKind(DeclModifierData mods) {
     return ModuleKindEnum.Concrete;
   }
 
+  /// <summary>
+  /// Before literals that end a block, we usually add CheckNoAttributes to avoid any non-attached or dangling attributes
+  /// </summary>
+  public void CheckNoAttributes(ref Attributes attrs) {
+    if (attrs != null) {
+      SemErr(ErrorId.p_extra_attributes, attrs.RangeToken, "Attribute not expected here");
+      attrs = null;
+    }
+  }
+
   // Check that token has not been set, then set it.
   public void CheckAndSetToken(ref IToken token) {
     if (token != null) {
@@ -725,10 +768,10 @@ Expression ProcessTupleArgs(List<ActualBinding> args, IToken lp) {
 
 
   public void ApplyOptionsFromAttributes(Attributes attrs) {
-    var overrides = attrs.AsEnumerable().Where(a => a.Name == "options")
+    var overrides = attrs.AsEnumerable().Where(a => a.Name == "options" || a is UserSuppliedAtAttribute { UserSuppliedName: "Options" })
       .Reverse().Select(a =>
-        (token: (a as UserSuppliedAttributes)?.tok,
-         options: a.Args.Select(arg => {
+        (token: a.tok,
+         options: UserSuppliedAtAttribute.GetUserSuppliedArguments(a).Select(arg => {
            if (arg is not LiteralExpr { Value: string optStr }) {
              SemErr(ErrorId.p_literal_string_required, arg.tok, "argument to :options attribute must be a literal string");
              return null;
diff --git a/Source/DafnyCore/AST/Statements/Assignment/AttributedToken.cs b/Source/DafnyCore/AST/Statements/Assignment/AttributedToken.cs
index 49545c285a5..a1f60a99abc 100644
--- a/Source/DafnyCore/AST/Statements/Assignment/AttributedToken.cs
+++ b/Source/DafnyCore/AST/Statements/Assignment/AttributedToken.cs
@@ -12,5 +12,8 @@ namespace Microsoft.Dafny;
 /// attributes).
 /// </summary>
 public record AttributedToken(IToken Token, Attributes Attrs) : IAttributeBearingDeclaration {
-  Attributes IAttributeBearingDeclaration.Attributes => Attrs;
+  Attributes IAttributeBearingDeclaration.Attributes {
+    get => Attrs;
+    set => throw new System.NotImplementedException();
+  }
 }
\ No newline at end of file
diff --git a/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs b/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs
index ab2331d019f..c20a0ab46ad 100644
--- a/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs
+++ b/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs
@@ -9,7 +9,11 @@ public class LocalVariable : RangeNode, IVariable, IAttributeBearingDeclaration
   readonly string name;
   public string DafnyName => Name;
   public Attributes Attributes;
-  Attributes IAttributeBearingDeclaration.Attributes => Attributes;
+  Attributes IAttributeBearingDeclaration.Attributes {
+    get => Attributes;
+    set => Attributes = value;
+  }
+
   public bool IsGhost;
   [ContractInvariantMethod]
   void ObjectInvariant() {
diff --git a/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs b/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs
index db68fdf4112..44aa0d7d31c 100644
--- a/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs
+++ b/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs
@@ -124,7 +124,10 @@ public virtual string GetCompileName(DafnyOptions options) {
   }
 
   public Attributes Attributes;  // readonly, except during class merging in the refinement transformations and when changed by Compiler.MarkCapitalizationConflict
-  Attributes IAttributeBearingDeclaration.Attributes => Attributes;
+  Attributes IAttributeBearingDeclaration.Attributes {
+    get => Attributes;
+    set => Attributes = value;
+  }
 
   [Pure]
   public override string ToString() {
diff --git a/Source/DafnyCore/AST/Types/Types.cs b/Source/DafnyCore/AST/Types/Types.cs
index 7c49af62df7..423797040a4 100644
--- a/Source/DafnyCore/AST/Types/Types.cs
+++ b/Source/DafnyCore/AST/Types/Types.cs
@@ -17,6 +17,11 @@ public abstract class Type : TokenNode {
   public override IEnumerable<INode> PreResolveChildren => TypeArgs.OfType<Node>();
   public static Type Nat() { return new UserDefinedType(Token.NoToken, "nat", null); }  // note, this returns an unresolved type
   public static Type String() { return new UserDefinedType(Token.NoToken, "string", null); }  // note, this returns an unresolved type
+
+  public static Type ResolvedString() {
+    return new SeqType(new CharType());
+  }
+
   public static readonly BigOrdinalType BigOrdinal = new BigOrdinalType();
 
   private static ThreadLocal<List<VisibilityScope>> _scopes = new();
diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg
index e41632969e0..0755626b118 100644
--- a/Source/DafnyCore/Dafny.atg
+++ b/Source/DafnyCore/Dafny.atg
@@ -213,6 +213,7 @@ PRODUCTIONS
 Dafny
 = (. IToken includeStartToken;
      IToken fileStartToken = t;
+     Attributes attrs = null;
   .)
   { "include"                 (. includeStartToken = t; .)
     stringToken               (. {
@@ -231,7 +232,9 @@ Dafny
                                }
                             .)
   }
-  { TopDecl<theModule, /* isTopLevel */ true> }
+  { AtAttributes<ref attrs>
+    TopDecl<theModule, /* isTopLevel */ true, ref attrs> }
+  (. CheckNoAttributes(ref attrs); .)
   (. 
     theModule.RangeToken = new RangeToken(fileStartToken.Next, t);
   .)
@@ -250,8 +253,11 @@ DeclModifier<ref DeclModifierData dmod>
   .
 
 /*------------------------------------------------------------------------*/
-TopDecl<. ModuleDefinition module, bool isTopLevel .>
-= (. DeclModifierData dmod = new DeclModifierData(); ModuleDecl submodule;
+TopDecl<ModuleDefinition module, bool isTopLevel, ref Attributes attrs>
+= (. DeclModifierData dmod = new DeclModifierData() {
+       Attributes = Consume(ref attrs)
+     };
+     ModuleDecl submodule;
      DatatypeDecl/*!*/ dt; TopLevelDecl td; IteratorDecl iter;
      TraitDecl/*!*/ trait;
   .)
@@ -323,7 +329,7 @@ ModuleDefinition<DeclModifierData dmod, ModuleDefinition parent, out ModuleDecl
      var dafnyOptionsBackup = theOptions;
      CheckDeclModifiers(ref dmod, "module", AllowedDeclModifiers.Abstract | AllowedDeclModifiers.Replaceable);
    .)
-   { Attribute<ref attrs> }            (. ApplyOptionsFromAttributes(attrs); .)
+   { Attribute<ref dmod.Attributes> }            (. ApplyOptionsFromAttributes(dmod.Attributes); .)
    ModuleQualifiedName<out var names>
    (. var name = names[^1];
       prefixIds = names.GetRange(0,names.Count-1).Select(n => n.StartToken).ToList();
@@ -334,12 +340,14 @@ ModuleDefinition<DeclModifierData dmod, ModuleDefinition parent, out ModuleDecl
    | Ident<out iderr> (. SemErr(ErrorId.p_bad_module_decl, t, $"expected either a '{{' or a 'refines' keyword here, found {iderr.val}"); .)
    ]
    (. module = new ModuleDefinition(RangeToken.NoToken, name, prefixIds, GetModuleKind(dmod), false,
-                                        idRefined == null ? null : new Implements(implementationKind, new ModuleQualifiedId(idRefined)), parent, attrs);
+                                        idRefined == null ? null : new Implements(implementationKind, new ModuleQualifiedId(idRefined)), parent, dmod.Attributes);
    .)
    SYNC                                (. tokenWithTrailingDocString = t; .)
    "{"                                 (. module.BodyStartTok = t; .)
-     { TopDecl<module, /* isTopLevel */ false>}
+     { AtAttributes<ref attrs>
+       TopDecl<module, /* isTopLevel */ false, ref attrs>}
    "}"
+   (. CheckNoAttributes(ref attrs); .)
     (.
       module.RangeToken = new RangeToken(dmod.FirstToken, t);
       module.TokenWithTrailingDocString = tokenWithTrailingDocString;
@@ -524,7 +532,7 @@ ClassDecl<DeclModifierData dmodClass, ModuleDefinition/*!*/ module, out TopLevel
   .)
   SYNC
   "class" (. CheckAndSetTokenOnce(ref dmodClass.FirstToken); .)
-  { Attribute<ref attrs> }
+  { Attribute<ref dmodClass.Attributes> }
   ClassName<out name>                     (. tokenWithTrailingDocString = t; .)
   [ GenericParameters<typeArgs, true> ] (. tokenWithTrailingDocString = t; .)
   [ ExtendsClause<parentTraits, out tokenWithTrailingDocString, null>
@@ -630,7 +638,6 @@ DatatypeDecl<DeclModifierData dmod, ModuleDefinition/*!*/ module, out DatatypeDe
 = (. Contract.Requires(module != null);
      Contract.Ensures(Contract.ValueAtReturn(out dt)!=null);
      Name/*!*/ name;
-     Attributes attrs = null;
      List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();
      List<Type> parentTraits = new List<Type>();
      List<DatatypeCtor/*!*/> ctors = new List<DatatypeCtor/*!*/>();
@@ -644,7 +651,7 @@ DatatypeDecl<DeclModifierData dmod, ModuleDefinition/*!*/ module, out DatatypeDe
   ( "datatype"
   | "codatatype"     (. co = true; .)
   )                                        (. CheckAndSetTokenOnce(ref dmod.FirstToken); .)
-  { Attribute<ref attrs> }
+  { Attribute<ref dmod.Attributes> }
   DatatypeName<out name>
   [ GenericParameters<typeArgs, true> ]
   [ ExtendsClause<parentTraits, out _, co ? "codatatype" : "datatype"> ]
@@ -659,9 +666,9 @@ DatatypeDecl<DeclModifierData dmod, ModuleDefinition/*!*/ module, out DatatypeDe
   )
   [ TypeMembers<module, members> ]
   (. if (co) {
-       dt = new CoDatatypeDecl(new RangeToken(dmod.FirstToken, t), name, module, typeArgs, ctors, parentTraits, members, attrs, isRefining);
+       dt = new CoDatatypeDecl(new RangeToken(dmod.FirstToken, t), name, module, typeArgs, ctors, parentTraits, members, dmod.Attributes, isRefining);
      } else {
-       dt = new IndDatatypeDecl(new RangeToken(dmod.FirstToken, t), name, module, typeArgs, ctors, parentTraits, members, attrs, isRefining);
+       dt = new IndDatatypeDecl(new RangeToken(dmod.FirstToken, t), name, module, typeArgs, ctors, parentTraits, members, dmod.Attributes, isRefining);
      }
      dt.BodyStartTok = bodyStart;
      dt.TokenWithTrailingDocString = bodyStart;
@@ -694,7 +701,9 @@ TypeMembers<. ModuleDefinition/*!*/ module, List<MemberDecl> members .>
 = (. DeclModifierData dmod;
   .)
   "{"
-  { (. dmod = new DeclModifierData(); .)
+  { (. dmod = new DeclModifierData();
+    .)
+    AtAttributes<ref dmod.Attributes>
     { DeclModifier<ref dmod> }
     ClassMemberDecl<dmod, members, false, false>
   }
@@ -763,7 +772,6 @@ LocalVarName<out IToken id> = NoUSIdent<out id> .
 NewtypeDecl<DeclModifierData dmod, ModuleDefinition module, out TopLevelDecl td>
 = (. Name name;
      IToken bvId;
-     Attributes attrs = null;
      td = null;
      Type baseType = null;
      Expression constraint;
@@ -774,7 +782,7 @@ NewtypeDecl<DeclModifierData dmod, ModuleDefinition module, out TopLevelDecl td>
      var typeParameters = new List<TypeParameter>();
   .)
   "newtype" (. CheckAndSetTokenOnce(ref dmod.FirstToken); .)
-  { Attribute<ref attrs> }
+  { Attribute<ref dmod.Attributes> }
   NewtypeName<out name>
   [ GenericParameters<typeParameters, true> ]
   [ ExtendsClause<parentTraits, out _, "newtype"> ]
@@ -792,13 +800,13 @@ NewtypeDecl<DeclModifierData dmod, ModuleDefinition module, out TopLevelDecl td>
     [ TypeMembers<module, members> ]
     (. td = new NewtypeDecl(new RangeToken(dmod.FirstToken, t), name, typeParameters, module,
          new BoundVar(bvId, bvId.val, baseType),
-         constraint, witnessKind, witness, parentTraits, members, attrs, isRefining: false);
+         constraint, witnessKind, witness, parentTraits, members, dmod.Attributes, isRefining: false);
     .)
   | Type<out baseType>
     WitnessClause<out var witnessKind, out witness>
     [ TypeMembers<module, members> ]
     (. td = new NewtypeDecl(new RangeToken(dmod.FirstToken, t), name, typeParameters, module,
-         baseType, witnessKind, witness, parentTraits, members, attrs, isRefining: false);
+         baseType, witnessKind, witness, parentTraits, members, dmod.Attributes, isRefining: false);
     .)
   )
   | ellipsis
@@ -806,7 +814,7 @@ NewtypeDecl<DeclModifierData dmod, ModuleDefinition module, out TopLevelDecl td>
     (. baseType = null; // Base type is not known yet
        td = new NewtypeDecl(new RangeToken(dmod.FirstToken, t), name, typeParameters, module, baseType,
          SubsetTypeDecl.WKind.CompiledZero, null,
-         parentTraits, members, attrs, isRefining: true);
+         parentTraits, members, dmod.Attributes, isRefining: true);
     .)
   )  (. if (td != null) {
           td.TokenWithTrailingDocString = t; 
@@ -819,7 +827,6 @@ SynonymTypeName<out Name name> = Name<out name> .
 // The following includes Opaque type definitions
 SynonymTypeDecl<DeclModifierData dmod, ModuleDefinition module, out TopLevelDecl td>
 = (. IToken bvId;
-     Attributes attrs = null;
      var characteristics = new TypeParameter.TypeParameterCharacteristics(false);
      var typeArgs = new List<TypeParameter>();
      td = null;
@@ -832,7 +839,7 @@ SynonymTypeDecl<DeclModifierData dmod, ModuleDefinition module, out TopLevelDecl
      var isRefining = false;
   .)
   "type"                      (. CheckAndSetTokenOnce(ref dmod.FirstToken); .)
-  { Attribute<ref attrs> }
+  { Attribute<ref dmod.Attributes> }
   SynonymTypeName<out var name>
   { TypeParameterCharacteristics<ref characteristics> }
   [ GenericParameters<typeArgs, true> ]
@@ -844,12 +851,12 @@ SynonymTypeDecl<DeclModifierData dmod, ModuleDefinition module, out TopLevelDecl
       Expression<out constraint, false, true>
       WitnessClause<out var witnessKind, out witness>
       (. td = new SubsetTypeDecl(new RangeToken(dmod.FirstToken, t), name, characteristics, typeArgs, module, 
-            new BoundVar(bvId, bvId.val, ty), constraint, witnessKind, witness, attrs);
+            new BoundVar(bvId, bvId.val, ty), constraint, witnessKind, witness, dmod.Attributes);
          kind = "subset type";
       .)
     |
       Type<out ty>
-      (. td = new TypeSynonymDecl(new RangeToken(dmod.FirstToken, t), name, characteristics, typeArgs, module, ty, attrs);
+      (. td = new TypeSynonymDecl(new RangeToken(dmod.FirstToken, t), name, characteristics, typeArgs, module, ty, dmod.Attributes);
          kind = "type synonym";
       .)
     )
@@ -864,7 +871,7 @@ SynonymTypeDecl<DeclModifierData dmod, ModuleDefinition module, out TopLevelDecl
          // abstract type declarations at the very outermost program scope get an automatic (!new)
          characteristics.ContainsNoReferenceTypes = true;
        }
-       td = new AbstractTypeDecl(new RangeToken(dmod.FirstToken, t), name, module, characteristics, typeArgs, parentTraits, members, attrs, isRefining);
+       td = new AbstractTypeDecl(new RangeToken(dmod.FirstToken, t), name, module, characteristics, typeArgs, parentTraits, members, dmod.Attributes, isRefining);
      }
      td.TokenWithTrailingDocString = t;
   .)
@@ -1043,7 +1050,7 @@ IteratorDecl<DeclModifierData dmod, ModuleDefinition module, out IteratorDecl/*!
   .)
   SYNC
   "iterator"                (. CheckAndSetTokenOnce(ref dmod.FirstToken); .)
-  { Attribute<ref attrs> }
+  { Attribute<ref dmod.Attributes> }    (. MergeInto(ref attrs, ref dmod.Attributes); .)
   IteratorName<out var name>
   (
     [ GenericParameters<typeArgs, true> ]
@@ -1155,7 +1162,6 @@ MethodDecl<DeclModifierData dmod, bool allowConstructor, out Method/*!*/ m>
      bool hasName = false;
      Name name = new Name("<noNameGiven>");  
      IToken keywordToken;
-     Attributes attrs = null;
      List<TypeParameter/*!*/>/*!*/ typeArgs = new List<TypeParameter/*!*/>();
      List<Formal/*!*/> ins = new List<Formal/*!*/>();
      List<Formal/*!*/> outs = new List<Formal/*!*/>();
@@ -1219,7 +1225,7 @@ MethodDecl<DeclModifierData dmod, bool allowConstructor, out Method/*!*/ m>
                                     .)
   )                                 (. keywordToken = t;
                                        CheckDeclModifiers(ref dmod, caption, allowed); .)
-  { Attribute<ref attrs> }
+  { Attribute<ref dmod.Attributes> }
   [ MethodFunctionName<out name>               (. hasName = true; .)
   ]
   (. if (!hasName) {
@@ -1262,25 +1268,25 @@ MethodDecl<DeclModifierData dmod, bool allowConstructor, out Method/*!*/ m>
                            req, new Specification<FrameExpression>(reads, readsAttrs), 
                            new Specification<FrameExpression>(mod, modAttrs), ens, 
                            new Specification<Expression>(dec, decAttrs), 
-                           (DividedBlockStmt)body, attrs, signatureEllipsis);
+                           (DividedBlockStmt)body, dmod.Attributes, signatureEllipsis);
      } else if (isLeastLemma) {
        m = new LeastLemma(range, name, dmod.IsStatic, kType, typeArgs, ins, outs,
-                          req, new Specification<FrameExpression>(reads, readsAttrs), new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);
+                          req, new Specification<FrameExpression>(reads, readsAttrs), new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, dmod.Attributes, signatureEllipsis);
      } else if (isGreatestLemma) {
        m = new GreatestLemma(range, name, dmod.IsStatic, kType, typeArgs, ins, outs,
-                             req, new Specification<FrameExpression>(reads, readsAttrs), new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);
+                             req, new Specification<FrameExpression>(reads, readsAttrs), new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, dmod.Attributes, signatureEllipsis);
      } else if (isLemma) {
        m = new Lemma(range, name, dmod.IsStatic, typeArgs, ins, outs,
-                     req, new Specification<FrameExpression>(reads, readsAttrs), new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);
+                     req, new Specification<FrameExpression>(reads, readsAttrs), new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, dmod.Attributes, signatureEllipsis);
      } else if (isTwoStateLemma) {
        m = new TwoStateLemma(range, name, dmod.IsStatic, typeArgs, ins, outs,
                              req, new Specification<FrameExpression>(reads, readsAttrs), new Specification<FrameExpression>(mod, modAttrs),
-                             ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);
+                             ens, new Specification<Expression>(dec, decAttrs), body, dmod.Attributes, signatureEllipsis);
      } else {
        m = new Method(range, name, dmod.IsStatic, dmod.IsGhost, typeArgs, ins, outs,
                       req, new Specification<FrameExpression>(reads, readsAttrs), 
                       new Specification<FrameExpression>(mod, modAttrs), ens, 
-                      new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);
+                      new Specification<Expression>(dec, decAttrs), body, dmod.Attributes, signatureEllipsis);
      }
      m.BodyStartTok = bodyStart;
      m.TokenWithTrailingDocString = tokenWithTrailingDocString;
@@ -1415,23 +1421,23 @@ Formals<.bool incoming, bool allowGhostKeyword, bool allowNewKeyword, bool allow
      Expression defaultValue;
      bool isNameOnly;
      bool isOlder;
-     Attributes attributes = null;
+     Attributes attrs = null;
      RangeToken range;
      Name name;
   .)
   "("
   [
-    { Attribute<ref attributes> }
+    { Attribute<ref attrs> }
     GIdentType<allowGhostKeyword, allowNewKeyword, incoming, allowOlderKeyword, out range, out name, out ty, out isGhost, out isOld, out isNameOnly, out isOlder>
     ParameterDefaultValue<incoming, out defaultValue>
-                 (. formals.Add(new Formal(name.Tok, name.Value, ty, incoming, isGhost, defaultValue, attributes, isOld, isNameOnly, isOlder)
+                 (. formals.Add(new Formal(name.Tok, name.Value, ty, incoming, isGhost, defaultValue, attrs, isOld, isNameOnly, isOlder)
                         { RangeToken = defaultValue != null ? new RangeToken(range.StartToken, defaultValue.EndToken) : range }
                     ); .)
-    { "," 
-      { Attribute<ref attributes> }
+    { ","
+      { Attribute<ref attrs> }
       GIdentType<allowGhostKeyword, allowNewKeyword, incoming, allowOlderKeyword, out range, out name, out ty, out isGhost, out isOld, out isNameOnly, out isOlder>
       ParameterDefaultValue<incoming, out defaultValue>
-                 (. formals.Add(new Formal(name.Tok, name.Value, ty, incoming, isGhost, defaultValue, attributes, isOld, isNameOnly, isOlder)
+                 (. formals.Add(new Formal(name.Tok, name.Value, ty, incoming, isGhost, defaultValue, attrs, isOld, isNameOnly, isOlder)
                         { RangeToken = defaultValue != null ? new RangeToken(range.StartToken, defaultValue.EndToken) : range }
                     ); .)
     }
@@ -1681,7 +1687,6 @@ GenericInstantiation<.List<Type> gt.>
 /*------------------------------------------------------------------------*/
 FunctionDecl<DeclModifierData dmod, out Function/*!*/ f>
 = (. Contract.Ensures(Contract.ValueAtReturn(out f) != null);
-     Attributes attrs = null;
      Name name = null; // To please compiler
      List<TypeParameter> typeArgs = new List<TypeParameter>();
      List<Formal> formals = new List<Formal>();
@@ -1691,6 +1696,7 @@ FunctionDecl<DeclModifierData dmod, out Function/*!*/ f>
      List<AttributedExpression> ens = new List<AttributedExpression>();
      List<FrameExpression> reads = new List<FrameExpression>();
      List<Expression> decreases;
+     Attributes attrs = null;
      Attributes decAttrs = null;
      Attributes readsAttrs = null;
      Expression body = null;
@@ -1747,7 +1753,7 @@ FunctionDecl<DeclModifierData dmod, out Function/*!*/ f>
   ( "function"   (. headToken = t; CheckAndSetTokenOnce(ref dmod.FirstToken); .)
     [ "method"   (. functionMethodToken = t; .)
     ]
-    { Attribute<ref attrs> }
+    { Attribute<ref dmod.Attributes> }
     MethodFunctionName<out name>
     (
       [ GenericParameters<typeArgs, false> ]
@@ -1770,7 +1776,7 @@ FunctionDecl<DeclModifierData dmod, out Function/*!*/ f>
   | "predicate"  (. headToken = t; isPredicate = true; CheckAndSetTokenOnce(ref dmod.FirstToken); .)
     [ "method"   (. functionMethodToken = t; .)
     ]
-    { Attribute<ref attrs> }
+    { Attribute<ref dmod.Attributes> }
     MethodFunctionName<out name>
     (
       [ GenericParameters<typeArgs, false> ]
@@ -1811,7 +1817,7 @@ FunctionDecl<DeclModifierData dmod, out Function/*!*/ f>
     | "copredicate"              (. CheckAndSetTokenOnce(ref dmod.FirstToken); errors.Deprecated(ErrorId.p_deprecated_copredicate, t, "the old keyword 'copredicate' has been renamed to the keyword phrase 'greatest predicate'"); .)
     )
     (. isGreatestPredicate = true; .)
-    { Attribute<ref attrs> }
+    { Attribute<ref dmod.Attributes> }
     MethodFunctionName<out name>
     (
       [ GenericParameters<typeArgs, false> ]
@@ -1982,39 +1988,38 @@ FunctionDecl<DeclModifierData dmod, out Function/*!*/ f>
      /* =========================================
       * Finally, we create the AST node for the function declaration we parsed.
       */
-
      var range = new RangeToken(dmod.FirstToken, t);
      if (isTwoState && isPredicate) {
        Contract.Assert(functionMethodToken == null && !dmod.IsGhost);
        f = new TwoStatePredicate(range, name, dmod.IsStatic, dmod.IsOpaque, typeArgs, formals, result,
                                  reqs, new Specification<FrameExpression>(reads, readsAttrs), ens, 
-                                 new Specification<Expression>(decreases, decAttrs), body, attrs, signatureEllipsis);
+                                 new Specification<Expression>(decreases, decAttrs), body, dmod.Attributes, signatureEllipsis);
      } else if (isTwoState) {
        Contract.Assert(functionMethodToken == null && !dmod.IsGhost);
        f = new TwoStateFunction(range, name, dmod.IsStatic, dmod.IsOpaque, typeArgs, formals, result, returnType,
                                 reqs, new Specification<FrameExpression>(reads, readsAttrs), ens, 
-                                new Specification<Expression>(decreases, decAttrs), body, attrs, signatureEllipsis);
+                                new Specification<Expression>(decreases, decAttrs), body, dmod.Attributes, signatureEllipsis);
      } else if (isPredicate) {
        Contract.Assert(functionMethodToken == null || !dmod.IsGhost);
        f = new Predicate(range, name, dmod.IsStatic, isGhost, dmod.IsOpaque, typeArgs, formals, result,
                          reqs, new Specification<FrameExpression>(reads, readsAttrs), ens, 
                          new Specification<Expression>(decreases, decAttrs), body, Predicate.BodyOriginKind.OriginalOrInherited,
-                         byMethodTok, byMethodBody, attrs, signatureEllipsis);
+                         byMethodTok, byMethodBody, dmod.Attributes, signatureEllipsis);
      } else if (isLeastPredicate) {
        Contract.Assert(functionMethodToken == null && !dmod.IsGhost);
        f = new LeastPredicate(range, name, dmod.IsStatic, dmod.IsOpaque, kType, typeArgs, formals, result,
-                              reqs, new Specification<FrameExpression>(reads, readsAttrs), ens, body, attrs, signatureEllipsis);
+                              reqs, new Specification<FrameExpression>(reads, readsAttrs), ens, body, dmod.Attributes, signatureEllipsis);
      } else if (isGreatestPredicate) {
        Contract.Assert(functionMethodToken == null && !dmod.IsGhost);
        f = new GreatestPredicate(range, name, dmod.IsStatic, dmod.IsOpaque, kType, typeArgs, formals, result,
-                                 reqs, new Specification<FrameExpression>(reads, readsAttrs), ens, body, attrs, signatureEllipsis);
+                                 reqs, new Specification<FrameExpression>(reads, readsAttrs), ens, body, dmod.Attributes, signatureEllipsis);
      } else {
        Contract.Assert(functionMethodToken == null || !dmod.IsGhost);
        f = new Function(range, name, dmod.IsStatic, isGhost, dmod.IsOpaque,
                         typeArgs, formals, result, returnType,
                         reqs, new Specification<FrameExpression>(reads, readsAttrs), ens, new Specification<Expression>(decreases, decAttrs), body,
                         byMethodTok, byMethodBody,
-                        attrs, signatureEllipsis);
+                        dmod.Attributes, signatureEllipsis);
      }
      f.BodyStartTok = bodyStart;
      f.TokenWithTrailingDocString = tokenWithTrailingDocString;
@@ -3833,7 +3838,9 @@ ParensExpression<out Expression e>
      var args = new List<ActualBinding>();
      e = dummyExpr;
   .)
- "("                                        (. lp = t; .)
+ "("
+ (. lp = t;
+ .)
   (
     MaybeDecreasesToExpression<out e, lp>
     ")"                                     (. rp = t;
@@ -4255,9 +4262,11 @@ NameSegment<out Expression e>
   ( IF(IsGenericInstantiation(true))
     (. typeArgs = new List<Type>(); .)
     GenericInstantiation<typeArgs>
-    [ AtCall<out atLabel, out openParen, out args> ]
+    [ IF(IsAtCall())
+      AtCall<out atLabel, out openParen, out args> ]
   | HashCall<id, out openParen, out typeArgs, out args>
-  | [ AtCall<out atLabel, out openParen, out args> ]
+  | [ IF(IsAtCall())
+      AtCall<out atLabel, out openParen, out args> ]
   )
   /* Note, since HashCall updates id.val, we make sure not to use id.val until after the possibility of calling HashCall. */
   (. e = new NameSegment(id, id.val, typeArgs);
@@ -4346,9 +4355,11 @@ Suffix<ref Expression e>
       ( IF(IsGenericInstantiation(true))
         (. typeArgs = new List<Type>(); .)
         GenericInstantiation<typeArgs>
-        [ AtCall<out atLabel, out openParen, out args> ]
+        [ IF(IsAtCall())
+          AtCall<out atLabel, out openParen, out args> ]
       | HashCall<id, out openParen, out typeArgs, out args>
-      | [ AtCall<out atLabel, out openParen, out args> ]
+      | [ IF(IsAtCall())
+          AtCall<out atLabel, out openParen, out args> ]
       )
       (. e = new ExprDotName(id, e, id.val, typeArgs) {
            RangeToken = new RangeToken(startToken, id)
@@ -4593,6 +4604,28 @@ Attribute<ref Attributes attrs>
   .)
   .
 
+AtAttributes<ref Attributes attrs>
+= { AtAttribute<ref attrs> }
+  .
+
+/* After literals that start a block, we usually add this
+   Note that it will parse all at-attributes at once since expression parsing
+   return attributes parsed after them. No need to wrap in a repeat statement
+*/
+AtAttribute<ref Attributes attrs>
+= (. IToken atToken = null;
+     Expression arg;
+  .)
+  "@"
+  (. atToken = t; .)
+  Expression<out arg, false, false, false>
+  (. 
+     var rtok = new RangeToken(atToken, t);
+     attrs = new UserSuppliedAtAttribute(t, arg, attrs);
+     attrs.RangeToken = rtok;
+  .)
+  .
+
 /*------------------------------------------------------------------------*/
 Ident<out IToken/*!*/ x>
 = (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); .)
diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs
index ae9de04f6b2..88ad0616f38 100644
--- a/Source/DafnyCore/Resolver/ModuleResolver.cs
+++ b/Source/DafnyCore/Resolver/ModuleResolver.cs
@@ -3512,7 +3512,7 @@ void ResolveCasePattern<VT>(CasePattern<VT> pat, Type sourceType, ResolutionCont
     /// <summary>
     /// This method is called at the tail end of Pass1 of the Resolver.
     /// </summary>
-    void FillInDefaultValueExpressions() {
+    internal void FillInDefaultValueExpressions() {
       var visited = new Dictionary<DefaultValueExpression, DefaultValueExpression.WorkProgress>();
       foreach (var e in allDefaultValueExpressions) {
         e.FillIn(this, visited);
diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs
index f78d2a8e742..d6950c5f50c 100644
--- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs
+++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs
@@ -319,15 +319,20 @@ public void ResolveAttributes(IAttributeBearingDeclaration attributeHost, Resolu
 
       // order does not matter much for resolution, so resolve them in reverse order
       foreach (var attr in attributeHost.Attributes.AsEnumerable()) {
-        if (attr is UserSuppliedAttributes) {
-          var usa = (UserSuppliedAttributes)attr;
+        if (attr is UserSuppliedAtAttribute { Builtin: true }) { // Already resolved
+          continue;
+        } else if (attr is UserSuppliedAttributes usa) {
           usa.Recognized = IsRecognizedAttribute(usa, attributeHost);
         }
         if (attr.Args != null) {
           foreach (var arg in attr.Args) {
             Contract.Assert(arg != null);
             if (!(Attributes.Contains(attributeHost.Attributes, "opaque_reveal") && attr.Name is "revealedFunction" && arg is NameSegment)) {
+              var prevCount = reporter.ErrorCount;
               ResolveExpression(arg, resolutionContext);
+              if (prevCount == reporter.ErrorCount && attr is UserSuppliedAtAttribute { Builtin: false }) {
+                reporter.Error(MessageSource.Resolver, attr.tok, "User-supplied @-Attributes not supported yet");
+              }
             } else {
               ResolveRevealLemmaAttribute(arg);
             }
@@ -3200,7 +3205,7 @@ void ResolveCallStmt(CallStmt s, ResolutionContext resolutionContext, Type recei
     /// "typeMap" is applied to the type of each formal.
     /// This method should be called only once. That is, bindings.arguments is required to be null on entry to this method.
     /// </summary>
-    void ResolveActualParameters(ActualBindings bindings, List<Formal> formals, IToken callTok, object context, ResolutionContext resolutionContext,
+    internal void ResolveActualParameters(ActualBindings bindings, List<Formal> formals, IToken callTok, object context, ResolutionContext resolutionContext,
       Dictionary<TypeParameter, Type> typeMap, Expression/*?*/ receiver) {
       Contract.Requires(bindings != null);
       Contract.Requires(formals != null);
diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.ActualParameters.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.ActualParameters.cs
index 6b6a9af13a9..b8ea8118052 100644
--- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.ActualParameters.cs
+++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.ActualParameters.cs
@@ -18,7 +18,7 @@ public partial class PreTypeResolver {
     /// "typeMap" is applied to the type of each formal.
     /// This method should be called only once. That is, bindings.arguments is required to be null on entry to this method.
     /// </summary>
-    void ResolveActualParameters(ActualBindings bindings, List<Formal> formals, IToken callTok, object context, ResolutionContext opts,
+    internal void ResolveActualParameters(ActualBindings bindings, List<Formal> formals, IToken callTok, object context, ResolutionContext opts,
       Dictionary<TypeParameter, PreType> typeMap, Expression/*?*/ receiver) {
       Contract.Requires(bindings != null);
       Contract.Requires(formals != null);
diff --git a/Source/DafnyCore/Rewriters/ExpandAtAttributes.cs b/Source/DafnyCore/Rewriters/ExpandAtAttributes.cs
new file mode 100644
index 00000000000..28a31de1e1b
--- /dev/null
+++ b/Source/DafnyCore/Rewriters/ExpandAtAttributes.cs
@@ -0,0 +1,44 @@
+using System;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Dafny;
+
+/// <summary>
+/// Expands @Attribute to their previous version {:attribute} when recognized
+/// Marks recognized user-supplied @-attributes as .Builtin = true
+/// That way, only those not .Builtin are resolved.
+/// </summary>
+public class ExpandAtAttributes : IRewriter {
+  private readonly SystemModuleManager systemModuleManager;
+  public ExpandAtAttributes(Program program, ErrorReporter reporter)
+    : base(reporter) {
+    Contract.Requires(reporter != null);
+    Contract.Requires(systemModuleManager != null);
+    systemModuleManager = program.SystemModuleManager;
+  }
+
+  internal override void PreResolve(Program program) {
+    program.Visit((INode node) => {
+      if (node is not IAttributeBearingDeclaration attributeHost) {
+        return true;
+      }
+
+      Attributes extraAttrs = null;
+      foreach (var attr in attributeHost.Attributes.AsEnumerable()) {
+        if (attr is not UserSuppliedAtAttribute userSuppliedAtAttribute) {
+          continue;
+        }
+
+        var newAttributes = Attributes.ExpandAtAttribute(program, userSuppliedAtAttribute);
+        Attributes.MergeInto(ref newAttributes, ref extraAttrs);
+      }
+
+      var newAttrs = attributeHost.Attributes;
+      Attributes.MergeInto(ref extraAttrs, ref newAttrs);
+      attributeHost.Attributes = newAttrs;
+
+      return true;
+    });
+  }
+}
\ No newline at end of file
diff --git a/Source/DafnyCore/Rewriters/RewriterCollection.cs b/Source/DafnyCore/Rewriters/RewriterCollection.cs
index 573ad83e3e1..220944c1d88 100644
--- a/Source/DafnyCore/Rewriters/RewriterCollection.cs
+++ b/Source/DafnyCore/Rewriters/RewriterCollection.cs
@@ -12,7 +12,7 @@ public static IList<IRewriter> GetRewriters(ErrorReporter reporter, Program prog
     if (reporter.Options.AuditProgram) {
       result.Add(new Auditor.Auditor(reporter));
     }
-
+    result.Add(new ExpandAtAttributes(program, reporter));
     result.Add(new AutoContractsRewriter(program, reporter));
     result.Add(new OpaqueMemberRewriter(reporter));
     result.Add(new AutoReqFunctionRewriter(program, reporter));
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs
index 10d78a37498..b12a28b7a2f 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs
+++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs
@@ -2009,7 +2009,8 @@ public QKeyValue TrAttributes(Attributes attrs, string skipThisAttribute) {
               // omit the extern attribute when /noExterns option is specified.
               (name is "extern" && options.DisallowExterns) ||
               (name is "timeLimit" && hasNewTimeLimit) ||
-              (name is "rlimit" && hasNewRLimit)
+              (name is "rlimit" && hasNewRLimit) ||
+              (attr is UserSuppliedAtAttribute)
           ) {
             continue;
           }
diff --git a/Source/DafnyDriver/Commands/BoogieExtractor.cs b/Source/DafnyDriver/Commands/BoogieExtractor.cs
index dd9a226fdc0..6b76b853faf 100644
--- a/Source/DafnyDriver/Commands/BoogieExtractor.cs
+++ b/Source/DafnyDriver/Commands/BoogieExtractor.cs
@@ -186,7 +186,7 @@ public override void VisitMethod(Method method) {
       return triggers;
     }
 
-    private QKeyValue? GetKeyValues(IToken tok, Attributes attributes) {
+    private QKeyValue? GetKeyValues(IToken tok, Attributes? attributes) {
       QKeyValue? kv = null;
       var extractAttributes = Attributes.FindAllExpressions(attributes, AttributeAttribute);
       if (extractAttributes == null) {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-builtin.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-builtin.dfy
new file mode 100644
index 00000000000..2e771767c22
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-builtin.dfy
@@ -0,0 +1,45 @@
+// RUN: %resolve "%s"
+// Attributes on top-level declarations
+
+@Options("--function-syntax:3")
+module SimpleLinearModule {
+}
+
+function f(x:int) : bool
+  requires x > 3
+{
+  x > 7
+}
+
+@Compile(true)
+@Fuel(low := 1)
+@Fuel(low := 1, high := 2)
+function g(y:int, b:bool) : bool
+{
+  if b then f(y + 2) else f(2*y)
+}
+
+@IsolateAssertions
+method Test(a: int, b: int, c: int)
+  requires a < b && b < c
+{
+  assert a < c; 
+  assert c > a;
+}
+
+datatype Unary = Zero | Succ(Unary)
+
+function UnaryToNat(n: Unary): nat {
+  match n
+  case Zero => 0
+  case Succ(p) => 1 + UnaryToNat(p)
+}
+
+function NatToUnary(n: nat): Unary {
+  if n == 0 then Zero else Succ(NatToUnary(n - 1))
+}
+
+@Induction(n)
+lemma ByInduction(n: int){
+
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy
new file mode 100644
index 00000000000..e401748ab3f
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy
@@ -0,0 +1,29 @@
+// RUN: %exits-with -any %resolve "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// Attributes on top-level declarations
+
+function f(x:int) : bool
+  requires x > 3
+{
+  x > 7
+}
+
+@compile("true") // Should be Compile
+@Compile("true") // Should be boolean
+@Compile(true, false) // Should have one argument
+@fuel(low := 1, 2) // Should be Fuel
+@Fuel(2, low := 1) // Wrong position of arguments
+function g(y:int, b:bool) : bool
+{
+  if b then f(y + 2) else f(2*y)
+}
+
+@isolate_assertions // Should be IsolateAssertions 
+@IsolateAssertions("noargument") // Should have no argument.
+// Above is not treated as a @call with label "IsolateAssertion"
+method Test(a: int, b: int, c: int)
+  requires a < b && b < c
+{
+  assert a < c; 
+  assert c > a;
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy.expect
new file mode 100644
index 00000000000..17364533b1b
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy.expect
@@ -0,0 +1,8 @@
+at-attributes-typos.dfy(15,9): Error: the parameter named 'low' is already given positionally
+at-attributes-typos.dfy(13,8): Error: wrong number of arguments (got 2, but datatype constructor 'Compile' expects at most 1: (0: bool))
+at-attributes-typos.dfy(12,8): Error: incorrect argument type for datatype constructor parameter '0' (expected bool, found string)
+at-attributes-typos.dfy(22,18): Error: wrong number of arguments (got 1, but datatype constructor 'IsolateAssertions' expects 0)
+at-attributes-typos.dfy(14,1): Error: unresolved identifier: fuel
+at-attributes-typos.dfy(11,1): Error: unresolved identifier: compile
+at-attributes-typos.dfy(21,1): Error: unresolved identifier: isolate_assertions
+7 resolution/type errors detected in at-attributes-typos.dfy
diff --git a/Source/XUnitExtensions/Lit/DiffCommand.cs b/Source/XUnitExtensions/Lit/DiffCommand.cs
index 0fc0d11e4a9..db7408470f2 100644
--- a/Source/XUnitExtensions/Lit/DiffCommand.cs
+++ b/Source/XUnitExtensions/Lit/DiffCommand.cs
@@ -32,6 +32,9 @@ public static ILitCommand Parse(string[] args) {
 
     public static string? Run(string expectedOutputFile, string actualOutput) {
       if (UpdateExpectFile) {
+        if (Path.GetExtension(expectedOutputFile) == ".tmp") {
+          return "With DAFNY_INTEGRATION_TESTS_UPDATE_EXPECT_FILE=true, first argument of %diff cannot be a *.tmp file, it should be an *.expect file";
+        }
         var path = Path.GetFullPath(expectedOutputFile).Replace("bin" + Path.DirectorySeparatorChar + "Debug" + Path.DirectorySeparatorChar + "net6.0" + Path.DirectorySeparatorChar, "");
         File.WriteAllText(path, actualOutput);
         return null;