FIELD NOTES TOPIC
iris-lean
1 note, newest first.
Harnessing Code Agents for Automatic Software Verification
A new method using a general language model code agent and a verification harness proves all targeted lemmas in Iris, Rust's standard libraries, and unfinished Lean 4 port of Iris, achieving full coverage without any…
