diff --git a/Cargo.lock b/Cargo.lock
index dfa1bc9..b334d65 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -765,6 +765,13 @@ version = "0.2.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "ebc1c04c71510c7f702b52b7c350734c9ff1295c464a03335b00bb84fc54f853"
 
+[[package]]
+name = "verifier"
+version = "0.1.0"
+dependencies = [
+ "jeff-format",
+]
+
 [[package]]
 name = "walkdir"
 version = "2.5.0"
diff --git a/Cargo.toml b/Cargo.toml
index 933795a..4d5c416 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -3,7 +3,7 @@ lto = "thin"
 
 [workspace]
 resolver = "2"
-members = ["impl/rs"]
+members = ["impl/rs", "tools/verifier"]
 
 [workspace.package]
 rust-version = "1.85"
diff --git a/examples/entangled_calls/entangled_calls.jeff b/examples/entangled_calls/entangled_calls.jeff
index a506f32..b58979e 100644
Binary files a/examples/entangled_calls/entangled_calls.jeff and b/examples/entangled_calls/entangled_calls.jeff differ
diff --git a/examples/entangled_calls/entangled_calls.txt b/examples/entangled_calls/entangled_calls.txt
index d431727..40ee93e 100644
--- a/examples/entangled_calls/entangled_calls.txt
+++ b/examples/entangled_calls/entangled_calls.txt
@@ -10,7 +10,7 @@
                     sources = [],
                     targets = [49],
                     operations = [
-                        (outputs = [0], instruction = (int = (const8 = 1))),
+                        (outputs = [0], instruction = (int = (const1 = true))),
                         (outputs = [1], instruction = (qubit = (alloc = void))),
                         (outputs = [2], instruction = (qubit = (alloc = void))),
                         (outputs = [3], instruction = (qubit = (alloc = void))),
@@ -21,7 +21,7 @@
                         (inputs = [8, 3], outputs = [9, 10], instruction = (qubit = (gate = (custom = (name = 5, numQubits = 1), controlQubits = 1)))),
                         (inputs = [10, 4], outputs = [11, 12], instruction = (qubit = (gate = (custom = (name = 5, numQubits = 1), controlQubits = 1)))),
                         (inputs = [12, 5], outputs = [13, 14], instruction = (qubit = (gate = (custom = (name = 5, numQubits = 1), controlQubits = 1)))),
-                        (outputs = [15], instruction = (intArray = (const8 = [0, 0, 0, 0, 0]))),
+                        (outputs = [15], instruction = (intArray = (const1 = [false, false, false, false, false]))),
                         (inputs = [7], outputs = [16], instruction = (qubit = (measure = void))),
                         (outputs = [17], instruction = (int = (const32 = 0))),
                         (inputs = [15, 17, 16], outputs = [18], instruction = (intArray = (setIndex = void))),
@@ -59,23 +59,23 @@
                     ]
                 ),
                 values = [
-                    (type = (int = 8)), (type = (qubit = void)), (type = (qubit = void)),
+                    (type = (int = 1)), (type = (qubit = void)), (type = (qubit = void)),
                     (type = (qubit = void)), (type = (qubit = void)), (type = (qubit = void)),
                     (type = (qubit = void)), (type = (qubit = void)), (type = (qubit = void)),
                     (type = (qubit = void)), (type = (qubit = void)), (type = (qubit = void)),
                     (type = (qubit = void)), (type = (qubit = void)), (type = (qubit = void)),
-                    (type = (intArray = (bitwidth = 8, length = (static = 5)))), (type = (int = 1)), (type = (int = 32)),
-                    (type = (intArray = (bitwidth = 8, length = (static = 5)))), (type = (int = 1)), (type = (int = 32)),
-                    (type = (intArray = (bitwidth = 8, length = (static = 5)))), (type = (int = 1)), (type = (int = 32)),
-                    (type = (intArray = (bitwidth = 8, length = (static = 5)))), (type = (int = 1)), (type = (int = 32)),
-                    (type = (intArray = (bitwidth = 8, length = (static = 5)))), (type = (int = 1)), (type = (int = 32)),
-                    (type = (intArray = (bitwidth = 8, length = (static = 5)))), (type = (int = 32)), (type = (int = 8)),
-                    (type = (int = 8)), (type = (int = 32)), (type = (int = 8)),
-                    (type = (int = 8)), (type = (int = 8)), (type = (int = 32)),
-                    (type = (int = 8)), (type = (int = 8)), (type = (int = 8)),
-                    (type = (int = 32)), (type = (int = 8)), (type = (int = 8)),
-                    (type = (int = 8)), (type = (int = 32)), (type = (int = 8)),
-                    (type = (int = 8)), (type = (int = 8))
+                    (type = (intArray = (bitwidth = 1, length = (static = 5)))), (type = (int = 1)), (type = (int = 32)),
+                    (type = (intArray = (bitwidth = 1, length = (static = 5)))), (type = (int = 1)), (type = (int = 32)),
+                    (type = (intArray = (bitwidth = 1, length = (static = 5)))), (type = (int = 1)), (type = (int = 32)),
+                    (type = (intArray = (bitwidth = 1, length = (static = 5)))), (type = (int = 1)), (type = (int = 32)),
+                    (type = (intArray = (bitwidth = 1, length = (static = 5)))), (type = (int = 1)), (type = (int = 32)),
+                    (type = (intArray = (bitwidth = 1, length = (static = 5)))), (type = (int = 32)), (type = (int = 1)),
+                    (type = (int = 1)), (type = (int = 32)), (type = (int = 1)),
+                    (type = (int = 1)), (type = (int = 1)), (type = (int = 32)),
+                    (type = (int = 1)), (type = (int = 1)), (type = (int = 1)),
+                    (type = (int = 32)), (type = (int = 1)), (type = (int = 1)),
+                    (type = (int = 1)), (type = (int = 32)), (type = (int = 1)),
+                    (type = (int = 1)), (type = (int = 1))
                 ]
             ),
         ),
@@ -90,7 +90,7 @@
                     ]
                 ),
                 values = [
-                    (type = (int = 8))
+                    (type = (int = 1))
                 ]
             ),
         ),
@@ -118,7 +118,7 @@
                     operations = []
                 ),
                 values = [
-                    (type = (int = 8))
+                    (type = (int = 1))
                 ]
             ),
         ),
diff --git a/examples/entangled_qs/entangled_qs.jeff b/examples/entangled_qs/entangled_qs.jeff
index 8637ae6..a61adaa 100644
Binary files a/examples/entangled_qs/entangled_qs.jeff and b/examples/entangled_qs/entangled_qs.jeff differ
diff --git a/examples/entangled_qs/entangled_qs.txt b/examples/entangled_qs/entangled_qs.txt
index 8a47123..89bd86a 100644
--- a/examples/entangled_qs/entangled_qs.txt
+++ b/examples/entangled_qs/entangled_qs.txt
@@ -18,7 +18,7 @@
                         (inputs = [7, 2], outputs = [8, 9], instruction = (qubit = (gate = (custom = (name = 2, numQubits = 1), controlQubits = 1)))),
                         (inputs = [9, 3], outputs = [10, 11], instruction = (qubit = (gate = (custom = (name = 2, numQubits = 1), controlQubits = 1)))),
                         (inputs = [11, 4], outputs = [12, 13], instruction = (qubit = (gate = (custom = (name = 2, numQubits = 1), controlQubits = 1)))),
-                        (outputs = [14], instruction = (intArray = (const8 = [0, 0, 0, 0, 0]))),
+                        (outputs = [14], instruction = (intArray = (const1 = [false, false, false, false, false]))),
                         (inputs = [6], outputs = [15], instruction = (qubit = (measure = void))),
                         (outputs = [16], instruction = (int = (const32 = 0))),
                         (inputs = [14, 16, 15], outputs = [17], instruction = (intArray = (setIndex = void))),
@@ -41,12 +41,12 @@
                     (type = (qubit = void)), (type = (qubit = void)), (type = (qubit = void)),
                     (type = (qubit = void)), (type = (qubit = void)), (type = (qubit = void)),
                     (type = (qubit = void)), (type = (qubit = void)), (type = (qubit = void)),
-                    (type = (qubit = void)), (type = (qubit = void)), (type = (intArray = (bitwidth = 8, length = (static = 5)))),
-                    (type = (int = 1)), (type = (int = 32)), (type = (intArray = (bitwidth = 8, length = (static = 5)))),
-                    (type = (int = 1)), (type = (int = 32)), (type = (intArray = (bitwidth = 8, length = (static = 5)))),
-                    (type = (int = 1)), (type = (int = 32)), (type = (intArray = (bitwidth = 8, length = (static = 5)))),
-                    (type = (int = 1)), (type = (int = 32)), (type = (intArray = (bitwidth = 8, length = (static = 5)))),
-                    (type = (int = 1)), (type = (int = 32)), (type = (intArray = (bitwidth = 8, length = (static = 5))))
+                    (type = (qubit = void)), (type = (qubit = void)), (type = (intArray = (bitwidth = 1, length = (static = 5)))),
+                    (type = (int = 1)), (type = (int = 32)), (type = (intArray = (bitwidth = 1, length = (static = 5)))),
+                    (type = (int = 1)), (type = (int = 32)), (type = (intArray = (bitwidth = 1, length = (static = 5)))),
+                    (type = (int = 1)), (type = (int = 32)), (type = (intArray = (bitwidth = 1, length = (static = 5)))),
+                    (type = (int = 1)), (type = (int = 32)), (type = (intArray = (bitwidth = 1, length = (static = 5)))),
+                    (type = (int = 1)), (type = (int = 32)), (type = (intArray = (bitwidth = 1, length = (static = 5))))
                 ]
             ),
         )
diff --git a/impl/rs/src/reader.rs b/impl/rs/src/reader.rs
index a9a3870..32ced8f 100644
--- a/impl/rs/src/reader.rs
+++ b/impl/rs/src/reader.rs
@@ -12,11 +12,12 @@ pub mod value;
 
 pub mod optype;
 
-pub use function::{Function, FunctionId};
+pub use function::{Function, FunctionDeclaration, FunctionDefinition, FunctionId};
 pub use metadata::{HasMetadata, Metadata};
 pub use module::Module;
 pub use op::Operation;
 pub use region::Region;
+pub use value::{FunctionIOValue, ValueId, ValueTable, WireValue};
 
 use derive_more::derive::{Display, Error, From};
 
diff --git a/tools/verifier/Cargo.toml b/tools/verifier/Cargo.toml
new file mode 100644
index 0000000..86150b8
--- /dev/null
+++ b/tools/verifier/Cargo.toml
@@ -0,0 +1,14 @@
+[package]
+name = "verifier"
+version = "0.1.0"
+rust-version.workspace = true
+edition.workspace = true
+homepage.workspace = true
+repository.workspace = true
+license.workspace = true
+
+[dependencies]
+jeff = { package = "jeff-format", path = "../../impl/rs" }
+
+[lints]
+workspace = true
diff --git a/tools/verifier/src/analysis.rs b/tools/verifier/src/analysis.rs
new file mode 100644
index 0000000..1b0bae0
--- /dev/null
+++ b/tools/verifier/src/analysis.rs
@@ -0,0 +1,83 @@
+//! Information collection over jeff regions.
+//!
+//! This module traverses a function's dataflow graph to gather statistics
+//! used by the verification passes.
+
+use jeff::reader::optype::{ControlFlowOp, OpType};
+use jeff::reader::{ReadError, Region};
+
+/// Producer and consumer counts for a single value.
+#[derive(Debug, Default, Clone, PartialEq, Eq)]
+pub struct ValueStats {
+    /// Number of operations that produce this value.
+    pub producers: u32,
+    /// Number of operations that consume this value.
+    pub consumers: u32,
+}
+
+/// Walk `region` recursively and accumulate producer/consumer counts into `stats`.
+///
+/// The slice must be pre-allocated with one entry per value in the function's value table.
+pub fn collect_value_stats(region: Region<'_>, stats: &mut [ValueStats]) -> Result<(), ReadError> {
+    for value in region.sources() {
+        stats[value?.id() as usize].producers += 1;
+    }
+
+    for value in region.targets() {
+        stats[value?.id() as usize].consumers += 1;
+    }
+
+    for op in region.operations() {
+        for value in op.inputs() {
+            stats[value?.id() as usize].consumers += 1;
+        }
+
+        for value in op.outputs() {
+            stats[value?.id() as usize].producers += 1;
+        }
+
+        if let OpType::ControlFlowOp(cf_op) = op.op_type() {
+            collect_cf_value_stats(cf_op.as_ref(), stats)?;
+        }
+    }
+
+    Ok(())
+}
+
+fn collect_cf_value_stats(
+    cf_op: &ControlFlowOp<'_>,
+    stats: &mut [ValueStats],
+) -> Result<(), ReadError> {
+    match cf_op {
+        ControlFlowOp::For { region } => {
+            collect_value_stats(*region, stats)?;
+        }
+        ControlFlowOp::While { condition, body } => {
+            collect_value_stats(*condition, stats)?;
+            collect_value_stats(*body, stats)?;
+        }
+        ControlFlowOp::DoWhile { body, condition } => {
+            collect_value_stats(*body, stats)?;
+            collect_value_stats(*condition, stats)?;
+        }
+        ControlFlowOp::Switch(switch_op) => {
+            for branch in switch_op.branches() {
+                collect_value_stats(branch, stats)?;
+            }
+            if let Some(default) = switch_op.default_branch() {
+                collect_value_stats(default, stats)?;
+            }
+        }
+    }
+    Ok(())
+}
+
+/// Build a [`Vec<ValueStats>`] with one entry per value in the function's value table.
+pub fn build_value_stats(
+    region: Region<'_>,
+    num_values: usize,
+) -> Result<Vec<ValueStats>, ReadError> {
+    let mut stats = vec![ValueStats::default(); num_values];
+    collect_value_stats(region, &mut stats)?;
+    Ok(stats)
+}
diff --git a/tools/verifier/src/errors.rs b/tools/verifier/src/errors.rs
new file mode 100644
index 0000000..81799e6
--- /dev/null
+++ b/tools/verifier/src/errors.rs
@@ -0,0 +1,155 @@
+use std::fmt;
+
+/// An error detected during verification of a jeff module.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum VerificationError {
+    /// The module version is unset (0.0.0).
+    MissingVersion,
+
+    /// The module version is set but does not match the version supported by this verifier.
+    IncompatibleVersion,
+
+    /// The module's entrypoint does not refer to a function definition.
+    InvalidEntrypoint,
+
+    /// An operation references a value index that is out of bounds in the function's value table.
+    ValueOutOfBounds {
+        /// The out-of-bounds value index.
+        value_id: u32,
+        /// The number of values in the table.
+        value_count: usize,
+    },
+
+    /// An operation consumes a value before any operation that produces it.
+    UsedBeforeDefined {
+        /// The value used out of order.
+        value_id: u32,
+    },
+
+    /// A value is produced by more than one operation.
+    /// In jeff's SSA value semantics, every value must have exactly one producer.
+    ValueProducedMultipleTimes {
+        /// The value produced multiple times.
+        value_id: u32,
+        /// The number of producing operations.
+        producers: u32,
+    },
+
+    /// A linear value (qubit or qureg) is consumed by more than one operation.
+    LinearValueConsumedMultipleTimes {
+        /// The value consumed multiple times.
+        value_id: u32,
+        /// The number of consuming operations.
+        consumers: u32,
+    },
+
+    /// A linear value (qubit or qureg) is produced but never consumed.
+    LinearValueNeverConsumed {
+        /// The value that is never consumed.
+        value_id: u32,
+    },
+
+    /// The input and output types of an int or float operation are not all the same bitwidth or precision.
+    TypeMismatch {
+        /// The name of the operation with mismatched types.
+        operation: &'static str,
+    },
+
+    /// An input value has a type that is not valid for the operation.
+    InvalidInputType {
+        /// The name of the operation with the invalid input.
+        operation: &'static str,
+    },
+
+    /// An output value has a type that is not valid for the operation.
+    InvalidOutputType {
+        /// The name of the operation with the invalid output.
+        operation: &'static str,
+    },
+
+    /// An operation has the wrong number of inputs or outputs for its declared arity.
+    WrongArity {
+        /// The name of the operation with the wrong arity.
+        operation: &'static str,
+    },
+
+    /// An operation inside a nested region directly references a value from an outer scope
+    /// without the value being explicitly passed in via the region's sources.
+    IsolationViolation {
+        /// The outer-scope value referenced directly.
+        value_id: u32,
+    },
+}
+
+impl fmt::Display for VerificationError {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self {
+            Self::MissingVersion => {
+                write!(f, "module version is unset (0.0.0)")
+            }
+            Self::IncompatibleVersion => {
+                write!(f, "module version is incompatible with the jeff program")
+            }
+            Self::InvalidEntrypoint => {
+                write!(
+                    f,
+                    "module entrypoint does not refer to a function definition"
+                )
+            }
+            Self::ValueOutOfBounds {
+                value_id,
+                value_count,
+            } => {
+                write!(
+                    f,
+                    "value {value_id} is out of bounds (function has {value_count} values)"
+                )
+            }
+            Self::UsedBeforeDefined { value_id } => {
+                write!(f, "value {value_id} is used before it is defined")
+            }
+            Self::ValueProducedMultipleTimes {
+                value_id,
+                producers,
+            } => {
+                write!(
+                    f,
+                    "value {value_id} is produced {producers} times (must be exactly once)"
+                )
+            }
+            Self::LinearValueConsumedMultipleTimes {
+                value_id,
+                consumers,
+            } => {
+                write!(
+                    f,
+                    "linear value {value_id} is consumed {consumers} times (must be exactly once)"
+                )
+            }
+            Self::LinearValueNeverConsumed { value_id } => {
+                write!(f, "linear value {value_id} is produced but never consumed")
+            }
+            Self::TypeMismatch { operation } => {
+                write!(
+                    f,
+                    "'{operation}' has inputs and outputs with mismatched types"
+                )
+            }
+            Self::InvalidInputType { operation } => {
+                write!(f, "'{operation}' has an input of an unexpected type")
+            }
+            Self::InvalidOutputType { operation } => {
+                write!(f, "'{operation}' has an output of an unexpected type")
+            }
+            Self::WrongArity { operation } => {
+                write!(f, "'{operation}' has the wrong number of inputs or outputs for its declared arity")
+            }
+            Self::IsolationViolation { value_id } => {
+                write!(
+                    f,
+                    "value {value_id} from an outer scope is used inside a nested region without being passed in via sources"
+                )
+            }
+        }
+    }
+}
diff --git a/tools/verifier/src/lib.rs b/tools/verifier/src/lib.rs
new file mode 100644
index 0000000..0ccee8b
--- /dev/null
+++ b/tools/verifier/src/lib.rs
@@ -0,0 +1,54 @@
+//! Verifier for jeff quantum program modules.
+//!
+//! The main entry point is [`verify_module`], which checks a decoded
+//! [`jeff::reader::Module`] against all verification passes and returns
+//! a list of [`VerificationError`]s.
+
+pub mod analysis;
+/// Verification error types and their display messages.
+pub mod errors;
+pub mod passes;
+
+use jeff::reader::{Function, FunctionDefinition, Module};
+
+pub use errors::VerificationError;
+
+use passes::isolation::verify_isolation;
+use passes::module_attributes::verify_module_attributes;
+use passes::type_checks::verify_operation_types;
+use passes::value_checks::verify_value_checks;
+
+/// Verify a decoded jeff module and return all detected errors.
+///
+/// Returns an empty [`Vec`] if the module is valid.
+/// Returns immediately with a single error if the module version is missing or incompatible,
+/// since subsequent passes would produce meaningless results against an unknown schema version.
+pub fn verify_module(module: Module<'_>) -> Vec<VerificationError> {
+    let v = module.version();
+    let s = &jeff::SCHEMA_VERSION;
+
+    if v.major == 0 && v.minor == 0 && v.patch == 0 {
+        return vec![VerificationError::MissingVersion];
+    }
+    if v.major != s.major || v.minor != s.minor || v.patch != s.patch {
+        return vec![VerificationError::IncompatibleVersion];
+    }
+
+    let mut errors = Vec::new();
+
+    verify_module_attributes(module, &mut errors);
+
+    for function in module.functions() {
+        if let Function::Definition(def) = function {
+            verify_definition(def, &mut errors);
+        }
+    }
+
+    errors
+}
+
+fn verify_definition(def: FunctionDefinition<'_>, errors: &mut Vec<VerificationError>) {
+    verify_value_checks(def, errors);
+    verify_operation_types(def.body(), errors);
+    verify_isolation(def, errors);
+}
diff --git a/tools/verifier/src/passes/isolation.rs b/tools/verifier/src/passes/isolation.rs
new file mode 100644
index 0000000..8c77ac9
--- /dev/null
+++ b/tools/verifier/src/passes/isolation.rs
@@ -0,0 +1,84 @@
+//! Checks that nested regions are isolated from outer scopes (IsolatedFromAbove).
+
+use std::collections::HashSet;
+
+use jeff::reader::optype::{ControlFlowOp, OpType};
+use jeff::reader::{FunctionDefinition, Region, ValueId};
+
+use crate::VerificationError;
+
+/// Check that no operation inside a nested region directly references a value from an outer scope.
+pub fn verify_isolation(def: FunctionDefinition<'_>, errors: &mut Vec<VerificationError>) {
+    check_region_isolation(def.body(), &HashSet::new(), errors);
+}
+
+fn check_region_isolation(
+    region: Region<'_>,
+    outer_values: &HashSet<ValueId>,
+    errors: &mut Vec<VerificationError>,
+) {
+    let mut locally_defined: HashSet<ValueId> = region
+        .sources()
+        .filter_map(|r| r.ok())
+        .map(|v| v.id())
+        .collect();
+
+    for op in region.operations() {
+        for input in op.inputs().filter_map(|r| r.ok()) {
+            if outer_values.contains(&input.id()) {
+                errors.push(VerificationError::IsolationViolation {
+                    value_id: input.id(),
+                });
+            }
+        }
+
+        for output in op.outputs().filter_map(|r| r.ok()) {
+            locally_defined.insert(output.id());
+        }
+
+        if let OpType::ControlFlowOp(cf_op) = op.op_type() {
+            let new_outer: HashSet<ValueId> = outer_values
+                .iter()
+                .chain(locally_defined.iter())
+                .cloned()
+                .collect();
+            check_cf_isolation(cf_op.as_ref(), &new_outer, errors);
+        }
+    }
+
+    for target in region.targets().filter_map(|r| r.ok()) {
+        if outer_values.contains(&target.id()) {
+            errors.push(VerificationError::IsolationViolation {
+                value_id: target.id(),
+            });
+        }
+    }
+}
+
+fn check_cf_isolation(
+    cf_op: &ControlFlowOp<'_>,
+    outer_values: &HashSet<ValueId>,
+    errors: &mut Vec<VerificationError>,
+) {
+    match cf_op {
+        ControlFlowOp::For { region } => {
+            check_region_isolation(*region, outer_values, errors);
+        }
+        ControlFlowOp::While { condition, body } => {
+            check_region_isolation(*condition, outer_values, errors);
+            check_region_isolation(*body, outer_values, errors);
+        }
+        ControlFlowOp::DoWhile { body, condition } => {
+            check_region_isolation(*body, outer_values, errors);
+            check_region_isolation(*condition, outer_values, errors);
+        }
+        ControlFlowOp::Switch(switch_op) => {
+            for branch in switch_op.branches() {
+                check_region_isolation(branch, outer_values, errors);
+            }
+            if let Some(default) = switch_op.default_branch() {
+                check_region_isolation(default, outer_values, errors);
+            }
+        }
+    }
+}
diff --git a/tools/verifier/src/passes/mod.rs b/tools/verifier/src/passes/mod.rs
new file mode 100644
index 0000000..f658f9c
--- /dev/null
+++ b/tools/verifier/src/passes/mod.rs
@@ -0,0 +1,6 @@
+//! Verification passes, one per category of check.
+
+pub mod isolation;
+pub mod module_attributes;
+pub mod type_checks;
+pub mod value_checks;
diff --git a/tools/verifier/src/passes/module_attributes.rs b/tools/verifier/src/passes/module_attributes.rs
new file mode 100644
index 0000000..a080e16
--- /dev/null
+++ b/tools/verifier/src/passes/module_attributes.rs
@@ -0,0 +1,15 @@
+//! Checks for required module-level attributes.
+
+use jeff::reader::{Function, Module};
+
+use crate::VerificationError;
+
+/// Verify that the module has a valid entrypoint.
+pub fn verify_module_attributes(module: Module<'_>, errors: &mut Vec<VerificationError>) {
+    match module.try_function(module.entrypoint_id()) {
+        None | Some(Function::Declaration(_)) => {
+            errors.push(VerificationError::InvalidEntrypoint);
+        }
+        Some(Function::Definition(_)) => {}
+    }
+}
diff --git a/tools/verifier/src/passes/type_checks.rs b/tools/verifier/src/passes/type_checks.rs
new file mode 100644
index 0000000..38a83c0
--- /dev/null
+++ b/tools/verifier/src/passes/type_checks.rs
@@ -0,0 +1,741 @@
+//! Checks for correct input/output types and bitwidth/precision uniformity.
+
+use jeff::reader::optype::{
+    ControlFlowOp, FloatArrayOp, FloatOp, IntArrayOp, IntOp, OpType, QubitOp, QubitRegisterOp,
+};
+use jeff::reader::Region;
+use jeff::types::{FloatPrecision, Type};
+
+use crate::VerificationError;
+
+/// Check that all operations in `region` (and its nested regions) have correctly typed inputs and outputs.
+pub fn verify_operation_types(region: Region<'_>, errors: &mut Vec<VerificationError>) {
+    check_region_types(region, errors);
+}
+
+fn check_region_types(region: Region<'_>, errors: &mut Vec<VerificationError>) {
+    for op in region.operations() {
+        let inputs: Vec<Type> = op.inputs().filter_map(|r| r.ok()).map(|v| v.ty()).collect();
+        let outputs: Vec<Type> = op
+            .outputs()
+            .filter_map(|r| r.ok())
+            .map(|v| v.ty())
+            .collect();
+        match op.op_type() {
+            OpType::IntOp(int_op) => check_int_op(int_op, &inputs, &outputs, errors),
+            OpType::FloatOp(float_op) => check_float_op(float_op, &inputs, &outputs, errors),
+            OpType::QubitOp(qubit_op) => check_qubit_op(qubit_op, &inputs, &outputs, errors),
+            OpType::QubitRegisterOp(qureg_op) => {
+                check_qureg_op(qureg_op, &inputs, &outputs, errors);
+            }
+            OpType::ControlFlowOp(cf_op) => check_cf_region_types(cf_op.as_ref(), errors),
+            OpType::IntArrayOp(int_array_op) => {
+                check_int_array_op(int_array_op, &inputs, &outputs, errors);
+            }
+            OpType::FloatArrayOp(float_array_op) => {
+                check_float_array_op(float_array_op, &inputs, &outputs, errors);
+            }
+            // FuncOp only has a function index so type checking calls require to find the
+            // callee signature at Module level, but this pass is only scoped to a Region.
+            // TODO: Scope Module into this pass / add a helper pass to build a
+            // function table for a signature lookup and check out of bounds index
+            OpType::FuncOp(_) => {}
+            _ => panic!("Unknown optype"),
+        }
+    }
+}
+
+fn check_cf_region_types(cf_op: &ControlFlowOp<'_>, errors: &mut Vec<VerificationError>) {
+    // TODO: Verify that SCF node input/output types.
+    match cf_op {
+        ControlFlowOp::For { region } => check_region_types(*region, errors),
+        ControlFlowOp::While { condition, body } => {
+            check_region_types(*condition, errors);
+            check_region_types(*body, errors);
+        }
+        ControlFlowOp::DoWhile { body, condition } => {
+            check_region_types(*body, errors);
+            check_region_types(*condition, errors);
+        }
+        ControlFlowOp::Switch(switch_op) => {
+            for branch in switch_op.branches() {
+                check_region_types(branch, errors);
+            }
+            if let Some(default) = switch_op.default_branch() {
+                check_region_types(default, errors);
+            }
+        }
+    }
+}
+
+fn is_int(ty: &Type, bits: impl Into<Option<u8>>) -> bool {
+    match bits.into() {
+        Some(b) => matches!(ty, Type::Int { bits: x } if *x == b),
+        None => matches!(ty, Type::Int { .. }),
+    }
+}
+
+fn is_float(ty: &Type, precision: impl Into<Option<FloatPrecision>>) -> bool {
+    match precision.into() {
+        Some(p) => matches!(ty, Type::Float { precision: x } if *x == p),
+        None => matches!(ty, Type::Float { .. }),
+    }
+}
+
+fn is_qubit(ty: &Type) -> bool {
+    matches!(ty, Type::Qubit)
+}
+
+fn is_qureg(ty: &Type) -> bool {
+    matches!(ty, Type::QubitRegister { .. })
+}
+
+fn is_int_array(ty: &Type) -> bool {
+    matches!(ty, Type::IntArray { .. })
+}
+
+fn is_float_array(ty: &Type) -> bool {
+    matches!(ty, Type::FloatArray { .. })
+}
+
+fn expect_input(
+    inputs: &[Type],
+    idx: usize,
+    pred: impl Fn(&Type) -> bool,
+    op: &'static str,
+    errors: &mut Vec<VerificationError>,
+) {
+    if inputs.get(idx).is_some_and(|ty| !pred(ty)) {
+        errors.push(VerificationError::InvalidInputType { operation: op });
+    }
+}
+
+fn expect_output(
+    outputs: &[Type],
+    idx: usize,
+    pred: impl Fn(&Type) -> bool,
+    op: &'static str,
+    errors: &mut Vec<VerificationError>,
+) {
+    if outputs.get(idx).is_some_and(|ty| !pred(ty)) {
+        errors.push(VerificationError::InvalidOutputType { operation: op });
+    }
+}
+
+fn check_arity(
+    inputs: &[Type],
+    expected_inputs: usize,
+    outputs: &[Type],
+    expected_outputs: usize,
+    op: &'static str,
+    errors: &mut Vec<VerificationError>,
+) {
+    if inputs.len() != expected_inputs || outputs.len() != expected_outputs {
+        errors.push(VerificationError::WrongArity { operation: op });
+    }
+}
+
+fn check_uniform_int(
+    inputs: &[Type],
+    outputs: &[Type],
+    name: &'static str,
+    errors: &mut Vec<VerificationError>,
+) {
+    for ty in inputs {
+        if !is_int(ty, None) {
+            errors.push(VerificationError::InvalidInputType { operation: name });
+            return;
+        }
+    }
+    for ty in outputs {
+        if !is_int(ty, None) {
+            errors.push(VerificationError::InvalidOutputType { operation: name });
+            return;
+        }
+    }
+    let mut bits: Option<u8> = None;
+    for ty in inputs.iter().chain(outputs.iter()) {
+        if let Type::Int { bits: b } = ty {
+            match bits {
+                None => bits = Some(*b),
+                Some(existing) if existing != *b => {
+                    errors.push(VerificationError::TypeMismatch { operation: name });
+                    return;
+                }
+                _ => {}
+            }
+        }
+    }
+}
+
+fn check_uniform_float(
+    inputs: &[Type],
+    outputs: &[Type],
+    name: &'static str,
+    errors: &mut Vec<VerificationError>,
+) {
+    for ty in inputs {
+        if !is_float(ty, None) {
+            errors.push(VerificationError::InvalidInputType { operation: name });
+            return;
+        }
+    }
+    for ty in outputs {
+        if !is_float(ty, None) {
+            errors.push(VerificationError::InvalidOutputType { operation: name });
+            return;
+        }
+    }
+    let mut precision: Option<FloatPrecision> = None;
+    for ty in inputs.iter().chain(outputs.iter()) {
+        if let Type::Float { precision: p } = ty {
+            match precision {
+                None => precision = Some(*p),
+                Some(existing) if existing != *p => {
+                    errors.push(VerificationError::TypeMismatch { operation: name });
+                    return;
+                }
+                _ => {}
+            }
+        }
+    }
+}
+
+fn check_int_op(
+    int_op: IntOp,
+    inputs: &[Type],
+    outputs: &[Type],
+    errors: &mut Vec<VerificationError>,
+) {
+    match int_op {
+        IntOp::Const1(_) => {
+            check_arity(inputs, 0, outputs, 1, "int const", errors);
+            expect_output(outputs, 0, |ty| is_int(ty, 1), "int const", errors);
+        }
+        IntOp::Const8(_) => {
+            check_arity(inputs, 0, outputs, 1, "int const", errors);
+            expect_output(outputs, 0, |ty| is_int(ty, 8), "int const", errors);
+        }
+        IntOp::Const16(_) => {
+            check_arity(inputs, 0, outputs, 1, "int const", errors);
+            expect_output(outputs, 0, |ty| is_int(ty, 16), "int const", errors);
+        }
+        IntOp::Const32(_) => {
+            check_arity(inputs, 0, outputs, 1, "int const", errors);
+            expect_output(outputs, 0, |ty| is_int(ty, 32), "int const", errors);
+        }
+        IntOp::Const64(_) => {
+            check_arity(inputs, 0, outputs, 1, "int const", errors);
+            expect_output(outputs, 0, |ty| is_int(ty, 64), "int const", errors);
+        }
+        IntOp::Add
+        | IntOp::Sub
+        | IntOp::Mul
+        | IntOp::DivS
+        | IntOp::DivU
+        | IntOp::Pow
+        | IntOp::And
+        | IntOp::Or
+        | IntOp::Xor
+        | IntOp::MinS
+        | IntOp::MinU
+        | IntOp::MaxS
+        | IntOp::MaxU
+        | IntOp::RemS
+        | IntOp::RemU
+        | IntOp::Shl
+        | IntOp::Shr => {
+            check_arity(inputs, 2, outputs, 1, "int arithmetic", errors);
+            check_uniform_int(inputs, outputs, "int arithmetic", errors);
+        }
+        IntOp::Not | IntOp::Abs => {
+            check_arity(inputs, 1, outputs, 1, "int arithmetic", errors);
+            check_uniform_int(inputs, outputs, "int arithmetic", errors);
+        }
+        IntOp::Eq | IntOp::LtS | IntOp::LteS | IntOp::LtU | IntOp::LteU => {
+            check_arity(inputs, 2, outputs, 1, "int comparison", errors);
+            check_uniform_int(inputs, &[], "int comparison", errors);
+            expect_output(outputs, 0, |ty| is_int(ty, 1), "int comparison", errors);
+        }
+        _ => {}
+    }
+}
+
+fn check_float_op(
+    float_op: FloatOp,
+    inputs: &[Type],
+    outputs: &[Type],
+    errors: &mut Vec<VerificationError>,
+) {
+    match float_op {
+        FloatOp::Const32(_) => {
+            check_arity(inputs, 0, outputs, 1, "float const", errors);
+            expect_output(
+                outputs,
+                0,
+                |ty| is_float(ty, FloatPrecision::Float32),
+                "float const",
+                errors,
+            );
+        }
+        FloatOp::Const64(_) => {
+            check_arity(inputs, 0, outputs, 1, "float const", errors);
+            expect_output(
+                outputs,
+                0,
+                |ty| is_float(ty, FloatPrecision::Float64),
+                "float const",
+                errors,
+            );
+        }
+        FloatOp::Add
+        | FloatOp::Sub
+        | FloatOp::Mul
+        | FloatOp::Pow
+        | FloatOp::Atan2
+        | FloatOp::Max
+        | FloatOp::Min => {
+            check_arity(inputs, 2, outputs, 1, "float op", errors);
+            check_uniform_float(inputs, outputs, "float op", errors);
+        }
+        FloatOp::Sqrt
+        | FloatOp::Abs
+        | FloatOp::Ceil
+        | FloatOp::Floor
+        | FloatOp::Exp
+        | FloatOp::Log
+        | FloatOp::Sin
+        | FloatOp::Cos
+        | FloatOp::Tan
+        | FloatOp::Asin
+        | FloatOp::Acos
+        | FloatOp::Atan
+        | FloatOp::Sinh
+        | FloatOp::Cosh
+        | FloatOp::Tanh
+        | FloatOp::Asinh
+        | FloatOp::Acosh
+        | FloatOp::Atanh => {
+            check_arity(inputs, 1, outputs, 1, "float op", errors);
+            check_uniform_float(inputs, outputs, "float op", errors);
+        }
+        FloatOp::Eq | FloatOp::Lt | FloatOp::Lte => {
+            check_arity(inputs, 2, outputs, 1, "float predicate", errors);
+            check_uniform_float(inputs, &[], "float predicate", errors);
+            expect_output(outputs, 0, |ty| is_int(ty, 1), "float predicate", errors);
+        }
+        FloatOp::IsNan | FloatOp::IsInf => {
+            check_arity(inputs, 1, outputs, 1, "float predicate", errors);
+            check_uniform_float(inputs, &[], "float predicate", errors);
+            expect_output(outputs, 0, |ty| is_int(ty, 1), "float predicate", errors);
+        }
+        _ => {}
+    }
+}
+
+fn check_qubit_op(
+    qubit_op: QubitOp<'_>,
+    inputs: &[Type],
+    outputs: &[Type],
+    errors: &mut Vec<VerificationError>,
+) {
+    match qubit_op {
+        QubitOp::Alloc => {
+            check_arity(inputs, 0, outputs, 1, "Alloc", errors);
+            expect_output(outputs, 0, is_qubit, "Alloc", errors);
+        }
+        QubitOp::Free | QubitOp::FreeZero => {
+            check_arity(inputs, 1, outputs, 0, "qubit free", errors);
+            expect_input(inputs, 0, is_qubit, "qubit free", errors);
+        }
+        QubitOp::Reset => {
+            check_arity(inputs, 1, outputs, 1, "Reset", errors);
+            expect_input(inputs, 0, is_qubit, "Reset", errors);
+            expect_output(outputs, 0, is_qubit, "Reset", errors);
+        }
+        QubitOp::Measure => {
+            check_arity(inputs, 1, outputs, 1, "Measure", errors);
+            expect_input(inputs, 0, is_qubit, "Measure", errors);
+            expect_output(outputs, 0, |ty| is_int(ty, 1), "Measure", errors);
+        }
+        QubitOp::MeasureNd => {
+            check_arity(inputs, 1, outputs, 2, "MeasureNd", errors);
+            expect_input(inputs, 0, is_qubit, "MeasureNd", errors);
+            expect_output(outputs, 0, is_qubit, "MeasureNd", errors);
+            expect_output(outputs, 1, |ty| is_int(ty, 1), "MeasureNd", errors);
+        }
+        QubitOp::Gate(gate) => {
+            let num_qubits = gate.num_qubits();
+            let num_params = gate.num_params();
+            if inputs.len() != num_qubits + num_params {
+                errors.push(VerificationError::WrongArity { operation: "Gate" });
+            }
+            if outputs.len() != num_qubits {
+                errors.push(VerificationError::WrongArity { operation: "Gate" });
+            }
+            for (i, ty) in inputs.iter().enumerate() {
+                if i < num_qubits {
+                    if !is_qubit(ty) {
+                        errors.push(VerificationError::InvalidInputType { operation: "Gate" });
+                    }
+                } else if i < num_qubits + num_params && !is_float(ty, None) {
+                    errors.push(VerificationError::InvalidInputType { operation: "Gate" });
+                }
+            }
+            for ty in outputs.iter().take(num_qubits) {
+                if !is_qubit(ty) {
+                    errors.push(VerificationError::InvalidOutputType { operation: "Gate" });
+                }
+            }
+        }
+        _ => {}
+    }
+}
+
+fn check_qureg_op(
+    qureg_op: QubitRegisterOp,
+    inputs: &[Type],
+    outputs: &[Type],
+    errors: &mut Vec<VerificationError>,
+) {
+    match qureg_op {
+        QubitRegisterOp::Alloc => {
+            check_arity(inputs, 1, outputs, 1, "qureg alloc", errors);
+            expect_input(inputs, 0, |ty| is_int(ty, 32), "qureg alloc", errors);
+            expect_output(outputs, 0, is_qureg, "qureg alloc", errors);
+        }
+        QubitRegisterOp::Free | QubitRegisterOp::FreeZero => {
+            check_arity(inputs, 1, outputs, 0, "qureg free", errors);
+            expect_input(inputs, 0, is_qureg, "qureg free", errors);
+        }
+        QubitRegisterOp::ExtractIndex => {
+            check_arity(inputs, 2, outputs, 2, "qureg extractIndex", errors);
+            expect_input(inputs, 0, is_qureg, "qureg extractIndex", errors);
+            expect_input(inputs, 1, |ty| is_int(ty, 32), "qureg extractIndex", errors);
+            expect_output(outputs, 0, is_qureg, "qureg extractIndex", errors);
+            expect_output(outputs, 1, is_qubit, "qureg extractIndex", errors);
+        }
+        QubitRegisterOp::InsertIndex => {
+            check_arity(inputs, 3, outputs, 1, "qureg insertIndex", errors);
+            expect_input(inputs, 0, is_qureg, "qureg insertIndex", errors);
+            expect_input(inputs, 1, |ty| is_int(ty, 32), "qureg insertIndex", errors);
+            expect_input(inputs, 2, is_qubit, "qureg insertIndex", errors);
+            expect_output(outputs, 0, is_qureg, "qureg insertIndex", errors);
+        }
+        QubitRegisterOp::ExtractSlice => {
+            check_arity(inputs, 3, outputs, 2, "qureg extractSlice", errors);
+            expect_input(inputs, 0, is_qureg, "qureg extractSlice", errors);
+            expect_input(inputs, 1, |ty| is_int(ty, 32), "qureg extractSlice", errors);
+            expect_input(inputs, 2, |ty| is_int(ty, 32), "qureg extractSlice", errors);
+            expect_output(outputs, 0, is_qureg, "qureg extractSlice", errors);
+            expect_output(outputs, 1, is_qureg, "qureg extractSlice", errors);
+        }
+        QubitRegisterOp::InsertSlice => {
+            check_arity(inputs, 3, outputs, 1, "qureg insertSlice", errors);
+            expect_input(inputs, 0, is_qureg, "qureg insertSlice", errors);
+            expect_input(inputs, 1, |ty| is_int(ty, 32), "qureg insertSlice", errors);
+            expect_input(inputs, 2, is_qureg, "qureg insertSlice", errors);
+            expect_output(outputs, 0, is_qureg, "qureg insertSlice", errors);
+        }
+        QubitRegisterOp::Length => {
+            check_arity(inputs, 1, outputs, 2, "qureg length", errors);
+            expect_input(inputs, 0, is_qureg, "qureg length", errors);
+            expect_output(outputs, 0, is_qureg, "qureg length", errors);
+            expect_output(outputs, 1, |ty| is_int(ty, 32), "qureg length", errors);
+        }
+        QubitRegisterOp::Split => {
+            check_arity(inputs, 2, outputs, 2, "qureg split", errors);
+            expect_input(inputs, 0, is_qureg, "qureg split", errors);
+            expect_input(inputs, 1, |ty| is_int(ty, 32), "qureg split", errors);
+            expect_output(outputs, 0, is_qureg, "qureg split", errors);
+            expect_output(outputs, 1, is_qureg, "qureg split", errors);
+        }
+        QubitRegisterOp::Join => {
+            check_arity(inputs, 2, outputs, 1, "qureg join", errors);
+            expect_input(inputs, 0, is_qureg, "qureg join", errors);
+            expect_input(inputs, 1, is_qureg, "qureg join", errors);
+            expect_output(outputs, 0, is_qureg, "qureg join", errors);
+        }
+        QubitRegisterOp::Create => {
+            if outputs.len() != 1 {
+                errors.push(VerificationError::WrongArity {
+                    operation: "qureg create",
+                });
+            }
+            for ty in inputs.iter() {
+                if !is_qubit(ty) {
+                    errors.push(VerificationError::InvalidInputType {
+                        operation: "qureg create",
+                    });
+                }
+            }
+            expect_output(outputs, 0, is_qureg, "qureg create", errors);
+        }
+        _ => {}
+    }
+}
+
+fn check_int_array_op(
+    int_array_op: IntArrayOp<'_>,
+    inputs: &[Type],
+    outputs: &[Type],
+    errors: &mut Vec<VerificationError>,
+) {
+    match int_array_op {
+        IntArrayOp::ConstArray1(_) => {
+            check_arity(inputs, 0, outputs, 1, "int array const", errors);
+            expect_output(
+                outputs,
+                0,
+                |ty| matches!(ty, Type::IntArray { bits: 1, .. }),
+                "int array const",
+                errors,
+            );
+        }
+        IntArrayOp::ConstArray8(_) => {
+            check_arity(inputs, 0, outputs, 1, "int array const", errors);
+            expect_output(
+                outputs,
+                0,
+                |ty| matches!(ty, Type::IntArray { bits: 8, .. }),
+                "int array const",
+                errors,
+            );
+        }
+        IntArrayOp::ConstArray16(_) => {
+            check_arity(inputs, 0, outputs, 1, "int array const", errors);
+            expect_output(
+                outputs,
+                0,
+                |ty| matches!(ty, Type::IntArray { bits: 16, .. }),
+                "int array const",
+                errors,
+            );
+        }
+        IntArrayOp::ConstArray32(_) => {
+            check_arity(inputs, 0, outputs, 1, "int array const", errors);
+            expect_output(
+                outputs,
+                0,
+                |ty| matches!(ty, Type::IntArray { bits: 32, .. }),
+                "int array const",
+                errors,
+            );
+        }
+        IntArrayOp::ConstArray64(_) => {
+            check_arity(inputs, 0, outputs, 1, "int array const", errors);
+            expect_output(
+                outputs,
+                0,
+                |ty| matches!(ty, Type::IntArray { bits: 64, .. }),
+                "int array const",
+                errors,
+            );
+        }
+        IntArrayOp::Zero { bits } => {
+            check_arity(inputs, 1, outputs, 1, "int array zero", errors);
+            expect_input(inputs, 0, |ty| is_int(ty, 32), "int array zero", errors);
+            expect_output(
+                outputs,
+                0,
+                |ty| matches!(ty, Type::IntArray { bits: b, .. } if *b == bits),
+                "int array zero",
+                errors,
+            );
+        }
+        IntArrayOp::GetIndex => {
+            check_arity(inputs, 2, outputs, 1, "int array getIndex", errors);
+            expect_input(inputs, 0, is_int_array, "int array getIndex", errors);
+            expect_input(inputs, 1, |ty| is_int(ty, 32), "int array getIndex", errors);
+            if let (Some(Type::IntArray { bits, .. }), Some(out_ty)) =
+                (inputs.first(), outputs.first())
+            {
+                if !is_int(out_ty, *bits) {
+                    errors.push(VerificationError::TypeMismatch {
+                        operation: "int array getIndex",
+                    });
+                }
+            }
+        }
+        IntArrayOp::SetIndex => {
+            check_arity(inputs, 3, outputs, 1, "int array setIndex", errors);
+            expect_input(inputs, 0, is_int_array, "int array setIndex", errors);
+            expect_input(inputs, 1, |ty| is_int(ty, 32), "int array setIndex", errors);
+            if let Some(Type::IntArray { bits, .. }) = inputs.first() {
+                let bits = *bits;
+                if inputs.get(2).is_some_and(|ty| !is_int(ty, bits)) {
+                    errors.push(VerificationError::TypeMismatch {
+                        operation: "int array setIndex",
+                    });
+                }
+                if outputs
+                    .first()
+                    .is_some_and(|ty| !matches!(ty, Type::IntArray { bits: b, .. } if *b == bits))
+                {
+                    errors.push(VerificationError::TypeMismatch {
+                        operation: "int array setIndex",
+                    });
+                }
+            }
+        }
+        IntArrayOp::Length => {
+            check_arity(inputs, 1, outputs, 1, "int array length", errors);
+            expect_input(inputs, 0, is_int_array, "int array length", errors);
+            expect_output(outputs, 0, |ty| is_int(ty, 32), "int array length", errors);
+        }
+        IntArrayOp::Create => {
+            if outputs.len() != 1 {
+                errors.push(VerificationError::WrongArity {
+                    operation: "int array create",
+                });
+            }
+            expect_output(outputs, 0, is_int_array, "int array create", errors);
+            if let Some(Type::IntArray { bits, .. }) = outputs.first() {
+                let bits = *bits;
+                for ty in inputs.iter() {
+                    if !is_int(ty, bits) {
+                        errors.push(VerificationError::TypeMismatch {
+                            operation: "int array create",
+                        });
+                        break;
+                    }
+                }
+            }
+        }
+        _ => {}
+    }
+}
+
+fn check_float_array_op(
+    float_array_op: FloatArrayOp<'_>,
+    inputs: &[Type],
+    outputs: &[Type],
+    errors: &mut Vec<VerificationError>,
+) {
+    match float_array_op {
+        FloatArrayOp::Const32(_) => {
+            check_arity(inputs, 0, outputs, 1, "float array const", errors);
+            expect_output(
+                outputs,
+                0,
+                |ty| {
+                    matches!(
+                        ty,
+                        Type::FloatArray {
+                            precision: FloatPrecision::Float32,
+                            ..
+                        }
+                    )
+                },
+                "float array const",
+                errors,
+            );
+        }
+        FloatArrayOp::Const64(_) => {
+            check_arity(inputs, 0, outputs, 1, "float array const", errors);
+            expect_output(
+                outputs,
+                0,
+                |ty| {
+                    matches!(
+                        ty,
+                        Type::FloatArray {
+                            precision: FloatPrecision::Float64,
+                            ..
+                        }
+                    )
+                },
+                "float array const",
+                errors,
+            );
+        }
+        FloatArrayOp::Zero { precision } => {
+            check_arity(inputs, 1, outputs, 1, "float array zero", errors);
+            expect_input(inputs, 0, |ty| is_int(ty, 32), "float array zero", errors);
+            expect_output(
+                outputs,
+                0,
+                |ty| matches!(ty, Type::FloatArray { precision: p, .. } if *p == precision),
+                "float array zero",
+                errors,
+            );
+        }
+        FloatArrayOp::GetIndex => {
+            check_arity(inputs, 2, outputs, 1, "float array getIndex", errors);
+            expect_input(inputs, 0, is_float_array, "float array getIndex", errors);
+            expect_input(
+                inputs,
+                1,
+                |ty| is_int(ty, 32),
+                "float array getIndex",
+                errors,
+            );
+            if let (Some(Type::FloatArray { precision, .. }), Some(out_ty)) =
+                (inputs.first(), outputs.first())
+            {
+                if !is_float(out_ty, *precision) {
+                    errors.push(VerificationError::TypeMismatch {
+                        operation: "float array getIndex",
+                    });
+                }
+            }
+        }
+        FloatArrayOp::SetIndex => {
+            check_arity(inputs, 3, outputs, 1, "float array setIndex", errors);
+            expect_input(inputs, 0, is_float_array, "float array setIndex", errors);
+            expect_input(
+                inputs,
+                1,
+                |ty| is_int(ty, 32),
+                "float array setIndex",
+                errors,
+            );
+            if let Some(Type::FloatArray { precision, .. }) = inputs.first() {
+                let precision = *precision;
+                if inputs.get(2).is_some_and(|ty| !is_float(ty, precision)) {
+                    errors.push(VerificationError::TypeMismatch {
+                        operation: "float array setIndex",
+                    });
+                }
+                if outputs.first().is_some_and(
+                    |ty| !matches!(ty, Type::FloatArray { precision: p, .. } if *p == precision),
+                ) {
+                    errors.push(VerificationError::TypeMismatch {
+                        operation: "float array setIndex",
+                    });
+                }
+            }
+        }
+        FloatArrayOp::Length => {
+            check_arity(inputs, 1, outputs, 1, "float array length", errors);
+            expect_input(inputs, 0, is_float_array, "float array length", errors);
+            expect_output(
+                outputs,
+                0,
+                |ty| is_int(ty, 32),
+                "float array length",
+                errors,
+            );
+        }
+        FloatArrayOp::Create => {
+            if outputs.len() != 1 {
+                errors.push(VerificationError::WrongArity {
+                    operation: "float array create",
+                });
+            }
+            expect_output(outputs, 0, is_float_array, "float array create", errors);
+            if let Some(Type::FloatArray { precision, .. }) = outputs.first() {
+                let precision = *precision;
+                for ty in inputs.iter() {
+                    if !is_float(ty, precision) {
+                        errors.push(VerificationError::TypeMismatch {
+                            operation: "float array create",
+                        });
+                        break;
+                    }
+                }
+            }
+        }
+        _ => {}
+    }
+}
diff --git a/tools/verifier/src/passes/value_checks.rs b/tools/verifier/src/passes/value_checks.rs
new file mode 100644
index 0000000..f5fa36d
--- /dev/null
+++ b/tools/verifier/src/passes/value_checks.rs
@@ -0,0 +1,135 @@
+//! Checks for value ordering, bounds, and linearity constraints.
+
+use std::collections::HashSet;
+
+use jeff::reader::optype::{ControlFlowOp, OpType};
+use jeff::reader::{FunctionDefinition, ReadError, Region, ValueId};
+use jeff::types::Type;
+
+use crate::analysis::build_value_stats;
+use crate::VerificationError;
+
+/// Check value ordering, out-of-bounds references, and linearity for a function definition.
+pub fn verify_value_checks(def: FunctionDefinition<'_>, errors: &mut Vec<VerificationError>) {
+    let values = def.values();
+    let num_values = values.len();
+
+    check_region_ordering(def.body(), &HashSet::new(), errors);
+
+    match build_value_stats(def.body(), num_values) {
+        Ok(stats) => {
+            for (id, value) in values.iter() {
+                let stat = &stats[id as usize];
+                if stat.producers > 1 {
+                    errors.push(VerificationError::ValueProducedMultipleTimes {
+                        value_id: id,
+                        producers: stat.producers,
+                    });
+                }
+                if is_linear(value.ty()) {
+                    if stat.consumers > 1 {
+                        errors.push(VerificationError::LinearValueConsumedMultipleTimes {
+                            value_id: id,
+                            consumers: stat.consumers,
+                        });
+                    }
+                    if stat.consumers == 0 && stat.producers > 0 {
+                        errors.push(VerificationError::LinearValueNeverConsumed { value_id: id });
+                    }
+                }
+            }
+        }
+        Err(e) => push_oob(e, errors),
+    }
+}
+
+fn is_linear(ty: Type) -> bool {
+    matches!(ty, Type::Qubit | Type::QubitRegister { .. })
+}
+
+fn push_oob(e: ReadError, errors: &mut Vec<VerificationError>) {
+    if let ReadError::ValueOutOfBounds { idx, count } = e {
+        errors.push(VerificationError::ValueOutOfBounds {
+            value_id: idx,
+            value_count: count,
+        });
+    }
+}
+
+fn check_region_ordering(
+    region: Region<'_>,
+    outer_defined: &HashSet<ValueId>,
+    errors: &mut Vec<VerificationError>,
+) {
+    let mut defined: HashSet<ValueId> = outer_defined.clone();
+
+    for result in region.sources() {
+        match result {
+            Ok(v) => {
+                defined.insert(v.id());
+            }
+            Err(e) => push_oob(e, errors),
+        }
+    }
+
+    for op in region.operations() {
+        for result in op.inputs() {
+            match result {
+                Ok(v) if !defined.contains(&v.id()) => {
+                    errors.push(VerificationError::UsedBeforeDefined { value_id: v.id() });
+                }
+                Ok(_) => {}
+                Err(e) => push_oob(e, errors),
+            }
+        }
+
+        for result in op.outputs() {
+            match result {
+                Ok(v) => {
+                    defined.insert(v.id());
+                }
+                Err(e) => push_oob(e, errors),
+            }
+        }
+
+        if let OpType::ControlFlowOp(cf_op) = op.op_type() {
+            check_cf_ordering(cf_op.as_ref(), &defined, errors);
+        }
+    }
+
+    for result in region.targets() {
+        match result {
+            Ok(v) if !defined.contains(&v.id()) => {
+                errors.push(VerificationError::UsedBeforeDefined { value_id: v.id() });
+            }
+            Ok(_) => {}
+            Err(e) => push_oob(e, errors),
+        }
+    }
+}
+
+fn check_cf_ordering(
+    cf_op: &ControlFlowOp<'_>,
+    outer_defined: &HashSet<ValueId>,
+    errors: &mut Vec<VerificationError>,
+) {
+    match cf_op {
+        ControlFlowOp::For { region } => check_region_ordering(*region, outer_defined, errors),
+        ControlFlowOp::While { condition, body } => {
+            check_region_ordering(*condition, outer_defined, errors);
+            check_region_ordering(*body, outer_defined, errors);
+        }
+        ControlFlowOp::DoWhile { body, condition } => {
+            check_region_ordering(*body, outer_defined, errors);
+            check_region_ordering(*condition, outer_defined, errors);
+        }
+        ControlFlowOp::Switch(switch_op) => {
+            for branch in switch_op.branches() {
+                check_region_ordering(branch, outer_defined, errors);
+            }
+            if let Some(default) = switch_op.default_branch() {
+                check_region_ordering(default, outer_defined, errors);
+            }
+        }
+    }
+}
diff --git a/tools/verifier/tests/encode_tests.sh b/tools/verifier/tests/encode_tests.sh
new file mode 100755
index 0000000..be2d0d1
--- /dev/null
+++ b/tools/verifier/tests/encode_tests.sh
@@ -0,0 +1,17 @@
+#!/bin/bash
+set -e
+
+if [ $# -ne 1 ]; then
+    echo "Usage: $0 <directory>" >&2
+    exit 1
+fi
+
+dir="$1"
+schema="$(dirname "$0")/../../../impl/capnp/jeff.capnp"
+
+find "$dir" -name "*.txt" -type f | while read -r txt; do
+    jeff="${txt%.txt}.jeff"
+    if ! capnp encode "$schema" Module < "$txt" > "$jeff"; then
+        echo "Error encoding $txt" >&2
+    fi
+done
diff --git a/tools/verifier/tests/negative.rs b/tools/verifier/tests/negative.rs
new file mode 100644
index 0000000..8f3adac
--- /dev/null
+++ b/tools/verifier/tests/negative.rs
@@ -0,0 +1,162 @@
+#![allow(missing_docs)]
+use jeff::reader::ReadJeff;
+use jeff::Jeff;
+use std::fs::File;
+use std::path::Path;
+use verifier::{verify_module, VerificationError};
+
+fn load_negative(name: &str) -> Vec<VerificationError> {
+    let path = Path::new(env!("CARGO_MANIFEST_DIR"))
+        .join("tests/negative")
+        .join(name);
+    let file = File::open(&path).unwrap_or_else(|_| panic!("missing fixture: {path:?}"));
+    verify_module(
+        Jeff::read(file)
+            .expect("failed to parse jeff file")
+            .module(),
+    )
+}
+
+#[test]
+fn missing_version() {
+    let errors = load_negative("missing_version.jeff");
+    assert!(
+        errors
+            .iter()
+            .any(|e| matches!(e, VerificationError::MissingVersion)),
+        "expected MissingVersion, got: {errors:?}"
+    );
+}
+
+#[test]
+fn incompatible_version() {
+    let errors = load_negative("incompatible_version.jeff");
+    assert!(
+        errors
+            .iter()
+            .any(|e| matches!(e, VerificationError::IncompatibleVersion)),
+        "expected IncompatibleVersion, got: {errors:?}"
+    );
+}
+
+#[test]
+fn invalid_entrypoint() {
+    let errors = load_negative("invalid_entrypoint.jeff");
+    assert!(
+        errors
+            .iter()
+            .any(|e| matches!(e, VerificationError::InvalidEntrypoint)),
+        "expected InvalidEntrypoint, got: {errors:?}"
+    );
+}
+
+#[test]
+fn value_out_of_bounds() {
+    let errors = load_negative("value_out_of_bounds.jeff");
+    assert!(
+        errors
+            .iter()
+            .any(|e| matches!(e, VerificationError::ValueOutOfBounds { .. })),
+        "expected ValueOutOfBounds, got: {errors:?}"
+    );
+}
+
+#[test]
+fn used_before_defined() {
+    let errors = load_negative("used_before_defined.jeff");
+    assert!(
+        errors
+            .iter()
+            .any(|e| matches!(e, VerificationError::UsedBeforeDefined { .. })),
+        "expected UsedBeforeDefined, got: {errors:?}"
+    );
+}
+
+#[test]
+fn value_produced_twice() {
+    let errors = load_negative("value_produced_twice.jeff");
+    assert!(
+        errors
+            .iter()
+            .any(|e| matches!(e, VerificationError::ValueProducedMultipleTimes { .. })),
+        "expected ValueProducedMultipleTimes, got: {errors:?}"
+    );
+}
+
+#[test]
+fn linear_never_consumed() {
+    let errors = load_negative("linear_never_consumed.jeff");
+    assert!(
+        errors
+            .iter()
+            .any(|e| matches!(e, VerificationError::LinearValueNeverConsumed { .. })),
+        "expected LinearValueNeverConsumed, got: {errors:?}"
+    );
+}
+
+#[test]
+fn linear_consumed_twice() {
+    let errors = load_negative("linear_consumed_twice.jeff");
+    assert!(
+        errors.iter().any(|e| matches!(
+            e,
+            VerificationError::LinearValueConsumedMultipleTimes { .. }
+        )),
+        "expected LinearValueConsumedMultipleTimes, got: {errors:?}"
+    );
+}
+
+#[test]
+fn type_mismatch() {
+    let errors = load_negative("type_mismatch.jeff");
+    assert!(
+        errors
+            .iter()
+            .any(|e| matches!(e, VerificationError::TypeMismatch { .. })),
+        "expected TypeMismatch, got: {errors:?}"
+    );
+}
+
+#[test]
+fn invalid_input_type() {
+    let errors = load_negative("invalid_input_type.jeff");
+    assert!(
+        errors
+            .iter()
+            .any(|e| matches!(e, VerificationError::InvalidInputType { .. })),
+        "expected InvalidInputType, got: {errors:?}"
+    );
+}
+
+#[test]
+fn invalid_output_type() {
+    let errors = load_negative("invalid_output_type.jeff");
+    assert!(
+        errors
+            .iter()
+            .any(|e| matches!(e, VerificationError::InvalidOutputType { .. })),
+        "expected InvalidOutputType, got: {errors:?}"
+    );
+}
+
+#[test]
+fn wrong_arity() {
+    let errors = load_negative("wrong_arity.jeff");
+    assert!(
+        errors
+            .iter()
+            .any(|e| matches!(e, VerificationError::WrongArity { .. })),
+        "expected WrongArity, got: {errors:?}"
+    );
+}
+
+#[test]
+fn isolation_violation() {
+    let errors = load_negative("isolation_violation.jeff");
+    assert!(
+        errors
+            .iter()
+            .any(|e| matches!(e, VerificationError::IsolationViolation { .. })),
+        "expected IsolationViolation, got: {errors:?}"
+    );
+}
diff --git a/tools/verifier/tests/negative/incompatible_version.jeff b/tools/verifier/tests/negative/incompatible_version.jeff
new file mode 100644
index 0000000..e09ed96
Binary files /dev/null and b/tools/verifier/tests/negative/incompatible_version.jeff differ
diff --git a/tools/verifier/tests/negative/incompatible_version.txt b/tools/verifier/tests/negative/incompatible_version.txt
new file mode 100644
index 0000000..64f9786
--- /dev/null
+++ b/tools/verifier/tests/negative/incompatible_version.txt
@@ -0,0 +1,13 @@
+( version = 0,
+  versionMinor = 1,
+  versionPatch = 0,
+  functions = [
+    ( name = 0,
+      definition = (
+        body = (
+          sources = [],
+          targets = [],
+          operations = [] ),
+        values = [] ) ) ],
+  strings = ["main"],
+  entrypoint = 0 )
diff --git a/tools/verifier/tests/negative/invalid_entrypoint.jeff b/tools/verifier/tests/negative/invalid_entrypoint.jeff
new file mode 100644
index 0000000..b26298f
Binary files /dev/null and b/tools/verifier/tests/negative/invalid_entrypoint.jeff differ
diff --git a/tools/verifier/tests/negative/invalid_entrypoint.txt b/tools/verifier/tests/negative/invalid_entrypoint.txt
new file mode 100644
index 0000000..e4776c1
--- /dev/null
+++ b/tools/verifier/tests/negative/invalid_entrypoint.txt
@@ -0,0 +1,8 @@
+( version = 0,
+  versionMinor = 2,
+  versionPatch = 0,
+  functions = [
+    ( name = 0,
+      declaration = (inputs = [], outputs = []) ) ],
+  strings = ["f"],
+  entrypoint = 0 )
diff --git a/tools/verifier/tests/negative/invalid_input_type.jeff b/tools/verifier/tests/negative/invalid_input_type.jeff
new file mode 100644
index 0000000..2c826c3
Binary files /dev/null and b/tools/verifier/tests/negative/invalid_input_type.jeff differ
diff --git a/tools/verifier/tests/negative/invalid_input_type.txt b/tools/verifier/tests/negative/invalid_input_type.txt
new file mode 100644
index 0000000..190b2d5
--- /dev/null
+++ b/tools/verifier/tests/negative/invalid_input_type.txt
@@ -0,0 +1,20 @@
+( version = 0,
+  versionMinor = 2,
+  versionPatch = 0,
+  functions = [
+    ( name = 0,
+      definition = (
+        body = (
+          sources = [],
+          targets = [],
+          operations = [
+            ( outputs = [0],
+              instruction = (int = (const32 = 0)) ),
+            ( inputs = [0],
+              outputs = [1],
+              instruction = (qubit = (measure = void)) ) ] ),
+        values = [
+          (type = (int = 32)),
+          (type = (int = 1)) ] ) ) ],
+  strings = ["main"],
+  entrypoint = 0 )
diff --git a/tools/verifier/tests/negative/invalid_output_type.jeff b/tools/verifier/tests/negative/invalid_output_type.jeff
new file mode 100644
index 0000000..fb47d1f
Binary files /dev/null and b/tools/verifier/tests/negative/invalid_output_type.jeff differ
diff --git a/tools/verifier/tests/negative/invalid_output_type.txt b/tools/verifier/tests/negative/invalid_output_type.txt
new file mode 100644
index 0000000..adfc328
--- /dev/null
+++ b/tools/verifier/tests/negative/invalid_output_type.txt
@@ -0,0 +1,16 @@
+( version = 0,
+  versionMinor = 2,
+  versionPatch = 0,
+  functions = [
+    ( name = 0,
+      definition = (
+        body = (
+          sources = [],
+          targets = [],
+          operations = [
+            ( outputs = [0],
+              instruction = (qubit = (alloc = void)) ) ] ),
+        values = [
+          (type = (int = 32)) ] ) ) ],
+  strings = ["main"],
+  entrypoint = 0 )
diff --git a/tools/verifier/tests/negative/isolation_violation.jeff b/tools/verifier/tests/negative/isolation_violation.jeff
new file mode 100644
index 0000000..d96f6fe
Binary files /dev/null and b/tools/verifier/tests/negative/isolation_violation.jeff differ
diff --git a/tools/verifier/tests/negative/isolation_violation.txt b/tools/verifier/tests/negative/isolation_violation.txt
new file mode 100644
index 0000000..998c2c6
--- /dev/null
+++ b/tools/verifier/tests/negative/isolation_violation.txt
@@ -0,0 +1,29 @@
+( version = 0,
+  versionMinor = 2,
+  versionPatch = 0,
+  functions = [
+    ( name = 0,
+      definition = (
+        body = (
+          sources = [],
+          targets = [],
+          operations = [
+            ( outputs = [0],
+              instruction = (int = (const1 = false)) ),
+            ( outputs = [1],
+              instruction = (int = (const32 = 1)) ),
+            ( inputs = [1, 1, 1],
+              instruction = (scf = (for = (
+                sources = [2],
+                targets = [],
+                operations = [
+                  ( inputs = [0],
+                    outputs = [3],
+                    instruction = (int = (not = void)) ) ] ) )) ) ] ),
+        values = [
+          (type = (int = 1)),
+          (type = (int = 32)),
+          (type = (int = 32)),
+          (type = (int = 1)) ] ) ) ],
+  strings = ["main"],
+  entrypoint = 0 )
diff --git a/tools/verifier/tests/negative/linear_consumed_twice.jeff b/tools/verifier/tests/negative/linear_consumed_twice.jeff
new file mode 100644
index 0000000..6c1b2a7
Binary files /dev/null and b/tools/verifier/tests/negative/linear_consumed_twice.jeff differ
diff --git a/tools/verifier/tests/negative/linear_consumed_twice.txt b/tools/verifier/tests/negative/linear_consumed_twice.txt
new file mode 100644
index 0000000..0c93260
--- /dev/null
+++ b/tools/verifier/tests/negative/linear_consumed_twice.txt
@@ -0,0 +1,20 @@
+( version = 0,
+  versionMinor = 2,
+  versionPatch = 0,
+  functions = [
+    ( name = 0,
+      definition = (
+        body = (
+          sources = [],
+          targets = [],
+          operations = [
+            ( outputs = [0],
+              instruction = (qubit = (alloc = void)) ),
+            ( inputs = [0],
+              instruction = (qubit = (free = void)) ),
+            ( inputs = [0],
+              instruction = (qubit = (free = void)) ) ] ),
+        values = [
+          (type = (qubit = void)) ] ) ) ],
+  strings = ["main"],
+  entrypoint = 0 )
diff --git a/tools/verifier/tests/negative/linear_never_consumed.jeff b/tools/verifier/tests/negative/linear_never_consumed.jeff
new file mode 100644
index 0000000..0f23a0b
Binary files /dev/null and b/tools/verifier/tests/negative/linear_never_consumed.jeff differ
diff --git a/tools/verifier/tests/negative/linear_never_consumed.txt b/tools/verifier/tests/negative/linear_never_consumed.txt
new file mode 100644
index 0000000..cdadc2b
--- /dev/null
+++ b/tools/verifier/tests/negative/linear_never_consumed.txt
@@ -0,0 +1,16 @@
+( version = 0,
+  versionMinor = 2,
+  versionPatch = 0,
+  functions = [
+    ( name = 0,
+      definition = (
+        body = (
+          sources = [],
+          targets = [],
+          operations = [
+            ( outputs = [0],
+              instruction = (qubit = (alloc = void)) ) ] ),
+        values = [
+          (type = (qubit = void)) ] ) ) ],
+  strings = ["main"],
+  entrypoint = 0 )
diff --git a/tools/verifier/tests/negative/missing_version.jeff b/tools/verifier/tests/negative/missing_version.jeff
new file mode 100644
index 0000000..73539a5
Binary files /dev/null and b/tools/verifier/tests/negative/missing_version.jeff differ
diff --git a/tools/verifier/tests/negative/missing_version.txt b/tools/verifier/tests/negative/missing_version.txt
new file mode 100644
index 0000000..5cf3146
--- /dev/null
+++ b/tools/verifier/tests/negative/missing_version.txt
@@ -0,0 +1,11 @@
+( version = 0,
+  functions = [
+    ( name = 0,
+      definition = (
+        body = (
+          sources = [],
+          targets = [],
+          operations = [] ),
+        values = [] ) ) ],
+  strings = ["main"],
+  entrypoint = 0 )
diff --git a/tools/verifier/tests/negative/type_mismatch.jeff b/tools/verifier/tests/negative/type_mismatch.jeff
new file mode 100644
index 0000000..432dad8
Binary files /dev/null and b/tools/verifier/tests/negative/type_mismatch.jeff differ
diff --git a/tools/verifier/tests/negative/type_mismatch.txt b/tools/verifier/tests/negative/type_mismatch.txt
new file mode 100644
index 0000000..9dfe6a3
--- /dev/null
+++ b/tools/verifier/tests/negative/type_mismatch.txt
@@ -0,0 +1,23 @@
+( version = 0,
+  versionMinor = 2,
+  versionPatch = 0,
+  functions = [
+    ( name = 0,
+      definition = (
+        body = (
+          sources = [],
+          targets = [2],
+          operations = [
+            ( outputs = [0],
+              instruction = (int = (const32 = 0)) ),
+            ( outputs = [1],
+              instruction = (int = (const64 = 0)) ),
+            ( inputs = [0, 1],
+              outputs = [2],
+              instruction = (int = (add = void)) ) ] ),
+        values = [
+          (type = (int = 32)),
+          (type = (int = 64)),
+          (type = (int = 32)) ] ) ) ],
+  strings = ["main"],
+  entrypoint = 0 )
diff --git a/tools/verifier/tests/negative/used_before_defined.jeff b/tools/verifier/tests/negative/used_before_defined.jeff
new file mode 100644
index 0000000..dfa1db9
Binary files /dev/null and b/tools/verifier/tests/negative/used_before_defined.jeff differ
diff --git a/tools/verifier/tests/negative/used_before_defined.txt b/tools/verifier/tests/negative/used_before_defined.txt
new file mode 100644
index 0000000..29f38f3
--- /dev/null
+++ b/tools/verifier/tests/negative/used_before_defined.txt
@@ -0,0 +1,20 @@
+( version = 0,
+  versionMinor = 2,
+  versionPatch = 0,
+  functions = [
+    ( name = 0,
+      definition = (
+        body = (
+          sources = [],
+          targets = [],
+          operations = [
+            ( inputs = [1],
+              outputs = [0],
+              instruction = (int = (not = void)) ),
+            ( outputs = [1],
+              instruction = (int = (const1 = false)) ) ] ),
+        values = [
+          (type = (int = 1)),
+          (type = (int = 1)) ] ) ) ],
+  strings = ["main"],
+  entrypoint = 0 )
diff --git a/tools/verifier/tests/negative/value_out_of_bounds.jeff b/tools/verifier/tests/negative/value_out_of_bounds.jeff
new file mode 100644
index 0000000..91ac7af
Binary files /dev/null and b/tools/verifier/tests/negative/value_out_of_bounds.jeff differ
diff --git a/tools/verifier/tests/negative/value_out_of_bounds.txt b/tools/verifier/tests/negative/value_out_of_bounds.txt
new file mode 100644
index 0000000..5bb7577
--- /dev/null
+++ b/tools/verifier/tests/negative/value_out_of_bounds.txt
@@ -0,0 +1,15 @@
+( version = 0,
+  versionMinor = 2,
+  versionPatch = 0,
+  functions = [
+    ( name = 0,
+      definition = (
+        body = (
+          sources = [],
+          targets = [],
+          operations = [
+            ( inputs = [0],
+              instruction = (qubit = (free = void)) ) ] ),
+        values = [] ) ) ],
+  strings = ["main"],
+  entrypoint = 0 )
diff --git a/tools/verifier/tests/negative/value_produced_twice.jeff b/tools/verifier/tests/negative/value_produced_twice.jeff
new file mode 100644
index 0000000..f3209c9
Binary files /dev/null and b/tools/verifier/tests/negative/value_produced_twice.jeff differ
diff --git a/tools/verifier/tests/negative/value_produced_twice.txt b/tools/verifier/tests/negative/value_produced_twice.txt
new file mode 100644
index 0000000..cc5cb2b
--- /dev/null
+++ b/tools/verifier/tests/negative/value_produced_twice.txt
@@ -0,0 +1,16 @@
+( version = 0,
+  versionMinor = 2,
+  versionPatch = 0,
+  functions = [
+    ( name = 0,
+      definition = (
+        body = (
+          sources = [0],
+          targets = [],
+          operations = [
+            ( outputs = [0],
+              instruction = (int = (const1 = false)) ) ] ),
+        values = [
+          (type = (int = 1)) ] ) ) ],
+  strings = ["main"],
+  entrypoint = 0 )
diff --git a/tools/verifier/tests/negative/wrong_arity.jeff b/tools/verifier/tests/negative/wrong_arity.jeff
new file mode 100644
index 0000000..160fe65
Binary files /dev/null and b/tools/verifier/tests/negative/wrong_arity.jeff differ
diff --git a/tools/verifier/tests/negative/wrong_arity.txt b/tools/verifier/tests/negative/wrong_arity.txt
new file mode 100644
index 0000000..a85f995
--- /dev/null
+++ b/tools/verifier/tests/negative/wrong_arity.txt
@@ -0,0 +1,18 @@
+( version = 0,
+  versionMinor = 2,
+  versionPatch = 0,
+  functions = [
+    ( name = 0,
+      definition = (
+        body = (
+          sources = [],
+          targets = [],
+          operations = [
+            ( outputs = [0],
+              instruction = (qubit = (alloc = void)) ),
+            ( inputs = [0],
+              instruction = (qubit = (gate = (custom = (name = 1, numQubits = 1, numParams = 0), controlQubits = 0, adjoint = false, power = 1))) ) ] ),
+        values = [
+          (type = (qubit = void)) ] ) ) ],
+  strings = ["main", "H"],
+  entrypoint = 0 )
diff --git a/tools/verifier/tests/positive.rs b/tools/verifier/tests/positive.rs
new file mode 100644
index 0000000..9f52bbd
--- /dev/null
+++ b/tools/verifier/tests/positive.rs
@@ -0,0 +1,105 @@
+#![allow(missing_docs)]
+use jeff::reader::ReadJeff;
+use jeff::Jeff;
+use std::fs::File;
+use std::path::Path;
+use verifier::{verify_module, VerificationError};
+
+fn load_positive(name: &str) -> Vec<VerificationError> {
+    let path = Path::new(env!("CARGO_MANIFEST_DIR"))
+        .join("tests/positive")
+        .join(name);
+    let file = File::open(&path).unwrap_or_else(|_| panic!("missing fixture: {path:?}"));
+    verify_module(
+        Jeff::read(file)
+            .expect("failed to parse jeff file")
+            .module(),
+    )
+}
+
+fn load_example(rel: &str) -> Vec<VerificationError> {
+    let path = Path::new(env!("CARGO_MANIFEST_DIR"))
+        .join("../../examples")
+        .join(rel);
+    let file = File::open(&path).unwrap_or_else(|_| panic!("missing example: {path:?}"));
+    verify_module(
+        Jeff::read(file)
+            .expect("failed to parse jeff file")
+            .module(),
+    )
+}
+
+// positive tests
+
+#[test]
+fn valid_alloc_gate_measure() {
+    let errors = load_positive("valid_alloc_gate_measure.jeff");
+    assert!(errors.is_empty(), "expected no errors, got: {errors:?}");
+}
+
+#[test]
+fn valid_deep_qubit_chain() {
+    let errors = load_positive("valid_deep_qubit_chain.jeff");
+    assert!(errors.is_empty(), "expected no errors, got: {errors:?}");
+}
+
+#[test]
+fn valid_for_qubit_isolation() {
+    let errors = load_positive("valid_for_qubit_isolation.jeff");
+    assert!(errors.is_empty(), "expected no errors, got: {errors:?}");
+}
+
+#[test]
+fn valid_int_float_ops() {
+    let errors = load_positive("valid_int_float_ops.jeff");
+    assert!(errors.is_empty(), "expected no errors, got: {errors:?}");
+}
+
+#[test]
+fn valid_while_isolation() {
+    let errors = load_positive("valid_while_isolation.jeff");
+    assert!(errors.is_empty(), "expected no errors, got: {errors:?}");
+}
+
+#[test]
+fn valid_three_qubit_gates() {
+    let errors = load_positive("valid_three_qubit_gates.jeff");
+    assert!(errors.is_empty(), "expected no errors, got: {errors:?}");
+}
+
+// examples
+#[test]
+fn example_qubits() {
+    let errors = load_example("qubits/qubits.jeff");
+    assert!(errors.is_empty(), "expected no errors, got: {errors:?}");
+}
+
+#[test]
+fn example_entangled_qs() {
+    let errors = load_example("entangled_qs/entangled_qs.jeff");
+    assert!(errors.is_empty(), "expected no errors, got: {errors:?}");
+}
+
+#[test]
+fn example_entangled_calls() {
+    let errors = load_example("entangled_calls/entangled_calls.jeff");
+    assert!(errors.is_empty(), "expected no errors, got: {errors:?}");
+}
+
+#[test]
+fn example_catalyst_simple() {
+    let errors = load_example("catalyst_simple/catalyst_simple.jeff");
+    assert!(errors.is_empty(), "expected no errors, got: {errors:?}");
+}
+
+#[test]
+fn example_catalyst_tket_opt() {
+    let errors = load_example("catalyst_tket_opt/catalyst_tket_opt.jeff");
+    assert!(errors.is_empty(), "expected no errors, got: {errors:?}");
+}
+
+#[test]
+fn example_python_optimization() {
+    let errors = load_example("python_optimization/python_optimization.jeff");
+    assert!(errors.is_empty(), "expected no errors, got: {errors:?}");
+}
diff --git a/tools/verifier/tests/positive/valid_alloc_gate_measure.jeff b/tools/verifier/tests/positive/valid_alloc_gate_measure.jeff
new file mode 100644
index 0000000..37e351e
Binary files /dev/null and b/tools/verifier/tests/positive/valid_alloc_gate_measure.jeff differ
diff --git a/tools/verifier/tests/positive/valid_alloc_gate_measure.txt b/tools/verifier/tests/positive/valid_alloc_gate_measure.txt
new file mode 100644
index 0000000..58bd5a7
--- /dev/null
+++ b/tools/verifier/tests/positive/valid_alloc_gate_measure.txt
@@ -0,0 +1,36 @@
+( version = 0,
+  versionMinor = 2,
+  versionPatch = 0,
+  functions = [
+    ( name = 0,
+      definition = (
+        body = (
+          sources = [],
+          targets = [5, 6],
+          operations = [
+            ( outputs = [0],
+              instruction = (qubit = (alloc = void)) ),
+            ( outputs = [1],
+              instruction = (qubit = (alloc = void)) ),
+            ( inputs = [0],
+              outputs = [2],
+              instruction = (qubit = (gate = (custom = (name = 1, numQubits = 1, numParams = 0), controlQubits = 0, adjoint = false, power = 1))) ),
+            ( inputs = [2, 1],
+              outputs = [3, 4],
+              instruction = (qubit = (gate = (custom = (name = 2, numQubits = 2, numParams = 0), controlQubits = 0, adjoint = false, power = 1))) ),
+            ( inputs = [3],
+              outputs = [5],
+              instruction = (qubit = (measure = void)) ),
+            ( inputs = [4],
+              outputs = [6],
+              instruction = (qubit = (measure = void)) ) ] ),
+        values = [
+          (type = (qubit = void)),
+          (type = (qubit = void)),
+          (type = (qubit = void)),
+          (type = (qubit = void)),
+          (type = (qubit = void)),
+          (type = (int = 1)),
+          (type = (int = 1)) ] ) ) ],
+  strings = ["main", "H", "CX"],
+  entrypoint = 0 )
diff --git a/tools/verifier/tests/positive/valid_deep_qubit_chain.jeff b/tools/verifier/tests/positive/valid_deep_qubit_chain.jeff
new file mode 100644
index 0000000..aaaece9
Binary files /dev/null and b/tools/verifier/tests/positive/valid_deep_qubit_chain.jeff differ
diff --git a/tools/verifier/tests/positive/valid_deep_qubit_chain.txt b/tools/verifier/tests/positive/valid_deep_qubit_chain.txt
new file mode 100644
index 0000000..fac04df
--- /dev/null
+++ b/tools/verifier/tests/positive/valid_deep_qubit_chain.txt
@@ -0,0 +1,60 @@
+( version = 0,
+  versionMinor = 2,
+  versionPatch = 0,
+  functions = [
+    ( name = 0,
+      definition = (
+        body = (
+          sources = [],
+          targets = [9, 10, 13],
+          operations = [
+            ( outputs = [0],
+              instruction = (qubit = (alloc = void)) ),
+            ( outputs = [1],
+              instruction = (qubit = (alloc = void)) ),
+            ( outputs = [2],
+              instruction = (qubit = (alloc = void)) ),
+            ( inputs = [1],
+              outputs = [3],
+              instruction = (qubit = (gate = (custom = (name = 1, numQubits = 1, numParams = 0), controlQubits = 0, adjoint = false, power = 1))) ),
+            ( inputs = [3, 2],
+              outputs = [4, 5],
+              instruction = (qubit = (gate = (custom = (name = 2, numQubits = 2, numParams = 0), controlQubits = 0, adjoint = false, power = 1))) ),
+            ( inputs = [0, 4],
+              outputs = [6, 7],
+              instruction = (qubit = (gate = (custom = (name = 2, numQubits = 2, numParams = 0), controlQubits = 0, adjoint = false, power = 1))) ),
+            ( inputs = [6],
+              outputs = [8],
+              instruction = (qubit = (gate = (custom = (name = 1, numQubits = 1, numParams = 0), controlQubits = 0, adjoint = false, power = 1))) ),
+            ( inputs = [8],
+              outputs = [9],
+              instruction = (qubit = (measure = void)) ),
+            ( inputs = [7],
+              outputs = [10],
+              instruction = (qubit = (measure = void)) ),
+            ( inputs = [5],
+              outputs = [11],
+              instruction = (qubit = (gate = (custom = (name = 3, numQubits = 1, numParams = 0), controlQubits = 0, adjoint = false, power = 1))) ),
+            ( inputs = [11],
+              outputs = [12],
+              instruction = (qubit = (gate = (custom = (name = 4, numQubits = 1, numParams = 0), controlQubits = 0, adjoint = false, power = 1))) ),
+            ( inputs = [12],
+              outputs = [13],
+              instruction = (qubit = (measure = void)) ) ] ),
+        values = [
+          (type = (qubit = void)),
+          (type = (qubit = void)),
+          (type = (qubit = void)),
+          (type = (qubit = void)),
+          (type = (qubit = void)),
+          (type = (qubit = void)),
+          (type = (qubit = void)),
+          (type = (qubit = void)),
+          (type = (qubit = void)),
+          (type = (int = 1)),
+          (type = (int = 1)),
+          (type = (qubit = void)),
+          (type = (qubit = void)),
+          (type = (int = 1)) ] ) ) ],
+  strings = ["main", "H", "CX", "X", "Z"],
+  entrypoint = 0 )
diff --git a/tools/verifier/tests/positive/valid_for_qubit_isolation.jeff b/tools/verifier/tests/positive/valid_for_qubit_isolation.jeff
new file mode 100644
index 0000000..6f66d42
Binary files /dev/null and b/tools/verifier/tests/positive/valid_for_qubit_isolation.jeff differ
diff --git a/tools/verifier/tests/positive/valid_for_qubit_isolation.txt b/tools/verifier/tests/positive/valid_for_qubit_isolation.txt
new file mode 100644
index 0000000..c025a57
--- /dev/null
+++ b/tools/verifier/tests/positive/valid_for_qubit_isolation.txt
@@ -0,0 +1,42 @@
+( version = 0,
+  versionMinor = 2,
+  versionPatch = 0,
+  functions = [
+    ( name = 0,
+      definition = (
+        body = (
+          sources = [],
+          targets = [5],
+          operations = [
+            ( outputs = [0],
+              instruction = (qubit = (alloc = void)) ),
+            ( outputs = [1],
+              instruction = (int = (const32 = 0)) ),
+            ( outputs = [2],
+              instruction = (int = (const32 = 1)) ),
+            ( outputs = [3],
+              instruction = (int = (const32 = 1)) ),
+            ( inputs = [1, 2, 3, 0],
+              outputs = [4],
+              instruction = (scf = (for = (
+                sources = [6, 7],
+                targets = [8],
+                operations = [
+                  ( inputs = [7],
+                    outputs = [8],
+                    instruction = (qubit = (gate = (custom = (name = 1, numQubits = 1, numParams = 0), controlQubits = 0, adjoint = false, power = 1))) ) ] ) )) ),
+            ( inputs = [4],
+              outputs = [5],
+              instruction = (qubit = (measure = void)) ) ] ),
+        values = [
+          (type = (qubit = void)),
+          (type = (int = 32)),
+          (type = (int = 32)),
+          (type = (int = 32)),
+          (type = (qubit = void)),
+          (type = (int = 1)),
+          (type = (int = 32)),
+          (type = (qubit = void)),
+          (type = (qubit = void)) ] ) ) ],
+  strings = ["main", "H"],
+  entrypoint = 0 )
diff --git a/tools/verifier/tests/positive/valid_int_float_ops.jeff b/tools/verifier/tests/positive/valid_int_float_ops.jeff
new file mode 100644
index 0000000..5ec52b7
Binary files /dev/null and b/tools/verifier/tests/positive/valid_int_float_ops.jeff differ
diff --git a/tools/verifier/tests/positive/valid_int_float_ops.txt b/tools/verifier/tests/positive/valid_int_float_ops.txt
new file mode 100644
index 0000000..46b1104
--- /dev/null
+++ b/tools/verifier/tests/positive/valid_int_float_ops.txt
@@ -0,0 +1,41 @@
+( version = 0,
+  versionMinor = 2,
+  versionPatch = 0,
+  functions = [
+    ( name = 0,
+      definition = (
+        body = (
+          sources = [],
+          targets = [2, 3, 6, 7],
+          operations = [
+            ( outputs = [0],
+              instruction = (int = (const32 = 10)) ),
+            ( outputs = [1],
+              instruction = (int = (const32 = 20)) ),
+            ( inputs = [0, 1],
+              outputs = [2],
+              instruction = (int = (add = void)) ),
+            ( inputs = [0, 1],
+              outputs = [3],
+              instruction = (int = (eq = void)) ),
+            ( outputs = [4],
+              instruction = (float = (const64 = 1.5)) ),
+            ( outputs = [5],
+              instruction = (float = (const64 = 2.5)) ),
+            ( inputs = [4, 5],
+              outputs = [6],
+              instruction = (float = (add = void)) ),
+            ( inputs = [4, 5],
+              outputs = [7],
+              instruction = (float = (lt = void)) ) ] ),
+        values = [
+          (type = (int = 32)),
+          (type = (int = 32)),
+          (type = (int = 32)),
+          (type = (int = 1)),
+          (type = (float = float64)),
+          (type = (float = float64)),
+          (type = (float = float64)),
+          (type = (int = 1)) ] ) ) ],
+  strings = ["main"],
+  entrypoint = 0 )
diff --git a/tools/verifier/tests/positive/valid_three_qubit_gates.jeff b/tools/verifier/tests/positive/valid_three_qubit_gates.jeff
new file mode 100644
index 0000000..e67fb6e
Binary files /dev/null and b/tools/verifier/tests/positive/valid_three_qubit_gates.jeff differ
diff --git a/tools/verifier/tests/positive/valid_three_qubit_gates.txt b/tools/verifier/tests/positive/valid_three_qubit_gates.txt
new file mode 100644
index 0000000..db0aa40
--- /dev/null
+++ b/tools/verifier/tests/positive/valid_three_qubit_gates.txt
@@ -0,0 +1,48 @@
+( version = 0,
+  versionMinor = 2,
+  versionPatch = 0,
+  functions = [
+    ( name = 0,
+      definition = (
+        body = (
+          sources = [],
+          targets = [8, 9, 10],
+          operations = [
+            ( outputs = [0],
+              instruction = (qubit = (alloc = void)) ),
+            ( outputs = [1],
+              instruction = (qubit = (alloc = void)) ),
+            ( outputs = [2],
+              instruction = (qubit = (alloc = void)) ),
+            ( inputs = [0],
+              outputs = [3],
+              instruction = (qubit = (gate = (custom = (name = 1, numQubits = 1, numParams = 0), controlQubits = 0, adjoint = false, power = 1))) ),
+            ( inputs = [3, 1],
+              outputs = [4, 5],
+              instruction = (qubit = (gate = (custom = (name = 2, numQubits = 2, numParams = 0), controlQubits = 0, adjoint = false, power = 1))) ),
+            ( inputs = [5, 2],
+              outputs = [6, 7],
+              instruction = (qubit = (gate = (custom = (name = 2, numQubits = 2, numParams = 0), controlQubits = 0, adjoint = false, power = 1))) ),
+            ( inputs = [4],
+              outputs = [8],
+              instruction = (qubit = (measure = void)) ),
+            ( inputs = [6],
+              outputs = [9],
+              instruction = (qubit = (measure = void)) ),
+            ( inputs = [7],
+              outputs = [10],
+              instruction = (qubit = (measure = void)) ) ] ),
+        values = [
+          (type = (qubit = void)),
+          (type = (qubit = void)),
+          (type = (qubit = void)),
+          (type = (qubit = void)),
+          (type = (qubit = void)),
+          (type = (qubit = void)),
+          (type = (qubit = void)),
+          (type = (qubit = void)),
+          (type = (int = 1)),
+          (type = (int = 1)),
+          (type = (int = 1)) ] ) ) ],
+  strings = ["main", "H", "CX"],
+  entrypoint = 0 )
diff --git a/tools/verifier/tests/positive/valid_while_isolation.jeff b/tools/verifier/tests/positive/valid_while_isolation.jeff
new file mode 100644
index 0000000..0939019
Binary files /dev/null and b/tools/verifier/tests/positive/valid_while_isolation.jeff differ
diff --git a/tools/verifier/tests/positive/valid_while_isolation.txt b/tools/verifier/tests/positive/valid_while_isolation.txt
new file mode 100644
index 0000000..bb93e48
--- /dev/null
+++ b/tools/verifier/tests/positive/valid_while_isolation.txt
@@ -0,0 +1,38 @@
+( version = 0,
+  versionMinor = 2,
+  versionPatch = 0,
+  functions = [
+    ( name = 0,
+      definition = (
+        body = (
+          sources = [],
+          targets = [1],
+          operations = [
+            ( outputs = [0],
+              instruction = (int = (const1 = false)) ),
+            ( inputs = [0],
+              outputs = [1],
+              instruction = (scf = (while = (
+                condition = (
+                  sources = [2],
+                  targets = [3],
+                  operations = [
+                    ( inputs = [2],
+                      outputs = [3],
+                      instruction = (int = (not = void)) ) ] ),
+                body = (
+                  sources = [4],
+                  targets = [5],
+                  operations = [
+                    ( inputs = [4],
+                      outputs = [5],
+                      instruction = (int = (not = void)) ) ] ) ) )) ) ] ),
+        values = [
+          (type = (int = 1)),
+          (type = (int = 1)),
+          (type = (int = 1)),
+          (type = (int = 1)),
+          (type = (int = 1)),
+          (type = (int = 1)) ] ) ) ],
+  strings = ["main"],
+  entrypoint = 0 )