diff --git a/formal/Drift.v b/formal/Drift.v
index 59b5050..d9730be 100644
--- a/formal/Drift.v
+++ b/formal/Drift.v
@@ -27,6 +27,15 @@
 
 Require Import Coq.Init.Logic.
 
+(* Keep Print Assumptions output on one line per axiom: the CI and Justfile
+   guards match /^name :/ with awk, and Coq's default ~78-column wrap would
+   split a longer axiom type across lines and silently escape the check. *)
+Set Printing Width 400.
+
+(* Keep Print Assumptions output on one line per axiom: the CI and Justfile
+   guards match /^name :/ with awk, and Coq's default ~78-column wrap would
+   split a longer axiom type across lines and silently escape the check. *)
+
 (** ** Domain *)
 
 (** Opaque score type. In the Rust source this is [f64]. *)
diff --git a/formal/Justfile b/formal/Justfile
index 9876c55..bc4eef6 100644
--- a/formal/Justfile
+++ b/formal/Justfile
@@ -17,31 +17,31 @@ all: provenance drift transaction planner wal normalizer vcl planner-semantic oc
 # --- Per-module compile recipes -------------------------------------------
 
 provenance:
-    {{COQC}} -q Provenance.v | tee Provenance.out
+    {{COQC}} -q Provenance.v > Provenance.out
 
 drift:
-    {{COQC}} -q Drift.v | tee Drift.out
+    {{COQC}} -q Drift.v > Drift.out
 
 transaction:
-    {{COQC}} -q Transaction.v | tee Transaction.out
+    {{COQC}} -q Transaction.v > Transaction.out
 
 planner:
-    {{COQC}} -q Planner.v | tee Planner.out
+    {{COQC}} -q Planner.v > Planner.out
 
 wal:
-    {{COQC}} -q WAL.v | tee WAL.out
+    {{COQC}} -q WAL.v > WAL.out
 
 normalizer:
-    {{COQC}} -q Normalizer.v | tee Normalizer.out
+    {{COQC}} -q Normalizer.v > Normalizer.out
 
 vcl:
-    {{COQC}} -q VCL.v | tee VCL.out
+    {{COQC}} -q VCL.v > VCL.out
 
 planner-semantic:
-    {{COQC}} -q PlannerSemantic.v | tee PlannerSemantic.out
+    {{COQC}} -q PlannerSemantic.v > PlannerSemantic.out
 
 octad:
-    {{COQC}} -q Octad.v | tee Octad.out
+    {{COQC}} -q Octad.v > Octad.out
 
 # --- Whitelist guards -----------------------------------------------------
 # Each module declares its own set of Parameters/Axioms; the guard greps
diff --git a/formal/Normalizer.v b/formal/Normalizer.v
index f5c56f4..b86c7d6 100644
--- a/formal/Normalizer.v
+++ b/formal/Normalizer.v
@@ -47,6 +47,15 @@
 Require Import Coq.Logic.FunctionalExtensionality.
 Require Import Coq.Bool.Bool.
 
+(* Keep Print Assumptions output on one line per axiom: the CI and Justfile
+   guards match /^name :/ with awk, and Coq's default ~78-column wrap would
+   split a longer axiom type across lines and silently escape the check. *)
+Set Printing Width 400.
+
+(* Keep Print Assumptions output on one line per axiom: the CI and Justfile
+   guards match /^name :/ with awk, and Coq's default ~78-column wrap would
+   split a longer axiom type across lines and silently escape the check. *)
+
 (** ** Domain *)
 
 Parameter modality : Type.
diff --git a/formal/Octad.v b/formal/Octad.v
index 594081f..cf4154f 100644
--- a/formal/Octad.v
+++ b/formal/Octad.v
@@ -89,6 +89,15 @@
 Require Import Coq.Lists.List.
 Require Import Coq.Bool.Bool.
 Require Import Coq.Logic.FunctionalExtensionality.
+
+(* Keep Print Assumptions output on one line per axiom: the CI and Justfile
+   guards match /^name :/ with awk, and Coq's default ~78-column wrap would
+   split a longer axiom type across lines and silently escape the check. *)
+Set Printing Width 400.
+
+(* Keep Print Assumptions output on one line per axiom: the CI and Justfile
+   guards match /^name :/ with awk, and Coq's default ~78-column wrap would
+   split a longer axiom type across lines and silently escape the check. *)
 Import ListNotations.
 
 (** ** [def:modset] — Modality Set
diff --git a/formal/Planner.v b/formal/Planner.v
index f58596d..093eb6a 100644
--- a/formal/Planner.v
+++ b/formal/Planner.v
@@ -32,6 +32,15 @@
 
 Require Import Coq.Lists.List.
 Require Import Coq.Sorting.Permutation.
+
+(* Keep Print Assumptions output on one line per axiom: the CI and Justfile
+   guards match /^name :/ with awk, and Coq's default ~78-column wrap would
+   split a longer axiom type across lines and silently escape the check. *)
+Set Printing Width 400.
+
+(* Keep Print Assumptions output on one line per axiom: the CI and Justfile
+   guards match /^name :/ with awk, and Coq's default ~78-column wrap would
+   split a longer axiom type across lines and silently escape the check. *)
 Import ListNotations.
 
 (** ** Domain *)
diff --git a/formal/PlannerSemantic.v b/formal/PlannerSemantic.v
index 0e9bf3d..81cf126 100644
--- a/formal/PlannerSemantic.v
+++ b/formal/PlannerSemantic.v
@@ -50,6 +50,15 @@
 
 Require Import Coq.Lists.List.
 Require Import Coq.Sorting.Permutation.
+
+(* Keep Print Assumptions output on one line per axiom: the CI and Justfile
+   guards match /^name :/ with awk, and Coq's default ~78-column wrap would
+   split a longer axiom type across lines and silently escape the check. *)
+Set Printing Width 400.
+
+(* Keep Print Assumptions output on one line per axiom: the CI and Justfile
+   guards match /^name :/ with awk, and Coq's default ~78-column wrap would
+   split a longer axiom type across lines and silently escape the check. *)
 Import ListNotations.
 
 (** ** Domain (reusing Planner.v abstractions) *)
diff --git a/formal/Provenance.v b/formal/Provenance.v
index 9f03886..8caaefd 100644
--- a/formal/Provenance.v
+++ b/formal/Provenance.v
@@ -35,6 +35,15 @@
 *)
 
 Require Import Coq.Lists.List.
+
+(* Keep Print Assumptions output on one line per axiom: the CI and Justfile
+   guards match /^name :/ with awk, and Coq's default ~78-column wrap would
+   split a longer axiom type across lines and silently escape the check. *)
+Set Printing Width 400.
+
+(* Keep Print Assumptions output on one line per axiom: the CI and Justfile
+   guards match /^name :/ with awk, and Coq's default ~78-column wrap would
+   split a longer axiom type across lines and silently escape the check. *)
 Import ListNotations.
 
 (** ** Domain *)
diff --git a/formal/Transaction.v b/formal/Transaction.v
index 3ce536c..b100dc6 100644
--- a/formal/Transaction.v
+++ b/formal/Transaction.v
@@ -38,6 +38,15 @@
 
 Require Import Coq.Init.Logic.
 
+(* Keep Print Assumptions output on one line per axiom: the CI and Justfile
+   guards match /^name :/ with awk, and Coq's default ~78-column wrap would
+   split a longer axiom type across lines and silently escape the check. *)
+Set Printing Width 400.
+
+(* Keep Print Assumptions output on one line per axiom: the CI and Justfile
+   guards match /^name :/ with awk, and Coq's default ~78-column wrap would
+   split a longer axiom type across lines and silently escape the check. *)
+
 (** ** Domain *)
 
 Inductive txn_state : Type :=
diff --git a/formal/VCL.v b/formal/VCL.v
index 21f4e7a..4530de9 100644
--- a/formal/VCL.v
+++ b/formal/VCL.v
@@ -43,6 +43,15 @@
 
 Require Import Coq.Init.Logic.
 
+(* Keep Print Assumptions output on one line per axiom: the CI and Justfile
+   guards match /^name :/ with awk, and Coq's default ~78-column wrap would
+   split a longer axiom type across lines and silently escape the check. *)
+Set Printing Width 400.
+
+(* Keep Print Assumptions output on one line per axiom: the CI and Justfile
+   guards match /^name :/ with awk, and Coq's default ~78-column wrap would
+   split a longer axiom type across lines and silently escape the check. *)
+
 (** ** Syntax *)
 
 Inductive ty : Type :=
diff --git a/formal/WAL.v b/formal/WAL.v
index 32f8c69..4df1c67 100644
--- a/formal/WAL.v
+++ b/formal/WAL.v
@@ -45,6 +45,15 @@
 
 Require Import Coq.Lists.List.
 Require Import Coq.Logic.FunctionalExtensionality.
+
+(* Keep Print Assumptions output on one line per axiom: the CI and Justfile
+   guards match /^name :/ with awk, and Coq's default ~78-column wrap would
+   split a longer axiom type across lines and silently escape the check. *)
+Set Printing Width 400.
+
+(* Keep Print Assumptions output on one line per axiom: the CI and Justfile
+   guards match /^name :/ with awk, and Coq's default ~78-column wrap would
+   split a longer axiom type across lines and silently escape the check. *)
 Import ListNotations.
 
 (** ** Domain *)