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.
11
questions
0
votes
1
answer
21
views
How do you assert a function does not revert in Certora?
In solidity, I have a function:
function do(uint256 a) public view returns(uint256) {
if (a == 25){
revert();
}
return a;
}
In Certora, how do I write a rule/invariant that this function ...
- 10.5k
0
votes
1
answer
31
views
Cause Kontrol to exit once a path has confirmed to cause an issue
I am running the kontrol formal verification tool, and it has been running for over 1.5 hours.
Is there a way to tell the tool to quit on finding a path that breaks the assertion? That way I don't ...
- 10.5k
3
votes
1
answer
63
views
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 ...
- 10.5k
1
vote
0
answers
25
views
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 ...
- 10.5k
4
votes
1
answer
341
views
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?
- 10.5k
0
votes
2
answers
75
views
Formal verification on Hardhat
Is there any tool to be able to do formal verification on hardhat projects that's open source?
- 259
0
votes
0
answers
17
views
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 ...
- 596
2
votes
0
answers
38
views
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 ...
- 21
2
votes
0
answers
31
views
Is there any free-to-use scenario builder?
The Compound Protocol has a collection of high-level integration tests, dubbed "scenarios":
https://github.com/compound-finance/compound-protocol/tree/v2.8.1/spec
Which look like this:
Test &...
- 17.3k
4
votes
1
answer
206
views
Difference between SMTChecker and Manticore?
Why would I use Trail of Bits' Manticore over SMTChecker, which is baked in the Solidity compiler?
- 17.3k
8
votes
1
answer
2k
views
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 ...
- 17.3k