As of May 31, 2023, we have updated our Code of Conduct.

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
52 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
18 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
178 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
46 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
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 ...
earizon's user avatar
  • 576
2 votes
0 answers
23 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
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 &...
Paul Razvan Berg's user avatar
4 votes
1 answer
187 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