Questions tagged [formal-verification]

Formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.

Filter by
Sorted by
Tagged with
3 votes
1 answer

What is a minimal symbolic execution example?

I'd like to see a minimal symbolic execution / formal verification example using the following function: function f(uint256 a) public returns(uint256){ a = a + 1; return a; } What would that look ...
1 vote
0 answers

What is an example of a runtime verification tool being used to audit a smart contract?

Runtime Verification i a computing system analysis and execution approach based on extracting information from a running system and using it to detect and possibly react to observed behaviors ...
4 votes
1 answer

What's the difference between SMT solvers and formal verification?

The question holds. What's the difference between the two? What would be an example of using these two tools on a minimal piece of solidity code?
0 votes
2 answers

Formal verification on Hardhat

Is there any tool to be able to do formal verification on hardhat projects that's open source?
0 votes
0 answers

Best Solidity code patterns to define "future ERCs"

Context: I would like to write an standard ("future ERC") with a set of rules to be respected by contracts implementing the standard. Such rules can include for example: "public ...
2 votes
0 answers

How to get the abstract model in smtlib2 format or z3 expressions from Solidity SMTChecker?

I want to get the abstract model in smtlib2 format or as Z3 expressions created by the SMTChecker. However, i cannot find any compiler switch or something to get the model. The SMTChecker ...
4 votes
1 answer

Difference between SMTChecker and Manticore?

Why would I use Trail of Bits' Manticore over SMTChecker, which is baked in the Solidity compiler?
2 votes
0 answers

Is there any free-to-use scenario builder?

The Compound Protocol has a collection of high-level integration tests, dubbed "scenarios": Which look like this: Test &...
8 votes
1 answer

What is SMTChecker used for in Solidity?

From the solidity docs: If you use pragma experimental SMTChecker;, then you get additional safety warnings which are obtained by querying an SMT solver. The component does not yet support all ...