3 ms·

I've been interested in any smart contract languages/VMs that are somehow more capable of being provably correct/secure. The only one I've come across is Kadena

I've been interested in any smart contract languages/VMs that are somehow more capable of being provably correct/secure. The only one I've come across is Kadena, which internally uses the Z3 prover, but I haven't looked into the source code in depth or if it's able to be applied to custom smart contracts (dApp) as well. 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.

jude- 5y ago
Disclaimer: I work on this. 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.
dguido 5y ago
Ugh, I have been advocating "Solidity--" for years and can't get funding to build it (Trail of Bits). 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/reviews/Liquity.pdf https://github.com/trailofbits/publications/blob/master/revi... Here's Echidna: https://github.com/crytic/echidna https://github.com/crytic/echidna and Manticore: https://github.com/trailofbits/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 https://github.com/crytic/slither/wiki/SlithIR

jude- 5y ago

Disclaimer: I work on this. 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.

dguido 5y ago

Ugh, I have been advocating "Solidity--" for years and can't get funding to build it (Trail of Bits). 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/reviews/Liquity.pdf https://github.com/trailofbits/publications/blob/master/revi... Here's Echidna: https://github.com/crytic/echidna https://github.com/crytic/echidna and Manticore: https://github.com/trailofbits/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 https://github.com/crytic/slither/wiki/SlithIR