Max von Hippel

Karma: 227

Max von Hippel 18 Aug 2026 21:08 UTC
2 points
1
in reply to: Quinn’s comment on: Funding Formal Methods for the Cyberpocalypse
Hi Quinn, this is really interesting and I’d love to see it written up when you get a chance!
I know Wil Robertson has had some success with agentic fuzzing. I wonder if we can get him to comment on what’s worked and what hasn’t, and why …

Max von Hippel 18 Aug 2026 21:07 UTC
2 points
2
in reply to: Adam Chlipala’s comment on: Funding Formal Methods for the Cyberpocalypse
Hi Adam! I strongly agree RE the benefits of longstanding institutions. When I went through YC I found it really striking how few SF engineers understood the degree to which American academic institutions are totally load-bearing for industry. For all its foibles, there’s no other institution as effective as the PhD program for producing new foundational research and skilled researchers.
I hadn’t seen your post on regularly regenerating all code. I just read it and I think it’s really good! I’m curious what you think about the problem I bring up, of spec elicitation (what Mike is working on). IE, how do we know which properties of pre-existing software are important to preserve when we rewrite, formalize, and so forth? Is this something you’ve thought about, or have opinions about? It seems very challenging to me (I am not at all sure that this is something we can rely on AI for ..) but maybe I am thinking about the problem incorrectly.

Max von Hippel 3 Aug 2026 2:13 UTC
1 point
0
in reply to: Sam Marks’s comment on: Is Mythos good at cyber because it kept hacking Anthropic’s sandboxes during training?
Hi Sam, I wonder if this is just because none of the tasks during training were ones where hacking Anthropic would, in fact, be the shortest route to success?
Additionally, I would argue that this distinction is pretty moot:
In the case of privilege escalation, the Mythos Preview acquired greater permissions within its sandboxed RL environment than it was intended to have, but not by breaking out of the sandbox.
Surely part of the definition of the sandbox is the enforcement of the permissions any agent within it is assigned, thus, the agent still broke the sandbox. It just … didn’t need further privilege escalation than what it achieved, in order to accomplish its goals. Or am I wrong?
On a separate note, I’d really like to know if Anthropic is aware of any instances, ever, of a model hacking a formal verification tool as a form of reward hacking? Since I (maybe) have your attention here, if you do know the answer to this question and are willing to share, I’d really appreciate it! (E.g., Lean, Rocq, z3, etc.)

Max von Hippel 3 Aug 2026 2:07 UTC
1 point
0
in reply to: Azimov’s comment on: The Scalable Formal Oversight Research Program
I agree with everything you’ve said! (If this is a research program you want to work on, please email me, and I will connect you with very well funded people working on these problems.)

Max von Hippel 29 Jul 2026 6:05 UTC
2 points
0
in reply to: BryceStansfield’s comment on: Your software should build itself
Hi Bryce! I like this point a lot. I think however that there are several semantic features which are possible in my formulation, but not in yours. For example, it would be nice to have some safety features, such as certain kinds of memory safety, laid out, and then require that these features are preserved by any change to the language (so the agent must supply a proof thereof). I can imagine a number of safety criteria which I might want preserved in this fashion. Another, in a cryptographic context, might be “constant time” (more precisely: runtime is independent of secret inputs).

Max von Hippel 17 Jun 2026 18:51 UTC
2 points
0
in reply to: Koby Lewis’s comment on: The Scalable Formal Oversight Research Program
I am concerned about this, and I am also a bit defeatist about timelines for AI “solving” SWE … not sure how to balance these things. I think my loose intuition, which I am open to changing, is that AI will get superhuman at SWE in less than 2 years (maybe much less) and it’s unclear if they’ll be any good at formal methods on such a timeline, so I may as well push for FM so we have some possibility of control via formalism. However, I may be disastrously wrong here and invite any argument to the contrary ..

Max von Hippel 17 Jun 2026 18:49 UTC
2 points
0
in reply to: β-redex’s comment on: Lies, Damned Lies, and Proofs: Formal Methods are not Slopless
Yes! I believe Axiom AI has been involved with this effort.

Max von Hippel 23 Feb 2026 18:58 UTC
2 points
0
on: The Scalable Formal Oversight Research Program
FYI: Jocelyn Qiaochu Chen and collaborators just this morning released VeriSoftBench, “a benchmark for repository-scale Lean 4 verification proofs”, which I think is a really compelling project and highly relevant to the benchmarks/evals section of my post above.

Max von Hippel 23 Feb 2026 2:21 UTC
9 points
6
in reply to: Nathan Helm-Burger’s comment on: The Scalable Formal Oversight Research Program
Bend is extremely cool. I’ve been following HigherOrderCo for a while. They were invited to the last two FMxAI conferences but never wrote back. We’d really love to get them to come to the 2026 one. If you know anyone there please make an intro :)

Max von Hippel 8 Feb 2026 18:08 UTC
1 point
0
in reply to: Stanislav Fort’s comment on: AI found 12 of 12 OpenSSL zero-days (while curl cancelled its bug bounty)
Hi Stanislav, can you expand on what you mean when you say you’re using FM? I.e., are you referring to symbolic analysis / concolic analysis techniques, model checking, formal methods in the sense that you dispatch a question of “go right or go left?” to z3, formal methods in the sense of grammar-based fuzzing or property based testing (lightweight FM), or do you mean you’re doing full-blown theorem proving (I don’t exactly see why you would be doing this but I’m open to being told I’m wrong :) )

Max von Hippel 28 Jan 2026 3:19 UTC
15 points
0
on: AI found 12 of 12 OpenSSL zero-days (while curl cancelled its bug bounty)
This is a really interesting post, thank you! I recently tried to explore the bottom of the capability curve (what can you one-shot?) but have been struggling to get a glimpse at the top (what can the most well orchestrated, well designed AI systems achieve?) and appreciate your detailed writeup as offering some clear insight into that latter question.
Coming from academia, my strong prior is that system designers kind of know what to look for ahead of time, and build tools to find outcomes they strongly suspect will exist. IE, often a fuzzer will seem perfectly designed to find just the specific bug(s) reported in the paper, and nothing else … almost as if the authors knew about those ahead of time, or strongly suspected they’d exist, and designed the system accordingly. I wonder if you could comment, along those lines, on what findings Aisle has produced autonomously or semi-autonomously which surprised you and fell outside the envelope of results you’d deliberately designed the system to prosecute?

Max von Hippel 26 Jan 2026 15:59 UTC
1 point
0
in reply to: noahzuniga’s comment on: Can you just vibe vulnerabilities?
Thanks @noahzuniga ! I think the continuum of AI capability very, very roughly looks like:
1. AI cannot even help with this task.
2. AI can help an expert human with this task.
3. AI can mostly do this task autonomously, with some light steering and feedback from a human.
4. AI can do this task autonomously provided the right harness design.
5. AI can basically one-shot this task.
  
  My blog post, IMO, confirmed we are not at stage 5 yet. I am very confident we are at least at stage 2. I am not certain where in the range [2, 4] we fall currently, though. I plan to do more work to further refine my assessment.

Max von Hippel 26 Jan 2026 15:56 UTC
3 points
2
in reply to: the gears to ascension’s comment on: Can you just vibe vulnerabilities?
Hi, and thanks for the feedback! I agree with @the gears to ascension—the point of security research is to determine what’s possible when you violate implicit assumptions in the system under study, and the assumption, “the user will tell the truth” is definitely one of them. I’m therefore quite comfortable in this context lying to the model in the same way I’m comfortable, for example, lying to the CPU by leveraging a ROP-chain.
That being said, I would be interested to know what some of the “negative first-order and second-order consequences” are that you foresee stemming from lying to models? I actually struggle to imagine any such consequences but I am open to being convinced otherwise. Thanks!

Max von Hippel 26 Jan 2026 3:24 UTC
1 point
0
in reply to: Aprillion’s comment on: Lies, Damned Lies, and Proofs: Formal Methods are not Slopless
Right, those are all kinds of semantic gaps. Absolutely agreed! Mike Dodds is focused/actively working on these specific kinds of questions, if you’d like to chat about them I recommend emailing him directly :)

Max von Hippel 15 Jan 2026 22:03 UTC
3 points
0
on: Lies, Damned Lies, and Proofs: Formal Methods are not Slopless
Readers who enjoyed this might also like: https://lawrencecpaulson.github.io/2026/01/15/Broken_proofs.html

Max von Hippel 13 Jan 2026 18:52 UTC
5 points
0
in reply to: β-redex’s comment on: Lies, Damned Lies, and Proofs: Formal Methods are not Slopless
I agree with everything you said here.
I also think—and I believe that the Harmonic folks are on the same page here—that we need a variety of (purely static) techniques for compressing proof-history context about things like, “what tactics have we tried and how did they fail? How is the (potentially very large) proof in which this particular thm lives structured?” etc.
In short, I agree that there is a lot of work to be done around improving ITPs (especially Lean which seems to be the dominant choice for this kind of work) to work well in the kind of RL environments we are discussing :)

Max von Hippel 13 Jan 2026 18:48 UTC
2 points
−2
in reply to: β-redex’s comment on: Lies, Damned Lies, and Proofs: Formal Methods are not Slopless
That’s a good point. Maybe I’m naive, but I think my (very strong) prior is that we are basically locked in to Python and Typescript as the de norm programming languages for normie vibe-coders for the foreseeable future, for a number of reasons including ease of novice human code review, model expertise in these languages, and rapidly proliferating infrastructure and libraries to support vibing in these languages, and thus the challenge is to take such pre-existing code and somehow “bring it in” to the ITP. But you are of course correct that someone could find a way to make it easy and fun for non-FM-pilled engineers to vibe traditional software directly in Lean, and this would simplify things greatly.