Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Leanstral: Open-source agent for trustworthy coding and formal proof engineering

mistral.ai

Post reply on HN
Print view View original

211–220 of 234 posts

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#211

Post by robertwer »

I’ve never worked with formal validation (barely remember my CS course). This release looks impressive. But I'm trying to wrap my head around the near-term practical applications for everyday software.

Right now, we see a lot of business experts in enterprises tempted to use AI to impl. business logic so they don't have to wait for (or pay) software experts. Would this kind of technology help these users any time soon?

My current theory is that the real breakthrough for these non-developers will only happen when they can actually verify the result themselves without needing an another expert in the loop. But I don't see that with formal validation anytime soon.

Do I overlook something?

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#212

Post by Abstract_Typist »

discreteevent wrote: post #157
chriswarbo wrote: post #147

Earlier quoted context omitted.

> The scientific approach starts with a theory that does it's best to explain some phenomenon At the risk of stretching the analogy, the LLM's internal representation is that theory: gradient-descent has tried to "explain" its input corpus (+ RL fine-tuning), which will likely contain relevant source code, documentation, papers, etc. to our problem. I'd also say that a piece of software is a theory too (quite literal…

The ai is just pattern matching. Vibing is not understanding, whether done by humans or machines. Vibe programmers (of which there are many) make a mess of the codebase piling on patch after patch. But they get the tests to pass! Vibing gives you something like the geocentric model of the solar system. It kind of works but but it's much more complicated and hard to work with.

Nice analogy *

I guess the current wave is going to give us Sofware Development Epicycles (SDEC?)

* All analogies are "wrong", some analogies are useful

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#213

Post by tin7in »

warpspin wrote: post #185
tin7in wrote: post #163

Earlier quoted context omitted.

They are building their own infra - south of Paris and another one was announced in Sweden recently.

Then why does their list of subprocessors list Google and Microsoft "for cloud infrastructure", specifically for "Le Chat, La Plateforme, Mistral Code"? Sounds to me as if they're mainly running on Azure. Also, they're listing CoreWeave as inference provider in "EEA" area, but CoreWeave is of course also an US company. Even if they have their data center physically in the EU, it must be considered open access for the…

They are not up yet. The Paris one is expected in 2028, the one in Sweden in 2027.

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#214

Post by wazHFsRy »

markusde wrote: post #161
wazHFsRy wrote: post #105

Earlier quoted context omitted.

Does that mean your production code is lean? Or do you translate some other language code to lean to verify it?

Also a very good question btw, people do both. For some projects Lean is expressive and performant enough to use on its own (or call into using the reverse FFI), other projects use a model of a real programming language like Rust. The disadvantage of the latter is that the Lean model of Rust has to be trusted.

Do you know if there are some resources or examples of this? Especially actual production stuff, not just side projects or proof of concepts?

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#216

Post by rafph »

This is a typical AI announcement. Putting FLTEval scores ahead of explanations, copying code from Rocq and basically not explaining at all what the setup does.

The average quality of an AI announcement is that of a Memecoin. Lots of graphs, meandering text and no substance.

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#217

Post by Andrei_dev »

Yeah, this tracks. Developers who actually read what the AI spits out catch the obvious mistakes. The ones who just tab-complete their way through a whole project don't. And where it bites you isn't where you'd expect — logic bugs get caught fast. It's the boring security stuff. No input validation, CORS wide open, admin routes with no auth at all. Formal verification tells you whether a function matches its spec. The problem with AI-generated code goes a level below that. It's everything nobody bothered specifying — like "maybe don't hardcode your database credentials."

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#218

Post by michaelgdwn »

The formal verification angle is what makes this interesting. Most coding agents optimize for "code that compiles and passes tests" — that's a low bar. Curious whether the proof artifacts are persisted for audit trails or thrown away after verification.

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#219

Post by AlotOfReading »

auggierose wrote: post #183
AlotOfReading wrote: post #166

Earlier quoted context omitted.

I'm not confusing them. That's why I gave each of the numbers for SeL4 separately. Knowing whether those theorems are the right theorems for the problem can be as difficult as understanding the implementation itself. Hence the example of SeL4 where the number of theorems exceeds lines of code in the original implementation and the formal model is large. It's my experience that most people doing formal methods have se…

I think you have been confusing them. Two theorems are the same if they have the same statement (spec). A proof is not a theorem, nobody cares about when two proofs are the same or not.

Yes, and if you have the wrong theorems, the proof doesn't matter. Verification vs validation. Proofs solve verification, but the hard problem of validation remains.

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#220

Post by AlotOfReading »

xpe wrote: post #171
AlotOfReading wrote: post #88

Earlier quoted context omitted.

I don't know why you created a new account for this, but take the textbook example of a nontrivial formally verified system: SeL4. That implementation was 8.7k of C code, which correspondend to 15k lines of Isabelle that ultimately needed 100k+ lines of proof to satisfy. And that was with the formal model excluding lots of important properties like hardware failure that actual systems deal with.

> I don't know why you created a new account for this What value does this add to the conversation? I’m not seeing it: am I missing something? It comes across as a kind of insult. They made a good point in my opinion! (The “Uhm no” part got it off on the wrong foot, I will admit.) But even if you felt annoyed or didn’t agree with the point, it was substantive and moved the conversation forward. I’m here for the (genu…

That's a fair callout, I might have come in hot.

The original point I was trying to make is the distinction between verification and validation. I'm a bit surprised it's been controversial, but maybe I expressed things poorly.

Post reply on HN