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.
12
questions
0
votes
1
answer
17
views
DYOR: Smart Contract Hash vs. Audit CheckSum w/ SHA256
Stack Exchange,
First off I would like to say, as a grateful reader on many different stack forums, thank you all for the competent, articulate and drama-free solutions written on these pages. So many ...
- 1
3
votes
1
answer
63
views
Clarification on Theorem 6 from Uniswap V1 Formalized Model: e_0 < e_2 and t_0 < t_2
References:
a link to the parent site
Formalized Model Document
- 131
3
votes
1
answer
51
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 ...
- 12.2k
0
votes
1
answer
35
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 ...
- 12.2k
3
votes
1
answer
72
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 ...
- 12.2k
1
vote
0
answers
26
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 ...
- 12.2k
4
votes
1
answer
683
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?
- 12.2k
0
votes
2
answers
98
views
Formal verification on Hardhat
Is there any tool to be able to do formal verification on hardhat projects that's open source?
- 379
2
votes
0
answers
57
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
32
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 &...
- 18.5k
4
votes
1
answer
228
views
Difference between SMTChecker and Manticore?
Why would I use Trail of Bits' Manticore over SMTChecker, which is baked in the Solidity compiler?
- 18.5k
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 ...
- 18.5k