Owner

viperproject

12 indexed repositories · View on GitHub

gobra
Gobra is an automated, modular verifier for Go programs, based on the Viper verification infrastructure.

Scala · 189 stars
silicon
Symbolic-execution-based verifier for the Viper intermediate verification language.

Scala · 145 stars
silver
Definition of the Viper intermediate verification language.

Scala · 100 stars
carbon
Verification-condition-generation-based verifier for the Viper intermediate verification language.

Scala · 38 stars
viperserver
HTTP server that manages verification requests to different tools from the Viper tool stack.

Scala · 16 stars
viper-ide
This is the main repository for the Viper IDE extension for VS Code.

TypeScript · 14 stars
VerifiedSCION
Verifying the SCION architecture using Gobra

Go · 12 stars
gobra-ide
VSCode Plugin for Gobra

TypeScript · 11 stars
vs-verification-toolbox
Useful component to build VS Code extensions for verifiers.

TypeScript · 6 stars
gobra-action
Github Action to verify Go code with Gobra directly in a CI workflow

Shell · 2 stars
gobra-libs
Standard library for the Gobra verifier for Go. Contains definitions and lemmas useful for verifying large projects.

Python · 2 stars
tutorial
This repo contains the sources of the official Viper tutorial. Feel free to submit your fixes and additions via pull requests. Please rep...

JavaScript · 0 stars

Beginner friendly Everything

Open All

quantifiedExp does not apply its `ignore` parameter, unlike `quantified` Open

Difficulty 3/5 1-2 days Newbie friendliness 68/100

viperproject/silicon#1006 · Opened Sep 9, 2026
Termination measures are not checked for closure spec calls Open

soundness termination-checking

Difficulty 4/5 3-5 days Newbie friendliness 48/100

viperproject/gobra#1106 · Opened Sep 4, 2026
Termination measures of interface methods are not checked across package boundaries Open

soundness termination-checking

Difficulty 5/5 Over a week Newbie friendliness 30/100

viperproject/gobra#1105 · Opened Sep 4, 2026
Recursive function plus quantifier that triggers on the function results in matching loop Open

Difficulty 5/5 Over a week Newbie friendliness 35/100

viperproject/silicon#1004 · Opened Aug 25, 2026
Carbon can prove false Open

Difficulty 4/5 3-5 days Newbie friendliness 48/100

viperproject/carbon#591 · Opened Aug 18, 2026
Type checker crashes on addressing an element of a slice obtained from a map lookup Open

Difficulty 2/5 1-3 hours Newbie friendliness 78/100

viperproject/gobra#1097 · Opened Aug 17, 2026
Confusing reason/offending position ID with sequencing operation Open

Difficulty 4/5 3-5 days Newbie friendliness 48/100

viperproject/silver#928 · Opened Aug 15, 2026
Tutorial.md is severely limited compared to actual *.g4 files Open

Difficulty 4/5 3-5 days Newbie friendliness 45/100

viperproject/gobra#1093 · Opened Aug 15, 2026
Termination plugin fails with unclear error Open

bug termination plugin

Difficulty 4/5 3-5 days Newbie friendliness 48/100

viperproject/silver#925 · 1 comment · Opened Aug 10, 2026
Unclear error message when injectivity check fails in a subexpression Open

Difficulty 4/5 3-5 days Newbie friendliness 48/100

viperproject/silicon#997 · Opened Aug 10, 2026
Quantified predicate permission over freshly-allocated pointers fails injectivity check, even for provably-fresh allocations Open

Difficulty 4/5 3-5 days Newbie friendliness 45/100

viperproject/gobra#1060 · Opened Jul 31, 2026
Pure interface method's definitional axiom does not fire through interface dispatch when the method recurses through another interface-typed call Open

Difficulty 4/5 3-5 days Newbie friendliness 48/100

viperproject/gobra#1059 · Opened Jul 30, 2026
Cannot prove non-nil after make Open

Difficulty 4/5 3-5 days Newbie friendliness 45/100

viperproject/gobra#1052 · 2 comments · Opened Jul 19, 2026
It is unnecessarily hard to prove injectivity of slices of struct pointers Open

Difficulty 4/5 3-5 days Newbie friendliness 45/100

viperproject/gobra#1051 · Opened Jul 18, 2026
Anonymous methods Open

enhancement

Difficulty 5/5 Over a week Newbie friendliness 35/100

viperproject/silver#922 · Opened Jul 13, 2026
Forward goto after variable declaration causes crash Open

Difficulty 4/5 3-5 days Newbie friendliness 35/100

viperproject/silicon#991 · Opened Jul 10, 2026
Doing bitvector work in cvc5 puts the solver in a broken state Open

Difficulty 4/5 3-5 days Newbie friendliness 48/100

viperproject/silicon#990 · Opened Jul 10, 2026
Conjunction of abstract functions is not able to be asserted Open

Difficulty 4/5 3-5 days Newbie friendliness 52/100

viperproject/carbon#588 · Opened Jul 10, 2026
Conjunction of abstract functions is not able to be asserted Open

Difficulty 4/5 3-5 days Newbie friendliness 45/100

viperproject/silicon#989 · 1 comment · Opened Jul 10, 2026
Irreducible CFG error reporting is not useful Open

Difficulty 5/5 Over a week Newbie friendliness 35/100

viperproject/silver#918 · Opened Jun 23, 2026
Proposed annotation: verified — heap-free function postconditions as domain axioms Open

encoding enhancement syntax

Difficulty 5/5 Over a week Newbie friendliness 35/100

viperproject/gobra#1037 · 9 comments · Opened Jun 14, 2026
Inconsistent treatment of recursive function postconditions Open

Difficulty 4/5 3-5 days Newbie friendliness 48/100

viperproject/silver#913 · Opened May 21, 2026
Invalid Triggers via Subslicing Open

bug encoding invalid triggers

Difficulty 4/5 3-5 days Newbie friendliness 42/100

viperproject/gobra#1030 · 1 comment · Opened May 13, 2026
Wands are not checked for self-framingness Open

magic-wands

Difficulty 4/5 3-5 days Newbie friendliness 48/100

viperproject/silicon#974 · Opened May 7, 2026
Gobra does not immediately realize semantics of copying arrays by assignment Open

bug encoding incompleteness

Difficulty 3/5 1-2 days Newbie friendliness 48/100

viperproject/gobra#1027 · 6 comments · Opened May 6, 2026
Can prove nil-ness and non-nilness from struct predicate Open

documentation

Difficulty 4/5 3-5 days Newbie friendliness 45/100

viperproject/gobra#1025 · 5 comments · Opened May 4, 2026
Wildcard permissions don't work inside predicate bodies Open

Difficulty 4/5 3-5 days Newbie friendliness 38/100

viperproject/carbon#584 · Opened Apr 23, 2026
Carbon does not "frame" trigger-matching heap-dependent functions which depend on QPs (without help) Open

Difficulty 5/5 Over a week Newbie friendliness 35/100

viperproject/carbon#583 · 1 comment · Opened Apr 17, 2026
Diagnostics count on errors is global Open

viperproject/viper-ide#566 · 1 reaction · 2 assignees · Opened Mar 26, 2026
Incorrect encoding of relational predicates Open

SIF

Difficulty 4/5 3-5 days Newbie friendliness 48/100

viperproject/silver#907 · 1 comment · Opened Mar 24, 2026
Clean up createRequire workarounds once VS Code ESM support is fixed Open

Difficulty 4/5 3-5 days Newbie friendliness 35/100

viperproject/vs-verification-toolbox#227 · Opened Mar 5, 2026
Incomplete Slice Allocation Spec Open

encoding enhancement

Difficulty 3/5 1-2 days Newbie friendliness 52/100

viperproject/gobra#1007 · Opened Mar 4, 2026
Parser Error for Reserved Keywords Open

enhancement parsing

Difficulty 4/5 3-5 days Newbie friendliness 45/100

viperproject/gobra#1005 · Opened Mar 2, 2026
Allow impure assertions for `assert by` Open

feature-request

Difficulty 3/5 1-2 days Newbie friendliness 38/100

viperproject/gobra#999 · Opened Feb 24, 2026
Invalid SMT Encoding Open

bug encoding

Difficulty 4/5 3-5 days Newbie friendliness 35/100

viperproject/gobra#997 · Opened Feb 20, 2026
Unintuitive semantics for mixed non-hyper-predicates and hyper-predicates Open

documentation SIF

Difficulty 5/5 Over a week Newbie friendliness 30/100

viperproject/gobra#996 · 10 comments · Opened Feb 17, 2026
Using `rel(t,0) < rel(t,1)` with implication in SIF mode causes an error. Open

SIF

Difficulty 4/5 3-5 days Newbie friendliness 32/100

viperproject/gobra#994 · 2 comments · Opened Feb 11, 2026
Assert might fail even defined before the `ghost if ` block in hypermode using `rel()` Open

SIF

Difficulty 4/5 3-5 days Newbie friendliness 45/100

viperproject/gobra#993 · 3 comments · Opened Feb 6, 2026
Cross execution access bug in `rel()` and `ghost if` blocks Open

SIF

Difficulty 4/5 3-5 days Newbie friendliness 35/100

viperproject/gobra#992 · 2 comments · Opened Feb 4, 2026
Incompleteness: Asserting a syntactically identical assertion fails Open

enhancement

Difficulty 4/5 3-5 days Newbie friendliness 35/100

viperproject/silver#902 · 2 comments · Opened Jan 28, 2026
`rel` Expressions in Triggers Open

bug SIF

Difficulty 4/5 3-5 days Newbie friendliness 35/100

viperproject/silver#901 · 1 comment · Opened Jan 28, 2026
Encoding bug when using `rel()` and a wrapper Open

SIF

Difficulty 4/5 3-5 days Newbie friendliness 35/100

viperproject/gobra#987 · 1 comment · Opened Jan 27, 2026
Asserting after assuming quantifier with heap-dependent trigger fails Open

bug incompleteness quantified-permissions

Difficulty 4/5 3-5 days Newbie friendliness 38/100

viperproject/silicon#959 · 2 comments · Opened Jan 15, 2026
Floating Point Literals Open

encoding enhancement

Difficulty 5/5 Over a week Newbie friendliness 30/100

viperproject/gobra#980 · 1 comment · Opened Dec 10, 2025
A potential bug in how Silicon handles loop invariant Open

Difficulty 4/5 3-5 days Newbie friendliness 38/100

viperproject/silicon#957 · 2 comments · Opened Dec 9, 2025
Crash when using a compound data structure in a closure encoding Open

Difficulty 4/5 3-5 days Newbie friendliness 45/100

viperproject/gobra#978 · Opened Dec 3, 2025
Confusing error message if ADT type and constructor named alike Open

Difficulty 4/5 3-5 days Newbie friendliness 45/100

viperproject/gobra#977 · Opened Dec 3, 2025
Dollars in argument identifiers confuse tab completion Open

Difficulty 3/5 1-2 days Newbie friendliness 45/100

viperproject/viper-ide#533 · Opened Nov 27, 2025
Internal function preconditions not assumed in wand-related scenario Open

incompleteness

viperproject/silicon#951 · 1 assignee · Opened Nov 24, 2025
Heap dependent function triggering Open

viperproject/silver#895 · 1 assignee · Opened Nov 5, 2025

Showing the newest 100

This page lists what was indexed most recently. Advanced filter has the whole inventory, narrowed by language, difficulty and how long a task takes.

Open advanced filter

viperproject

Showing the newest 100

Get new issues in your inbox