Post #1546531
2026-04-14 02:10 UTC
Replies (3)
-
@mansr@society.oftrolls.com 2026-04-14 06:04
@regehr @dpiponi If I've understood it correctly, formal verification can prove that two things are equivalent. It doesn't prove that either of them is the thing you want.
-
@david_chisnall@infosec.exchange 2026-04-14 07:18
@regehr @dpiponi The team next to mine in my last job was adopting EverCrypt. EverCrypt is a formally verified set of crypto libraries. They were proven to be memory safe. The temporal safety proof obligation was expressed as ‘no memory is accessed after it is freed’. This was proven to hold. Running it in an SGX enclave with 32 MiB of total available RAM rapidly showed how it had been achieved: no memory was ever freed. Fixing the code was fairly simple, fixing the proofs was much harder.
-
@GeorgWeissenbacher@fediscience.org 2026-04-14 14:17
@regehr @dpiponi that’s a problem with any kind of verification. In fact, that’s the validation problem (is the specification describing what we want) vs. the verification problem (does the implementation satisfy the specification). Validation would deserve a lot more focus from our community, especially in times of LLMs.