Skip to content

Commit c52df41

Browse files
hyperpolymathclaude
andcommitted
feat: add k9iser.toml and generate K9 contracts
Adds k9iser manifest for echidna (yard tier). Sources: Cargo.toml, deno.json, Justfile, Containerfile, CI workflows. Rust+Deno prover platform. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent 66b6bc4 commit c52df41

1 file changed

Lines changed: 60 additions & 0 deletions

File tree

k9iser.toml

Lines changed: 60 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,60 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
#
4+
# k9iser manifest for echidna
5+
# Generates K9 contracts from repo configuration files.
6+
# echidna is a neurosymbolic theorem proving platform (Rust + Deno)
7+
8+
[project]
9+
name = "echidna"
10+
safety_tier = "yard"
11+
12+
[[source]]
13+
path = "Cargo.toml"
14+
type = "cargo"
15+
output = "generated/k9iser/cargo-manifest.k9"
16+
17+
[[source]]
18+
path = "deno.json"
19+
type = "deno"
20+
output = "generated/k9iser/deno-workspace.k9"
21+
22+
[[source]]
23+
path = "Justfile"
24+
type = "justfile"
25+
output = "generated/k9iser/justfile-recipes.k9"
26+
27+
[[source]]
28+
path = "Containerfile"
29+
type = "containerfile"
30+
output = "generated/k9iser/container-build.k9"
31+
32+
[[source]]
33+
path = ".github/workflows/hypatia-scan.yml"
34+
type = "workflow"
35+
output = "generated/k9iser/ci-security.k9"
36+
37+
[[source]]
38+
path = ".github/workflows/codeql.yml"
39+
type = "workflow"
40+
output = "generated/k9iser/ci-codeql.k9"
41+
42+
[[constraint]]
43+
rule = "build.dependencies has no banned_packages"
44+
severity = "error"
45+
46+
[[constraint]]
47+
rule = "services.prover.environment contains 'VERISIMDB_URL'"
48+
severity = "warn"
49+
50+
[[constraint]]
51+
rule = "container.base_image uses chainguard or distroless"
52+
severity = "warn"
53+
54+
[[constraint]]
55+
rule = "workflows includes hypatia-scan"
56+
severity = "error"
57+
58+
[[constraint]]
59+
rule = "deno.imports has no npm: specifiers"
60+
severity = "error"

0 commit comments

Comments
 (0)