diff --git a/nullability_verification/BUILD b/nullability_verification/BUILD
new file mode 100644
index 0000000..fb9700b
--- /dev/null
+++ b/nullability_verification/BUILD
@@ -0,0 +1,50 @@
+# Verification for null safety
+
+cc_library(
+    name = "pointer_nullability_lattice",
+    hdrs = ["pointer_nullability_lattice.h"],
+    deps = [
+        "@llvm-project//clang:analysis",
+        "@llvm-project//llvm:Support",
+    ],
+)
+
+cc_library(
+    name = "pointer_nullability_matchers",
+    srcs = ["pointer_nullability_matchers.cc"],
+    hdrs = ["pointer_nullability_matchers.h"],
+    deps = [
+        "@llvm-project//clang:ast_matchers",
+        "@llvm-project//llvm:Support",
+    ],
+)
+
+cc_library(
+    name = "pointer_nullability_analysis",
+    srcs = ["pointer_nullability_analysis.cc"],
+    hdrs = ["pointer_nullability_analysis.h"],
+    deps = [
+        ":pointer_nullability_lattice",
+        ":pointer_nullability_matchers",
+        "//common:check",
+        "@llvm-project//clang:analysis",
+        "@llvm-project//clang:ast",
+        "@llvm-project//clang:ast_matchers",
+        "@llvm-project//clang:basic",
+        "@llvm-project//clang:tooling",
+    ],
+)
+
+cc_test(
+    name = "pointer_nullability_analysis_test",
+    srcs = ["pointer_nullability_analysis_test.cc"],
+    deps = [
+        ":pointer_nullability_analysis",
+        "@llvm-project//clang/unittests:dataflow_testing_support",
+        "@llvm-project//llvm:Support",
+        "@llvm-project//llvm:TestingSupport",
+        "@llvm-project//llvm:gmock",
+        "@llvm-project//llvm:gtest",
+        "@llvm-project//llvm:gtest_main",
+    ],
+)
diff --git a/nullability_verification/pointer_nullability_analysis.cc b/nullability_verification/pointer_nullability_analysis.cc
new file mode 100644
index 0000000..5cde0c3
--- /dev/null
+++ b/nullability_verification/pointer_nullability_analysis.cc
@@ -0,0 +1,139 @@
+// Part of the Crubit project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+#include "nullability_verification/pointer_nullability_analysis.h"
+
+#include <iostream>
+#include <string>
+
+#include "common/check.h"
+#include "nullability_verification/pointer_nullability_lattice.h"
+#include "nullability_verification/pointer_nullability_matchers.h"
+#include "clang/AST/ASTContext.h"
+#include "clang/AST/Expr.h"
+#include "clang/ASTMatchers/ASTMatchFinder.h"
+#include "clang/ASTMatchers/ASTMatchers.h"
+#include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
+#include "clang/Analysis/FlowSensitive/MatchSwitch.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
+#include "clang/Basic/LLVM.h"
+
+namespace clang {
+namespace tidy {
+namespace nullability {
+
+using ast_matchers::MatchFinder;
+using dataflow::BoolValue;
+using dataflow::Environment;
+using dataflow::MatchSwitchBuilder;
+using dataflow::PointerValue;
+using dataflow::SkipPast;
+using dataflow::TransferState;
+using dataflow::Value;
+
+namespace {
+
+void initialisePointerNullability(
+    const Expr* Expr, const MatchFinder::MatchResult&,
+    TransferState<PointerNullabilityLattice>& State) {
+  if (auto* PointerVal = cast_or_null<PointerValue>(
+          State.Env.getValue(*Expr, SkipPast::Reference))) {
+    if (!State.Lattice.hasPointerNullability(PointerVal)) {
+      State.Lattice.setPointerNullability(PointerVal,
+                                          &State.Env.makeAtomicBoolValue());
+    }
+  }
+}
+
+void transferDereference(const UnaryOperator* UnaryOp,
+                         const MatchFinder::MatchResult&,
+                         TransferState<PointerNullabilityLattice>& State) {
+  auto* PointerExpr = UnaryOp->getSubExpr();
+  if (auto* PointerVal = cast_or_null<PointerValue>(
+          State.Env.getValue(*PointerExpr, SkipPast::Reference))) {
+    auto PointerNullability = State.Lattice.getPointerNullability(PointerVal);
+    CHECK(PointerNullability != nullptr);
+    if (State.Env.flowConditionImplies(*PointerNullability)) {
+      return;
+    }
+  }
+  State.Lattice.addViolation(PointerExpr);
+}
+
+void transferNullCheckComparison(
+    const Expr* NullCheck, const Expr* PointerExpr,
+    TransferState<PointerNullabilityLattice>& State) {
+  if (auto* PointerVal = cast_or_null<PointerValue>(
+          State.Env.getValue(*PointerExpr, SkipPast::Reference))) {
+    auto* PointerNullability = State.Lattice.getPointerNullability(PointerVal);
+    CHECK(PointerNullability != nullptr);
+
+    // For binary operations, the dataflow framework automatically creates a
+    // corresponding BoolVal
+    auto* ExistingDFVal =
+        cast_or_null<BoolValue>(State.Env.getValue(*NullCheck, SkipPast::None));
+    CHECK(ExistingDFVal != nullptr);
+    State.Env.addToFlowCondition(
+        State.Env.makeIff(*ExistingDFVal, *PointerNullability));
+  }
+}
+
+void transferNullCheckImplicitCastPtrToBool(
+    const Expr* CastExpr, const MatchFinder::MatchResult&,
+    TransferState<PointerNullabilityLattice>& State) {
+  if (auto* PointerVal = cast_or_null<PointerValue>(State.Env.getValue(
+          *CastExpr->IgnoreImplicit(), SkipPast::Reference))) {
+    auto* PointerNullability = State.Lattice.getPointerNullability(PointerVal);
+    CHECK(PointerNullability != nullptr);
+
+    auto& CastExprLoc = State.Env.createStorageLocation(*CastExpr);
+    State.Env.setValue(CastExprLoc, *PointerNullability);
+    State.Env.setStorageLocation(*CastExpr, CastExprLoc);
+  }
+}
+
+auto buildTransferer() {
+  return MatchSwitchBuilder<TransferState<PointerNullabilityLattice>>()
+      // Initialise nullability state of pointers
+      .CaseOf<Expr>(isPointerExpr(), initialisePointerNullability)
+      // Pointer dereference
+      .CaseOf<UnaryOperator>(isPointerDereference(), transferDereference)
+      // Nullability check
+      .CaseOf<BinaryOperator>(
+          isNEQNullBinOp(/*BindID=*/"pointer"),
+          [](const BinaryOperator* binOp,
+             const MatchFinder::MatchResult& result,
+             TransferState<PointerNullabilityLattice>& State) {
+            transferNullCheckComparison(
+                binOp, result.Nodes.getNodeAs<Expr>("pointer"), State);
+          })
+      .CaseOf<Expr>(isImplicitCastPtrToBool(),
+                    transferNullCheckImplicitCastPtrToBool)
+      .Build();
+}
+}  // namespace
+
+PointerNullabilityAnalysis::PointerNullabilityAnalysis(ASTContext& Context)
+    : DataflowAnalysis<PointerNullabilityAnalysis, PointerNullabilityLattice>(
+          Context),
+      Transferer(buildTransferer()) {}
+
+void PointerNullabilityAnalysis::transfer(const Stmt* Stmt,
+                                          PointerNullabilityLattice& Lattice,
+                                          Environment& Env) {
+  TransferState<PointerNullabilityLattice> State(Lattice, Env);
+  Transferer(*Stmt, getASTContext(), State);
+}
+
+bool PointerNullabilityAnalysis::merge(QualType Type, const Value& Val1,
+                                       const Environment& Env1,
+                                       const Value& Val2,
+                                       const Environment& Env2,
+                                       Value& MergedVal,
+                                       Environment& MergedEnv) {
+  return false;
+}
+}  // namespace nullability
+}  // namespace tidy
+}  // namespace clang
diff --git a/nullability_verification/pointer_nullability_analysis.h b/nullability_verification/pointer_nullability_analysis.h
new file mode 100644
index 0000000..f15c358
--- /dev/null
+++ b/nullability_verification/pointer_nullability_analysis.h
@@ -0,0 +1,54 @@
+// Part of the Crubit project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+#ifndef CRUBIT_NULLABILITY_VERIFICATION_POINTER_NULLABILITY_ANALYSIS_H_
+#define CRUBIT_NULLABILITY_VERIFICATION_POINTER_NULLABILITY_ANALYSIS_H_
+
+#include "nullability_verification/pointer_nullability_lattice.h"
+#include "clang/AST/ASTContext.h"
+#include "clang/AST/Expr.h"
+#include "clang/AST/Stmt.h"
+#include "clang/AST/Type.h"
+#include "clang/Analysis/FlowSensitive/DataflowAnalysis.h"
+#include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
+#include "clang/Analysis/FlowSensitive/DataflowLattice.h"
+#include "clang/Analysis/FlowSensitive/MatchSwitch.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
+#include "clang/Tooling/Tooling.h"
+
+namespace clang {
+namespace tidy {
+namespace nullability {
+
+// Current iteration marks lattice unsafe if there exists a pointer
+// dereference
+// TODO(b/233582219): Implement tracking of nullability to distinguish
+// safe/unsafe accesses
+
+class PointerNullabilityAnalysis
+    : public dataflow::DataflowAnalysis<PointerNullabilityAnalysis,
+                                        PointerNullabilityLattice> {
+ public:
+  explicit PointerNullabilityAnalysis(ASTContext& context);
+
+  static PointerNullabilityLattice initialElement() { return {}; }
+
+  void transfer(const Stmt* Stmt, PointerNullabilityLattice& Lattice,
+                dataflow::Environment& Env);
+
+  bool merge(QualType Type, const dataflow::Value& Val1,
+             const dataflow::Environment& Env1, const dataflow::Value& Val2,
+             const dataflow::Environment& Env2, dataflow::Value& MergedVal,
+             dataflow::Environment& MergedEnv) override;
+
+ private:
+  // Applies transfer functions on statements
+  dataflow::MatchSwitch<dataflow::TransferState<PointerNullabilityLattice>>
+      Transferer;
+};
+}  // namespace nullability
+}  // namespace tidy
+}  // namespace clang
+
+#endif  // CRUBIT_NULLABILITY_VERIFICATION_POINTER_NULLABILITY_ANALYSIS_H_
diff --git a/nullability_verification/pointer_nullability_analysis_test.cc b/nullability_verification/pointer_nullability_analysis_test.cc
new file mode 100644
index 0000000..a8ff6c1
--- /dev/null
+++ b/nullability_verification/pointer_nullability_analysis_test.cc
@@ -0,0 +1,151 @@
+// Part of the Crubit project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+#include "nullability_verification/pointer_nullability_analysis.h"
+
+#include <string>
+
+#include "third_party/llvm/llvm-project/clang/unittests/Analysis/FlowSensitive/TestingSupport.h"
+#include "llvm/ADT/ArrayRef.h"
+#include "llvm/ADT/StringRef.h"
+#include "llvm/Support/Error.h"
+#include "llvm/Testing/Support/Error.h"
+#include "third_party/llvm/llvm-project/llvm/utils/unittest/googlemock/include/gmock/gmock.h"
+#include "third_party/llvm/llvm-project/llvm/utils/unittest/googletest/include/gtest/gtest.h"
+
+namespace clang {
+namespace tidy {
+namespace nullability {
+namespace {
+
+using ::testing::Pair;
+using ::testing::Test;
+using ::testing::UnorderedElementsAre;
+
+using dataflow::DataflowAnalysisState;
+using dataflow::Environment;
+using dataflow::test::checkDataflow;
+
+MATCHER(IsSafe, "") { return arg.Lattice.isSafe(); }
+MATCHER(IsUnsafe, "") { return !arg.Lattice.isSafe(); }
+
+class PointerNullabilityTest : public Test {
+ protected:
+  template <typename Matcher>
+  void expectDataflow(llvm::StringRef Code, Matcher Expectations) {
+    ASSERT_THAT_ERROR(
+        checkDataflow<PointerNullabilityAnalysis>(
+            Code, "target",
+            [](ASTContext& ASTCtx, Environment&) {
+              return PointerNullabilityAnalysis(ASTCtx);
+            },
+            [&Expectations](
+                llvm::ArrayRef<
+                    std::pair<std::string,
+                              DataflowAnalysisState<PointerNullabilityLattice>>>
+                    Results,
+                ASTContext&) { EXPECT_THAT(Results, Expectations); },
+            {"-fsyntax-only", "-std=c++17"}),
+        llvm::Succeeded());
+  }
+};
+
+TEST_F(PointerNullabilityTest, SafeNoOp) {
+  std::string Code = R"(
+    void target(int* maybeNull) {
+      1 + 2;
+      /*[[check]]*/
+    }
+  )";
+  expectDataflow(Code, UnorderedElementsAre(Pair("check", IsSafe())));
+}
+
+TEST_F(PointerNullabilityTest, UnsafeUnchecked) {
+  std::string Code = R"(
+    void target(int* maybeNull) {
+      *maybeNull;
+      /*[[check]]*/
+    }
+  )";
+  expectDataflow(Code, UnorderedElementsAre(Pair("check", IsUnsafe())));
+}
+
+TEST_F(PointerNullabilityTest, SafeCheckNEQNull) {
+  std::string NullLiteralOnRight = R"(
+    void target(int* maybeNull) {
+      if (maybeNull != nullptr) {
+        *maybeNull;
+        /*[[check-safe]]*/
+      } else {
+        *maybeNull;
+        /*[[check-unsafe1]]*/
+      }
+      *maybeNull;
+      /*[[check-unsafe2]]*/
+    }
+  )";
+  expectDataflow(NullLiteralOnRight,
+                 UnorderedElementsAre(Pair("check-safe", IsSafe()),
+                                      Pair("check-unsafe1", IsUnsafe()),
+                                      Pair("check-unsafe2", IsUnsafe())));
+
+  std::string NullLiteralOnLeft = R"(
+    void target(int* maybeNull) {
+      if (nullptr != maybeNull) {
+        *maybeNull;
+        /*[[check-safe]]*/
+      } else {
+        *maybeNull;
+        /*[[check-unsafe1]]*/
+      }
+      *maybeNull;
+      /*[[check-unsafe2]]*/
+    }
+  )";
+  expectDataflow(NullLiteralOnLeft,
+                 UnorderedElementsAre(Pair("check-safe", IsSafe()),
+                                      Pair("check-unsafe1", IsUnsafe()),
+                                      Pair("check-unsafe2", IsUnsafe())));
+}
+
+TEST_F(PointerNullabilityTest, SafeCheckImplicitCastToBool) {
+  std::string Code = R"(
+    void target(int* maybeNull) {
+      if (maybeNull) {
+        *maybeNull;
+        /*[[check-safe]]*/
+      } else {
+        *maybeNull;
+        /*[[check-unsafe1]]*/
+      }
+      *maybeNull;
+      /*[[check-unsafe2]]*/
+    }
+  )";
+  expectDataflow(Code, UnorderedElementsAre(Pair("check-safe", IsSafe()),
+                                            Pair("check-unsafe1", IsUnsafe()),
+                                            Pair("check-unsafe2", IsUnsafe())));
+  std::string NegatedCondition = R"(
+    void target(int* maybeNull) {
+      if (!maybeNull) {
+        *maybeNull;
+        /*[[check-unsafe1]]*/
+      } else {
+        *maybeNull;
+        /*[[check-safe]]*/
+      }
+      *maybeNull;
+      /*[[check-unsafe2]]*/
+    }
+  )";
+  expectDataflow(NegatedCondition,
+                 UnorderedElementsAre(Pair("check-safe", IsSafe()),
+                                      Pair("check-unsafe1", IsUnsafe()),
+                                      Pair("check-unsafe2", IsUnsafe())));
+}
+
+}  // namespace
+}  // namespace nullability
+}  // namespace tidy
+}  // namespace clang
diff --git a/nullability_verification/pointer_nullability_lattice.h b/nullability_verification/pointer_nullability_lattice.h
new file mode 100644
index 0000000..917e075
--- /dev/null
+++ b/nullability_verification/pointer_nullability_lattice.h
@@ -0,0 +1,61 @@
+// Part of the Crubit project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+#ifndef CRUBIT_NULLABILITY_VERIFICATION_POINTER_NULLABILITY_LATTICE_H_
+#define CRUBIT_NULLABILITY_VERIFICATION_POINTER_NULLABILITY_LATTICE_H_
+
+#include <ostream>
+
+#include "clang/Analysis/FlowSensitive/DataflowLattice.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
+#include "llvm/ADT/DenseMap.h"
+#include "llvm/ADT/DenseSet.h"
+
+namespace clang {
+namespace tidy {
+namespace nullability {
+class PointerNullabilityLattice {
+ public:
+  PointerNullabilityLattice() = default;
+
+  bool operator==(const PointerNullabilityLattice& Other) const { return true; }
+
+  dataflow::LatticeJoinEffect join(const PointerNullabilityLattice& Other) {
+    return dataflow::LatticeJoinEffect::Unchanged;
+  }
+
+  bool hasPointerNullability(clang::dataflow::PointerValue* PointerVal) {
+    return pointer_nullabilities_.find(PointerVal) !=
+           pointer_nullabilities_.end();
+  }
+
+  dataflow::BoolValue* getPointerNullability(
+      dataflow::PointerValue* PointerVal) {
+    auto search = pointer_nullabilities_.find(PointerVal);
+    return search == pointer_nullabilities_.end() ? nullptr : search->second;
+  }
+
+  void setPointerNullability(dataflow::PointerValue* PointerVal,
+                             dataflow::BoolValue* BoolVal) {
+    pointer_nullabilities_[PointerVal] = BoolVal;
+  }
+
+  bool isSafe() const { return violations_.empty(); }
+  void addViolation(const Expr* Violation) { violations_.insert(Violation); }
+
+ private:
+  llvm::DenseSet<const Expr*> violations_;
+  llvm::DenseMap<dataflow::PointerValue*, dataflow::BoolValue*>
+      pointer_nullabilities_;
+};
+
+inline std::ostream& operator<<(std::ostream& OS,
+                                const PointerNullabilityLattice& L) {
+  return OS << "Pointer Nullability Lattice";
+}
+}  // namespace nullability
+}  // namespace tidy
+}  // namespace clang
+
+#endif  // CRUBIT_NULLABILITY_VERIFICATION_POINTER_NULLABILITY_LATTICE_H_
diff --git a/nullability_verification/pointer_nullability_matchers.cc b/nullability_verification/pointer_nullability_matchers.cc
new file mode 100644
index 0000000..37c4266
--- /dev/null
+++ b/nullability_verification/pointer_nullability_matchers.cc
@@ -0,0 +1,49 @@
+// Part of the Crubit project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+#include "nullability_verification/pointer_nullability_matchers.h"
+
+#include "clang/ASTMatchers/ASTMatchers.h"
+#include "llvm/ADT/StringRef.h"
+
+namespace clang {
+namespace tidy {
+namespace nullability {
+
+using ast_matchers::binaryOperator;
+using ast_matchers::booleanType;
+using ast_matchers::expr;
+using ast_matchers::hasImplicitDestinationType;
+using ast_matchers::hasOperands;
+using ast_matchers::hasOperatorName;
+using ast_matchers::hasSourceExpression;
+using ast_matchers::hasType;
+using ast_matchers::hasUnaryOperand;
+using ast_matchers::ignoringImplicit;
+using ast_matchers::implicitCastExpr;
+using ast_matchers::isAnyPointer;
+using ast_matchers::nullPointerConstant;
+using ast_matchers::unaryOperator;
+using ast_matchers::internal::Matcher;
+
+Matcher<Stmt> isPointerExpr() { return expr(hasType(isAnyPointer())); }
+
+Matcher<Stmt> isPointerDereference() {
+  return unaryOperator(hasOperatorName("*"), hasUnaryOperand(isPointerExpr()));
+}
+
+Matcher<Stmt> isNEQNullBinOp(llvm::StringRef BindID) {
+  return binaryOperator(
+      hasOperatorName("!="),
+      hasOperands(ignoringImplicit(nullPointerConstant()),
+                  expr(hasType(isAnyPointer())).bind(BindID)));
+}
+
+Matcher<Stmt> isImplicitCastPtrToBool() {
+  return implicitCastExpr(hasSourceExpression(isPointerExpr()),
+                          hasImplicitDestinationType(booleanType()));
+}
+}  // namespace nullability
+}  // namespace tidy
+}  // namespace clang
diff --git a/nullability_verification/pointer_nullability_matchers.h b/nullability_verification/pointer_nullability_matchers.h
new file mode 100644
index 0000000..ed30a23
--- /dev/null
+++ b/nullability_verification/pointer_nullability_matchers.h
@@ -0,0 +1,23 @@
+// Part of the Crubit project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+#ifndef CRUBIT_NULLABILITY_VERIFICATION_POINTER_NULLABILITY_MATCHERS_H_
+#define CRUBIT_NULLABILITY_VERIFICATION_POINTER_NULLABILITY_MATCHERS_H_
+
+#include "clang/ASTMatchers/ASTMatchersInternal.h"
+
+namespace clang {
+namespace tidy {
+namespace nullability {
+
+ast_matchers::internal::Matcher<Stmt> isPointerExpr();
+ast_matchers::internal::Matcher<Stmt> isPointerDereference();
+ast_matchers::internal::Matcher<Stmt> isNEQNullBinOp(llvm::StringRef BindID);
+ast_matchers::internal::Matcher<Stmt> isImplicitCastPtrToBool();
+
+}  // namespace nullability
+}  // namespace tidy
+}  // namespace clang
+
+#endif  // CRUBIT_NULLABILITY_VERIFICATION_POINTER_NULLABILITY_MATCHERS_H_