Read and write exact bytes
Use snapshot or serializable isolation, point reads, bounded scans, mutations, singleton commits, and atomic commit groups.
An embedded database for Ada applications.
Flyology.DB is a transactional key-value store that runs in your process. Read and write byte keys and values with snapshot or serializable isolation. The library persists its commit log and checkpoints to local Files or S3-compatible object storage, so a new process can reopen the same database.
Ada applicationopens transactions · reads · writes
calls
Flyology.DBisolation · commit log · checkpoints
persists to
Object storagelocal Files or a caller-owned S3 client
A new process can reopen from the same durable objects.
Data modelByte keys and values, organized into column families.
StorageLocal Files or a caller-owned S3-compatible client.
DeploymentEmbedded library, one writer, optional read-only replicas.
Status0.1.0-dev, experimental, no production qualification.
Using the database
Create, transact, checkpoint, reopen.
The public API follows an explicit lifecycle. Your application supplies storage, identities, and limits; Flyology.DB owns transactional state and persisted database objects.
Create or open
Bind a Files or S3-compatible storage client, define persisted limits and column families, then create a database or open its existing durable state.
Read and write
Begin a snapshot or serializable transaction, get and scan keys, stage mutations, and commit one transaction or an atomic group.
Checkpoint and reopen
Flush changed families into immutable runs, close every owner, and reconstruct the database from object storage in a new process.
Current profile
The database path that works today.
The experimental profile joins transactions, column families, checkpointing, compaction, recovery, and provider-neutral storage. It leaves scheduling, identities, retention, and infrastructure policy with the application.
Checkpoint deliberately
Flush changed families and compact exact caller-selected runs. Current operations retain predecessors and choose no deletion policy.
Reopen from authority
Discard process-local state, construct fresh owners, and rebuild one complete authenticated view from object storage.
Append stable namespaces
Add a higher never-reused family ID over a retained checkpoint, including a later authenticated commit suffix.
Drive bounded operations
Choose synchronous calls or caller-owned completion sets and buffers without changing publication certainty.
Keep transport outside DB
Bind provider-neutral Files storage or caller-owned authenticated S3-compatible clients. The database adds no endpoint or retry policy.
How durability works
A commit becomes visible in one controlled step.
Flyology.DB first stores a complete immutable commit object. Flyology.DB then uses compare-and-swap to replace the exact metadata version that the transaction read. If another writer has already changed that metadata version, the stale writer cannot replace the current database state.
Store the complete commit
Write the transaction identities, mutations, lengths, and integrity data as one immutable object before the commit becomes visible.
Publish from the version read
Replace metadata only when the stored version still matches the transaction's predecessor. This is the compare-and-swap publication step.
Resolve an uncertain response
If the storage response is lost, read the durable state using the original receipt. Never submit the application transaction again under a new identity.
Assurance boundary
Tests, models, and proofs cover different questions.
Executed evidence supports the exact reviewed source and dependency tree. It does not convert the experimental profile into a production or performance claim.
- Deterministic workflowRepository, engine, client, crash-recovery, Files, showcase, and TidesDB gates.
- Six-provider matrixRustFS, SeaweedFS, MinIO, Flyology memory, Files, and SQLite across three repetitions.
- TLA+ and TLAPSBounded state exploration, negative probes, recovery witnesses, proofs, and four maintained Ada trace replays.
- SPARKSelected format, policy, bounds, and transition units prove without assumptions or justified checks.
Create a local database, then reopen it.
The maintained Files example begins with one transaction and grows into checkpoint recovery and a second column family. It leaves the durable root in your custody for inspection.