ExplainerFormal verificationAgentic codingNovember 2026

Six ways to check
that code is right

From unit tests to a machine-checked proof, on one 32-line function that blocks requests to private addresses. Each rung found something the one below it missed.

FULL EXPLAINER, CODE
AND GLOSSARY

When one agent writes code and tests, both share its blind spot

Trust the tests

An agent writes hundreds of lines a minute.
It writes the tests from the same understanding.
A misunderstanding passes both. CI goes green.

Trust a spec and a checker

You read one line: refuse what the OS reads as private.
A tool checks it on thousands of inputs, or all.
The tool checks a model's code like anyone's.

A person can check the spec in seconds, so trust sits there. Agents make the strong rungs cheap: the checker rejects a wrong proof, so a bad draft costs a retry. AlphaProof works this way: a model writes Lean proofs, and Lean checks them.

3 of 3 tests passed, and 127.0.0.1 got through

server-side request forgery

A service that fetches user URLs must refuse private hosts. This guard reads four decimal numbers with int():

def is_blocked(
    host: str,
) -> bool:
    """True if the guard should refuse to connect to this host."""
    numbers = parse_ipv4(host)
    if numbers is None:
        return False  # not an IP address, so treat it as a hostname
    a, b = numbers[0], numbers[1]
    if a == 127 or a == 10:
        return True
    if a == 172 and 16 <= b <= 32:
        return True
    return a == 192 and b == 168

Bug 1 is a typo: the 172 range ends at 31, not 32.

Bug 2: the OS parses with inet_aton, which takes octal, hex and one- to four-part forms:

Host	Guard blocks?	OS reads
127.0.0.1	yes	127.0.0.1
0177.0.0.1	no	127.0.0.1
0x7f.0.0.1	no	127.0.0.1
127.1	no	127.0.0.1
2130706433	no	127.0.0.1
10.0	no	10.0.0.0
172.32.0.1	yes	public

Measured with Python's socket.inet_aton on Linux. OWASP lists these spellings as standard SSRF bypasses.

3 of 3

example tests pass on the guard with both bugs

10 of 20

runs in which a plain random generator found the bypass

65,536

inputs a 0.24-second loop checks to prove the range

2³²

addresses Z3 and Lean cover without running one

Six rungs, each a stronger check

Example tests

the inputs the author thought of

testing

Property-based (Hypothesis)

generated inputs against one rule

testing

Exhaustive enumeration

every input in a small, finite set

testing

State-machine testing

random sequences, a rule after each step

testing

Solver (Z3)

reasons about every input at once

formal

Proof (Lean)

a kernel checks every proof step

formal

Rungs 2 to 4 still run the real code. Rungs 5 and 6 reason about a model of it.

No rung caught every bug

Rung	Typo 172.32	Octal, hex	Short forms	DNS switch
1 Example	miss	miss	miss	n/a
2 Property	miss	miss	10.0	n/a
3 Exhaustive	found	6 of 768	miss	n/a
4 State	n/a	n/a	n/a	found
5 Solver	found	not in model	not in model	n/a
6 Proof	refused	not in model	not in model	n/a

"Miss": the first failure reported was another bug, or none. "Not in model": the formula left parsing out. "n/a": outside what the rung checks.

Six ideas every rung is built from

SpecificationWhat the code must do, stated without saying how.

PropertyA spec as code that returns true or false for any input.

CounterexampleAn input that breaks the property: proof of a bug.

OracleWhat you trust for the right answer. Here, inet_aton.

Input spaceEvery possible input. Small enough, and a loop proves it.

ShrinkingCutting a failing input down to the smallest that fails.

Demonstration code for learning, with bugs left in on purpose: not a production SSRF defense. Counts are from runs on 1 November 2026.

aarora79.github.io/explainers/formal-verification-ladder1 / 2

The evidence

What each rung ran and found

Real code and real output from the explainer's demo folder. Python 3.14, Hypothesis 6.170.2, Z3, Lean 4.35.0.

Rungs 5 and 6 cover 4.3 billion addresses and run none

log scale

inputs actually runinputs covered by reasoningHypothesis runs 100 examples or sequences per test by default.

Rung 2: state a rule

@given(host=hosts())
def test_guard_agrees_with_the_os(
    host: str,
) -> None:
    assert is_blocked(host) == os_reaches_blocked(host)

E           host='10.0',
FAILED test_rung2_property.py::test_guard_agrees_with_the_os

The strategy builds 1 to 4 parts in decimal, octal or hex. Weighting it toward 10, 127, 172 and 192 took it from 10 of 20 runs to 20 of 20.

Rung 4: two lookups

"""Check the address, then connect. It looks the name up twice."""
if is_blocked(dns.resolve(name)):
    return
connections.append(dns.resolve(name))

E       AssertionError: connected to ['127.0.0.1']
E       state = FetchMachine()
E       state.dns_changes(answer='127.0.0.1')
E       state.fetch_page()

Lookup one passes the check; lookup two connects. No input to the guard is wrong, so rungs 1 to 3 miss it. Output trimmed to the steps.

Rung 5: a solver

guards = {
    "as written (b <= 32)": And(a == 172, 16 <= b, b <= 32),
    "fixed (b <= 31)": And(a == 172, 16 <= b, b <= 31),
}
for name, guard in guards.items():
    solver = Solver()
    solver.add(octets_valid, guard != spec)  # any disagreement

as written (b <= 32): counterexample 172.32.255.255
fixed (b <= 31): no counterexample in all 2**32 addresses

"No counterexample" means unsatisfiable: a proof over every input, with none run.

Rung 6: a proof

def guard172 (a b : Nat) : Prop :=
  a = 172 ∧ 16 ≤ b ∧ b ≤ 31

theorem guard_matches_spec (a b c d : Nat)
    (ha : a < 256) (hb : b < 256) (hc : c < 256) (hd : d < 256) :
    guard172 a b ↔ inPrivate172 (toNat a b c d) := by
  unfold guard172 inPrivate172 toNat
  omega

error: omega could not prove the goal:
  16 ≤ e ≤ 32
where
 e := ↑b

Lean accepts the fix. With b ≤ 32 it refuses and names b. Output trimmed.

The fix: parse like the OS, look up once

"""True if the guard should refuse to connect to this host."""
try:
    address = ipaddress.IPv4Address(socket.inet_aton(host))
except OSError:
    return False  # not an address; the DNS check handles names
if host != str(address):
    return True  # an unusual spelling: refuse rather than guess
return any(address in network for network in BLOCKED)

"""Look the name up once, check that address, connect to it."""
address = dns.resolve(name)
if is_blocked(address):
    return
connections.append(address)

It refuses odd spellings like 010.0.0.1 too, so the property runs one way: if the OS would reach a blocked address, the guard refuses. All three checks pass.

What a pass cannot tell you

A wrong spec passes every rung. Drop 169.254.0.0/16 (cloud metadata) and the proof still checks.
Generators miss bugs: 10 of 20 plain runs passed.
Models leave things out. Z3 and Lean never saw the parser.
Agents can weaken a check with an assume(), a swapped oracle or a Lean sorry. Review those diffs like firewall rules.

Run it yourself

cd demo
uv run --no-project --with hypothesis \
  --with pytest pytest -q
# expect 4 failed, 6 passed
uv run --no-project --with z3-solver \
  python rung5_solver.py

Pick a rung: 2 and 3 for most code, 4 when a bug needs steps, 5 and 6 for a small core such as an access check.

Demonstration code for learning, not a production SSRF defense: review and harden before use. Counts are from runs on 1 November 2026.

aarora79.github.io/explainers/formal-verification-ladder2 / 2

Six ways to checkthat code is right

When one agent writes code and tests, both share its blind spot

3 of 3 tests passed, and 127.0.0.1 got through

Six rungs, each a stronger check

No rung caught every bug

Six ideas every rung is built from

What each rung ran and found

Rungs 5 and 6 cover 4.3 billion addresses and run none

Rung 2: state a rule

Rung 4: two lookups

Rung 5: a solver

Rung 6: a proof

The fix: parse like the OS, look up once

What a pass cannot tell you

Run it yourself

Six ways to check
that code is right