LOGOS takes its name from the Greek λόγος (logos), meaning “reason” or “account.” The name reflects its purpose: generating logical specifications of function behavior as ACSL contracts for C.
LOGOS provides a skill for authoring ACSL function contracts and a Python wrapper that inserts those contracts into C source and optionally verifies the result with Frama-C WP. The agent decides contract semantics; the wrapper handles rendering, annotation, verification, and reports.
The input must already contain ACSL. Input programs, case studies, generated contracts, annotated source, and proof reports belong in external project directories and are not distributed in this repository.
For AutoDeduct integration, start with the AutoDeduct LLM branch and its setup and usage guide. AutoDeduct calls LOGOS to generate contracts, apply them, verify with Frama-C, and consume the verification report.
| Workflow | How it runs | Guide |
|---|---|---|
| AutoDeduct LLM with local tools | Host Codex uses the local LOGOS skill; AutoDeduct runs the wrapper and Frama-C locally | AutoDeduct local setup |
| AutoDeduct LLM with Docker verification | AutoDeduct extracts the image's skill for host Codex, then runs the wrapper and Frama-C in Docker | AutoDeduct Docker setup |
| Standalone LOGOS | Ask Codex to author contracts, then apply and optionally verify them with the local wrapper | Standalone usage |
AutoDeduct's LLM workflow runs Codex on the host. Running Codex inside its container is unsupported. Docker is optional when verification dependencies are installed locally.
- Setup: Python, libclang, verification tools, and platform support.
- Standalone usage: agent prompts, contract files, and wrapper commands.
- AutoDeduct integration: host launcher, local/Docker runtimes, and the JSON handoff.
- Verification and scope: proof results, reports, limitations, and artifact policy.
- Skill instructions: instructions and contract schema used by the agent.
skill/SKILL.md: contract-generation skill.skill/scripts/generate_acsl.py: Python wrapper entry point.skill/scripts/acsl_tool/: parsing, rendering, annotation, and verification.tests/: automated checks.scripts/measure_codex_contracts.py: measurement utility.docs/: user guides.
LOGOS's original software is licensed under the GNU General Public License
v2.0 only (GPL-2.0-only). See LICENSE for the full terms and
NOTICE for licensing scope and separately owned material.