If you use agents to generate formal verification, how do you tell if the properties that are verified are the correct ones?

In my view, AI currently relies primarily on human-developed tools for verification. Although AI has used some reinforcement learning (RL) algorithms to identify the paths humans have taken at each level, these paths are essentially still based on human mathematical tools and require confirmation by human experts. We need a more revolutionary framework to provide AI for mathematics with new methods and verification pathways.

You don't. You place unwavering faith in the machine god.

This is why, for formal methods to really be the next step, we'll need deterministic source to CoC language compilers, and we'll need to go back again.

Lean is kind of an unfortunate, cargo cult choice because it only compiles to C. Really for software we should use a prover that has a lot more targets, like Danfy. Even Rocq (formerly Coq) can compile down to several functional languages, which is more than we can say for lean.

As usual, the AI crowd latched on to the first solution that came to mind, and thanks to its prominence in mathematics applications recently just lazily are starting to try and apply it to computing, without actually understanding anything or weighing trade offs. Of course, now we are basically stuck with Lean since the models will have been trained hard on it. At least it's a CoC language, but now we need to build a bunch of extra compilation around it for this to really work.

Most of this feels fairly orthogonal to the question asked. And the reasons lean are chosen are fairly simple: it is designed to also be used for programming and it's actually successful. Compiling to C is fairly obviously a bad choice (well I guess not obviously, people keep implementing languages this way for some reason) but arguably one of the least important factors in choosing which prover to use. The alternatives to lean would be Idris (which is both unsound and unpopular), ats (which is unpopular) or rocq (which is more reasonable but still is mostly an academic project).

Compiling to C seems obviously an excellent choice for compiling a language to. It is a good choice as a target language, and one can rely on a lot of existing tooling, a stable standard, good interoperability, and wide platform support. It is also simply enough to be modeled precisely.

make no mistakes

mostly jk, although agents themselves are of course getting better at detecting whether a formal spec is faithful to a natural language spec

Applications: implications, simulations, and experiments. Gobble the frontier; wring out the usable.

This reads as gibberish.

KeyError localizes the issue to the lookup (ie “right here this key should be present and it’s not) vs later in the code where it can be hard to trace where the None value came from or how to handle it.

Well... yeah but at the cost of halting your entire program? As opposed to logging?

Think of it like an assert.

Sometimes you do want some flow to terminate if a schema / data contract is breached, and not have this broken data contract propagate elsewhere / outwards.

And/or, it is a perfectly valid pattern to indeed add try..catch, and contain (hence "localize") the issue there and then. If there is a way to handle this breach - you will need some kind of if check anyway. Catching by matching against the particular KeyError exception is in fact robust - and if you forgot to add an intended catch, then the exception will propagate upstack, yes - which is what you want - and this way you do not need to worry about forgetting an "if None" check.

This sort of approach makes it structurally impossible to "forget" - if exception is not caught, it will abort the cannot-be-null breach continuing with program flow, possibly (e.g.) ending up persisted in some place it shouldn't be, causing problems later.

Python uses `except`, not `catch`.

...sure, that's true :) but you get the point. p.s. and the software design pattern applies in general, imho.

yes, that makes sense. Thank yu so much!

How would you recommend others get access to the kind of support that worked for you? Is there a specific type of therapist or coach?

They also halved API prices with GPT-6, so I think it’ll net out pretty close for sol and Luna, but much less to be used for Astra.

I probably incorrectly read

> we provide that customer’s connection to the internet

as providing the DNS infra for their customers.

What plans did you put in place? What did you do to ensure knowledge transfer?

Strict WIP limits, all non-trivial projects need two human collaborators who are both responsible for understanding and signing off on the project plan, docs, code, test strategy, etc., and regular sync-up meetings.

So do you still have humans doing code review? What did “sign off on code” look like in practice? (We’ve been thinking about this a lot too)

Yes, human code review is back. AI is allowed to help, but we require that two actual humans actually understand every change. And yeah, it did speed things up. Not the rate at which we were shipping code, of course. But the rate at which we were shipping usable product.

This is actually in line with a well-established Six Sigma practice. When you've got a poorly performing value chain, the first thing to do is find out which step is struggling and then force the step immediately before it to slow down. If the reason why isn't obvious, search for a clip of the I Love Lucy chocolate factory scene on YouTube for a perfect explanation.

"We reinvented everything and called it a success"

It seems like you're saying "This is a platform to iterate on your agents and make them better over time", but the headline of your site does not communicate that at all.

Your website is full of AI-isms, which makes it hard to parse what you're doing. (3 punchy sentence headline, "X is not Y." , "never able to claim").

Sounds like you have a cool product, try writing at least the front page of your site yourself and it'll be much much more engaging.

What does "changing the specialist" mean? changing the model? The prompt?

Thank you - you are right on both the headline issue and AI-isms. We will work on these.

Changing the specialist means changing: the prompt, the tools, the model, or some harness configurations we expose. In practice, coding agents typically try different tool sets in the first few dozens of variants, then mostly play with the system prompt with some set of "good" tools they find.

> I expect the gruesome writing style of LLMs to be fixed relatively soon, seeing how it can already be prevented with just a few lines of stylistic instructions

What instructions do you use to prevent the gruesome writing style? I have… not found this to be the case.

Currently I append the snippet below to prompts where I care about the resulting text. Just putting it in the context up front isn't as effective, and I assume if the overall prompt is large, or the context window is full, it will also be less effective.

> Use plain, clear, everyday language with a linear deductive flow; avoid hyperbole, juxtapositions, metaphors, analogies, punchlines.

I’ll try it thanks! I just got good mileage out of “don’t use ‘X, never Y’ format” on a document too, but I think linear deductive flow Covers it

Agreed. Throwing it back into an AI tool to condense it helps, but def hard to read.