Skip to main content
Share Your Experience: Take the 2024 Developer Survey

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
0 votes
0 answers
16 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
Vegetal605's user avatar
2 votes
1 answer
41 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 ...
Patrick Collins's user avatar
0 votes
1 answer
34 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 ...
Patrick Collins's user avatar
3 votes
1 answer
70 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 ...
Patrick Collins's user avatar
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 ...
Patrick Collins's user avatar
4 votes
1 answer
561 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?
Patrick Collins's user avatar
0 votes
2 answers
93 views

Formal verification on Hardhat

Is there any tool to be able to do formal verification on hardhat projects that's open source?
Josep Bové's user avatar
2 votes
0 answers
52 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 ...
Hassan's user avatar
  • 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 &...
Paul Razvan Berg's user avatar
4 votes
1 answer
219 views

Difference between SMTChecker and Manticore?

Why would I use Trail of Bits' Manticore over SMTChecker, which is baked in the Solidity compiler?
Paul Razvan Berg's user avatar
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 ...
Paul Razvan Berg's user avatar