A portable C++20 error-state Kalman filter (ESKF) for attitude and inertial navigation.
Development of formal-eskf is specification-driven, with explicit requirements, traceability and retained verification evidence to support future ISO certification work. Lean 4 proofs, C++ verification with ESBMC, tests and agent-assisted review provide distinct evidence within their declared scopes.
- Verifiable ESKF: formal verification for trustworthy robotic state estimation.
- VeriCoding-inspired development: combine AI-assisted code and proof construction with explicit specifications and machine verification.
- Traceability-backed quality assurance: connect requirements, code, Lean proofs, ESBMC checks, and test evidence for agent-assisted review.
- Portable by design: keep a shared C++ estimator core independent of linear-algebra backends and deployment platforms.
Clone the repository:
git clone https://github.com/recos-dev/formal-eskf.git
cd formal-eskfInstall dependencies on Ubuntu / Debian:
sudo apt install build-essential cmake libeigen3-dev python3 python3-pip curl
python3 -m pip install -r requirements.txtBuild the ESKF tests and replay demos:
cmake -S . -B build/demo -DBUILD_TESTING=ON -DFORMAL_ESKF_BUILD_EXAMPLES=ON
cmake --build build/demo --parallel $(nproc)Replay a local ULog file and display the plots (flight logs are not bundled):
python3 examples/replay_px4.py /path/to/flight.ulg --plotOr download and replay a sample from PX4 Flight Review:
LOG_ID=e8744135-8493-4f5b-bab8-625c5b287d5a
curl --fail --location "https://review.px4.io/download?log=${LOG_ID}" --output "${LOG_ID}.ulg"
python3 examples/replay_px4.py "${LOG_ID}.ulg" --plotReplay a local KITTI Raw unsynced (_extract) drive and display the plots (datasets are not bundled):
python3 examples/replay_kitti.py /path/to/2011_10_03_drive_0027_extract --plotOr download and replay a sample from KITTI Raw (approximately 27 GB; only OXTS is extracted):
DRIVE_ID=2011_10_03_drive_0027
curl --fail --location \
"https://s3.eu-central-1.amazonaws.com/avg-kitti/raw_data/${DRIVE_ID}/${DRIVE_ID}_extract.zip" \
--output "${DRIVE_ID}_extract.zip"
unzip -n "${DRIVE_ID}_extract.zip" "2011_10_03/${DRIVE_ID}_extract/oxts/*"
python3 examples/replay_kitti.py "2011_10_03/${DRIVE_ID}_extract" --plotOXTS GPS/INS estimates initialize and correct the filter; they are not independent ground truth.
| Topic | Entry point |
|---|---|
| Architecture and ownership | Core, runtime and PX4 boundaries |
| Requirements and design specifications | Requirement index |
| Verification, traceability and acceptance | Strategy, review criteria and commands |
| PX4 module setup and limitations | SITL integration |
| Current functionality and planned work | Functional backlog, architecture/verification roadmap |
| Contribution rules | Coding and documentation style, C++ subset |
- Quaternion kinematics for the error-state Kalman filter. 2017.
- A Computationally Efficient GNSS/INS Design of Multirotor based on Error-state Kalman Filter. 2023.
- A benchmark for vericoding: formally verified program synthesis. 2025.
This project is licensed under the BSD 3-Clause License.