| caching | Enable caching of verification results. The possible values are 0 (disabled) and 1 (enabled). | yes | 0 |
| projectLocation | Location in which the project is located in the workflow context. By default, it looks in a folder with the same name as the repository. | no | — |
| includePaths | Directories used for package lookup. Their paths are relative to the project location. | no | — |
| enableFriendClauses | Enable friend package invariants (experimental). | no | 0 |
| files | List of Go and Gobra files to verify. | no | — |
| packages | Names of the packages to verify. By default, all packages are verified. | no | — |
| excludePackages | Names of packages that should not be verified. This option takes precedence over the `package` option. | no | — |
| recursive | Verify nested packages recursively | no | 0 |
| respectFunctionPrePermAmounts | Respects precise permission amounts in pure function preconditions instead of only checking read access, as done in older versions of Gobra. This option should be used for verifying legacy projects written with the old interpretation of fractional permissions. New projects are encouraged to set this flag to false. | no | 0 |
| overflow | Check for arithmetic overflows in integer expressions. | no | 0 |
| chop | Maximum number of files in which a file can be split with the chopper feature of Gobra. Larger values may improve the verification time of large codebases. | — | 1 |
| viperBackend | Which Viper backend to use. Can be one of "SILICON", "VSWITHSILICON", "CARBON", and "VSWITHCARBON". | yes | SILICON |
| javaXss | Java stack size. Should be increased in case of frequent stack overflows. | yes | 1g |
| javaXmx | Maximum size of the heap. | yes | 4g |
| timeout | Time-out for the verification job. Note that a GitHub workflow step times-out automatically after 6 hours. | no | 6h |
| imageName | Base image of Gobra to be used. | yes | ghcr.io/viperproject/gobra |
| imageVersion | Version of the base image to be used. | yes | latest |
| headerOnly | Whether Gobra should only verify files with the header "// +gobra". | no | 0 |
| module | Name of current module that should be used for resolving imports. | no | — |
| assumeInjectivityOnInhale | Assume injectivity of the receiver expression when inhaling quantified permissions, instead of checking it, like in Viper versions previous to 2022.02. | no | 1 |
| checkConsistency | — | no | 0 |
| mceMode | Exhale Mode used together with a silicon-based backend. It can be enabled ("on"), disabled("off"), or enabled on demand ("od"). | no | on |
| parallelizeBranches | Parallelize branches in the silicon backend. | no | 0 |
| requireTriggers | Require that all quantifiers have user-provided triggers. | no | 0 |
| conditionalizePermissions | Tries to reduce the number of branches that Gobra has to deal with the option --conditionalizePermissions | no | 0 |
| disableNL | Disable non-linear integer arithmetic. Non compatible yet with Carbon | no | 0 |
| moreJoins | Specifies if silicon should be run with more joins completely enabled ("all"), disabled ("off"), or only for impure conditionals ("impure"). | no | off |
| unsafeWildcardOptimization | Perform the optimization described in silicon's PR #756. You must ensure that the necessary conditions for the optimization are met. | no | 0 |
| useZ3API | Use the Z3 API in silicon. | no | 0 |
| statsFile | Path where the generated stats.json file will be stored | no | /stats/ |