---
# System prepended metadata

title: 'FFI projects (Prusti, Gobra, Nagini, ...), minutes 2022-09-07'

---

# FFI projects (Prusti, Gobra, Nagini, ...), minutes 2022-09-07

- share specs of FFI interfaces
  - Python C extension API
  - JNI API
  - ...
- common specification patterns?
  - e.g. deal with refcounts (or acquire/release pairs) with obligations
- FFI generators
  - the native code is generated automatically, the native library is not aware of it
  - e.g. Go's Cgo, Python's `ctypes`, Luajit's `ffi` package
  - in this case, extern specs need to be attached to the native library and assume(?) that the FFI generator generates correct glue code
- decide on a common C/native specification language
  - VeriFast ? - separation logic based, might work with Viper
