> But probably not that useful for building an API backed service.

At least in domains that are "important" (and perhaps everyone thinks their business/API is important?), I'd want this.

For example - Stripe. If I'm using the stripe API, I want it to be guaranteed to work exactly as documented in all scenarios, given that money is at stake?

Getting the Stripe API written in Lean is a different challenge, of course.

> an AI agent is in the critical path in production i.e. non-deterministic action may occur(albeit with recovery)

Most software verification is proved "for all possible inputs", e.g. the system maintains some invariant regardless of which sequence of actions is taken. Those inputs could be from a user interacting with the software, or they could be API calls made to our library, etc. There's no reason you couldn't model an AI agent's choices in a similar way: i.e. prove that the desired invariants hold, for all possible sequences of actions the AI component might choose.

That might be straightforward, if the AI agent is constrained to pick from a simple set of domain-specific actions. In contrast, we can't say much about a system involving an AI agent with a full Bash shell.

> What scenarios does it make sense to have a lean proof from the start?

It's usually much easier to verify software that was written and structured with that in mind; rather than trying to reason about some arbitrary blob of code after-the-fact. So, if you do want to prove stuff, it should very much be in there from the start.

> Most software verification is proved "for all possible inputs", e.g. the system maintains some invariant regardless of which sequence of actions is taken.

Without suggesting that this has no value-- it must be noted that such verification only applies on theoretical hardware and to the specific behavior in scope of the verification. Actual hardware is nondeterministic, and an algorithm can be correct while suffering from a side-channel.

We can formally verify the Verilog or equivalent too.

You cannot formally verify heat-induced transistor stability issues, solar radiation, next-cell state change caused by EMF from adjacent cells (rowhammer)....

And while possible, good luck validating systems against intentional attacks-- fault injection, power tampering, bus attacks....

It is vital that "formally verified within X scope" does not turn into the leaky abstraction "is secure". Go watch Microsoft's talk on XBox security, and what they had to do to make it as secure as it is (primarily: tightly control hardware, code, and platform). It is not something you throw AI at, and it's not something that you can generalize to the entire computing world.

You can model physical devices to arbitrary degrees of precision. Lanyon is doing it. These are not limitations of verification. Metrological models of semiconductor fabrication can even do verification over the distribution of faulty circuit outcomes.

A backend API service may have some core business logic or other properties that would be worthwhile to prove certain properties about.

We need proof systems that are designed to work with our programming languages- working with the code so it more likely represents reality. I like verus with Rust and I have a skill for using it: https://github.com/gregwebs/skills-sdlc/blob/main/skills/rus...

Cryptographic systems are actually somewhat of an awkward thing to build with lean actually because many of the things that we assume to be true with them are either straight up not true (like lack of collisions in important hashes) or beyond the capabilities of our current math knowledge.