diff --git a/Makefile b/Makefile
index e4cc9658f0..03e7db0741 100644
--- a/Makefile
+++ b/Makefile
@@ -179,7 +179,8 @@ JAVA_EXTRA_ARGS_32  := $(JAVA_EXTRA_ARGS_ALL)
 
 OUTPUT_VOS := \
 	src/Fancy/Montgomery256.vo \
-	src/Fancy/Barrett256.vo
+	src/Fancy/Barrett256.vo \
+	src/UnsaturatedSolinasHeuristics/Tests.vo
 
 OUTPUT_PREOUTS := \
 	Crypto.Fancy.Montgomery256.Prod.MontRed256 \
@@ -189,7 +190,8 @@ OUTPUT_PREOUTS := \
 	Crypto.Fancy.Barrett256.Prod.MulMod \
 	Crypto.Fancy.Barrett256.prod_barrett_red256_correct \
 	Crypto.Fancy.Barrett256.prod_barrett_red256_correct.Assumptions \
-	Crypto.Fancy.Barrett256.barrett_red256
+	Crypto.Fancy.Barrett256.barrett_red256 \
+	Crypto.UnsaturatedSolinasHeuristics.Tests.get_possible_limbs
 
 CHECK_OUTPUTS := $(addprefix check-,$(OUTPUT_PREOUTS))
 ACCEPT_OUTPUTS := $(addprefix accept-,$(OUTPUT_PREOUTS))
diff --git a/_CoqProject b/_CoqProject
index 7eb971e2fa..2bd3890e87 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -159,6 +159,7 @@ src/Stringification/IR.v
 src/Stringification/Java.v
 src/Stringification/Language.v
 src/Stringification/Rust.v
+src/UnsaturatedSolinasHeuristics/Tests.v
 src/Util/AdditionChainExponentiation.v
 src/Util/Arg.v
 src/Util/AutoRewrite.v
diff --git a/output-tests/Crypto.UnsaturatedSolinasHeuristics.Tests.get_possible_limbs.expected b/output-tests/Crypto.UnsaturatedSolinasHeuristics.Tests.get_possible_limbs.expected
new file mode 100644
index 0000000000..e49ae54212
--- /dev/null
+++ b/output-tests/Crypto.UnsaturatedSolinasHeuristics.Tests.get_possible_limbs.expected
@@ -0,0 +1,62 @@
+possible_limbs = 
+Some
+  [("2^127 - 1", [(64, [3]); (32, [5; 6; 7])]);
+  ("2^129 - 25", [(64, [3; 4; 5]); (32, [5; 6; 7; 8; 9])]);
+  ("2^130 - 5", [(64, [3; 4; 5]); (32, [5; 6; 7; 8; 9])]);
+  ("2^137 - 13", [(64, [3; 4; 5]); (32, [6; 7; 8; 9])]);
+  ("2^140 - 27", [(64, [3; 4; 5]); (32, [6; 7; 8; 9])]);
+  ("2^141 - 9", [(64, [3; 4; 5]); (32, [6; 7; 8; 9])]);
+  ("2^150 - 5", [(64, [3; 4; 5]); (32, [6; 7; 8; 9])]);
+  ("2^150 - 3", [(64, [3; 4; 5]); (32, [6; 7; 8; 9])]);
+  ("2^152 - 17", [(64, [3; 4; 5]); (32, [6; 7; 8; 9])]);
+  ("2^158 - 15", [(64, [3; 4; 5]); (32, [6; 7; 8; 9])]);
+  ("2^165 - 25", [(64, [3; 4; 5]); (32, [7; 8; 9; 10; 11])]);
+  ("2^166 - 5", [(64, [3; 4; 5]); (32, [7; 8; 9; 10; 11])]);
+  ("2^171 - 19", [(64, [3; 4; 5]); (32, [7; 8; 9; 10; 11])]);
+  ("2^174 - 17", [(64, [3; 4; 5]); (32, [7; 8; 9; 10; 11])]);
+  ("2^174 - 3", [(64, [3; 4; 5]); (32, [7; 8; 9; 10; 11])]);
+  ("2^189 - 25", [(64, [4; 5]); (32, [8; 9; 10; 11])]);
+  ("2^190 - 11", [(64, [4; 5]); (32, [8; 9; 10; 11])]);
+  ("2^191 - 19", [(64, [4; 5]); (32, [8; 9; 10; 11])]);
+  ("2^194 - 33", [(64, [4; 5; 6; 7]); (32, [8; 9; 10; 11; 12; 13])]);
+  ("2^196 - 15", [(64, [4; 5; 6; 7]); (32, [8; 9; 10; 11; 12; 13])]);
+  ("2^198 - 17", [(64, [4; 5; 6; 7]); (32, [8; 9; 10; 11; 12; 13])]);
+  ("2^206 - 5", [(64, [4; 5; 6; 7]); (32, [8; 9; 10; 11; 12; 13])]);
+  ("2^212 - 29", [(64, [4; 5; 6; 7]); (32, [9; 10; 11; 12; 13])]);
+  ("2^213 - 3", [(64, [4; 5; 6; 7]); (32, [8; 9; 10; 11; 12; 13])]);
+  ("2^221 - 3", [(64, [4; 5; 6; 7]); (32, [9; 10; 11; 12; 13])]);
+  ("2^222 - 117", [(64, [4; 5; 6; 7]); (32, [9; 10; 11; 12; 13])]);
+  ("2^226 - 5", [(64, [4; 5; 6; 7]); (32, [9; 10; 11; 12; 13; 14; 15])]);
+  ("2^230 - 27", [(64, [4; 5; 6; 7]); (32, [9; 10; 11; 12; 13; 14; 15])]);
+  ("2^235 - 15", [(64, [4; 5; 6; 7]); (32, [9; 10; 11; 12; 13; 14; 15])]);
+  ("2^243 - 9", [(64, [5; 6; 7]); (32, [9; 10; 11; 12; 13; 14; 15])]);
+  ("2^251 - 9", [(64, [5; 6; 7]); (32, [10; 11; 12; 13; 14; 15])]);
+  ("2^255 - 765", [(64, [5; 6; 7]); (32, [11; 12; 13; 14; 15])]);
+  ("2^255 - 19", [(64, [5; 6; 7]); (32, [10; 11; 12; 13; 14; 15])]);
+  ("2^256 - 189", [(64, [5; 6; 7]); (32, [11; 12; 13; 14; 15])]);
+  ("2^266 - 3",
+  [(64, [5; 6; 7; 8; 9]); (32, [10; 11; 12; 13; 14; 15; 16; 17])]);
+  ("2^285 - 9", [(64, [5; 6; 7; 8; 9]); (32, [11; 12; 13; 14; 15; 16; 17])]);
+  ("2^291 - 19",
+  [(64, [5; 6; 7; 8; 9]); (32, [12; 13; 14; 15; 16; 17; 18; 19])]);
+  ("2^321 - 9",
+  [(64, [6; 7; 8; 9; 10; 11]); (32, [13; 14; 15; 16; 17; 18; 19; 20; 21])]);
+  ("2^336 - 17",
+  [(64, [6; 7; 8; 9; 10; 11]); (32, [13; 14; 15; 16; 17; 18; 19; 20; 21])]);
+  ("2^336 - 3",
+  [(64, [6; 7; 8; 9; 10; 11]); (32, [13; 14; 15; 16; 17; 18; 19; 20; 21])]);
+  ("2^338 - 15",
+  [(64, [6; 7; 8; 9; 10; 11]); (32, [13; 14; 15; 16; 17; 18; 19; 20; 21])]);
+  ("2^192 - 2^64 - 1", [(64, [4; 5]); (32, [9; 10; 11])]);
+  ("2^216 - 2^108 - 1", [(64, [4; 5; 6; 7]); (32, [8; 10; 11; 12; 13])]);
+  ("2^322 - 2^161 - 1",
+  [(64, [6; 7; 8; 9; 10; 11]); (32, [12; 14; 15; 16; 17; 18; 19; 20; 21])]);
+  ("2^205 - 45*2^198 - 1", [(64, []); (32, [])]);
+  ("2^224 - 2^96 + 1", [(64, [5; 6; 7]); (32, [10; 11; 12; 13])]);
+  ("2^256 - 2^224 + 2^192 + 2^96 - 1",
+  [(64, [5; 6; 7]); (32, [11; 12; 13; 14; 15])]);
+  ("2^256 - 2^32 - 977", [(64, [6; 7]); (32, [12; 13; 14; 15])]);
+  ("2^256 - 4294968273", [(64, [6; 7]); (32, [])]);
+  ("2^256 - 88*2^240 - 1", [(64, []); (32, [])]);
+  ("2^254 - 127*2^240 - 1", [(64, []); (32, [])])]
+     : option (list (string * list (nat * list nat)))
diff --git a/src/UnsaturatedSolinasHeuristics/Tests.v b/src/UnsaturatedSolinasHeuristics/Tests.v
new file mode 100644
index 0000000000..0c9ed739aa
--- /dev/null
+++ b/src/UnsaturatedSolinasHeuristics/Tests.v
@@ -0,0 +1,157 @@
+Require Import Coq.Strings.String.
+Require Import Coq.Lists.List.
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.Option.
+Require Import Crypto.UnsaturatedSolinasHeuristics.
+Require Import Crypto.Util.Strings.ParseArithmeticToTaps.
+Require Import Crypto.Util.OptionList.
+Import ListNotations.
+Import Coq.Lists.List.
+Local Open Scope option_scope.
+Local Open Scope string_scope.
+Local Open Scope list_scope.
+Local Open Scope nat_scope.
+Local Open Scope Z_scope.
+Local Open Scope core_scope.
+
+Definition single_tap_primes : list string :=
+  [
+    (* single-tap: *)
+
+    "2^127 - 1"; (* "kummer strikes back" *)
+  "2^129 - 25";
+  "2^130 - 5"; (* poly1305 *)
+  "2^137 - 13";
+  "2^140 - 27";
+  "2^141 - 9";
+  "2^150 - 5";
+  "2^150 - 3";
+  "2^152 - 17";
+  "2^158 - 15";
+  "2^165 - 25";
+  "2^166 - 5";
+  "2^171 - 19";
+  "2^174 - 17";
+  "2^174 - 3";
+  "2^189 - 25";
+  "2^190 - 11";
+  "2^191 - 19";
+  "2^194 - 33";
+  "2^196 - 15";
+  "2^198 - 17";
+  "2^206 - 5";
+  "2^212 - 29";
+  "2^213 - 3";
+  "2^221 - 3";
+  "2^222 - 117";
+  "2^226 - 5";
+  "2^230 - 27";
+  "2^235 - 15";
+  "2^243 - 9";
+  "2^251 - 9";
+  "2^255 - 765";
+  "2^255 - 19"; (* curve25519 *)
+  "2^256 - 189";
+  "2^266 - 3";
+  "2^285 - 9";
+  "2^291 - 19";
+  "2^321 - 9";
+  "2^336 - 17";
+  "2^336 - 3";
+  "2^338 - 15";
+  "2^369 - 25";
+  "2^379 - 19";
+  "2^382 - 105";
+  "2^383 - 421";
+  "2^383 - 187";
+  "2^383 - 31";
+  "2^384 - 317";
+  "2^389 - 21";
+  "2^401 - 31";
+  "2^413 - 21";
+  "2^414 - 17";
+  "2^444 - 17";
+  "2^452 - 3";
+  "2^468 - 17";
+  "2^488 - 17";
+  "2^489 - 21";
+  "2^495 - 31";
+  "2^511 - 481";
+  "2^511 - 187";
+  "2^512 - 569";
+  "2^521 - 1" (* p512 *)
+  ].
+
+Definition two_tap_golden_ratio_primes : list string :=
+  [
+
+    (* two taps, golden ratio: *)
+
+    "2^192 - 2^64 - 1";
+  "2^216 - 2^108 - 1";
+  "2^322 - 2^161 - 1";
+  "2^416 - 2^208 - 1";
+  "2^448 - 2^224 - 1"; (* goldilocks *)
+  "2^450 - 2^225 - 1";
+  "2^480 - 2^240 - 1" (* ridinghood *)
+  ].
+
+Definition two_or_more_tap_primes : list string :=
+  [
+    (* two or more taps *)
+
+    "2^205 - 45*2^198 - 1";
+  "2^224 - 2^96 + 1"; (* p224 *)
+  "2^256 - 2^224 + 2^192 + 2^96 - 1"; (* p256 *)
+  "2^256 - 2^32 - 977"; (* bitcoin *)
+  "2^256 - 4294968273"; (* bitcoin, for 64-bit impl *)
+  "2^384 - 2^128 - 2^96 + 2^32 - 1" (* p384 *)
+  ].
+
+Definition montgomery_friendly_primes : list string :=
+  [
+    (* Montgomery-Friendly *)
+
+    "2^256 - 88*2^240 - 1";
+  "2^254 - 127*2^240 - 1";
+  "2^384 - 79*2^376 - 1";
+  "2^384 - 5*2^368 - 1";
+  "2^512 - 491*2^496 - 1";
+  "2^510 - 290*2^496 - 1"
+  ].
+
+Definition multitap_primes : list string :=
+  two_tap_golden_ratio_primes
+    ++ two_or_more_tap_primes
+    ++ montgomery_friendly_primes.
+
+Definition primes : list string :=
+  single_tap_primes ++ multitap_primes.
+
+Local Instance : tight_upperbound_fraction_opt := default_tight_upperbound_fraction.
+
+(* 15.5 s for primes up to 2^301 *)
+(* 25.674 s for primes up to 2^351 *)
+(* 76.298 s for primes 2^300 up to 2^401 *)
+Local Open Scope nat_scope.
+Local Open Scope core_scope.
+Time Definition possible_limbs :=
+  Eval native_compute in
+    Option.List.lift
+      (Option.List.map
+         (fun p => match parseZ_arith_to_taps p with
+                   | Some (s, c)
+                     => if (s <=? 2^350)%Z
+                        then Some (Some (p, [(64, get_possible_limbs s c 64); (32, get_possible_limbs s c 32)]))
+                        else None
+                   | None => Some None
+                   end)
+         primes).
+Local Notation "[ ]" := nil (format "[ ]") : core_scope.
+Local Notation "[ x ]" := (cons x nil) : core_scope.
+Local Notation "[ x ; y ; .. ; z ]" :=  (cons x (cons y .. (cons z nil) ..)) (format "'[hv ' [ x ;  '/' y ;  '/' .. ;  '/' z ] ']'") : core_scope.
+Local Close Scope list_scope.
+Local Open Scope core_scope.
+Set Printing Width 250.
+Redirect "Crypto.UnsaturatedSolinasHeuristics.Tests.get_possible_limbs"
+         Print possible_limbs.