Skip to content

Comment on C*: Unifying Programming and Verification in C (2025)parent

Comments

And neither can be made as ergonomic as no verification at all. It's all about how much you need. Functional verification isn't an appropriate tool where a single bug is catastrophic.

yet nothing prevents you or your agent from changing invariants to fit the algorithm and making it incorrect.

If the thing we're trying to prove is ungrounded, it's trivially true that any verification method falls apart. You're still encoding priors in your testing methodology. No matter how robust you think your testing suite is, I can still trick it if given free reign over the codebase.

AboutSource Built by g1lg1l

Hackerly is an independent reader for Hacker News, built on the public HN API. Not affiliated with Y Combinator.