6 ms·

Suppose I write a distributed algorithm in Rust. To verify it, I might describe the algorithm again in TLA+, model-check that specification, and prove that it s

by _tgxm 1mo ago

Suppose I write a distributed algorithm in Rust. To verify it, I might describe the algorithm again in TLA+, model-check that specification, and prove that it satisfies the properties I care about. Now I have two artifacts: TLA+ specification --> proved Rust implementation --> runtime But the proof establishes something like: TLA_Spec => Safety What I actually need is: Rust_Program => Safety I believe this is called model-code gap and there are ways to address it but I haven't found an easy-to-follow approach.

david-gpu 1mo ago
I last touched formal verification methods 20 years ago. Back then, Coq had the capacity to automatically transform your proof into OCaml. I would have expected that this would have only gotten better with time.
- djsjajah 1mo ago
  It’s been renamed recently. Maybe a few times. I think it’s rocq now. [1] [1] https://rocq-prover.org/docs https://rocq-prover.org/docs
  - Nail2680 1mo ago
    Huh, I missed all of that. The linked discussion about the renaming from your link was a bit odd: https://discourse.rocq-prover.org/t/coq-community-survey-2022-results-part-iv-and-itp-paper-announcement/2001#renaming-coq-8 https://discourse.rocq-prover.org/t/coq-community-survey-202... It seemed to me from the survey that most people didn't want it changed or didn't care, but due to anglophone users they decided to change it anyway.
black_knight 1mo ago
I saw a fascinating talk by Clément Pit‑Claudel on closing this gap. I don’t have references handy but his website seems like a starting place: https://pit-claudel.fr/clement/ https://pit-claudel.fr/clement/ As I remember it, he was formalising compilation by connecting the semantics of the higher level to the lower level one inside the proof assistant, so that proofs would carry through.
deleted 1mo ago
[deleted]
y1n0 1mo ago
Something like TLA is to prove the design of an algorithm is what you intended. Proving a specific implementation in a specific language is really the domain of that language or tools targeting that language. In digital design for example, SystemVerilog has a whole sub-language for specifying formal properties that can be proved in simulation or with tools that prove the properties mathematically.
baq 1mo ago
LLMs are pretty good at this. Not perfect by any means as the model is just a model after all - always wrong, sometimes useful - but the act of writing a TLA+ model helps the frontier LLMs to write correct executable code. It also works the other way around - given code, it can build a model in TLA+ and find latent bugs which it'll likely miss otherwise. (https://github.com/specula-org/Specula https://github.com/specula-org/Specula)
rrook 1mo ago
I think the reality is that it has to be baked into the language. Here's my real attempt at that - if you model the system in the language, the compiler can reason about the distributed fleet: https://hale-lang.org/proof/ https://hale-lang.org/proof/
JCattheATM 1mo ago
> I believe this is called model-code gap and there are ways to address it but I haven't found an easy-to-follow approach. I would say Ada SPARK solves this problem.
- ajdude 1mo ago
  Not just that, I've been seeing a huge effort in the Ada community to leverage LLMs to convert a lot of libraries into formally verified SPARK code. One of the biggest issues I see with vibe coded stuff is that it's difficult to review and difficult to prove that it's doing what you think it's doing, but with a strongly type language like Ada and formal verification with SPARK, LLM output is easy to read and easy to prove.
nylonstrung 1mo ago
I think the gap is real and for it to be resolved, the spec language needs to be elevated to a source of truth and possibly do some degree of codegen, which is currently not well realized with Lean The analogy I'd make is to the idea of "type driven development" that buf/protoc represent, where one defines their types and schema in proto and then types for specific languages are generated from that The limitations there however is that proto is not a programming language and inflexible/inexpressive whereas Lean is one of the most expressive languages to date
noosphr 1mo ago
Apply this to building a house and complaining that the architecture drawings don't include the technical drawings. The two are different artifacts for different jobs. The same is true for code and architecture. That they have an impedance mismatch is a feature.
- inigyou 1mo ago
  It would be even better if there was a machine that could take your architecture and technical drawings and alert you of any mismatches.
japgolly 1mo ago
In my opinion, it's not very different than writing an implementation of quicksort by looking at pseudocode in an algorithms book. You still need to write unit/property tests for your implementation if you want to verify it to be correct. Any time you code up an externally specified algorithm, the onus is still on you to verify your implementation, even if the correctness of the algorithm is already verified.
yencabulator 1mo ago
This is why I'm more interested in the kinds of formal methods that integrate with the actual program source code. A couple of examples, in a rough order of approachability by a working programmer: https://github.com/model-checking/kani https://github.com/model-checking/kani https://github.com/flux-rs/flux https://github.com/flux-rs/flux https://github.com/viperproject/prusti-dev https://github.com/viperproject/prusti-dev https://creusot.rs/ https://creusot.rs/ I really wish one of these projects overcomes its academic origins and becomes a software development tool. Kani is closest to that pragmatism, but correspondingly its theory side is not quite as powerful -- though it's been getting new features that make real code easier to deal with, earlier when I played with it it could only reason about very simple functions. Flux also looked surprisingly approachable, but I haven't used it in anger yet. There's hope that Rust will include language-level conventions for expressing contracts that all these tools can then take advantage of, because e.g. a `verus! {}` macro wrapping everything was never gonna be a viable way forward, and hopefully this will also gives us a syntax that looks like programming not math (I'm looking at you, Creusot): https://github.com/rust-lang/rust/issues/128044 https://github.com/rust-lang/rust/issues/128044

by _tgxm 1mo ago

david-gpu 1mo ago

I last touched formal verification methods 20 years ago. Back then, Coq had the capacity to automatically transform your proof into OCaml. I would have expected that this would have only gotten better with time.

djsjajah 1mo ago
It’s been renamed recently. Maybe a few times. I think it’s rocq now. [1] [1] https://rocq-prover.org/docs https://rocq-prover.org/docs
- Nail2680 1mo ago
  Huh, I missed all of that. The linked discussion about the renaming from your link was a bit odd: https://discourse.rocq-prover.org/t/coq-community-survey-2022-results-part-iv-and-itp-paper-announcement/2001#renaming-coq-8 https://discourse.rocq-prover.org/t/coq-community-survey-202... It seemed to me from the survey that most people didn't want it changed or didn't care, but due to anglophone users they decided to change it anyway.

black_knight 1mo ago

I saw a fascinating talk by Clément Pit‑Claudel on closing this gap. I don’t have references handy but his website seems like a starting place: https://pit-claudel.fr/clement/ https://pit-claudel.fr/clement/ As I remember it, he was formalising compilation by connecting the semantics of the higher level to the lower level one inside the proof assistant, so that proofs would carry through.

deleted 1mo ago

[deleted]

y1n0 1mo ago

Something like TLA is to prove the design of an algorithm is what you intended. Proving a specific implementation in a specific language is really the domain of that language or tools targeting that language. In digital design for example, SystemVerilog has a whole sub-language for specifying formal properties that can be proved in simulation or with tools that prove the properties mathematically.

baq 1mo ago

LLMs are pretty good at this. Not perfect by any means as the model is just a model after all - always wrong, sometimes useful - but the act of writing a TLA+ model helps the frontier LLMs to write correct executable code. It also works the other way around - given code, it can build a model in TLA+ and find latent bugs which it'll likely miss otherwise. (https://github.com/specula-org/Specula https://github.com/specula-org/Specula)

rrook 1mo ago

I think the reality is that it has to be baked into the language. Here's my real attempt at that - if you model the system in the language, the compiler can reason about the distributed fleet: https://hale-lang.org/proof/ https://hale-lang.org/proof/

JCattheATM 1mo ago

> I believe this is called model-code gap and there are ways to address it but I haven't found an easy-to-follow approach. I would say Ada SPARK solves this problem.

ajdude 1mo ago
Not just that, I've been seeing a huge effort in the Ada community to leverage LLMs to convert a lot of libraries into formally verified SPARK code. One of the biggest issues I see with vibe coded stuff is that it's difficult to review and difficult to prove that it's doing what you think it's doing, but with a strongly type language like Ada and formal verification with SPARK, LLM output is easy to read and easy to prove.

nylonstrung 1mo ago

I think the gap is real and for it to be resolved, the spec language needs to be elevated to a source of truth and possibly do some degree of codegen, which is currently not well realized with Lean The analogy I'd make is to the idea of "type driven development" that buf/protoc represent, where one defines their types and schema in proto and then types for specific languages are generated from that The limitations there however is that proto is not a programming language and inflexible/inexpressive whereas Lean is one of the most expressive languages to date

noosphr 1mo ago

Apply this to building a house and complaining that the architecture drawings don't include the technical drawings. The two are different artifacts for different jobs. The same is true for code and architecture. That they have an impedance mismatch is a feature.

inigyou 1mo ago
It would be even better if there was a machine that could take your architecture and technical drawings and alert you of any mismatches.

japgolly 1mo ago

In my opinion, it's not very different than writing an implementation of quicksort by looking at pseudocode in an algorithms book. You still need to write unit/property tests for your implementation if you want to verify it to be correct. Any time you code up an externally specified algorithm, the onus is still on you to verify your implementation, even if the correctness of the algorithm is already verified.

yencabulator 1mo ago

This is why I'm more interested in the kinds of formal methods that integrate with the actual program source code. A couple of examples, in a rough order of approachability by a working programmer: https://github.com/model-checking/kani https://github.com/model-checking/kani https://github.com/flux-rs/flux https://github.com/flux-rs/flux https://github.com/viperproject/prusti-dev https://github.com/viperproject/prusti-dev https://creusot.rs/ https://creusot.rs/ I really wish one of these projects overcomes its academic origins and becomes a software development tool. Kani is closest to that pragmatism, but correspondingly its theory side is not quite as powerful -- though it's been getting new features that make real code easier to deal with, earlier when I played with it it could only reason about very simple functions. Flux also looked surprisingly approachable, but I haven't used it in anger yet. There's hope that Rust will include language-level conventions for expressing contracts that all these tools can then take advantage of, because e.g. a `verus! {}` macro wrapping everything was never gonna be a viable way forward, and hopefully this will also gives us a syntax that looks like programming not math (I'm looking at you, Creusot): https://github.com/rust-lang/rust/issues/128044 https://github.com/rust-lang/rust/issues/128044