diff --git a/lang/funcs/core/fmt/printf_func.go b/lang/funcs/core/fmt/printf_func.go
index 5ada7240..2f4a45e4 100644
--- a/lang/funcs/core/fmt/printf_func.go
+++ b/lang/funcs/core/fmt/printf_func.go
@@ -64,6 +64,125 @@ func (obj *PrintfFunc) ArgGen(index int) (string, error) {
 	return util.NumToAlpha(index - 1), nil
 }
 
+// Unify returns the list of invariants that this func produces.
+func (obj *PrintfFunc) Unify(expr interfaces.Expr) ([]interfaces.Invariant, error) {
+	var invariants []interfaces.Invariant
+	var invar interfaces.Invariant
+
+	// func(format string, args... variant) string
+
+	formatName, err := obj.ArgGen(0)
+	if err != nil {
+		return nil, err
+	}
+
+	dummyFormat := &interfaces.ExprAny{} // corresponds to the format type
+	dummyOut := &interfaces.ExprAny{}    // corresponds to the out string
+
+	// format arg type of string
+	invar = &interfaces.EqualsInvariant{
+		Expr: dummyFormat,
+		Type: types.TypeStr,
+	}
+	invariants = append(invariants, invar)
+
+	// return type of string
+	invar = &interfaces.EqualsInvariant{
+		Expr: dummyOut,
+		Type: types.TypeStr,
+	}
+	invariants = append(invariants, invar)
+
+	// generator function
+	fn := func(fnInvariants []interfaces.Invariant, solved map[interfaces.Expr]*types.Type) ([]interfaces.Invariant, error) {
+		for _, invariant := range fnInvariants {
+			// search for this special type of invariant
+			cfavInvar, ok := invariant.(*interfaces.CallFuncArgsValueInvariant)
+			if !ok {
+				continue
+			}
+			// did we find the mapping from us to ExprCall ?
+			if cfavInvar.Func != expr {
+				continue
+			}
+			// cfavInvar.Expr is the ExprCall!
+			// cfavInvar.Args are the args that ExprCall uses!
+			if len(cfavInvar.Args) == 0 {
+				return nil, fmt.Errorf("unable to build function with no args")
+			}
+
+			value, err := cfavInvar.Args[0].Value() // is it known?
+			if err != nil {
+				return nil, fmt.Errorf("format string is not known statically")
+			}
+
+			if k := value.Type().Kind; k != types.KindStr {
+				return nil, fmt.Errorf("unable to build function with 0th arg of kind: %s", k)
+			}
+			format := value.Str() // must not panic
+			typList, err := parseFormatToTypeList(format)
+			if err != nil {
+				return nil, errwrap.Wrapf(err, "could not parse format string")
+			}
+
+			// full function
+			mapped := make(map[string]interfaces.Expr)
+			ordered := []string{formatName}
+			mapped[formatName] = dummyFormat
+
+			var invariants []interfaces.Invariant
+			var invar interfaces.Invariant
+			for i, x := range typList {
+				argName, err := obj.ArgGen(i + 1) // skip 0th
+				if err != nil {
+					return nil, err
+				}
+				if argName == formatArgName {
+					return nil, fmt.Errorf("could not build function with %d args", i+1) // +1 for format arg
+				}
+
+				dummyArg := &interfaces.ExprAny{}
+				invar := &interfaces.EqualsInvariant{
+					Expr: dummyArg,
+					Type: x,
+				}
+				invariants = append(invariants, invar)
+
+				mapped[argName] = dummyArg
+				ordered = append(ordered, argName)
+			}
+
+			invar = &interfaces.EqualityWrapFuncInvariant{
+				Expr1:    expr, // maps directly to us!
+				Expr2Map: mapped,
+				Expr2Ord: ordered,
+				Expr2Out: dummyOut,
+			}
+			invariants = append(invariants, invar)
+
+			// TODO: do we return this relationship with ExprCall?
+			invar = &interfaces.EqualityWrapCallInvariant{
+				// TODO: should Expr1 and Expr2 be reversed???
+				Expr1: cfavInvar.Expr,
+				//Expr2Func: cfavInvar.Func, // same as below
+				Expr2Func: expr,
+			}
+			invariants = append(invariants, invar)
+
+			// TODO: are there any other invariants we should build?
+			return invariants, nil // generator return
+		}
+		// We couldn't tell the solver anything it didn't already know!
+		return nil, fmt.Errorf("couldn't generate new invariants")
+	}
+	invar = &interfaces.GeneratorInvariant{
+		Func: fn,
+	}
+	invariants = append(invariants, invar)
+
+	return invariants, nil
+}
+
 // Polymorphisms returns the possible type signature for this function. In this
 // case, since the number of arguments can be infinite, it returns the final
 // precise type if it can be gleamed from the format argument. If it cannot, it