The tricky part is that prompts can look “correct” but still behave unpredictably depending on phrasing.
Leanstral: Open-source agent for trustworthy coding and formal proof engineering
201–210 of 234 posts
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#202It’s great to see this pattern of people realising that agents can specify the desired behavior then write code to conform to the specs. TDD, verification, whatever your tool; verification suites of all sorts accrue over time into a very detailed repository of documentation of how things are supposed to work that, being executable, puts zero tokens in the context when the code is correct. It’s more powerful than ream…
[flagged]
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#203It’s great to see this pattern of people realising that agents can specify the desired behavior then write code to conform to the specs. TDD, verification, whatever your tool; verification suites of all sorts accrue over time into a very detailed repository of documentation of how things are supposed to work that, being executable, puts zero tokens in the context when the code is correct. It’s more powerful than ream…
> That’s because it encodes details, not intent. Be careful here - make sure you encode the right details. I've seen many cases where the tests are encoding the details of how it was implemented and not what it is intended to do. This means that you can't refactor anything because your tests are enforcing a design. (refactor is changing code without deleting tests, the trick is how can you make design changes without…
While you are right that you need to be encoding the right details, I disagree on the tests enforcing a design point.
As part of the proper testing strategy, you will have tests that cover individual behavior of a small block/function (real "unit" tests), tests that cover integration points only up to the integration itself, and a small number of end-to-end or multi-component integration tests.
Only the last category should stay mostly idempotent under refactoring, depending on the type of refactor you are doing.
Integration tests will obviously be affected when you are refactoring the interfaces between components, and unit tests will be affected when you are refactoring the components themselves. Yes, you should apply the strategy that keeps it under incremental reverse TDD approach (do the refactor and keep the old interface, potentially by calling into new API from the old; then in second step replace use of old API as well, including in tests).
Tests generally define behavior and implementation in a TDD approach: it'd be weird if they do not need changing at all when you are changing the implementation.
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#204Formal verification and code synthesis feel like natural companions for automated scientific discovery. I’ve been working on a small (~800‑line) Python agent that uses sparse regression to uncover governing equations directly from data; it’s managed to validate twelve physical laws, including deriving the Sun’s rotation rate from NASA plasma measurements and correcting Gemini’s plasma conservation. Having an agent like Leanstral that can reason about proofs and specifications would be a powerful complement to data‑driven model discovery — it closes the loop between experimentation and provable correctness.
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#205Earlier quoted context omitted.
Is it though? Most people I know that use agents for building software and tried to switch to local development, every single time they switch back to Claude/codex. It's just not worth it. The models are that much better and continue to get released / improve. And it's much cheaper unless you're doing like 24/7 stuff. Even on the $200/m plan, that's cheaper than buying a $3k dgx or $5k m4 max with enough ram. Not to…
A single DGX Spark can service a whole department of mathematicians (or programmers), and you can cluster up to 4 of them them to fit very large models like GLM-5 and quants of Kimi K2.5. This is nearing frontier-level model size. I understand the value proposition of the frontier cloud models, but we're not as far off from self-hosting as you think, and it's becoming more viable for domain-specific models.
That's great news- I wonder if that will help drive cloud costs down too
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#206[flagged]
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#207It’s great to see this pattern of people realising that agents can specify the desired behavior then write code to conform to the specs. TDD, verification, whatever your tool; verification suites of all sorts accrue over time into a very detailed repository of documentation of how things are supposed to work that, being executable, puts zero tokens in the context when the code is correct. It’s more powerful than ream…
That matches what I’ve seen as well — generation is the easy part, validation is the bottleneck.
I’ve been experimenting with a small sparse-regression system that infers governing equations from raw data, and it can produce a lot of plausible candidates quickly. The hard part is filtering out the ones that look right but violate underlying constraints.
For example, it recovered the Sun’s rotation (~25.1 days vs 27 actual) from solar wind data, but most candidate equations were subtly wrong until you enforced consistency checks.
Feels like systems that treat verification as the source of truth (not just an afterthought) are the ones that will actually scale.
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#208[flagged]
There are also software model checkers that can model distributed processes. You have to simplify the state a bit, otherwise you get a state space explosion.
I tried it out myself, I let AI add action transitions through the code, like: // A -> B: some description. Then I validate via a test that every action transition defined in my model is also defined somewhere commented in code, and other way around that every comment exists in the model.
Finally, I let AI write model check queries on particular properties. If I notice a particular bug, then I ask AI to analyze the model and the model check queries on why it could happen, and ask to strengthen it.
It sounds like a lot of effort, but I got it working in a half hour.
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#209I just feel like Mistral is heading for bad financial times when they are focusing on fringe academic areas and not on building a business out of their research. Initial Mistral was largely based on LLaMA, then they added innovative MoE and since then disappeared, doing AI consulting for big EU companies instead.
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#210Earlier quoted context omitted.
> That’s because it encodes details, not intent. Be careful here - make sure you encode the right details. I've seen many cases where the tests are encoding the details of how it was implemented and not what it is intended to do. This means that you can't refactor anything because your tests are enforcing a design. (refactor is changing code without deleting tests, the trick is how can you make design changes without…
While you are right that you need to be encoding the right details, I disagree on the tests enforcing a design point. As part of the proper testing strategy, you will have tests that cover individual behavior of a small block/function (real "unit" tests), tests that cover integration points only up to the integration itself, and a small number of end-to-end or multi-component integration tests. Only the last category…
Fine, but don't check in the tests that prove implementation since they will be deleted soon anyway. The only tests to check in are ones that - by failing - informed you that you broke something. We don't know which those tests are and because most tests run fast we tend to check in lots of tests that will never fail in a useful way.