tkz1312

I was surprised to discover recently that C++ is in a pretty nice sweet spot for verification (at least at the binary level), where it has some useful type system features, but will get out of your way and generate simple ASM (without e.g. spamming bounds checks and panics everywhere as rust does).

wasn't it setup in an unexploitable configuration (not actually serving a php page IIRC?) for most of the time, and then got popped within like 2 hours once fixed?

Another article about scaling agents that waffles around for ages and doesnt mention proof systems. Proof systems work. Proof systems let your robots generate thousands of lines of code and you know it's bug free without having to check a single line. Proof systems let you review and iterate on a contained and simple system model and then use those guarantees across huge parts of your code.

Just giving up and ceding control of our codebases to the robots is not a serious engineering proposition.

Sounds like you would have been in support of the US export bans on cryptography back in the day ;)

The groups with a lot of resources are always going to have the best tools available. The question is what tools do I (a person with limited time and resources) get access to. I am in a better position if the delta between my tooling and their tooling is minimized.

Because the people I want to defend against includes those with enough resources to train and fine tune models with strong offensive capabilities themselves.

I am a defender, and I really really want to have access to high quality models that are good at finding vulns and hacking. Leaving them in the hands only of government agencies and orgs with enough resources to do extensive training / fine tuning seems like the absolute worst possible case for the future security of global software systems.

Semantics of a language describe the behaviour of a sentence in that language when executed. When you have semantics in a theorem prover you can construct equivalence proofs between programs expressed in different languages (or proofs that a compiler from one language to another is semantics preserving).

I was mostly referring to accuracy when I said "good" above, in the sense that they should reflect the actual behaviour of the language they describe.

You don't really need compilers anymore. LLM's can write programs over any AST and provide an equivalence proof provided you have good semantics for the source and target.

I've been extracting a lot of verified C from theorem provers recently.

sure zero was a bit strong, but I personally feel pretty good about depending on only the go stdlib, compared to pulling in litellm.

Claude will write you something custom that fits your exact requirements with zero supply chain risk in an afternoon.

You can batch calls if you're serving a lot of people at once.

I only ship code I don't understand if it comes with a proof of correctness

Using nix to generate k8s yaml is actually quite pleasant. You avoid all the string templating bullshit and can use nix functions and the nixos module system to build proper abstractions.

distillation and the Chinese open weights models is pretty the only thing that still makes me feel like there is hope that AI might have a positive impact on society.

llms work best on optimization problems. especially when wrapped in a proof system.

I'm pretty convinced most serious software will have some kind of proof system inside within the next few years.

You don't need to review proof code.

In the last 9 months or so llms have gone from just another useful proof tactic (like grind or sledgehammer or sat solvers) to being so good at writing proofs that I don't even bother to try myself anymore.

As someone who has done software verification professionally for many years the last 6 months or so have looked extremely vertical. The robots are better proof authors than I probably ever could be even if I dedicated the rest of my days to the practice, and projects that once would have taken months now take a day or two.

It's surprisingly easy to prove something subtly different than you intend actually. Digesting and understanding a theorem statement can often take significant time and expertise.

well you can just have much stronger safety guarantees in a theorem prover than in the rust type system, and C is a much easier thing to embed in a theorem prover than rust.

I know how they work pretty well and most days I still have moments where I am struck by how bizarre and magical these thinking machines are.

I fully expect formally verified C to become the standard for any reasonably critical software. It's astonishing how easy it is to crank out program equivalence proofs these days...

the only substantive difference I've noticed is between languages with a proof system and those without, where with a proof system is orders of magnitude better for agentic work.

I'm assuming you have not spent a lot of time trying to prove stuff about non trivial programs if the trade offs between SMT based approaches and interactive theorem provers are not clear to you.

SMT solvers are highly automated, but very opaque and hard to debug. Interactive theorem provers can scale to larger problems and harder properties at the cost of increased manual proof burden. The ever increasing ability of llms to write proofs in a theorem prover has in recent years tipped the balance significantly towards preferring itp based approaches over pure SMT ones. The current state of the art for program verification is probably a mix of llm and traditional (tactics, SMT, etc.) proof automation inside an itp.

conversations on this site about formal methods are currently absolute cess pits of dunning kruger and confidently stated yet highly misinformed takes from those with close to little experience in the field.

reviewing the definitions and theorem statement is a huge amount of work that requires a deep expertise in mathematics and lean. checking correctness of the proof itself can be delegated to machine, checking that the claim that has been proved is free of mistakes is something that still requires much human attention.

I mean it obviously impacts the people who live in the Congo...