Three places where we used Lean 4 alongside C++, Rust, and Python

The claim

When an engineer or an AI assistant rewrites a parser, a storage codec, or an optimization solver, unit tests check only the inputs someone wrote. Over the past four months, we wrote 9,623 lines of Lean 4 (v4.13.0) across 5 repositories (de Moura & Ullrich, 2021). Those files contain 264 machine-checked theorems with 0 sorrys and 0 custom axioms.

Industrial formal verification succeeds when scoped to complex invariants rather than full compilers or finite lookup tables (Newcombe et al., 2015; Bornholt et al., 2021). Evaluating Lean 4 across five production and research repositories established our engineering boundary for where formal proofs outperform exhaustive unit tests.

Where Lean 4 paid off, it was never used alone. In C++ (yugabyte-db), we paired 170 Lean 4 theorems with 36.0M to 251.9M differential fuzz checks and 28-run single-VM ABBA benchmarks. In Rust (what_the_log), we compiled 1,368 lines of Lean 4 to C (libWTL.a) and called it directly from cargo test via extern "C" (Cutler et al., 2024). In Python (energy_trading_vidigais), we did not verify the linear-programming solver. Instead, we exported primal-dual Karush-Kuhn-Tucker (KKT) certificates as JSON and checked strong duality in Lean 4 (McConnell et al., 2011).

Across those three codebases and our 512-line DuckDB recursive graph query model, our proofs and harnesses caught 7 C++ defects and edge cases. Those 7 findings comprised 3 pre-merge candidate fast-path defects blocked in our performance lab and 4 boundary edge cases isolated by 251.9M-input fuzzing. They also caught 1 DuckDB recursive SQL cycle bug and blocked 3 energy-bid dispatch faults, while ABBA benchmarks rejected 9 slow C++ patches. By contrast, a 1,932-line Lean 4 Python triage enum verifier confirmed 0 defects in baseline and established our finite-enum ROI boundary.

I lead Applied AI and Support at Yugabyte. The yugabyte-db engine, what_the_log (report 06), the Python triage enum verifier (report 01), and the DuckDB recursive graph query belong to our operations stack. The European energy balancing prototype (energy_trading_vidigais) is a separate research project built with Antonio Vidigal (energy dashboard).

What to do before adding Lean 4 to a systems repo

1. Bridge the model to the binary. A Lean 4 proof over a hand-transcribed function checks the transcription, not the C++ or Rust compiler. Link Lean via C-ABI FFI into cargo test (@[export]), or pair the proof with a multi-million-input differential fuzzer (McKeeman, 1998).
2. Check solver certificates instead of verifying the solver. Do not formalize simplex or interior-point solvers in Lean. Export the primal allocation and dual multipliers, and check zero duality gap in 247 lines of Lean (McConnell et al., 2011; Pnueli et al., 1998).
3. Never confuse mathematical equivalence with a speedup. A branchless clz varint patch (B1) passed 31 Lean theorems and 156.0M fuzz checks, gained +17.4% on ARM64, and lost -39.1% on AMD.
4. Skip Lean for small finite enums. If a rule checks a 4-value Severity enum (P0 to P3), an exhaustive 20-line Python test gives the same guarantee without maintaining two codebases.

Inventory across the five repositories

Every theorem across all 5 repositories compiles under leanprover/lean4:v4.13.0 with 0 sorrys and 0 custom axioms (#print axioms audited across 97 declarations in Audit.lean).

Pattern 1: C++ storage fast paths (yugabyte-db, 4,713 LOC, 170 theorems)

In October 2026, we ran a time-boxed cloud performance lab on yugabyte-db (main at c04597a6f88). We targeted RocksDB and DocDB read and seek hot paths (fast_varint.cc, doc_hybrid_time.cc, block.cc, cache.cc, skiplist.h).

To prevent subtle storage corruption, every candidate patch had to pass three gates.

1. A zero-sorry Lean 4 proof. We wrote 4,192 lines and 157 theorems in PerfEquiv/ (plus 438 LOC and 13 theorems in HLC.lean and LeaderLease.lean). Each module transcribes the baseline C++ function and the candidate fast path, proving observational equivalence.
2. Differential fuzzing (36.0M to 251.9M inputs) and G2-v4 database equivalence (1,299,104 keys). G2-v4 writes a fresh 126,324-key database per binary and cross-dumps both. It also reads a 1,000,000-key benchmark database and two 172,780-key frozen databases, requiring 100% SHA-256 hex-dump identity.
3. A step-isolation ABBA win of at least +2.0% (28 runs per arm). On e2-standard-32 (pinned cores 12 to 15), A/A noise floors were ±1.26% on readrandom, ±0.10% on overwrite, and ±0.13% on docdb-perf-test.

Five promoted C++ patches and nine rejected by hardware gates

Of 14 candidates evaluated, 5 passed all three gates and 9 were rejected or downgraded (cand15 promoted lab branch tip at 7a8f720b42).

Two findings stood out from combining Lean 4 with ABBA hardware benchmarks:

1. A proof of equivalence says nothing about instruction latency (B1 and S22). Candidate B1 replaced the shift-and-count loop in FastVarInt with __builtin_clzll and division by 7. We proved 31 theorems in FastVarInt.lean (452 LOC) and ran 36.0M fuzz checks on macOS (+17.4% speedup on ARM64) plus 120.0M on Linux. On x86_64, the clz -> mulhi(/7) dependency chain lost to the branch predictor on short varints: -12.0% to -17.0% on Intel e2 (-14.5% midpoint) and -39.1% on AMD Zen 3 (t2d). Repacking LRUHandle from 88 to 80 bytes (S22, Kiriansky et al., 2016) won +11.17% on Intel e2 reads and +4.12% on overwrite. On AMD Zen 3 (t2d), S22 flipped to -2.14% (readrandom) and -2.31% (seekrandom) while gaining +1.54% on overwrite.
2. Why component lenses beat distributed cluster benchmarks. On a 3-node RF=3 YSQL cluster (t2d-standard-4 across 3 zones), the A/A median noise floor was 6.24%. That noise floor hid S21 and S22 (+0.53% to +1.25% end-to-end). Component ABBA harnesses (±1.26% floor) are the only way to attribute storage-engine wins; the 3-node cluster test can only certify no regression.

Seven C++ defects and edge cases caught before production

Our Lean 4 models and differential harnesses exposed 3 pre-merge candidate fast-path defects in the lab and 4 boundary edge cases in existing code. All candidate-patch bugs were blocked prior to merge, all codec boundary checks were upstreamed, and zero customer production clusters were affected.

Pre-merge candidate fast-path defects blocked in the performance lab:

1. Dead lookahead prefetch in candidate S21 (S29SeekDecodeAndInsertLock.lean). In BlockIter::Seek, candidate S21 checked if (current_ + 64 < restarts_) right after MoveToRestartBlock(index). Formalizing the cursor state for S29 proved that MoveToRestartBlock updates NextEntryOffset() and leaves current_ at restarts_ on fresh iterators (s29_fresh_iter_s21_lookahead_dead). Thus S21's lookahead was 100% dead on readrandom and prefetched stale offsets on reused seekrandom iterators (-2.05% AMD t2d regression). Anchoring on NextEntryOffset() in S29 (s29_lookahead_targets_restart_offset) fixed the unshipped candidate (+3.24%).
2. Early-exit status initialization in candidate S26 (block.cc, proved in S26UpdateSecondaryIterator.lean). In the unshipped S26 fast path, early-exiting Block::NewIterator on a corrupt block called SetStatus() without Initialize(), leaving block_entry_cache_ stale (s26_set_status_only_leaves_stale).
3. Iterator pin-cleanup visibility in candidate S26 (iterator.h, proved in S26UpdateSecondaryIterator.lean). In the unshipped S26 in-place iterator reuse patch, struct Cleanup name-hid Cleanup(), leaking pinned block handles across reuses (s26_skipped_cleanup_leaks_pin).

Pre-existing boundary edge cases isolated by 251.9M-input fuzzing:

4. Signed overflow boundary at INT64_MIN (fast_varint.h). FastEncodeDescendingSignedVarInt negates v (-v), which is undefined behavior at v = INT64_MIN in C++. Under clang++ -O2, it constant-folded to c0 00. Under -O2 -fwrapv (4 failures in 251,875,692 fuzz checks), INT64_MIN encoded to 00 3f 7f ff..., reversing sort order at the extreme boundary.
5. Non-canonical trailer bit patterns (doc_hybrid_time.cc). A 3.0M-pair differential probe uncovered 50,295 one's-complement -0 alias pairs and 209,499 wrap pairs accepted with Status::OK() while violating byte-order equivalence.
6. Rejected-insert metric counter (cache.cc). When strict_capacity_limit_ rejected an insert (!s.ok()) in LRUCache::Insert, the metrics_->cache_usage gauge was incremented by charge without checking s.ok().
7. Simultaneous fresh-cluster startup race (ysql_catalog_config.cc). Starting yb-master and yb-tserver at the exact same millisecond on a fresh RF=3 lab cluster triggered a startup CHECK (num_tablets > 0).

Pattern 2: linking Lean 4 into Rust's cargo test via C-ABI FFI (what_the_log, 1,368 LOC, 31 theorems)

In report 06, we described optimizing what_the_log (wtl), our 27.6k-line Rust log-to-Parquet engine (51,954 templates). To check that parallel optimizations never corrupt parsing, burst compression, or Bloom filters, we wrote a 1,368-line Lean 4 specification (formal_spec/WTL/, 31 theorems on disk).

Three core theorems anchor WTL/Proofs.lean (470 LOC):

1. Linear parser step bound (parser_termination_and_safety). For any input string $s$, the streaming glog parser terminates in at most $10|s| + 50$ steps without backtracking explosion.
2. Lossless burst conservation (burst_compression_lossless and compressEvents_conserves_count). Decompressing a temporal run-length burst (<= 60 s span cap, 60,000 ms) recovers exact firstTs and lastTs bounds and all 9 entity columns. It also preserves exact event counts (sum(repetition_count) = N). Across 4 production benchmarks (2.62 billion total events), count conservation held with 0 discrepancies. That included 2.44 billion lines (532.8 million bursts) on 1.415 TB Bundle B14, and capping a 63.1-hour burst on B17 to 60 s.
3. Zero Bloom filter false negatives (bloom_filter_zero_false_negatives). Verified across 98 production row groups (94.7% Bloom byte reduction in report 06) with 0 false negatives.

Compiling Lean 4 to libWTL.a (RustFFI.lean, 147 LOC)

Instead of assuming our Lean functions matched our Rust code, we used Lean 4's @[export] attribute in WTL/RustFFI.lean (6 exported C-ABI symbols). Lean's Perceus compiler (Reinking et al., 2021) compiles the specification into ~485 KiB of C (Proofs.lean erases to 9,298 bytes) and builds libWTL.a.

In wtl-v2/tests/lean_ffi_differential.rs, Rust's cargo test links libWTL.a via extern "C" (8-byte Lean object header plus 58 scalar bytes in #[repr(C)]). The test suite runs 301 live differential checks against the production Rust structs (0 divergences, Cutler et al., 2024). Those 301 checks cover 100 glog lines (80 valid and 20 malformed), 100 burst-merge scenarios, 100 Bloom hash probes, and 1 schema-v8 check.

We also ran cargo-mutants (Jia & Harman, 2011) across the Rust workspace (794 unit tests, 121 total mutants). All 72 semantic data-plane mutants (parser offsets, burst bounds, and Bloom bitmasks) were killed (100.0%, plus 1 timeout kill and 1 unviable mutant). The 47 surviving mutants were CLI eprintln! strings and Vec::with_capacity hints (59.5% raw kill rate).

In-crate differential testing across 3,864 multi-wildcard templates also verified the PR #63 memoized verifier (0 divergences). Runtime on 24 x 4 MB synthetic lines fell from 900.0 s (SIGKILL) to 2.59 s (347x). Bundle B23 fell from 947.4 s to 11.2 s (85x), and Bundle B24 fell from 1,112.9 s to 11.5 s (97x).

Pattern 3: checking Python LP duality certificates before energy gate closure (energy_trading_vidigais, 1,098 LOC, 30 theorems)

In energy_trading_vidigais, our Python engine optimizes battery bids across 18 European PICASSO zones (15-minute Market Time Units, 4-second TSO cycles). Under European balancing rules, gate closure is at T-25 minutes before delivery (bid generation runs at T-30).

Verifying a numerical linear-programming solver (scipy / HiGHS) in Lean 4 would take years. Instead, we used the certifying algorithm pattern (McConnell et al., 2011; Pnueli et al., 1998). At T-26 minutes (1 minute before gate closure), a 433-line Python bridge (verify_bid_dispatch.py) exports the candidate dispatch as a JSON Karush-Kuhn-Tucker (KKT) certificate. Lean 4 checks that certificate across 1,098 LOC and 30 theorems (BalancingMarket.lean, MeritOrderProofs.lean, DualityCertificates.lean, and BatteryStateOfCharge.lean).

Lean 4 checks four decidable conditions in 2.28 seconds.

1. Primal feasibility (PrimalFeasible). Every allocation $x_i$ satisfies $0 \le x_i \le Q_i$ and $\sum x_i = D$.
2. Dual feasibility (DualFeasible). Stationarity $c_i - \lambda + \mu_i - \nu_i = 0$ holds with $\mu_i, \nu_i \ge 0$.
3. Complementary slackness and EUR 0 duality gap (primal_cost_eq_dual_objective and optimality_certificate_guarantee). Primal cost $\sum c_i x_i$ equals dual objective $\lambda D - \sum \mu_i Q_i$. Both equal EUR 3,290 on the 65 MW DE audit and EUR 3,400 on the self-test (EUR 0 gap), proving global optimality.
4. Multi-step battery State-of-Charge (SoC) bounds (trajectory_preserves_invariant). Across a 100 MWh battery with a [10, 90] MWh safe envelope (10 MWh minimum reserve floor), worst-case activation never underflows or overflows the pack.

In our adversarial test suite, the Lean 4 gate blocked 3 of 3 injected dispatch faults before submission. It rejected an out-of-merit bid ladder (80 vs 40 EUR/MWh) and a 150 MW flow exceeding a 100 MW interconnector limit. It also blocked a 30 MWh discharge from 20 MWh (-10 MWh, below the 10 MWh floor).

Defining the ROI boundary: DuckDB recursive graph query vs Python triage enum verifier

Comparing our two smaller Lean 4 deployments defines the engineering boundary between high-return formalization and finite-domain testing.

1. High-return (DuckDB recursive graph query, 512 LOC, 12 theorems + 129 LOC Python oracle). In GraphTheory.lean, modeling our DuckDB recursive CTE organizational relationship graph query exposed a subtle cycle-detection flaw (naive_cycle_check_rejects_unvisited_node, proved by native_decide). The SQL query checked INSTR(p.path_str, e.source) = 0 to prevent cycles. When "target_inc" was already in the path "target_inc -> ibm", the substring check falsely rejected organization "inc" as a cycle. We replaced INSTR with discrete list membership (NOT list_contains, verified by set_cycle_check_sound).
2. Finite-enum ROI boundary (Python triage enum verifier, 1,932 LOC, 21 theorems + 794 LOC duplicate Python kernel + 451 LOC tests). In Guardrails.lean and TicketTriage.lean, we formalized a 4-value Severity enum (P0 to P3) and a 5-value DeploymentType enum. Several theorems (quorum_loss_requires_p0, screen_url_implies_aeon_cloud) were 1-line by rfl proofs on lookup tables. The Lean proof confirmed 0 defects in our production severity and deployment lookup rules. Because production containers omit the Lean toolchain, mirroring all 1,932 lines of Lean required 794 lines in the Python verifier module. That result established our finite-enum ROI boundary and let us retire the duplicate 794-LOC Python subprocess kernel for exhaustive pytest CI checks (20 lines).

Verification gates and methodology checks

• Testing whether a Lean proof guarantees C++ performance (B1 and S22). FastVarInt.lean (31 theorems) and 156.0M fuzz checks proved B1 100% equivalent to baseline, yet ABBA benchmarks rejected it (-12.0% to -17.0% Intel, -39.1% AMD Zen 3). Mathematical equivalence is orthogonal to pipeline stalls.
• Testing raw SST file sha256sum (G1) and ldb dump (G2-v2). Raw SST file hashes failed on identical binaries due to background compaction races. Standard ldb dump --db silently output 0 bytes on .sst.sblock.0 sidecars, forcing us to build the 1,299,104-key G2-v4 iterator dump gate.
• Mutation testing the Rust + Lean FFI test suite (cargo-mutants). Rather than trusting test count (794 tests), we injected 121 mutants. All 72 semantic data-plane mutants were killed (100.0%), while 47 CLI logging and capacity-hint mutants survived.
• Injecting invalid LP certificates (verify_bid_dispatch.py). We tested non-monotone bid ladders (80 vs 40 EUR/MWh), SoC underflow (-10 MWh), and ATC overloads (150 vs 100 MW) to confirm the Lean binary exits non-zero.

Candidates and designs rejected by our verification gates

1. Nine Lean-verified C++ candidates. All 9 (B1, Wave-1, S20, S23, S24, S26, S27, S19, S25) were rejected by ABBA or Phase-0 hardware gates despite passing Lean 4 proofs.
2. S21's current_ + 64 < restarts_ lookahead check: proved dead on fresh iterators in S29SeekDecodeAndInsertLock.lean and replaced with NextEntryOffset().
3. Using 3-node RF=3 distributed benchmarks (6.24% A/A noise floor) to measure 2% to 6% storage patches.
4. DuckDB INSTR(path_str, source) = 0 cycle checking: disproved by counterexample in GraphTheory.lean.
5. Maintaining a duplicate 794-LOC Python subprocess kernel alongside 1,932 LOC of Lean 4 in the Python triage enum verifier. After the Lean proof confirmed 0 defects in the production lookup rules, we retired the duplicate kernel for direct exhaustive pytest checks in CI.

Pressure tests

Every finding was checked against the six standing fronts in Methods.

What this does not show

In yugabyte-db, the Lean 4 modules in PerfEquiv/ verify functional transcriptions of the C++ algorithms under explicit integer and byte-lane assumptions (T1 to T6 in FastVarInt.lean). They do not verify the raw C++ AST or clang++ machine code. Bridging that gap relies on the 36.0M to 251.9M differential fuzz runs and the 1,299,104-key G2-v4 database dumps.

In what_the_log, the C-ABI FFI differential suite runs 301 structured cases (100 glog, 100 burst, 100 Bloom, 1 schema). Marshaling String and CGlogPrefix across the Lean runtime boundary adds per-call overhead. High-volume equivalence over millions of lines runs through our in-crate Rust differential oracles (3,864 templates and 6.44M real lines) and 128-bit DuckDB multiset digests.

Finally, in energy_trading_vidigais, DualityCertificates.lean verifies exact integer KKT certificates (Int and Nat in EUR/MWh and MW) at T-26 minutes (2.28 s). Full multi-zone network flow with floating-point tolerances requires rational scaling before certificate export.

Reproduce

We are preparing our Rust log-to-Parquet workspace and its Lean 4 specification (formal_spec/) for open-source release under the Apache 2.0 license. Every number in this report and its four figures is recorded in numbers.json, with file integrity hashes listed in MANIFEST.md.

References

• Bornholt, J., Joshi, R., Astrauskas, V., Cully, B., Kragl, B., Markle, S., et al. (2021). Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3. Proceedings of ACM SOSP 2021. DOI.
• Chen, S., Ailamaki, A., Gibbons, P. B., & Mowry, T. C. (2007). Improving Hash Join Performance through Prefetching. ACM Transactions on Database Systems. DOI.
• Cutler, J. W., Disselkoen, C., Eline, A., He, S., Headley, K., Hicks, M., et al. (2024). Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization. Proceedings of the ACM on Programming Languages (OOPSLA 2024). DOI. arXiv.
• de Moura, L., & Ullrich, S. (2021). The Lean 4 Theorem Prover and Programming Language. Proceedings of CADE-28. DOI.
• Jia, Y., & Harman, M. (2011). An Analysis and Survey of the Development of Mutation Testing. IEEE Transactions on Software Engineering. DOI.
• Kiriansky, V., Zhang, Y., & Amarasinghe, S. (2016). Optimizing Indirect Memory References with milk. Proceedings of IEEE/ACM PACT 2016. DOI.
• McConnell, R. M., Mehlhorn, K., Näher, S., & Schweitzer, P. (2011). Certifying Algorithms. Computer Science Review. DOI.
• McKeeman, W. M. (1998). Differential Testing for Software. Digital Technical Journal.
• Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., & Deardeuff, M. (2015). How Amazon Web Services Uses Formal Methods. Communications of the ACM. DOI.
• Pnueli, A., Siegel, M., & Singerman, E. (1998). Translation Validation. Proceedings of TACAS 1998. DOI.
• Reinking, A., Xie, N., de Moura, L., & Leijen, D. (2021). Perceus: Garbage Free Reference Counting with Reuse. Proceedings of ACM PLDI 2021. DOI.