Start with "246 Findings From our Smart Contract Audits: An Executive Summary" [1]
[1] https://blog.trailofbits.com/2019/08/08/246-findings-from-ou...
Projects are willing to spend up to millions to squash away vulnerabilities. For example Balancer opened a bug bounty for their v2 with $2M USD for 1 critical bug:
https://docs-v2.balancer.finance/core-concepts-1/security/bu...
Without a legal framework of smart contract enforcement, recognition of literally-hypothetical assets as valuable, the public nature of blockchains that would preclude "unauthorized access," and unlike an exchange holding assets on behalf of customers - smart contracts are effectively leaving money on the ground for anyone clever enough to pick it up.
Clearly I haven't given it as much thought as the people involved, but it seems like if I'm not using my abilities full-time to hack and loot smart contracts, I'm missing the most direct and best possible effort/reward application of that kind of skill.
Of course, if the smart contract expressly permitted anyone to take tokens out of it via any means allowed by the platform, that's a different story.
Given the general enthusiasm of blockchain proponents to believe that "the code is law", it's a pretty easy argument to make that taking advantage of poorly-written code is well within the user's authorized capabilities. Will it win in court? shrug
I would treat it essentially as arbitration on steroids; just as in arbitration, you make up an alternative process for deciding who pays whom and how disputes are resolved, so that in most cases you can use the alternate process, however, in unusual cases or boundary cases or outright fraud by one party you can escalate to the full legal system.
Are there other blockchains that are similar? Is there a strict subset and prover for Solidity or other languages? Or things like proven smart contract kernels that can be built on top of? Eg, OpenZeppelin Contracts, but with provers rather than only audits.
We use two tools to offer quick turnaround automated testing and verification for Solidity: Echidna (like QuickCheck for Solidity) and Manticore (a symbolic verifier). They each let you write high level properties in the span of 1-2 weeks that cover a large amount of potential use cases.
Here's an example of what that looks like: https://github.com/trailofbits/publications/blob/master/revi...
Here's Echidna: https://github.com/crytic/echidna
and Manticore: https://github.com/trailofbits/manticore
Sometimes we also use custom static analyses built around Slither's IR during projects too: https://github.com/crytic/slither/wiki/SlithIR
You should check out Clarity (clarity-lang.org). It's an on-chain interpreted language, so what you see is what will run. It's statically typed and decidable, such that you can reason about all the halting states of the program as well as the upper bounds on the amount of computing resources used. It's used by the Stacks blockchain and Algorand.
