diff --git a/src/dafny/ast.rs b/src/dafny/ast.rs
new file mode 100644
index 00000000..8b06a783
--- /dev/null
+++ b/src/dafny/ast.rs
@@ -0,0 +1,225 @@
+/// A full Dafny file emitted by the backend.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct File {
+    pub decls: Vec<Decl>,
+}
+
+/// Top-level Dafny declarations supported by the current backend.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub enum Decl {
+    Type(TypeDecl),
+    Function(FunctionDecl),
+    Method(MethodDecl),
+}
+
+/// A lightweight Dafny `type` declaration for an abstract HeyVL domain.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct TypeDecl {
+    pub name: String,
+}
+
+/// A Dafny `function` declaration, optionally with a definition body.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct FunctionDecl {
+    pub name: String,
+    pub params: Vec<Param>,
+    pub return_ty: Type,
+    pub body: Option<Expr>,
+}
+
+/// A Dafny `method` declaration with contracts and an optional body.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct MethodDecl {
+    pub axiom: bool,
+    pub name: String,
+    pub params: Vec<Param>,
+    pub returns: Vec<Param>,
+    pub requires: Vec<Expr>,
+    pub ensures: Vec<Expr>,
+    pub decreases_star: bool,
+    pub body: Option<Block>,
+}
+
+/// A sequence of Dafny statements surrounded by `{ ... }`.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct Block {
+    pub stmts: Vec<Stmt>,
+}
+
+/// The statement fragment the backend knows how to emit.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub enum Stmt {
+    Block(Block),
+    Var(VarDecl),
+    Assign(AssignStmt),
+    Call(CallStmt),
+    AssignCall(AssignCallStmt),
+    SuchThatAssign(SuchThatAssignStmt),
+    Assert(AssertStmt),
+    Assume(AssumeStmt),
+    If(IfStmt),
+    While(WhileStmt),
+}
+
+/// A Dafny local variable declaration.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct VarDecl {
+    pub name: String,
+    pub ty: Type,
+    pub init: VarInit,
+}
+
+/// The initialization forms used for local variables in emitted Dafny.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub enum VarInit {
+    Expr(Expr),
+    MethodCall { method: String, args: Vec<Expr> },
+    SuchThat(Expr),
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct AssignStmt {
+    pub lhs: String,
+    pub rhs: Expr,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct CallStmt {
+    pub method: String,
+    pub args: Vec<Expr>,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct AssignCallStmt {
+    pub lhs: Vec<String>,
+    pub method: String,
+    pub args: Vec<Expr>,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct SuchThatAssignStmt {
+    pub lhs: Vec<String>,
+    pub predicate: Expr,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct AssertStmt {
+    pub expr: Expr,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct AssumeStmt {
+    pub axiom: bool,
+    pub expr: Expr,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct IfStmt {
+    pub cond: Expr,
+    pub then_branch: Block,
+    pub else_branch: Block,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct WhileStmt {
+    pub cond: Expr,
+    pub invariants: Vec<Expr>,
+    pub decreases_star: bool,
+    pub body: Block,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct Param {
+    pub name: String,
+    pub ty: Type,
+}
+
+/// The minimal Dafny type fragment needed by the backend.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub enum Type {
+    Bool,
+    Int,
+    Nat,
+    Seq(Box<Type>),
+    Named(String),
+}
+
+/// The expression fragment shared by the lowering and pretty-printing passes.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub enum Expr {
+    Var(String),
+    BoolLit(bool),
+    NumberLit(String),
+    StringLit(String),
+    Call {
+        function: String,
+        args: Vec<Expr>,
+    },
+    Ite {
+        cond: Box<Expr>,
+        then_expr: Box<Expr>,
+        else_expr: Box<Expr>,
+    },
+    Binary {
+        op: BinaryOp,
+        lhs: Box<Expr>,
+        rhs: Box<Expr>,
+    },
+    Unary {
+        op: UnaryOp,
+        expr: Box<Expr>,
+    },
+    Quantified {
+        quantifier: Quantifier,
+        vars: Vec<QuantVar>,
+        triggers: Vec<Vec<Expr>>,
+        body: Box<Expr>,
+    },
+    SeqLen(Box<Expr>),
+    Index {
+        collection: Box<Expr>,
+        index: Box<Expr>,
+    },
+    Update {
+        collection: Box<Expr>,
+        index: Box<Expr>,
+        value: Box<Expr>,
+    },
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub enum BinaryOp {
+    Add,
+    Sub,
+    Mul,
+    Div,
+    Mod,
+    And,
+    Or,
+    Eq,
+    Lt,
+    Le,
+    Ne,
+    Ge,
+    Gt,
+    Impl,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub enum UnaryOp {
+    Not,
+    Parens,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub enum Quantifier {
+    Forall,
+    Exists,
+}
+
+/// A typed quantified variable in a Dafny quantifier.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct QuantVar {
+    pub name: String,
+    pub ty: Type,
+}
diff --git a/src/dafny/index.rs b/src/dafny/index.rs
new file mode 100644
index 00000000..024b9156
--- /dev/null
+++ b/src/dafny/index.rs
@@ -0,0 +1,152 @@
+use regex::Regex;
+
+use crate::{
+    ast::{
+        AxiomDecl, DeclKind, DeclRef, DomainDecl, DomainSpec, FileId, FuncDecl, Ident, ProcDecl,
+    },
+    driver::{
+        front::{Module, SourceUnit},
+        item::SourceUnitName,
+    },
+};
+
+/// A flattened reference to one declaration that may appear in an emitted file.
+#[derive(Clone)]
+pub(crate) enum FlatDeclRef {
+    Proc(DeclRef<ProcDecl>),
+    Domain(DeclRef<DomainDecl>),
+    Func(DeclRef<FuncDecl>),
+    Axiom(DeclRef<AxiomDecl>),
+}
+
+#[derive(Clone, Copy, PartialEq, Eq)]
+pub(crate) enum FlatDeclKind {
+    Proc,
+    Domain,
+    Func,
+    Axiom,
+}
+
+/// Metadata used to group and order declarations during file emission.
+#[derive(Clone)]
+pub(crate) struct FlatDeclRecord {
+    pub(crate) ident: Ident,
+    pub(crate) file_id: FileId,
+    pub(crate) kind: FlatDeclKind,
+    pub(crate) decl: FlatDeclRef,
+    pub(crate) source_name: Option<SourceUnitName>,
+}
+
+/// Lookup table from identifiers to the flattened declaration order used by the backend.
+pub(crate) struct DeclIndex {
+    pub(crate) ordered: Vec<FlatDeclRecord>,
+    by_ident: std::collections::HashMap<Ident, usize>,
+}
+
+impl DeclIndex {
+    /// Collect top-level and domain-nested declarations into a single stable order.
+    pub(crate) fn new(module: &Module) -> Self {
+        let mut ordered = Vec::new();
+        let mut by_ident = std::collections::HashMap::new();
+
+        for item in &module.items {
+            match &**item {
+                SourceUnit::Decl(DeclKind::ProcDecl(proc_ref)) => {
+                    let record = FlatDeclRecord {
+                        ident: proc_ref.borrow().name,
+                        file_id: proc_ref.borrow().span.file,
+                        kind: FlatDeclKind::Proc,
+                        decl: FlatDeclRef::Proc(proc_ref.clone()),
+                        source_name: Some(item.name().clone()),
+                    };
+                    by_ident.insert(record.ident, ordered.len());
+                    ordered.push(record);
+                }
+                SourceUnit::Decl(DeclKind::DomainDecl(domain_ref)) => {
+                    let domain = domain_ref.borrow();
+                    let file_id = domain.span.file;
+                    let record = FlatDeclRecord {
+                        ident: domain.name,
+                        file_id,
+                        kind: FlatDeclKind::Domain,
+                        decl: FlatDeclRef::Domain(domain_ref.clone()),
+                        source_name: None,
+                    };
+                    by_ident.insert(record.ident, ordered.len());
+                    ordered.push(record);
+
+                    for spec in &domain.body {
+                        let record = match spec {
+                            DomainSpec::Function(func_ref) => FlatDeclRecord {
+                                ident: func_ref.borrow().name,
+                                file_id,
+                                kind: FlatDeclKind::Func,
+                                decl: FlatDeclRef::Func(func_ref.clone()),
+                                source_name: None,
+                            },
+                            DomainSpec::Axiom(axiom_ref) => FlatDeclRecord {
+                                ident: axiom_ref.borrow().name,
+                                file_id,
+                                kind: FlatDeclKind::Axiom,
+                                decl: FlatDeclRef::Axiom(axiom_ref.clone()),
+                                source_name: None,
+                            },
+                        };
+                        by_ident.insert(record.ident, ordered.len());
+                        ordered.push(record);
+                    }
+                }
+                SourceUnit::Decl(DeclKind::FuncDecl(func_ref)) => {
+                    let record = FlatDeclRecord {
+                        ident: func_ref.borrow().name,
+                        file_id: func_ref.borrow().span.file,
+                        kind: FlatDeclKind::Func,
+                        decl: FlatDeclRef::Func(func_ref.clone()),
+                        source_name: None,
+                    };
+                    by_ident.insert(record.ident, ordered.len());
+                    ordered.push(record);
+                }
+                SourceUnit::Decl(DeclKind::AxiomDecl(axiom_ref)) => {
+                    let record = FlatDeclRecord {
+                        ident: axiom_ref.borrow().name,
+                        file_id: axiom_ref.borrow().span.file,
+                        kind: FlatDeclKind::Axiom,
+                        decl: FlatDeclRef::Axiom(axiom_ref.clone()),
+                        source_name: None,
+                    };
+                    by_ident.insert(record.ident, ordered.len());
+                    ordered.push(record);
+                }
+                SourceUnit::Decl(_) | SourceUnit::Raw(_) => {}
+            }
+        }
+
+        DeclIndex { ordered, by_ident }
+    }
+
+    pub(crate) fn get(&self, ident: Ident) -> Option<&FlatDeclRecord> {
+        self.by_ident.get(&ident).map(|index| &self.ordered[*index])
+    }
+
+    /// Return the selected top-level `proc` roots defined in one source file.
+    pub(crate) fn selected_roots_for_file(
+        &self,
+        file_id: FileId,
+        filter: Option<&Regex>,
+    ) -> Vec<Ident> {
+        self.ordered
+            .iter()
+            .filter(|record| {
+                record.kind == FlatDeclKind::Proc
+                    && record.file_id == file_id
+                    && record
+                        .source_name
+                        .as_ref()
+                        .map(|name| filter.is_none_or(|regex| regex.is_match(&name.to_string())))
+                        .unwrap_or(false)
+            })
+            .map(|record| record.ident)
+            .collect()
+    }
+}
diff --git a/src/dafny/lower.rs b/src/dafny/lower.rs
new file mode 100644
index 00000000..8fbb3b62
--- /dev/null
+++ b/src/dafny/lower.rs
@@ -0,0 +1,867 @@
+use std::collections::HashSet;
+
+use ariadne::ReportKind;
+
+use super::{
+    ast as dafny_ast,
+    index::{DeclIndex, FlatDeclKind, FlatDeclRecord, FlatDeclRef},
+};
+use crate::{
+    ast::{
+        BinOpKind, DeclKind, DeclRef, Diagnostic, Expr, ExprKind, FileId, FuncDecl, Ident, Label,
+        LitKind, Param, ProcDecl, ProcSpec, QuantOpKind, QuantVar, Span, Stmt, StmtKind, TyKind,
+        UnOpKind, VarDecl,
+    },
+    depgraph::DepGraph,
+    driver::error::CaesarError,
+    tyctx::TyCtx,
+};
+
+/// A lowering error that can be reported as a Caesar diagnostic at a precise source span.
+#[derive(Debug, Clone)]
+pub(crate) struct TranslationError {
+    span: Span,
+    message: String,
+    label: String,
+    note: Option<String>,
+}
+
+impl TranslationError {
+    pub(crate) fn unsupported(
+        span: Span,
+        message: impl Into<String>,
+        label: impl Into<String>,
+    ) -> Self {
+        TranslationError {
+            span,
+            message: message.into(),
+            label: label.into(),
+            note: None,
+        }
+    }
+
+    pub(crate) fn diagnostic(&self, kind: ReportKind<'static>) -> Diagnostic {
+        let diagnostic = Diagnostic::new(kind, self.span)
+            .with_message(&self.message)
+            .with_label(Label::new(self.span).with_message(&self.label));
+        if let Some(note) = &self.note {
+            diagnostic.with_note(note)
+        } else {
+            diagnostic
+        }
+    }
+}
+
+/// Stateful lowering context from surface HeyVL declarations to the internal Dafny AST.
+pub(crate) struct DafnyLowerer<'a> {
+    pub(crate) tcx: &'a TyCtx,
+    pub(crate) depgraph: &'a DepGraph,
+    pub(crate) index: &'a DeclIndex,
+}
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+enum SupportedListIntrinsic {
+    Len,
+    Select,
+    Store,
+}
+
+impl<'a> DafnyLowerer<'a> {
+    /// Check whether one locally declared item can be lowered by this backend.
+    pub(crate) fn local_support(&self, record: &FlatDeclRecord) -> Result<(), TranslationError> {
+        match &record.decl {
+            FlatDeclRef::Domain(_) => {
+                self.lower_domain(record)?;
+            }
+            FlatDeclRef::Func(func_ref) => {
+                self.lower_function(func_ref)?;
+            }
+            FlatDeclRef::Axiom(axiom_ref) => {
+                self.lower_axiom_expr(&axiom_ref.borrow().axiom)?;
+            }
+            FlatDeclRef::Proc(proc_ref) => {
+                self.lower_proc(proc_ref, &HashSet::new())?;
+            }
+        }
+        Ok(())
+    }
+
+    /// Lower the declarations selected for one source file into a Dafny AST file.
+    pub(crate) fn lower_file(
+        &self,
+        file_id: FileId,
+        roots: &[Ident],
+        included: &HashSet<Ident>,
+    ) -> Result<dafny_ast::File, CaesarError> {
+        let mut decls = Vec::new();
+
+        for record in self.index.ordered.iter().filter(|record| {
+            record.kind == FlatDeclKind::Domain && included.contains(&record.ident)
+        }) {
+            decls.push(dafny_ast::Decl::Type(self.lower_domain(record).map_err(
+                |err| CaesarError::Diagnostic(err.diagnostic(ReportKind::Error)),
+            )?));
+        }
+
+        for record in
+            self.index.ordered.iter().filter(|record| {
+                record.kind == FlatDeclKind::Func && included.contains(&record.ident)
+            })
+        {
+            let FlatDeclRef::Func(func_ref) = &record.decl else {
+                unreachable!();
+            };
+            decls.push(dafny_ast::Decl::Function(
+                self.lower_function(func_ref)
+                    .map_err(|err| CaesarError::Diagnostic(err.diagnostic(ReportKind::Error)))?,
+            ));
+        }
+
+        let root_set: HashSet<_> = roots.iter().copied().collect();
+        for record in self.index.ordered.iter().filter(|record| {
+            record.kind == FlatDeclKind::Proc
+                && included.contains(&record.ident)
+                && !root_set.contains(&record.ident)
+        }) {
+            let FlatDeclRef::Proc(proc_ref) = &record.decl else {
+                unreachable!();
+            };
+            decls.push(dafny_ast::Decl::Method(
+                self.lower_proc(proc_ref, included)
+                    .map_err(|err| CaesarError::Diagnostic(err.diagnostic(ReportKind::Error)))?,
+            ));
+        }
+
+        for record in self.index.ordered.iter().filter(|record| {
+            record.kind == FlatDeclKind::Proc
+                && record.file_id == file_id
+                && root_set.contains(&record.ident)
+        }) {
+            let FlatDeclRef::Proc(proc_ref) = &record.decl else {
+                unreachable!();
+            };
+            decls.push(dafny_ast::Decl::Method(
+                self.lower_proc(proc_ref, included)
+                    .map_err(|err| CaesarError::Diagnostic(err.diagnostic(ReportKind::Error)))?,
+            ));
+        }
+
+        Ok(dafny_ast::File { decls })
+    }
+
+    fn lower_domain(
+        &self,
+        record: &FlatDeclRecord,
+    ) -> Result<dafny_ast::TypeDecl, TranslationError> {
+        let FlatDeclRef::Domain(domain_ref) = &record.decl else {
+            unreachable!();
+        };
+        let domain = domain_ref.borrow();
+        Ok(dafny_ast::TypeDecl {
+            name: domain.name.name.to_owned(),
+        })
+    }
+
+    fn lower_function(
+        &self,
+        func_ref: &DeclRef<FuncDecl>,
+    ) -> Result<dafny_ast::FunctionDecl, TranslationError> {
+        let func = func_ref.borrow();
+        let body = {
+            let body = func.body.borrow();
+            body.as_ref()
+                .map(|expr| self.lower_expr(expr))
+                .transpose()?
+        };
+        Ok(dafny_ast::FunctionDecl {
+            name: func.name.name.to_owned(),
+            params: func
+                .inputs
+                .node
+                .iter()
+                .map(|param| self.lower_param(param))
+                .collect::<Result<Vec<_>, _>>()?,
+            return_ty: self.lower_type(&func.output, func.span)?,
+            body,
+        })
+    }
+
+    fn lower_proc(
+        &self,
+        proc_ref: &DeclRef<ProcDecl>,
+        included: &HashSet<Ident>,
+    ) -> Result<dafny_ast::MethodDecl, TranslationError> {
+        let proc = proc_ref.borrow();
+        if proc.direction != crate::ast::Direction::Down {
+            return Err(TranslationError::unsupported(
+                proc.span,
+                format!("Dafny: `coproc {}` is not supported", proc.name.name),
+                "expected `proc` here",
+            ));
+        }
+        if let Some(calculus) = proc.calculus {
+            let calculus_name = calculus.name.to_owned();
+            if calculus_name != "wp" && calculus_name != "ert" {
+                return Err(TranslationError::unsupported(
+                    calculus.span,
+                    format!("Dafny: calculus `@{}` is not supported", calculus.name),
+                    "expected no calculus, `@wp`, or `@ert`",
+                ));
+            }
+        }
+
+        let body = proc.body.borrow();
+        let mut method_body = None;
+        if let Some(block) = &*body {
+            let mut stmts = Vec::new();
+            let reachable = self.depgraph.get_reachable([proc.name]);
+            for record in &self.index.ordered {
+                if record.kind != FlatDeclKind::Axiom
+                    || !included.contains(&record.ident)
+                    || !reachable.contains(&record.ident)
+                {
+                    continue;
+                }
+                let FlatDeclRef::Axiom(axiom_ref) = &record.decl else {
+                    unreachable!();
+                };
+                stmts.push(dafny_ast::Stmt::Assume(dafny_ast::AssumeStmt {
+                    axiom: true,
+                    expr: self.lower_axiom_expr(&axiom_ref.borrow().axiom)?,
+                }));
+            }
+            stmts.extend(self.lower_block(block)?.stmts);
+            method_body = Some(dafny_ast::Block { stmts });
+        }
+
+        Ok(dafny_ast::MethodDecl {
+            axiom: body.is_none(),
+            name: proc.name.name.to_owned(),
+            params: proc
+                .inputs
+                .node
+                .iter()
+                .map(|param| self.lower_param(param))
+                .collect::<Result<Vec<_>, _>>()?,
+            returns: proc
+                .outputs
+                .node
+                .iter()
+                .map(|param| self.lower_param(param))
+                .collect::<Result<Vec<_>, _>>()?,
+            requires: proc
+                .spec
+                .iter()
+                .filter_map(|spec| match spec {
+                    ProcSpec::Requires(expr) => Some(self.lower_embedded_bool(expr)),
+                    ProcSpec::Ensures(_) => None,
+                })
+                .collect::<Result<Vec<_>, _>>()?,
+            ensures: proc
+                .spec
+                .iter()
+                .filter_map(|spec| match spec {
+                    ProcSpec::Requires(_) => None,
+                    ProcSpec::Ensures(expr) => Some(self.lower_embedded_bool(expr)),
+                })
+                .collect::<Result<Vec<_>, _>>()?,
+            decreases_star: body.is_some(),
+            body: method_body,
+        })
+    }
+
+    fn lower_block(&self, block: &crate::ast::Block) -> Result<dafny_ast::Block, TranslationError> {
+        let mut stmts = Vec::new();
+        for stmt in &block.node {
+            stmts.extend(self.lower_stmt(stmt)?);
+        }
+        Ok(dafny_ast::Block { stmts })
+    }
+
+    fn lower_stmt(&self, stmt: &Stmt) -> Result<Vec<dafny_ast::Stmt>, TranslationError> {
+        match &stmt.node {
+            StmtKind::Seq(stmts) => {
+                let block = crate::ast::Spanned::new(stmt.span, stmts.clone());
+                Ok(vec![dafny_ast::Stmt::Block(self.lower_block(&block)?)])
+            }
+            StmtKind::Var(var_ref) => Ok(vec![self.lower_var_decl(&var_ref.borrow())?]),
+            StmtKind::Assign(lhses, rhs) => {
+                if let ExprKind::Call(ident, args) = &rhs.kind {
+                    if let Some(decl) = self.tcx.get(*ident) {
+                        match decl.as_ref() {
+                            DeclKind::ProcDecl(_) => {
+                                let lowered_args = self.lower_exprs(args)?;
+                                return Ok(vec![if lhses.is_empty() {
+                                    dafny_ast::Stmt::Call(dafny_ast::CallStmt {
+                                        method: ident.name.to_owned(),
+                                        args: lowered_args,
+                                    })
+                                } else {
+                                    dafny_ast::Stmt::AssignCall(dafny_ast::AssignCallStmt {
+                                        lhs: lhses
+                                            .iter()
+                                            .map(|ident| ident.name.to_owned())
+                                            .collect(),
+                                        method: ident.name.to_owned(),
+                                        args: lowered_args,
+                                    })
+                                }]);
+                            }
+                            DeclKind::ProcIntrin(_) => {
+                                return Err(TranslationError::unsupported(
+                                    rhs.span,
+                                    format!(
+                                        "Dafny: intrinsic procedure `{}` is not supported",
+                                        ident.name
+                                    ),
+                                    "unsupported procedure call",
+                                ));
+                            }
+                            _ => {}
+                        }
+                    }
+                }
+
+                if lhses.len() != 1 {
+                    return Err(TranslationError::unsupported(
+                        stmt.span,
+                        "Dafny: tuple assignment is only supported for procedure calls",
+                        "unsupported assignment",
+                    ));
+                }
+
+                Ok(vec![dafny_ast::Stmt::Assign(dafny_ast::AssignStmt {
+                    lhs: lhses[0].name.to_owned(),
+                    rhs: self.lower_expr(rhs)?,
+                })])
+            }
+            StmtKind::Havoc(direction, vars) => {
+                if *direction != crate::ast::Direction::Down {
+                    return Err(TranslationError::unsupported(
+                        stmt.span,
+                        "Dafny: `cohavoc` is not supported",
+                        "expected `havoc` here",
+                    ));
+                }
+
+                Ok(vars
+                    .iter()
+                    .map(|ident| {
+                        dafny_ast::Stmt::SuchThatAssign(dafny_ast::SuchThatAssignStmt {
+                            lhs: vec![ident.name.to_owned()],
+                            predicate: true_expr(),
+                        })
+                    })
+                    .collect())
+            }
+            StmtKind::Assert(direction, expr) => {
+                if *direction != crate::ast::Direction::Down {
+                    return Err(TranslationError::unsupported(
+                        stmt.span,
+                        "Dafny: `coassert` is not supported",
+                        "expected `assert ?(b)` here",
+                    ));
+                }
+
+                Ok(vec![dafny_ast::Stmt::Assert(dafny_ast::AssertStmt {
+                    expr: self.lower_embedded_bool(expr)?,
+                })])
+            }
+            StmtKind::Assume(direction, expr) => {
+                if *direction != crate::ast::Direction::Down {
+                    return Err(TranslationError::unsupported(
+                        stmt.span,
+                        "Dafny: `coassume` is not supported",
+                        "expected `assume ?(b)` here",
+                    ));
+                }
+
+                Ok(vec![dafny_ast::Stmt::Assume(dafny_ast::AssumeStmt {
+                    axiom: true,
+                    expr: self.lower_embedded_bool(expr)?,
+                })])
+            }
+            StmtKind::If(cond, lhs, rhs) => Ok(vec![dafny_ast::Stmt::If(dafny_ast::IfStmt {
+                cond: self.lower_expr(cond)?,
+                then_branch: self.lower_block(lhs)?,
+                else_branch: self.lower_block(rhs)?,
+            })]),
+            StmtKind::While(_, _) => Err(TranslationError::unsupported(
+                stmt.span,
+                "Dafny: `while` loops must use `@invariant(?(...))`",
+                "missing supported loop invariant",
+            )),
+            StmtKind::Annotation(_, ident, inputs, inner) => {
+                if ident.name.to_owned() != "invariant" {
+                    return Err(TranslationError::unsupported(
+                        stmt.span,
+                        format!("Dafny: annotation `@{}` is not supported", ident.name),
+                        "unsupported annotation",
+                    ));
+                }
+                if inputs.len() != 1 {
+                    return Err(TranslationError::unsupported(
+                        stmt.span,
+                        "Dafny: `@invariant` expects exactly one argument",
+                        "invalid invariant annotation",
+                    ));
+                }
+                let StmtKind::While(cond, body) = &inner.node else {
+                    return Err(TranslationError::unsupported(
+                        stmt.span,
+                        "Dafny: `@invariant` must annotate a `while` loop",
+                        "expected `@invariant(?(...)) while ...`",
+                    ));
+                };
+
+                Ok(vec![dafny_ast::Stmt::While(dafny_ast::WhileStmt {
+                    cond: self.lower_expr(cond)?,
+                    invariants: vec![self.lower_embedded_bool(&inputs[0])?],
+                    decreases_star: true,
+                    body: self.lower_block(body)?,
+                })])
+            }
+            StmtKind::Compare(_, _)
+            | StmtKind::Negate(_)
+            | StmtKind::Validate(_)
+            | StmtKind::Tick(_)
+            | StmtKind::Weigh(_)
+            | StmtKind::Demonic(_, _)
+            | StmtKind::Angelic(_, _)
+            | StmtKind::Additive(_, _)
+            | StmtKind::Label(_) => Err(TranslationError::unsupported(
+                stmt.span,
+                "Dafny: statement is not supported by this backend",
+                "unsupported statement",
+            )),
+        }
+    }
+
+    fn lower_var_decl(&self, var: &VarDecl) -> Result<dafny_ast::Stmt, TranslationError> {
+        let ty = self.lower_type(&var.ty, var.span)?;
+        let init = if let Some(init) = &var.init {
+            if let ExprKind::Call(ident, args) = &init.kind {
+                if let Some(decl) = self.tcx.get(*ident) {
+                    match decl.as_ref() {
+                        DeclKind::ProcDecl(_) => dafny_ast::VarInit::MethodCall {
+                            method: ident.name.to_owned(),
+                            args: self.lower_exprs(args)?,
+                        },
+                        DeclKind::ProcIntrin(_) => {
+                            return Err(TranslationError::unsupported(
+                                init.span,
+                                format!(
+                                    "Dafny: intrinsic procedure `{}` is not supported",
+                                    ident.name
+                                ),
+                                "unsupported procedure call",
+                            ));
+                        }
+                        _ => dafny_ast::VarInit::Expr(self.lower_expr(init)?),
+                    }
+                } else {
+                    dafny_ast::VarInit::Expr(self.lower_expr(init)?)
+                }
+            } else {
+                dafny_ast::VarInit::Expr(self.lower_expr(init)?)
+            }
+        } else {
+            dafny_ast::VarInit::SuchThat(true_expr())
+        };
+
+        Ok(dafny_ast::Stmt::Var(dafny_ast::VarDecl {
+            name: var.name.name.to_owned(),
+            ty,
+            init,
+        }))
+    }
+
+    fn lower_axiom_expr(&self, expr: &Expr) -> Result<dafny_ast::Expr, TranslationError> {
+        self.lower_expr(expr)
+    }
+
+    fn lower_embedded_bool(&self, expr: &Expr) -> Result<dafny_ast::Expr, TranslationError> {
+        match &expr.kind {
+            ExprKind::Unary(un_op, operand) if un_op.node == UnOpKind::Embed => {
+                self.lower_expr(operand)
+            }
+            _ => Err(TranslationError::unsupported(
+                expr.span,
+                "Dafny: Boolean specifications must use the `?(b)` embedding",
+                "expected `?(b)` here",
+            )),
+        }
+    }
+
+    fn lower_expr(&self, expr: &Expr) -> Result<dafny_ast::Expr, TranslationError> {
+        match &expr.kind {
+            ExprKind::Var(ident) => Ok(dafny_ast::Expr::Var(ident.name.to_owned())),
+            ExprKind::Call(ident, args) => self.lower_call_expr(*ident, args, expr.span),
+            ExprKind::Ite(cond, lhs, rhs) => Ok(dafny_ast::Expr::Ite {
+                cond: Box::new(self.lower_expr(cond)?),
+                then_expr: Box::new(self.lower_expr(lhs)?),
+                else_expr: Box::new(self.lower_expr(rhs)?),
+            }),
+            ExprKind::Binary(op, lhs, rhs) => {
+                let op = match op.node {
+                    BinOpKind::Add => dafny_ast::BinaryOp::Add,
+                    BinOpKind::Sub => dafny_ast::BinaryOp::Sub,
+                    BinOpKind::Mul => dafny_ast::BinaryOp::Mul,
+                    BinOpKind::Div => dafny_ast::BinaryOp::Div,
+                    BinOpKind::Mod => dafny_ast::BinaryOp::Mod,
+                    BinOpKind::And => dafny_ast::BinaryOp::And,
+                    BinOpKind::Or => dafny_ast::BinaryOp::Or,
+                    BinOpKind::Eq => dafny_ast::BinaryOp::Eq,
+                    BinOpKind::Lt => dafny_ast::BinaryOp::Lt,
+                    BinOpKind::Le => dafny_ast::BinaryOp::Le,
+                    BinOpKind::Ne => dafny_ast::BinaryOp::Ne,
+                    BinOpKind::Ge => dafny_ast::BinaryOp::Ge,
+                    BinOpKind::Gt => dafny_ast::BinaryOp::Gt,
+                    BinOpKind::Impl => dafny_ast::BinaryOp::Impl,
+                    BinOpKind::Inf
+                    | BinOpKind::Sup
+                    | BinOpKind::CoImpl
+                    | BinOpKind::Compare
+                    | BinOpKind::CoCompare => {
+                        return Err(TranslationError::unsupported(
+                            expr.span,
+                            "Dafny: this HeyVL operator is not supported",
+                            "unsupported operator",
+                        ));
+                    }
+                };
+                Ok(dafny_ast::Expr::Binary {
+                    op,
+                    lhs: Box::new(self.lower_expr(lhs)?),
+                    rhs: Box::new(self.lower_expr(rhs)?),
+                })
+            }
+            ExprKind::Unary(un_op, operand) => match un_op.node {
+                UnOpKind::Not => Ok(dafny_ast::Expr::Unary {
+                    op: dafny_ast::UnaryOp::Not,
+                    expr: Box::new(self.lower_expr(operand)?),
+                }),
+                UnOpKind::Parens => Ok(dafny_ast::Expr::Unary {
+                    op: dafny_ast::UnaryOp::Parens,
+                    expr: Box::new(self.lower_expr(operand)?),
+                }),
+                UnOpKind::Embed => Err(TranslationError::unsupported(
+                    expr.span,
+                    "Dafny: `?(b)` is only supported in pre/post/assert/assume/@invariant",
+                    "unsupported Boolean embedding",
+                )),
+                UnOpKind::Iverson | UnOpKind::Non => Err(TranslationError::unsupported(
+                    expr.span,
+                    "Dafny: quantitative unary operators are not supported",
+                    "unsupported unary operator",
+                )),
+            },
+            ExprKind::Cast(operand) => self.lower_cast(expr, operand),
+            ExprKind::Quant(quant_op, vars, ann, body) => {
+                let quantifier = match quant_op.node {
+                    QuantOpKind::Forall => dafny_ast::Quantifier::Forall,
+                    QuantOpKind::Exists => dafny_ast::Quantifier::Exists,
+                    QuantOpKind::Inf | QuantOpKind::Sup => {
+                        return Err(TranslationError::unsupported(
+                            expr.span,
+                            "Dafny: quantitative quantifiers are not supported",
+                            "unsupported quantifier",
+                        ));
+                    }
+                };
+                let vars = vars
+                    .iter()
+                    .map(|var| self.lower_quant_var(var))
+                    .collect::<Result<Vec<_>, _>>()?;
+                let triggers = ann
+                    .triggers
+                    .iter()
+                    .map(|trigger| self.lower_exprs(trigger.terms()))
+                    .collect::<Result<Vec<_>, _>>()?;
+                Ok(dafny_ast::Expr::Quantified {
+                    quantifier,
+                    vars,
+                    triggers,
+                    body: Box::new(self.lower_expr(body)?),
+                })
+            }
+            ExprKind::Subst(_, _, _) => Err(TranslationError::unsupported(
+                expr.span,
+                "Dafny: substitution expressions are not supported",
+                "unsupported expression",
+            )),
+            ExprKind::Lit(lit) => self.lower_lit(&lit.node, expr.span),
+        }
+    }
+
+    fn lower_call_expr(
+        &self,
+        ident: Ident,
+        args: &[Expr],
+        span: Span,
+    ) -> Result<dafny_ast::Expr, TranslationError> {
+        if let Some(intrinsic) = supported_list_intrinsic(self.tcx, ident) {
+            return match intrinsic {
+                SupportedListIntrinsic::Len => {
+                    let [list] = args else {
+                        return Err(TranslationError::unsupported(
+                            span,
+                            "Dafny: `len` expects one argument",
+                            "invalid intrinsic call",
+                        ));
+                    };
+                    Ok(dafny_ast::Expr::SeqLen(Box::new(self.lower_expr(list)?)))
+                }
+                SupportedListIntrinsic::Select => {
+                    let [list, index] = args else {
+                        return Err(TranslationError::unsupported(
+                            span,
+                            "Dafny: `select` expects two arguments",
+                            "invalid intrinsic call",
+                        ));
+                    };
+                    Ok(dafny_ast::Expr::Index {
+                        collection: Box::new(self.lower_expr(list)?),
+                        index: Box::new(self.lower_expr(index)?),
+                    })
+                }
+                SupportedListIntrinsic::Store => {
+                    let [list, index, value] = args else {
+                        return Err(TranslationError::unsupported(
+                            span,
+                            "Dafny: `store` expects three arguments",
+                            "invalid intrinsic call",
+                        ));
+                    };
+                    Ok(dafny_ast::Expr::Update {
+                        collection: Box::new(self.lower_expr(list)?),
+                        index: Box::new(self.lower_expr(index)?),
+                        value: Box::new(self.lower_expr(value)?),
+                    })
+                }
+            };
+        }
+
+        let decl = self.tcx.get(ident).ok_or_else(|| {
+            TranslationError::unsupported(
+                span,
+                format!("Dafny: unknown callee `{}`", ident.name),
+                "unknown call target",
+            )
+        })?;
+        match decl.as_ref() {
+            DeclKind::FuncDecl(_) => Ok(dafny_ast::Expr::Call {
+                function: ident.name.to_owned(),
+                args: self.lower_exprs(args)?,
+            }),
+            DeclKind::FuncIntrin(_) => Err(TranslationError::unsupported(
+                span,
+                format!(
+                    "Dafny: intrinsic function `{}` is not supported",
+                    ident.name
+                ),
+                "unsupported intrinsic function",
+            )),
+            DeclKind::ProcDecl(_) | DeclKind::ProcIntrin(_) => Err(TranslationError::unsupported(
+                span,
+                format!(
+                    "Dafny: procedure `{}` cannot be used in expression position",
+                    ident.name
+                ),
+                "expected a pure function call",
+            )),
+            _ => Err(TranslationError::unsupported(
+                span,
+                format!("Dafny: call target `{}` is not supported", ident.name),
+                "unsupported call target",
+            )),
+        }
+    }
+
+    fn lower_cast(&self, expr: &Expr, operand: &Expr) -> Result<dafny_ast::Expr, TranslationError> {
+        let Some(target_ty) = expr.ty.as_ref() else {
+            return Err(TranslationError::unsupported(
+                expr.span,
+                "Dafny: cast without a resolved target type is not supported",
+                "unsupported cast",
+            ));
+        };
+        match target_ty {
+            TyKind::Bool | TyKind::Int | TyKind::UInt => self.lower_expr(operand),
+            TyKind::Real | TyKind::UReal | TyKind::EUReal | TyKind::SpecTy => {
+                Err(TranslationError::unsupported(
+                    expr.span,
+                    "Dafny: quantitative casts are not supported",
+                    "unsupported cast",
+                ))
+            }
+            _ => self.lower_expr(operand),
+        }
+    }
+
+    fn lower_quant_var(&self, var: &QuantVar) -> Result<dafny_ast::QuantVar, TranslationError> {
+        match var {
+            QuantVar::Fresh(decl_ref) => {
+                let decl = decl_ref.borrow();
+                Ok(dafny_ast::QuantVar {
+                    name: decl.name.name.to_owned(),
+                    ty: self.lower_type(&decl.ty, decl.span)?,
+                })
+            }
+            QuantVar::Shadow(ident) => {
+                let decl = self.tcx.get(*ident).ok_or_else(|| {
+                    TranslationError::unsupported(
+                        ident.span,
+                        format!(
+                            "Dafny: could not resolve quantified variable `{}`",
+                            ident.name
+                        ),
+                        "unresolved quantified variable",
+                    )
+                })?;
+                if let DeclKind::VarDecl(var_ref) = decl.as_ref() {
+                    let var = var_ref.borrow();
+                    Ok(dafny_ast::QuantVar {
+                        name: ident.name.to_owned(),
+                        ty: self.lower_type(&var.ty, ident.span)?,
+                    })
+                } else {
+                    Err(TranslationError::unsupported(
+                        ident.span,
+                        format!("Dafny: `{}` is not a variable", ident.name),
+                        "invalid quantified variable",
+                    ))
+                }
+            }
+        }
+    }
+
+    fn lower_param(&self, param: &Param) -> Result<dafny_ast::Param, TranslationError> {
+        Ok(dafny_ast::Param {
+            name: param.name.name.to_owned(),
+            ty: self.lower_type(&param.ty, param.span)?,
+        })
+    }
+
+    fn lower_type(&self, ty: &TyKind, span: Span) -> Result<dafny_ast::Type, TranslationError> {
+        match ty {
+            TyKind::Bool => Ok(dafny_ast::Type::Bool),
+            TyKind::Int => Ok(dafny_ast::Type::Int),
+            TyKind::UInt => Ok(dafny_ast::Type::Nat),
+            TyKind::List(element_ty) => Ok(dafny_ast::Type::Seq(Box::new(
+                self.lower_type(element_ty, span)?,
+            ))),
+            TyKind::Domain(domain_ref) => Ok(dafny_ast::Type::Named(
+                domain_ref.borrow().name.name.to_owned(),
+            )),
+            TyKind::Tuple(_) => Err(TranslationError::unsupported(
+                span,
+                "Dafny: tuple types are only supported in procedure returns",
+                "unsupported type",
+            )),
+            TyKind::Real | TyKind::UReal | TyKind::EUReal | TyKind::String | TyKind::SpecTy => {
+                Err(TranslationError::unsupported(
+                    span,
+                    format!("Dafny: type `{ty}` is not supported by this backend"),
+                    "unsupported type",
+                ))
+            }
+            TyKind::Unresolved(_) | TyKind::None => Err(TranslationError::unsupported(
+                span,
+                "Dafny: unresolved type is not supported",
+                "unsupported type",
+            )),
+        }
+    }
+
+    fn lower_lit(&self, lit: &LitKind, span: Span) -> Result<dafny_ast::Expr, TranslationError> {
+        match lit {
+            LitKind::Bool(value) => Ok(dafny_ast::Expr::BoolLit(*value)),
+            LitKind::UInt(value) => Ok(dafny_ast::Expr::NumberLit(value.to_string())),
+            LitKind::Str(value) => Ok(dafny_ast::Expr::StringLit(value.to_string())),
+            LitKind::Frac(_) | LitKind::Infinity => Err(TranslationError::unsupported(
+                span,
+                "Dafny: quantitative literals are not supported",
+                "unsupported literal",
+            )),
+        }
+    }
+
+    fn lower_exprs(&self, exprs: &[Expr]) -> Result<Vec<dafny_ast::Expr>, TranslationError> {
+        exprs.iter().map(|expr| self.lower_expr(expr)).collect()
+    }
+}
+
+/// Ensure that every required dependency is either locally lowerable or a supported intrinsic.
+pub(crate) fn ensure_required_decl_supported(
+    ident: Ident,
+    lowerer: &DafnyLowerer<'_>,
+    tcx: &TyCtx,
+) -> Result<(), CaesarError> {
+    if let Some(record) = lowerer.index.get(ident) {
+        lowerer
+            .local_support(record)
+            .map_err(|err| CaesarError::Diagnostic(err.diagnostic(ReportKind::Error)))?;
+        return Ok(());
+    }
+
+    let decl = tcx.get(ident).ok_or_else(|| {
+        CaesarError::UserError(
+            format!("Missing declaration for dependency `{}`.", ident.name).into(),
+        )
+    })?;
+    match decl.as_ref() {
+        DeclKind::FuncIntrin(_) if supported_list_intrinsic(tcx, ident).is_some() => Ok(()),
+        DeclKind::ProcIntrin(_) => Err(CaesarError::Diagnostic(
+            TranslationError::unsupported(
+                ident.span,
+                format!(
+                    "Dafny: intrinsic procedure `{}` is not supported",
+                    ident.name
+                ),
+                "unsupported procedure call",
+            )
+            .diagnostic(ReportKind::Error),
+        )),
+        DeclKind::FuncIntrin(_) => Err(CaesarError::Diagnostic(
+            TranslationError::unsupported(
+                ident.span,
+                format!(
+                    "Dafny: intrinsic function `{}` is not supported",
+                    ident.name
+                ),
+                "unsupported intrinsic function",
+            )
+            .diagnostic(ReportKind::Error),
+        )),
+        other => Err(CaesarError::Diagnostic(
+            TranslationError::unsupported(
+                ident.span,
+                format!(
+                    "Dafny: declaration kind `{}` is not supported",
+                    other.kind_name()
+                ),
+                "unsupported dependency",
+            )
+            .diagnostic(ReportKind::Error),
+        )),
+    }
+}
+
+fn supported_list_intrinsic(tcx: &TyCtx, ident: Ident) -> Option<SupportedListIntrinsic> {
+    let decl = tcx.get(ident)?;
+    if !matches!(decl.as_ref(), DeclKind::FuncIntrin(_)) {
+        return None;
+    }
+
+    match ident.name.to_owned().as_str() {
+        "len" => Some(SupportedListIntrinsic::Len),
+        "select" => Some(SupportedListIntrinsic::Select),
+        "store" => Some(SupportedListIntrinsic::Store),
+        _ => None,
+    }
+}
+
+fn true_expr() -> dafny_ast::Expr {
+    dafny_ast::Expr::BoolLit(true)
+}
diff --git a/src/dafny/mod.rs b/src/dafny/mod.rs
new file mode 100644
index 00000000..3d390da3
--- /dev/null
+++ b/src/dafny/mod.rs
@@ -0,0 +1,10 @@
+mod ast;
+mod index;
+mod lower;
+mod pretty;
+mod translate;
+
+#[cfg(test)]
+mod tests;
+
+pub use self::translate::translate_to_dafny;
diff --git a/src/dafny/pretty.rs b/src/dafny/pretty.rs
new file mode 100644
index 00000000..cfa8a8f6
--- /dev/null
+++ b/src/dafny/pretty.rs
@@ -0,0 +1,272 @@
+use super::ast;
+
+pub fn print_file(file: &ast::File) -> String {
+    file.decls
+        .iter()
+        .map(print_decl)
+        .collect::<Vec<_>>()
+        .join("\n\n")
+}
+
+fn print_decl(decl: &ast::Decl) -> String {
+    match decl {
+        ast::Decl::Type(type_decl) => format!("type {}(0,==)", type_decl.name),
+        ast::Decl::Function(function) => print_function(function),
+        ast::Decl::Method(method) => print_method(method),
+    }
+}
+
+fn print_function(function: &ast::FunctionDecl) -> String {
+    let mut lines = vec![format!(
+        "function {}({}): {}",
+        function.name,
+        join_params(&function.params),
+        print_type(&function.return_ty)
+    )];
+    if let Some(body) = &function.body {
+        lines.push("{".to_owned());
+        lines.push(format!("    {}", print_expr(body)));
+        lines.push("}".to_owned());
+    }
+    lines.join("\n")
+}
+
+fn print_method(method: &ast::MethodDecl) -> String {
+    let mut header = format!(
+        "method{} {}({})",
+        if method.axiom { " {:axiom}" } else { "" },
+        method.name,
+        join_params(&method.params)
+    );
+    if !method.returns.is_empty() {
+        header.push_str(&format!(" returns ({})", join_params(&method.returns)));
+    }
+
+    let mut lines = vec![header];
+    for requires in &method.requires {
+        lines.push(format!("    requires {}", print_expr(requires)));
+    }
+    for ensures in &method.ensures {
+        lines.push(format!("    ensures {}", print_expr(ensures)));
+    }
+    if method.decreases_star {
+        lines.push("    decreases *".to_owned());
+    }
+    if let Some(body) = &method.body {
+        lines.push("{".to_owned());
+        lines.extend(print_block(body, 4));
+        lines.push("}".to_owned());
+    }
+    lines.join("\n")
+}
+
+fn print_block(block: &ast::Block, indent: usize) -> Vec<String> {
+    let mut lines = Vec::new();
+    for stmt in &block.stmts {
+        lines.extend(print_stmt(stmt, indent));
+    }
+    lines
+}
+
+fn print_stmt(stmt: &ast::Stmt, indent: usize) -> Vec<String> {
+    let pad = " ".repeat(indent);
+    match stmt {
+        ast::Stmt::Block(block) => {
+            let mut lines = vec![format!("{pad}{{")];
+            lines.extend(print_block(block, indent + 4));
+            lines.push(format!("{pad}}}"));
+            lines
+        }
+        ast::Stmt::Var(var) => vec![match &var.init {
+            ast::VarInit::Expr(expr) => format!(
+                "{pad}var {}: {} := {};",
+                var.name,
+                print_type(&var.ty),
+                print_expr(expr)
+            ),
+            ast::VarInit::MethodCall { method, args } => format!(
+                "{pad}var {}: {} := {}({});",
+                var.name,
+                print_type(&var.ty),
+                method,
+                join_exprs(args)
+            ),
+            ast::VarInit::SuchThat(expr) => format!(
+                "{pad}var {}: {} :| {};",
+                var.name,
+                print_type(&var.ty),
+                print_expr(expr)
+            ),
+        }],
+        ast::Stmt::Assign(assign) => {
+            vec![format!(
+                "{pad}{} := {};",
+                assign.lhs,
+                print_expr(&assign.rhs)
+            )]
+        }
+        ast::Stmt::Call(call) => vec![format!("{pad}{}({});", call.method, join_exprs(&call.args))],
+        ast::Stmt::AssignCall(call) => {
+            let prefix = if call.lhs.is_empty() {
+                String::new()
+            } else {
+                format!("{} := ", call.lhs.join(", "))
+            };
+            vec![format!(
+                "{pad}{prefix}{}({});",
+                call.method,
+                join_exprs(&call.args)
+            )]
+        }
+        ast::Stmt::SuchThatAssign(assign) => vec![format!(
+            "{pad}{} :| {};",
+            assign.lhs.join(", "),
+            print_expr(&assign.predicate)
+        )],
+        ast::Stmt::Assert(assert) => vec![format!("{pad}assert {};", print_expr(&assert.expr))],
+        ast::Stmt::Assume(assume) => vec![format!(
+            "{pad}assume{} {};",
+            if assume.axiom { " {:axiom}" } else { "" },
+            print_expr(&assume.expr)
+        )],
+        ast::Stmt::If(if_stmt) => {
+            let mut lines = vec![format!("{pad}if {} {{", print_expr(&if_stmt.cond))];
+            lines.extend(print_block(&if_stmt.then_branch, indent + 4));
+            lines.push(format!("{pad}}} else {{"));
+            lines.extend(print_block(&if_stmt.else_branch, indent + 4));
+            lines.push(format!("{pad}}}"));
+            lines
+        }
+        ast::Stmt::While(while_stmt) => {
+            let mut lines = vec![format!("{pad}while {}", print_expr(&while_stmt.cond))];
+            for invariant in &while_stmt.invariants {
+                lines.push(format!("{pad}    invariant {}", print_expr(invariant)));
+            }
+            if while_stmt.decreases_star {
+                lines.push(format!("{pad}    decreases *"));
+            }
+            lines.push(format!("{pad}{{"));
+            lines.extend(print_block(&while_stmt.body, indent + 4));
+            lines.push(format!("{pad}}}"));
+            lines
+        }
+    }
+}
+
+fn print_expr(expr: &ast::Expr) -> String {
+    match expr {
+        ast::Expr::Var(name) => name.clone(),
+        ast::Expr::BoolLit(value) => value.to_string(),
+        ast::Expr::NumberLit(value) => value.clone(),
+        ast::Expr::StringLit(value) => format!("\"{}\"", value.escape_default()),
+        ast::Expr::Call { function, args } => format!("{function}({})", join_exprs(args)),
+        ast::Expr::Ite {
+            cond,
+            then_expr,
+            else_expr,
+        } => format!(
+            "(if {} then {} else {})",
+            print_expr(cond),
+            print_expr(then_expr),
+            print_expr(else_expr)
+        ),
+        ast::Expr::Binary { op, lhs, rhs } => format!(
+            "({} {} {})",
+            print_expr(lhs),
+            print_binary_op(op),
+            print_expr(rhs)
+        ),
+        ast::Expr::Unary { op, expr } => match op {
+            ast::UnaryOp::Not => format!("!({})", print_expr(expr)),
+            ast::UnaryOp::Parens => format!("({})", print_expr(expr)),
+        },
+        ast::Expr::Quantified {
+            quantifier,
+            vars,
+            triggers,
+            body,
+        } => {
+            let triggers = triggers
+                .iter()
+                .map(|trigger| format!(" {{:trigger {}}}", join_exprs(trigger)))
+                .collect::<Vec<_>>()
+                .join("");
+            format!(
+                "({} {}{} :: {})",
+                print_quantifier(quantifier),
+                join_quant_vars(vars),
+                triggers,
+                print_expr(body)
+            )
+        }
+        ast::Expr::SeqLen(expr) => format!("|{}|", print_expr(expr)),
+        ast::Expr::Index { collection, index } => {
+            format!("{}[{}]", print_expr(collection), print_expr(index))
+        }
+        ast::Expr::Update {
+            collection,
+            index,
+            value,
+        } => format!(
+            "{}[{} := {}]",
+            print_expr(collection),
+            print_expr(index),
+            print_expr(value)
+        ),
+    }
+}
+
+fn print_binary_op(op: &ast::BinaryOp) -> &'static str {
+    match op {
+        ast::BinaryOp::Add => "+",
+        ast::BinaryOp::Sub => "-",
+        ast::BinaryOp::Mul => "*",
+        ast::BinaryOp::Div => "/",
+        ast::BinaryOp::Mod => "%",
+        ast::BinaryOp::And => "&&",
+        ast::BinaryOp::Or => "||",
+        ast::BinaryOp::Eq => "==",
+        ast::BinaryOp::Lt => "<",
+        ast::BinaryOp::Le => "<=",
+        ast::BinaryOp::Ne => "!=",
+        ast::BinaryOp::Ge => ">=",
+        ast::BinaryOp::Gt => ">",
+        ast::BinaryOp::Impl => "==>",
+    }
+}
+
+fn print_quantifier(quantifier: &ast::Quantifier) -> &'static str {
+    match quantifier {
+        ast::Quantifier::Forall => "forall",
+        ast::Quantifier::Exists => "exists",
+    }
+}
+
+fn print_type(ty: &ast::Type) -> String {
+    match ty {
+        ast::Type::Bool => "bool".to_owned(),
+        ast::Type::Int => "int".to_owned(),
+        ast::Type::Nat => "nat".to_owned(),
+        ast::Type::Seq(element_ty) => format!("seq<{}>", print_type(element_ty)),
+        ast::Type::Named(name) => name.clone(),
+    }
+}
+
+fn join_params(params: &[ast::Param]) -> String {
+    params
+        .iter()
+        .map(|param| format!("{}: {}", param.name, print_type(&param.ty)))
+        .collect::<Vec<_>>()
+        .join(", ")
+}
+
+fn join_quant_vars(vars: &[ast::QuantVar]) -> String {
+    vars.iter()
+        .map(|var| format!("{}: {}", var.name, print_type(&var.ty)))
+        .collect::<Vec<_>>()
+        .join(", ")
+}
+
+fn join_exprs(exprs: &[ast::Expr]) -> String {
+    exprs.iter().map(print_expr).collect::<Vec<_>>().join(", ")
+}
diff --git a/src/dafny/tests.rs b/src/dafny/tests.rs
new file mode 100644
index 00000000..288aa00a
--- /dev/null
+++ b/src/dafny/tests.rs
@@ -0,0 +1,254 @@
+use std::path::PathBuf;
+
+use ariadne::ReportKind;
+use regex::Regex;
+
+use super::{
+    index::DeclIndex,
+    lower::DafnyLowerer,
+    pretty,
+    translate::{select_included_decls, FilePlan},
+};
+use crate::{
+    ast::SourceFilePath,
+    depgraph::DepGraph,
+    driver::{
+        commands::{
+            options::{DafnyOptions, DafnyScope, InputOptions},
+            verify::VerifyCommand,
+        },
+        front::parse_and_tycheck,
+    },
+    front::parser::ParserMode,
+    servers::{Server, TestServer},
+    smt::funcs::axiomatic::AxiomInstantiation,
+};
+
+fn translate_test_source(
+    source: &str,
+    scope: DafnyScope,
+    filter: Option<&str>,
+    werr: bool,
+) -> (
+    Result<String, crate::driver::error::CaesarError>,
+    TestServer,
+) {
+    let mut verify_options = VerifyCommand::default();
+    verify_options.input_options.werr = werr;
+
+    let mut server = TestServer::new(&verify_options);
+    let file_id = server
+        .get_files_internal()
+        .lock()
+        .unwrap()
+        .add(SourceFilePath::Builtin, source.to_owned())
+        .id;
+
+    let input_options = InputOptions {
+        files: vec![],
+        raw: false,
+        parser_mode: ParserMode::Both,
+        werr,
+        filter: None,
+    };
+
+    let res = (|| {
+        let (mut module, tcx) = parse_and_tycheck(
+            &input_options,
+            &verify_options.debug_options,
+            &mut server,
+            &[file_id],
+        )?;
+
+        let mut depgraph = DepGraph::new(AxiomInstantiation::Decreasing);
+        for source_unit in &mut module.items {
+            source_unit.enter_mut().populate_depgraph(&mut depgraph)?;
+        }
+
+        let index = DeclIndex::new(&module);
+        let lowerer = DafnyLowerer {
+            tcx: &tcx,
+            depgraph: &depgraph,
+            index: &index,
+        };
+        let filter = filter.map(|regex| Regex::new(regex).unwrap());
+        let roots = index.selected_roots_for_file(file_id, filter.as_ref());
+        let dafny_options = DafnyOptions {
+            dafny_dir: None,
+            run_dafny: false,
+            dafny_scope: scope,
+        };
+        let included =
+            select_included_decls(&dafny_options, &mut server, &lowerer, file_id, &roots, &tcx)?;
+        let plan = FilePlan {
+            file_id,
+            output_path: PathBuf::from("test.dfy"),
+            roots,
+            included,
+        };
+        let file = lowerer.lower_file(plan.file_id, &plan.roots, &plan.included)?;
+        Ok(pretty::print_file(&file))
+    })();
+
+    (res, server)
+}
+
+#[test]
+fn reachable_scope_includes_selected_root_and_helper() {
+    let source = r#"
+            proc helper(x: UInt) -> (y: UInt)
+                pre ?(true)
+                post ?(y == x)
+            {
+                y = x
+            }
+
+            proc root(x: UInt) -> (y: UInt)
+                pre ?(true)
+                post ?(y == x)
+            {
+                y = helper(x)
+            }
+
+            proc unused(x: UInt) -> (y: UInt)
+                pre ?(true)
+                post ?(y == x)
+            {
+                y = x
+            }
+        "#;
+    let rendered = translate_test_source(source, DafnyScope::Reachable, Some("root$"), true)
+        .0
+        .unwrap();
+    assert!(rendered.contains("method helper"));
+    assert!(rendered.contains("method root"));
+    assert!(!rendered.contains("method unused"));
+}
+
+#[test]
+fn all_scope_includes_unreachable_translateable_proc() {
+    let source = r#"
+            proc helper(x: UInt) -> (y: UInt)
+                pre ?(true)
+                post ?(y == x)
+            {
+                y = x
+            }
+
+            proc root(x: UInt) -> (y: UInt)
+                pre ?(true)
+                post ?(y == x)
+            {
+                y = helper(x)
+            }
+
+            proc unused(x: UInt) -> (y: UInt)
+                pre ?(true)
+                post ?(y == x)
+            {
+                y = x
+            }
+        "#;
+    let rendered = translate_test_source(source, DafnyScope::All, Some("root$"), true)
+        .0
+        .unwrap();
+    assert!(rendered.contains("method helper"));
+    assert!(rendered.contains("method root"));
+    assert!(rendered.contains("method unused"));
+}
+
+#[test]
+fn all_scope_warns_and_skips_unreachable_unsupported_decl() {
+    let source = r#"
+            proc root(x: UInt) -> (y: UInt)
+                pre ?(true)
+                post ?(y == x)
+            {
+                y = x
+            }
+
+            coproc ghost() -> ()
+                pre ?(false)
+                post ?(false)
+            {}
+        "#;
+    let (res, server) = translate_test_source(source, DafnyScope::All, Some("root$"), false);
+    let rendered = res.unwrap();
+    assert!(rendered.contains("method root"));
+    assert!(!rendered.contains("ghost"));
+    assert_eq!(server.diagnostics.len(), 1);
+    assert_eq!(server.diagnostics[0].kind(), ReportKind::Warning);
+}
+
+#[test]
+fn required_unsupported_dependency_fails_translation() {
+    let source = r#"
+            proc root() -> (b: Bool)
+                pre ?(true)
+                post ?(b == true || b == false)
+            {
+                b = flip(0.5)
+            }
+        "#;
+    let res = translate_test_source(source, DafnyScope::Reachable, Some("root$"), true).0;
+    assert!(res.is_err());
+}
+
+#[test]
+fn user_defined_select_stays_a_function_call() {
+    let source = r#"
+            domain List {
+                func nil(): List
+                func select(ls: List, i: UInt): Int
+            }
+
+            proc root(ls: List) -> (x: Int)
+                post ?(x == select(ls, 0))
+            {
+                x = select(ls, 0)
+            }
+        "#;
+    let rendered = translate_test_source(source, DafnyScope::Reachable, Some("root$"), true)
+        .0
+        .unwrap();
+    assert!(rendered.contains("function select(ls: List, i: nat): int"));
+    assert!(rendered.contains("ensures ((x == select(ls, 0)))"));
+    assert!(rendered.contains("x := select(ls, 0);"));
+    assert!(!rendered.contains("ls[0]"));
+}
+
+#[test]
+fn builtin_select_and_len_stay_sequence_operations() {
+    let source = r#"
+            proc root(ls: []Int) -> (x: Int)
+                pre ?(0 < len(ls))
+                post ?(x == select(ls, 0))
+            {
+                x = select(ls, 0)
+            }
+        "#;
+    let rendered = translate_test_source(source, DafnyScope::Reachable, Some("root$"), true)
+        .0
+        .unwrap();
+    assert!(rendered.contains("requires ((0 < |ls|))"));
+    assert!(rendered.contains("ensures ((x == ls[0]))"));
+    assert!(rendered.contains("x := ls[0];"));
+}
+
+#[test]
+fn builtin_store_stays_a_sequence_update() {
+    let source = r#"
+            proc root(ls: []Int) -> (res: []Int)
+                pre ?(0 < len(ls))
+                post ?(select(res, 0) == 7)
+            {
+                res = store(ls, 0, 7)
+            }
+        "#;
+    let rendered = translate_test_source(source, DafnyScope::Reachable, Some("root$"), true)
+        .0
+        .unwrap();
+    assert!(rendered.contains("requires ((0 < |ls|))"));
+    assert!(rendered.contains("ensures ((res[0] == 7))"));
+    assert!(rendered.contains("res := ls[0 := 7];"));
+}
diff --git a/src/dafny/translate.rs b/src/dafny/translate.rs
new file mode 100644
index 00000000..52fc0cde
--- /dev/null
+++ b/src/dafny/translate.rs
@@ -0,0 +1,223 @@
+use std::{
+    collections::HashSet,
+    fs::create_dir_all,
+    path::{Path, PathBuf},
+    process::Command,
+};
+
+use ariadne::ReportKind;
+use regex::Regex;
+
+use super::{
+    index::DeclIndex,
+    lower::{ensure_required_decl_supported, DafnyLowerer},
+    pretty,
+};
+use crate::{
+    ast::{FileId, Ident, SourceFilePath},
+    depgraph::DepGraph,
+    driver::{
+        commands::options::{DafnyOptions, DafnyScope, InputOptions},
+        error::CaesarError,
+        front::Module,
+    },
+    resource_limits::LimitsRef,
+    servers::Server,
+    smt::funcs::axiomatic::AxiomInstantiation,
+    tyctx::TyCtx,
+};
+
+/// Per-file translation state after scope selection has been resolved.
+pub(crate) struct FilePlan {
+    pub(crate) file_id: FileId,
+    pub(crate) output_path: PathBuf,
+    pub(crate) roots: Vec<Ident>,
+    pub(crate) included: HashSet<Ident>,
+}
+
+/// Translate the selected HeyVL files into Dafny files and optionally run `dafny verify`.
+pub fn translate_to_dafny(
+    options: &DafnyOptions,
+    input_options: &InputOptions,
+    module: &mut Module,
+    server: &mut dyn Server,
+    limits_ref: &LimitsRef,
+    tcx: &TyCtx,
+    user_files: &[FileId],
+) -> Result<(), CaesarError> {
+    if options.dafny_dir.is_none() && !options.run_dafny {
+        return Err(CaesarError::UserError(
+            "Either --dafny-dir or --run-dafny must be provided.".into(),
+        ));
+    }
+
+    let filter = match &input_options.filter {
+        Some(filter) => Some(Regex::new(filter).map_err(|err| {
+            CaesarError::UserError(format!("Invalid filter regex: {err}").into())
+        })?),
+        None => None,
+    };
+
+    let mut depgraph = DepGraph::new(AxiomInstantiation::Decreasing);
+    for source_unit in &mut module.items {
+        source_unit.enter_mut().populate_depgraph(&mut depgraph)?;
+    }
+
+    let index = DeclIndex::new(module);
+
+    let mut temp_dir = None;
+    let output_dir = if let Some(dafny_dir) = &options.dafny_dir {
+        dafny_dir.clone()
+    } else {
+        let dir = tempfile::tempdir().map_err(|err| {
+            CaesarError::UserError(format!("Could not create temporary directory: {err}").into())
+        })?;
+        let path = dir.path().to_owned();
+        temp_dir = Some(dir);
+        path
+    };
+
+    let lowerer = DafnyLowerer {
+        tcx,
+        depgraph: &depgraph,
+        index: &index,
+    };
+
+    let mut wrote_anything = false;
+    for file_id in user_files {
+        limits_ref.check_limits()?;
+        let roots = index.selected_roots_for_file(*file_id, filter.as_ref());
+        if roots.is_empty() {
+            continue;
+        }
+
+        let stored_file = server.get_file(*file_id).ok_or_else(|| {
+            CaesarError::UserError("Could not retrieve loaded source file.".into())
+        })?;
+        let output_path = output_file_path(&stored_file.path, &output_dir)?;
+        let included = select_included_decls(options, server, &lowerer, *file_id, &roots, tcx)?;
+        let plan = FilePlan {
+            file_id: *file_id,
+            output_path,
+            roots,
+            included,
+        };
+        let dafny_file = lowerer.lower_file(plan.file_id, &plan.roots, &plan.included)?;
+        let rendered = pretty::print_file(&dafny_file);
+        create_dir_all(plan.output_path.parent().unwrap())?;
+        std::fs::write(&plan.output_path, rendered)?;
+        wrote_anything = true;
+
+        if options.run_dafny {
+            run_dafny_verify(&plan.output_path)?;
+        }
+    }
+
+    drop(temp_dir.take());
+
+    if !wrote_anything {
+        return Err(CaesarError::UserError(
+            "No matching top-level procs were selected for Dafny translation.".into(),
+        ));
+    }
+
+    Ok(())
+}
+
+fn output_file_path(
+    source_path: &SourceFilePath,
+    output_dir: &Path,
+) -> Result<PathBuf, CaesarError> {
+    let relative = source_path
+        .relative_to_cwd()
+        .map_err(CaesarError::IoError)?;
+    match relative {
+        SourceFilePath::Path(path) => {
+            let mut output_path = output_dir.join(path);
+            output_path.set_extension("dfy");
+            Ok(output_path)
+        }
+        _ => Err(CaesarError::UserError(
+            "The Dafny backend only supports filesystem-backed input files.".into(),
+        )),
+    }
+}
+
+fn run_dafny_verify(path: &Path) -> Result<(), CaesarError> {
+    let output = Command::new("dafny").arg("verify").arg(path).output()?;
+    if output.status.success() {
+        return Ok(());
+    }
+
+    let stdout = String::from_utf8_lossy(&output.stdout);
+    let stderr = String::from_utf8_lossy(&output.stderr);
+    Err(CaesarError::UserError(
+        format!(
+            "`dafny verify {}` failed with status {}.\nstdout:\n{}\nstderr:\n{}",
+            path.display(),
+            output.status,
+            stdout,
+            stderr
+        )
+        .into(),
+    ))
+}
+
+/// Choose the declarations that must be present in one emitted `.dfy` file.
+pub(crate) fn select_included_decls(
+    options: &DafnyOptions,
+    server: &mut dyn Server,
+    lowerer: &DafnyLowerer<'_>,
+    file_id: FileId,
+    roots: &[Ident],
+    tcx: &TyCtx,
+) -> Result<HashSet<Ident>, CaesarError> {
+    let mut seeds = HashSet::new();
+    let root_set: HashSet<_> = roots.iter().copied().collect();
+
+    match options.dafny_scope {
+        DafnyScope::Reachable => {
+            for root in roots {
+                ensure_required_decl_supported(*root, lowerer, tcx)?;
+                seeds.insert(*root);
+            }
+        }
+        DafnyScope::All => {
+            for record in &lowerer.index.ordered {
+                if record.file_id != file_id {
+                    continue;
+                }
+                let local_support = lowerer.local_support(record);
+                if root_set.contains(&record.ident) {
+                    local_support.map_err(|err| {
+                        CaesarError::Diagnostic(err.diagnostic(ReportKind::Error))
+                    })?;
+                    seeds.insert(record.ident);
+                    continue;
+                }
+
+                match local_support {
+                    Ok(()) => {
+                        seeds.insert(record.ident);
+                    }
+                    Err(err) => {
+                        server.add_diagnostic(err.diagnostic(ReportKind::Warning).with_note(
+                            "Skipping this declaration while translating with `--dafny-scope all`.",
+                        ))?;
+                    }
+                }
+            }
+        }
+    }
+
+    let included: HashSet<_> = lowerer
+        .depgraph
+        .get_reachable(seeds.iter().copied())
+        .into_hash_set();
+
+    for ident in &included {
+        ensure_required_decl_supported(*ident, lowerer, tcx)?;
+    }
+
+    Ok(included)
+}
diff --git a/src/depgraph.rs b/src/depgraph.rs
index a61e4fe5..375a68c0 100644
--- a/src/depgraph.rs
+++ b/src/depgraph.rs
@@ -21,6 +21,10 @@ impl Dependencies {
         self.0.contains(ident)
     }
 
+    pub fn into_hash_set(self) -> HashSet<Ident> {
+        self.0
+    }
+
     pub fn union(self, other: Self) -> Self {
         Dependencies(self.0.union(&other.0).cloned().collect())
     }
diff --git a/src/driver/commands/dafny.rs b/src/driver/commands/dafny.rs
new file mode 100644
index 00000000..fe24d8da
--- /dev/null
+++ b/src/driver/commands/dafny.rs
@@ -0,0 +1,84 @@
+use std::{ops::DerefMut, process::ExitCode, sync::Mutex, time::Instant};
+
+use clap::Args;
+
+use crate::{
+    ast::FileId,
+    dafny::translate_to_dafny,
+    driver::{
+        commands::{
+            mk_cli_server,
+            options::{DafnyOptions, DebugOptions, InputOptions, ResourceLimitOptions},
+        },
+        error::{finalize_caesar_result, CaesarError},
+        front::parse_and_tycheck,
+    },
+    resource_limits::LimitsRef,
+    servers::Server,
+};
+
+#[derive(Debug, Default, Args)]
+pub struct DafnyCommand {
+    #[command(flatten)]
+    pub input_options: InputOptions,
+
+    #[command(flatten)]
+    pub rlimit_options: ResourceLimitOptions,
+
+    #[command(flatten)]
+    pub dafny_options: DafnyOptions,
+
+    #[command(flatten)]
+    pub debug_options: DebugOptions,
+}
+
+pub fn run_dafny_command(options: DafnyCommand) -> ExitCode {
+    let (user_files, server) = match mk_cli_server(&options.input_options) {
+        Ok(value) => value,
+        Err(value) => return value,
+    };
+    let res = dafny_main(&options, user_files, &server).map(|_| true);
+    finalize_caesar_result(server, &options.rlimit_options, res)
+}
+
+fn dafny_main(
+    options: &DafnyCommand,
+    user_files: Vec<FileId>,
+    server: &Mutex<dyn Server>,
+) -> Result<(), CaesarError> {
+    if options.input_options.raw {
+        return Err(CaesarError::UserError(
+            "The Dafny backend does not support `--raw`; pass HeyVL declarations instead.".into(),
+        ));
+    }
+
+    let parse_input_options = InputOptions {
+        files: options.input_options.files.clone(),
+        raw: options.input_options.raw,
+        parser_mode: options.input_options.parser_mode,
+        werr: options.input_options.werr,
+        filter: None,
+    };
+
+    let mut server_lock = server.lock().unwrap();
+    let (mut module, tcx) = parse_and_tycheck(
+        &parse_input_options,
+        &options.debug_options,
+        &mut *server_lock,
+        &user_files,
+    )?;
+
+    let timeout = Instant::now() + options.rlimit_options.timeout();
+    let mem_limit = options.rlimit_options.mem_limit();
+    let limits_ref = LimitsRef::new(Some(timeout), Some(mem_limit));
+
+    translate_to_dafny(
+        &options.dafny_options,
+        &options.input_options,
+        &mut module,
+        server_lock.deref_mut(),
+        &limits_ref,
+        &tcx,
+        &user_files,
+    )
+}
diff --git a/src/driver/commands/mod.rs b/src/driver/commands/mod.rs
index 33503a63..1c8b1671 100644
--- a/src/driver/commands/mod.rs
+++ b/src/driver/commands/mod.rs
@@ -1,5 +1,6 @@
 //! (CLI) command and option declarations to run Caesar with.
 
+pub mod dafny;
 pub mod model_check;
 pub mod options;
 pub mod refinement;
@@ -19,6 +20,7 @@ use clap::{crate_description, Args, CommandFactory, Parser, Subcommand};
 use crate::{
     ast::FileId,
     driver::commands::{
+        dafny::{run_dafny_command, DafnyCommand},
         model_check::{run_model_checking_command, ModelCheckCommand},
         options::{DebugOptions, InputOptions},
         refinement::run_verify_entailment_command,
@@ -62,6 +64,7 @@ impl CaesarCli {
         match options.command {
             CaesarCommand::Verify(options) => run_verify_command(options).await,
             CaesarCommand::Entailment(options) => run_verify_entailment_command(options).await,
+            CaesarCommand::Dafny(options) => run_dafny_command(options),
             CaesarCommand::Mc(options) => run_model_checking_command(options),
             CaesarCommand::Lsp(options) => run_lsp_command(options).await,
             CaesarCommand::ShellCompletions(options) => run_shell_completions_command(options),
@@ -91,6 +94,9 @@ pub enum CaesarCommand {
     Verify(VerifyCommand),
     /// Check refinement via entailment between `coproc`/`proc` pairs.
     Entailment(VerifyCommand),
+    /// Export HeyVL files to Dafny and optionally run `dafny verify`.
+    #[clap(visible_alias = "to-dafny")]
+    Dafny(DafnyCommand),
     /// Model checking via JANI, can run Storm directly.
     #[clap(visible_alias = "to-jani")]
     Mc(ModelCheckCommand),
@@ -109,6 +115,7 @@ impl CaesarCommand {
         match &self {
             CaesarCommand::Verify(verify_options) => Some(&verify_options.debug_options),
             CaesarCommand::Entailment(verify_options) => Some(&verify_options.debug_options),
+            CaesarCommand::Dafny(dafny_options) => Some(&dafny_options.debug_options),
             CaesarCommand::Lsp(verify_options) => Some(&verify_options.debug_options),
             CaesarCommand::Mc(mc_options) => Some(&mc_options.debug_options),
             CaesarCommand::ShellCompletions(_) => None,
diff --git a/src/driver/commands/options.rs b/src/driver/commands/options.rs
index 062423d4..a61187f3 100644
--- a/src/driver/commands/options.rs
+++ b/src/driver/commands/options.rs
@@ -127,6 +127,30 @@ impl ModelCheckingOptions {
     }
 }
 
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Default, ValueEnum)]
+pub enum DafnyScope {
+    #[default]
+    Reachable,
+    All,
+}
+
+#[derive(Debug, Default, Clone, Args)]
+#[command(next_help_heading = "Dafny Options")]
+pub struct DafnyOptions {
+    /// Export translated declarations to Dafny files in the provided directory.
+    #[arg(long)]
+    pub dafny_dir: Option<PathBuf>,
+
+    /// Run `dafny verify` on each generated file.
+    #[arg(long)]
+    pub run_dafny: bool,
+
+    /// Choose whether to emit only declarations reachable from selected procs
+    /// or all locally translatable declarations from each selected file.
+    #[arg(long, default_value = "reachable")]
+    pub dafny_scope: DafnyScope,
+}
+
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Default, ValueEnum)]
 pub enum QuantifierInstantiation {
     /// Use all available quantifier instantiation heuristics, in particular
diff --git a/src/main.rs b/src/main.rs
index a1df5e82..4973085d 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -8,6 +8,7 @@ use std::process::ExitCode;
 use crate::driver::commands::CaesarCli;
 
 mod ast;
+mod dafny;
 mod depgraph;
 mod driver;
 mod front;
diff --git a/tests/boolean/dafny_comparison/binary_search_trees.heyvl b/tests/boolean/dafny_comparison/binary_search_trees.heyvl
new file mode 100644
index 00000000..00e031f3
--- /dev/null
+++ b/tests/boolean/dafny_comparison/binary_search_trees.heyvl
@@ -0,0 +1,181 @@
+// RUN: @caesar @file
+// Curated from an external Caesar/Dafny comparison corpus.
+// This file groups small operations over a symbolic binary-search tree domain.
+
+domain Tree {
+    func nil(): Tree
+    func node(left: Tree, value: Int, right: Tree): Tree
+
+    func left_child(tree: Tree): Tree
+    axiom left_child_node forall left: Tree, value: Int, right: Tree.
+        left_child(node(left, value, right)) == left
+
+    func root_value(tree: Tree): Int
+    axiom root_value_node forall left: Tree, value: Int, right: Tree.
+        root_value(node(left, value, right)) == value
+
+    func right_child(tree: Tree): Tree
+    axiom right_child_node forall left: Tree, value: Int, right: Tree.
+        right_child(node(left, value, right)) == right
+
+    func is_nil(tree: Tree): Bool
+    axiom is_nil_def forall tree: Tree.
+        is_nil(tree) == (tree == nil())
+
+    axiom node_not_nil forall left: Tree, value: Int, right: Tree.
+        node(left, value, right) != nil()
+
+    func contains(tree: Tree, value: Int): Bool =
+        ite(
+            is_nil(tree),
+            false,
+            (value == root_value(tree)) ||
+            contains(left_child(tree), value) ||
+            contains(right_child(tree), value)
+        )
+
+    func within(tree: Tree, has_lower: Bool, lower: Int, has_upper: Bool, upper: Int): Bool =
+        ite(
+            is_nil(tree),
+            true,
+            (!has_lower || (lower < root_value(tree))) &&
+            (!has_upper || (root_value(tree) < upper)) &&
+            within(left_child(tree), has_lower, lower, true, root_value(tree)) &&
+            within(right_child(tree), true, root_value(tree), has_upper, upper)
+        )
+
+    func is_bst(tree: Tree): Bool =
+        ite(
+            is_nil(tree),
+            true,
+            is_bst(left_child(tree)) &&
+            is_bst(right_child(tree)) &&
+            (forall value: Int. contains(left_child(tree), value) ==> (value < root_value(tree))) &&
+            (forall value: Int. contains(right_child(tree), value) ==> (root_value(tree) < value))
+        )
+
+    func structural_bst(tree: Tree): Bool =
+        within(tree, false, 0, false, 0)
+
+    func min_value(tree: Tree): Int =
+        ite(is_nil(left_child(tree)), root_value(tree), min_value(left_child(tree)))
+
+    func max_value(tree: Tree): Int =
+        ite(is_nil(right_child(tree)), root_value(tree), max_value(right_child(tree)))
+
+}
+
+proc get_min(tree: Tree) -> (result: Int)
+    pre ?(is_bst(tree) && !is_nil(tree))
+    post ?(
+        (result == min_value(tree)) &&
+        contains(tree, result) &&
+        (forall value: Int.
+            (contains(tree, value) && (value != result)) ==> (result < value))
+    )
+{
+    var left: Tree = left_child(tree)
+    var root: Int = root_value(tree)
+    if is_nil(left) {
+        result = root
+    } else {
+        result = get_min(left)
+    }
+}
+
+proc contains_value(tree: Tree, value: Int) -> (present: Bool)
+    post ?(present == contains(tree, value))
+{
+    if is_nil(tree) {
+        present = false
+    } else {
+        var root: Int = root_value(tree)
+        if value == root {
+            present = true
+        } else {
+            var in_left: Bool = contains_value(left_child(tree), value)
+            if in_left {
+                present = true
+            } else {
+                present = contains_value(right_child(tree), value)
+            }
+        }
+    }
+}
+
+proc insert_in_range(
+    tree: Tree,
+    value: Int,
+    has_lower: Bool,
+    lower: Int,
+    has_upper: Bool,
+    upper: Int
+) -> (result: Tree)
+    pre ?(within(tree, has_lower, lower, has_upper, upper))
+    pre ?((!has_lower || (lower < value)) && (!has_upper || (value < upper)))
+    post ?(within(result, has_lower, lower, has_upper, upper))
+    post ?(contains(result, value))
+    post ?(forall witness: Int. contains(tree, witness) ==> contains(result, witness))
+{
+    if is_nil(tree) {
+        result = node(nil(), value, nil())
+    } else {
+        var left: Tree = left_child(tree)
+        var root: Int = root_value(tree)
+        var right: Tree = right_child(tree)
+
+        if value < root {
+            var new_left: Tree = insert_in_range(left, value, has_lower, lower, true, root)
+            result = node(new_left, root, right)
+        } else {
+            if root < value {
+                var new_right: Tree = insert_in_range(right, value, true, root, has_upper, upper)
+                result = node(left, root, new_right)
+            } else {
+                result = tree
+            }
+        }
+    }
+}
+
+proc insert_value(tree: Tree, value: Int) -> (result: Tree)
+    pre ?(structural_bst(tree))
+    post ?(structural_bst(result))
+    post ?(contains(result, value))
+    post ?(forall witness: Int. contains(tree, witness) ==> contains(result, witness))
+{
+    result = insert_in_range(tree, value, false, 0, false, 0)
+}
+
+proc get_max(tree: Tree) -> (result: Int)
+    pre ?(is_bst(tree) && !is_nil(tree))
+    post ?(
+        (result == max_value(tree)) &&
+        contains(tree, result) &&
+        (forall value: Int.
+            (contains(tree, value) && (value != result)) ==> (value < result))
+    )
+{
+    var right: Tree = right_child(tree)
+    var root: Int = root_value(tree)
+    if is_nil(right) {
+        result = root
+    } else {
+        result = get_max(right)
+    }
+}
+
+proc insert_example() -> ()
+{
+    var tree: Tree = nil()
+    tree = insert_value(tree, 4)
+    tree = insert_value(tree, 2)
+    tree = insert_value(tree, 8)
+    tree = insert_value(tree, 6)
+
+    assert ?(structural_bst(tree))
+    assert ?(contains(tree, 2))
+    assert ?(contains(tree, 4))
+    assert ?(contains(tree, 6))
+    assert ?(contains(tree, 8))
+}
diff --git a/tests/boolean/dafny_comparison/bubble_sort.heyvl b/tests/boolean/dafny_comparison/bubble_sort.heyvl
new file mode 100644
index 00000000..1ac6b6e3
--- /dev/null
+++ b/tests/boolean/dafny_comparison/bubble_sort.heyvl
@@ -0,0 +1,91 @@
+// RUN: @caesar @file
+// Curated from an external Caesar/Dafny comparison corpus.
+// This file keeps a proof-oriented bubble-sort implementation over built-in lists.
+
+proc sort_pair_at(input: []Int, index: UInt) -> (result: []Int)
+    pre ?(index + 1 < len(input))
+    post ?(
+        (len(result) == len(input)) &&
+        (select(result, index) <= select(result, index + 1)) &&
+        (forall k: UInt.
+            ((k < len(input)) && (k != index) && (k != index + 1)) ==>
+                (select(result, k) == select(input, k)))
+    )
+{
+    if select(input, index) > select(input, index + 1) {
+        var left: Int = select(input, index)
+        var right: Int = select(input, index + 1)
+        result = store(input, index, right)
+        result = store(result, index + 1, left)
+    } else {
+        result = input
+    }
+}
+
+proc bubble_sort(input: []Int) -> (sorted: []Int)
+    post ?(
+        (len(input) == len(sorted)) &&
+        (forall p: UInt, q: UInt.
+            ((p < q) && (q < len(sorted))) ==> (select(sorted, p) <= select(sorted, q)))
+    )
+{
+    sorted = input
+    var i: UInt = 0
+    var last: UInt = ite(0 < len(sorted), len(sorted) - 1, 0)
+
+    @invariant(?(
+        (i <= last) &&
+        (len(input) == len(sorted)) &&
+        (forall p: UInt, q: UInt.
+            ((last - i <= p) && (p < q) && (q <= last) && (last < len(sorted))) ==>
+                (select(sorted, p) <= select(sorted, q))) &&
+        (forall p: UInt, q: UInt.
+            ((p < last - i) && (last - i < q) && (q < len(sorted))) ==>
+                (select(sorted, p) <= select(sorted, q)))
+    ))
+    while 0 < last - i {
+        var j: UInt = 0
+
+        @invariant(?(
+            (j <= last - i) &&
+            (len(input) == len(sorted)) &&
+            (forall p: UInt, q: UInt.
+                ((last - i <= p) && (p < q) && (q <= last) && (last < len(sorted))) ==>
+                    (select(sorted, p) <= select(sorted, q))) &&
+            (forall p: UInt, q: UInt.
+                ((p < last - i) && (last - i < q) && (q < len(sorted))) ==>
+                    (select(sorted, p) <= select(sorted, q))) &&
+            (forall k: UInt. (k <= j) ==> (select(sorted, k) <= select(sorted, j)))
+        ))
+        while j < last - i {
+            if select(sorted, j) > select(sorted, j + 1) {
+                var left: Int = select(sorted, j)
+                var right: Int = select(sorted, j + 1)
+                sorted = store(sorted, j, right)
+                sorted = store(sorted, j + 1, left)
+            } else {}
+
+            j = j + 1
+        }
+
+        i = i + 1
+    }
+}
+
+proc bubble_sort_example() -> ()
+{
+    var input: []Int
+    assume ?(len(input) == 5)
+    input = store(input, 0, 3)
+    input = store(input, 1, 2)
+    input = store(input, 2, 5)
+    input = store(input, 3, 1)
+    input = store(input, 4, 4)
+
+    var sorted: []Int = bubble_sort(input)
+    assert ?(
+        forall p: UInt, q: UInt.
+            ((p < q) && (q < len(sorted))) ==> (select(sorted, p) <= select(sorted, q))
+    )
+    assert ?(len(sorted) == 5)
+}
diff --git a/tests/boolean/dafny_comparison/insertion_sort.heyvl b/tests/boolean/dafny_comparison/insertion_sort.heyvl
new file mode 100644
index 00000000..d94f14b5
--- /dev/null
+++ b/tests/boolean/dafny_comparison/insertion_sort.heyvl
@@ -0,0 +1,80 @@
+// RUN: @caesar verify --function-encoding fuel-param-computation --max-fuel 8 @file
+// Invented for the Caesar/Dafny comparison corpus.
+// This file keeps a small insertion-sort development over a symbolic cons-list model.
+
+domain List {
+    func nil(): List
+    func cons(head: Int, tail: List): List
+
+    func head(list: List): Int
+    axiom head_cons forall value: Int, rest: List.
+        head(cons(value, rest)) == value
+
+    func tail(list: List): List
+    axiom tail_cons forall value: Int, rest: List.
+        tail(cons(value, rest)) == rest
+
+    func is_nil(list: List): Bool
+    axiom is_nil_def forall list: List.
+        is_nil(list) == (list == nil())
+
+    axiom cons_not_nil forall value: Int, rest: List.
+        cons(value, rest) != nil()
+
+    func insert_sorted(value: Int, list: List): List =
+        ite(
+            is_nil(list),
+            cons(value, nil()),
+            ite(
+                value <= head(list),
+                cons(value, list),
+                cons(head(list), insert_sorted(value, tail(list)))
+            )
+        )
+
+    func insertion_sorted(list: List): List =
+        ite(
+            is_nil(list),
+            nil(),
+            insert_sorted(head(list), insertion_sorted(tail(list)))
+        )
+}
+
+proc insert_sorted_value(value: Int, list: List) -> (result: List)
+    post ?(result == insert_sorted(value, list))
+{
+    if is_nil(list) {
+        result = cons(value, nil())
+    } else {
+        var first: Int = head(list)
+        var rest: List = tail(list)
+        if value <= first {
+            result = cons(value, list)
+        } else {
+            var inserted_rest: List = insert_sorted_value(value, rest)
+            result = cons(first, inserted_rest)
+        }
+    }
+}
+
+proc insertion_sort(list: List) -> (result: List)
+    post ?(result == insertion_sorted(list))
+{
+    if is_nil(list) {
+        result = nil()
+    } else {
+        var first: Int = head(list)
+        var rest: List = tail(list)
+        var sorted_rest: List = insertion_sort(rest)
+        result = insert_sorted_value(first, sorted_rest)
+    }
+}
+
+proc insertion_sort_example() -> ()
+{
+    var input: List =
+        cons(3, cons(2, cons(5, cons(1, cons(4, nil())))))
+
+    var result: List = insertion_sort(input)
+    assert ?(result == cons(1, cons(2, cons(3, cons(4, cons(5, nil()))))))
+}
diff --git a/tests/boolean/dafny_comparison/left_pad.heyvl b/tests/boolean/dafny_comparison/left_pad.heyvl
new file mode 100644
index 00000000..20705fe0
--- /dev/null
+++ b/tests/boolean/dafny_comparison/left_pad.heyvl
@@ -0,0 +1,49 @@
+// RUN: @caesar @file
+// Curated from an external Caesar/Dafny comparison corpus.
+// This example pads a symbolic list on the left until it reaches the requested width.
+
+domain List {
+    func nil(): List
+    func cons(head: Int, tail: List): List
+
+    func head(list: List): Int
+    axiom head_cons forall value: Int, rest: List.
+        head(cons(value, rest)) == value
+
+    func tail(list: List): List
+    axiom tail_cons forall value: Int, rest: List.
+        tail(cons(value, rest)) == rest
+
+    func is_nil(list: List): Bool
+    axiom is_nil_def forall list: List.
+        is_nil(list) == (list == nil())
+
+    axiom cons_not_nil forall value: Int, rest: List.
+        cons(value, rest) != nil()
+
+    func length(list: List): UInt =
+        ite(is_nil(list), 0, 1 + length(tail(list)))
+
+    func select(list: List, index: UInt): Int =
+        ite(is_nil(list), 0, ite(index == 0, head(list), select(tail(list), index - 1)))
+
+    func padding(width: UInt, list: List): UInt =
+        ite(width < length(list), 0, width - length(list))
+}
+
+proc left_pad(list: List, width: UInt, fill: Int) -> (result: List)
+    post ?(
+        (length(result) == ite(width < length(list), length(list), width)) &&
+        (forall i: UInt.
+            (i < padding(width, list)) ==> (select(result, i) == fill)) &&
+        (forall j: UInt.
+            ((padding(width, list) <= j) && (j < length(result))) ==>
+                (select(result, j) == select(list, j - padding(width, list))))
+    )
+{
+    if width <= length(list) {
+        result = list
+    } else {
+        result = left_pad(cons(fill, list), width, fill)
+    }
+}
diff --git a/tests/boolean/dafny_comparison/list_operations.heyvl b/tests/boolean/dafny_comparison/list_operations.heyvl
new file mode 100644
index 00000000..f3bf3bfc
--- /dev/null
+++ b/tests/boolean/dafny_comparison/list_operations.heyvl
@@ -0,0 +1,82 @@
+// RUN: @caesar @file
+// Curated from an external Caesar/Dafny comparison corpus.
+// This file collects a few symbolic list operations over a small cons-list model.
+
+domain List {
+    func nil(): List
+    func cons(head: Int, tail: List): List
+
+    func head(list: List): Int
+    axiom head_cons forall value: Int, rest: List.
+        head(cons(value, rest)) == value
+
+    func tail(list: List): List
+    axiom tail_cons forall value: Int, rest: List.
+        tail(cons(value, rest)) == rest
+
+    func is_nil(list: List): Bool
+    axiom is_nil_def forall list: List.
+        is_nil(list) == (list == nil())
+
+    axiom cons_not_nil forall value: Int, rest: List.
+        cons(value, rest) != nil()
+
+    func length(list: List): UInt =
+        ite(is_nil(list), 0, 1 + length(tail(list)))
+
+    func select(list: List, index: UInt): Int =
+        ite(is_nil(list), 0, ite(index == 0, head(list), select(tail(list), index - 1)))
+}
+
+proc store_at(list: List, index: UInt, value: Int) -> (result: List)
+    pre ?(index < length(list))
+    post ?(
+        (length(result) == length(list)) &&
+        (select(result, index) == value) &&
+        (forall k: UInt.
+            ((k < length(list)) && (k != index)) ==> (select(result, k) == select(list, k)))
+    )
+{
+    if is_nil(list) {
+        result = list
+    } else {
+        var first: Int = head(list)
+        var rest: List = tail(list)
+        if index == 0 {
+            result = cons(value, rest)
+        } else {
+            var updated_rest: List = store_at(rest, index - 1, value)
+            result = cons(first, updated_rest)
+        }
+    }
+}
+
+proc append_value(list: List, value: Int) -> (result: List)
+    post ?(
+        (length(result) == length(list) + 1) &&
+        (select(result, length(list)) == value) &&
+        (forall k: UInt.
+            (k < length(list)) ==> (select(result, k) == select(list, k)))
+    )
+{
+    if is_nil(list) {
+        result = cons(value, nil())
+    } else {
+        var first: Int = head(list)
+        var rest: List = tail(list)
+        var extended_rest: List = append_value(rest, value)
+        result = cons(first, extended_rest)
+    }
+}
+
+proc get_last(list: List) -> (result: Int)
+    pre ?(!is_nil(list))
+    post ?(result == select(list, length(list) - 1))
+{
+    var rest: List = tail(list)
+    if is_nil(rest) {
+        result = head(list)
+    } else {
+        result = get_last(rest)
+    }
+}
diff --git a/tests/boolean/dafny_comparison/quicksort.heyvl b/tests/boolean/dafny_comparison/quicksort.heyvl
new file mode 100644
index 00000000..8c94cf93
--- /dev/null
+++ b/tests/boolean/dafny_comparison/quicksort.heyvl
@@ -0,0 +1,81 @@
+// RUN: @caesar verify --function-encoding fuel-param-computation --max-fuel 8 @file
+// Invented for the Caesar/Dafny comparison corpus.
+// This file keeps a small quicksort development over a symbolic cons-list model.
+
+domain List {
+    func nil(): List
+    func cons(head: Int, tail: List): List
+
+    func head(list: List): Int
+    axiom head_cons forall value: Int, rest: List.
+        head(cons(value, rest)) == value
+
+    func tail(list: List): List
+    axiom tail_cons forall value: Int, rest: List.
+        tail(cons(value, rest)) == rest
+
+    func is_nil(list: List): Bool
+    axiom is_nil_def forall list: List.
+        is_nil(list) == (list == nil())
+
+    axiom cons_not_nil forall value: Int, rest: List.
+        cons(value, rest) != nil()
+
+    func append(left: List, right: List): List =
+        ite(is_nil(left), right, cons(head(left), append(tail(left), right)))
+
+    func filter_leq(pivot: Int, list: List): List =
+        ite(
+            is_nil(list),
+            nil(),
+            ite(
+                head(list) <= pivot,
+                cons(head(list), filter_leq(pivot, tail(list))),
+                filter_leq(pivot, tail(list))
+            )
+        )
+
+    func filter_gt(pivot: Int, list: List): List =
+        ite(
+            is_nil(list),
+            nil(),
+            ite(
+                pivot < head(list),
+                cons(head(list), filter_gt(pivot, tail(list))),
+                filter_gt(pivot, tail(list))
+            )
+        )
+
+    func quicksorted(list: List): List =
+        ite(
+            is_nil(list),
+            nil(),
+            append(
+                quicksorted(filter_leq(head(list), tail(list))),
+                cons(head(list), quicksorted(filter_gt(head(list), tail(list))))
+            )
+        )
+}
+
+proc quicksort(list: List) -> (result: List)
+    post ?(result == quicksorted(list))
+{
+    if is_nil(list) {
+        result = nil()
+    } else {
+        var pivot: Int = head(list)
+        var rest: List = tail(list)
+        var lower: List = quicksort(filter_leq(pivot, rest))
+        var greater: List = quicksort(filter_gt(pivot, rest))
+        result = append(lower, cons(pivot, greater))
+    }
+}
+
+proc quicksort_example() -> ()
+{
+    var input: List =
+        cons(3, cons(2, cons(5, cons(1, cons(4, nil())))))
+
+    var result: List = quicksort(input)
+    assert ?(result == quicksorted(input))
+}
diff --git a/tests/boolean/dafny_comparison/selection_sort.heyvl b/tests/boolean/dafny_comparison/selection_sort.heyvl
new file mode 100644
index 00000000..9df010e3
--- /dev/null
+++ b/tests/boolean/dafny_comparison/selection_sort.heyvl
@@ -0,0 +1,78 @@
+// RUN: @caesar @file
+// Invented for the Caesar/Dafny comparison corpus.
+// This file keeps a small selection-sort development over built-in lists.
+
+proc min_index_from(input: []Int, start: UInt) -> (index: UInt)
+    pre ?(start < len(input))
+    post ?(
+        (start <= index) &&
+        (index < len(input)) &&
+        (forall k: UInt.
+            ((start <= k) && (k < len(input))) ==> (select(input, index) <= select(input, k)))
+    )
+{
+    index = start
+    var j: UInt = start
+
+    @invariant(?(
+        (start <= index) &&
+        (index < len(input)) &&
+        (start <= j) &&
+        (j <= len(input)) &&
+        (forall k: UInt.
+            ((start <= k) && (k < j)) ==> (select(input, index) <= select(input, k)))
+    ))
+    while j < len(input) {
+        if select(input, j) < select(input, index) {
+            index = j
+        } else {}
+
+        j = j + 1
+    }
+}
+
+proc selection_sort(input: []Int) -> (sorted: []Int)
+    post ?(
+        (len(input) == len(sorted)) &&
+        (forall p: UInt, q: UInt.
+            ((p < q) && (q < len(sorted))) ==> (select(sorted, p) <= select(sorted, q)))
+    )
+{
+    sorted = input
+    var i: UInt = 0
+
+    @invariant(?(
+        (i <= len(sorted)) &&
+        (len(input) == len(sorted)) &&
+        (forall p: UInt, q: UInt.
+            ((p < q) && (q < i)) ==> (select(sorted, p) <= select(sorted, q))) &&
+        (forall p: UInt, q: UInt.
+            ((p < i) && (i <= q) && (q < len(sorted))) ==> (select(sorted, p) <= select(sorted, q)))
+    ))
+    while i < len(sorted) {
+        var min: UInt = min_index_from(sorted, i)
+        var first: Int = select(sorted, i)
+        var least: Int = select(sorted, min)
+        sorted = store(sorted, i, least)
+        sorted = store(sorted, min, first)
+        i = i + 1
+    }
+}
+
+proc selection_sort_example() -> ()
+{
+    var input: []Int
+    assume ?(len(input) == 5)
+    input = store(input, 0, 3)
+    input = store(input, 1, 2)
+    input = store(input, 2, 5)
+    input = store(input, 3, 1)
+    input = store(input, 4, 4)
+
+    var sorted: []Int = selection_sort(input)
+    assert ?(
+        forall p: UInt, q: UInt.
+            ((p < q) && (q < len(sorted))) ==> (select(sorted, p) <= select(sorted, q))
+    )
+    assert ?(len(sorted) == 5)
+}
diff --git a/tests/dafny/all_scope.heyvl b/tests/dafny/all_scope.heyvl
new file mode 100644
index 00000000..9fe53b24
--- /dev/null
+++ b/tests/dafny/all_scope.heyvl
@@ -0,0 +1,22 @@
+// RUN: bash -c 'dir=$(mktemp -d); @caesar dafny --filter "root$" @file --dafny-dir "$dir" --dafny-scope all; out="$dir/tests/dafny/all_scope.dfy"; grep -q "method helper" "$out" && grep -q "method root" "$out" && grep -q "method unused" "$out"'
+
+proc helper(x: UInt) -> (y: UInt)
+    pre ?(true)
+    post ?(y == x)
+{
+    y = x
+}
+
+proc root(x: UInt) -> (y: UInt)
+    pre ?(true)
+    post ?(y == x)
+{
+    y = helper(x)
+}
+
+proc unused(x: UInt) -> (y: UInt)
+    pre ?(true)
+    post ?(y == x)
+{
+    y = x
+}
diff --git a/tests/dafny/all_skip_unsupported.heyvl b/tests/dafny/all_skip_unsupported.heyvl
new file mode 100644
index 00000000..e1141b6b
--- /dev/null
+++ b/tests/dafny/all_skip_unsupported.heyvl
@@ -0,0 +1,13 @@
+// RUN: bash -c 'dir=$(mktemp -d); out=$(@caesar dafny --filter "root$" @file --dafny-dir "$dir" --dafny-scope all 2>&1); status=$?; test $status -eq 0; printf "%s" "$out" | grep -q "coproc ghost"; dfy="$dir/tests/dafny/all_skip_unsupported.dfy"; grep -q "method root" "$dfy" && ! grep -q "method ghost" "$dfy"'
+
+proc root(x: UInt) -> (y: UInt)
+    pre ?(true)
+    post ?(y == x)
+{
+    y = x
+}
+
+coproc ghost() -> ()
+    pre ?(false)
+    post ?(false)
+{}
diff --git a/tests/dafny/comparison_binary_search_trees.heyvl b/tests/dafny/comparison_binary_search_trees.heyvl
new file mode 100644
index 00000000..c62407cc
--- /dev/null
+++ b/tests/dafny/comparison_binary_search_trees.heyvl
@@ -0,0 +1 @@
+// RUN: bash -c 'dir=$(mktemp -d); @caesar dafny tests/boolean/dafny_comparison/binary_search_trees.heyvl --dafny-dir "$dir"; out="$dir/tests/boolean/dafny_comparison/binary_search_trees.dfy"; grep -q "type Tree(0,==)" "$out" && grep -q "function within" "$out" && grep -q "method contains_value" "$out" && grep -q "method insert_value" "$out" && grep -q "method get_min" "$out" && grep -q "method get_max" "$out"'
diff --git a/tests/dafny/comparison_bubble_sort.heyvl b/tests/dafny/comparison_bubble_sort.heyvl
new file mode 100644
index 00000000..ca78175e
--- /dev/null
+++ b/tests/dafny/comparison_bubble_sort.heyvl
@@ -0,0 +1 @@
+// RUN: bash -c 'dir=$(mktemp -d); @caesar dafny tests/boolean/dafny_comparison/bubble_sort.heyvl --dafny-dir "$dir"; out="$dir/tests/boolean/dafny_comparison/bubble_sort.dfy"; grep -q "method sort_pair_at" "$out" && grep -q "method bubble_sort" "$out" && grep -q "method bubble_sort_example" "$out"'
diff --git a/tests/dafny/comparison_insertion_sort.heyvl b/tests/dafny/comparison_insertion_sort.heyvl
new file mode 100644
index 00000000..0c0dcf4d
--- /dev/null
+++ b/tests/dafny/comparison_insertion_sort.heyvl
@@ -0,0 +1 @@
+// RUN: bash -c 'dir=$(mktemp -d); @caesar dafny tests/boolean/dafny_comparison/insertion_sort.heyvl --dafny-dir "$dir"; out="$dir/tests/boolean/dafny_comparison/insertion_sort.dfy"; grep -q "type List(0,==)" "$out" && grep -q "function insert_sorted" "$out" && grep -q "function insertion_sorted" "$out" && grep -q "method insertion_sort" "$out" && grep -q "method insertion_sort_example" "$out"'
diff --git a/tests/dafny/comparison_left_pad.heyvl b/tests/dafny/comparison_left_pad.heyvl
new file mode 100644
index 00000000..f768da84
--- /dev/null
+++ b/tests/dafny/comparison_left_pad.heyvl
@@ -0,0 +1 @@
+// RUN: bash -c 'dir=$(mktemp -d); @caesar dafny tests/boolean/dafny_comparison/left_pad.heyvl --dafny-dir "$dir"; out="$dir/tests/boolean/dafny_comparison/left_pad.dfy"; grep -q "type List(0,==)" "$out" && grep -q "method left_pad" "$out"'
diff --git a/tests/dafny/comparison_list_operations.heyvl b/tests/dafny/comparison_list_operations.heyvl
new file mode 100644
index 00000000..a7a42b98
--- /dev/null
+++ b/tests/dafny/comparison_list_operations.heyvl
@@ -0,0 +1 @@
+// RUN: bash -c 'dir=$(mktemp -d); @caesar dafny tests/boolean/dafny_comparison/list_operations.heyvl --dafny-dir "$dir"; out="$dir/tests/boolean/dafny_comparison/list_operations.dfy"; grep -q "type List(0,==)" "$out" && grep -q "method store_at" "$out" && grep -q "method append_value" "$out" && grep -q "method get_last" "$out"'
diff --git a/tests/dafny/comparison_quicksort.heyvl b/tests/dafny/comparison_quicksort.heyvl
new file mode 100644
index 00000000..561072cd
--- /dev/null
+++ b/tests/dafny/comparison_quicksort.heyvl
@@ -0,0 +1 @@
+// RUN: bash -c 'dir=$(mktemp -d); @caesar dafny tests/boolean/dafny_comparison/quicksort.heyvl --dafny-dir "$dir"; out="$dir/tests/boolean/dafny_comparison/quicksort.dfy"; grep -q "type List(0,==)" "$out" && grep -q "function append" "$out" && grep -q "function quicksorted" "$out" && grep -q "method quicksort" "$out"'
diff --git a/tests/dafny/comparison_selection_sort.heyvl b/tests/dafny/comparison_selection_sort.heyvl
new file mode 100644
index 00000000..09ac24b2
--- /dev/null
+++ b/tests/dafny/comparison_selection_sort.heyvl
@@ -0,0 +1 @@
+// RUN: bash -c 'dir=$(mktemp -d); @caesar dafny tests/boolean/dafny_comparison/selection_sort.heyvl --dafny-dir "$dir"; out="$dir/tests/boolean/dafny_comparison/selection_sort.dfy"; grep -q "method min_index_from" "$out" && grep -q "method selection_sort" "$out" && grep -q "method selection_sort_example" "$out"'
diff --git a/tests/dafny/reachable_scope.heyvl b/tests/dafny/reachable_scope.heyvl
new file mode 100644
index 00000000..243169fc
--- /dev/null
+++ b/tests/dafny/reachable_scope.heyvl
@@ -0,0 +1,22 @@
+// RUN: bash -c 'dir=$(mktemp -d); @caesar dafny --filter "root$" @file --dafny-dir "$dir"; out="$dir/tests/dafny/reachable_scope.dfy"; grep -q "method helper" "$out" && grep -q "method root" "$out" && ! grep -q "method unused" "$out"'
+
+proc helper(x: UInt) -> (y: UInt)
+    pre ?(true)
+    post ?(y == x)
+{
+    y = x
+}
+
+proc root(x: UInt) -> (y: UInt)
+    pre ?(true)
+    post ?(y == x)
+{
+    y = helper(x)
+}
+
+proc unused(x: UInt) -> (y: UInt)
+    pre ?(true)
+    post ?(y == x)
+{
+    y = x
+}
diff --git a/tests/dafny/required_unsupported.heyvl b/tests/dafny/required_unsupported.heyvl
new file mode 100644
index 00000000..928b4bc7
--- /dev/null
+++ b/tests/dafny/required_unsupported.heyvl
@@ -0,0 +1,8 @@
+// RUN: bash -c 'out=$(@caesar dafny --filter "root$" @file --dafny-dir "$(mktemp -d)" 2>&1); status=$?; test $status -ne 0; printf "%s" "$out" | grep -q "intrinsic procedure"'
+
+proc root() -> (b: Bool)
+    pre ?(true)
+    post ?(b == true || b == false)
+{
+    b = flip(0.5)
+}
diff --git a/website/docs/caesar/README.md b/website/docs/caesar/README.md
index 8c8a1016..e76187dc 100644
--- a/website/docs/caesar/README.md
+++ b/website/docs/caesar/README.md
@@ -4,7 +4,7 @@ sidebar_position: 6
 
 # The Caesar Tool
 
-The `caesar` binary contains all of Caesar's functionality: verifying HeyVL files, [checking entailments](./entailment.md), running the [LSP server](./vscode-and-lsp.md), and [translation support for model checking](../model-checking.md).
+The `caesar` binary contains all of Caesar's functionality: verifying HeyVL files, [checking entailments](./entailment.md), running the [LSP server](./vscode-and-lsp.md), [translation support for model checking](../model-checking.md), and an experimental [Dafny backend](../dafny.md).
 
 **Print help:**
 The command-line help information is much more detailed than this document.
@@ -51,6 +51,11 @@ Set a memory limit of 16000 megabytes with `--mem 16000`.
 The `caesar entailment` subcommand checks whether one `coproc`'s verification condition entails one `proc`'s verification condition.
 See [Entailment Checking](./entailment.md) for more information.
 
+## Subcommand `caesar dafny`
+
+The `caesar dafny` subcommand exports a supported Boolean fragment of HeyVL to Dafny and can optionally run `dafny verify` on the generated files.
+See the dedicated [Dafny backend documentation](../dafny.md) for the supported fragment, translation strategy, and command-line options.
+
 ## More Topics
 
 ```mdx-code-block
diff --git a/website/docs/dafny.md b/website/docs/dafny.md
new file mode 100644
index 00000000..a1c6d51a
--- /dev/null
+++ b/website/docs/dafny.md
@@ -0,0 +1,161 @@
+---
+sidebar_position: 8
+description: Caesar can export a Boolean fragment of HeyVL to Dafny.
+---
+
+# Dafny Backend
+
+Caesar can export a supported Boolean fragment of HeyVL to [Dafny](https://dafny.org/).
+This backend is **experimental** and currently aimed at **proof-oriented, Boolean** HeyVL programs:
+top-level `proc`s with classical control flow, specifications of the form `?(b)`, and a small set of helper declarations.
+
+The output is intended to be useful for verification, not especially idiomatic Dafny.
+Generated methods use `decreases *`, declarations without bodies are translated axiomatically, and some translated files still need manual cleanup before Dafny accepts them.
+
+## Usage
+
+For a simple example, consider the following HeyVL procedure:
+
+```heyvl
+proc max_value(x: Int, y: Int) -> (m: Int)
+    post ?(x <= m && y <= m)
+    post ?(m == x || m == y)
+{
+    if x <= y {
+        m = y
+    } else {
+        m = x
+    }
+}
+```
+
+This is the kind of input the backend is designed for:
+classical control flow with Boolean specifications written as `?(b)`.
+
+To export the file to Dafny, run:
+
+```bash
+caesar dafny example.heyvl --dafny-dir out --run-dafny
+```
+
+Caesar emits **one `.dfy` file per input `.heyvl` file** and mirrors the input path under the output directory.
+The generated Dafny will contain a method shaped roughly like this:
+
+```dafny
+method max_value(x: int, y: int) returns (m: int)
+    ensures ((x <= m) && (y <= m))
+    ensures ((m == x) || (m == y))
+    decreases *
+{
+    if (x <= y) {
+        m := y;
+    } else {
+        m := x;
+    }
+}
+```
+
+In particular:
+
+ * the output file is written as `out/.../example.dfy`
+ * each `post ?(...)` becomes a Dafny `ensures`
+ * a `proc` with a body becomes a Dafny `method` with `decreases *`
+ * `--run-dafny` asks Caesar to invoke `dafny verify` on the generated file
+
+For example,
+
+```text
+tests/boolean/procs/proc-smoke.heyvl
+```
+
+is written to
+
+```text
+out/tests/boolean/procs/proc-smoke.dfy
+```
+
+This requires the `dafny` executable to be available on the [`PATH`](https://en.wikipedia.org/wiki/PATH_(variable)).
+If `--run-dafny` is used without `--dafny-dir`, Caesar writes the generated files to a temporary directory and verifies them there.
+
+The command is also available as:
+
+```bash
+caesar to-dafny ...
+```
+
+`--filter <regex>` selects the root procedures to translate.
+`--dafny-scope reachable` (the default) emits the selected procedures together with everything reachable from them.
+`--dafny-scope all` emits every declaration from the selected file that the backend can translate, plus any reachable helpers needed from other files.
+Unsupported declarations that are unreachable in `all` mode are skipped with a warning; unsupported required declarations still make translation fail.
+
+## Supported Fragment
+
+The backend expects ordinary HeyVL input using supported declarations and Boolean specifications.
+Quantitative features and most proof-rule-specific encodings are out of scope.
+
+### Declarations
+
+ * top-level `proc` declarations
+ * domain declarations
+ * definitional `func`s
+ * functions without bodies
+ * axioms
+
+### Specifications and Statements
+
+ * `pre` and `post` conditions of the form `?(b)`
+ * `assert ?(b)` and `assume ?(b)`
+ * assignments, blocks, local variables, and conditionals
+ * recursive and non-recursive procedure calls
+ * `while` loops written as `@invariant(?(...)) while ...`
+ * `havoc`
+
+### Expressions and Types
+
+ * `Bool`, `Int`, `UInt`
+ * lists `[]T`, translated to Dafny sequences `seq<T>`
+ * arithmetic and comparison operators
+ * `&&`, `||`, `==>`, `!`, and `ite`
+ * `forall` and `exists`
+ * function and procedure calls
+ * built-in list intrinsics `len`, `select`, and `store`
+ * explicit quantifier triggers
+
+## Translation
+
+The translation is intentionally direct.
+The most important choices are:
+
+ * `Bool` becomes `bool`, `Int` becomes `int`, `UInt` becomes `nat`, and `[]T` becomes `seq<T>`.
+ * Abstract HeyVL domains become Dafny type declarations of the form `type D(0,==)`.
+ * `proc`s with bodies become Dafny `method`s with `decreases *`.
+ * `proc`s without bodies become `method {:axiom}` declarations.
+ * Definitional HeyVL functions become Dafny `function`s or `predicate`s.
+ * `assert ?(b)` becomes `assert b`.
+ * `assume ?(b)` becomes `assume {:axiom} b`.
+ * `@invariant(?(b)) while ...` becomes a Dafny loop invariant together with `decreases *`.
+ * Reachable HeyVL axioms are inserted as `assume {:axiom} ...;` statements into translated method bodies.
+
+## Limitations
+
+The backend currently does **not** support:
+
+ * `coproc`
+ * probabilistic primitives such as `flip`
+ * quantitative expressions, quantitative casts, and non-Boolean embeddings
+ * proof-rule-specific encodings and the richer quantitative core language
+ * most proof-rule annotations beyond `@invariant(?(...))`
+
+Some translated files still need manual adjustment before they pass `dafny verify`.
+The most common issue at the moment is Dafny rejecting recursive helper functions over symbolic domains for lack of an acceptable termination argument.
+
+At the moment, the backend is best viewed as a working export path for a supported Boolean fragment and a basis for experimenting with Dafny-oriented encodings.
+
+## Examples
+
+The repository contains small examples that exercise the backend:
+
+ * translation smoke tests in [tests/dafny](https://github.com/moves-rwth/caesar/tree/main/tests/dafny)
+ * curated Boolean examples in [tests/boolean/dafny_comparison](https://github.com/moves-rwth/caesar/tree/main/tests/boolean/dafny_comparison)
+
+These include sequence-based sorting examples, symbolic list examples, and symbolic binary-search-tree examples.
diff --git a/website/src/theme/prism-include-languages.js b/website/src/theme/prism-include-languages.js
index b7338629..a30a5ef1 100644
--- a/website/src/theme/prism-include-languages.js
+++ b/website/src/theme/prism-include-languages.js
@@ -16,5 +16,6 @@ export default function prismIncludeLanguages(PrismObject) {
     require(`prismjs/components/prism-${lang}`);
   });
   require(`./prism-language-heyvl`);
+  require(`./prism-language-dafny`);
   delete globalThis.Prism;
 }
diff --git a/website/src/theme/prism-language-dafny.js b/website/src/theme/prism-language-dafny.js
new file mode 100644
index 00000000..04d0167c
--- /dev/null
+++ b/website/src/theme/prism-language-dafny.js
@@ -0,0 +1,24 @@
+Prism.languages.dafny = {
+	'comment': {
+		pattern: /\/\/.*|\/\*[\s\S]*?(?:\*\/|$)/,
+		greedy: true
+	},
+	'string': {
+		pattern: /"(?:\\.|[^"\\])*"/,
+		greedy: true
+	},
+	'attribute': {
+		pattern: /\{:[^{}]*\}/,
+		inside: {
+			'keyword': /\b(?:axiom|trigger)\b/,
+			'punctuation': /[{}:]/
+		}
+	},
+	'keyword': /\b(?:abstract|assert|assume|break|by|calc|case|class|const|constructor|continue|datatype|decreases|else|ensures|exists|false|for|forall|function|ghost|if|in|include|invariant|import|is|label|lemma|match|method|modifies|module|nat|new|null|old|predicate|print|reads|refines|requires|return|returns|reveals|seq|set|static|then|trait|true|type|var|while|witness)\b/,
+	'boolean': /\b(?:false|true)\b/,
+	'number': /-?\b\d+(?:\.\d+)?\b/,
+	'operator': /&&|\|\||==>|:=|==|!=|<=|>=|<|>|\+|-|\*|\/|%|!/,
+	'punctuation': /[()[\]{}.,;:]/,
+};
+
+Prism.languages.dfy = Prism.languages.dafny;