[B! あとで読む] 定理証明ガードレールで AI エージェントに業務ルールを守らせる - freee Developers Hub
https://b.hatena.ne.jp/entry/s/developers.freee.co.jp/entry/lean-formal-verification-ai-agent-guardrails

どうせなら本番環境自体もLeanで作ったバイナリにしちゃえばいいような＞＜（一応（？）汎用のコンパイラでもあるわけだし＞＜）