diff --git a/Examples/SarifTest.boogie.st b/Examples/SarifTest.boogie.st
new file mode 100644
index 000000000..f7270b1da
--- /dev/null
+++ b/Examples/SarifTest.boogie.st
@@ -0,0 +1,13 @@
+program Boogie;
+
+// Simple test program for SARIF output
+procedure AddPositive(x : int, y : int) returns (z : int)
+spec {
+  requires [x_positive]: (x > 0);
+  requires [y_positive]: (y > 0);
+  ensures [result_positive]: (z > 0);
+  ensures [result_sum]: (z == x + y);
+}
+{
+  z := x + y;
+};
diff --git a/Strata.lean b/Strata.lean
index 5c5225eef..798e6b8b1 100644
--- a/Strata.lean
+++ b/Strata.lean
@@ -15,8 +15,12 @@ import Strata.DL.SMT.SMT
 import Strata.DL.Lambda.Lambda
 import Strata.DL.Imperative.Imperative
 
+/- Utilities -/
+import Strata.Util.Sarif
+
 /- Boogie -/
 import Strata.Languages.Boogie.StatementSemantics
+import Strata.Languages.Boogie.SarifOutput
 
 /- Code Transforms -/
 import Strata.Transform.CallElimCorrect
diff --git a/Strata/Languages/Boogie/Options.lean b/Strata/Languages/Boogie/Options.lean
index 042feea1d..4f22665b1 100644
--- a/Strata/Languages/Boogie/Options.lean
+++ b/Strata/Languages/Boogie/Options.lean
@@ -13,6 +13,8 @@ structure Options where
   removeIrrelevantAxioms : Bool
   /-- Solver time limit in seconds -/
   solverTimeout : Nat
+  /-- Output results in SARIF format -/
+  outputSarif : Bool
 
 def Options.default : Options := {
   verbose := true,
@@ -21,7 +23,8 @@ def Options.default : Options := {
   checkOnly := false,
   stopOnFirstError := false,
   removeIrrelevantAxioms := false,
-  solverTimeout := 10
+  solverTimeout := 10,
+  outputSarif := false
 }
 
 instance : Inhabited Options where
diff --git a/Strata/Languages/Boogie/SarifOutput.lean b/Strata/Languages/Boogie/SarifOutput.lean
new file mode 100644
index 000000000..fa4f6156e
--- /dev/null
+++ b/Strata/Languages/Boogie/SarifOutput.lean
@@ -0,0 +1,85 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.Languages.Boogie.Verifier
+import Strata.Util.Sarif
+
+/-!
+# Boogie SARIF Output
+
+This module provides Boogie-specific conversion functions for SARIF output.
+-/
+
+namespace Boogie.Sarif
+
+open Strata.Sarif Strata.SMT
+
+/-! ## Boogie-Specific Conversion Functions -/
+
+/-- Convert Boogie Outcome to SARIF Level -/
+def outcomeToLevel : Outcome → Level
+  | .pass => .none
+  | .fail => .error
+  | .unknown => .warning
+  | .implementationError _ => .error
+
+/-- Convert Boogie Outcome to a descriptive message -/
+def outcomeToMessage (outcome : Outcome) (smtResult : SMT.Result) : String :=
+  match outcome with
+  | .pass => "Verification succeeded"
+  | .fail =>
+    match smtResult with
+    | .sat m =>
+      if m.isEmpty then
+        "Verification failed"
+      else
+        s!"Verification failed with counterexample: {Std.format m}"
+    | _ => "Verification failed"
+  | .unknown => "Verification result unknown (solver timeout or incomplete)"
+  | .implementationError msg => s!"Verification error: {msg}"
+
+/-- Extract location information from metadata -/
+def extractLocation (md : Imperative.MetaData Expression) : Option Location := do
+  let fileRangeElem ← md.findElem Imperative.MetaData.fileRange
+  match fileRangeElem.value with
+  | .fileRange fr =>
+    let uri := match fr.file with
+               | .file path => path
+    pure { uri, startLine := fr.start.line, startColumn := fr.start.column }
+  | _ => none
+
+/-- Convert a VCResult to a SARIF Result -/
+def vcResultToSarifResult (vcr : VCResult) : Strata.Sarif.Result :=
+  let ruleId := vcr.obligation.label
+  let level := outcomeToLevel vcr.result
+  let messageText := outcomeToMessage vcr.result vcr.smtResult
+  let message : Strata.Sarif.Message := { text := messageText }
+
+  let locations := match extractLocation vcr.obligation.metadata with
+    | some loc => #[locationToSarif loc]
+    | none => #[]
+
+  { ruleId, level, message, locations }
+
+/-- Convert VCResults to a SARIF document -/
+def vcResultsToSarif (vcResults : VCResults) : Strata.Sarif.SarifDocument :=
+  let tool : Strata.Sarif.Tool := {
+    driver := {
+      name := "Strata",
+      version := "0.1.0",
+      informationUri := "https://github.com/strata-org/Strata"
+    }
+  }
+
+  let results := vcResults.map vcResultToSarifResult
+
+  let run : Strata.Sarif.Run := { tool, results }
+
+  { version := "2.1.0",
+    schema := "https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json",
+    runs := #[run] }
+
+end Boogie.Sarif
diff --git a/Strata/Util/Sarif.lean b/Strata/Util/Sarif.lean
new file mode 100644
index 000000000..ff4bb51df
--- /dev/null
+++ b/Strata/Util/Sarif.lean
@@ -0,0 +1,142 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Lean.Data.Json
+
+/-!
+# SARIF Output
+
+This module provides support for outputting results in SARIF
+(Static Analysis Results Interchange Format) version 2.1.0.
+
+SARIF specification: https://docs.oasis-open.org/sarif/sarif/v2.1.0/sarif-v2.1.0.html
+-/
+
+namespace Strata.Sarif
+
+open Lean (Json ToJson FromJson)
+
+/-! ## SARIF Data Structures -/
+
+/-- SARIF location representing a position in source code -/
+structure Location where
+  uri : String
+  startLine : Nat
+  startColumn : Nat
+  deriving Repr, ToJson, FromJson, BEq
+
+/-- SARIF artifact location representing a file URI -/
+structure ArtifactLocation where
+  uri : String
+  deriving Repr, ToJson, FromJson
+
+/-- SARIF region representing a source code region with line and column information -/
+structure Region where
+  startLine : Nat
+  startColumn : Nat
+  deriving Repr, ToJson, FromJson
+
+/-- SARIF physical location with region information -/
+structure PhysicalLocation where
+  artifactLocation : ArtifactLocation
+  region : Region
+  deriving Repr, ToJson, FromJson
+
+/-- SARIF location wrapper -/
+structure SarifLocation where
+  physicalLocation : PhysicalLocation
+  deriving Repr, ToJson, FromJson
+
+/-- SARIF message -/
+structure Message where
+  text : String
+  deriving Repr, ToJson, FromJson
+
+/-- SARIF result level -/
+inductive Level where
+  | none     -- Verification passed
+  | note     -- Informational
+  | warning  -- Unknown result or potential issue
+  | error    -- Verification failed
+  deriving Repr, DecidableEq
+
+instance : ToString Level where
+  toString
+  | .none => "none"
+  | .note => "note"
+  | .warning => "warning"
+  | .error => "error"
+
+instance : ToJson Level where
+  toJson level := Json.str (toString level)
+
+instance : FromJson Level where
+  fromJson? j := do
+    let s ← j.getStr?
+    match s with
+    | "none" => pure .none
+    | "note" => pure .note
+    | "warning" => pure .warning
+    | "error" => pure .error
+    | _ => throw s!"Invalid SARIF level: {s}"
+
+/-- SARIF result representing a single verification result -/
+structure Result where
+  ruleId : String
+  level : Level
+  message : Message
+  locations : Array SarifLocation := #[]
+  deriving Repr, ToJson, FromJson
+
+instance : Inhabited Result where
+  default := { ruleId := "", level := .none, message := { text := "" } }
+
+/-- SARIF tool driver information -/
+structure Driver where
+  name : String
+  version : String := "0.1.0"
+  informationUri : String := "https://github.com/strata-org/Strata"
+  deriving Repr, ToJson, FromJson, Inhabited
+
+/-- SARIF tool information -/
+structure Tool where
+  driver : Driver
+  deriving Repr, ToJson, FromJson, Inhabited
+
+/-- SARIF run representing a single analysis run -/
+structure Run where
+  tool : Tool
+  results : Array Result
+  deriving Repr, ToJson, FromJson
+
+instance : Inhabited Run where
+  default := { tool := default, results := #[] }
+
+/-- Top-level SARIF document -/
+structure SarifDocument where
+  version : String := "2.1.0"
+  /-- Schema URI as specified by SARIF 2.1.0 -/
+  schema : String := "https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json"
+  runs : Array Run
+  deriving Repr, ToJson, FromJson
+
+/-! ## Utility Functions -/
+
+/-- Convert a location to SARIF format -/
+def locationToSarif (loc : Location) : SarifLocation :=
+  let artifactLocation : ArtifactLocation := { uri := loc.uri }
+  let region : Region := { startLine := loc.startLine, startColumn := loc.startColumn }
+  { physicalLocation := { artifactLocation, region } }
+
+/-- Convert SARIF document to JSON string -/
+def toJsonString (sarif : SarifDocument) : String :=
+  Json.compress (ToJson.toJson sarif)
+
+/-- Convert SARIF document to pretty-printed JSON string -/
+def toPrettyJsonString (sarif : SarifDocument) : String :=
+  Json.pretty (ToJson.toJson sarif)
+
+end Strata.Sarif
diff --git a/StrataTest/Languages/Boogie/SarifOutputTests.lean b/StrataTest/Languages/Boogie/SarifOutputTests.lean
new file mode 100644
index 000000000..6c6800593
--- /dev/null
+++ b/StrataTest/Languages/Boogie/SarifOutputTests.lean
@@ -0,0 +1,268 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.Languages.Boogie.SarifOutput
+import Strata.Languages.Boogie.Verifier
+import Lean.Data.Json
+
+/-!
+# SARIF Output Tests
+
+This file contains tests for the SARIF output functionality, including:
+- SARIF JSON structure validation
+- VCResult to SARIF conversion
+- Various verification result types (success, failure, error, unknown)
+- Source location mapping
+-/
+
+namespace Boogie.Sarif.Tests
+
+open Lean (Json)
+open Imperative
+open Strata.Sarif (Level Message)
+open Boogie.SMT (SMTModel Result)
+
+/-! ## Test Helpers -/
+
+/-- Create a simple metadata with file and location information -/
+def makeMetadata (file : String) (line col : Nat) : MetaData Expression :=
+  let uri := Imperative.Uri.file file
+  let pos : Lean.Position := { line := line, column := col }
+  let fr : Imperative.FileRange := { file := uri, start := pos, ending := pos }
+  #[{ fld := Imperative.MetaData.fileRange, value := .fileRange fr }]
+
+/-- Create a simple proof obligation for testing -/
+def makeObligation (label : String) (md : MetaData Expression := #[]) : ProofObligation Expression :=
+  { label := label
+    property := .assert
+    assumptions := []
+    obligation := Lambda.LExpr.boolConst () true
+    metadata := md }
+
+/-- Create a VCResult for testing -/
+def makeVCResult (label : String) (outcome : Outcome) (smtResult : Result := .unknown) (md : MetaData Expression := #[]) : VCResult :=
+  { obligation := makeObligation label md
+    smtResult := smtResult
+    result := outcome
+    verbose := true }
+
+/-! ## Level Conversion Tests -/
+
+-- Test that pass (verified) maps to "none" level
+#guard outcomeToLevel .pass = Level.none
+
+-- Test that fail maps to "error" level
+#guard outcomeToLevel .fail = Level.error
+
+-- Test that unknown maps to "warning" level
+#guard outcomeToLevel .unknown = Level.warning
+
+-- Test that implementationError maps to "error" level
+#guard outcomeToLevel (.implementationError "test error") = Level.error
+
+/-! ## Message Generation Tests -/
+
+-- Test pass message
+#guard outcomeToMessage .pass .unknown = "Verification succeeded"
+
+-- Test fail message without counterexample
+#guard outcomeToMessage .fail .unknown = "Verification failed"
+
+-- Test unknown message
+#guard (outcomeToMessage .unknown .unknown).startsWith "Verification result unknown"
+
+-- Test error message
+#guard (outcomeToMessage (.implementationError "test error") .unknown).startsWith "Verification error:"
+
+/-! ## Location Extraction Tests -/
+
+-- Test location extraction from complete metadata
+#guard_msgs in
+#eval
+  let md := makeMetadata "/test/file.st" 10 5
+  let loc? := extractLocation md
+  match loc? with
+  | some loc =>
+    if loc.uri = "/test/file.st" && loc.startLine = 10 && loc.startColumn = 5 then
+      pure ()
+    else
+      IO.println s!"Location extraction test failed: uri={loc.uri} line={loc.startLine} col={loc.startColumn}"
+  | none => IO.println "Location extraction test failed: no location"
+
+-- Test location extraction from empty metadata
+#guard (extractLocation #[] == none)
+
+-- Test location extraction from metadata with wrong value type
+#guard
+  let md : MetaData Expression := #[
+    { fld := Imperative.MetaData.fileRange, value := .msg "not a fileRange" }
+  ]
+  (extractLocation md == none)
+
+/-! ## VCResult to SARIF Conversion Tests -/
+
+-- Test converting a successful VCResult
+#guard_msgs in
+#eval
+  let md := makeMetadata "/test/file.st" 10 5
+  let vcr := makeVCResult "test_obligation" .pass .unsat md
+  let sarifResult := vcResultToSarifResult vcr
+  if sarifResult.ruleId = "test_obligation" &&
+     sarifResult.level = Level.none &&
+     sarifResult.locations.size = 1 then
+    pure ()
+  else
+    IO.println s!"Successful VCResult conversion test failed: {repr sarifResult}"
+
+-- Test converting a failed VCResult
+#guard_msgs in
+#eval
+  let md := makeMetadata "/test/file.st" 20 10
+  let vcr := makeVCResult "failed_obligation" .fail (.sat []) md
+  let sarifResult := vcResultToSarifResult vcr
+  if sarifResult.ruleId = "failed_obligation" &&
+     sarifResult.level = Level.error &&
+     sarifResult.message.text = "Verification failed" then
+    pure ()
+  else
+    IO.println s!"Failed VCResult conversion test failed: {repr sarifResult}"
+
+-- Test converting an unknown VCResult
+#guard_msgs in
+#eval
+  let vcr := makeVCResult "unknown_obligation" .unknown
+  let sarifResult := vcResultToSarifResult vcr
+  if sarifResult.ruleId = "unknown_obligation" &&
+     sarifResult.level = Level.warning &&
+     sarifResult.locations.size = 0 then
+    pure ()
+  else
+    IO.println s!"Unknown VCResult conversion test failed: {repr sarifResult}"
+
+-- Test converting an error VCResult
+#guard_msgs in
+#eval
+  let vcr := makeVCResult "error_obligation" (.implementationError "SMT solver error")
+  let sarifResult := vcResultToSarifResult vcr
+  if sarifResult.ruleId = "error_obligation" &&
+     sarifResult.level = Level.error &&
+     (sarifResult.message.text.startsWith "Verification error:") then
+    pure ()
+  else
+    IO.println s!"Error VCResult conversion test failed: {repr sarifResult}"
+
+/-! ## SARIF Document Structure Tests -/
+
+#guard_msgs in
+#eval
+  let vcResults : VCResults := #[]
+  let sarif := vcResultsToSarif vcResults
+  if sarif.version = "2.1.0" &&
+     sarif.runs.size = 1 &&
+     sarif.runs[0]!.results.size = 0 &&
+     sarif.runs[0]!.tool.driver.name = "Strata" then
+    pure ()
+  else
+    IO.println s!"Empty SARIF document test failed"
+
+-- Test creating a SARIF document with multiple VCResults
+#guard_msgs in
+#eval
+  let md1 := makeMetadata "/test/file1.st" 10 5
+  let md2 := makeMetadata "/test/file2.st" 20 10
+  let vcResults : VCResults := #[
+    makeVCResult "obligation1" .pass .unsat md1,
+    makeVCResult "obligation2" .fail (.sat []) md2,
+    makeVCResult "obligation3" .unknown
+  ]
+  let sarif := vcResultsToSarif vcResults
+  if sarif.version = "2.1.0" &&
+     sarif.runs.size = 1 &&
+     sarif.runs[0]!.results.size = 3 &&
+     sarif.runs[0]!.results[0]!.level = Level.none &&
+     sarif.runs[0]!.results[1]!.level = Level.error &&
+     sarif.runs[0]!.results[2]!.level = Level.warning then
+    pure ()
+  else
+    IO.println s!"Multiple VCResults SARIF document test failed"
+
+/-! ## JSON Serialization Tests -/
+
+#guard_msgs in
+#eval
+  let json := Lean.ToJson.toJson Level.none
+  match json with
+  | Json.str "none" => pure ()
+  | _ => IO.println s!"Level serialization test failed: {json}"
+
+#guard_msgs in
+#eval
+  let msg : Message := { text := "Test message" }
+  let _ := Lean.ToJson.toJson msg
+  -- Just check that it serializes without error
+  pure ()
+
+-- Test full SARIF document JSON generation
+#guard_msgs in
+#eval
+  let md := makeMetadata "/test/example.st" 15 7
+  let vcResults : VCResults := #[
+    makeVCResult "test_assertion" .pass .unsat md
+  ]
+  let sarif := vcResultsToSarif vcResults
+  let jsonStr := Strata.Sarif.toJsonString sarif
+
+  -- Check that the JSON contains expected fields
+  if (jsonStr.splitOn "\"version\":\"2.1.0\"").length > 1 &&
+     (jsonStr.splitOn "\"Strata\"").length > 1 &&
+     (jsonStr.splitOn "test_assertion").length > 1 then
+    pure ()
+  else
+    IO.println s!"SARIF document JSON generation test failed"
+
+-- Test pretty JSON generation
+#guard_msgs in
+#eval
+  let vcResults : VCResults := #[
+    makeVCResult "simple_test" .pass
+  ]
+  let sarif := vcResultsToSarif vcResults
+  let prettyJson := Strata.Sarif.toPrettyJsonString sarif
+
+  -- Pretty JSON should contain newlines for formatting
+  if prettyJson.contains '\n' then
+    pure ()
+  else
+    IO.println s!"Pretty JSON generation test failed"
+
+/-! ## Integration Test with Counter-Examples -/
+
+-- Test SARIF output with counter-example
+#guard_msgs in
+#eval
+  let cex : SMTModel := [((BoogieIdent.unres "x", some .int), "42")]
+  let md := makeMetadata "/test/cex.st" 25 3
+  let vcr := makeVCResult "cex_obligation" .fail (.sat cex) md
+  let sarifResult := vcResultToSarifResult vcr
+
+  if sarifResult.level = Level.error &&
+     (sarifResult.message.text.splitOn "counterexample").length > 1 &&
+     sarifResult.locations.size = 1 then
+    pure ()
+  else
+    IO.println s!"Counter-example SARIF test failed: {repr sarifResult}"
+
+/-! ## Schema URI Test -/
+
+#guard_msgs in
+#eval
+  let sarif := vcResultsToSarif #[]
+  if sarif.schema = "https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json" then
+    pure ()
+  else
+    IO.println s!"Schema URI test failed: {sarif.schema}"
+
+end Boogie.Sarif.Tests
diff --git a/StrataVerify.lean b/StrataVerify.lean
index ff7aef041..7c7d8a161 100644
--- a/StrataVerify.lean
+++ b/StrataVerify.lean
@@ -6,6 +6,7 @@
 
 -- Executable for verifying a Strata program from a file.
 import Strata.Languages.Boogie.Verifier
+import Strata.Languages.Boogie.SarifOutput
 import Strata.Languages.C_Simp.Verify
 import Strata.Util.IO
 import Std.Internal.Parsec
@@ -21,6 +22,8 @@ def parseOptions (args : List String) : Except Std.Format (Options × String) :=
       | opts, "--type-check" :: rest => go {opts with typeCheckOnly := true} rest
       | opts, "--parse-only" :: rest => go {opts with parseOnly := true} rest
       | opts, "--stop-on-first-error" :: rest => go {opts with stopOnFirstError := true} rest
+      | opts, "--sarif" :: rest => go {opts with outputSarif := true} rest
+      | opts, "--output-format=sarif" :: rest => go {opts with outputSarif := true} rest
       | opts, "--solver-timeout" :: secondsStr :: rest =>
          let n? := String.toNat? secondsStr
          match n? with
@@ -40,7 +43,9 @@ def usageMessage : Std.Format :=
   --type-check                Exit after semantic dialect's type inference/checking.{Std.Format.line}  \
   --parse-only                Exit after DDM parsing and type checking.{Std.Format.line}  \
   --stop-on-first-error       Exit after the first verification error.{Std.Format.line}  \
-  --solver-timeout <seconds>  Set the solver time limit per proof goal."
+  --solver-timeout <seconds>  Set the solver time limit per proof goal.{Std.Format.line}  \
+  --sarif                     Output results in SARIF format to <file>.sarif{Std.Format.line}  \
+  --output-format=sarif       Output results in SARIF format to <file>.sarif"
 
 def main (args : List String) : IO UInt32 := do
   let parseResult := parseOptions args
@@ -79,6 +84,26 @@ def main (args : List String) : IO UInt32 := do
         catch e =>
           println! f!"{e}"
           return (1 : UInt32)
+
+        -- Output in SARIF format if requested
+        if opts.outputSarif then
+          -- Skip SARIF generation for C_Simp files because the translation from C_Simp to
+          -- Boogie discards metadata (file, line, column information), making SARIF output
+          -- less useful. The vcResultsToSarif function would work type-wise (both produce
+          -- Boogie.VCResults), but the resulting SARIF would lack location information.
+          if file.endsWith ".csimp.st" then
+            println! "SARIF output is not supported for C_Simp files (.csimp.st) because location metadata is not preserved during translation to Boogie."
+          else
+            let sarifDoc := Boogie.Sarif.vcResultsToSarif vcResults
+            let sarifJson := Strata.Sarif.toPrettyJsonString sarifDoc
+            let sarifFile := file ++ ".sarif"
+            try
+              IO.FS.writeFile sarifFile sarifJson
+              println! f!"SARIF output written to {sarifFile}"
+            catch e =>
+              println! f!"Error writing SARIF output to {sarifFile}: {e.toString}"
+
+        -- Also output standard format
         for vcResult in vcResults do
           let posStr := Imperative.MetaData.formatFileRangeD vcResult.obligation.metadata
           println! f!"{posStr} [{vcResult.obligation.label}]: {vcResult.result}"