A little formal verification · Emerging Patterns

The idea

Lean is both a programming language and an interactive theorem prover. An agent can help formulate a property, propose a proof, and iterate on feedback from the checker. The promise is a stronger guarantee for a carefully bounded piece of logic.

Start with a small pure function and an explicit invariant. Keep ordinary tests for the rest of the system.

When it helps

Consider this for a compact algorithm or state transition whose correctness matters and whose intended behavior can be expressed precisely. The first challenge is deciding what to prove.

Put it into practice

This tiny example defines a clamped value and states that it cannot exceed its cap. It illustrates the shape of a proof-oriented workflow; it does not verify an external implementation.

Illustrative Lean 4 snippet

def clamp (value cap : Nat) : Nat :=
  min value cap

theorem clamp_le_cap (value cap : Nat) :
    clamp value cap ≤ cap := by
  exact Nat.min_le_right value cap

Have the agent state the property before attempting the proof. Check the file with the pinned Lean toolchain. Review assumptions and reject unfinished proofs using sorry or unreviewed axioms.

Where it breaks down

A proof of a Lean model does not automatically establish correctness of corresponding TypeScript, Rust, or Python code. The connection to the shipped implementation needs its own justification.

It is also possible to prove the wrong specification. Review the statement with domain knowledge. I/O, integration, and environmental assumptions may remain outside the proof.

Connect the patterns

Use scenarios for end-to-end behavior and proofs for precise local invariants. Both are feedback mechanisms, but they answer different questions.

Prove the parts that matter