# 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