diff --git a/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs
index 9bf8edc631..89ed6dddcd 100644
--- a/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs
+++ b/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs
@@ -32,7 +32,7 @@ protected override CompletionRegistrationOptions CreateRegistrationOptions(Compl
       return new CompletionRegistrationOptions {
         DocumentSelector = DocumentSelector.ForLanguage("dafny"),
         ResolveProvider = false,
-        TriggerCharacters = new Container<string>(".")
+        TriggerCharacters = new Container<string>(".", "@")
       };
     }
 
@@ -49,7 +49,7 @@ public override async Task<CompletionList> Handle(CompletionParams request, Canc
         logger.LogWarning("location requested for unloaded document {DocumentUri}", request.TextDocument.Uri);
         return new CompletionList();
       }
-      return new CompletionProcessor(symbolGuesser, logger, document, request, cancellationToken, options).Process();
+      return new CompletionProcessor(symbolGuesser, logger, document, request, cancellationToken, options, await projects.GetProjectManager(request.TextDocument.Uri)).Process();
     }
 
     private class CompletionProcessor {
@@ -59,15 +59,18 @@ private class CompletionProcessor {
       private readonly IdeState state;
       private readonly CompletionParams request;
       private readonly CancellationToken cancellationToken;
+      private readonly ProjectManager? projectManager;
 
       public CompletionProcessor(ISymbolGuesser symbolGuesser, ILogger<DafnyCompletionHandler> logger, IdeState state,
-        CompletionParams request, CancellationToken cancellationToken, DafnyOptions options) {
+        CompletionParams request, CancellationToken cancellationToken, DafnyOptions options,
+        ProjectManager? projectManager) {
         this.symbolGuesser = symbolGuesser;
         this.state = state;
         this.request = request;
         this.cancellationToken = cancellationToken;
         this.options = options;
         this.logger = logger;
+        this.projectManager = projectManager;
       }
 
       public CompletionList Process() {
@@ -75,6 +78,10 @@ public CompletionList Process() {
           return CreateDotCompletionList();
         }
 
+        if (IsAtAttribute()) {
+          return CreateAtAttributeCompletionList();
+        }
+
         if (logger.IsEnabled(LogLevel.Trace)) {
           var program = (Program)state.ResolvedProgram!;
           var writer = new StringWriter();
@@ -86,11 +93,69 @@ public CompletionList Process() {
         return new CompletionList();
       }
 
+      private static string GetLastTwoCharactersBeforePositionIncluded(TextReader fileContent, DafnyPosition position) {
+        // To track the last two characters
+        char? prevChar = null;
+        char? currentChar = null;
+
+        // Read line by line
+        for (int lineNum = 0; lineNum <= position.Line; lineNum++) {
+          string? line = fileContent.ReadLine();
+          if (line == null) {
+            throw new InvalidOperationException("Reached end of file before finding the specified line.");
+          }
+
+          // If we are on the line of the specified position, handle the partial line case
+          if (lineNum == position.Line) {
+            int columnIndex = position.Column - 1; // Convert 1-based to 0-based index
+            for (int i = 0; i <= columnIndex; i++) {
+              prevChar = currentChar;
+              currentChar = line[i];
+            }
+            break;
+          } else {
+            // Otherwise, track the last two characters of this full line (including newline)
+            foreach (char c in line + '\n')  // Include '\n' for line end tracking
+            {
+              prevChar = currentChar;
+              currentChar = c;
+            }
+          }
+        }
+
+        // Handle case where fewer than 2 characters are available
+        if (prevChar == null) {
+          return currentChar?.ToString() ?? "";
+        }
+        return $"{prevChar}{currentChar}";
+      }
+
       private bool IsDotExpression() {
         var node = state.Program.FindNode<INode>(request.TextDocument.Uri.ToUri(), request.Position.ToDafnyPosition());
         return node?.RangeToken.EndToken.val == ".";
       }
 
+      private bool IsAtAttribute() {
+        var position = request.Position.ToDafnyPosition();
+        if (projectManager == null) {
+          return false;
+        }
+        var fileContent = projectManager.ReadFile(request.TextDocument.Uri.ToUri());
+        var lastTwoChars = GetLastTwoCharactersBeforePositionIncluded(fileContent, position);
+        var isAtAttribute =
+          lastTwoChars == "@" ||
+          lastTwoChars.Length >= 2 && lastTwoChars[1] == '@' && char.IsWhiteSpace(lastTwoChars[0]);
+        return isAtAttribute;
+      }
+
+      private CompletionList CreateAtAttributeCompletionList() {
+        var completionItems =
+          Attributes.BuiltinAtAttributes.Select(b =>
+            CreateCompletionItem(b.Name)
+          ).ToList();
+        return new CompletionList(completionItems);
+      }
+
       private CompletionList CreateDotCompletionList() {
         IEnumerable<ILegacySymbol> members;
         if (symbolGuesser.TryGetTypeBefore(state,
@@ -122,6 +187,15 @@ private static bool IsConstructor(ILegacySymbol symbol) {
         return symbol is MethodSymbol method && method.Name == "_ctor";
       }
 
+      private CompletionItem CreateCompletionItem(string attributeName) {
+        return new CompletionItem {
+          Label = attributeName,
+          Kind = CompletionItemKind.Constructor,
+          InsertText = attributeName, // TODO: Parentheses
+          Detail = "" // TODO: Details of attribute name
+        };
+      }
+
       private CompletionItem CreateCompletionItem(ILegacySymbol symbol) {
         return new CompletionItem {
           Label = symbol.Name,
diff --git a/Source/DafnyLanguageServer/Workspace/ProjectManager.cs b/Source/DafnyLanguageServer/Workspace/ProjectManager.cs
index 9498e3ba54..09bff0e272 100644
--- a/Source/DafnyLanguageServer/Workspace/ProjectManager.cs
+++ b/Source/DafnyLanguageServer/Workspace/ProjectManager.cs
@@ -2,6 +2,7 @@
 using System.Collections.Concurrent;
 using System.Collections.Generic;
 using System.CommandLine;
+using System.IO;
 using System.Linq;
 using System.Numerics;
 using System.Reactive.Concurrency;
@@ -126,6 +127,10 @@ public ProjectManager(
 
   private const int MaxRememberedChanges = 100;
 
+  public TextReader ReadFile(Uri fileToRead) {
+    return fileSystem.ReadFile(fileToRead);
+  }
+
   public void UpdateDocument(DidChangeTextDocumentParams documentChange) {
     StartNewCompilation(documentChange.TextDocument.Uri.ToUri(), documentChange);
   }