Open davidrpugh opened 7 years ago
Relevant to actually implementing some kind of formal verification tools on the JVM...
http://babelfish.arc.nasa.gov/trac/jpf/wiki
...unsurprisingly, NASA has developed a formal verification toolkit for the JVM.
@davidrpugh I'm very interested in that! Especially since I'm still collaborating with my former colleagues at King's College in London on the verification of agent-based simulation models (you may remember the Skype presentation that I gave about my research about a year ago).
I think both formal and semi-formal approaches are useful and necessary. Formal verification is definitely crucial in the context of smart contracts. On the other hand, approximate (i.e. simulation-based) verification is great for showing and quantifying the emergence of system-level properties about auctions and marketplaces that are too complex to be analysed formally. The four rules mentioned above seem like a very good starting point. I think they should be expressible in a variant of the temporal-logic specification language that I developed and be answerable using statistical model checking. We could then show that, given a particular simulation model, the auction is incentive-compatible with a certain level of confidence (e.g. 99%) and error rate (e.g. 1%).
Such an approximate verification approach could sit on top of ESL and form part of the overall V&V process. It would be great if we could bring together these two strands of work (ESL and ABM verification).
@bherd-rb I think that we should push on this. Seems to be very interesting research topic as well as a topic that has substantial practically relevance.
The incentive compatibility (or lack thereof) of a particular auction mechanism is a critical property of a particular auction mechanism. Whilst certain classes of mechanisms are provably incentive compatible, in many such cases computing the optimal, incentive compatible allocation is an NP-hard problem. Common "greedy" heuristics that are applied to solve these auction problems in practice often result in allocations that are provably not incentive compatible.
Are there any conditions for which we can guarantee that the approximate result computed using a particular heuristic is incentive compatible? Quoting @bherd-rb from #39 ...
Formal verification of contracts and algorithms, such as auctions and markets, that process them is of huge practical relevance. The lack of formal verification of contracts developed using Ethereum's Solidity contract language has already led to the theft of millions of dollars and continues to lead to buggy contracts that limit the progress of development of Blockchain-based smart contracting solutions.
@bherd-rb As a long term project goal, could we use formal verification techniques to prove important properties, such as incentive compatibility, of the auction mechanisms that we are developing?