diff --git a/nmigen/formal.py b/nmigen/asserts.py
similarity index 100%
rename from nmigen/formal.py
rename to nmigen/asserts.py
diff --git a/nmigen/hdl/ast.py b/nmigen/hdl/ast.py
index 757f5268..c5376d0d 100644
--- a/nmigen/hdl/ast.py
+++ b/nmigen/hdl/ast.py
@@ -993,7 +993,7 @@ def Fell(expr, clocks=0, domain=None):
 
 @final
 class Initial(Value):
-    """Start indicator, for formal verification.
+    """Start indicator, for model checking.
 
     An ``Initial`` signal is ``1`` at the first cycle of model checking, and ``0`` at any other.
     """
diff --git a/nmigen/lib/fifo.py b/nmigen/lib/fifo.py
index c59a040c..2808e549 100644
--- a/nmigen/lib/fifo.py
+++ b/nmigen/lib/fifo.py
@@ -1,7 +1,7 @@
 """First-in first-out queues."""
 
 from .. import *
-from ..formal import *
+from ..asserts import *
 from ..tools import log2_int
 from .coding import GrayEncoder
 
diff --git a/nmigen/test/test_lib_coding.py b/nmigen/test/test_lib_coding.py
index 4cdd83f1..6052c9a6 100644
--- a/nmigen/test/test_lib_coding.py
+++ b/nmigen/test/test_lib_coding.py
@@ -1,6 +1,6 @@
 from .tools import *
 from ..hdl import *
-from ..formal import *
+from ..asserts import *
 from ..back.pysim import *
 from ..lib.coding import *
 
diff --git a/nmigen/test/test_lib_fifo.py b/nmigen/test/test_lib_fifo.py
index 9176037f..9d136c89 100644
--- a/nmigen/test/test_lib_fifo.py
+++ b/nmigen/test/test_lib_fifo.py
@@ -1,6 +1,6 @@
 from .tools import *
 from ..hdl import *
-from ..formal import *
+from ..asserts import *
 from ..back.pysim import *
 from ..lib.fifo import *