Lean is useful even when you do not verify the implementation itself. You can encode a specification as a small executable model, generate a test corpus from that model, feed the same inputs to a real checker, compiler, or runtime, and report disagreements as counterexamples.
The essential separation is:
- Correctness inside the model: Lean checks the semantic decision procedure and its theorems.
- Correspondence with the implementation: an external adapter runs the implementation and compares its observations with Lean's decisions.
A successful Lean build does not prove that the real compiler is correct. Conversely, a mismatch is not a failed formalization. It is a valuable result showing that the specification, model, adapter, or implementation disagrees with another layer.
ADR / language specification
|
v
Lean semantic model ---- proofs and broken-model witnesses
|
v
versioned generated corpus
|
v
implementation adapter
|
+---- checker
+---- compiler
+---- runtime
|
v
match / mismatch / infrastructure error
|
v
minimal counterexample + issue + regression guard
In this architecture, Lean is the source of truth for expected semantics and the implementation is the observed system. If the specification is ambiguous, do not silently change the expected result to match current behavior. Present the smallest input and both outcomes to the domain owner, then record the decision.
Do not begin by formalizing the parser, resolver, type checker, code generator, and runtime together. Retain only the types and rules required to decide the property under investigation.
For call typing, a useful first slice may contain only:
- primitive types
- nominal types with recursively visible type arguments
- type variables
- function signatures
- positional and labeled arguments
- type-variable substitutions
- an accept-or-reject decision
inductive Ty where
| int
| string
| array (element : Ty)
| var (index : Nat)
deriving DecidableEq, Repr
structure Signature where
parameters : List Ty
result : Ty
deriving DecidableEq, Repr
inductive Verdict where
| accept (result : Ty)
| reject (reason : String)
deriving DecidableEq, Repr
def checkCall (signature : Signature) (actual : List Ty) : Verdict :=
if signature.parameters.length ≠ actual.length then
.reject "arity-mismatch"
else if signature.parameters = actual then
.accept signature.result
else
.reject "type-mismatch"In a real model, make successful checking return more than a Boolean. A proof-carrying result can retain resolved arguments, a substitution, the return type, and evidence that all of them follow the rules. Later theorems can reuse the fact that every accepted call is well typed.
Document where the model begins and what it excludes. For example: “This model begins after parsing and name resolution” and “Diagnostic wording and Wasm representation are out of scope.” These boundaries do not hide weaknesses; they state precisely what has and has not been established.
With negative cases alone, an oracle that always rejects can pass. With positive cases alone, an oracle that performs no checking can pass. For each rule, include at least:
- a sanity case that must be accepted
- a counterexample that must be rejected
- a deliberately broken checker with the important rule removed
For example, a checker that compares only the outer constructor of Array[Int] and Array[String] erases the element type and accepts the mismatch.
def sameHead : Ty → Ty → Bool
| .array _, .array _ => true
| left, right => decide (left = right)
example : sameHead (.array .int) (.array .string) = true := by
native_decideThis broken witness demonstrates that the corpus can actually detect type-argument erasure. It is a small form of mutation testing.
Do not duplicate expected results by hand in shell code or in the implementation under test. Define each case once in Lean.
structure OracleCase where
name : String
issue : String
source : String
signature : Signature
arguments : List Ty
expected : Verdict
def OracleCase.actual (testCase : OracleCase) : Verdict :=
checkCall testCase.signature testCase.arguments
def OracleCase.passes (testCase : OracleCase) : Bool :=
decide (testCase.actual = testCase.expected)
def allCasesPass : Bool :=
cases.all OracleCase.passes
example : allCasesPass = true := by
native_decideEach case should contain at least a stable name, a related issue, an expected verdict, details, and a source fixture for the real implementation. A TSV record might look like this:
version 1
name issue verdict detail source
same-type-variable-mismatch #1001 reject type-mismatch fn same[T](...)
Version the corpus format so changes to the Lean-to-adapter contract are explicit. TSV is easy to inspect and consume from shell. JSON Lines is often better when observations contain nested diagnostics or multiple phases.
Committing the generated corpus makes semantic changes visible in review and lets adapters consume it without installing Lean. In CI, regenerate to a temporary file and diff it against the committed artifact. This rejects manual edits and forgotten regeneration.
lake build --wfail
lake env lean --run OracleMain.lean > "$actual"
diff -u oracle/call-typing.tsv "$actual"The adapter should only turn one corpus row into a source file, execute the target command, and normalize the result into a stable observation.
if compiler check "$source_file" >"$log_file" 2>&1; then
actual=accept
else
status=$?
case "$status" in
1) actual=reject ;;
*) actual=error ;;
esac
fiSeparate semantic rejection from infrastructure failure. A type error reported with exit code 1 is an observation. A command crash, timeout, fixture-generation failure, or unexpected exit code is not an oracle mismatch and must be reported separately.
Diagnostic strings are unstable, so begin with exit codes or machine-readable error kinds. If wording and source locations matter, treat them as a separate presentation oracle.
At minimum, distinguish these outcomes:
| Lean | Implementation | Interpretation |
|---|---|---|
| accept | reject | over-rejection, missing implementation, or an overly broad model |
| reject | accept | a soundness hole or an unresolved specification decision |
| accept/reject | error | compiler, adapter, or fixture infrastructure failure |
Observing the checker, compiler, and runtime separately also finds phase-parity bugs.
expected: reject
checker: accept
compiler: reject
runtime: not-run
This is not harmless merely because compilation eventually rejects the program. If successful check results are consumed by an IDE, build cache, or agent tool, the phase contract is broken.
A general system should use an observation vector instead of one Boolean verdict:
Observation {
parse
check
compile
run
normalized_output
}
Compare only the phases required for the property, while keeping “not run” distinct from failure.
If every mismatch fails CI immediately, an oracle cannot be introduced while known implementation gaps exist. Provide two modes:
- Report mode lists semantic mismatches but exits successfully. Infrastructure errors still fail.
- Strict mode fails when any semantic mismatch exists.
Start in report mode and build a counterexample ledger. Link every mismatch to an issue. Move a slice to strict mode once the implementation agrees. Do not make CI green by weakening expected semantics to current behavior.
The highest-value cases usually come from real incidents reduced to minimal source programs. Preserve a neighboring positive case as well as the failing case.
Enumerate a finite subset of types, effect rows, patterns, or state transitions in Lean and extract combinations that violate an invariant.
def smallTypes : List Ty :=
[.int, .string, .array .int, .array .string]
def pairs (items : List Ty) : List (Ty × Ty) :=
items.flatMap fun left =>
items.map fun right => (left, right)
def disagreements : List (Ty × Ty) :=
pairs smallTypes |>.filter fun pair =>
sameHead pair.1 pair.2 && decide (pair.1 ≠ pair.2)This resembles bounded model checking. It is not a proof over the infinite domain, but it naturally produces concrete and already-small witnesses.
Remove type-argument comparison, erase effect rows, check only arity, or remove a cancellation-point restriction. If the corpus cannot distinguish the broken variant from the real model, it needs more cases.
A property-based testing tool can generate and shrink source ASTs while Lean supplies the semantic expectation. Remember that the source-to-model translator then becomes another component whose correctness must be tested.
- Extract one allowed, forbidden, or invariant claim from a specification, ADR, or bug.
- Add the corresponding Lean example first and observe an undefined-name or proof-failure Red.
- Implement the smallest types, rules, and cases needed to make Lean Green.
- Confirm that a broken variant accepts the counterexample, proving the test is load-bearing.
- Regenerate the corpus only from Lean.
- Run the implementation adapter in report mode.
- File each mismatch with the minimal source, expected result, observed result, and affected phase.
- Keep the case after the implementation is fixed and promote the slice to a strict gate.
Lean does not need to run on every ordinary change when the formal model is untouched. A path-filtered workflow can run only for:
on:
pull_request:
paths:
- "formal/**"
- ".github/workflows/formal.yml"A useful job split is:
- Lean build and theorem checking
- generated-corpus freshness
- adapter unit tests
- implementation differential report
- strict correspondence for slices with zero known mismatches
To detect implementation regressions, run a lightweight corpus adapter in normal CI or in another job filtered to the relevant implementation paths.
Lean is a strong fit for semantics intended to remain a durable source of truth: type-and-effect relations, handler rules, module visibility, transition systems, and scheduler invariants.
Ordinary property or differential tests are often cheaper for:
- exact diagnostic wording and colors
- formatter whitespace
- backend-specific numeric corner cases
- OS, filesystem, and network integration
- performance thresholds
If one of these contains a durable mathematical contract such as round-trip preservation, no out-of-bounds access, or exactly-once execution, formalize that abstract property and test implementation correspondence separately.
vibe-lang generates a versioned TSV corpus from a Lean call-typing model and feeds each source fixture to its self-hosted checker.
In the 2026-07-19 expansion, 22 of 25 cases matched and three remained as explicit counterexamples:
- a nominal-head mismatch between
ResultandOption - a nested nominal-type mismatch
- checker/compiler disagreement for mixed positional and labeled arguments
The Oracle was not weakened to match current behavior. The gaps were recorded in Issue #1001. PR #1002 adds cases for repeated type-variable correlation, nested generics, arity, argument modes, and broken-model witnesses.
The important claim is not “Lean proved the real compiler.” Lean made the semantic expectation executable and reviewable, while the bridge continuously turned implementation disagreement into reproducible source programs.
- The source of truth and observed system are distinct
- The model's starting point and exclusions are documented
- Positive cases, negative cases, and broken witnesses exist
- Successful checking retains evidence
- The corpus is generated only from Lean
- The corpus format is versioned and deterministic
- Semantic rejection and infrastructure failure are distinct
- Report and strict modes are separate
- Mismatches are preserved as minimal sources and linked issues
- Phase parity is observed across checker, compiler, and runtime when needed
- Lean model correctness and implementation correspondence are not called the same proof