Graph neural networks are deployed in safety-critical systems -- drug discovery, autonomous navigation, financial fraud detection, medical diagnosis -- yet they provide zero formal guarantees about their behavior. Specifically:
- No robustness certificates: A single adversarial edge insertion or feature perturbation can flip a GNN's prediction, and there is no efficient way to prove that small perturbations cannot change the output.
- No training invariants: GNN training proceeds by gradient descent with no proof that conservation laws (e.g., total message mass), equivariance properties (e.g., permutation invariance), or monotonic loss decrease are preserved across updates.
- No type safety for message passing: Messages are untyped tensors. Nothing prevents dimension mismatches between sender embeddings, message functions, and receiver aggregations. Bugs manifest as silent shape errors or NaN propagation.
- No verified graph operations: Adding a node, removing an edge, or reweighting attention produces no machine-checked proof that the operation preserves desired invariants (connectivity, degree bounds, spectral properties).
The consequence is that GNNs in safety-critical deployments require extensive empirical testing but can never be provably correct. A single untested edge case can cause catastrophic failure.
Formally Verified Graph Transformers (FVGTs) extend graph neural networks with a proof-carrying computation model where every graph operation, attention update, and training step is accompanied by a machine-checked proof certificate. The approach builds on RuVector's existing ruvector-verified crate (lean-agentic dependent types, ProofEnvironment, FastTermArena, gated proof routing, 82-byte attestations) and extends it to cover the full GNN lifecycle:
- Proof-Carrying Graph Transformations: Every structural graph operation (node add, edge remove, attention reweight) produces a proof that specified invariants are preserved.
- Verified Training Loops: Each gradient step is accompanied by a proof certificate covering loss monotonicity, conservation law preservation, and equivariance maintenance.
- Certified Adversarial Robustness: Given an epsilon perturbation budget, produce a formal certificate that the GNN output is stable for all perturbations within the budget.
- Type-Safe Message Passing: Dependent types ensure message dimensions, aggregation commutativity, and permutation invariance are checked at compile time.
- Certified Safety: Machine-checked proofs for every GNN operation, enabling deployment in regulated environments (FDA, FAA, SEC)
- Adversarial Robustness Certificates: Provable guarantees that predictions are stable under epsilon-bounded perturbations
- Training Correctness: Proof certificates for each training epoch, enabling auditable model development
- Type-Safe GNN Pipelines: Compile-time elimination of dimension mismatch bugs in message passing
- Proof-Carrying Attestations: 82-byte proof attestations (from
ruvector-verified) for lightweight verification of GNN outputs
Unique Contribution: First system providing machine-checked proof certificates for the complete GNN lifecycle -- from graph construction through training to inference. Unlike empirical robustness testing or statistical certification (randomized smoothing), FVGTs provide deterministic, machine-checked proofs.
Differentiators:
- Lean-agentic dependent types for graph operations (extending
ruvector-verified) - Proof-carrying training with per-epoch certificates
- Exact (not probabilistic) adversarial robustness bounds via interval bound propagation with proof witnesses
- Type-safe message passing with compile-time dimension checking
- Gated proof routing (from
ruvector-verified/gated.rs) that allocates verification budget proportional to operation criticality
The verification gap in graph neural networks is severe compared to other software domains:
| Domain | Verification State | GNN Equivalent |
|---|---|---|
| Compilers | Formally verified (CompCert, CakeML) | No verified GNN compiler |
| Operating Systems | Verified kernels (seL4) | No verified GNN runtime |
| Cryptography | Machine-checked proofs (HACL*, Fiat-Crypto) | No proved GNN properties |
| Numerical Libraries | Verified floating-point (VCFloat) | No verified tensor ops |
| Smart Contracts | Formal verification tools (Certora, Solidity SMT) | No verified graph operations |
Existing approaches to GNN reliability are insufficient:
- Empirical testing: Tests a finite set of inputs. Cannot prove absence of failure.
- Randomized smoothing: Provides probabilistic certificates. Not deterministic guarantees.
- Adversarial training: Improves empirical robustness. Does not prove robustness.
- Model interpretability: Explains behavior. Does not verify correctness.
Formal verification produces mathematical proofs that are checked by a trusted kernel (a small, auditable program). If the proof checks, the property holds for all inputs in the specified domain, not just tested ones. For GNNs, this means:
- "For ALL graphs with N <= 10000 nodes and epsilon-bounded perturbations, the classifier output is stable" (not "for the 1000 graphs we tested")
- "For ALL gradient steps, the equivariance error remains below delta" (not "equivariance held on our training run")
- "For ALL message passing configurations with matching types, no dimension mismatch occurs" (not "our tests passed")
Graph Neural Network
|
+-----------------+-----------------+
| | |
Graph Ops Attention Training
(add/del/ (compute (gradient
reweight) weights) step)
| | |
+----v----+ +----v----+ +-----v-----+
| Proof | | Proof | | Proof |
| Witness | | Witness | | Witness |
| Gen | | Gen | | Gen |
+----+----+ +----+----+ +-----+-----+
| | |
+--------+--------+--------+--------+
| |
+-------v-------+ +-----v--------+
| ProofEnv | | FastTermArena|
| (ruvector- | | (bump alloc |
| verified) | | + dedup) |
+-------+-------+ +-----+--------+
| |
+-------v-----------------v--------+
| Gated Proof Router |
| Reflex | Standard | Deep |
| <10ns | <1us | <100us |
+------------------+---------------+
|
+--------v--------+
| Proof |
| Attestation |
| (82 bytes) |
+-----------------+
Verification Coverage:
Graph Construction Message Passing Attention Weights
+---+---+---+ +---+---+ +---+---+---+
|dim|deg|con| proved |typ|agg| proved |eps|sym|pos| proved
+---+---+---+ +---+---+ +---+---+---+
dim = dimension typ = type safety eps = robustness
deg = degree bounds agg = commutativity sym = symmetry
con = connectivity pos = positivity
use ruvector_verified::{
ProofEnvironment, ProofAttestation, VerifiedOp, VerifiedStage,
};
#[cfg(feature = "fast-arena")]
use ruvector_verified::fast_arena::FastTermArena;
#[cfg(feature = "gated-proofs")]
use ruvector_verified::gated::{route_proof, ProofKind, ProofTier, verify_tiered};
/// A graph with proof-carrying operations.
///
/// Every structural modification produces a proof that invariants hold.
/// Invariants are registered at construction time and checked incrementally.
pub struct VerifiedGraph<V, E> {
/// Node data indexed by node ID
nodes: Vec<V>,
/// Adjacency list with edge data
adjacency: Vec<Vec<(usize, E)>>,
/// Registered invariants to maintain
invariants: Vec<GraphInvariant>,
/// Proof environment for constructing and caching proofs
env: ProofEnvironment,
/// Fast term arena for high-throughput proof construction
#[cfg(feature = "fast-arena")]
arena: FastTermArena,
/// Proof certificates for graph operations
certificates: Vec<GraphCertificate>,
}
/// Graph invariants that must be maintained across operations.
#[derive(Debug, Clone)]
pub enum GraphInvariant {
/// All node feature vectors have dimension d
UniformDimension(u32),
/// Maximum node degree
MaxDegree(usize),
/// Graph remains connected (single component)
Connected,
/// No self-loops
NoSelfLoops,
/// Edge weights are non-negative
NonNegativeWeights,
/// Total edge weight is conserved (within epsilon)
WeightConservation { total: f32, epsilon: f32 },
/// Node count within bounds
NodeCountBounds { min: usize, max: usize },
/// Custom invariant with proof obligation
Custom { name: String, proof_kind: ProofKind },
}
/// A machine-checked certificate for a graph operation.
#[derive(Debug, Clone)]
pub struct GraphCertificate {
/// Operation that was verified
pub operation: GraphOperation,
/// Proof term IDs for each maintained invariant
pub invariant_proofs: Vec<u32>,
/// Proof tier used (from gated routing)
pub tier: ProofTier,
/// Compact attestation (82 bytes, serializable)
pub attestation: ProofAttestation,
/// Wall-clock verification time
pub verification_time_ns: u64,
}
/// Graph operations that produce proof certificates.
#[derive(Debug, Clone)]
pub enum GraphOperation {
/// Add a node with feature vector
AddNode { node_id: usize, dim: u32 },
/// Remove a node
RemoveNode { node_id: usize },
/// Add an edge with weight
AddEdge { src: usize, dst: usize, weight: f32 },
/// Remove an edge
RemoveEdge { src: usize, dst: usize },
/// Reweight an edge
ReweightEdge { src: usize, dst: usize, old_weight: f32, new_weight: f32 },
/// Update attention weights for a node
UpdateAttention { node_id: usize, new_weights: Vec<(usize, f32)> },
/// Batch operation
Batch { operations: Vec<GraphOperation> },
}
/// Verified message passing configuration.
///
/// Uses dependent types to ensure dimension safety at the type level.
/// The phantom type parameters encode the message dimensions.
pub struct VerifiedMessagePass<const D_IN: usize, const D_MSG: usize, const D_OUT: usize> {
/// Message function weights: D_IN -> D_MSG
message_weights: [[f32; D_MSG]; D_IN],
/// Aggregation function (must be commutative + associative)
aggregation: VerifiedAggregation,
/// Update function weights: D_IN + D_MSG -> D_OUT
update_weights: [[f32; D_OUT]; { D_IN + D_MSG }],
/// Proof that aggregation is commutative
commutativity_proof: u32,
/// Proof that dimensions are consistent
dim_proof: u32,
}
/// Aggregation functions with verified properties.
#[derive(Debug, Clone)]
pub enum VerifiedAggregation {
/// Sum aggregation (commutative, associative -- trivially provable)
Sum { commutativity_proof: u32 },
/// Mean aggregation (commutative -- proved via sum commutativity + division)
Mean { commutativity_proof: u32 },
/// Max aggregation (commutative, associative -- proved via total order)
Max { commutativity_proof: u32, associativity_proof: u32 },
/// Attention-weighted sum (commutative when weights are symmetric)
AttentionWeighted {
symmetry_proof: Option<u32>,
positivity_proof: u32,
normalization_proof: u32,
},
}
/// Adversarial robustness certificate for a GNN prediction.
#[derive(Debug, Clone)]
pub struct RobustnessCertificate {
/// The prediction being certified
pub prediction: Vec<f32>,
/// Perturbation budget (L_inf norm for node features)
pub epsilon_features: f32,
/// Perturbation budget (number of edge additions/deletions)
pub epsilon_structure: usize,
/// Certified lower bound on correct-class margin
pub certified_margin: f32,
/// Whether the prediction is certifiably robust
pub is_robust: bool,
/// Proof term IDs for the certification chain
pub proof_chain: Vec<u32>,
/// Attestation
pub attestation: ProofAttestation,
}
/// Training certificate for one gradient step.
#[derive(Debug, Clone)]
pub struct TrainingStepCertificate {
/// Epoch number
pub epoch: usize,
/// Step within epoch
pub step: usize,
/// Loss before this step
pub loss_before: f32,
/// Loss after this step
pub loss_after: f32,
/// Proof that loss decreased (or explanation if it increased)
pub loss_monotonicity: LossMonotonicity,
/// Proof that equivariance is preserved
pub equivariance_proof: Option<u32>,
/// Proof that conservation laws hold
pub conservation_proofs: Vec<(String, u32)>,
/// Attestation
pub attestation: ProofAttestation,
}
/// Loss monotonicity status for a training step.
#[derive(Debug, Clone)]
pub enum LossMonotonicity {
/// Loss decreased -- proof of decrease
Decreased { proof_id: u32, delta: f32 },
/// Loss increased within tolerance (e.g., due to stochastic minibatch)
IncreasedWithinTolerance { delta: f32, tolerance: f32 },
/// Loss increased beyond tolerance -- flagged for review
IncreasedBeyondTolerance { delta: f32, tolerance: f32 },
}impl<V, E> VerifiedGraph<V, E>
where
V: AsRef<[f32]>, // Node features accessible as float slice
E: Into<f32> + Copy, // Edge data convertible to weight
{
/// Add a node with verified invariant preservation.
///
/// Produces proofs for:
/// - Dimension correctness (UniformDimension)
/// - Node count bounds (NodeCountBounds)
/// - Self-loop absence (NoSelfLoops -- trivially true for new node)
pub fn verified_add_node(
&mut self,
features: V,
) -> Result<GraphCertificate, VerificationError> {
let node_id = self.nodes.len();
let dim = features.as_ref().len() as u32;
// Route proof obligation to cheapest tier
#[cfg(feature = "gated-proofs")]
let tier_decision = route_proof(
ProofKind::DimensionEquality {
expected: self.expected_dim(),
actual: dim,
},
&self.env,
);
let mut invariant_proofs = Vec::new();
// Check each invariant
for invariant in &self.invariants {
let proof_id = match invariant {
GraphInvariant::UniformDimension(expected) => {
ruvector_verified::prove_dim_eq(&mut self.env, *expected, dim)?
}
GraphInvariant::NodeCountBounds { min: _, max } => {
if node_id + 1 > *max {
return Err(VerificationError::InvariantViolation(
format!("node count {} exceeds max {}", node_id + 1, max)
));
}
self.env.alloc_term()
}
GraphInvariant::NoSelfLoops => {
// New node has no edges, so no self-loops. Trivial proof.
self.env.alloc_term()
}
// Other invariants are trivially maintained by AddNode
_ => self.env.alloc_term(),
};
invariant_proofs.push(proof_id);
}
// Perform the operation
self.nodes.push(features);
self.adjacency.push(Vec::new());
// Construct attestation
let attestation = ProofAttestation::new(
&self.env,
&invariant_proofs,
"AddNode",
);
let cert = GraphCertificate {
operation: GraphOperation::AddNode { node_id, dim },
invariant_proofs,
tier: ProofTier::Reflex,
attestation,
verification_time_ns: 0, // filled by caller
};
self.certificates.push(cert.clone());
self.env.stats.proofs_verified += 1;
Ok(cert)
}
/// Add an edge with verified invariant preservation.
///
/// Produces proofs for:
/// - No self-loops (src != dst)
/// - Max degree not exceeded
/// - Non-negative weight
/// - Weight conservation (if applicable)
pub fn verified_add_edge(
&mut self,
src: usize,
dst: usize,
edge_data: E,
) -> Result<GraphCertificate, VerificationError> {
let weight: f32 = edge_data.into();
let mut invariant_proofs = Vec::new();
for invariant in &self.invariants {
let proof_id = match invariant {
GraphInvariant::NoSelfLoops => {
if src == dst {
return Err(VerificationError::InvariantViolation(
format!("self-loop: {} -> {}", src, dst)
));
}
self.env.alloc_term()
}
GraphInvariant::MaxDegree(max) => {
let new_degree = self.adjacency[src].len() + 1;
if new_degree > *max {
return Err(VerificationError::InvariantViolation(
format!("degree {} exceeds max {}", new_degree, max)
));
}
self.env.alloc_term()
}
GraphInvariant::NonNegativeWeights => {
if weight < 0.0 {
return Err(VerificationError::InvariantViolation(
format!("negative weight: {}", weight)
));
}
self.env.alloc_term()
}
_ => self.env.alloc_term(),
};
invariant_proofs.push(proof_id);
}
// Perform the operation
self.adjacency[src].push((dst, edge_data));
self.adjacency[dst].push((src, edge_data));
let attestation = ProofAttestation::new(
&self.env,
&invariant_proofs,
"AddEdge",
);
let cert = GraphCertificate {
operation: GraphOperation::AddEdge { src, dst, weight },
invariant_proofs,
tier: ProofTier::Standard { max_fuel: 100 },
attestation,
verification_time_ns: 0,
};
self.certificates.push(cert.clone());
self.env.stats.proofs_verified += 1;
Ok(cert)
}
}/// Type-safe message passing with compile-time dimension checking.
///
/// The const generics D_IN, D_MSG, D_OUT enforce dimension compatibility
/// at compile time. No runtime dimension check is needed -- the Rust
/// type system prevents dimension mismatches.
impl<const D_IN: usize, const D_MSG: usize, const D_OUT: usize>
VerifiedMessagePass<D_IN, D_MSG, D_OUT>
{
/// Execute verified message passing on a graph.
///
/// For each node v:
/// 1. For each neighbor u: compute message m_uv = W_msg * h_u
/// 2. Aggregate: m_v = AGG({m_uv : u in N(v)})
/// 3. Update: h_v' = W_upd * [h_v || m_v]
///
/// Returns updated embeddings with proof certificates.
pub fn forward(
&self,
node_features: &[[f32; D_IN]],
adjacency: &[Vec<usize>],
env: &mut ProofEnvironment,
) -> Result<(Vec<[f32; D_OUT]>, MessagePassCertificate), VerificationError> {
let n = node_features.len();
let mut output = vec![[0.0f32; D_OUT]; n];
let mut aggregation_proofs = Vec::with_capacity(n);
for v in 0..n {
// Compute messages from all neighbors
let messages: Vec<[f32; D_MSG]> = adjacency[v].iter()
.map(|&u| self.compute_message(&node_features[u]))
.collect();
// Verified aggregation with commutativity proof
let (aggregated, agg_proof) = self.verified_aggregate(
&messages,
env,
)?;
aggregation_proofs.push(agg_proof);
// Update: concatenate node features with aggregated message
output[v] = self.compute_update(&node_features[v], &aggregated);
}
// Construct permutation invariance proof.
// The proof relies on aggregation commutativity:
// If AGG is commutative, then permuting neighbors does not
// change the result, so the entire layer is permutation-equivariant.
let perm_proof = self.prove_permutation_equivariance(env)?;
let cert = MessagePassCertificate {
num_nodes: n,
aggregation_proofs,
permutation_equivariance_proof: perm_proof,
dim_in: D_IN as u32,
dim_msg: D_MSG as u32,
dim_out: D_OUT as u32,
};
Ok((output, cert))
}
/// Compute message from a neighbor's features.
/// Dimension safety guaranteed by const generics: [f32; D_IN] -> [f32; D_MSG]
fn compute_message(&self, neighbor_features: &[f32; D_IN]) -> [f32; D_MSG] {
let mut msg = [0.0f32; D_MSG];
for j in 0..D_MSG {
for i in 0..D_IN {
msg[j] += self.message_weights[i][j] * neighbor_features[i];
}
}
msg
}
/// Verified aggregation with proof of commutativity.
fn verified_aggregate(
&self,
messages: &[[f32; D_MSG]],
env: &mut ProofEnvironment,
) -> Result<([f32; D_MSG], u32), VerificationError> {
if messages.is_empty() {
return Ok(([0.0f32; D_MSG], env.alloc_term()));
}
let result = match &self.aggregation {
VerifiedAggregation::Sum { commutativity_proof } => {
let mut sum = [0.0f32; D_MSG];
for msg in messages {
for j in 0..D_MSG {
sum[j] += msg[j];
}
}
(sum, *commutativity_proof)
}
VerifiedAggregation::Mean { commutativity_proof } => {
let mut sum = [0.0f32; D_MSG];
for msg in messages {
for j in 0..D_MSG {
sum[j] += msg[j];
}
}
let count = messages.len() as f32;
for j in 0..D_MSG {
sum[j] /= count;
}
(sum, *commutativity_proof)
}
VerifiedAggregation::Max { commutativity_proof, .. } => {
let mut max_val = [f32::NEG_INFINITY; D_MSG];
for msg in messages {
for j in 0..D_MSG {
if msg[j] > max_val[j] {
max_val[j] = msg[j];
}
}
}
(max_val, *commutativity_proof)
}
VerifiedAggregation::AttentionWeighted { positivity_proof, .. } => {
// For attention-weighted aggregation, weights must sum to 1
// and be non-negative. Proof is provided at construction.
let mut weighted = [0.0f32; D_MSG];
let uniform_weight = 1.0 / messages.len() as f32;
for msg in messages {
for j in 0..D_MSG {
weighted[j] += uniform_weight * msg[j];
}
}
(weighted, *positivity_proof)
}
};
Ok(result)
}
/// Prove permutation equivariance of the message passing layer.
///
/// The proof structure:
/// 1. AGG is commutative (by construction, proof stored in self)
/// 2. Commutative AGG => permuting neighbors does not change AGG output
/// 3. Same AGG output => same update output (deterministic function)
/// 4. Therefore, permuting node indices produces the same output
/// (up to the same permutation applied to the output)
fn prove_permutation_equivariance(
&self,
env: &mut ProofEnvironment,
) -> Result<u32, VerificationError> {
// The proof is a composition of the commutativity proof
// with the determinism of the update function.
let comm_proof = match &self.aggregation {
VerifiedAggregation::Sum { commutativity_proof } => *commutativity_proof,
VerifiedAggregation::Mean { commutativity_proof } => *commutativity_proof,
VerifiedAggregation::Max { commutativity_proof, .. } => *commutativity_proof,
VerifiedAggregation::AttentionWeighted { normalization_proof, .. } => {
*normalization_proof
}
};
// Compose: commutativity => permutation equivariance
let equivariance_proof = env.alloc_term();
env.stats.proofs_verified += 1;
Ok(equivariance_proof)
}
/// Compute update: [h_v || m_v] -> h_v'
fn compute_update(
&self,
node_features: &[f32; D_IN],
aggregated: &[f32; D_MSG],
) -> [f32; D_OUT] {
let mut out = [0.0f32; D_OUT];
for k in 0..D_OUT {
// First D_IN weights apply to node features
for i in 0..D_IN {
out[k] += self.update_weights[i][k] * node_features[i];
}
// Next D_MSG weights apply to aggregated message
for j in 0..D_MSG {
out[k] += self.update_weights[D_IN + j][k] * aggregated[j];
}
}
out
}
}
/// Certificate for a message passing operation.
#[derive(Debug, Clone)]
pub struct MessagePassCertificate {
pub num_nodes: usize,
pub aggregation_proofs: Vec<u32>,
pub permutation_equivariance_proof: u32,
pub dim_in: u32,
pub dim_msg: u32,
pub dim_out: u32,
}/// Interval Bound Propagation (IBP) for certified GNN robustness.
///
/// Propagates interval bounds [lower, upper] through the GNN layers.
/// If the certified margin is positive (correct class score - max other
/// class score > 0 for all points in the interval), the prediction
/// is certifiably robust.
pub struct IntervalBoundCertifier {
/// Feature perturbation budget (L_inf)
epsilon_features: f32,
/// Structural perturbation budget (edge additions/deletions)
epsilon_structure: usize,
}
impl IntervalBoundCertifier {
/// Certify a GNN prediction under feature perturbation.
///
/// For each layer, propagate interval bounds:
/// [l_out, u_out] = W_pos * [l_in, u_in] + W_neg * [u_in, l_in] + b
/// where W_pos = max(W, 0), W_neg = min(W, 0).
///
/// The final interval gives guaranteed bounds on the output.
pub fn certify_prediction<const D: usize>(
&self,
node_features: &[f32; D],
layer_weights: &[Vec<Vec<f32>>],
adjacency: &[Vec<usize>],
node_idx: usize,
env: &mut ProofEnvironment,
) -> Result<RobustnessCertificate, VerificationError> {
// Initialize intervals from epsilon-ball around input
let mut lower = [0.0f32; D];
let mut upper = [0.0f32; D];
for i in 0..D {
lower[i] = node_features[i] - self.epsilon_features;
upper[i] = node_features[i] + self.epsilon_features;
}
let mut proof_chain = Vec::new();
// Propagate through each layer
for (layer_idx, weights) in layer_weights.iter().enumerate() {
let (new_lower, new_upper, proof) = self.propagate_interval_layer(
&lower, &upper,
weights,
env,
)?;
// Truncate to current dimension (simplified for pseudocode)
for i in 0..D.min(new_lower.len()) {
lower[i] = new_lower[i];
upper[i] = new_upper[i];
}
proof_chain.push(proof);
}
// Compute certified margin
// For classification: margin = min_score[correct] - max_score[other]
let prediction: Vec<f32> = lower.iter()
.zip(upper.iter())
.map(|(&l, &u)| (l + u) / 2.0)
.collect();
let correct_class = prediction.iter()
.enumerate()
.max_by(|(_, a), (_, b)| a.partial_cmp(b).unwrap())
.map(|(i, _)| i)
.unwrap_or(0);
let correct_lower = lower[correct_class];
let max_other_upper = upper.iter()
.enumerate()
.filter(|(i, _)| *i != correct_class)
.map(|(_, &u)| u)
.fold(f32::NEG_INFINITY, f32::max);
let certified_margin = correct_lower - max_other_upper;
// Construct robustness proof
let robustness_proof = env.alloc_term();
env.stats.proofs_verified += 1;
proof_chain.push(robustness_proof);
let attestation = ProofAttestation::new(
&self.env_ref(env),
&proof_chain,
"RobustnessCertificate",
);
Ok(RobustnessCertificate {
prediction,
epsilon_features: self.epsilon_features,
epsilon_structure: self.epsilon_structure,
certified_margin,
is_robust: certified_margin > 0.0,
proof_chain,
attestation,
})
}
/// Propagate intervals through one linear layer.
///
/// Uses the DeepPoly/IBP decomposition:
/// For W = W_pos + W_neg (positive and negative parts):
/// lower_out = W_pos * lower_in + W_neg * upper_in + bias
/// upper_out = W_pos * upper_in + W_neg * lower_in + bias
fn propagate_interval_layer(
&self,
lower: &[f32],
upper: &[f32],
weights: &[Vec<f32>],
env: &mut ProofEnvironment,
) -> Result<(Vec<f32>, Vec<f32>, u32), VerificationError> {
let out_dim = weights.len();
let mut new_lower = vec![0.0f32; out_dim];
let mut new_upper = vec![0.0f32; out_dim];
for j in 0..out_dim {
for (i, &w) in weights[j].iter().enumerate() {
if i >= lower.len() { break; }
if w >= 0.0 {
new_lower[j] += w * lower[i];
new_upper[j] += w * upper[i];
} else {
new_lower[j] += w * upper[i];
new_upper[j] += w * lower[i];
}
}
}
let proof = env.alloc_term();
Ok((new_lower, new_upper, proof))
}
}/// A training loop where each gradient step produces a certificate.
pub struct VerifiedTrainer {
/// Learning rate
lr: f32,
/// Loss tolerance for monotonicity checking
loss_tolerance: f32,
/// Conservation laws to verify
conservation_laws: Vec<ConservationLaw>,
/// Accumulated certificates
certificates: Vec<TrainingStepCertificate>,
}
/// A conservation law that must hold across gradient updates.
#[derive(Debug, Clone)]
pub struct ConservationLaw {
/// Human-readable name
pub name: String,
/// Function to compute the conserved quantity
pub compute: ConservedQuantity,
/// Tolerance for floating-point drift
pub tolerance: f32,
}
/// Types of conserved quantities in GNN training.
#[derive(Debug, Clone)]
pub enum ConservedQuantity {
/// Total message mass: sum of all messages in a layer
TotalMessageMass,
/// Attention weight normalization: sum of attention weights per node = 1
AttentionNormalization,
/// Weight matrix orthogonality: W^T * W ~ I
WeightOrthogonality { tolerance: f32 },
}
impl VerifiedTrainer {
/// Execute one verified training step.
///
/// 1. Compute loss
/// 2. Compute gradients
/// 3. Apply gradient update
/// 4. Verify conservation laws
/// 5. Check loss monotonicity
/// 6. Produce certificate
pub fn verified_step(
&mut self,
weights: &mut Vec<Vec<f32>>,
loss_before: f32,
gradients: &[Vec<f32>],
env: &mut ProofEnvironment,
epoch: usize,
step: usize,
) -> Result<TrainingStepCertificate, VerificationError> {
// Snapshot conserved quantities before update
let quantities_before: Vec<f32> = self.conservation_laws.iter()
.map(|law| self.compute_quantity(&law.compute, weights))
.collect();
// Apply gradient update
for (w, g) in weights.iter_mut().zip(gradients.iter()) {
for (wi, gi) in w.iter_mut().zip(g.iter()) {
*wi -= self.lr * gi;
}
}
// Compute new loss (caller provides via callback in real implementation)
let loss_after = loss_before * 0.99; // placeholder: real impl calls forward pass
// Verify conservation laws
let mut conservation_proofs = Vec::new();
for (i, law) in self.conservation_laws.iter().enumerate() {
let quantity_after = self.compute_quantity(&law.compute, weights);
let drift = (quantity_after - quantities_before[i]).abs();
if drift > law.tolerance {
return Err(VerificationError::InvariantViolation(format!(
"conservation law '{}' violated: drift {} > tolerance {}",
law.name, drift, law.tolerance,
)));
}
let proof_id = env.alloc_term();
env.stats.proofs_verified += 1;
conservation_proofs.push((law.name.clone(), proof_id));
}
// Check loss monotonicity
let loss_delta = loss_after - loss_before;
let loss_monotonicity = if loss_delta <= 0.0 {
LossMonotonicity::Decreased {
proof_id: env.alloc_term(),
delta: loss_delta.abs(),
}
} else if loss_delta <= self.loss_tolerance {
LossMonotonicity::IncreasedWithinTolerance {
delta: loss_delta,
tolerance: self.loss_tolerance,
}
} else {
LossMonotonicity::IncreasedBeyondTolerance {
delta: loss_delta,
tolerance: self.loss_tolerance,
}
};
let attestation = ProofAttestation::new_training(
env,
epoch,
step,
loss_after,
);
let cert = TrainingStepCertificate {
epoch,
step,
loss_before,
loss_after,
loss_monotonicity,
equivariance_proof: None, // computed separately if needed
conservation_proofs,
attestation,
};
self.certificates.push(cert.clone());
Ok(cert)
}
/// Compute a conserved quantity from the current weights.
fn compute_quantity(&self, quantity: &ConservedQuantity, weights: &[Vec<f32>]) -> f32 {
match quantity {
ConservedQuantity::TotalMessageMass => {
weights.iter().flat_map(|w| w.iter()).sum()
}
ConservedQuantity::AttentionNormalization => {
// Check that each row sums to ~1
let mut max_deviation = 0.0f32;
for row in weights {
let sum: f32 = row.iter().sum();
max_deviation = max_deviation.max((sum - 1.0).abs());
}
max_deviation
}
ConservedQuantity::WeightOrthogonality { tolerance: _ } => {
// Compute ||W^T * W - I||_F (Frobenius norm)
// Simplified: compute max diagonal deviation
let n = weights.len().min(weights.first().map_or(0, |r| r.len()));
let mut deviation = 0.0f32;
for i in 0..n {
for j in 0..n {
let dot: f32 = weights.iter()
.map(|row| {
let a = if i < row.len() { row[i] } else { 0.0 };
let b = if j < row.len() { row[j] } else { 0.0 };
a * b
})
.sum();
let target = if i == j { 1.0 } else { 0.0 };
deviation += (dot - target).powi(2);
}
}
deviation.sqrt()
}
}
}
}/// Proof-producing graph comparison.
///
/// Given two graphs G1 and G2, either produces a verified isomorphism
/// mapping or a proof that no isomorphism exists.
pub struct VerifiedIsomorphism;
impl VerifiedIsomorphism {
/// Attempt to find and prove a graph isomorphism.
///
/// Uses the Weisfeiler-Leman (WL) color refinement test as a
/// necessary condition. If WL distinguishes the graphs, produce
/// a distinguishing proof. If WL does not distinguish them,
/// attempt to construct an explicit isomorphism via backtracking.
pub fn check_isomorphism(
adj1: &[Vec<usize>],
adj2: &[Vec<usize>],
env: &mut ProofEnvironment,
) -> IsomorphismResult {
let n1 = adj1.len();
let n2 = adj2.len();
// Quick check: different sizes cannot be isomorphic
if n1 != n2 {
let proof_id = env.alloc_term();
return IsomorphismResult::NotIsomorphic {
reason: format!("different node counts: {} vs {}", n1, n2),
proof_id,
};
}
// Quick check: different degree sequences
let mut degrees1: Vec<usize> = adj1.iter().map(|a| a.len()).collect();
let mut degrees2: Vec<usize> = adj2.iter().map(|a| a.len()).collect();
degrees1.sort_unstable();
degrees2.sort_unstable();
if degrees1 != degrees2 {
let proof_id = env.alloc_term();
return IsomorphismResult::NotIsomorphic {
reason: "different degree sequences".into(),
proof_id,
};
}
// WL color refinement (1-WL)
let (colors1, colors2, wl_rounds) = Self::wl_refine(adj1, adj2);
if colors1 != colors2 {
let proof_id = env.alloc_term();
return IsomorphismResult::NotIsomorphic {
reason: format!("WL distinguished after {} rounds", wl_rounds),
proof_id,
};
}
// WL did not distinguish -- attempt explicit isomorphism
// (Simplified: in production, use VF2 or similar with proof witness)
if let Some(mapping) = Self::find_mapping(adj1, adj2) {
let proof_id = env.alloc_term();
env.stats.proofs_verified += 1;
IsomorphismResult::Isomorphic {
mapping,
proof_id,
}
} else {
let proof_id = env.alloc_term();
IsomorphismResult::NotIsomorphic {
reason: "no valid mapping found".into(),
proof_id,
}
}
}
/// Weisfeiler-Leman 1-dimensional color refinement.
fn wl_refine(
adj1: &[Vec<usize>],
adj2: &[Vec<usize>],
) -> (Vec<u64>, Vec<u64>, usize) {
let n = adj1.len();
let mut colors1 = vec![0u64; n];
let mut colors2 = vec![0u64; n];
// Initialize colors from degree
for i in 0..n {
colors1[i] = adj1[i].len() as u64;
colors2[i] = adj2[i].len() as u64;
}
let mut rounds = 0;
loop {
rounds += 1;
let new1 = Self::wl_step(&colors1, adj1);
let new2 = Self::wl_step(&colors2, adj2);
if new1 == colors1 && new2 == colors2 {
break; // Stable coloring
}
colors1 = new1;
colors2 = new2;
if rounds > n { break; } // WL converges in at most n rounds
}
// Sort for comparison
let mut sorted1 = colors1.clone();
let mut sorted2 = colors2.clone();
sorted1.sort_unstable();
sorted2.sort_unstable();
(sorted1, sorted2, rounds)
}
/// One step of WL refinement: new_color = hash(old_color, sorted neighbor colors)
fn wl_step(colors: &[u64], adj: &[Vec<usize>]) -> Vec<u64> {
colors.iter().enumerate().map(|(i, &c)| {
let mut neighbor_colors: Vec<u64> = adj[i].iter()
.map(|&j| colors[j])
.collect();
neighbor_colors.sort_unstable();
// Hash: combine self color with sorted neighbor colors
let mut h = c.wrapping_mul(0x517cc1b727220a95);
for &nc in &neighbor_colors {
h = h.wrapping_mul(0x100000001b3) ^ nc;
}
h
}).collect()
}
/// Attempt to find an explicit isomorphism mapping (simplified).
fn find_mapping(adj1: &[Vec<usize>], adj2: &[Vec<usize>]) -> Option<Vec<usize>> {
let n = adj1.len();
if n == 0 { return Some(Vec::new()); }
// Simplified identity check for same-structure graphs
let mut mapping = vec![0usize; n];
for i in 0..n { mapping[i] = i; }
// Verify the identity mapping
for i in 0..n {
let neighbors1: std::collections::HashSet<usize> =
adj1[i].iter().cloned().collect();
let mapped_neighbors: std::collections::HashSet<usize> =
adj2[mapping[i]].iter().map(|&j| mapping[j]).collect();
if neighbors1 != mapped_neighbors {
return None;
}
}
Some(mapping)
}
}
/// Result of a verified isomorphism check.
#[derive(Debug)]
pub enum IsomorphismResult {
/// Graphs are isomorphic, with verified mapping and proof
Isomorphic {
mapping: Vec<usize>,
proof_id: u32,
},
/// Graphs are not isomorphic, with distinguishing proof
NotIsomorphic {
reason: String,
proof_id: u32,
},
}We extend ruvector-verified's lean-agentic type theory with graph-specific constructions. The core types from invariants.rs -- Nat, RuVec, Eq, HnswIndex, PipelineStage -- are extended with:
-- Graph type: indexed by node count and feature dimension
Graph : Nat -> Nat -> Type
-- Node in a graph: indexed by graph and node ID
Node : Graph n d -> Fin n -> Type
-- Edge in a graph: between two nodes
Edge : Graph n d -> Fin n -> Fin n -> Type
-- Message type: from source dimension to message dimension
Message : Nat -> Nat -> Type
-- Aggregation with commutativity proof
CommAgg : (d : Nat) -> (agg : Message d d -> Message d d -> Message d d) ->
(comm : forall x y, Eq (agg x y) (agg y x)) -> Type
-- GNN Layer: typed input and output dimensions
GNNLayer : Nat -> Nat -> Type
-- Composition: verified pipeline stage composition
compose_gnn : GNNLayer d1 d2 -> GNNLayer d2 d3 -> GNNLayer d1 d3
These types correspond to the Rust const generic parameters (D_IN, D_MSG, D_OUT) and the VerifiedStage<A, B> composition from ruvector-verified/pipeline.rs. The key advantage is that dimension mismatches become compile-time errors rather than runtime crashes.
Permutation equivariance is the fundamental property of GNNs: applying a permutation to the input nodes applies the same permutation to the output. In dependent type theory:
-- Permutation equivariance theorem
equivariant : (f : GNNLayer d_in d_out) ->
(G : Graph n d_in) ->
(sigma : Perm n) ->
Eq (f (permute sigma G)) (permute sigma (f G))
The proof proceeds by induction on the layer structure:
- Message computation is per-edge, so permuting nodes permutes messages.
- Aggregation is commutative (proved by
CommAgg), so permuting the message multiset does not change the aggregated result. - Update is per-node, so permuting nodes permutes updates.
This proof is constructed once per aggregation type and reused for every forward pass, corresponding to the cached commutativity_proof in VerifiedAggregation.
-
ruvector-verified: This is the primary integration point. The existingProofEnvironment,FastTermArena, gated proof routing (Reflex/Standard/Deeptiers),VerifiedStage<A, B>composition, dimension proofs (prove_dim_eq), andProofAttestationare directly extended for GNN verification. Theinvariants.rssymbol table gains graph-specific declarations (Graph,Node,Edge,CommAgg). Thepipeline.rscompose_stagesfunction generalizes tocompose_gnnfor GNN layer composition. -
ruvector-gnn: The core GNN crate (layer.rs,training.rs,ewc.rs,search.rs) gains verified wrappers. EachLayer::forwardcall can optionally produce aMessagePassCertificate. Thetraining.rsmodule gains aVerifiedTrainerthat wraps gradient steps with conservation law checking. EWC (ewc.rs) integrates naturally: the Fisher information matrix itself becomes a verified invariant that must be preserved. -
ruvector-attention: The 18+ attention mechanisms gain robustness certification. TheIntervalBoundCertifierpropagates bounds through attention weight computation. Thetopology/gated_attention.rsmodule's gating decisions become proof obligations routed through the gated proof router. -
ruvector-graph: Graph construction and modification operations gain verified wrappers. TheVerifiedGraph<V, E>struct wraps the existing graph with invariant tracking and proof generation. -
ruvector-mincut-gated-transformer: The energy gate (energy_gate.rs), speculative decoding (speculative.rs), and Mamba SSM (mamba.rs) gain verified execution paths. The gated proof router's tier system mirrors the mincut-gated-transformer'sGateController-- both route computation to the cheapest sufficient tier. -
ruvector-coherence: Spectral coherence metrics (spectral.rs) become verified invariants. The coherence score is a conserved quantity that must remain within bounds across graph operations, verified by theConservationLawframework.
ruvector-verified/src/
graph_types.rs # Graph, Node, Edge type constructors
message_pass.rs # Verified message passing with dimension proofs
robustness.rs # Interval bound propagation certifier
training.rs # Verified training loop with certificates
isomorphism.rs # Proof-producing graph comparison
conservation.rs # Conservation law verification
ruvector-gnn/src/
verified_layer.rs # Verified wrapper for GNN layers
verified_train.rs # Integration with ruvector-verified trainer
By 2030, every production GNN training run produces a complete proof certificate chain. Each epoch's certificate attests to loss monotonicity, conservation law preservation, and equivariance maintenance. Key milestones:
- Per-Epoch Certificates: Each training epoch produces a compact proof certificate (< 1KB) that can be independently verified in < 1ms. The certificate chain for an entire training run is < 1MB.
- Verified Hyperparameter Selection: The proof system extends to hyperparameter choices, certifying that learning rate schedules satisfy convergence conditions for the loss landscape's smoothness class.
- Proof-Carrying Model Cards: Trained GNN models ship with machine-checked proof certificates documenting their verified properties -- equivariance, robustness bounds, conservation laws, and training convergence.
- Verified Distributed Training: Proof certificates for gradient aggregation across distributed workers, ensuring that model averaging preserves invariants despite communication delays and floating-point non-associativity.
By 2036, formally verified graph transformers are deployed in systems where correctness is non-negotiable:
- Autonomous Vehicles: GNN-based perception and planning modules carry proof certificates that predictions are stable under sensor noise within calibrated epsilon bounds. Regulatory approval (SAE Level 4+) requires verified perception.
- Medical Diagnostics: Drug interaction prediction GNNs carry proof certificates that molecular graph operations preserve chemical validity (valence constraints, aromaticity conservation). The FDA requires proof-carrying AI for diagnostic approval.
- Financial Infrastructure: Fraud detection GNNs produce verified graph isomorphism certificates for transaction pattern matching. False positive rates are provably bounded, enabling deployment in real-time settlement systems.
- Critical Infrastructure: Power grid GNNs carry proofs that load balancing recommendations satisfy stability constraints (Lyapunov conditions), preventing cascading failures.
- Proof-Carrying Inference as a Service: Cloud GNN inference endpoints return predictions bundled with compact proof attestations (82 bytes, from
ruvector-verified) that clients verify locally in microseconds.
- Extend
ruvector-verified/invariants.rswith graph-specific type declarations - Implement
VerifiedGraph<V, E>with invariant tracking - Add proof-carrying
AddNodeandAddEdgeoperations - Unit tests for invariant verification
- Implement
VerifiedMessagePasswith const generic dimension checking - Add
VerifiedAggregationwith commutativity proofs - Prove permutation equivariance from aggregation commutativity
- Integration tests with
ruvector-gnnlayers
- Implement
IntervalBoundCertifierwith IBP propagation - Add structural perturbation bounds (edge addition/deletion)
- Generate
RobustnessCertificatewith proof attestations - Benchmark certification overhead on standard GNN benchmarks
- Implement
VerifiedTrainerwith per-step certificates - Add conservation law framework (
ConservationLaw,ConservedQuantity) - Implement loss monotonicity checking with tolerance bands
- Integration with
ruvector-gnn/training.rs
- End-to-end verified GNN pipeline: construction -> training -> inference
- Benchmark proof overhead (target: < 5% for Reflex tier, < 20% for Deep tier)
- Generate proof certificate chain for complete training run
- Document verified GNN API and proof certificate format
| Metric | Target |
|---|---|
| Proof Generation Overhead (Reflex tier) | < 10ns per operation |
| Proof Generation Overhead (Standard tier) | < 1us per operation |
| Proof Generation Overhead (Deep tier) | < 100us per operation |
| Proof Verification Time | < 1ms per certificate |
| Robustness Certificate Generation | < 50ms per prediction |
| Training Certificate Size | < 1KB per epoch |
| Dimension Mismatch Bugs | 0 (compile-time elimination) |
| Conservation Law Drift | < 1e-6 per training step |
| Proof Cache Hit Rate | > 80% for repeated operations |
-
Risk: Proof Overhead Slows Training
- Mitigation: Gated proof routing (
ruvector-verified/gated.rs) directs trivial proofs to the Reflex tier (< 10ns). Only complex obligations use the Deep tier. Average overhead target: < 5%.
- Mitigation: Gated proof routing (
-
Risk: Floating-Point Non-Determinism Breaks Proofs
- Mitigation: Conservation laws use tolerance bands (not exact equality). The proof system certifies "within epsilon" rather than "exactly equal."
-
Risk: IBP Bounds Too Loose for Practical Certification
- Mitigation: Layer-wise interval tightening via linear relaxation (CROWN/alpha-CROWN). Trade certification time for tighter bounds.
-
Risk: Proof Certificates Grow Too Large
- Mitigation: 82-byte attestations from
ruvector-verifiedprovide compact summaries. Full proof terms are stored inFastTermArenaand can be reconstructed from attestations.
- Mitigation: 82-byte attestations from
-
Risk: Limited Coverage of Real GNN Architectures
- Mitigation: Start with verified sum/mean/max aggregation (covers GCN, GraphSAGE, GIN). Extend to attention-weighted aggregation (GAT) in Phase 3. Custom aggregations require custom commutativity proofs.