tkz1312

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.