What is the state of the ecosystem for proof engineering?

[quinn-dougherty]

Describe the feature you'd like

A unified workflow for proving properties about contracts and dapps.

Suppose I'm a proof engineer tasked with formally verifying dozens of formulae about a cardano dapp and it's underlying contract. How do I reason about:

1. selecting a proof assistant
2. ingesting plutus and haskell code that my team has written as terms in that proof assistant
3. if the project is at a different stage, maybe translating the spec into such a proof assistant, (as a bonus, in such away that the proof assistant -represented spec can be leveraged by the implementation engineers).
4. other considerations that might be at play designing specs to prove the onchain and offchain code's adherence to, such as common failure modes or blindspots.

Is there some major hyperlink I haven't found that explains this?

Describe alternatives you've considered

Here are some options.

Proof assistants

• Agda 2 to leverage the plutus-metatheory labor? What are the gains here? here is a 2005 citation on translating haskell expressions into agda 2.
• hs-to-coq offers an axiomatize feature, which might make it possible to work with a critical subset of plutus in the event that coqization of all of plutus is intractable, which it should be because plutus is turing complete and hs-to-coq is restricted to total haskell.
• Revive/update K's plutus core semantics, which is currently listed as "archived"
• Right now, I can only imagine nomos being useful validating specs, I don't yet see how we would use it to validate running code. Here's a good citation regarding the overall session types / plutus interaction
• I'm vaguely aware of some production code verification done in isabelle, so I briefly duckduckwent to a paper called Translating haskell to isabelle

Did I miss any candidates?

pipelines/workflows

Something inspired by the hs-to-coq tutorial would look like

1. perhaps using git-submodules, place dapp and contract code in src-haskell/
2. codegen from haskell to a proof assistant and dump it in src-myproofassistant/
3. write your formulae, specs, and their proofs in a theories/ subdir

nix code ought to be leveraged to make this look like

1. contents of src-haskell is input to the .nix file, perhaps read directly from a github commit.
2. contents of src-myproofassistant perhaps read-only to the user, write access is restricted only to the codegen tool
3. i.e. the step from having a contract or dapp I want to prove stuff about to working in my theories/ subdir should be nix-build with some arguments, modulo the near certainty of the codegen tool not working on the whole codebase on the first try.
4. Some debugging capabilities for when the codegen tool's behavior isn't exactly what you want at first.

What sort of pipeline or workflow would other proof engineers like to have?

[ak3n]

Thanks for the questions and links!

Unfortunately there is no any major hyperlink that may help at this point. I want to recommend to post this to https://cardano.stackexchange.com/ or somewhere else to get more attention and discussion, so it won't get lost here among other issues. And because it's more about the community and collaboration of users rather than the developers yet.

I'm closing this as there is no technical issue on plutus side to resolve.

[quinn-dougherty]

I think this question provided the conversation starter I'd be looking for, but it's been largely ignored. I'll try /r/CardanoDevelopers. Thanks!