Should Kani Rust Verifier, CodeQL, and code coverage testers be added to GitHub Actions testing for SQLPage?

[bluelightspirit]

Should Kani Rust Verifier be added to GitHub Actions testing for SQLPage?

https://github.com/model-checking/kani says that Kani is useful for checking both safety and correctness of Rust code.

1. Safety: Kani automatically checks for many kinds of undefined behavior. This makes it particularly useful for verifying unsafe code blocks in Rust, where the "unsafe superpowers" are unchecked by the compiler.
2. Correctness: Kani automatically checks panics (e.g. unwrap() on None), arithmetic overflows, and custom correctness properties, either in the form of assertions (assert!(...)) or function contracts.

The latest GitHub Actions only test Docker, Playwright, Hurl, and 6 databases from what I can see at https://github.com/sqlpage/SQLPage/actions/runs/35495163231 - as well as Windows and Rust Crate I suppose. However, Kani is not included. Salvo added Kani through dependabot recently on July 13, 2026 from my understanding at salvo-rs/salvo#1670 by merging such change. More details of this is found at ParkMyCar/compact_str#480; plus safety and correctness may cover the part of having more assistance with code reviewing rather than eyeball thousands to millions of lines of code (I don't know how many SQLPage has total).

https://github.com/sqlpage/SQLPage?tab=contributing-ov-file#end-to-end-tests seems Playwright is used to test web and maybe database functionality more than Rust code safety and correctness Kani claims to check.

<<<<<<<<<<<<<<

Should CodeQL be added to GitHub Actions testing for SQLPage?

CodeQL discovers vulnerabilities across a codebase. https://codeql.github.com/
Some resources to learn CodeQL are found at https://github.com/advanced-security/awesome-codeql

salvo-rs/salvo@9beb091 - if you click on the green checkmark next to 12 / 12 you can see CodeQL is Salvo's first test. Salvo is a popular Rust-based web framework. There is also some code coverage tests they do there, but I probably would consider that out of scope for SQLPage unless told otherwise.

actix/actix-web@ad0d97b - for actix-web, which SQLPage is powered by, CodeQL also is part of the test suite for actix-web, if you click the red X next to 12 / 16.

<<<<<<<<<<<<<

Should Rust code coverage tests be done for SQLPage?

https://github.com/taiki-e/cargo-llvm-cov and https://github.com/xd009642/tarpaulin are some options. Salvo appears to use codecov from https://github.com/codecov/codecov-action (salvo-rs/salvo@9beb091 - if you click on the green checkmark next to 12 / 12). However, Codecov is primarily written in Python. Tarpaulin is for the Cargo build system while cargo-llvm-cov is for the LLVM source-based code coverage.

Tarpaulin is good for this specifically versus cargo-llvm-cov Perplexity says:
When Tarpaulin still makes sense
Choose or retain Tarpaulin when you specifically need one of these:

1. Existing project configuration and CI are built around .tarpaulin.toml.
2. The project has a known-good Linux/x86-64 ptrace setup.
3. Its process-tracing behavior works better for a particular workload than LLVM profiling does.
4. You want its established configuration, exclusions, Docker image, or direct coverage-service workflow compatibility. Tarpaulin supports report formats including JSON, XML, HTML, and LCOV, and documents Codecov/Coveralls integrations.

Perhaps it is best to use all 3 of these, but I'm not necessarily an expert in being able to figure out what code coverage tests are best for Rust coding since my coding experience is mostly in Java and Python...

[lovasoa]

Hi ! Did you encounter actual safety and correctness issues in sqlpage ? If so, then please report those !