diff --git a/.gitignore b/.gitignore
index 113e2a203e..7c7b709064 100644
--- a/.gitignore
+++ b/.gitignore
@@ -85,3 +85,7 @@ pythonenv*
 /clang/utils/analyzer/projects/*/RefScanBuildResults
 # automodapi puts generated documentation files here.
 /lldb/docs/python_api/
+
+
+# custom
+docs/
\ No newline at end of file
diff --git a/README.md b/README.md
index a7afe77e9d..4c2469762a 100644
--- a/README.md
+++ b/README.md
@@ -63,6 +63,31 @@ All contract syntax is gated behind `-fverify-contracts`. Without the flag,
 none of these names are reserved — existing C++ that uses `pre`, `post`, etc.
 as identifiers compiles unchanged.
 
+## Build the cpp-verify clang compiler
+
+```bash
+cmake -S llvm -B build -G Ninja \
+    -DCMAKE_BUILD_TYPE=Release \
+    -DLLVM_ENABLE_PROJECTS="clang" \
+    -DLLVM_TARGETS_TO_BUILD="X86,AArch64" \
+    -DCMAKE_EXPORT_COMPILE_COMMANDS=ON
+
+# Symlink compile_commands.json for clangd / IDE integration
+ln -sf build/compile_commands.json compile_commands.json
+
+ninja -C build clang -j$(nproc)
+```
+
+## Usage
+
+```bash
+# Identifying tokens and dumping the output
+./build/bin/clang++ -cc1 -fverify-contracts -dump-tokens samples/test1.cpp
+
+# Parsing AST with contracts and dumping the output
+./build/bin/clang++ -cc1 -fverify-contracts -ast-dump samples/test1.cpp
+```
+
 ## Architecture
 
 ```
diff --git a/clang/include/clang/AST/ASTContext.h b/clang/include/clang/AST/ASTContext.h
index 68205dd1c1..b2fd8e06ef 100644
--- a/clang/include/clang/AST/ASTContext.h
+++ b/clang/include/clang/AST/ASTContext.h
@@ -94,6 +94,21 @@ class AtomicExpr;
 class BlockExpr;
 struct BlockVarCopyInit;
 class BuiltinTemplateDecl;
+
+/// Contract information attached to a FunctionDecl via side table.
+struct FunctionContractInfo {
+  SmallVector<Expr *, 2> Preconditions;
+  SmallVector<Expr *, 2> Postconditions;
+  Expr *Decreases = nullptr;
+  bool IsSpec = false;
+  bool IsProof = false;
+};
+
+/// Contract information attached to a WhileStmt/ForStmt via side table.
+struct LoopContractInfo {
+  SmallVector<Expr *, 2> Invariants;
+  Expr *Decreases = nullptr;
+};
 class CharUnits;
 class ConceptDecl;
 class CXXABI;
@@ -351,6 +366,13 @@ class ASTContext : public RefCountedBase<ASTContext> {
   /// Mapping from __block VarDecls to BlockVarCopyInit.
   llvm::DenseMap<const VarDecl *, BlockVarCopyInit> BlockVarCopyInits;
 
+  /// CppVerify: contract info for functions (pre/post/decreases/spec/proof).
+  llvm::DenseMap<const FunctionDecl *, FunctionContractInfo *>
+      FunctionContracts;
+
+  /// CppVerify: contract info for loops (invariant/decreases).
+  llvm::DenseMap<const Stmt *, LoopContractInfo *> LoopContracts;
+
   /// Mapping from GUIDs to the corresponding MSGuidDecl.
   mutable llvm::FoldingSet<MSGuidDecl> MSGuidDecls;
 
@@ -3422,6 +3444,16 @@ class ASTContext : public RefCountedBase<ASTContext> {
   /// nullptr if none exists.
   BlockVarCopyInit getBlockVarCopyInit(const VarDecl* VD) const;
 
+  /// CppVerify: get or create contract info for a function.
+  FunctionContractInfo &getOrCreateFunctionContract(const FunctionDecl *FD);
+  /// CppVerify: get contract info for a function, or nullptr if none.
+  const FunctionContractInfo *getFunctionContract(const FunctionDecl *FD) const;
+
+  /// CppVerify: get or create contract info for a loop statement.
+  LoopContractInfo &getOrCreateLoopContract(const Stmt *S);
+  /// CppVerify: get contract info for a loop, or nullptr if none.
+  const LoopContractInfo *getLoopContract(const Stmt *S) const;
+
   /// Allocate an uninitialized TypeSourceInfo.
   ///
   /// The caller should initialize the memory held by TypeSourceInfo using
diff --git a/clang/include/clang/AST/ASTDumper.h b/clang/include/clang/AST/ASTDumper.h
index 71ac467e51..80b8ae15a2 100644
--- a/clang/include/clang/AST/ASTDumper.h
+++ b/clang/include/clang/AST/ASTDumper.h
@@ -23,9 +23,12 @@ class ASTDumper : public ASTNodeTraverser<ASTDumper, TextNodeDumper> {
 
   const bool ShowColors;
 
+  const ASTContext *Ctx = nullptr;
+
 public:
   ASTDumper(raw_ostream &OS, const ASTContext &Context, bool ShowColors)
-      : NodeDumper(OS, Context, ShowColors), OS(OS), ShowColors(ShowColors) {}
+      : NodeDumper(OS, Context, ShowColors), OS(OS), ShowColors(ShowColors),
+        Ctx(&Context) {}
 
   ASTDumper(raw_ostream &OS, bool ShowColors)
       : NodeDumper(OS, ShowColors), OS(OS), ShowColors(ShowColors) {}
@@ -44,6 +47,11 @@ class ASTDumper : public ASTNodeTraverser<ASTDumper, TextNodeDumper> {
   void VisitFunctionTemplateDecl(const FunctionTemplateDecl *D);
   void VisitClassTemplateDecl(const ClassTemplateDecl *D);
   void VisitVarTemplateDecl(const VarTemplateDecl *D);
+
+  // CppVerify: dump contract side-table entries as child nodes.
+  void VisitFunctionDecl(const FunctionDecl *D);
+  void VisitWhileStmt(const WhileStmt *S);
+  void VisitForStmt(const ForStmt *S);
 };
 
 } // namespace clang
diff --git a/clang/include/clang/AST/ExprContract.h b/clang/include/clang/AST/ExprContract.h
new file mode 100644
index 0000000000..3f9bb4bf28
--- /dev/null
+++ b/clang/include/clang/AST/ExprContract.h
@@ -0,0 +1,197 @@
+//===--- ExprContract.h - Contract expression AST nodes ---------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// This file defines AST nodes for CppVerify contract expressions:
+//   ForallExpr, ExistsExpr, OldExpr, ResultExpr
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_AST_EXPRCONTRACT_H
+#define LLVM_CLANG_AST_EXPRCONTRACT_H
+
+#include "clang/AST/Decl.h"
+#include "clang/AST/Expr.h"
+#include "clang/AST/Type.h"
+
+namespace clang {
+
+// Forward declaration for serialization friend access.
+class ASTStmtReader;
+
+/// ForallExpr - Represents a bounded universal quantifier:
+///   forall(binder, lo, hi, body)
+/// means: for all binder in [lo, hi), body holds.
+class ForallExpr : public Expr {
+  friend class ASTStmtReader;
+  SourceLocation ForallLoc;
+  SourceLocation LParenLoc;
+  SourceLocation RParenLoc;
+  VarDecl *BoundVar;
+  enum { LO, HI, BODY, NUM_SUBEXPRS };
+  Stmt *SubExprs[NUM_SUBEXPRS];
+
+public:
+  ForallExpr(SourceLocation ForallLoc, SourceLocation LParenLoc,
+             SourceLocation RParenLoc, VarDecl *BoundVar, Expr *Lo, Expr *Hi,
+             Expr *Body, QualType BoolTy)
+      : Expr(ForallExprClass, BoolTy, VK_PRValue, OK_Ordinary),
+        ForallLoc(ForallLoc), LParenLoc(LParenLoc), RParenLoc(RParenLoc),
+        BoundVar(BoundVar) {
+    SubExprs[LO] = Lo;
+    SubExprs[HI] = Hi;
+    SubExprs[BODY] = Body;
+    setDependence(ExprDependence::None);
+  }
+
+  explicit ForallExpr(EmptyShell Empty) : Expr(ForallExprClass, Empty) {}
+
+  VarDecl *getBoundVar() const { return BoundVar; }
+  Expr *getLo() const { return cast<Expr>(SubExprs[LO]); }
+  Expr *getHi() const { return cast<Expr>(SubExprs[HI]); }
+  Expr *getBody() const { return cast<Expr>(SubExprs[BODY]); }
+
+  SourceLocation getForallLoc() const { return ForallLoc; }
+  SourceLocation getLParenLoc() const { return LParenLoc; }
+  SourceLocation getRParenLoc() const { return RParenLoc; }
+  SourceLocation getBeginLoc() const LLVM_READONLY { return ForallLoc; }
+  SourceLocation getEndLoc() const LLVM_READONLY { return RParenLoc; }
+
+  static bool classof(const Stmt *T) {
+    return T->getStmtClass() == ForallExprClass;
+  }
+
+  child_range children() {
+    return child_range(&SubExprs[0], &SubExprs[NUM_SUBEXPRS]);
+  }
+  const_child_range children() const {
+    return const_child_range(&SubExprs[0], &SubExprs[NUM_SUBEXPRS]);
+  }
+};
+
+/// ExistsExpr - Represents a bounded existential quantifier:
+///   exists(binder, lo, hi, body)
+/// means: there exists binder in [lo, hi) such that body holds.
+class ExistsExpr : public Expr {
+  friend class ASTStmtReader;
+  SourceLocation ExistsLoc;
+  SourceLocation LParenLoc;
+  SourceLocation RParenLoc;
+  VarDecl *BoundVar;
+  enum { LO, HI, BODY, NUM_SUBEXPRS };
+  Stmt *SubExprs[NUM_SUBEXPRS];
+
+public:
+  ExistsExpr(SourceLocation ExistsLoc, SourceLocation LParenLoc,
+             SourceLocation RParenLoc, VarDecl *BoundVar, Expr *Lo, Expr *Hi,
+             Expr *Body, QualType BoolTy)
+      : Expr(ExistsExprClass, BoolTy, VK_PRValue, OK_Ordinary),
+        ExistsLoc(ExistsLoc), LParenLoc(LParenLoc), RParenLoc(RParenLoc),
+        BoundVar(BoundVar) {
+    SubExprs[LO] = Lo;
+    SubExprs[HI] = Hi;
+    SubExprs[BODY] = Body;
+    setDependence(ExprDependence::None);
+  }
+
+  explicit ExistsExpr(EmptyShell Empty) : Expr(ExistsExprClass, Empty) {}
+
+  VarDecl *getBoundVar() const { return BoundVar; }
+  Expr *getLo() const { return cast<Expr>(SubExprs[LO]); }
+  Expr *getHi() const { return cast<Expr>(SubExprs[HI]); }
+  Expr *getBody() const { return cast<Expr>(SubExprs[BODY]); }
+
+  SourceLocation getExistsLoc() const { return ExistsLoc; }
+  SourceLocation getLParenLoc() const { return LParenLoc; }
+  SourceLocation getRParenLoc() const { return RParenLoc; }
+  SourceLocation getBeginLoc() const LLVM_READONLY { return ExistsLoc; }
+  SourceLocation getEndLoc() const LLVM_READONLY { return RParenLoc; }
+
+  static bool classof(const Stmt *T) {
+    return T->getStmtClass() == ExistsExprClass;
+  }
+
+  child_range children() {
+    return child_range(&SubExprs[0], &SubExprs[NUM_SUBEXPRS]);
+  }
+  const_child_range children() const {
+    return const_child_range(&SubExprs[0], &SubExprs[NUM_SUBEXPRS]);
+  }
+};
+
+/// OldExpr - Represents old(expr), referring to the value of expr at
+/// function entry. Only valid in postconditions and proof function bodies.
+class OldExpr : public Expr {
+  friend class ASTStmtReader;
+  SourceLocation OldLoc;
+  SourceLocation LParenLoc;
+  SourceLocation RParenLoc;
+  Stmt *Inner;
+
+public:
+  OldExpr(SourceLocation OldLoc, SourceLocation LParenLoc,
+          SourceLocation RParenLoc, Expr *Inner)
+      : Expr(OldExprClass, Inner->getType(), VK_PRValue, OK_Ordinary),
+        OldLoc(OldLoc), LParenLoc(LParenLoc), RParenLoc(RParenLoc),
+        Inner(Inner) {
+    setDependence(ExprDependence::None);
+  }
+
+  explicit OldExpr(EmptyShell Empty) : Expr(OldExprClass, Empty) {}
+
+  Expr *getInner() const { return cast<Expr>(Inner); }
+
+  SourceLocation getOldLoc() const { return OldLoc; }
+  SourceLocation getLParenLoc() const { return LParenLoc; }
+  SourceLocation getRParenLoc() const { return RParenLoc; }
+  SourceLocation getBeginLoc() const LLVM_READONLY { return OldLoc; }
+  SourceLocation getEndLoc() const LLVM_READONLY { return RParenLoc; }
+
+  static bool classof(const Stmt *T) {
+    return T->getStmtClass() == OldExprClass;
+  }
+
+  child_range children() { return child_range(&Inner, &Inner + 1); }
+  const_child_range children() const {
+    return const_child_range(&Inner, &Inner + 1);
+  }
+};
+
+/// ResultExpr - Represents 'result' in postconditions, referring to the
+/// return value of the enclosing function.
+class ResultExpr : public Expr {
+  friend class ASTStmtReader;
+  SourceLocation ResultLoc;
+
+public:
+  ResultExpr(SourceLocation ResultLoc, QualType ReturnType)
+      : Expr(ResultExprClass, ReturnType, VK_PRValue, OK_Ordinary),
+        ResultLoc(ResultLoc) {
+    setDependence(ExprDependence::None);
+  }
+
+  explicit ResultExpr(EmptyShell Empty) : Expr(ResultExprClass, Empty) {}
+
+  SourceLocation getResultLoc() const { return ResultLoc; }
+  SourceLocation getBeginLoc() const LLVM_READONLY { return ResultLoc; }
+  SourceLocation getEndLoc() const LLVM_READONLY { return ResultLoc; }
+
+  static bool classof(const Stmt *T) {
+    return T->getStmtClass() == ResultExprClass;
+  }
+
+  child_range children() {
+    return child_range(child_iterator(), child_iterator());
+  }
+  const_child_range children() const {
+    return const_child_range(const_child_iterator(), const_child_iterator());
+  }
+};
+
+} // namespace clang
+
+#endif // LLVM_CLANG_AST_EXPRCONTRACT_H
diff --git a/clang/include/clang/AST/RecursiveASTVisitor.h b/clang/include/clang/AST/RecursiveASTVisitor.h
index ddec2c52fb..e013f260a8 100644
--- a/clang/include/clang/AST/RecursiveASTVisitor.h
+++ b/clang/include/clang/AST/RecursiveASTVisitor.h
@@ -27,6 +27,7 @@
 #include "clang/AST/Expr.h"
 #include "clang/AST/ExprCXX.h"
 #include "clang/AST/ExprConcepts.h"
+#include "clang/AST/ExprContract.h"
 #include "clang/AST/ExprObjC.h"
 #include "clang/AST/ExprOpenMP.h"
 #include "clang/AST/LambdaCapture.h"
@@ -35,6 +36,7 @@
 #include "clang/AST/OpenMPClause.h"
 #include "clang/AST/Stmt.h"
 #include "clang/AST/StmtCXX.h"
+#include "clang/AST/StmtContract.h"
 #include "clang/AST/StmtObjC.h"
 #include "clang/AST/StmtOpenACC.h"
 #include "clang/AST/StmtOpenMP.h"
@@ -2596,6 +2598,14 @@ DEF_TRAVERSE_STMT(ReturnStmt, {})
 DEF_TRAVERSE_STMT(SwitchStmt, {})
 DEF_TRAVERSE_STMT(WhileStmt, {})
 
+// CppVerify contract nodes.
+DEF_TRAVERSE_STMT(ContractAssertStmt, {})
+DEF_TRAVERSE_STMT(ExistsExpr, { TRY_TO(TraverseDecl(S->getBoundVar())); })
+DEF_TRAVERSE_STMT(ForallExpr, { TRY_TO(TraverseDecl(S->getBoundVar())); })
+DEF_TRAVERSE_STMT(GhostBlockStmt, {})
+DEF_TRAVERSE_STMT(OldExpr, {})
+DEF_TRAVERSE_STMT(ResultExpr, {})
+
 DEF_TRAVERSE_STMT(ConstantExpr, {})
 
 DEF_TRAVERSE_STMT(CXXDependentScopeMemberExpr, {
diff --git a/clang/include/clang/AST/StmtContract.h b/clang/include/clang/AST/StmtContract.h
new file mode 100644
index 0000000000..481b59b8e4
--- /dev/null
+++ b/clang/include/clang/AST/StmtContract.h
@@ -0,0 +1,98 @@
+//===--- StmtContract.h - Contract statement AST nodes ----------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// This file defines AST nodes for CppVerify contract statements:
+//   ContractAssertStmt, GhostBlockStmt
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_AST_STMTCONTRACT_H
+#define LLVM_CLANG_AST_STMTCONTRACT_H
+
+#include "clang/AST/Expr.h"
+#include "clang/AST/Stmt.h"
+
+namespace clang {
+
+// Forward declaration for serialization friend access.
+class ASTStmtReader;
+
+/// ContractAssertStmt - Represents contract_assert(expr);
+/// Generates a verification condition, not a runtime check.
+class ContractAssertStmt : public Stmt {
+  friend class ASTStmtReader;
+  SourceLocation ContractAssertLoc;
+  SourceLocation LParenLoc;
+  SourceLocation RParenLoc;
+  Stmt *Cond;
+
+public:
+  ContractAssertStmt(SourceLocation ContractAssertLoc,
+                     SourceLocation LParenLoc, SourceLocation RParenLoc,
+                     Expr *Cond)
+      : Stmt(ContractAssertStmtClass),
+        ContractAssertLoc(ContractAssertLoc), LParenLoc(LParenLoc),
+        RParenLoc(RParenLoc), Cond(Cond) {}
+
+  explicit ContractAssertStmt(EmptyShell Empty)
+      : Stmt(ContractAssertStmtClass), Cond(nullptr) {}
+
+  Expr *getCond() const { return cast<Expr>(Cond); }
+
+  SourceLocation getContractAssertLoc() const { return ContractAssertLoc; }
+  SourceLocation getLParenLoc() const { return LParenLoc; }
+  SourceLocation getRParenLoc() const { return RParenLoc; }
+  SourceLocation getBeginLoc() const LLVM_READONLY { return ContractAssertLoc; }
+  SourceLocation getEndLoc() const LLVM_READONLY { return RParenLoc; }
+
+  static bool classof(const Stmt *T) {
+    return T->getStmtClass() == ContractAssertStmtClass;
+  }
+
+  child_range children() { return child_range(&Cond, &Cond + 1); }
+  const_child_range children() const {
+    return const_child_range(&Cond, &Cond + 1);
+  }
+};
+
+/// GhostBlockStmt - Represents ghost { ... }
+/// Code inside a ghost block exists only for verification purposes.
+/// CodeGen skips it entirely.
+class GhostBlockStmt : public Stmt {
+  friend class ASTStmtReader;
+  SourceLocation GhostLoc;
+  Stmt *Body;
+
+public:
+  GhostBlockStmt(SourceLocation GhostLoc, Stmt *Body)
+      : Stmt(GhostBlockStmtClass), GhostLoc(GhostLoc), Body(Body) {}
+
+  explicit GhostBlockStmt(EmptyShell Empty)
+      : Stmt(GhostBlockStmtClass), Body(nullptr) {}
+
+  Stmt *getBody() const { return Body; }
+
+  SourceLocation getGhostLoc() const { return GhostLoc; }
+  SourceLocation getBeginLoc() const LLVM_READONLY { return GhostLoc; }
+  SourceLocation getEndLoc() const LLVM_READONLY {
+    return Body->getEndLoc();
+  }
+
+  static bool classof(const Stmt *T) {
+    return T->getStmtClass() == GhostBlockStmtClass;
+  }
+
+  child_range children() { return child_range(&Body, &Body + 1); }
+  const_child_range children() const {
+    return const_child_range(&Body, &Body + 1);
+  }
+};
+
+} // namespace clang
+
+#endif // LLVM_CLANG_AST_STMTCONTRACT_H
diff --git a/clang/include/clang/AST/StmtVisitor.h b/clang/include/clang/AST/StmtVisitor.h
index 8b7b728dea..31d8ed7a46 100644
--- a/clang/include/clang/AST/StmtVisitor.h
+++ b/clang/include/clang/AST/StmtVisitor.h
@@ -15,10 +15,12 @@
 
 #include "clang/AST/ExprCXX.h"
 #include "clang/AST/ExprConcepts.h"
+#include "clang/AST/ExprContract.h"
 #include "clang/AST/ExprObjC.h"
 #include "clang/AST/ExprOpenMP.h"
 #include "clang/AST/Stmt.h"
 #include "clang/AST/StmtCXX.h"
+#include "clang/AST/StmtContract.h"
 #include "clang/AST/StmtObjC.h"
 #include "clang/AST/StmtOpenACC.h"
 #include "clang/AST/StmtOpenMP.h"
diff --git a/clang/include/clang/Basic/DiagnosticParseKinds.td b/clang/include/clang/Basic/DiagnosticParseKinds.td
index 63fc4bf2e1..fb882b1d65 100644
--- a/clang/include/clang/Basic/DiagnosticParseKinds.td
+++ b/clang/include/clang/Basic/DiagnosticParseKinds.td
@@ -1883,4 +1883,20 @@ def err_hlsl_number_literal_underflow : Error<
   "float literal has a magnitude that is too small to be represented as a float type">;
 def err_hlsl_rootsig_non_zero_flag : Error<"flag value is neither a literal 0 nor a named value">;
 
+// CppVerify contract parsing diagnostics
+def err_contract_expected_lparen : Error<
+  "expected '(' after '%0'">;
+def err_contract_expected_comma : Error<
+  "expected ',' in %0 expression">;
+def err_contract_expected_rparen : Error<
+  "expected ')' after %0 expression">;
+def err_contract_expected_semi : Error<
+  "expected ';' after contract_assert">;
+def err_contract_expected_body : Error<
+  "expected '{' after ghost">;
+def err_result_outside_postcondition : Error<
+  "'result' can only be used in postconditions">;
+def err_old_outside_postcondition : Error<
+  "'old' can only be used in postconditions">;
+
 } // end of Parser diagnostics
diff --git a/clang/include/clang/Basic/DiagnosticSemaKinds.td b/clang/include/clang/Basic/DiagnosticSemaKinds.td
index 43315a6f7b..55b59e6f85 100644
--- a/clang/include/clang/Basic/DiagnosticSemaKinds.td
+++ b/clang/include/clang/Basic/DiagnosticSemaKinds.td
@@ -13862,4 +13862,20 @@ def err_cuda_device_kernel_launch_not_supported
 def err_cuda_device_kernel_launch_require_rdc
     : Error<"kernel launch from __device__ or __global__ function requires "
             "relocatable device code (i.e. requires -fgpu-rdc)">;
+// CppVerify contract semantic diagnostics
+def err_contract_expr_not_bool : Error<
+  "contract expression must be convertible to bool">;
+def err_contract_result_not_in_post : Error<
+  "'result' can only appear in a postcondition">;
+def err_contract_old_not_in_post : Error<
+  "'old' can only appear in a postcondition">;
+def err_contract_quantifier_bound_not_int : Error<
+  "quantifier bound must have integer type">;
+def err_contract_quantifier_body_not_bool : Error<
+  "quantifier body must have boolean type">;
+def err_proof_fn_must_return_void : Error<
+  "proof function must return void">;
+def err_contract_decreases_not_int : Error<
+  "decreases expression must have integer type">;
+
 } // end of sema component.
diff --git a/clang/include/clang/Basic/StmtNodes.td b/clang/include/clang/Basic/StmtNodes.td
index b08b9fe3b9..66488fca7e 100644
--- a/clang/include/clang/Basic/StmtNodes.td
+++ b/clang/include/clang/Basic/StmtNodes.td
@@ -337,3 +337,11 @@ def OpenACCAsteriskSizeExpr : StmtNode<Expr>;
 
 // HLSL Constructs.
 def HLSLOutArgExpr : StmtNode<Expr>;
+
+// CppVerify Contract Nodes.
+def ContractAssertStmt : StmtNode<Stmt>;
+def GhostBlockStmt : StmtNode<Stmt>;
+def ForallExpr : StmtNode<Expr>;
+def ExistsExpr : StmtNode<Expr>;
+def OldExpr : StmtNode<Expr>;
+def ResultExpr : StmtNode<Expr>;
diff --git a/clang/include/clang/Parse/Parser.h b/clang/include/clang/Parse/Parser.h
index f7e7b0ec51..0204256e41 100644
--- a/clang/include/clang/Parse/Parser.h
+++ b/clang/include/clang/Parse/Parser.h
@@ -7449,6 +7449,39 @@ class Parser : public CodeCompletionHandler {
   StmtResult ParseForStatement(SourceLocation *TrailingElseLoc,
                                LabelDecl *PrecedingLabel);
 
+  //===--------------------------------------------------------------------===//
+  // CppVerify Contract Parsing
+
+  /// Parse invariant/decreases clauses after a while/for condition.
+  /// Called from ParseWhileStatement/ParseForStatement.
+  void ParseLoopContractClauses(SmallVectorImpl<Expr *> &Invariants,
+                                Expr *&Decreases);
+
+  /// Parse ghost { ... } block.
+  StmtResult ParseGhostBlock();
+
+  /// Parse contract_assert(expr);
+  StmtResult ParseContractAssert();
+
+  /// Parse forall(binder, lo, hi, body) or exists(binder, lo, hi, body).
+  ExprResult ParseQuantifierExpr();
+
+  /// Parse old(expr).
+  ExprResult ParseOldExpr();
+
+  /// Parse 'result' keyword in postconditions.
+  ExprResult ParseResultExpr();
+
+  /// True when we are currently parsing a postcondition expression.
+  bool InContractPostcondition = false;
+
+  /// The return type of the function whose contracts we are currently
+  /// parsing, extracted from the DeclSpec before the FunctionDecl exists.
+  QualType CurrentContractReturnType;
+
+  /// The FunctionDecl whose contracts we are currently parsing (if any).
+  Decl *CurrentContractFunction = nullptr;
+
   /// ParseGotoStatement
   /// \verbatim
   ///       jump-statement:
diff --git a/clang/include/clang/Sema/DeclSpec.h b/clang/include/clang/Sema/DeclSpec.h
index 43a48c92fc..e71d8dd88a 100644
--- a/clang/include/clang/Sema/DeclSpec.h
+++ b/clang/include/clang/Sema/DeclSpec.h
@@ -368,6 +368,11 @@ class DeclSpec {
   unsigned FS_virtual_specified : 1;
   LLVM_PREFERRED_TYPE(bool)
   unsigned FS_noreturn_specified : 1;
+  // CppVerify: spec/proof function qualifiers.
+  LLVM_PREFERRED_TYPE(bool)
+  unsigned FS_spec_specified : 1;
+  LLVM_PREFERRED_TYPE(bool)
+  unsigned FS_proof_specified : 1;
 
   // friend-specifier
   LLVM_PREFERRED_TYPE(bool)
@@ -462,7 +467,8 @@ class DeclSpec {
         TypeSpecPipe(false), TypeSpecSat(false), ConstrainedAuto(false),
         TypeQualifiers(TQ_unspecified), FS_inline_specified(false),
         FS_forceinline_specified(false), FS_virtual_specified(false),
-        FS_noreturn_specified(false), FriendSpecifiedFirst(false),
+        FS_noreturn_specified(false), FS_spec_specified(false),
+        FS_proof_specified(false), FriendSpecifiedFirst(false),
         ConstexprSpecifier(
             static_cast<unsigned>(ConstexprSpecKind::Unspecified)),
         Attrs(attrFactory), writtenBS(), ObjCQualifiers(nullptr) {}
@@ -631,6 +637,12 @@ class DeclSpec {
   bool isNoreturnSpecified() const { return FS_noreturn_specified; }
   SourceLocation getNoreturnSpecLoc() const { return FS_noreturnLoc; }
 
+  // CppVerify: spec/proof function qualifiers.
+  bool isSpecFunctionSpecified() const { return FS_spec_specified; }
+  bool isProofFunctionSpecified() const { return FS_proof_specified; }
+  void setSpecFunctionSpec() { FS_spec_specified = true; }
+  void setProofFunctionSpec() { FS_proof_specified = true; }
+
   void ClearFunctionSpecs() {
     FS_inline_specified = false;
     FS_inlineLoc = SourceLocation();
diff --git a/clang/include/clang/Sema/Sema.h b/clang/include/clang/Sema/Sema.h
index d68ed7c75b..5351b2b8f3 100644
--- a/clang/include/clang/Sema/Sema.h
+++ b/clang/include/clang/Sema/Sema.h
@@ -10275,6 +10275,12 @@ class Sema final : public SemaBase {
   /// of the expression From to bool (C++0x [conv]p3).
   ExprResult PerformContextuallyConvertToBool(Expr *From);
 
+  /// ActOnContractCondition - Semantic action for a contract condition
+  /// (pre/post/invariant/contract_assert). Verifies the expression is
+  /// contextually convertible to bool. Called from the parser after parsing
+  /// each contract condition expression. (SemaContract.cpp)
+  ExprResult ActOnContractCondition(ExprResult E);
+
   /// PerformContextuallyConvertToObjCPointer - Perform a contextual
   /// conversion of the expression From to an Objective-C pointer type.
   /// Returns a valid but null ExprResult if no conversion sequence exists.
diff --git a/clang/include/clang/Serialization/ASTBitCodes.h b/clang/include/clang/Serialization/ASTBitCodes.h
index 5a86d540e5..45e3d7bb7b 100644
--- a/clang/include/clang/Serialization/ASTBitCodes.h
+++ b/clang/include/clang/Serialization/ASTBitCodes.h
@@ -2065,6 +2065,14 @@ enum StmtCode {
   EXPR_HLSL_OUT_ARG,
 
   STMT_DEFER,
+
+  // CppVerify contract constructs
+  STMT_CONTRACT_ASSERT,
+  STMT_GHOST_BLOCK,
+  EXPR_FORALL,
+  EXPR_EXISTS,
+  EXPR_OLD,
+  EXPR_RESULT,
 };
 
 /// The kinds of designators that can occur in a
diff --git a/clang/lib/AST/ASTContext.cpp b/clang/lib/AST/ASTContext.cpp
index 100e37c131..2e01c77aea 100644
--- a/clang/lib/AST/ASTContext.cpp
+++ b/clang/lib/AST/ASTContext.cpp
@@ -3092,6 +3092,33 @@ void ASTContext::setBlockVarCopyInit(const VarDecl*VD, Expr *CopyExpr,
   BlockVarCopyInits[VD].setExprAndFlag(CopyExpr, CanThrow);
 }
 
+// CppVerify contract side table accessors.
+FunctionContractInfo &
+ASTContext::getOrCreateFunctionContract(const FunctionDecl *FD) {
+  auto &Info = FunctionContracts[FD];
+  if (!Info)
+    Info = new (*this) FunctionContractInfo();
+  return *Info;
+}
+
+const FunctionContractInfo *
+ASTContext::getFunctionContract(const FunctionDecl *FD) const {
+  auto I = FunctionContracts.find(FD);
+  return I != FunctionContracts.end() ? I->second : nullptr;
+}
+
+LoopContractInfo &ASTContext::getOrCreateLoopContract(const Stmt *S) {
+  auto &Info = LoopContracts[S];
+  if (!Info)
+    Info = new (*this) LoopContractInfo();
+  return *Info;
+}
+
+const LoopContractInfo *ASTContext::getLoopContract(const Stmt *S) const {
+  auto I = LoopContracts.find(S);
+  return I != LoopContracts.end() ? I->second : nullptr;
+}
+
 TypeSourceInfo *ASTContext::CreateTypeSourceInfo(QualType T,
                                                  unsigned DataSize) const {
   if (!DataSize)
diff --git a/clang/lib/AST/ASTDumper.cpp b/clang/lib/AST/ASTDumper.cpp
index 8e651a0a68..c854058ccb 100644
--- a/clang/lib/AST/ASTDumper.cpp
+++ b/clang/lib/AST/ASTDumper.cpp
@@ -19,6 +19,9 @@
 #include "clang/Basic/SourceManager.h"
 #include "llvm/Support/raw_ostream.h"
 
+// CppVerify: contract side-table dumping support.
+// FunctionContractInfo/LoopContractInfo are defined in ASTContext.h.
+
 using namespace clang;
 using namespace clang::comments;
 
@@ -172,6 +175,61 @@ void ASTDumper::VisitVarTemplateDecl(const VarTemplateDecl *D) {
   dumpTemplateDecl(D, false);
 }
 
+//===----------------------------------------------------------------------===//
+// CppVerify: contract side-table dump methods
+//===----------------------------------------------------------------------===//
+
+void ASTDumper::VisitFunctionDecl(const FunctionDecl *D) {
+  // Delegate standard traversal (params, body, etc.) to the base.
+  ASTNodeTraverser<ASTDumper, TextNodeDumper>::VisitFunctionDecl(D);
+
+  // Then add contract clauses from the side table as extra children.
+  if (!Ctx)
+    return;
+  const FunctionContractInfo *FCI = Ctx->getFunctionContract(D);
+  if (!FCI)
+    return;
+  for (const Expr *E : FCI->Preconditions)
+    Visit(E, "pre");
+  for (const Expr *E : FCI->Postconditions)
+    Visit(E, "post");
+  if (FCI->Decreases)
+    Visit(FCI->Decreases, "decreases");
+}
+
+void ASTDumper::VisitWhileStmt(const WhileStmt *S) {
+  // Contract clauses are in the side table, not in S->children(), so add them.
+  if (!Ctx)
+    return;
+  const LoopContractInfo *LCI = Ctx->getLoopContract(S);
+  if (!LCI)
+    return;
+  for (const Expr *E : LCI->Invariants)
+    Visit(E, "invariant");
+  if (LCI->Decreases)
+    Visit(LCI->Decreases, "decreases");
+}
+
+// Note: VisitWhileStmt/VisitForStmt only append extra children (contract
+// side-table entries). The base ASTNodeTraverser does NOT define VisitWhileStmt
+// or VisitForStmt — it relies on the generic Stmt children() iterator for
+// those. Our overrides add contract info *after* the base traversal has already
+// enumerated the WhileStmt/ForStmt children. When no contract info exists, there
+// is nothing extra to add, so we return early; the base traversal still runs.
+
+void ASTDumper::VisitForStmt(const ForStmt *S) {
+  // Contract clauses are in the side table, not in S->children(), so add them.
+  if (!Ctx)
+    return;
+  const LoopContractInfo *LCI = Ctx->getLoopContract(S);
+  if (!LCI)
+    return;
+  for (const Expr *E : LCI->Invariants)
+    Visit(E, "invariant");
+  if (LCI->Decreases)
+    Visit(LCI->Decreases, "decreases");
+}
+
 //===----------------------------------------------------------------------===//
 // Type method implementations
 //===----------------------------------------------------------------------===//
diff --git a/clang/lib/AST/ASTStructuralEquivalence.cpp b/clang/lib/AST/ASTStructuralEquivalence.cpp
index da64c92221..88b66a1ddf 100644
--- a/clang/lib/AST/ASTStructuralEquivalence.cpp
+++ b/clang/lib/AST/ASTStructuralEquivalence.cpp
@@ -72,9 +72,11 @@
 #include "clang/AST/DeclTemplate.h"
 #include "clang/AST/ExprCXX.h"
 #include "clang/AST/ExprConcepts.h"
+#include "clang/AST/ExprContract.h"
 #include "clang/AST/ExprObjC.h"
 #include "clang/AST/ExprOpenMP.h"
 #include "clang/AST/NestedNameSpecifier.h"
+#include "clang/AST/StmtContract.h"
 #include "clang/AST/StmtObjC.h"
 #include "clang/AST/StmtOpenACC.h"
 #include "clang/AST/StmtOpenMP.h"
diff --git a/clang/lib/AST/ASTTypeTraits.cpp b/clang/lib/AST/ASTTypeTraits.cpp
index 84eb77730b..cef4e20ba7 100644
--- a/clang/lib/AST/ASTTypeTraits.cpp
+++ b/clang/lib/AST/ASTTypeTraits.cpp
@@ -17,6 +17,8 @@
 #include "clang/AST/ASTContext.h"
 #include "clang/AST/Attr.h"
 #include "clang/AST/DeclCXX.h"
+#include "clang/AST/ExprContract.h"
+#include "clang/AST/StmtContract.h"
 #include "clang/AST/DeclObjC.h"
 #include "clang/AST/NestedNameSpecifier.h"
 #include "clang/AST/OpenMPClause.h"
diff --git a/clang/lib/AST/CMakeLists.txt b/clang/lib/AST/CMakeLists.txt
index f9a5f4f0e7..62960ac632 100644
--- a/clang/lib/AST/CMakeLists.txt
+++ b/clang/lib/AST/CMakeLists.txt
@@ -61,6 +61,7 @@ add_clang_library(clangAST
   ExprClassification.cpp
   ExprConcepts.cpp
   ExprConstant.cpp
+  ExprContract.cpp
   ExprCXX.cpp
   ExprObjC.cpp
   ExternalASTMerger.cpp
@@ -119,6 +120,7 @@ add_clang_library(clangAST
   ScanfFormatString.cpp
   SelectorLocationsKind.cpp
   Stmt.cpp
+  StmtContract.cpp
   StmtCXX.cpp
   StmtIterator.cpp
   StmtObjC.cpp
diff --git a/clang/lib/AST/DynamicRecursiveASTVisitor.cpp b/clang/lib/AST/DynamicRecursiveASTVisitor.cpp
index 6d7925b437..199941a504 100644
--- a/clang/lib/AST/DynamicRecursiveASTVisitor.cpp
+++ b/clang/lib/AST/DynamicRecursiveASTVisitor.cpp
@@ -11,7 +11,9 @@
 //
 //===----------------------------------------------------------------------===//
 #include "clang/AST/DynamicRecursiveASTVisitor.h"
+#include "clang/AST/ExprContract.h"
 #include "clang/AST/RecursiveASTVisitor.h"
+#include "clang/AST/StmtContract.h"
 
 using namespace clang;
 
diff --git a/clang/lib/AST/Expr.cpp b/clang/lib/AST/Expr.cpp
index 4bb979e51b..be90be2711 100644
--- a/clang/lib/AST/Expr.cpp
+++ b/clang/lib/AST/Expr.cpp
@@ -22,7 +22,9 @@
 #include "clang/AST/DependenceFlags.h"
 #include "clang/AST/EvaluatedExprVisitor.h"
 #include "clang/AST/ExprCXX.h"
+#include "clang/AST/ExprContract.h"
 #include "clang/AST/IgnoreExpr.h"
+#include "clang/AST/StmtContract.h"
 #include "clang/AST/Mangle.h"
 #include "clang/AST/RecordLayout.h"
 #include "clang/Basic/Builtins.h"
diff --git a/clang/lib/AST/ExprClassification.cpp b/clang/lib/AST/ExprClassification.cpp
index 9995d1b411..f1f44f1404 100644
--- a/clang/lib/AST/ExprClassification.cpp
+++ b/clang/lib/AST/ExprClassification.cpp
@@ -16,7 +16,9 @@
 #include "clang/AST/DeclObjC.h"
 #include "clang/AST/DeclTemplate.h"
 #include "clang/AST/ExprCXX.h"
+#include "clang/AST/ExprContract.h"
 #include "clang/AST/ExprObjC.h"
+#include "clang/AST/StmtContract.h"
 #include "llvm/Support/ErrorHandling.h"
 
 using namespace clang;
@@ -481,6 +483,13 @@ static Cl::Kinds ClassifyInternal(ASTContext &Ctx, const Expr *E) {
     if (isa<ArrayType>(E->getType()))
       return Cl::CL_ArrayTemporary;
     return Cl::CL_ClassTemporary;
+
+  // CppVerify contract expressions — always pure rvalues.
+  case Expr::ForallExprClass:
+  case Expr::ExistsExprClass:
+  case Expr::OldExprClass:
+  case Expr::ResultExprClass:
+    return Cl::CL_PRValue;
   }
 
   llvm_unreachable("unhandled expression kind in classification");
diff --git a/clang/lib/AST/ExprConstant.cpp b/clang/lib/AST/ExprConstant.cpp
index ec7ca893fb..0c31538a6b 100644
--- a/clang/lib/AST/ExprConstant.cpp
+++ b/clang/lib/AST/ExprConstant.cpp
@@ -44,10 +44,12 @@
 #include "clang/AST/CharUnits.h"
 #include "clang/AST/CurrentSourceLocExprScope.h"
 #include "clang/AST/Expr.h"
+#include "clang/AST/ExprContract.h"
 #include "clang/AST/InferAlloc.h"
 #include "clang/AST/OSLog.h"
 #include "clang/AST/OptionalDiagnostic.h"
 #include "clang/AST/RecordLayout.h"
+#include "clang/AST/StmtContract.h"
 #include "clang/AST/StmtVisitor.h"
 #include "clang/AST/Type.h"
 #include "clang/AST/TypeLoc.h"
diff --git a/clang/lib/AST/ExprContract.cpp b/clang/lib/AST/ExprContract.cpp
new file mode 100644
index 0000000000..9ee279d3c9
--- /dev/null
+++ b/clang/lib/AST/ExprContract.cpp
@@ -0,0 +1,16 @@
+//===--- ExprContract.cpp - Contract expression AST node impl ---*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/AST/ExprContract.h"
+#include "clang/AST/ASTContext.h"
+
+using namespace clang;
+
+// All methods are inline in the header for now. This file exists so the
+// build system has a .cpp to compile and link, and for future non-inline
+// implementations (e.g., profiling, serialization).
diff --git a/clang/lib/AST/ItaniumMangle.cpp b/clang/lib/AST/ItaniumMangle.cpp
index fa28c0d444..42f892d7af 100644
--- a/clang/lib/AST/ItaniumMangle.cpp
+++ b/clang/lib/AST/ItaniumMangle.cpp
@@ -24,7 +24,9 @@
 #include "clang/AST/Expr.h"
 #include "clang/AST/ExprCXX.h"
 #include "clang/AST/ExprConcepts.h"
+#include "clang/AST/ExprContract.h"
 #include "clang/AST/ExprObjC.h"
+#include "clang/AST/StmtContract.h"
 #include "clang/AST/Mangle.h"
 #include "clang/AST/TypeLoc.h"
 #include "clang/Basic/ABI.h"
diff --git a/clang/lib/AST/Stmt.cpp b/clang/lib/AST/Stmt.cpp
index 10aacd75a6..3615573758 100644
--- a/clang/lib/AST/Stmt.cpp
+++ b/clang/lib/AST/Stmt.cpp
@@ -19,9 +19,11 @@
 #include "clang/AST/Expr.h"
 #include "clang/AST/ExprCXX.h"
 #include "clang/AST/ExprConcepts.h"
+#include "clang/AST/ExprContract.h"
 #include "clang/AST/ExprObjC.h"
 #include "clang/AST/ExprOpenMP.h"
 #include "clang/AST/StmtCXX.h"
+#include "clang/AST/StmtContract.h"
 #include "clang/AST/StmtObjC.h"
 #include "clang/AST/StmtOpenACC.h"
 #include "clang/AST/StmtOpenMP.h"
diff --git a/clang/lib/AST/StmtContract.cpp b/clang/lib/AST/StmtContract.cpp
new file mode 100644
index 0000000000..990fb0e26d
--- /dev/null
+++ b/clang/lib/AST/StmtContract.cpp
@@ -0,0 +1,14 @@
+//===--- StmtContract.cpp - Contract statement AST node impl ----*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/AST/StmtContract.h"
+
+using namespace clang;
+
+// All methods are inline in the header for now. This file exists so the
+// build system has a .cpp to compile and link.
diff --git a/clang/lib/AST/StmtPrinter.cpp b/clang/lib/AST/StmtPrinter.cpp
index 4d1ad387b8..8e16f7ad23 100644
--- a/clang/lib/AST/StmtPrinter.cpp
+++ b/clang/lib/AST/StmtPrinter.cpp
@@ -22,6 +22,7 @@
 #include "clang/AST/DeclTemplate.h"
 #include "clang/AST/Expr.h"
 #include "clang/AST/ExprCXX.h"
+#include "clang/AST/ExprContract.h"
 #include "clang/AST/ExprObjC.h"
 #include "clang/AST/ExprOpenMP.h"
 #include "clang/AST/NestedNameSpecifier.h"
@@ -29,6 +30,7 @@
 #include "clang/AST/PrettyPrinter.h"
 #include "clang/AST/Stmt.h"
 #include "clang/AST/StmtCXX.h"
+#include "clang/AST/StmtContract.h"
 #include "clang/AST/StmtObjC.h"
 #include "clang/AST/StmtOpenMP.h"
 #include "clang/AST/StmtSYCL.h"
@@ -599,6 +601,48 @@ void StmtPrinter::VisitCapturedStmt(CapturedStmt *Node) {
   PrintStmt(Node->getCapturedDecl()->getBody());
 }
 
+// CppVerify contract nodes
+void StmtPrinter::VisitContractAssertStmt(ContractAssertStmt *Node) {
+  Indent() << "contract_assert(";
+  PrintExpr(Node->getCond());
+  OS << ");\n";
+}
+
+void StmtPrinter::VisitGhostBlockStmt(GhostBlockStmt *Node) {
+  Indent() << "ghost ";
+  PrintStmt(Node->getBody());
+}
+
+void StmtPrinter::VisitForallExpr(ForallExpr *Node) {
+  OS << "forall(" << Node->getBoundVar()->getName() << ", ";
+  PrintExpr(Node->getLo());
+  OS << ", ";
+  PrintExpr(Node->getHi());
+  OS << ", ";
+  PrintExpr(Node->getBody());
+  OS << ")";
+}
+
+void StmtPrinter::VisitExistsExpr(ExistsExpr *Node) {
+  OS << "exists(" << Node->getBoundVar()->getName() << ", ";
+  PrintExpr(Node->getLo());
+  OS << ", ";
+  PrintExpr(Node->getHi());
+  OS << ", ";
+  PrintExpr(Node->getBody());
+  OS << ")";
+}
+
+void StmtPrinter::VisitOldExpr(OldExpr *Node) {
+  OS << "old(";
+  PrintExpr(Node->getInner());
+  OS << ")";
+}
+
+void StmtPrinter::VisitResultExpr(ResultExpr *) {
+  OS << "result";
+}
+
 void StmtPrinter::VisitSYCLKernelCallStmt(SYCLKernelCallStmt *Node) {
   PrintStmt(Node->getOutlinedFunctionDecl()->getBody());
 }
diff --git a/clang/lib/AST/StmtProfile.cpp b/clang/lib/AST/StmtProfile.cpp
index a626d04367..7439c3633d 100644
--- a/clang/lib/AST/StmtProfile.cpp
+++ b/clang/lib/AST/StmtProfile.cpp
@@ -16,8 +16,10 @@
 #include "clang/AST/DeclTemplate.h"
 #include "clang/AST/Expr.h"
 #include "clang/AST/ExprCXX.h"
+#include "clang/AST/ExprContract.h"
 #include "clang/AST/ExprObjC.h"
 #include "clang/AST/ExprOpenMP.h"
+#include "clang/AST/StmtContract.h"
 #include "clang/AST/ODRHash.h"
 #include "clang/AST/OpenMPClause.h"
 #include "clang/AST/StmtVisitor.h"
@@ -393,6 +395,31 @@ void StmtProfiler::VisitCapturedStmt(const CapturedStmt *S) {
   VisitStmt(S);
 }
 
+// CppVerify contract nodes
+void StmtProfiler::VisitContractAssertStmt(const ContractAssertStmt *S) {
+  VisitStmt(S);
+}
+
+void StmtProfiler::VisitGhostBlockStmt(const GhostBlockStmt *S) {
+  VisitStmt(S);
+}
+
+void StmtProfiler::VisitForallExpr(const ForallExpr *E) {
+  VisitExpr(E);
+}
+
+void StmtProfiler::VisitExistsExpr(const ExistsExpr *E) {
+  VisitExpr(E);
+}
+
+void StmtProfiler::VisitOldExpr(const OldExpr *E) {
+  VisitExpr(E);
+}
+
+void StmtProfiler::VisitResultExpr(const ResultExpr *E) {
+  VisitExpr(E);
+}
+
 void StmtProfiler::VisitSYCLKernelCallStmt(const SYCLKernelCallStmt *S) {
   VisitStmt(S);
 }
diff --git a/clang/lib/AST/TextNodeDumper.cpp b/clang/lib/AST/TextNodeDumper.cpp
index 7bc0404db1..9dcb68f40d 100644
--- a/clang/lib/AST/TextNodeDumper.cpp
+++ b/clang/lib/AST/TextNodeDumper.cpp
@@ -12,6 +12,7 @@
 
 #include "clang/AST/TextNodeDumper.h"
 #include "clang/AST/APValue.h"
+#include "clang/AST/ASTContext.h"
 #include "clang/AST/DeclFriend.h"
 #include "clang/AST/DeclOpenMP.h"
 #include "clang/AST/DeclTemplate.h"
@@ -2386,6 +2387,16 @@ void TextNodeDumper::VisitFunctionDecl(const FunctionDecl *D) {
     OS << " instantiated_from";
     dumpPointer(Instance);
   }
+
+  // CppVerify: annotate spec/proof functions from the contract side table.
+  if (Context) {
+    if (const FunctionContractInfo *FCI = Context->getFunctionContract(D)) {
+      if (FCI->IsSpec)
+        OS << " contract_spec";
+      if (FCI->IsProof)
+        OS << " contract_proof";
+    }
+  }
 }
 
 void TextNodeDumper::VisitCXXDeductionGuideDecl(
diff --git a/clang/lib/CodeGen/CGExprScalar.cpp b/clang/lib/CodeGen/CGExprScalar.cpp
index 6fd94752f5..ec69c7a336 100644
--- a/clang/lib/CodeGen/CGExprScalar.cpp
+++ b/clang/lib/CodeGen/CGExprScalar.cpp
@@ -26,6 +26,7 @@
 #include "clang/AST/Attr.h"
 #include "clang/AST/DeclObjC.h"
 #include "clang/AST/Expr.h"
+#include "clang/AST/ExprContract.h"
 #include "clang/AST/ParentMapContext.h"
 #include "clang/AST/RecordLayout.h"
 #include "clang/AST/StmtVisitor.h"
@@ -530,6 +531,23 @@ class ScalarExprEmitter
   Value *VisitGNUNullExpr(const GNUNullExpr *E) {
     return EmitNullValue(E->getType());
   }
+
+  // CppVerify: contract expressions are never emitted — they only exist
+  // in contract clauses and ghost blocks which CodeGen skips entirely.
+  // Return a poison value as a safety net.
+  Value *VisitForallExpr(const ForallExpr *) {
+    return llvm::PoisonValue::get(CGF.ConvertType(CGF.getContext().BoolTy));
+  }
+  Value *VisitExistsExpr(const ExistsExpr *) {
+    return llvm::PoisonValue::get(CGF.ConvertType(CGF.getContext().BoolTy));
+  }
+  Value *VisitOldExpr(const OldExpr *E) {
+    return llvm::PoisonValue::get(CGF.ConvertType(E->getType()));
+  }
+  Value *VisitResultExpr(const ResultExpr *E) {
+    return llvm::PoisonValue::get(CGF.ConvertType(E->getType()));
+  }
+
   Value *VisitOffsetOfExpr(OffsetOfExpr *E);
   Value *VisitUnaryExprOrTypeTraitExpr(const UnaryExprOrTypeTraitExpr *E);
   Value *VisitAddrLabelExpr(const AddrLabelExpr *E) {
diff --git a/clang/lib/CodeGen/CGStmt.cpp b/clang/lib/CodeGen/CGStmt.cpp
index c050fd41ac..d0aa79c5bb 100644
--- a/clang/lib/CodeGen/CGStmt.cpp
+++ b/clang/lib/CodeGen/CGStmt.cpp
@@ -104,6 +104,12 @@ void CodeGenFunction::EmitStmt(const Stmt *S, ArrayRef<const Attr *> Attrs) {
   case Stmt::SEHFinallyStmtClass:
   case Stmt::MSDependentExistsStmtClass:
     llvm_unreachable("invalid statement class to emit generically");
+
+  // CppVerify: ghost/contract nodes emit nothing during codegen.
+  case Stmt::GhostBlockStmtClass:
+  case Stmt::ContractAssertStmtClass:
+    break;
+
   case Stmt::NullStmtClass:
   case Stmt::CompoundStmtClass:
   case Stmt::DeclStmtClass:
diff --git a/clang/lib/Parse/ParseDecl.cpp b/clang/lib/Parse/ParseDecl.cpp
index f8c49646fc..45955cfa75 100644
--- a/clang/lib/Parse/ParseDecl.cpp
+++ b/clang/lib/Parse/ParseDecl.cpp
@@ -4152,6 +4152,24 @@ void Parser::ParseDeclarationSpecifiers(
     case tok::kw_inline:
       isInvalid = DS.setFunctionSpecInline(Loc, PrevSpec, DiagID);
       break;
+
+    // CppVerify: spec/proof function qualifiers.
+    case tok::kw_spec:
+      // Also mark inline so Clang's normal function machinery works.
+      // The dedicated FS_spec_specified bit preserves the original intent.
+      isInvalid = DS.setFunctionSpecInline(Loc, PrevSpec, DiagID);
+      if (!isInvalid) {
+        DS.SetRangeStart(Loc);
+        DS.setSpecFunctionSpec();
+      }
+      break;
+    case tok::kw_proof:
+      isInvalid = DS.setFunctionSpecInline(Loc, PrevSpec, DiagID);
+      if (!isInvalid) {
+        DS.SetRangeStart(Loc);
+        DS.setProofFunctionSpec();
+      }
+      break;
     case tok::kw_virtual:
       // C++ for OpenCL does not allow virtual function qualifier, to avoid
       // function pointers restricted in OpenCL v2.0 s6.9.a.
@@ -5860,6 +5878,10 @@ bool Parser::isDeclarationSpecifier(
   case tok::kw_explicit:
   case tok::kw__Noreturn:
 
+    // CppVerify function qualifiers
+  case tok::kw_spec:
+  case tok::kw_proof:
+
     // alignment-specifier
   case tok::kw__Alignas:
 
diff --git a/clang/lib/Parse/ParseExpr.cpp b/clang/lib/Parse/ParseExpr.cpp
index 3515343202..7b388d13ff 100644
--- a/clang/lib/Parse/ParseExpr.cpp
+++ b/clang/lib/Parse/ParseExpr.cpp
@@ -22,6 +22,7 @@
 
 #include "clang/AST/ASTContext.h"
 #include "clang/AST/Availability.h"
+#include "clang/AST/ExprContract.h"
 #include "clang/AST/ExprCXX.h"
 #include "clang/AST/LocInfoType.h"
 #include "clang/Basic/PrettyStackTrace.h"
@@ -1087,6 +1088,18 @@ Parser::ParseCastExpression(CastParseKind ParseKind, bool isAddressOfOperand,
     Res = Actions.ActOnGNUNullExpr(ConsumeToken());
     break;
 
+  // CppVerify contract expressions
+  case tok::kw_forall:
+  case tok::kw_exists:
+    return ParseQuantifierExpr();
+  case tok::kw_old:
+    return ParseOldExpr();
+  case tok::kw_result:
+    // Use break (not return) so ParsePostfixExpressionSuffix handles
+    // member access, e.g. result.x for struct return types.
+    Res = ParseResultExpr();
+    break;
+
   case tok::plusplus:      // unary-expression: '++' unary-expression [C99]
   case tok::minusminus: {  // unary-expression: '--' unary-expression [C99]
     if (NotPrimaryExpression)
@@ -3475,3 +3488,177 @@ ExprResult Parser::ParseAvailabilityCheckExpr(SourceLocation BeginLoc) {
   return Actions.ObjC().ActOnObjCAvailabilityCheckExpr(
       AvailSpecs, BeginLoc, Parens.getCloseLocation());
 }
+
+//===----------------------------------------------------------------------===//
+// CppVerify Contract Expression Parsing
+//===----------------------------------------------------------------------===//
+
+/// Parse forall(binder, lo, hi, body) or exists(binder, lo, hi, body)
+ExprResult Parser::ParseQuantifierExpr() {
+  assert((Tok.is(tok::kw_forall) || Tok.is(tok::kw_exists)) &&
+         "Expected forall or exists");
+  bool IsForall = Tok.is(tok::kw_forall);
+  SourceLocation KwLoc = ConsumeToken();
+
+  if (Tok.isNot(tok::l_paren)) {
+    Diag(Tok, diag::err_contract_expected_lparen)
+        << (IsForall ? "forall" : "exists");
+    return ExprError();
+  }
+  SourceLocation LParenLoc = ConsumeParen();
+
+  // Parse binder name (an identifier that becomes a fresh int variable).
+  if (Tok.isNot(tok::identifier)) {
+    Diag(Tok, diag::err_expected) << tok::identifier;
+    SkipUntil(tok::r_paren, StopAtSemi);
+    return ExprError();
+  }
+  IdentifierInfo *BinderII = Tok.getIdentifierInfo();
+  SourceLocation BinderLoc = ConsumeToken();
+
+  if (ExpectAndConsume(tok::comma)) {
+    SkipUntil(tok::r_paren, StopAtSemi);
+    return ExprError();
+  }
+
+  // Parse lo expression
+  ExprResult Lo = ParseAssignmentExpression();
+  if (Lo.isInvalid()) {
+    SkipUntil(tok::r_paren, StopAtSemi);
+    return ExprError();
+  }
+
+  if (ExpectAndConsume(tok::comma)) {
+    SkipUntil(tok::r_paren, StopAtSemi);
+    return ExprError();
+  }
+
+  // Parse hi expression
+  ExprResult Hi = ParseAssignmentExpression();
+  if (Hi.isInvalid()) {
+    SkipUntil(tok::r_paren, StopAtSemi);
+    return ExprError();
+  }
+
+  if (ExpectAndConsume(tok::comma)) {
+    SkipUntil(tok::r_paren, StopAtSemi);
+    return ExprError();
+  }
+
+  // Create the bound variable and push it into scope.
+  ASTContext &Ctx = Actions.getASTContext();
+  VarDecl *BoundVar = VarDecl::Create(
+      Ctx, Actions.CurContext, BinderLoc, BinderLoc, BinderII, Ctx.IntTy,
+      Ctx.getTrivialTypeSourceInfo(Ctx.IntTy, BinderLoc), SC_None);
+
+  // Push a scope for the binder and add the decl.
+  ParseScope QuantifierScope(this, Scope::DeclScope);
+  Actions.PushOnScopeChains(BoundVar, getCurScope(), /*AddToContext=*/false);
+
+  // Parse body expression
+  ExprResult Body = ParseAssignmentExpression();
+  if (Body.isInvalid()) {
+    SkipUntil(tok::r_paren, StopAtSemi);
+    return ExprError();
+  }
+
+  QuantifierScope.Exit();
+
+  // Validate bound types: lo and hi must be integer.
+  if (!Lo.get()->getType()->isIntegerType()) {
+    Diag(Lo.get()->getExprLoc(), diag::err_contract_quantifier_bound_not_int);
+    SkipUntil(tok::r_paren, StopAtSemi);
+    return ExprError();
+  }
+  if (!Hi.get()->getType()->isIntegerType()) {
+    Diag(Hi.get()->getExprLoc(), diag::err_contract_quantifier_bound_not_int);
+    SkipUntil(tok::r_paren, StopAtSemi);
+    return ExprError();
+  }
+
+  // Validate body: must be contextually convertible to bool.
+  ExprResult BodyBool = Actions.ActOnContractCondition(Body);
+  if (BodyBool.isInvalid()) {
+    SkipUntil(tok::r_paren, StopAtSemi);
+    return ExprError();
+  }
+
+  if (Tok.isNot(tok::r_paren)) {
+    Diag(Tok, diag::err_contract_expected_rparen)
+        << (IsForall ? "forall" : "exists");
+    SkipUntil(tok::r_paren, StopAtSemi);
+    return ExprError();
+  }
+  SourceLocation RParenLoc = ConsumeParen();
+
+  QualType BoolTy = Ctx.BoolTy;
+  if (IsForall)
+    return new (Ctx) ForallExpr(KwLoc, LParenLoc, RParenLoc, BoundVar,
+                                Lo.get(), Hi.get(), BodyBool.get(), BoolTy);
+  return new (Ctx) ExistsExpr(KwLoc, LParenLoc, RParenLoc, BoundVar,
+                              Lo.get(), Hi.get(), BodyBool.get(), BoolTy);
+}
+
+/// Parse old(expr)
+ExprResult Parser::ParseOldExpr() {
+  assert(Tok.is(tok::kw_old) && "Expected 'old'");
+  SourceLocation OldLoc = ConsumeToken();
+
+  // 'old' is only valid in postconditions.
+  // TODO: also allow in proof function bodies once InProofFunctionBody is tracked.
+  if (!InContractPostcondition) {
+    Diag(OldLoc, diag::err_old_outside_postcondition);
+    return ExprError();
+  }
+
+  if (Tok.isNot(tok::l_paren)) {
+    Diag(Tok, diag::err_contract_expected_lparen) << "old";
+    return ExprError();
+  }
+  SourceLocation LParenLoc = ConsumeParen();
+
+  ExprResult Inner = ParseExpression();
+  if (Inner.isInvalid()) {
+    SkipUntil(tok::r_paren, StopAtSemi);
+    return ExprError();
+  }
+
+  if (Tok.isNot(tok::r_paren)) {
+    Diag(Tok, diag::err_contract_expected_rparen) << "old";
+    SkipUntil(tok::r_paren, StopAtSemi);
+    return ExprError();
+  }
+  SourceLocation RParenLoc = ConsumeParen();
+
+  ASTContext &Ctx = Actions.getASTContext();
+  return new (Ctx) OldExpr(OldLoc, LParenLoc, RParenLoc, Inner.get());
+}
+
+/// Parse 'result' keyword
+ExprResult Parser::ParseResultExpr() {
+  assert(Tok.is(tok::kw_result) && "Expected 'result'");
+  SourceLocation ResultLoc = ConsumeToken();
+
+  // 'result' is only valid in postconditions.
+  if (!InContractPostcondition) {
+    Diag(ResultLoc, diag::err_result_outside_postcondition);
+    return ExprError();
+  }
+
+  // Use the return type computed from the full Declarator before contract
+  // parsing. CurrentContractReturnType is set via GetTypeForDeclarator in
+  // ParseFunctionDefinition, so it reflects the true return type including
+  // pointers, references, typedefs, etc.
+  QualType RetTy = CurrentContractReturnType;
+  if (RetTy.isNull()) {
+    // Fallback: try the FunctionDecl if available (e.g. from a previous pass).
+    if (CurrentContractFunction)
+      if (auto *FD = dyn_cast<FunctionDecl>(CurrentContractFunction))
+        RetTy = FD->getReturnType();
+  }
+  if (RetTy.isNull())
+    RetTy = Actions.getASTContext().IntTy; // last-resort fallback
+
+  ASTContext &Ctx = Actions.getASTContext();
+  return new (Ctx) ResultExpr(ResultLoc, RetTy);
+}
diff --git a/clang/lib/Parse/ParseStmt.cpp b/clang/lib/Parse/ParseStmt.cpp
index 260f812636..3f2f6f72cc 100644
--- a/clang/lib/Parse/ParseStmt.cpp
+++ b/clang/lib/Parse/ParseStmt.cpp
@@ -12,6 +12,7 @@
 //===----------------------------------------------------------------------===//
 
 #include "clang/AST/PrettyDeclStackTrace.h"
+#include "clang/AST/StmtContract.h"
 #include "clang/Basic/Attributes.h"
 #include "clang/Basic/PrettyStackTrace.h"
 #include "clang/Basic/TargetInfo.h"
@@ -284,6 +285,14 @@ StmtResult Parser::ParseStatementOrDeclarationAfterAttributes(
   case tok::kw_switch:              // C99 6.8.4.2: switch-statement
     return ParseSwitchStatement(TrailingElseLoc, PrecedingLabel);
 
+  // CppVerify contract statements
+  case tok::kw_ghost:
+    return ParseGhostBlock();
+  case tok::kw_contract_assert:
+    Res = ParseContractAssert();
+    SemiError = "contract_assert";
+    break;
+
   case tok::kw_while:               // C99 6.8.5.1: while-statement
     return ParseWhileStatement(TrailingElseLoc, PrecedingLabel);
   case tok::kw_do:                  // C99 6.8.5.2: do-statement
@@ -1750,6 +1759,12 @@ StmtResult Parser::ParseWhileStatement(SourceLocation *TrailingElseLoc,
                                 Sema::ConditionKind::Boolean, LParen, RParen))
     return StmtError();
 
+  // CppVerify: parse loop contract clauses (invariant/decreases) if present.
+  SmallVector<Expr *, 2> Invariants;
+  Expr *LoopDecreases = nullptr;
+  if (getLangOpts().VerifyContracts)
+    ParseLoopContractClauses(Invariants, LoopDecreases);
+
   // OpenACC Restricts a while-loop inside of certain construct/clause
   // combinations, so diagnose that here in OpenACC mode.
   SemaOpenACC::LoopInConstructRAII LCR{getActions().OpenACC()};
@@ -1783,7 +1798,17 @@ StmtResult Parser::ParseWhileStatement(SourceLocation *TrailingElseLoc,
   if (Cond.isInvalid() || Body.isInvalid())
     return StmtError();
 
-  return Actions.ActOnWhileStmt(WhileLoc, LParen, Cond, RParen, Body.get());
+  StmtResult Result =
+      Actions.ActOnWhileStmt(WhileLoc, LParen, Cond, RParen, Body.get());
+
+  // Store loop contracts in ASTContext side table.
+  if (Result.isUsable() && (!Invariants.empty() || LoopDecreases)) {
+    LoopContractInfo &LCI =
+        Actions.getASTContext().getOrCreateLoopContract(Result.get());
+    LCI.Invariants = std::move(Invariants);
+    LCI.Decreases = LoopDecreases;
+  }
+  return Result;
 }
 
 StmtResult Parser::ParseDoStatement(LabelDecl *PrecedingLabel) {
@@ -2176,6 +2201,12 @@ StmtResult Parser::ParseForStatement(SourceLocation *TrailingElseLoc,
   // Match the ')'.
   T.consumeClose();
 
+  // CppVerify: parse loop contract clauses (invariant/decreases) if present.
+  SmallVector<Expr *, 2> ForInvariants;
+  Expr *ForDecreases = nullptr;
+  if (getLangOpts().VerifyContracts)
+    ParseLoopContractClauses(ForInvariants, ForDecreases);
+
   // C++ Coroutines [stmt.iter]:
   //   'co_await' can only be used for a range-based for statement.
   if (CoawaitLoc.isValid() && !ForRangeInfo.ParsedForRangeDecl()) {
@@ -2271,9 +2302,18 @@ StmtResult Parser::ParseForStatement(SourceLocation *TrailingElseLoc,
   if (ForRangeInfo.ParsedForRangeDecl())
     return Actions.FinishCXXForRangeStmt(ForRangeStmt.get(), Body.get());
 
-  return Actions.ActOnForStmt(ForLoc, T.getOpenLocation(), FirstPart.get(),
-                              SecondPart, ThirdPart, T.getCloseLocation(),
-                              Body.get());
+  StmtResult ForResult = Actions.ActOnForStmt(
+      ForLoc, T.getOpenLocation(), FirstPart.get(), SecondPart, ThirdPart,
+      T.getCloseLocation(), Body.get());
+
+  // Store loop contracts in ASTContext side table.
+  if (ForResult.isUsable() && (!ForInvariants.empty() || ForDecreases)) {
+    LoopContractInfo &LCI =
+        Actions.getASTContext().getOrCreateLoopContract(ForResult.get());
+    LCI.Invariants = std::move(ForInvariants);
+    LCI.Decreases = ForDecreases;
+  }
+  return ForResult;
 }
 
 StmtResult Parser::ParseGotoStatement() {
@@ -2706,3 +2746,111 @@ void Parser::ParseMicrosoftIfExistsStatement(StmtVector &Stmts) {
   }
   Braces.consumeClose();
 }
+
+//===----------------------------------------------------------------------===//
+// CppVerify Contract Statement Parsing
+//===----------------------------------------------------------------------===//
+
+/// Parse loop contract clauses: invariant(expr) and decreases(expr)
+/// These appear after the while/for condition ')' and before the body '{'.
+void Parser::ParseLoopContractClauses(SmallVectorImpl<Expr *> &Invariants,
+                                      Expr *&Decreases) {
+  while (Tok.is(tok::kw_invariant) || Tok.is(tok::kw_decreases)) {
+    bool IsInvariant = Tok.is(tok::kw_invariant);
+    ConsumeToken();
+
+    if (Tok.isNot(tok::l_paren)) {
+      Diag(Tok, diag::err_contract_expected_lparen)
+          << (IsInvariant ? "invariant" : "decreases");
+      return;
+    }
+    ConsumeParen();
+
+    ExprResult E = ParseExpression();
+    if (E.isInvalid()) {
+      SkipUntil(tok::r_paren, StopAtSemi);
+      return;
+    }
+
+    // Invariants must be bool; decreases is an integer measure.
+    if (IsInvariant) {
+      E = Actions.ActOnContractCondition(E);
+      if (E.isInvalid()) {
+        SkipUntil(tok::r_paren, StopAtSemi);
+        return;
+      }
+    } else {
+      // decreases: validate integer type.
+      if (!E.get()->getType()->isIntegerType()) {
+        Diag(E.get()->getExprLoc(),
+             diag::err_contract_decreases_not_int);
+        SkipUntil(tok::r_paren, StopAtSemi);
+        return;
+      }
+    }
+
+    if (Tok.isNot(tok::r_paren)) {
+      Diag(Tok, diag::err_contract_expected_rparen)
+          << (IsInvariant ? "invariant" : "decreases");
+      SkipUntil(tok::r_paren, StopAtSemi);
+      return;
+    }
+    ConsumeParen();
+
+    if (IsInvariant)
+      Invariants.push_back(E.get());
+    else
+      Decreases = E.get();
+  }
+}
+
+/// Parse ghost { ... }
+StmtResult Parser::ParseGhostBlock() {
+  assert(Tok.is(tok::kw_ghost) && "Expected 'ghost'");
+  SourceLocation GhostLoc = ConsumeToken();
+
+  if (Tok.isNot(tok::l_brace)) {
+    Diag(Tok, diag::err_contract_expected_body);
+    return StmtError();
+  }
+
+  StmtResult Body = ParseCompoundStatement();
+  if (Body.isInvalid())
+    return StmtError();
+
+  return new (Actions.getASTContext()) GhostBlockStmt(GhostLoc, Body.get());
+}
+
+/// Parse contract_assert(expr);
+StmtResult Parser::ParseContractAssert() {
+  assert(Tok.is(tok::kw_contract_assert) && "Expected 'contract_assert'");
+  SourceLocation CALoc = ConsumeToken();
+
+  if (Tok.isNot(tok::l_paren)) {
+    Diag(Tok, diag::err_contract_expected_lparen) << "contract_assert";
+    return StmtError();
+  }
+  SourceLocation LParenLoc = ConsumeParen();
+
+  ExprResult Cond = ParseExpression();
+  if (Cond.isInvalid()) {
+    SkipUntil(tok::r_paren, StopAtSemi);
+    return StmtError();
+  }
+
+  Cond = Actions.ActOnContractCondition(Cond);
+  if (Cond.isInvalid()) {
+    SkipUntil(tok::r_paren, StopAtSemi);
+    return StmtError();
+  }
+
+  if (Tok.isNot(tok::r_paren)) {
+    Diag(Tok, diag::err_contract_expected_rparen) << "contract_assert";
+    SkipUntil(tok::r_paren, StopAtSemi);
+    return StmtError();
+  }
+  SourceLocation RParenLoc = ConsumeParen();
+
+  return new (Actions.getASTContext())
+      ContractAssertStmt(CALoc, LParenLoc, RParenLoc, Cond.get());
+}
diff --git a/clang/lib/Parse/Parser.cpp b/clang/lib/Parse/Parser.cpp
index 8f6f023dd7..9c73b0ab7b 100644
--- a/clang/lib/Parse/Parser.cpp
+++ b/clang/lib/Parse/Parser.cpp
@@ -14,6 +14,7 @@
 #include "clang/AST/ASTConsumer.h"
 #include "clang/AST/ASTContext.h"
 #include "clang/AST/ASTLambda.h"
+#include "clang/AST/Decl.h"
 #include "clang/AST/DeclTemplate.h"
 #include "clang/Basic/DiagnosticParse.h"
 #include "clang/Basic/StackExhaustionHandler.h"
@@ -1067,6 +1068,12 @@ bool Parser::isStartOfFunctionDefinition(const ParsingDeclarator &Declarator) {
     return KW.is(tok::kw_default) || KW.is(tok::kw_delete);
   }
 
+  // CppVerify: contract clauses (pre/post/decreases) precede the function body.
+  if (getLangOpts().VerifyContracts &&
+      (Tok.is(tok::kw_pre) || Tok.is(tok::kw_post) ||
+       Tok.is(tok::kw_decreases)))
+    return true;
+
   return Tok.is(tok::colon) ||         // X() : Base() {} (used for ctors)
          Tok.is(tok::kw_try);          // X() try { ... }
 }
@@ -1237,7 +1244,107 @@ Decl *Parser::ParseFunctionDefinition(ParsingDeclarator &D,
   if (FTI.isKNRPrototype())
     ParseKNRParamDeclarations(D);
 
-  // We should have either an opening brace or, in a C++ constructor,
+  // CppVerify: parse contract clauses (pre/post/decreases) before the body.
+  SmallVector<Expr *, 2> ContractPreconditions;
+  SmallVector<Expr *, 2> ContractPostconditions;
+  Expr *ContractDecreases = nullptr;
+  // Detect spec/proof from DeclSpec bits set during declaration parsing.
+  bool IsSpecFn = getLangOpts().VerifyContracts &&
+                  D.getDeclSpec().isSpecFunctionSpecified();
+  bool IsProofFn = getLangOpts().VerifyContracts &&
+                   D.getDeclSpec().isProofFunctionSpecified();
+
+  if (getLangOpts().VerifyContracts) {
+    // Re-enter function parameters into scope so contract conditions can
+    // reference them. This mirrors ParseTrailingRequiresClause in
+    // ParseDeclCXX.cpp: create a FunctionPrototypeScope and push params.
+    std::optional<ParseScope> ContractParamScope;
+    if (D.isFunctionDeclarator() &&
+        (Tok.is(tok::kw_pre) || Tok.is(tok::kw_post) ||
+         Tok.is(tok::kw_decreases))) {
+      ContractParamScope.emplace(this, Scope::DeclScope |
+                                           Scope::FunctionDeclarationScope |
+                                           Scope::FunctionPrototypeScope);
+      Actions.ActOnStartTrailingRequiresClause(getCurScope(), D);
+
+      // Compute the return type from the full Declarator (not just the
+      // DeclSpec) so that 'result' in postconditions gets the correct type.
+      // This handles pointers, references, typedefs, trailing return types,
+      // struct returns, etc. — all declarator modifiers are accounted for.
+      // The FunctionDecl doesn't exist yet, so we ask Sema to compute the
+      // full function type from the Declarator and extract the return type.
+      {
+        TypeSourceInfo *TSI = Actions.GetTypeForDeclarator(D);
+        QualType FullType = TSI->getType();
+        if (const auto *FT = FullType->getAs<FunctionType>())
+          CurrentContractReturnType = FT->getReturnType();
+        else
+          CurrentContractReturnType = Actions.getASTContext().IntTy;
+      }
+    }
+
+    while (Tok.is(tok::kw_pre) || Tok.is(tok::kw_post) ||
+           Tok.is(tok::kw_decreases)) {
+      bool IsPre = Tok.is(tok::kw_pre);
+      bool IsPost = Tok.is(tok::kw_post);
+      ConsumeToken();
+
+      if (Tok.isNot(tok::l_paren)) {
+        Diag(Tok, diag::err_contract_expected_lparen)
+            << (IsPre ? "pre" : IsPost ? "post" : "decreases");
+        break;
+      }
+      ConsumeParen();
+
+      // For postconditions, enable 'result' and 'old' parsing.
+      if (IsPost)
+        InContractPostcondition = true;
+
+      ExprResult E = ParseExpression();
+
+      if (IsPost)
+        InContractPostcondition = false;
+
+      if (E.isInvalid()) {
+        SkipUntil(tok::r_paren, StopAtSemi);
+        continue;
+      }
+
+      // Pre/post conditions must be bool; decreases is an integer measure.
+      if (IsPre || IsPost) {
+        E = Actions.ActOnContractCondition(E);
+        if (E.isInvalid()) {
+          SkipUntil(tok::r_paren, StopAtSemi);
+          continue;
+        }
+      } else {
+        // decreases: validate integer type.
+        if (!E.get()->getType()->isIntegerType()) {
+          Diag(E.get()->getExprLoc(),
+               diag::err_contract_decreases_not_int);
+          SkipUntil(tok::r_paren, StopAtSemi);
+          continue;
+        }
+      }
+
+      if (Tok.isNot(tok::r_paren)) {
+        Diag(Tok, diag::err_contract_expected_rparen)
+            << (IsPre ? "pre" : IsPost ? "post" : "decreases");
+        SkipUntil(tok::r_paren, StopAtSemi);
+        continue;
+      }
+      ConsumeParen();
+
+      if (IsPre)
+        ContractPreconditions.push_back(E.get());
+      else if (IsPost)
+        ContractPostconditions.push_back(E.get());
+      else
+        ContractDecreases = E.get();
+    }
+  }
+
+  // We should have either an opening brace, or in a C++ constructor,
   // we may have a colon.
   if (Tok.isNot(tok::l_brace) &&
       (!getLangOpts().CPlusPlus ||
@@ -1389,6 +1496,28 @@ Decl *Parser::ParseFunctionDefinition(ParsingDeclarator &D,
   // Break out of the ParsingDeclarator context before we parse the body.
   D.complete(Res);
 
+  // CppVerify: store contract clauses on the FunctionDecl.
+  if (Res && (!ContractPreconditions.empty() ||
+              !ContractPostconditions.empty() || ContractDecreases ||
+              IsSpecFn || IsProofFn)) {
+    if (auto *FD = dyn_cast<FunctionDecl>(Res)) {
+      FunctionContractInfo &FCI =
+          Actions.getASTContext().getOrCreateFunctionContract(FD);
+      FCI.Preconditions = std::move(ContractPreconditions);
+      FCI.Postconditions = std::move(ContractPostconditions);
+      FCI.Decreases = ContractDecreases;
+      FCI.IsSpec = IsSpecFn;
+      FCI.IsProof = IsProofFn;
+      CurrentContractFunction = Res;
+    }
+  }
+
+  // Reset contract parsing state so it doesn't leak into subsequent functions.
+  CurrentContractReturnType = QualType();
+  // Note: CurrentContractFunction is intentionally kept alive — it can be
+  // used by the VCGen backend later. InContractPostcondition was already
+  // reset after each post(...) clause above.
+
   // Break out of the ParsingDeclSpec context, too.  This const_cast is
   // safe because we're always the sole owner.
   D.getMutableDeclSpec().abort();
diff --git a/clang/lib/Sema/CMakeLists.txt b/clang/lib/Sema/CMakeLists.txt
index 0ebf56ecff..13a161e635 100644
--- a/clang/lib/Sema/CMakeLists.txt
+++ b/clang/lib/Sema/CMakeLists.txt
@@ -45,6 +45,7 @@ add_clang_library(clangSema
   SemaCodeComplete.cpp
   SemaConcept.cpp
   SemaConsumer.cpp
+  SemaContract.cpp
   SemaCoroutine.cpp
   SemaCUDA.cpp
   SemaDirectX.cpp
diff --git a/clang/lib/Sema/SemaContract.cpp b/clang/lib/Sema/SemaContract.cpp
new file mode 100644
index 0000000000..2819232a4b
--- /dev/null
+++ b/clang/lib/Sema/SemaContract.cpp
@@ -0,0 +1,34 @@
+//===--- SemaContract.cpp - Semantic Analysis for Contracts ------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// This file implements semantic analysis for CppVerify contract constructs.
+// For the MVP, contract expressions are parsed as normal Clang expressions
+// and get basic type checking through the standard Sema pipeline. This file
+// provides a home for future contract-specific semantic checks.
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/AST/ASTContext.h"
+#include "clang/AST/ExprContract.h"
+#include "clang/AST/StmtContract.h"
+#include "clang/Sema/Sema.h"
+
+using namespace clang;
+
+/// ActOnContractCondition - Semantic action called by the parser after
+/// parsing a contract condition expression (pre/post/invariant/contract_assert).
+///
+/// Verifies that the expression is contextually convertible to bool.
+///
+/// ForallExpr and ExistsExpr already carry type BoolTy so the conversion is
+/// a no-op; plain integer/pointer expressions receive the standard bool cast.
+ExprResult Sema::ActOnContractCondition(ExprResult E) {
+  if (E.isInvalid())
+    return E;
+  return PerformContextuallyConvertToBool(E.get());
+}
diff --git a/clang/lib/Sema/TreeTransform.h b/clang/lib/Sema/TreeTransform.h
index 5a1e5fedba..2cc163acbd 100644
--- a/clang/lib/Sema/TreeTransform.h
+++ b/clang/lib/Sema/TreeTransform.h
@@ -21,11 +21,13 @@
 #include "clang/AST/Expr.h"
 #include "clang/AST/ExprCXX.h"
 #include "clang/AST/ExprConcepts.h"
+#include "clang/AST/ExprContract.h"
 #include "clang/AST/ExprObjC.h"
 #include "clang/AST/ExprOpenMP.h"
 #include "clang/AST/OpenMPClause.h"
 #include "clang/AST/Stmt.h"
 #include "clang/AST/StmtCXX.h"
+#include "clang/AST/StmtContract.h"
 #include "clang/AST/StmtObjC.h"
 #include "clang/AST/StmtOpenACC.h"
 #include "clang/AST/StmtOpenMP.h"
@@ -17900,6 +17902,87 @@ ExprResult TreeTransform<Derived>::TransformHLSLOutArgExpr(HLSLOutArgExpr *E) {
   return getDerived().TransformExpr(E->getArgLValue());
 }
 
+//===----------------------------------------------------------------------===//
+// CppVerify contract node transforms
+//===----------------------------------------------------------------------===//
+
+// Contract nodes are ghost/spec constructs that are stripped before codegen.
+// Template instantiation just rebuilds them unchanged by transforming children.
+
+template <typename Derived>
+StmtResult
+TreeTransform<Derived>::TransformContractAssertStmt(ContractAssertStmt *S) {
+  ExprResult Cond = getDerived().TransformExpr(S->getCond());
+  if (Cond.isInvalid())
+    return StmtError();
+  if (!getDerived().AlwaysRebuild() && Cond.get() == S->getCond())
+    return S;
+  return new (SemaRef.Context) ContractAssertStmt(
+      S->getContractAssertLoc(), S->getLParenLoc(), S->getRParenLoc(),
+      Cond.getAs<Expr>());
+}
+
+template <typename Derived>
+StmtResult TreeTransform<Derived>::TransformGhostBlockStmt(GhostBlockStmt *S) {
+  StmtResult Body = getDerived().TransformStmt(S->getBody());
+  if (Body.isInvalid())
+    return StmtError();
+  if (!getDerived().AlwaysRebuild() && Body.get() == S->getBody())
+    return S;
+  return new (SemaRef.Context) GhostBlockStmt(S->getGhostLoc(), Body.get());
+}
+
+template <typename Derived>
+ExprResult TreeTransform<Derived>::TransformForallExpr(ForallExpr *E) {
+  ExprResult Lo = getDerived().TransformExpr(E->getLo());
+  if (Lo.isInvalid()) return ExprError();
+  ExprResult Hi = getDerived().TransformExpr(E->getHi());
+  if (Hi.isInvalid()) return ExprError();
+  ExprResult Body = getDerived().TransformExpr(E->getBody());
+  if (Body.isInvalid()) return ExprError();
+  if (!getDerived().AlwaysRebuild() && Lo.get() == E->getLo() &&
+      Hi.get() == E->getHi() && Body.get() == E->getBody())
+    return E;
+  return new (SemaRef.Context)
+      ForallExpr(E->getForallLoc(), E->getLParenLoc(), E->getRParenLoc(),
+                 E->getBoundVar(), Lo.getAs<Expr>(), Hi.getAs<Expr>(),
+                 Body.getAs<Expr>(), SemaRef.Context.BoolTy);
+}
+
+template <typename Derived>
+ExprResult TreeTransform<Derived>::TransformExistsExpr(ExistsExpr *E) {
+  ExprResult Lo = getDerived().TransformExpr(E->getLo());
+  if (Lo.isInvalid()) return ExprError();
+  ExprResult Hi = getDerived().TransformExpr(E->getHi());
+  if (Hi.isInvalid()) return ExprError();
+  ExprResult Body = getDerived().TransformExpr(E->getBody());
+  if (Body.isInvalid()) return ExprError();
+  if (!getDerived().AlwaysRebuild() && Lo.get() == E->getLo() &&
+      Hi.get() == E->getHi() && Body.get() == E->getBody())
+    return E;
+  return new (SemaRef.Context)
+      ExistsExpr(E->getExistsLoc(), E->getLParenLoc(), E->getRParenLoc(),
+                 E->getBoundVar(), Lo.getAs<Expr>(), Hi.getAs<Expr>(),
+                 Body.getAs<Expr>(), SemaRef.Context.BoolTy);
+}
+
+template <typename Derived>
+ExprResult TreeTransform<Derived>::TransformOldExpr(OldExpr *E) {
+  ExprResult Inner = getDerived().TransformExpr(E->getInner());
+  if (Inner.isInvalid()) return ExprError();
+  if (!getDerived().AlwaysRebuild() && Inner.get() == E->getInner())
+    return E;
+  return new (SemaRef.Context)
+      OldExpr(E->getOldLoc(), E->getLParenLoc(), E->getRParenLoc(),
+              Inner.getAs<Expr>());
+}
+
+template <typename Derived>
+ExprResult TreeTransform<Derived>::TransformResultExpr(ResultExpr *E) {
+  // ResultExpr has no children to transform.
+  return E;
+}
+
 } // end namespace clang
 
 #endif // LLVM_CLANG_LIB_SEMA_TREETRANSFORM_H
diff --git a/clang/lib/Serialization/ASTReaderStmt.cpp b/clang/lib/Serialization/ASTReaderStmt.cpp
index 5553139dfa..98f6bdb729 100644
--- a/clang/lib/Serialization/ASTReaderStmt.cpp
+++ b/clang/lib/Serialization/ASTReaderStmt.cpp
@@ -24,6 +24,7 @@
 #include "clang/AST/DependenceFlags.h"
 #include "clang/AST/Expr.h"
 #include "clang/AST/ExprCXX.h"
+#include "clang/AST/ExprContract.h"
 #include "clang/AST/ExprObjC.h"
 #include "clang/AST/ExprOpenMP.h"
 #include "clang/AST/NestedNameSpecifier.h"
@@ -31,6 +32,7 @@
 #include "clang/AST/OperationKinds.h"
 #include "clang/AST/Stmt.h"
 #include "clang/AST/StmtCXX.h"
+#include "clang/AST/StmtContract.h"
 #include "clang/AST/StmtObjC.h"
 #include "clang/AST/StmtOpenMP.h"
 #include "clang/AST/StmtSYCL.h"
@@ -2988,6 +2990,59 @@ void ASTStmtReader::VisitHLSLOutArgExpr(HLSLOutArgExpr *S) {
   S->IsInOut = Record.readBool();
 }
 
+//===----------------------------------------------------------------------===//
+// CppVerify Contract Node Deserialization
+//===----------------------------------------------------------------------===//
+
+void ASTStmtReader::VisitContractAssertStmt(ContractAssertStmt *S) {
+  VisitStmt(S);
+  S->Cond = Record.readSubExpr();
+  S->ContractAssertLoc = readSourceLocation();
+  S->LParenLoc = readSourceLocation();
+  S->RParenLoc = readSourceLocation();
+}
+
+void ASTStmtReader::VisitGhostBlockStmt(GhostBlockStmt *S) {
+  VisitStmt(S);
+  S->Body = Record.readSubStmt();
+  S->GhostLoc = readSourceLocation();
+}
+
+void ASTStmtReader::VisitForallExpr(ForallExpr *E) {
+  VisitExpr(E);
+  E->BoundVar = readDeclAs<VarDecl>();
+  E->SubExprs[ForallExpr::LO] = Record.readSubExpr();
+  E->SubExprs[ForallExpr::HI] = Record.readSubExpr();
+  E->SubExprs[ForallExpr::BODY] = Record.readSubExpr();
+  E->ForallLoc = readSourceLocation();
+  E->LParenLoc = readSourceLocation();
+  E->RParenLoc = readSourceLocation();
+}
+
+void ASTStmtReader::VisitExistsExpr(ExistsExpr *E) {
+  VisitExpr(E);
+  E->BoundVar = readDeclAs<VarDecl>();
+  E->SubExprs[ExistsExpr::LO] = Record.readSubExpr();
+  E->SubExprs[ExistsExpr::HI] = Record.readSubExpr();
+  E->SubExprs[ExistsExpr::BODY] = Record.readSubExpr();
+  E->ExistsLoc = readSourceLocation();
+  E->LParenLoc = readSourceLocation();
+  E->RParenLoc = readSourceLocation();
+}
+
+void ASTStmtReader::VisitOldExpr(OldExpr *E) {
+  VisitExpr(E);
+  E->Inner = Record.readSubExpr();
+  E->OldLoc = readSourceLocation();
+  E->LParenLoc = readSourceLocation();
+  E->RParenLoc = readSourceLocation();
+}
+
+void ASTStmtReader::VisitResultExpr(ResultExpr *E) {
+  VisitExpr(E);
+  E->ResultLoc = readSourceLocation();
+}
+
 //===----------------------------------------------------------------------===//
 // ASTReader Implementation
 //===----------------------------------------------------------------------===//
@@ -4542,6 +4597,26 @@ Stmt *ASTReader::ReadStmtFromStream(ModuleFile &F) {
     case EXPR_HLSL_OUT_ARG:
       S = HLSLOutArgExpr::CreateEmpty(Context);
       break;
+
+    // CppVerify contract nodes
+    case STMT_CONTRACT_ASSERT:
+      S = new (Context) ContractAssertStmt(Empty);
+      break;
+    case STMT_GHOST_BLOCK:
+      S = new (Context) GhostBlockStmt(Empty);
+      break;
+    case EXPR_FORALL:
+      S = new (Context) ForallExpr(Empty);
+      break;
+    case EXPR_EXISTS:
+      S = new (Context) ExistsExpr(Empty);
+      break;
+    case EXPR_OLD:
+      S = new (Context) OldExpr(Empty);
+      break;
+    case EXPR_RESULT:
+      S = new (Context) ResultExpr(Empty);
+      break;
     }
 
     // We hit a STMT_STOP, so we're done with this expression.
diff --git a/clang/lib/Serialization/ASTWriterStmt.cpp b/clang/lib/Serialization/ASTWriterStmt.cpp
index 8f22156f93..abd5601b6a 100644
--- a/clang/lib/Serialization/ASTWriterStmt.cpp
+++ b/clang/lib/Serialization/ASTWriterStmt.cpp
@@ -16,7 +16,9 @@
 #include "clang/AST/DeclCXX.h"
 #include "clang/AST/DeclObjC.h"
 #include "clang/AST/DeclTemplate.h"
+#include "clang/AST/ExprContract.h"
 #include "clang/AST/ExprOpenMP.h"
+#include "clang/AST/StmtContract.h"
 #include "clang/AST/StmtVisitor.h"
 #include "clang/Serialization/ASTReader.h"
 #include "clang/Serialization/ASTRecordWriter.h"
@@ -3088,6 +3090,65 @@ void ASTStmtWriter::VisitHLSLOutArgExpr(HLSLOutArgExpr *S) {
   Code = serialization::EXPR_HLSL_OUT_ARG;
 }
 
+//===----------------------------------------------------------------------===//
+// CppVerify Contract Node Serialization
+//===----------------------------------------------------------------------===//
+
+void ASTStmtWriter::VisitContractAssertStmt(ContractAssertStmt *S) {
+  VisitStmt(S);
+  Record.AddStmt(S->getCond());
+  Record.AddSourceLocation(S->getContractAssertLoc());
+  Record.AddSourceLocation(S->getLParenLoc());
+  Record.AddSourceLocation(S->getRParenLoc());
+  Code = serialization::STMT_CONTRACT_ASSERT;
+}
+
+void ASTStmtWriter::VisitGhostBlockStmt(GhostBlockStmt *S) {
+  VisitStmt(S);
+  Record.AddStmt(S->getBody());
+  Record.AddSourceLocation(S->getGhostLoc());
+  Code = serialization::STMT_GHOST_BLOCK;
+}
+
+void ASTStmtWriter::VisitForallExpr(ForallExpr *E) {
+  VisitExpr(E);
+  Record.AddDeclRef(E->getBoundVar());
+  Record.AddStmt(E->getLo());
+  Record.AddStmt(E->getHi());
+  Record.AddStmt(E->getBody());
+  Record.AddSourceLocation(E->getForallLoc());
+  Record.AddSourceLocation(E->getLParenLoc());
+  Record.AddSourceLocation(E->getRParenLoc());
+  Code = serialization::EXPR_FORALL;
+}
+
+void ASTStmtWriter::VisitExistsExpr(ExistsExpr *E) {
+  VisitExpr(E);
+  Record.AddDeclRef(E->getBoundVar());
+  Record.AddStmt(E->getLo());
+  Record.AddStmt(E->getHi());
+  Record.AddStmt(E->getBody());
+  Record.AddSourceLocation(E->getExistsLoc());
+  Record.AddSourceLocation(E->getLParenLoc());
+  Record.AddSourceLocation(E->getRParenLoc());
+  Code = serialization::EXPR_EXISTS;
+}
+
+void ASTStmtWriter::VisitOldExpr(OldExpr *E) {
+  VisitExpr(E);
+  Record.AddStmt(E->getInner());
+  Record.AddSourceLocation(E->getOldLoc());
+  Record.AddSourceLocation(E->getLParenLoc());
+  Record.AddSourceLocation(E->getRParenLoc());
+  Code = serialization::EXPR_OLD;
+}
+
+void ASTStmtWriter::VisitResultExpr(ResultExpr *E) {
+  VisitExpr(E);
+  Record.AddSourceLocation(E->getResultLoc());
+  Code = serialization::EXPR_RESULT;
+}
+
 //===----------------------------------------------------------------------===//
 // ASTWriter Implementation
 //===----------------------------------------------------------------------===//
diff --git a/clang/test/Verify/backward_compat.cpp b/clang/test/Verify/backward_compat.cpp
new file mode 100644
index 0000000000..f5ef0efa93
--- /dev/null
+++ b/clang/test/Verify/backward_compat.cpp
@@ -0,0 +1,21 @@
+// RUN: %clang_cc1 -std=c++17 -verify %s
+//
+// Week-2 milestone test: without -fverify-contracts, all contract keywords
+// are valid identifiers and the file compiles without any diagnostics.
+//
+// expected-no-diagnostics
+
+int pre = 1;
+int post = 2;
+int invariant = 3;
+int decreases = 4;
+int ghost = 5;
+int result = pre + post + invariant + decreases + ghost;
+
+// 'spec', 'proof', 'contract_assert', 'forall', 'exists', 'old' are also
+// plain identifiers without the flag.
+int spec = 6;
+int proof = 7;
+int old = 8;
+
+int forall_value = spec + proof + old;
diff --git a/clang/test/Verify/basic_contracts.cpp b/clang/test/Verify/basic_contracts.cpp
new file mode 100644
index 0000000000..4ee02b70b9
--- /dev/null
+++ b/clang/test/Verify/basic_contracts.cpp
@@ -0,0 +1,30 @@
+// RUN: %clang_cc1 -std=c++17 -fverify-contracts -ast-dump %s | FileCheck %s
+//
+// Week-2 milestone test: verify that contract AST nodes appear in -ast-dump
+// output when -fverify-contracts is active.
+//
+// CHECK: FunctionDecl {{.*}} safe_add
+// CHECK: GhostBlockStmt
+// CHECK: ContractAssertStmt
+// CHECK: ForallExpr
+
+int safe_add(int a, int b)
+  pre(a >= 0)
+  pre(b >= 0)
+  post(result >= 0)
+{
+  ghost {
+    contract_assert(a + b >= 0);
+  }
+  return a + b;
+}
+
+int clamped_index(int i, int n)
+  pre(n > 0)
+  pre(forall(j, 0, n, j >= 0))
+  post(result >= 0)
+{
+  if (i < 0) return 0;
+  if (i >= n) return n - 1;
+  return i;
+}
diff --git a/clang/test/Verify/ghost_blocks.cpp b/clang/test/Verify/ghost_blocks.cpp
new file mode 100644
index 0000000000..ecbfbce05d
--- /dev/null
+++ b/clang/test/Verify/ghost_blocks.cpp
@@ -0,0 +1,20 @@
+// RUN: %clang_cc1 -std=c++17 -fverify-contracts -ast-dump %s | FileCheck %s
+// RUN: %clang_cc1 -std=c++17 -fverify-contracts -emit-llvm -o %t %s
+//
+// Test that ghost blocks and contract_assert:
+// 1. Appear in the AST dump
+// 2. Produce zero codegen (no LLVM IR for ghost content)
+//
+// CHECK: GhostBlockStmt
+// CHECK: ContractAssertStmt
+
+int abs_val(int x)
+  pre(x != -2147483648)
+  post(result >= 0)
+{
+  ghost {
+    contract_assert(x != -2147483648);
+  }
+  if (x < 0) return -x;
+  return x;
+}
diff --git a/clang/test/Verify/loop_contracts.cpp b/clang/test/Verify/loop_contracts.cpp
new file mode 100644
index 0000000000..8e740b6d73
--- /dev/null
+++ b/clang/test/Verify/loop_contracts.cpp
@@ -0,0 +1,39 @@
+// RUN: %clang_cc1 -std=c++17 -fverify-contracts -ast-dump %s | FileCheck %s
+//
+// Week-2 milestone test: verify that loop contract AST nodes (invariant,
+// decreases) are accepted by the parser and visible in -ast-dump.
+//
+// CHECK: FunctionDecl {{.*}} sum
+// CHECK: WhileStmt
+
+int sum(int n)
+  pre(n >= 0)
+  post(result >= 0)
+{
+  int s = 0, i = 0;
+  while (i < n)
+    invariant(s >= 0)
+    invariant(i >= 0)
+    decreases(n - i)
+  {
+    s += i;
+    i++;
+  }
+  return s;
+}
+
+int factorial(int n)
+  pre(n >= 0)
+  post(result >= 1)
+{
+  int r = 1, k = 1;
+  while (k <= n)
+    invariant(r >= 1)
+    invariant(k >= 1)
+    decreases(n - k + 1)
+  {
+    r *= k;
+    k++;
+  }
+  return r;
+}
diff --git a/samples/test1.cpp b/samples/test1.cpp
new file mode 100644
index 0000000000..7c48e64d53
--- /dev/null
+++ b/samples/test1.cpp
@@ -0,0 +1,365 @@
+// =============================================================================
+// CppVerify Comprehensive Test
+//
+// This file exercises every contract construct and is designed to catch
+// regressions in: keyword lexing, contract parsing, AST node types,
+// return-type resolution for 'result', context restrictions for 'old'/'result',
+// quantifier type checking, loop contracts on both while and for, ghost blocks,
+// contract_assert, spec/proof function qualifiers, and multiple pre/post
+// clauses.
+//
+// Build & test:
+//   ./build/bin/clang++ -cc1 -fverify-contracts -ast-dump samples/test1.cpp
+//   ./build/bin/clang++ -cc1 -fverify-contracts -emit-llvm -o /dev/null samples/test1.cpp
+// =============================================================================
+
+// ---------------------------------------------------------------------------
+// 1. Spec function (int return) with decreases
+// ---------------------------------------------------------------------------
+spec int factorial(int n)
+  decreases(n)
+{
+    if (n <= 1) return 1;
+    return n * factorial(n - 1);
+}
+
+// ---------------------------------------------------------------------------
+// 2. Proof function (void return) with pre/post/decreases + recursion
+// ---------------------------------------------------------------------------
+proof void lemma_factorial_positive(int n)
+  pre(n >= 1)
+  post(factorial(n) >= 1)
+  decreases(n)
+{
+    if (n == 1) {
+        // base case: factorial(1) == 1 >= 1
+    } else {
+        lemma_factorial_positive(n - 1);
+    }
+}
+
+// ---------------------------------------------------------------------------
+// 3. Regular function with multiple pre/post, while-loop contracts,
+//    ghost block, contract_assert, result, and spec function calls in
+//    contracts.
+// ---------------------------------------------------------------------------
+int safe_factorial(int n)
+  pre(n >= 0)
+  pre(n <= 12)
+  post(result == factorial(n))
+  post(result >= 1)
+{
+    if (n == 0) return 1;
+
+    int acc = 1;
+    int i = 1;
+
+    while (i <= n)
+      invariant(1 <= i && i <= n + 1)
+      invariant(acc == factorial(i - 1))
+      decreases(n - i + 1)
+    {
+        ghost {
+            lemma_factorial_positive(i);
+            contract_assert(acc * i >= acc);
+        }
+
+        acc = acc * i;
+        i = i + 1;
+    }
+
+    return acc;
+}
+
+// ---------------------------------------------------------------------------
+// 4. Spec functions returning bool — exercises forall/exists quantifiers
+// ---------------------------------------------------------------------------
+spec bool all_positive(int arr[], int n)
+{
+    return forall(i, 0, n, arr[i] > 0);
+}
+
+spec bool has_zero(int arr[], int n)
+{
+    return exists(i, 0, n, arr[i] == 0);
+}
+
+// ---------------------------------------------------------------------------
+// 5. Function with old() and result — exercises postcondition-only keywords
+// ---------------------------------------------------------------------------
+int increment(int x)
+  pre(x < 2147483647)
+  post(result == old(x) + 1)
+{
+    return x + 1;
+}
+
+// ---------------------------------------------------------------------------
+// 6. Non-int return types — catches stale CurrentContractReturnType bugs.
+//    Each function's 'result' must get the correct QualType from the DeclSpec.
+// ---------------------------------------------------------------------------
+
+// 6a. bool return type
+bool is_positive(int x)
+  post(result == (old(x) > 0))
+{
+    return x > 0;
+}
+
+// 6b. unsigned int return type
+unsigned int safe_subtract(unsigned int a, unsigned int b)
+  pre(a >= b)
+  post(result == old(a) - old(b))
+{
+    return a - b;
+}
+
+// 6c. long return type
+long wide_add(long a, long b)
+  pre(a >= 0)
+  pre(b >= 0)
+  post(result >= old(a))
+  post(result >= old(b))
+{
+    return a + b;
+}
+
+// 6d. short return type
+short clamp_to_short(int x)
+  pre(x >= -32768)
+  pre(x <= 32767)
+  post(result == old(x))
+{
+    return (short)x;
+}
+
+// ---------------------------------------------------------------------------
+// 7. For-loop contracts — catches missing VisitForStmt in AST dumper
+// ---------------------------------------------------------------------------
+int sum_range(int n)
+  pre(n >= 0)
+  post(result >= 0)
+{
+    int s = 0;
+    for (int i = 0; i < n; i = i + 1)
+      invariant(s >= 0)
+      invariant(i >= 0)
+      decreases(n - i)
+    {
+        s = s + i;
+    }
+    return s;
+}
+
+// ---------------------------------------------------------------------------
+// 8. Multiple ghost blocks + interleaved contract_asserts
+// ---------------------------------------------------------------------------
+int double_val(int x)
+  pre(x >= 0)
+  pre(x <= 1000000)
+  post(result == old(x) + old(x))
+{
+    ghost {
+        contract_assert(x >= 0);
+    }
+
+    int r = x + x;
+
+    ghost {
+        contract_assert(r == x + x);
+        contract_assert(r >= 0);
+    }
+
+    return r;
+}
+
+// ---------------------------------------------------------------------------
+// 9. Spec function calling another spec function — exercises spec-to-spec
+//    call resolution and return type propagation
+// ---------------------------------------------------------------------------
+spec int double_factorial(int n)
+{
+    return factorial(n) * factorial(n);
+}
+
+spec bool factorial_is_positive(int n)
+{
+    return factorial(n) >= 1;
+}
+
+// ---------------------------------------------------------------------------
+// 10. Proof function with multiple lemma calls in ghost block
+// ---------------------------------------------------------------------------
+proof void lemma_factorials_positive(int a, int b)
+  pre(a >= 1)
+  pre(b >= 1)
+  post(factorial(a) + factorial(b) >= 2)
+{
+    lemma_factorial_positive(a);
+    lemma_factorial_positive(b);
+}
+
+// ---------------------------------------------------------------------------
+// 11. Function with only preconditions (no postconditions) — verifies that
+//     missing post doesn't cause issues
+// ---------------------------------------------------------------------------
+int checked_div(int a, int b)
+  pre(b != 0)
+{
+    return a / b;
+}
+
+// ---------------------------------------------------------------------------
+// 12. Function with only postconditions (no preconditions)
+// ---------------------------------------------------------------------------
+int abs_val(int x)
+  post(result >= 0)
+{
+    if (x < 0) return -x;
+    return x;
+}
+
+// ---------------------------------------------------------------------------
+// 13. Back-to-back functions with different return types — stress test for
+//     CurrentContractReturnType resetting between function definitions
+// ---------------------------------------------------------------------------
+bool flag_a(int x)
+  post(result == (old(x) > 0))
+{
+    return x > 0;
+}
+
+int value_b(int x)
+  pre(x >= 0)
+  post(result == old(x) + 1)
+{
+    return x + 1;
+}
+
+bool flag_c(int y)
+  post(result == (old(y) != 0))
+{
+    return y != 0;
+}
+
+unsigned int value_d(unsigned int z)
+  post(result == old(z))
+{
+    return z;
+}
+
+// ---------------------------------------------------------------------------
+// 14. While-loop with only invariant (no decreases) — exercises optional
+//     decreases clause
+// ---------------------------------------------------------------------------
+int find_first_nonzero(int arr[], int n)
+  pre(n > 0)
+{
+    int i = 0;
+    while (i < n)
+      invariant(i >= 0)
+    {
+        if (arr[i] != 0) return i;
+        i = i + 1;
+    }
+    return -1;
+}
+
+// ---------------------------------------------------------------------------
+// 15. Quantifier in postcondition — exercises forall inside post()
+// ---------------------------------------------------------------------------
+spec bool all_zero(int arr[], int n)
+{
+    return forall(i, 0, n, arr[i] == 0);
+}
+
+void zero_fill(int arr[], int n)
+  pre(n >= 0)
+  post(all_zero(arr, n))
+{
+    for (int i = 0; i < n; i = i + 1)
+      invariant(i >= 0)
+      invariant(all_zero(arr, i))
+      decreases(n - i)
+    {
+        arr[i] = 0;
+    }
+}
+
+// ---------------------------------------------------------------------------
+// 16. Pointer return types — exercises full-Declarator return type resolution.
+//     The 'result' keyword must be typed as 'int *', not just 'int'.
+// ---------------------------------------------------------------------------
+int *find_ptr(int arr[], int n, int val)
+  pre(n > 0)
+{
+    for (int i = 0; i < n; i = i + 1)
+    {
+        if (arr[i] == val) return &arr[i];
+    }
+    return (int *)0;
+}
+
+// ---------------------------------------------------------------------------
+// 17. Const pointer return — exercises pointer + const qualifier on return.
+// ---------------------------------------------------------------------------
+const int *find_const(const int arr[], int n, int val)
+  pre(n > 0)
+{
+    for (int i = 0; i < n; i = i + 1)
+    {
+        if (arr[i] == val) return &arr[i];
+    }
+    return (const int *)0;
+}
+
+// ---------------------------------------------------------------------------
+// 18. Struct return type — exercises struct return with contracts.
+// ---------------------------------------------------------------------------
+struct Point {
+    int x;
+    int y;
+};
+
+Point make_origin()
+  post(result.x == 0)
+  post(result.y == 0)
+{
+    Point p;
+    p.x = 0;
+    p.y = 0;
+    return p;
+}
+
+Point translate(Point p, int dx, int dy)
+  post(result.x == old(p.x) + old(dx))
+  post(result.y == old(p.y) + old(dy))
+{
+    Point r;
+    r.x = p.x + dx;
+    r.y = p.y + dy;
+    return r;
+}
+
+// ---------------------------------------------------------------------------
+// 19. Typedef return type — exercises TST_typename path through Declarator.
+// ---------------------------------------------------------------------------
+typedef unsigned long usize;
+
+usize safe_len(int arr[], int n)
+  pre(n >= 0)
+  post(result >= 0)
+{
+    return (usize)n;
+}
+
+// ---------------------------------------------------------------------------
+// 20. Pointer return with postcondition — 'result' must be typed 'int *'
+//     (this is the key regression test for the DeclSpec-only bug).
+// ---------------------------------------------------------------------------
+int *max_ptr(int *a, int *b)
+  post(result == old(a) || result == old(b))
+{
+    if (*a >= *b) return a;
+    return b;
+}