Qwen-Solidity-Invariants

A Qwen 3 8B model fine-tuned for detecting invariants in Solidity smart contracts.

Model Description

This model is a fine-tuned version of Qwen/Qwen3-8B, optimized to identify and analyze invariants in Solidity code. It can run on GPUs with less than 12GB of VRAM thanks to 4-bit quantization.

Use Cases

• Discovering and documenting invariants in Solidity smart contracts
• Analyzing logical and economic invariants in DeFi protocols
• Cross-contract invariant detection
• Formal verification support by identifying properties to prove

Prompt Format

Analyze the function(s) below and return the held invariants. 
For each invariant, provide: 
 - Description: What the invariant ensures 
 - Expression: The format expression (use Solidity-like syntax) 
 - Criticality: high, medium, or low 
 
Return invariants in a clear, structured format.

```solidity
// Place target function source code here
function example() public {
    // ...
}
```

```solidity
// Place inner function source code here (if analyzing cross-contract invariants)
function innerFunction() internal {
    // ...
}
```

Example Input

  Analyze the function(s) below and return the held invariants.
For each invariant, provide:
- Description: What the invariant ensures
- Expression: The formal expression (use Solidity-like syntax)
- Criticality: high, medium, or low

Return invariants in a clear, structured format.

```solidity
function addGoo(uint256 gooAmount) external {\r
        // Burn goo being added to gobbler.\r
        goo.burnForGobblers(msg.sender, gooAmount);\r
\r
        // Increase msg.sender's virtual goo balance.\r
        updateUserGooBalance(msg.sender, gooAmount, GooBalanceUpdateType.INCREASE);\r
    }
```
```solidity
function updateUserGooBalance(\r
        address user,\r
        uint256 gooAmount,\r
        GooBalanceUpdateType updateType\r
    ) internal {\r
        // Will revert due to underflow if we're decreasing by more than the user's current balance.\r
        // Don't need to do checked addition in the increase case, but we do it anyway for convenience.\r
        uint256 updatedBalance = updateType == GooBalanceUpdateType.INCREASE\r
            ? gooBalance(user) + gooAmount\r
            : gooBalance(user) - gooAmount;\r
\r
        // Snapshot the user's new goo balance with the current timestamp.\r
        getUserData[user].lastBalance = uint128(updatedBalance);\r
        getUserData[user].lastTimestamp = uint64(block.timestamp);\r
\r
        emit GooBalanceUpdated(user, updatedBalance);\r
    }
```
```solidity
function gooBalance(address user) public view returns (uint256) {\r
        // Compute the user's virtual goo balance using LibGOO.\r
        // prettier-ignore\r
        return LibGOO.computeGOOBalance(\r
            getUserData[user].emissionMultiple,\r
            getUserData[user].lastBalance,\r
            uint256(toDaysWadUnsafe(block.timestamp - getUserData[user].lastTimestamp))\r
        );\r
    }
```
```solidity
function gooBalance(address user) public view returns (uint256) {\r
        // Compute the user's virtual goo balance using LibGOO.\r
        // prettier-ignore\r
        return LibGOO.computeGOOBalance(\r
            getUserData[user].emissionMultiple,\r
            getUserData[user].lastBalance,\r
            uint256(toDaysWadUnsafe(block.timestamp - getUserData[user].lastTimestamp))\r
        );\r
    }
```

Result:

Successful addGoo execution requires the external Goo burn to have succeeded for the same sender and amount before local user goo state is updated.
After a successful addGoo call, the sender's goo accrual timestamp checkpoint is reset to the current block timestamp (uint64).
On successful addGoo, the sender's stored lastBalance becomes prior computed goo balance plus gooAmount, then stored as uint128.

Hardware Requirements

Quantization	Minimum VRAM
Q4_0 (this model)	~6-8 GB

Tested to run on consumer GPUs (e.g., RTX 3060, RTX 4070).

Inference Settings

Parameter	Value
Temperature	0.3
Top P	0.8
Repeat Penalty	1.2
Context Window	8192

Limitations

• This model discovers existing invariants, not vulnerabilities
• The model may occasionally produce false positives or miss complex invariants
• Cross-contract analysis requires providing all relevant function source codes
• Results should be reviewed by a subject matter expert for completeness

Training

• Base Model: Qwen/Qwen3-8B
• LoRA Rank: 32, Alpha: 64
• Target Modules: q_proj, k_proj, v_proj, o_proj, gate_proj, up_proj, down_proj

Citations

If you use this model, please cite:

@model{qwen-solidity-invariants,
  title = {Qwen-Solidity-Invariants},
  author = {l-lyubenov},
  url = {https://huggingface.co/l-lyubenov/qwen-invariants}
}