verus-lang verus issues

verus-lang / verus

Verified Rust for low-level systems code

MIT License

1.25k stars 72 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Fix state machine example in book

#1358 suaviloquence closed 3 days ago
1
Fix typo in state machines book

#1357 suaviloquence closed 4 days ago
1
New attribute-based syntax for exec function specifications

#1356 Chris-Hawblitzel opened 5 days ago
1
Broadcast group with non-broadcast items generates ill-typed AIR

#1355 matthias-brun opened 6 days ago
0
Add fibonacci example to the Guide to illustrate how spec, proof, and exec code work together

#1354 parno opened 6 days ago
1
replace the after_crate_root_parsing callback with after_expansion, fixes #1331

#1353 utaal opened 1 week ago
0
Update README.md to create a list of examples of using Verus

#1352 parno opened 1 week ago
0
Add white outlines to the logos to look nicer on dark mode

#1351 jaybosamiya-ms opened 1 week ago
0
Document the `all_spec` functionality for assert-by-compute

#1350 parno closed 1 week ago
0
Timeouts due to sequence axioms

#1349 matthias-brun opened 1 week ago
0
call_requires/call_ensures don't have expected behavior for "normal" function calls

#1348 tjhance opened 1 week ago
0
spurious 'let variables in trigger' error

#1347 tjhance opened 1 week ago
0
can't implement trait (e.g., Clone) for recursive datatype that uses Option

#1346 tjhance opened 1 week ago
1
Cast bool to integer?

#1345 ziqiaozhou opened 1 week ago
1
Add allow(non_snake_case) to __VERUS_CONST_BODY__

#1344 ziqiaozhou closed 1 week ago
0
bugfix: handle trigger annotations for nested quantifiers

#1343 tjhance closed 1 week ago
0
get_impl_paths more exhaustive checks

#1342 tjhance opened 1 week ago
0
make trait method resolution more exhaustive, fixes #1312

#1341 tjhance opened 1 week ago
0
Make macos_allow_gatekeeper a bit safer

#1340 tchajed opened 2 weeks ago
1
Field-less enums: an issue potentially introduced with the version bump to 1.79

#1339 y1ca1 opened 2 weeks ago
1
Make it more pleasant to write a proof-by-computation over a range of values

#1338 parno closed 1 week ago
0
internal error: CastToInteger should have been removed before here

#1337 jonhnet opened 3 weeks ago
0
Can't prove `let c = a && b; assert(c == a && b);`

#1336 zhengyao-lin closed 3 weeks ago
3
get_impl_paths/recursion-checking does not handle Sync/Send inference

#1335 tjhance opened 3 weeks ago
2
const in array types causes rustc error

#1334 tjhance opened 3 weeks ago
1
Failed precondition error message doesn't point to source code

#1333 nwtnni opened 3 weeks ago
1
Panic asserting `call_ensures` about `clone`

#1332 hayley-leblanc closed 3 weeks ago
2
Please avoid the after_crate_root_parsing driver callback

#1331 bjorn3 opened 3 weeks ago
1
Rust 1.82.0

#1330 utaal opened 3 weeks ago
0
Add some multiset-related lemmas

#1329 zeldovich closed 6 days ago
0
Copy trait impl is not generated in lifetime checking when using #[derive(Copy)]

#1328 ziqiaozhou closed 3 weeks ago
1
ill-typed AIR code, when using reveal

#1327 zeldovich opened 3 weeks ago
0
Add saturate_add && option::map

#1326 ziqiaozhou closed 3 weeks ago
0
V1.82

#1325 ziqiaozhou closed 3 weeks ago
0
Incorrect warning with `#![verus::trusted]`

#1324 matthias-brun closed 4 weeks ago
0
allow #[verifier(external_body)] again on consts

#1323 utaal closed 4 weeks ago
4
`external_body` consts panic the verifier

#1322 matthias-brun opened 4 weeks ago
0
Incorrect warning when using `global size_of usize == n`

#1321 matthias-brun closed 4 weeks ago
0
Add --log smt-transcript option

#1320 Chris-Hawblitzel closed 3 weeks ago
0
Add SMTLIB field-update support to AIR

#1319 tim-rohde closed 5 days ago
0
Update to verusfmt v0.5.0

#1318 jaybosamiya-ms closed 1 month ago
0
Represent large sequence literals using the recently added ArrayLiteral support

#1317 parno closed 1 month ago
0
update default z3 version to 4.13.0 and fix the runtime version check

#1316 Catoverflow opened 1 month ago
4
Consolidate code for classifying 'external' items

#1315 tjhance closed 4 weeks ago
0
Remove warning on trigger if the broadcast proof function does not have a parameters?

#1314 ziqiaozhou closed 2 weeks ago
5
Verus not respecting --no-solver-version-check flag

#1313 Catoverflow closed 1 month ago
8
buggy behavior for tuple clone

#1312 tjhance opened 1 month ago
1
lifetime-generate can't handle Arc/Rc/Box being used as receiver

#1311 tjhance opened 1 month ago
0
[lifetime-generate] Trait bound is not satisfied (external impl of a trait)

#1310 BLepers opened 1 month ago
1
external_trait_specification: consistency check causes panic

#1309 BLepers opened 1 month ago
1