Property-Based Testing in Python
Prove code correctness for all inputs using Hypothesis and formal methods.
Introduction
30 Second Summary
Think about how you'd prove a bridge is safe. You wouldn't just drive one car across it and call it done. You'd need to prove it holds for any car, at any weight, in any condition.
In this project, you will build a property-based test suite that proves your code works for all possible inputs, not just the ones you thought to check. You'll test a bounded stack data structure, discover bugs automatically, and connect this testing approach to formal mathematical proofs.
What You'll Build
A comprehensive property-based testing project that tests a bounded stack using Hypothesis strategies, stateful testing, and connects the concepts to formal verification in Rocq.
By the end of this project, you'll have:
- A test suite that proves properties hold for ALL inputs using Hypothesis strategies and shrinking.
- A working stateful test that models a system and discovers bugs through sequences of operations.
- A conceptual bridge document connecting property-based testing to formal verification in Rocq.
- Secret Mission: Build a custom @composite strategy for generating valid operation sequences and test a batch executor function.
Are there any prerequisites?
You should be comfortable with Python basics, including writing functions and using assertions. Completing the Code Verification Agent project first is recommended but not required.
Before We Start
Property-based testing requires specialized libraries that can generate thousands of random inputs and automatically shrink failures to minimal examples.
In this step, you'll install Hypothesis and pytest, create your project folder, and run a quick test to confirm everything works.
In this step, get ready to:
- Install Hypothesis and pytest into your Python environment.
- Create the project folder with your stack module and test files.
- Verify the installation by running a minimal Hypothesis test.
Install Hypothesis and pytest
- Press Cmd+Space (macOS) or the Windows key (Windows) to open your search bar.
- Type VS Code and press Enter to open it.
- Open the integrated terminal by pressing Ctrl+` (macOS and Windows).
Hypothesis is a property-based testing library for Python. It generates random test inputs and automatically finds the smallest example that breaks your code.
- Install both libraries by running this command:
pip install hypothesis pytestWhat does this command do?
This installs two packages. hypothesis is the property-based testing engine that generates random inputs and shrinks failures. pytest is the test runner that discovers and executes your test functions.
- Confirm the installation succeeded by running:
python -c "import hypothesis; print(hypothesis.__version__)"You should see a version number printed (such as 6.152.9 or similar).
Seeing 'command not found' for pip?
Try pip3 instead of pip. On some systems, pip points to an older Python version while pip3 points to Python 3.
If that still doesn't work, try python3 -m pip install hypothesis pytest to call pip through your Python 3 installation directly.
Help me troubleshoot my pip installation
Create the project structure
Your project needs a dedicated folder with separate files for the stack implementation, property tests, stateful tests, and a verification bridge document.
- Move to your Desktop by running this command:
cd ~/Desktop- Create your project folder and move into it by running these commands:
mkdir property-testing
cd property-testing- Create the four project files with placeholder content by running these commands:
echo "# empty placeholder" > stack.py
echo "# empty placeholder" > test_properties.py
echo "# empty placeholder" > test_stateful.py
echo "# empty placeholder" > VERIFICATION_BRIDGE.mdWhat are these files for?
- stack.py will hold the bounded stack implementation you're testing.
- test_properties.py will contain your property-based tests using Hypothesis strategies.
- test_stateful.py will contain your stateful model-based test.
- VERIFICATION_BRIDGE.md will map property-based testing concepts to formal verification in Rocq.
- Confirm the files exist by running:
lsYou should see VERIFICATION_BRIDGE.md, stack.py, test_properties.py, and test_stateful.py in the output.
- Open the property-testing folder in VS Code by running:
code .Seeing 'command not found' for code?
The code command needs to be installed in your PATH. In VS Code, press Cmd+Shift+P (macOS) or Ctrl+Shift+P (Windows), type Shell Command: Install, and select the option to install it. Then try again.
Alternatively, open VS Code manually, click File, click Open Folder, and select the property-testing folder on your Desktop.
Help me open my project folder in VS Code
Verify the installation with a minimal test
Before building the real test suite, you'll confirm Hypothesis and pytest work together by running a tiny property-based test.
- In VS Code, click on test_properties.py in the Explorer sidebar to open it.
- Replace the placeholder content with this minimal test:
"""Verify Hypothesis is installed correctly."""
from hypothesis import given, strategies as st
@given(st.integers())
def test_hypothesis_works(n):
"""Check that Hypothesis can generate integers."""
assert isinstance(n, int)What does this test do?
The @given decorator tells Hypothesis to generate random integers and pass them to your test function. By default, Hypothesis generates 100 random inputs per test.
The assertion is trivially true (generated integers are always integers), but the point is to confirm the entire pipeline works: Hypothesis generates data, pytest discovers the test, and everything runs without import errors.
- Save test_properties.py.
- Run the test in your VS Code terminal by running this command:
pytest test_properties.py -vYou should see test_properties.py::test_hypothesis_works PASSED along with a 1 passed summary at the bottom.
Test not passing or import error?
Make sure you saved the file before running pytest. Unsaved changes won't be picked up.
If you see an ImportError for hypothesis, your terminal might be using a different Python than the one you installed packages to. Try running python3 -m pytest test_properties.py -v instead.
Help me fix my Hypothesis test
- Now that the installation is confirmed, reset test_properties.py back to its placeholder so the file is clean for Step 2. Replace its contents with:
# empty placeholder- Save test_properties.py.
✔️ Awesome, I've got everything!
Great. Make sure all four files are saved in your property-testing folder and you're ready for the next step.
ⓧ I'd like to double check the full code
Each file in your project should contain only this single line:
# empty placeholder# empty placeholder# empty placeholder# empty placeholderYour testing environment is ready and confirmed working. Next up, you'll implement the bounded stack that these tests will exercise.
Implement the Bounded Stack
Your testing environment is ready. Now you need something to test.
Property-based testing works best when the system under test has clear invariants that must hold for all inputs. A bounded stack is a perfect target because it has strict rules: its size can never go negative, it can never exceed its capacity, and push followed by pop must return the original value.
In this step, get ready to:
- Write a BoundedStack class with push, pop, peek, size, and query methods.
- Introduce a deliberate off-by-one bug for Hypothesis to discover later.
Write the BoundedStack class
A bounded stack is a last-in-first-out data structure with a maximum capacity. You will implement it with operations that enforce these constraints and raise exceptions when violated.
- In VS Code, open stack.py from the Explorer sidebar.
- Select all the placeholder content and replace it with the following class definition:
"""A bounded stack implementation with a subtle bug for Hypothesis to find."""
class BoundedStack:
"""A stack with a maximum capacity.
Invariants:
- 0 <= len(self._items) <= self._capacity
- peek() returns the last pushed item
- push then pop is identity (stack unchanged)
"""
def __init__(self, capacity: int):
if capacity < 1:
raise ValueError("Capacity must be at least 1")
self._capacity = capacity
self._items: list = []
@property
def capacity(self) -> int:
return self._capacity
def push(self, item) -> None:
"""Push an item onto the stack. Raises OverflowError if full."""
if self.is_full():
raise OverflowError("Stack is full")
self._items.append(item)
def pop(self):
"""Pop and return the top item. Raises IndexError if empty."""
if self.is_empty():
raise IndexError("Stack is empty")
return self._items.pop()
def peek(self):
"""Return the top item without removing it. Raises IndexError if empty."""
if self.is_empty():
raise IndexError("Stack is empty")
return self._items[-1]
def size(self) -> int:
"""Return the current number of items."""
return len(self._items)
def is_empty(self) -> bool:
"""Return True if the stack has no items."""
return len(self._items) == 0What does this code do?
This defines a stack class with a fixed maximum size. The __init__ method rejects capacities below 1 and stores items in a private list.
The push method checks is_full() before adding an item. The pop and peek methods check is_empty() before accessing items. Both raise exceptions if the preconditions fail.
Notice that push calls self.is_full() which does not exist yet. You will add it next.
- Save stack.py. The file is not runnable yet because is_full() is still missing.
Introduce a subtle bug
The whole point of property-based testing is to find bugs that humans miss. You will now write the is_full() method with a deliberate off-by-one error. This simulates the kind of subtle mistake that passes unit tests but fails under exhaustive random input.
- In stack.py, add the following method at the bottom of the BoundedStack class, below is_empty:
def is_full(self) -> bool:
"""Return True if the stack is at capacity.
BUG: Uses > instead of >=, allowing one extra item when capacity
items are already present. This only triggers when you push exactly
at capacity.
"""
return len(self._items) > self._capacity # BUG: should be >=Why introduce a bug on purpose?
The comparison uses > instead of the correct >=. This means is_full() returns False when the stack has exactly capacity items. The stack then allows one extra push beyond its limit.
A typical unit test like "push 3 items to a stack of size 5" would never catch this. But Hypothesis generates hundreds of random inputs including the exact boundary case that triggers the failure.
- Save stack.py.
- Verify the class works by running this quick test in your terminal:
python3 -c "from stack import BoundedStack; s = BoundedStack(3); s.push(1); s.push(2); print(f'Size: {s.size()}, Peek: {s.peek()}')"- You should see Size: 2, Peek: 2 in the output.
Seeing a NameError or ImportError?
- Make sure your terminal is in the project folder that contains stack.py. Run ls to confirm the file is listed.
- Check that is_full is indented at the same level as the other methods. Python requires consistent indentation inside a class body.
- Confirm you saved the file after adding is_full.
help me debug my stack.py import error
Why can you push 2 items without hitting the bug?
The bug only triggers at the exact boundary. A stack with capacity 3 allows pushes at sizes 0, 1, and 2 (all less than 3). The bug appears when you try to push at size 3, because 3 > 3 is False, so is_full() incorrectly says there is still room.
✔️ Awesome, I've got everything!
Great. Double check you saved stack.py and that your terminal output shows Size: 2, Peek: 2.
ⓧ I'd like to double check the full code
Here is the complete stack.py at this point:
"""A bounded stack implementation with a subtle bug for Hypothesis to find."""
class BoundedStack:
"""A stack with a maximum capacity.
Invariants:
- 0 <= len(self._items) <= self._capacity
- peek() returns the last pushed item
- push then pop is identity (stack unchanged)
"""
def __init__(self, capacity: int):
if capacity < 1:
raise ValueError("Capacity must be at least 1")
self._capacity = capacity
self._items: list = []
@property
def capacity(self) -> int:
return self._capacity
def push(self, item) -> None:
"""Push an item onto the stack. Raises OverflowError if full."""
if self.is_full():
raise OverflowError("Stack is full")
self._items.append(item)
def pop(self):
"""Pop and return the top item. Raises IndexError if empty."""
if self.is_empty():
raise IndexError("Stack is empty")
return self._items.pop()
def peek(self):
"""Return the top item without removing it. Raises IndexError if empty."""
if self.is_empty():
raise IndexError("Stack is empty")
return self._items[-1]
def size(self) -> int:
"""Return the current number of items."""
return len(self._items)
def is_empty(self) -> bool:
"""Return True if the stack has no items."""
return len(self._items) == 0
def is_full(self) -> bool:
"""Return True if the stack is at capacity.
BUG: Uses > instead of >=, allowing one extra item when capacity
items are already present. This only triggers when you push exactly
at capacity.
"""
return len(self._items) > self._capacity # BUG: should be >=Your bounded stack is ready, bug and all. Next up, you will write property-based tests with Hypothesis that automatically discover this off-by-one error without you having to think of the right test case.
Write Property-Based Tests with Hypothesis
Your BoundedStack is implemented with a deliberate off-by-one bug hiding in is_full(). A handful of unit tests would probably miss it. Property-based testing flips the script: instead of checking one example at a time, you declare properties that must hold for ALL inputs and let Hypothesis generate hundreds of random examples to hunt for violations.
In this step, you will write tests that express algebraic properties of your stack (push/pop symmetry, size invariants) and use strategies and filtering to generate valid inputs. Then you will run the test suite and watch Hypothesis discover the bug automatically, shrinking it down to the smallest possible failing case.
In this step, get ready to:
- Write algebraic property tests for push, pop, and size.
- Build a custom composite strategy and use filtering with assume() to generate valid test inputs.
- Run the tests and watch Hypothesis discover the off-by-one bug.
Test algebraic properties
Algebraic properties are universal truths about your data structure. For a stack, "push then pop returns the original value" is always true regardless of what you push. These properties work like mathematical axioms that must hold for every possible input.
- Open test_properties.py in VS Code and replace its contents with the imports and three algebraic property tests by pasting this code:
"""Property-based tests for BoundedStack using Hypothesis."""
from hypothesis import given, assume, settings, strategies as st
from stack import BoundedStack
# --- Algebraic properties ---
@given(st.integers(min_value=1, max_value=20), st.integers())
def test_push_pop_symmetry(capacity, value):
"""Push then pop returns the pushed value."""
stack = BoundedStack(capacity)
stack.push(value)
assert stack.pop() == value
@given(st.integers(min_value=1, max_value=20), st.integers())
def test_push_pop_identity(capacity, value):
"""Push then pop leaves stack unchanged (empty -> empty)."""
stack = BoundedStack(capacity)
stack.push(value)
stack.pop()
assert stack.is_empty()
assert stack.size() == 0
@given(st.integers(min_value=1, max_value=20), st.integers())
def test_push_increases_size(capacity, value):
"""Pushing one item increases size by exactly 1."""
stack = BoundedStack(capacity)
old_size = stack.size()
stack.push(value)
assert stack.size() == old_size + 1What does this code do?
The @given decorator tells Hypothesis to generate random inputs matching each strategy. st.integers(min_value=1, max_value=20) produces random capacities. st.integers() with no bounds produces any integer value.
Each test declares a property that must be universally true. If Hypothesis finds ANY input where the property fails, the test fails. By default, Hypothesis tests each property with 100 random examples.
- Save test_properties.py. You will not run the tests yet. The next chunk adds more tests that use a custom strategy.
Use built-in strategies and filtering
Some properties need a stack that already has items in it ("peek does not change size" requires a non-empty stack). You need a way to generate stacks in arbitrary valid states. That is what a composite strategy does.
- In test_properties.py, find the comment # --- Algebraic properties --- and add the strategy helper section ABOVE it (right below the from stack import BoundedStack line):
# --- Strategy helpers ---
@st.composite
def bounded_stacks(draw, min_capacity=1, max_capacity=10):
"""Generate a BoundedStack in a valid random state."""
capacity = draw(st.integers(min_value=min_capacity, max_value=max_capacity))
num_items = draw(st.integers(min_value=0, max_value=capacity))
items = draw(st.lists(st.integers(), min_size=num_items, max_size=num_items))
stack = BoundedStack(capacity)
for item in items:
stack.push(item)
return stackWhat is a composite strategy?
The @st.composite decorator lets you build strategies that depend on previously drawn values. Here, num_items depends on capacity (you cannot have more items than the capacity allows). Each call to draw() pulls a random value from the strategy you pass it.
This generates stacks with random capacity AND a random number of pre-filled elements. Every generated stack is guaranteed to be in a valid state because the generation logic respects the capacity constraint.
- Now add these five tests at the bottom of test_properties.py, after the test_push_increases_size function:
@given(bounded_stacks())
def test_size_never_exceeds_capacity(stack):
"""The stack size must never exceed its capacity."""
assert stack.size() <= stack.capacity
@given(bounded_stacks(), st.integers())
def test_push_to_full_stack_raises(stack, value):
"""Pushing to a full stack must raise OverflowError."""
assume(stack.size() == stack.capacity)
try:
stack.push(value)
# If we get here, the stack allowed an illegal push (BUG!)
assert False, f"Stack allowed push beyond capacity {stack.capacity}"
except OverflowError:
pass # Expected behavior
@given(st.integers(min_value=1, max_value=10))
def test_fill_then_check_full(capacity):
"""Filling a stack to capacity should make is_full() return True.
This test is designed to catch the off-by-one bug.
"""
stack = BoundedStack(capacity)
for i in range(capacity):
stack.push(i)
assert stack.is_full(), (
f"Stack with {stack.size()}/{stack.capacity} items "
f"should be full but is_full() returned False"
)
@given(bounded_stacks())
def test_peek_does_not_modify(stack):
"""Peek should not change the stack size."""
assume(not stack.is_empty())
size_before = stack.size()
_ = stack.peek()
assert stack.size() == size_before
@given(bounded_stacks(), st.integers())
def test_peek_returns_last_pushed(stack, value):
"""After push(x), peek() must return x."""
assume(not stack.is_full())
stack.push(value)
assert stack.peek() == valueHow does assume() work?
The assume() function tells Hypothesis to discard any test case where the condition is false. It does not count discarded cases toward the 100-example limit. This is how you express preconditions like "only test this property when the stack is full" without wasting your test budget.
The test_fill_then_check_full test is the key bug-catcher. It fills a stack to exactly its stated capacity and then asserts is_full() returns True. The off-by-one bug (using > instead of >=) means a stack at capacity still reports False for is_full().
- Save test_properties.py.
✔️ Awesome, I've got everything!
Great. Double check you have saved the file.
ⓧ I'd like to double check the full code
"""Property-based tests for BoundedStack using Hypothesis."""
from hypothesis import given, assume, settings, strategies as st
from stack import BoundedStack
# --- Strategy helpers ---
@st.composite
def bounded_stacks(draw, min_capacity=1, max_capacity=10):
"""Generate a BoundedStack in a valid random state."""
capacity = draw(st.integers(min_value=min_capacity, max_value=max_capacity))
num_items = draw(st.integers(min_value=0, max_value=capacity))
items = draw(st.lists(st.integers(), min_size=num_items, max_size=num_items))
stack = BoundedStack(capacity)
for item in items:
stack.push(item)
return stack
# --- Algebraic properties ---
@given(st.integers(min_value=1, max_value=20), st.integers())
def test_push_pop_symmetry(capacity, value):
"""Push then pop returns the pushed value."""
stack = BoundedStack(capacity)
stack.push(value)
assert stack.pop() == value
@given(st.integers(min_value=1, max_value=20), st.integers())
def test_push_pop_identity(capacity, value):
"""Push then pop leaves stack unchanged (empty -> empty)."""
stack = BoundedStack(capacity)
stack.push(value)
stack.pop()
assert stack.is_empty()
assert stack.size() == 0
@given(st.integers(min_value=1, max_value=20), st.integers())
def test_push_increases_size(capacity, value):
"""Pushing one item increases size by exactly 1."""
stack = BoundedStack(capacity)
old_size = stack.size()
stack.push(value)
assert stack.size() == old_size + 1
@given(bounded_stacks())
def test_size_never_exceeds_capacity(stack):
"""The stack size must never exceed its capacity."""
assert stack.size() <= stack.capacity
@given(bounded_stacks(), st.integers())
def test_push_to_full_stack_raises(stack, value):
"""Pushing to a full stack must raise OverflowError."""
assume(stack.size() == stack.capacity)
try:
stack.push(value)
# If we get here, the stack allowed an illegal push (BUG!)
assert False, f"Stack allowed push beyond capacity {stack.capacity}"
except OverflowError:
pass # Expected behavior
@given(st.integers(min_value=1, max_value=10))
def test_fill_then_check_full(capacity):
"""Filling a stack to capacity should make is_full() return True.
This test is designed to catch the off-by-one bug.
"""
stack = BoundedStack(capacity)
for i in range(capacity):
stack.push(i)
assert stack.is_full(), (
f"Stack with {stack.size()}/{stack.capacity} items "
f"should be full but is_full() returned False"
)
@given(bounded_stacks())
def test_peek_does_not_modify(stack):
"""Peek should not change the stack size."""
assume(not stack.is_empty())
size_before = stack.size()
_ = stack.peek()
assert stack.size() == size_before
@given(bounded_stacks(), st.integers())
def test_peek_returns_last_pushed(stack, value):
"""After push(x), peek() must return x."""
assume(not stack.is_full())
stack.push(value)
assert stack.peek() == valueWatch Hypothesis find the bug
Time for the payoff. You will run the full test suite and watch Hypothesis automatically discover the off-by-one bug in is_full(). It will also shrink the failing example down to the smallest case that triggers the bug.
- Run the property tests by executing this command in your terminal:
pytest test_properties.py -vMost tests pass, but test_fill_then_check_full fails. Hypothesis reports something like:
Falsifying example: test_fill_then_check_full(
capacity=1,
)What just happened?
Hypothesis tried random capacity values and found that filling a stack with capacity 1 to exactly 1 item still makes is_full() return False. Then it shrank the example to the simplest case: capacity=1.
This is shrinking in action. Hypothesis first finds a large failing example, then systematically tries simpler inputs until it finds the minimal reproducing case. The bug is clear: len(self._items) > self._capacity only triggers when you have MORE items than capacity, but you can never get there because push() checks is_full() first. The condition should be >=.
Why leave the bug unfixed?
You will keep this bug in place intentionally. In the next step you will build a stateful test that also catches it. Seeing the same bug caught by two different techniques reinforces why property-based testing is so powerful.
Tests not running?
Make sure you are running the command from the same folder that contains both stack.py and test_properties.py. If you see an import error, check that the filename is exactly stack.py (not Stack.py or bounded_stack.py).
If you see all tests passing with no failures, double check that is_full() in stack.py still uses > (the bug). The comparison len(self._items) > self._capacity is the deliberate error.
Help me debug my test setup.
Your property tests just proved that no amount of unit tests with hand-picked values would have caught this bug as quickly. Next up, you will build a stateful test that models your stack with a plain Python list and discovers bugs through sequences of operations.
Build Custom Strategies and Stateful Tests
Your property-based tests already caught the off-by-one bug in is_full(). Each test used @given to assert a single property for random inputs.
Real bugs often hide in sequences of operations, not individual calls. In this step, you will build a stateful test that generates random sequences of push, pop, and peek operations, checking that your stack matches a known-correct model after every single step.
In this step, get ready to:
- Understand how the existing @composite strategy uses dependent generation.
- Build a RuleBasedStateMachine that models the stack with a Python list.
- Run the stateful test and observe Hypothesis generating operation sequences.
Understand the @composite strategy
Before writing the stateful test, take a moment to study the bounded_stacks strategy you already have in test_properties.py. This is a @composite strategy, which is Hypothesis's tool for dependent generation.
- In VS Code, open test_properties.py and scroll to the top where the bounded_stacks function is defined.
@st.composite
def bounded_stacks(draw, min_capacity=1, max_capacity=10):
"""Generate a BoundedStack in a valid random state."""
capacity = draw(st.integers(min_value=min_capacity, max_value=max_capacity))
num_items = draw(st.integers(min_value=0, max_value=capacity))
items = draw(st.lists(st.integers(), min_size=num_items, max_size=num_items))
stack = BoundedStack(capacity)
for item in items:
stack.push(item)
return stackWhat is dependent generation?
The draw function lets each random choice depend on the previous one. First, Hypothesis picks a random capacity. Then it picks num_items that is bounded by that capacity. Then it generates a list of exactly that many items.
This guarantees every generated stack is in a valid state. No filtering needed, no wasted attempts. This pattern of dependent generation is what makes @composite so powerful for testing data structures with internal constraints.
Build a RuleBasedStateMachine test
A RuleBasedStateMachine goes beyond single-property tests. It defines a set of operations (rules) that Hypothesis calls in random order, checking invariants after every single operation.
The trick is to maintain a "model" alongside your implementation. The model is a simple Python list that we know is correct. After every operation, we assert the real stack and the model agree.
- In VS Code, open test_stateful.py and replace the placeholder content with the following imports and class setup:
"""Stateful testing for BoundedStack using Hypothesis RuleBasedStateMachine."""
from hypothesis import settings
from hypothesis.stateful import (
Bundle,
RuleBasedStateMachine,
rule,
precondition,
invariant,
)
from hypothesis import strategies as st
from stack import BoundedStack
class BoundedStackMachine(RuleBasedStateMachine):
"""A state machine that tests BoundedStack against a list model."""
def __init__(self):
super().__init__()
self.capacity = 5
self.stack = BoundedStack(self.capacity)
self.model: list = []
@rule(value=st.integers())
@precondition(lambda self: len(self.model) < self.capacity)
def push(self, value):
"""Push a value onto both the real stack and the model."""
self.stack.push(value)
self.model.append(value)
@rule()
@precondition(lambda self: len(self.model) > 0)
def pop(self):
"""Pop from both the real stack and the model, assert they match."""
real_value = self.stack.pop()
model_value = self.model.pop()
assert real_value == model_value
@rule()
@precondition(lambda self: len(self.model) > 0)
def peek(self):
"""Peek at both and assert they match."""
assert self.stack.peek() == self.model[-1]What does this code do?
- @rule(value=st.integers()) tells Hypothesis this is an operation it can call with a random integer.
- @precondition(lambda self: len(self.model) < self.capacity) ensures Hypothesis only calls push when there is room in the stack.
- self.model is a plain Python list that acts as the "correct" specification. After every operation, the real stack must match this list.
- Each rule performs the same operation on both the real stack and the model, then asserts they agree.
Now add the invariants that Hypothesis checks after every single operation, plus the line that exposes the machine as a pytest test case.
- Add the following code at the bottom of the BoundedStackMachine class (indented inside the class), followed by the TestBoundedStack line outside the class:
@invariant()
def size_matches(self):
"""After every operation, sizes must agree."""
assert self.stack.size() == len(self.model)
@invariant()
def capacity_respected(self):
"""The stack must never exceed its capacity."""
assert self.stack.size() <= self.capacity
@invariant()
def fullness_consistent(self):
"""is_full() must be True exactly when size == capacity."""
assert self.stack.is_full() == (len(self.model) == self.capacity)
TestBoundedStack = BoundedStackMachine.TestCaseWhat are invariants in a state machine?
Invariants are conditions that MUST be true after every single operation. Hypothesis checks all three invariants after every push, pop, and peek call. If any invariant fails at any point in the sequence, the test fails.
The fullness_consistent invariant is the one designed to catch the off-by-one bug. It asserts that is_full() returns True exactly when the model list has capacity items.
Why a model-based approach?
Testing against a model is the most powerful pattern in property-based testing. You build a simple, obviously correct version (a Python list) and assert the complex version (BoundedStack) always agrees with it.
In formal verification, this is called a refinement proof. You are proving that the implementation "refines" (correctly implements) the specification. Your stateful test is the same idea, verified with random operation sequences instead of mathematical proof.
- Save test_stateful.py.
Seeing an IndentationError?
The three invariant methods must be indented inside the BoundedStackMachine class. The TestBoundedStack = BoundedStackMachine.TestCase line must be at the module level (no indentation).
help me fix my indentation in test_stateful.py
✔️ Awesome, I've got everything!
Great. Double check you have saved your file before moving on.
ⓧ I'd like to double check the full code
"""Stateful testing for BoundedStack using Hypothesis RuleBasedStateMachine."""
from hypothesis import settings
from hypothesis.stateful import (
Bundle,
RuleBasedStateMachine,
rule,
precondition,
invariant,
)
from hypothesis import strategies as st
from stack import BoundedStack
class BoundedStackMachine(RuleBasedStateMachine):
"""A state machine that tests BoundedStack against a list model."""
def __init__(self):
super().__init__()
self.capacity = 5
self.stack = BoundedStack(self.capacity)
self.model: list = []
@rule(value=st.integers())
@precondition(lambda self: len(self.model) < self.capacity)
def push(self, value):
"""Push a value onto both the real stack and the model."""
self.stack.push(value)
self.model.append(value)
@rule()
@precondition(lambda self: len(self.model) > 0)
def pop(self):
"""Pop from both the real stack and the model, assert they match."""
real_value = self.stack.pop()
model_value = self.model.pop()
assert real_value == model_value
@rule()
@precondition(lambda self: len(self.model) > 0)
def peek(self):
"""Peek at both and assert they match."""
assert self.stack.peek() == self.model[-1]
@invariant()
def size_matches(self):
"""After every operation, sizes must agree."""
assert self.stack.size() == len(self.model)
@invariant()
def capacity_respected(self):
"""The stack must never exceed its capacity."""
assert self.stack.size() <= self.capacity
@invariant()
def fullness_consistent(self):
"""is_full() must be True exactly when size == capacity."""
assert self.stack.is_full() == (len(self.model) == self.capacity)
TestBoundedStack = BoundedStackMachine.TestCaseRun the stateful test
Time to let Hypothesis loose. It will generate random sequences of push, pop, and peek operations, checking all three invariants after every step in the sequence.
- Run the stateful test by executing this command in your terminal:
pytest test_stateful.py -vYou should see a failure in the fullness_consistent invariant. Hypothesis found a sequence of push operations that fills the stack to capacity, at which point is_full() returns False even though the model list has exactly capacity items.
What is Hypothesis doing here?
Hypothesis is generating random sequences like: push(0), push(1), push(2), push(3), push(4). After the fifth push, the model has 5 items (matching the capacity of 5). The invariant checks whether is_full() agrees with len(self.model) == self.capacity.
Because the bug uses > instead of >=, the stack reports "not full" when it has exactly capacity items. Hypothesis shrinks the failing sequence down to the minimal set of operations needed to trigger the bug.
Test passes without any failures?
Check that stack.py still has the bug (> instead of >= in is_full()). If you accidentally fixed it, the tests will pass. The bug is intentional for this exercise.
Also verify that the TestBoundedStack = BoundedStackMachine.TestCase line is at the bottom of the file. Without it, pytest cannot discover the state machine as a test.
help me debug why my stateful test isn't finding the bug
Your stateful test just proved that testing sequences of operations catches bugs that individual property tests might miss. Hypothesis explored random interleavings of push, pop, and peek to find the exact sequence that breaks the model-implementation agreement. Next, you will connect everything you have learned to formal verification concepts in Rocq.
Connect Property-Based Testing to Formal Verification
You've built a test suite that discovers bugs through random generation and stateful exploration. These techniques share a deep connection with formal verification, where properties are not just tested but mathematically proven.
In this step, you'll write a bridge document that maps every Hypothesis concept you've used to its formal equivalent in Rocq (formerly Coq). This is the mental model you'll carry into formal verification work at SkyLabs AI.
In this step, get ready to:
- Map PBT concepts to their Rocq equivalents (strategies to types, properties to theorems, stateful tests to refinement proofs).
- Write Rocq pseudocode showing how your stack properties translate to formal theorems.
- Summarize the verification spectrum from unit tests through formal proofs.
Write the verification bridge document
The core insight is that every Hypothesis feature you've used has a direct analogue in a formal proof system. Strategies define input domains just like types do. The @given decorator means "for all values" just like the mathematical quantifier forall.
- In VS Code, open VERIFICATION_BRIDGE.md (the empty placeholder).
- Replace the placeholder content with the following, which establishes the verification spectrum and maps each Hypothesis concept to its Rocq equivalent:
# From Property-Based Testing to Formal Verification in Rocq
## The Verification Spectrum
| Level | Approach | Guarantee | Tool |
|-------|----------|-----------|------|
| 1 | Unit Tests | "Works for THESE inputs" | pytest |
| 2 | Property-Based Tests | "Works for RANDOM inputs (high confidence)" | Hypothesis |
| 3 | Formal Proofs | "Works for ALL inputs (mathematical certainty)" | Rocq |
SkyLabs AI works across levels 2 and 3. Property-based testing is the
practical bridge that builds the mental model for formal proofs.
## Concept Mapping: Hypothesis to Rocq
### Strategies = Types
In Hypothesis:
```python
@given(st.integers(min_value=0, max_value=100))
def test_property(n): ...
```
In Rocq (pseudocode):
```
Theorem property : forall (n : nat), n <= 100 -> <property holds>.
```
A strategy defines the *domain* of valid inputs. In Rocq, this is
expressed as a type (nat, list, etc.) plus preconditions.
### @given = Universal Quantification (forall)
`@given(strategy)` means "for all values this strategy can produce."
In Rocq, this is literally `forall`. The difference: Hypothesis *samples*
from the space; Rocq *proves* over the entire space.
### Properties = Theorems
```python
def test_push_pop_symmetry(capacity, value):
stack = BoundedStack(capacity)
stack.push(value)
assert stack.pop() == value
```
In Rocq:
```
Theorem push_pop_symmetry :
forall (cap : nat) (v : Z) (s : stack),
valid_stack s cap ->
pop (push s v) = (v, s).
```
### Shrinking = Proof Simplification
When Hypothesis finds a counterexample, it *shrinks* it to the minimal
failing case. In formal verification, this corresponds to finding the
simplest counterexample that violates a specification.
### RuleBasedStateMachine = Refinement Proofs
Our stateful test maintains a *model* (Python list) alongside the
*implementation* (BoundedStack) and asserts they always agree. This is
exactly a **refinement proof**: showing that an implementation refines
(correctly implements) a specification.
In Rocq, refinement is proven by showing a simulation relation holds
across all state transitions.What does this content cover?
The verification spectrum table places your work in context. Unit tests check specific examples, PBT checks random examples with high confidence, and formal proofs give mathematical certainty.
Each concept mapping shows a Hypothesis feature you already used alongside its Rocq equivalent. The RuleBasedStateMachine to refinement proof connection is the most powerful: your stateful test from Step 4 is structurally identical to how formal systems verify implementations against specifications.
Include a Rocq pseudocode example
The Curry-Howard correspondence is the theoretical foundation connecting programming and proving. In Rocq, a proof is literally a program and a theorem is literally a type.
- Add the following section below the "RuleBasedStateMachine = Refinement Proofs" section you just wrote:
## The Curry-Howard Correspondence
The deepest connection: in Rocq, a **proof IS a program** and a
**theorem IS a type**. When you prove `push_pop_symmetry`, you are
literally constructing a function that inhabits that type.
This means:
- Writing a proof = writing a program
- Type-checking = proof verification
- The Rocq kernel = a small, trusted proof checkerWhat is the Curry-Howard correspondence?
This is the key insight that makes Rocq work. Because types and theorems are the same thing, the Rocq type-checker can verify proofs mechanically. If your proof program type-checks, the theorem is guaranteed to be correct.
The Rocq kernel (the proof checker) is intentionally small. A small kernel means fewer places for bugs to hide in the verifier itself.
Summarize the spectrum of verification
The final two sections answer the practical question: why start with PBT instead of jumping straight to formal proofs? They also explain what Rocq adds beyond what Hypothesis can achieve.
- Add these final sections below the Curry-Howard section:
## Why PBT First?
1. **Same mental model**: Think in universals ("for all x, P(x) holds")
2. **Same vocabulary**: properties, invariants, preconditions, models
3. **Immediate feedback**: Tests run in seconds; proofs can take hours
4. **Bug-finding power**: PBT catches most bugs; proofs catch ALL bugs
5. **Incremental path**: Start with PBT, graduate to proofs for critical code
## What Rocq Adds
- **Certainty**: Not "high confidence" but mathematical proof
- **Extraction**: Rocq can extract verified OCaml/Haskell programs
- **Dependent types**: Types that depend on values (e.g., "list of length n")
- **Tactics**: Semi-automated proof construction (like a proof IDE)
At SkyLabs AI, you'll use Rocq to verify properties of software that
PBT alone cannot guarantee. The thinking is the same; the tool is stronger.What does this section explain?
"Why PBT First?" lists five reasons that property-based testing is the right starting point. You already think in universals ("for all stacks, size never exceeds capacity"). Formal proofs use the same thinking but with mathematical certainty instead of random sampling.
"What Rocq Adds" highlights the gap: program extraction (verified code you can ship), dependent types (types that encode constraints), and tactics (semi-automated proof construction).
- Save VERIFICATION_BRIDGE.md.
- Open the VS Code Markdown preview by pressing Cmd+Shift+V (macOS) or Ctrl+Shift+V (Windows). You should see a formatted document with the verification spectrum table, five concept mapping sections, and the two closing summaries.
Preview looks broken or shows raw markdown?
Make sure the file is saved with the .md extension. VS Code uses the extension to decide how to render the preview.
Check that the code fences (triple backticks) are closed properly. An unclosed fence will swallow everything below it into a single code block.
Help me debug my VERIFICATION_BRIDGE.md markdown preview
✔️ Awesome, I've got everything!
Great. Double check that your file is saved.
ⓧ I'd like to double check the full code
Here is the complete VERIFICATION_BRIDGE.md for comparison:
# From Property-Based Testing to Formal Verification in Rocq
## The Verification Spectrum
| Level | Approach | Guarantee | Tool |
|-------|----------|-----------|------|
| 1 | Unit Tests | "Works for THESE inputs" | pytest |
| 2 | Property-Based Tests | "Works for RANDOM inputs (high confidence)" | Hypothesis |
| 3 | Formal Proofs | "Works for ALL inputs (mathematical certainty)" | Rocq |
SkyLabs AI works across levels 2 and 3. Property-based testing is the
practical bridge that builds the mental model for formal proofs.
## Concept Mapping: Hypothesis to Rocq
### Strategies = Types
In Hypothesis:
```python
@given(st.integers(min_value=0, max_value=100))
def test_property(n): ...
```
In Rocq (pseudocode):
```
Theorem property : forall (n : nat), n <= 100 -> <property holds>.
```
A strategy defines the *domain* of valid inputs. In Rocq, this is
expressed as a type (nat, list, etc.) plus preconditions.
### @given = Universal Quantification (forall)
`@given(strategy)` means "for all values this strategy can produce."
In Rocq, this is literally `forall`. The difference: Hypothesis *samples*
from the space; Rocq *proves* over the entire space.
### Properties = Theorems
```python
def test_push_pop_symmetry(capacity, value):
stack = BoundedStack(capacity)
stack.push(value)
assert stack.pop() == value
```
In Rocq:
```
Theorem push_pop_symmetry :
forall (cap : nat) (v : Z) (s : stack),
valid_stack s cap ->
pop (push s v) = (v, s).
```
### Shrinking = Proof Simplification
When Hypothesis finds a counterexample, it *shrinks* it to the minimal
failing case. In formal verification, this corresponds to finding the
simplest counterexample that violates a specification.
### RuleBasedStateMachine = Refinement Proofs
Our stateful test maintains a *model* (Python list) alongside the
*implementation* (BoundedStack) and asserts they always agree. This is
exactly a **refinement proof**: showing that an implementation refines
(correctly implements) a specification.
In Rocq, refinement is proven by showing a simulation relation holds
across all state transitions.
## The Curry-Howard Correspondence
The deepest connection: in Rocq, a **proof IS a program** and a
**theorem IS a type**. When you prove `push_pop_symmetry`, you are
literally constructing a function that inhabits that type.
This means:
- Writing a proof = writing a program
- Type-checking = proof verification
- The Rocq kernel = a small, trusted proof checker
## Why PBT First?
1. **Same mental model**: Think in universals ("for all x, P(x) holds")
2. **Same vocabulary**: properties, invariants, preconditions, models
3. **Immediate feedback**: Tests run in seconds; proofs can take hours
4. **Bug-finding power**: PBT catches most bugs; proofs catch ALL bugs
5. **Incremental path**: Start with PBT, graduate to proofs for critical code
## What Rocq Adds
- **Certainty**: Not "high confidence" but mathematical proof
- **Extraction**: Rocq can extract verified OCaml/Haskell programs
- **Dependent types**: Types that depend on values (e.g., "list of length n")
- **Tactics**: Semi-automated proof construction (like a proof IDE)
At SkyLabs AI, you'll use Rocq to verify properties of software that
PBT alone cannot guarantee. The thinking is the same; the tool is stronger.Your bridge document is complete. You now have a reference that maps every Hypothesis concept you've used to its formal verification counterpart in Rocq. Next up: the Secret Mission challenges you to build a custom operation strategy and batch executor.
Secret mission
Custom Operation Strategy and Batch Executor
Your property tests check individual operations. But real systems process batches of commands. Can you build a custom @composite strategy that generates valid operation sequences, and prove that batch execution matches sequential execution?
Clean Up Your Resources
Clean Up Your Resources
This project runs entirely locally on your machine, so there are no ongoing costs or cloud resources to worry about. Decide whether to keep your files for future reference, or delete them entirely.
Resources you used:
- Project files: stack.py, test_properties.py, test_stateful.py, test_batch.py, VERIFICATION_BRIDGE.md.
- Python packages: hypothesis and pytest.
Keep everything running
No action needed. Choose this if you plan to keep experimenting with property-based testing or want to reference your tests later.
- Your project files remain on your Desktop.
- Hypothesis and pytest stay installed in your Python environment for future use.
Pause - I'll come back to this later
There are no running processes or servers to stop. Your project is just files on disk.
- Close VS Code to free up memory.
- Your files and installed packages will still be there when you come back.
Delete - I don't want to use this again
Remove all project files and uninstall the packages you added.
- Delete your project folder from your Desktop. On macOS/Linux, run the following command (replace the folder name with yours):
rm -rf ~/Desktop/[[PROJECT_FOLDER="your-project-folder-name"]]On Windows, run:
Remove-Item -Recurse -Force ~\Desktop\[[PROJECT_FOLDER="your-project-folder-name"]]- Uninstall Hypothesis and pytest by running:
pip uninstall hypothesis pytest -yNice Work!
Nice Work!
You've just built a test suite that thinks in universals, not examples. Your property-based tests prove that your BoundedStack satisfies algebraic laws across thousands of random inputs, and your stateful tests discovered bugs through sequences of operations no human would think to try.
You've learned how to:
- Wrote property-based tests using @given, Hypothesis strategies, and assume() to prove properties hold for all inputs.
- Built a RuleBasedStateMachine that models your system with a specification and discovers bugs through sequences of operations.
- Connected property-based testing concepts to formal verification in Rocq with a bridge document mapping strategies to types, properties to theorems, and stateful tests to refinement proofs.
- Created a custom @composite strategy for generating valid operation sequences and tested a batch executor function.
Ready to quiz yourself?