# Proof-Carrying Evolution: Language Models Design Formally Verifiable Controllers

- Source: arXiv cs.RO
- Published: 2026-11-02T05:00:00.000Z
- RoboHot: https://robohot.news/en/items/pqqcfoxpy6vjhbmcsqu77p037
- Original: https://arxiv.org/abs/2610.42043

## Summary

The study proposes Proof-Carrying Evolution (PCE), in which a language model provides both a controller and its certificate during search; only candidates that pass certificate verification can be returned, and the deployed artifact is the control law together with its certificate. The authors compare four language models with classical search and synthesis methods on speed-limited docking, maneuvering-target pursuit, and SO(3) attitude control. Certificates for linear problems are verified using exact rational arithmetic; on SO(3), floating-point verification is followed by exact re-verification of each reported champion. The best run of each method also receives a Lean 4 proof.